[t step towards cata application on any argument (faulty)
martin.hofmann@uni-bamberg.de**20091216095214] hunk ./src/Igor2/RuleDevelopment/Cata.hs 14
+import Data.List ((\\))
+import Data.Maybe
hunk ./src/Igor2/RuleDevelopment/Cata.hs 25
-    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"
+    if hasListT . last . lhs . crul $ cr then listCata cr
+      else do i <- (applyC $ detCataArg . lhs .crul $ cr) :: (IM (Either String Int))
+              either (const $ noCata "Wrong Type") (genericCata cr) i
+--     else do b <- (applyC $ matches (lastArg cr)  muVar) :: (IM (Either String Bool))
+--             if either (const False) id b then genericCata cr
+--              else noCata "Wrong Type"
hunk ./src/Igor2/RuleDevelopment/Cata.hs 32
+-- get the index of the last argument whose type is instance of Mu 
+detCataArg :: (MonadError e m) => [TExp] -> C m Int
+detCataArg as = doit $ zip as [0..]
+    where
+    doit []     = fail "No appropriate type!"
+    doit (x:xs) = doit xs `catchError` \_ ->
+                    matches (fst x) muVar >> return (snd x)
hunk ./src/Igor2/RuleDevelopment/Cata.hs 40
-lastArg  = last . lhs . crul
-initArgs = init . lhs . crul
+ithArg i = (!!i) . lhs . crul 
+butIthArg i = (\l -> l \\ [l!!i]) . lhs . crul
hunk ./src/Igor2/RuleDevelopment/Cata.hs 43
-genericCata :: CovrRule -> IM [(CovrRules,[Call])]
-genericCata cr = do   
-    llogWA  $ text "Check if 'cata' applies to: " <^> pretty cr
+genericCata :: CovrRule -> Int -> IM [(CovrRules,[Call])]
+genericCata cr i = do   
hunk ./src/Igor2/RuleDevelopment/Cata.hs 46
-    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
+    ctors <- maybe (return Nothing) ctorsOf $ dataName . typeOf . (ithArg i) $ cr
+    (maybe (fail $ "No Partition possible for argument " ++ (show i) ++ "! ") return 
+        (ctors >>= partByCtors i evi) >>= mkCata i cr) 
+        `catchError`
+         \e -> noCata $ "Universal Property not satisfied for argument " ++ 
+                        (show i) ++ "! " ++ e
hunk ./src/Igor2/RuleDevelopment/Cata.hs 53
-partByCtors :: [CovrRule] -> [Name] -> Maybe [[CovrRule]]
-partByCtors rs ns = mapM (byCtor rs) ns
+partByCtors :: Int -> [CovrRule] -> [Name] -> Maybe [[CovrRule]]
+partByCtors i rs ns = mapM (byCtor rs) ns
hunk ./src/Igor2/RuleDevelopment/Cata.hs 56
-    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
+    byCtor rs n = let rs' = filter ((hasCtor n) . (ithArg i)) rs in
+                  if null rs' then Nothing else Just rs'
+    --hasCtor n (TVarE _ _)        = True
hunk ./src/Igor2/RuleDevelopment/Cata.hs 64
-mkCata :: CovrRule -> [[CovrRule]] -> IM [(CovrRules,[Call])]
-mkCata cr parts = do
+-- make the catamorphisms with all necessary mediating functions
+mkCata :: Int -> CovrRule -> [[CovrRule]] -> IM [(CovrRules,[Call])]
+mkCata i cr parts = do
hunk ./src/Igor2/RuleDevelopment/Cata.hs 68
-     mfns <- mapM abduceIOs parts
+     mfns <- mapM (abduceIOs i) parts
hunk ./src/Igor2/RuleDevelopment/Cata.hs 70
-     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 mfuns = map (mkMediators (butIthArg i cr)) mfcr     
+     let fExp = foldTAppE  cataEx [botEx, (mkInfxs mfuns), ithArg i cr]
+     let cr' = modifycrul cr (\r -> rule (lhs r) fExp)
hunk ./src/Igor2/RuleDevelopment/Cata.hs 74
+     llogNO $ text "Generic 'cata' applicable on argument" <+> int i
+     llogDE $ text "With partitions" <+> pretty parts
hunk ./src/Igor2/RuleDevelopment/Cata.hs 92
-abduceIOs :: [CovrRule] -> IM Name
-abduceIOs crs = mapM abduceIO crs >>=  addIO . rules
+-- abduce IO examples for one mediating function, add them to the evidence and 
+-- return the name of the mediating function. The first argument 'i' is the 
+-- index of the catamorphism-enabled argument, the second are all examples of 
+-- the initial rule with the same constructor at position 'i'
+abduceIOs :: Int -> [CovrRule] -> IM Name
+abduceIOs i crs = mapM (abduceIO i) crs >>=  addIO . rules
hunk ./src/Igor2/RuleDevelopment/Cata.hs 99
-abduceIO :: CovrRule -> IM Rule 
-abduceIO cr = case subterms carg of
-               [] -> return . iorule $  wild
+-- abduce a single example given the index of the cata-argument and the example
+-- of the initial rule
+abduceIO :: Int -> CovrRule -> IM Rule 
+abduceIO i cr = case subterms carg of
+               [] -> return . iorule $ wild
+               -- the cata-arg is a constant constructor with no arguments
+               -- so it is not required for the function and replaced by a wildcard
hunk ./src/Igor2/RuleDevelopment/Cata.hs 108
+               -- the cata-arg is a constructor with at least one argument
hunk ./src/Igor2/RuleDevelopment/Cata.hs 110
-    args = initArgs cr
-    carg = lastArg cr 
-    wild = tWildE "a" (typeOf carg)
+    args = butIthArg i cr
+    carg = ithArg i cr 
+    wild = tVarE "_x" (typeOf carg)
hunk ./src/Igor2/RuleDevelopment/Cata.hs 119
-nestedTupE [a]    = a
+nestedTupE [a]    = a -- tTupE [a]
hunk ./src/Igor2/SynthesisEngine.hs 58
-           
+            
hunk ./src/Igor2/SynthesisEngine.hs 103
+    
+    getEvidence >>= \io -> llogDE ( linebreak <> text "IGOR initialised to:" <$> indent 2 (pretty io))
hunk ./src/Syntax/Ppr.hs 138
+toExp (TTupE [e] _)       = toExp e -- not really necessary, but removes parenthesis from 1-ary tuples introduced during cata
hunk ./src/Syntax/Ppr.hs 151
-toPat (TWildE n _)        = TH.WildP
+toPat (TWildE n _)        = TH.WildP            -- now the existentials are really wildcards
hunk ./src/Syntax/Ppr.hs 154
+toPat (TTupE [e] _)       = toPat e