[sections as argument functions for folds, dirty map detection
martin.hofmann@uni-bamberg.de**20091007092320] hunk ./src/RuleDevelopment/UniProp.hs 4
-import Data.Maybe (catMaybes, listToMaybe, fromJust)
-import Data.List (partition, nub)
+import Data.Maybe (catMaybes, listToMaybe, fromJust, mapMaybe)
+import Data.List (partition, nub, findIndices, (\\))
hunk ./src/RuleDevelopment/UniProp.hs 8
+import Control.Arrow
hunk ./src/RuleDevelopment/UniProp.hs 26
-    maybe noFoldCall (mkFoldCall cr)(checkUniPropAndMkIOs evi)
+    maybe (tryDirtyMap cr evi) (mkFoldCall cr)(checkUniPropAndMkIOs evi)
+     
hunk ./src/RuleDevelopment/UniProp.hs 31
-mkFoldCall :: CovrRule -> (RHS,[Rule]) -> IM [(CovrRules,[Call])]
-mkFoldCall cr (v,fios) = (liftM (:[])) . fromJust . msum $ 
-                        [ mbFilter cr (v,fios)
-                        , mbMap cr (v,fios)
-                        ,Just $ mkFold cr (v,fios)]
+tryDirtyMap :: CovrRule -> [Rule] -> IM [(CovrRules,[Call])]
+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)])]
+    where    
+    mbMapIO r = liftM (map (\(i,o) -> rule ((init . lhs $ r) ++ [i]) o)) $ liftM2 zip (mbListElems . last . lhs $ r)(mbListElems . rhs $ r)
+
+mkFoldCall :: CovrRule -> (Rule,[Rule]) -> IM [(CovrRules,[Call])]
+mkFoldCall cr (vr,fios) = (liftM (:[])) . fromJust . msum $ 
+                        [ mbFilter cr (vr,fios)
+                        , mbMap cr (vr,fios)
+                        ,Just $ mkFold cr (vr,fios)]
hunk ./src/RuleDevelopment/UniProp.hs 66
-mbFilter :: CovrRule -> (RHS,[Rule]) -> Maybe (IM (CovrRules,[Call]))
-mbFilter cr (v,ios) = do 
+mbFilter :: CovrRule -> (Rule,[Rule]) -> Maybe (IM (CovrRules,[Call]))
+mbFilter cr (_,ios) = do 
hunk ./src/RuleDevelopment/UniProp.hs 74
-    case partition sndArgIsOut ios of
+    case partition lastArgIsOut ios of
hunk ./src/RuleDevelopment/UniProp.hs 76
-            if all sndArgConsed f then Just $ do 
+            if all lastArgConsed f then Just $ do 
hunk ./src/RuleDevelopment/UniProp.hs 90
-                let pExp = (mkTConE afnm) afty
+                let pExp = foldTAppE ((mkTConE afnm) afty) (init . lhs . crul $ cr)
hunk ./src/RuleDevelopment/UniProp.hs 93
-                            [pExp, head.lhs.crul $ cr]
+                            [pExp, last.lhs.crul $ cr]
hunk ./src/RuleDevelopment/UniProp.hs 102
-                           in rule (take 1 (lhs r))(mkTConE n [ConT ''Bool]))
+                           in rule (init . lhs $ r)(mkTConE n [ConT ''Bool]))
hunk ./src/RuleDevelopment/UniProp.hs 105
-mbMap  cr (v,ios) = 
+mbMap :: CovrRule -> (Rule,[Rule]) -> Maybe (IM (CovrRules,[Call]))
+mbMap  cr (_,ios) = 
hunk ./src/RuleDevelopment/UniProp.hs 109
-    if all sndArgConsed ios 
+    if all lastArgConsed ios 
hunk ./src/RuleDevelopment/UniProp.hs 125
-        let afExp = (mkTConE afnm) afty
+        let afExp = foldTAppE ((mkTConE afnm) afty)(init . lhs . crul $ cr)
hunk ./src/RuleDevelopment/UniProp.hs 128
-                    [afExp, head.lhs.crul $ cr]
+                    [afExp, last.lhs.crul $ cr]
hunk ./src/RuleDevelopment/UniProp.hs 133
-    mkMapIO r = rule (take 1 (lhs r)) (head . subterms . rhs $  r)
+    mkMapIO r = rule (init . lhs $ r) (head . subterms . rhs $  r)
hunk ./src/RuleDevelopment/UniProp.hs 136
-mkFold :: CovrRule -> (RHS,[Rule]) -> IM (CovrRules,[Call])
-mkFold cr (v,ios) =  do 
+mkFold :: CovrRule -> (Rule,[Rule]) -> IM (CovrRules,[Call])
+mkFold cr (vr,ios) =  do 
+
+    {- When allowing sections as argument functions, it is possible that the 
+       default value contains a variable.king simply the rhs of the base case 
+       would lead to an unbound variable:
+       
+        fun1 x0 x1 = foldr (fun2 x0) [a] x1 
+        
+       with I/O for the base case:
+        
+        fun1 a [] = [a]
+       
+       We could try to fund a substitution to replace the variable 'a':
+       
+       1) Bind the lhs of the example to the lhs of the generalised rule:
+          fun1 x0 x1
+          fun1  a []
+          ~~> [x0/a, x1/[]] 
+       2) Now take only those substitutions, which substitutes contain variables
+          ( [x0/a] ) and replace them by the variable in the lhs of the example:
+          fun1 a [] = [a] ~~>  fun1 x0 [] = [x0]
+       
+       This leads to the following rule:
+       
+        fun1 x0 x1 = foldr (fun2 x0) [x0] x1
+       
+       However, the base case for 'fun2' would  be like like this:
+       
+        fun2 x0 x1 [x0] = <some rhs>
+        
+       Note the x0 occurs more than once, because this is exactly how we built
+       'fun2' before, namely that the base case of 'fun2' uses 'x0'. In fact, we
+       use 'x0' for the base case _and_ additionally pass it as argument. 
+       Therefore, we remove those variables from the argumetn list of the
+       argument function.       
+    -}
+    
+    subs <- lift $ matchesLhs vr (crul cr)
+    let v = foldl replaceInverseIn (rhs vr) (filter (hasVars . snd) subs)  
+    let usedVarInd = findIndices (flip elem (getVars v)) (lhs . crul $ cr)
+        
hunk ./src/RuleDevelopment/UniProp.hs 179
-    afnm  <- addIO . rules $ ios
+    afnm  <- addIO . rules . (map (rmArgsAt usedVarInd))$ ios
hunk ./src/RuleDevelopment/UniProp.hs 185
-    let atys = typeOf v : (unArrowT . typeOf . crul $ cr)
+    let atys = (typeOf . rhs $ vr) : (unArrowT . typeOf . crul $ cr)
hunk ./src/RuleDevelopment/UniProp.hs 188
---        -- f x0 = foldr fun1    v x0
---        --              ^afExp^
---        --        ^ fExp         ^  
-    let afExp = (mkTConE afnm) afty
+--        -- f x0 = foldr (fun1 ..)    v x0
+--        --              ^afExp  ^
+--        --        ^ fExp          ^  
+    let afExp = foldTAppE ((mkTConE afnm) afty) ((rmAll usedVarInd) . init . lhs . crul $ cr)
hunk ./src/RuleDevelopment/UniProp.hs 194
-                    [afExp, v, head.lhs.crul $ cr]
+                    [afExp, v, last.lhs.crul $ cr]
hunk ./src/RuleDevelopment/UniProp.hs 197
+    
hunk ./src/RuleDevelopment/UniProp.hs 199
+    where
+    replaceInverseIn = (flip (uncurry . flip $ replaceTerm))
+    rmArgsAt is r = rule (rmAll is (lhs r)) (rhs r)
+    rmAll is l =  l \\ (map (l!!) is)
hunk ./src/RuleDevelopment/UniProp.hs 210
-checkUniPropAndMkIOs :: [Rule] -> Maybe (RHS,[Rule])
+checkUniPropAndMkIOs :: [Rule] -> Maybe (Rule,[Rule])
hunk ./src/RuleDevelopment/UniProp.hs 213
-    mapM (abduceIO evi) rs >>= 
-      return . (,) (rhs r)
+     mapM (abduceIO evi) rs >>= 
+      return . (,) r
hunk ./src/RuleDevelopment/UniProp.hs 220
-definedOnNil = maybeStripNil . partition (hasNilIn.lhs)
+definedOnNil = maybeStripNil . partition (hasNilIn.(:[]).last.lhs)
hunk ./src/RuleDevelopment/UniProp.hs 230
+-- check wether last in-type and out type is a list and both have same length
+listAndSameLength :: Rule -> Bool
+listAndSameLength r =  maybe False id $ liftM2 ((==) `on` length)  (mbListElems . last . lhs $ r)(mbListElems . rhs $ r)
+
+mbListElems :: (Monad m) =>  TExp -> m [TExp]
+mbListElems (TListE l t) = return l
+mbListElems t@(TAppE _ _ _) =
+         case unfoldTAppE t of 
+            [TConE n _, x, xs] -> if isCons n 
+                                    then mbListElems xs >>= return . (x:)
+                                    else fail "No List" 
+            [TConE n _]        -> if isNil n then return [] else fail "No List" 
+            _owise             -> fail "No List" 
+mbListElems _  = fail "No List" 
hunk ./src/RuleDevelopment/UniProp.hs 245
-sndArgIsOut r = ((lhs r) !! 1) == (rhs r)
+lastArgIsOut r = (last . lhs $ r) == (rhs r)
hunk ./src/RuleDevelopment/UniProp.hs 249
-sndArgConsed r =  
-    case rhs r of
-       TListE (x:xs) t -> ((lhs r) !! 1) == TListE xs t
+lastArgConsed r =  
+    case rhs $ r of
+       TListE (x:xs) t -> (last . lhs $ r) == TListE xs t
hunk ./src/RuleDevelopment/UniProp.hs 254
-            [TConE n _, _, xs] -> isCons n  && ((lhs r) !! 1) == xs
+            [TConE n _, _, xs] -> isCons n  && (last . lhs $ r) == xs
hunk ./src/RuleDevelopment/UniProp.hs 263
-    (x,xs) <- headTail.lhs $ r
-    xs'    <- matchEvals [xs] evi
-    let io = rule [x,xs'] (rhs r)
+    (as,(x,xs)) <- liftM ((,) (init . lhs $ r)) $ headTail . (:[]) . last. lhs $ r
+    xs'    <- matchEvals (as ++ [xs]) evi
+    let io = rule (as ++ [x,xs']) (rhs r)
hunk ./src/RuleDevelopment/UniProp.hs 269
+-- headTail [TVarE x t@(AppT ListT et)]  = Just (TVarE (mkName "x") et, TVarE (mkName "xs") t)