[Bugfix in naive map, naive map is now last fallback if fold fails.
martin.hofmann@uni-bamberg.de**20091012151248] hunk ./src/RuleDevelopment.hs 24
-    (fs,ms,ps,cs) <- compSucs h r
+    (fs,ns,ms,ps,cs) <- compSucs h r
hunk ./src/RuleDevelopment.hs 27
+    let nhs = mapMaybe (developH r h) ns 
hunk ./src/RuleDevelopment.hs 31
-    let all = concat $ [fhs, mhs, phs, chs]
+    let all = concat $ [fhs, nhs, mhs, phs, chs]
hunk ./src/RuleDevelopment.hs 37
-             text "MTCH:" <^> text "Advancements:" <$> pretty ms <^>
-             text "Hypotheses  :" <$> pretty mhs <$>
-             text "FOLD:" <^> text "Advancements:" <$> pretty fs <^>
+             text "OP1a: FOLD" <^> text "Advancements:" <$> pretty fs <^>
hunk ./src/RuleDevelopment.hs 39
-             text "PART:" <^> text "Advancements:" <$> pretty ps <^>
+             text "OP1b: NAIVE_MAP" <^> text "Advancements:" <$> pretty ns <^>
+             text "Hypotheses  :" <$> pretty nhs <$>
+             text "OP2: MTCH" <^> text "Advancements:" <$> pretty ms <^>
+             text "Hypotheses  :" <$> pretty mhs <$>
+             text "OP3: PART" <^> text "Advancements:" <$> pretty ps <^>
hunk ./src/RuleDevelopment.hs 45
-             text "CALL:" <^> text "Advancements:" <$> pretty cs <^>
+             text "OP4: CALL" <^> text "Advancements:" <$> pretty cs <^>
hunk ./src/RuleDevelopment.hs 52
-        if not $ null fs then return (fs,[],[],[])
-          else liftM3 ((,,,)[]) 
+        if not $ null fs then return (fs,[],[],[],[])
+          else liftM4 ((,,,,)[])
+                      (return []) -- (naiveMap r) 
hunk ./src/RuleDevelopment/UniProp.hs 26
-    evi  <- liftM (map crul) $ breakupM cr
-    maybe (tryDirtyMap cr evi) (mkFoldCall cr)(checkUniPropAndMkIOs evi)
+    evi  <-  liftM (map crul) $ breakupM cr
+    maybe (naiveMap cr evi) (mkFoldCall cr)(checkUniPropAndMkIOs $ evi)
hunk ./src/RuleDevelopment/UniProp.hs 30
+noFoldCall :: IM [(CovrRules,[Call])]
hunk ./src/RuleDevelopment/UniProp.hs 33
-tryDirtyMap :: CovrRule -> [Rule] -> IM [(CovrRules,[Call])]
-tryDirtyMap cr evi = noFoldCall
---    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)])]
---    where    
---    mbMapIO r = liftM (map (\(i,o) -> rule ((init . lhs $ r) ++ [i]) o)) $ liftM2 zip (mbListElems . last . lhs $ r)(mbListElems . rhs $ r)
+naiveMap :: CovrRule -> [Rule] -> IM [(CovrRules,[Call])]
+naiveMap cr evi = do
+    let ios = nub . concat . (mapMaybe mbMapIO) $ evi 
+    if (not $ 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)])]
+    where    
+    mbMapIO r = liftM (map (\(i,o) -> rule ((init . lhs $ r) ++ [i]) o)) $ liftM2 zip (mbListElems . last . lhs $ r)(mbListElems . rhs $ r)
hunk ./src/RuleDevelopment/UniProp.hs 67
-mbFilter cr (_,evi) = do 
+mbFilter cr (bc,evi) = do 
hunk ./src/RuleDevelopment/UniProp.hs 78
-            if (not $ all lastArgConsed f) || (null $ on intersect (map lhs) fio tio)
+            if  or [not $ hasMapProperty (bc,evi), null $ on intersect (map lhs) fio tio]
hunk ./src/RuleDevelopment/UniProp.hs 109
-mbMap  cr (_,evi) = 
+mbMap  cr (bc,evi) = 
hunk ./src/RuleDevelopment/UniProp.hs 113
-    if  (not $ all lastArgConsed evi) || (any hasFreeVars ios) || (null ios)
+    if or [not $ hasMapProperty (bc,evi), any hasFreeVars ios,  null ios]
hunk ./src/RuleDevelopment/UniProp.hs 218
-      return . (,) r
+      return . (,) r 
hunk ./src/RuleDevelopment/UniProp.hs 244
-                                    else fail "No List" 
+                                    else fail "No List"
hunk ./src/RuleDevelopment/UniProp.hs 246
-            _owise             -> fail "No List" 
-mbListElems _  = fail "No List" 
+            _owise             -> fail "No List"  
+mbListElems l  = fail "No List" 
hunk ./src/RuleDevelopment/UniProp.hs 251
--- check wether the second argument of a rule occurs unchanged in the output 
--- after a cons
-lastArgConsed r =  
-    case rhs $ r of
-       TListE (x:xs) t -> (last . lhs $ r) == TListE xs t
-       t@(TAppE _ _ _) ->
-         case unfoldTAppE t of
-            [TConE n _, _, xs] -> isCons n  && (last . lhs $ r) == xs
-            _owise -> False
-       _owise -> False
+
+
+hasMapProperty :: (Rule,[Rule]) -> Bool
+hasMapProperty (bc,evi) = 
+    and [ isNilList . last . lhs $ bc
+        , isNilList . rhs $ bc
+        , all lastArgConsed evi]
+    where
+    -- check wether the second argument of a rule occurs unchanged in the output 
+    -- after a cons
+    lastArgConsed r = 
+        case rhs $ r of
+           TListE (x:xs) t -> (last . lhs $ r) == TListE xs t
+           t@(TAppE _ _ _) ->
+             case unfoldTAppE t of
+                [TConE n _, _, xs] -> isCons n  && (last . lhs $ r) == xs
+                _owise -> False
+           _owise -> False
hunk ./src/Syntax/Expressions.hs 3
---(
---
---    TExp(..),
---
---    module Language.Haskell.TH,
---    module Syntax.Types
---    )
+(
+
+    TExp(..),
+    mkTConE, foldTAppE, unfoldTAppE ,
+    isHOApp, isNilList, 
+    unfoldAppE, toPat, fromTExp,
+
+    )
hunk ./src/Syntax/Expressions.hs 674
-isHOApp = hasHOT . head . unfoldTAppE          
+isHOApp = hasHOT . head . unfoldTAppE    
+
+isNilList (TListE [] _) = True
+isNilList (TConE n _)   = isNil n
+isNilList _ = False 
+      