[directly use filter and map when applicable
martin.hofmann@uni-bamberg.de**20090831172258] hunk ./src/Logging/PrettyPrinter.hs 93
-                    ,"GHC.Base.","GHC.Types."]
+                    ,"GHC.Base.","GHC.Types.", "GHC.List."]
hunk ./src/RuleDevelopment/UniProp.hs 4
-import Data.Maybe (catMaybes, listToMaybe)
-import Data.List (partition)
+import Data.Maybe (catMaybes, listToMaybe, fromJust)
+import Data.List (partition, nub)
hunk ./src/RuleDevelopment/UniProp.hs 30
-mkFoldCall cr (v,fios) =  do 
+mkFoldCall cr (v,fios) = (liftM (:[])) . fromJust . msum $ [ mbFilter cr (v,fios)
+                                                   , mbMap cr (v,fios)
+                                                   ,Just $ mkFold cr (v,fios)]
+
+mbFilter :: CovrRule -> (RHS,[Rule]) -> Maybe (IM (CovrRules,[Call]))
+mbFilter cr (v,ios) = do 
+-- all IOs of fold's argument function can be partinioned into those where the 
+-- 2nd input argument is identical to the output, and those where the second 
+-- argument occurs unchanged in the output after a cons 
+--
+--   >fun1 (S x0) x1 = x1
+--   >fun1 (Z) x0 = Z : x0
+
+    case partition sndArgIsOut ios of
+        (t@(_:_),f@(_:_)) -> 
+            if all sndArgConsed f then Just $ do 
+                let pios = (++) (map (makeFilterIO False) f)(map (makeFilterIO True) t)
+                prednm  <- addIO.rules $ pios
+                predcr  <- coverAll prednm
+--                
+--                --filter :: (a -> Bool) -> [a] -> [a]
+                let pExp = (mkTConE prednm) . unArrowT . typeOf . crul $ predcr
+                let fExp = foldTAppE (mkTConE 'filter (concatMap (unArrowT . typeOf . crul) [predcr, cr])) [pExp, head.lhs.crul $ cr]
+                let cr' = modifycrul cr (\r -> rule (lhs r) fExp)
+    
+                return (S.fromList [cr',predcr],[(name cr',prednm, LT)])
+              else Nothing
+        otherwise         -> Nothing
+    where    
+    makeFilterIO b r = let n = if b then 'True else 'False 
+                 in rule (take 1 (lhs r))(mkTConE n [ConT ''Bool])
+
+
+mbMap  cr (v,ios) = 
+-- the second argument of all IOs of fold's argument function 
+-- occurs unchanged in the output after a cons 
+    if all sndArgConsed ios 
+      then Just $ do 
+        afnm  <- addIO . rules . nub . (map makeMapIO) $ ios
+        afcr  <- coverAll afnm
+--      the argument function
+  
+--      map :: (a -> b) -> [a] -> [b]
+        let afExp = (mkTConE afnm) . unArrowT . typeOf . crul $ afcr
+        let mExp = foldTAppE (mkTConE 'map (concatMap (unArrowT . typeOf . crul) [afcr, cr])) [afExp, head.lhs.crul $ cr]
+        let cr' = modifycrul cr (\r -> rule (lhs r) mExp)
+        return (S.fromList [cr',afcr],[(name cr',afnm, LT)])
+      else Nothing
+    where    
+    makeMapIO r = rule (take 1 (lhs r)) (head . subterms . rhs $  r)
+    
+sndArgIsOut r = ((lhs r) !! 1) == (rhs r)
+
+sndArgConsed r =  
+    case rhs r of
+       TListE (x:xs) t -> ((lhs r) !! 1) == TListE xs t
+       t@(TAppE _ _ _) ->
+         case unfoldTAppE t of
+            [TConE n _, _, xs] -> isCons n  && ((lhs r) !! 1) == xs
+            _owise -> False
+       _owise -> False
+
+                                          
+mkFold :: CovrRule -> (RHS,[Rule]) -> IM (CovrRules,[Call])
+mkFold cr (v,fios) =  do 
hunk ./src/RuleDevelopment/UniProp.hs 112
-mkCallsAndDeps :: Name -> [Rule] -> CovrRule ->  IM [(CovrRules,[Call])]
+mkCallsAndDeps :: Name -> [Rule] -> CovrRule ->  IM (CovrRules,[Call])
hunk ./src/RuleDevelopment/UniProp.hs 116
-    return [(S.fromList [foldcr,subcr],calls)]
+    return (S.fromList [foldcr,subcr],calls)
hunk ./src/RuleDevelopment/UniProp.hs 138
+{- | Check if the given IO examples fulfill the universal property of fold:
+      - they are defined on the empty list
+      - all IOs are closed
+
+-}
hunk ./src/RuleDevelopment/UniProp.hs 145
-    noNilIfDefForNil evi >>= \(r,rs) -> 
+    definedOnNil evi >>= \(r,rs) -> 
hunk ./src/RuleDevelopment/UniProp.hs 147
-     return . (,) (rhs r)
-    
-noNilIfDefForNil :: [Rule] -> Maybe (Rule,[Rule])
-noNilIfDefForNil = maybeStripNil . partition (hasNilIn.lhs)
+      return . (,) (rhs r)
+
+{-| If the given IO exmaples are defined on for the empty list, a tuple 
+    containig the base case and the other IOs is returned, Nothing otherwise
+-}    
+definedOnNil :: [Rule] -> Maybe (Rule,[Rule])
+definedOnNil = maybeStripNil . partition (hasNilIn.lhs)
hunk ./src/RuleDevelopment/UniProp.hs 156
-maybeStripNil (l1, l2) = 
-    listToMaybe l1 >>= \l1' -> 
-     return (l1', l2)
+maybeStripNil (l1, l2) =  listToMaybe l1 >>= return . flip (,) l2 
hunk ./src/RuleDevelopment/UniProp.hs 160
-hasNilIn [TConE n _]   = isNil n
+hasNilIn [a@(TAppE _ _ _)] = (\(TConE n _) -> isNil n) $ head . unfoldTAppE $ a
hunk ./src/RuleDevelopment/UniProp.hs 163
+{-|
+
+-}
hunk ./src/RuleDevelopment/UniProp.hs 170
-    return $ rule [x,xs'] (rhs r)         
+    let io = rule [x,xs'] (rhs r)
+    if not . hasFreeVars $ io then Just io else Nothing         