[BUGFIX: sometimes, modified arg fun of map, filter was not a function anymore
martin.hofmann@uni-bamberg.de**20091007155701] hunk ./src/RuleDevelopment/UniProp.hs 5
-import Data.List (partition, nub, findIndices, (\\))
+import Data.List (partition, nub, findIndices, (\\), intersect)
hunk ./src/RuleDevelopment/UniProp.hs 32
-tryDirtyMap cr evi 
-    | all listAndSameLength evi = mkDirtyMap cr evi
-    | otherwise                 = noFoldCall   
-
-mkDirtyMap :: CovrRule -> [Rule] -> IM [(CovrRules,[Call])]
-mkDirtyMap cr evi = do
-        llogNO (text "Dirty map detected!")
-        afnm  <- addIO . rules . nub . concat . (mapMaybe mbMapIO) $ evi
-        afcr  <- coverAll afnm
---      the argument function
-  
-        -- map :: (a -> b) -> [a] -> [b]
-        -- map :: ^   afty   ^ -> ^  atys  ^
-        let afty = [typeOf . crul $ afcr]                
-        let atys = unArrowT . typeOf . crul $ cr        
-        
-        -- f x0 = map fun1   x0
-        --            ^afExp^
-        --        ^ mExp      ^  
-        let afExp = foldTAppE ((mkTConE afnm) afty)(init . lhs . crul $ cr)
-        let mExp = foldTAppE 
-                    (mkTConE 'map (afty ++ atys))
-                    [afExp, last.lhs.crul $ cr]
-        let cr' = modifycrul cr (\r -> rule (lhs r) mExp)
-        return [(S.fromList [cr',afcr],[(name cr',afnm, LT)])]
+tryDirtyMap cr evi = 
+    let ios = nub . concat . (mapMaybe mbMapIO) $ evi in 
+    if (all listAndSameLength evi) || (any hasFreeVars ios) || (null ios) then noFoldCall
+    -- check for naive map property, if there are ios, and if ios are a function
+      else do llogNO (text "Naive map detected!")
+              afnm  <- addIO . rules $ ios
+              afcr  <- coverAll afnm
+       --      the argument function
+          
+              -- map :: (a -> b) -> [a] -> [b]
+              -- map :: ^   afty   ^ -> ^  atys  ^
+              let afty = [typeOf . crul $ afcr]                
+              let atys = unArrowT . typeOf . crul $ cr        
+                  
+              -- f x0 = map fun1   x0
+              --            ^afExp^
+              --        ^ mExp      ^  
+              let afExp = foldTAppE ((mkTConE afnm) afty)(init . lhs . crul $ cr)
+              let mExp = foldTAppE 
+                          (mkTConE 'map (afty ++ atys))
+                          [afExp, last.lhs.crul $ cr]
+              let cr' = modifycrul cr (\r -> rule (lhs r) mExp)
+              return [(S.fromList [cr',afcr],[(name cr',afnm, LT)])]
hunk ./src/RuleDevelopment/UniProp.hs 65
-mbFilter cr (_,ios) = do 
+mbFilter cr (_,evi) = do 
hunk ./src/RuleDevelopment/UniProp.hs 72
-    case partition lastArgIsOut ios of
+    case partition lastArgIsOut evi of
hunk ./src/RuleDevelopment/UniProp.hs 74
-            if all lastArgConsed f then Just $ do 
+            let fio = (mkFIO False f) 
+                tio = (mkFIO True t) in
+            if (not $ all lastArgConsed f) || (null $ on intersect (map lhs) fio tio) 
+            -- check filter property, and check if ios are a function
+              then Nothing else Just $ do 
hunk ./src/RuleDevelopment/UniProp.hs 100
-              else Nothing
hunk ./src/RuleDevelopment/UniProp.hs 107
-mbMap  cr (_,ios) = 
+mbMap  cr (_,evi) = 
+    let ios = nub . (map mkMapIO) $ evi in 
hunk ./src/RuleDevelopment/UniProp.hs 111
-    if all lastArgConsed ios 
-      then Just $ do 
+    if  (not $ all lastArgConsed ios) || (any hasFreeVars ios) 
+      then Nothing  
+      else Just $ do 
hunk ./src/RuleDevelopment/UniProp.hs 115
-        afnm  <- addIO . rules . nub . (map mkMapIO) $ ios
+        afnm  <- addIO . rules $ ios
hunk ./src/RuleDevelopment/UniProp.hs 134
-      else Nothing