[First implemementation of generic catamorphisms
martin.hofmann@uni-bamberg.de**20091211151209] move ./src/Igor2/RuleDevelopment/UniProp.hs ./src/Igor2/RuleDevelopment/ListCata.hs
hunk ./src/IOInterpreter.hs 48
+        lift (putStrLn m)
+        setImportsQ [("Prelude", Nothing)
+                    ,("Generics.Pointless.Combinators",Nothing)
+                    ,("Generics.Pointless.Functors",Nothing)
+                    ,("Generics.Pointless.RecursionPatterns", Nothing)
+                    ]
+        lift (putStrLn m)
+        ms <- getLoadedModules
+        lift (print ms)
hunk ./src/IOInterpreter.hs 58
-        setImportsQ [("Prelude", Nothing)]
hunk ./src/IOInterpreter.hs 60
+-- force evaluation to catch errors
hunk ./src/Igor2/RuleDevelopment.hs 11
-import Igor2.RuleDevelopment.UniProp
+import Igor2.RuleDevelopment.Cata
hunk ./src/Igor2/RuleDevelopment.hs 55
-        fs <- ifIsSet inEnhanced (foldUProp r) []  
+        fs <- ifIsSet inEnhanced (cataIntro r) []  
addfile ./src/Igor2/RuleDevelopment/Cata.hs
hunk ./src/Igor2/RuleDevelopment/Cata.hs 1
+{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
+module Igor2.RuleDevelopment.Cata where
+
+import Igor2.Data.IgorMonad
+import Igor2.Data.CallDependencies
+import Igor2.Data.Rules
+import Igor2.RuleDevelopment.ListCata
+
+import Syntax
+import Igor2.Ppr
+import Igor2.Logging
+
+import Control.Monad.Error
+import Data.Either
+import Generics.Pointless.Functors (Mu)
+import Generics.Pointless.Combinators ((\/), _L)
+import Generics.Pointless.RecursionPatterns (cata)
+
+cataIntro :: CovrRule -> IM [(CovrRules,[Call])]
+cataIntro cr = do
+    waypointS $ text "Catamorphism Introduction"
+    llogNO  $ text "Check if 'cata' applies to: " <^> pretty cr
+    if hasListT . lastArg $ cr then listCata cr
+     else do b <- (applyC $ matches (lastArg cr) muVar) :: (IM (Either String Bool))
+             if either (error) id b then genericCata cr
+              else noCata "Wrong Type"
+
+
+lastArg  = last . lhs . crul
+initArgs = init . lhs . crul
+
+genericCata :: CovrRule -> IM [(CovrRules,[Call])]
+genericCata cr = do   
+    llogWA  $ text "Check if 'cata' applies to: " <^> pretty cr
+    evi   <- breakupM cr
+    ctors <- maybe (return Nothing) ctorsOf $ dataName . typeOf . lastArg $ cr
+    (maybe (fail "No Partition possible") return (ctors >>= partByCtors evi) >>= mkCata cr) `catchError` \e -> noCata $ "Universal Property not satisfied!" ++ e
+
+partByCtors :: [CovrRule] -> [Name] -> Maybe [[CovrRule]]
+partByCtors rs ns = mapM (byCtor rs) ns
+    where
+    byCtor rs n = let rs' = filter ((hasCtor n) . lastArg) rs in
+                  trace ((showp rs) ++ "\n" ++ (show n) ++ "\n" ++(showp rs')) $ if null rs' then Nothing else Just rs'
+    hasCtor n (TVarE _ _)        = True
+    hasCtor n (TConE n' _)       = n == n'
+    hasCtor n (TAppE e _ _)      = hasCtor n e
+    hasCtor n (TInfixE _ c _ _ ) = hasCtor n c
+    hasCtor n  _                 = False 
+
+mkCata :: CovrRule -> [[CovrRule]] -> IM [(CovrRules,[Call])]
+mkCata cr parts = do
+--     let crty = arrowTy
+     mfns <- mapM abduceIOs parts
+     mfcr <- mapM coverAll mfns
+     let mfuns = map (mkMediators (initArgs cr)) mfcr     
+     let fExp = foldTAppE  cataEx [botEx, (mkInfxs mfuns)]
+     let cr' = modifycrul cr (\r -> rule (init . lhs $ r) fExp)
+     let clls = map  (\mfn -> (name cr',mfn, LT)) mfns 
+     return [(covrRules (cr':mfcr),clls)]
+     where
+     mkMediators as r = let fty = (map typeOf) . lhs . crul $ r
+                            fex = tConE (name r) fty in
+                            foldTAppE fex as
+     mkInfxs [l,r] = let lty = typeOf l
+                         rty = typeOf r
+                         ety = foldAppT (conT ''Either) [head . unArrowT $ lty,head . unArrowT $ rty]
+                     in  tInfixE (tConE '(\/) [lty,rty,ety,last . unArrowT $ lty]) l r 
+     mkInfxs (l:rs)= let r = mkInfxs rs
+                         lty = typeOf l
+                         rty = typeOf r
+                         ety = foldAppT (conT ''Either) [head . unArrowT $ lty,head . unArrowT $ rty]
+                     in  tInfixE (tConE '(\/) [lty,rty,ety,last . unArrowT $ rty]) l r 
+     
+
+abduceIOs :: [CovrRule] -> IM Name
+abduceIOs crs = mapM abduceIO crs >>=  addIO . rules
+
+abduceIO :: CovrRule -> IM Rule 
+abduceIO cr = case subterms carg of
+               [] -> return . iorule $  wild
+               as -> do cargs <- mapM mkCArg as
+                        return . iorule . nestedTupE $ cargs
+    where
+    args = initArgs cr
+    carg = lastArg cr 
+    wild = tWildE "a" (typeOf carg)
+    iorule ca = rule (args ++ [ca])(rhs . crul $ cr)
+    mkCArg a 
+        | (typeOf a)==(typeOf carg) = evalIO (name cr) (args ++ [a]) >>= 
+                                       maybe (fail "Insufficient support in Examples") (return . id)
+        | otherwise                 = return a
+    
+nestedTupE [a]    = a
+nestedTupE [a,b]  = tTupE [a,b]
+nestedTupE (x:xs) = tTupE [x,nestedTupE xs]
+        
+noCata s = llogNO (text "Catamorphism not applicable: " <+> text s) >> return []
+
+muVar = tVarE "a" $ forallT ["a"][ (''Mu,"a")] (varT "a")
+botEx = TConE ('_L) (varT "a")
+cataEx = TConE ('cata) $ ForallT [ mkName "a", mkName "b"]
+                                 [ AppT (conT ''Mu) (varT "a")
+                                 , AppT (conT (mkName "Generics.Pointless.Functors.Functor")) (AppT (conT (mkName "Generics.Pointless.Functors.PF")) (varT "a"))] 
+                                 (AppT (AppT ArrowT (varT "a")) 
+                                       (AppT (AppT ArrowT (AppT (AppT ArrowT (AppT (AppT (conT (mkName "Generics.Pointless.Functors.F")) (varT "a")) (varT "b"))) (varT "b"))) (AppT (AppT ArrowT (varT "a")) (varT "b"))))
+                                 
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 2
-module Igor2.RuleDevelopment.UniProp where
+module Igor2.RuleDevelopment.ListCata (
+
+    listCata
+    
+    )where
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 13
-import Control.Arrow
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 24
-foldUProp :: CovrRule -> IM [(CovrRules,[Call])]
-foldUProp cr = do
-    waypointS $ text "Universal Property of 'fold'"
-    llogNO (text "Check if 'fold' applies to: " <^>
-            pretty cr)
+listCata :: CovrRule -> IM [(CovrRules,[Call])]
+listCata cr = do
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 28
-    maybe (naiveMap cr evi) (mkFoldCall cr)mbios
+    maybe (naiveMap cr evi) (mkFoldCall cr) mbios
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 34
-noFoldCall = llogNO (text "UniProp not applicable!") >> return []
+noFoldCall = do llogNO (text "ListCata not applicable!" <+>
+                        text "Universal Propertiy not satisfied!")
+                return []
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 86
-                llogNO (text "UniProp for Cata applicable, 'filter' detected!")
+                llogNO (text "ListCata applicable, 'filter' detected!")
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 121
-        llogNO (text "UniProp for Cata applicable, 'map' detected!")
+        llogNO (text "ListCata applicable, 'map' detected!")
hunk ./src/Igor2/RuleDevelopment/ListCata.hs 187
-    llogNO (text "UniProp for Cata applicable, fallback to 'foldr'!")
+    llogNO (text "ListCata applicable, fallback to 'foldr'!")
hunk ./src/Syntax/Builder.hs 27
+import Generics.Pointless.Functors (Mu)
+
hunk ./src/Syntax/Builder.hs 360
+    | s == "Mu"      = ''Mu
hunk ./src/Syntax/Type.hs 31
-    allPreds,isFunT, isHOT,
+    allPreds,isFunT, isHOT, isListT, dataName, 
hunk ./src/Syntax/Type.hs 37
-    hasFunT,  hasHOT,   
+    hasFunT,  hasHOT, hasListT
hunk ./src/Syntax/Type.hs 85
+isListT :: Type -> Bool
+isListT (AppT ListT _)    = True
+isListT (AppT (ConT n) _) = isNil n
+isListT   _               = False
hunk ./src/Syntax/Type.hs 90
+-- The name of a data type if it is a data type and not a primitive
+dataName :: (Monad m) => Type -> m Name
+dataName (ForallT _ _ t) = dataName t
+dataName (VarT _)        = fail "dataName: Variable!"
+dataName (ConT n)        = return n
+dataName (TupleT n)
+        | n<2            = return ''()
+        | otherwise      = return . mkName . concat $ ["(",replicate (n-1) ',',")"]
+dataName ArrowT          = return ''(->)
+dataName ListT           = return ''[]
+dataName (AppT t _)      = dataName t
hunk ./src/Syntax/Type.hs 114
-
+hasListT :: (Typed t) => t -> Bool
+hasListT = isListT . typeOf