[para intro implemented
martin.hofmann@uni-bamberg.de**20100810121005] hunk ./src/Igor2/RuleDevelopment.hs 55
-        fs <- ifIsSet inEnhanced (cataIntro r) []  
+        fs <- ifIsSet inEnhanced (tyMorphIntro r) []  
hunk ./src/Igor2/RuleDevelopment/Cata.hs 20
-import Generics.Pointless.RecursionPatterns (cata)
+import Generics.Pointless.RecursionPatterns (cata, para)
hunk ./src/Igor2/RuleDevelopment/Cata.hs 22
-cataIntro :: CovrRule -> IM [(CovrRules,[Call])]
-cataIntro cr = do
+tyMorphIntro  :: CovrRule -> IM [(CovrRules,[Call])]
+tyMorphIntro cr = do 
+  p <- usePara 
+  (if p then paraIntro else cataIntro) cr
hunk ./src/Igor2/RuleDevelopment/Cata.hs 27
-    waypointS $ text "Catamorphism Introduction"
-    llogNO $ text "Check if 'cata' applies to: " <^> pretty cr    
+cataIntro :: CovrRule -> IM [(CovrRules,[Call])]
+cataIntro cr = do  
+  waypointS $ text "Catamorphism Introduction"
+  llogNO $ text "Check if 'cata' applies to: " <^> pretty cr    
hunk ./src/Igor2/RuleDevelopment/Cata.hs 32
-    (genCataArgIs cr >>= gmsg >>= oneOrNone (genericCata cr))
-    `catchError` 
-    (\e1 -> llogNO (text e1) >> 
-     (smsg (lstCataArgIs cr) >>= oneOrNone (listCata cr)))
-    `catchError`
-    \e2 -> llogNO (text e2) >> return []
+  tyMorphIdcs cr >>= gmsg >>= oneOrNone (genericCata cr)
+  `catchError` 
+  (\e1 -> llogNO (text e1) >> (smsg (lstCataArgIs cr) >>= oneOrNone (listCata cr)))
+  `catchError`
+  \e2 -> llogNO (text e2) >> return []
hunk ./src/Igor2/RuleDevelopment/Cata.hs 44
+             
+             
hunk ./src/Igor2/RuleDevelopment/Cata.hs 51
--- get the indices of all arguments In reverse order) which are catamorhpism enabled 
-genCataArgIs :: CovrRule -> IM [Int]
-genCataArgIs cr = 
+-- get the indices of all arguments In reverse order which are applicable for
+-- catamorhpism or paramorphisms
+tyMorphIdcs :: CovrRule -> IM [Int]
+tyMorphIdcs cr = 
hunk ./src/Igor2/RuleDevelopment/Cata.hs 121
-checkIOs = mbfail . (all allEqual). (groupBy ((((all $ uncurry equal) . ) . zip) `on` lhs))
+checkIOs = mbfail . (all allEqual). 
+           (groupBy ((((all $ uncurry equal) . ) . zip) `on` lhs))
hunk ./src/Igor2/RuleDevelopment/Cata.hs 124
-    mbfail b = if b then return () else fail "Contradiction in abduced IOs: Not a function!"
+    mbfail b = if b then return () 
+               else fail "Contradiction in abduced IOs: Not a function!"
hunk ./src/Igor2/RuleDevelopment/Cata.hs 141
-               -- so it is not required for the function and replaced by a wildcard
+               -- so it is not required for the function and replaced by a 
+               -- wildcard
hunk ./src/Igor2/RuleDevelopment/Cata.hs 152
-        | (typeOf a)==(typeOf carg) = evalIO (name cr) (insertAt i a args) >>= 
-                                       maybe (fail "Insufficient support in Examples") (return . id)
+        | (typeOf a)==(typeOf carg) = 
+            evalIO (name cr) (insertAt i a args) >>= 
+                   maybe (fail "Insufficient support in Examples") (return . id)
hunk ./src/Igor2/RuleDevelopment/Cata.hs 157
+
+-- This is not DRY!!! copied from Cata, only small changes, 
+    
+
+-- fails if nothing can be found
+genericPara :: CovrRule -> Int -> IM [(CovrRules,[Call])]
+genericPara cr i = do 
+    llogNO msg
+    evi   <- breakupM cr
+    (dataTypeName i (crul cr) >>= ctorsOf >>= partByCtors i evi >>= mkPara i cr) 
+     `catchError` \e -> noPara i e
+    where
+    -- data type Name of the th argument of the covering rule
+    dataTypeName = ((dataName . typeOf) .) . ithArg
+    msg = linebreak <> text "Check argument" <+> 
+          int i <+> text "for general 'para'!"
+    noPara i e = fail $ "Paramorphism not applicable for argument " ++ 
+                        (show i) ++ "! Universal Property not satisfied: " ++
+                        (show e)
+                        
+paraIntro :: CovrRule -> IM [(CovrRules,[Call])]
+paraIntro cr = do
+
+    waypointS $ text "Paramorphism Introduction"
+    llogNO $ text "Check if 'para' applies to: " <^> pretty cr    
+    
+    (tyMorphIdcs cr >>= gmsg >>= oneOrNone (genericPara cr))
+    `catchError` 
+    \e2 -> llogNO (text e2) >> return []
+    
+    where
+    gmsg i = llogNO ( linebreak <> 
+                      text "Try generic paraemorphism for argument indices" <+>
+                      pretty i) >> return i             
+             
+abduceParaIOs :: Int -> [CovrRule] -> IM [Rule]
+abduceParaIOs i crs = mapM (abduceParaIO i) crs 
+
+abduceParaIO :: Int -> CovrRule -> IM Rule 
+abduceParaIO 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
+               as -> do cargs <- mapM mkCArg as
+                        return . iorule . nestedTupE $ (carg:cargs)
+               -- the cata-arg is a constructor with at least one argument
+    where
+    args = butIthArg i $ crul cr
+    carg = ithArg i $ crul cr 
+    wild = tVarE "_x" (typeOf carg)
+    iorule ca = rule (args ++ [ca])(rhs . crul $ cr)
+    mkCArg a 
+        | (typeOf a)==(typeOf carg) = 
+            evalIO (name cr) (insertAt i a args) >>= 
+                   maybe (fail "Insufficient support in Examples") (return . id)
+        | otherwise                 = return a
+                                      
+mkPara :: Int -> CovrRule -> [[CovrRule]] -> IM [(CovrRules,[Call])]
+mkPara i cr parts = do
+--     let crty = arrowTy
+     ios  <- mapM (abduceIOs i) parts
+     mfns <- mapM checkIOs ios >> mapM (addIO . rules) ios
+     mfcr <- mapM coverAll mfns
+     let mfuns = map (mkMediators (butIthArg i $ crul cr)) mfcr     
+     let fExp = foldTAppE  paraEx [botEx, (mkInfxs mfuns), ithArg i $ crul cr]
+     let cr' = modifycrul cr (\r -> rule (lhs r) fExp)
+     let clls = map  (\mfn -> (name cr',mfn, EQ)) mfns 
+     llogNO $ text "Generic 'para' applicable on argument" <+> int i
+     llogDE $ text "With partitions" <+> pretty parts
+     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) $ map (head . unArrowT) [lty,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)$ map (head . unArrowT) [lty,rty]
+        in  tInfixE (tConE '(\/) [lty,rty,ety,last . unArrowT $ rty]) l r 
+-- end not DRY                                      
+                                      
hunk ./src/Igor2/RuleDevelopment/Cata.hs 254
-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"))))
-                                 
-
+               
+cataEx = TConE ('cata) $ 
+         ForallT [ mkName "a", mkName "b"]
+                 [ AppT (conT ''Mu) (varT "a")
+                 , AppT fctr (AppT pctr (varT "a"))] 
+                 (AppT (AppT ArrowT (varT "a")) (AppT (AppT ArrowT (AppT (AppT ArrowT (AppT (AppT fctr (varT "a")) (varT "b"))) (varT "b"))) (AppT (AppT ArrowT (varT "a")) (varT "b"))))
+                
+paraEx =  TConE ('cata) $ 
+         ForallT [ mkName "a", mkName "b"]
+                 [ AppT (conT ''Mu) (varT "a")
+                 , AppT fctr (AppT pctr (varT "a"))] 
+                 (AppT (AppT ArrowT (varT "a")) (AppT (AppT ArrowT (AppT (AppT ArrowT (AppT (AppT fctr (tupT [varT "b",varT "a"])) (varT "b"))) (varT "b"))) (AppT (AppT ArrowT (varT "a")) (varT "b"))))
+                 
+fctr = conT (mkName "Generics.Pointless.Functors.Functor")
+pctr = conT (mkName "Generics.Pointless.Functors.PF")