[various bugfixes and 'Subfunction intro' now more simple
martin.hofmann@uni-bamberg.de**20090423130550
 BUGFIX: computing opePosition was erroneous, open Vars  must be set when computing difference btween lhs and rhs
 BUGFIX: antiunifying ragged lists, (:) now as infix, solved problem when 'straight' part of list is empty
 BUGFIX: Introduce Subfunction, wrong type of subterm due to mkArrowT, foldAppT, foldAppE, etc
 CHANGE: insertCall _> mkCallAt
 CHANGE: IOData does not check for subsuming IOs anymore
 NEW:    matching 2 rules and keeping track of subsumption beyond PatT and ExpT
 NEW:    instance Pretty TimeDiff
 
] hunk ./src/Data/IOData.hs 88
-insertRules :: Rules -> IOData -> (Bool,Name,IOData)
-insertRules rs iod@(IOD{ evidence = bk }) = (True,n',iod')
+insertRules :: Rules -> IOData -> (Name,IOData)
+insertRules rs iod@(IOD{ evidence = bk }) = (n',iod')
hunk ./src/Data/IOData.hs 216
-modifyFrag rf@(RF _ f _ o ) g = rf{frag= g f, opos= openPositions (g f)}
+modifyFrag rf@(RF _ f _ o ) g =  rf{frag= g f, opos= openPositions (g f)}
hunk ./src/Data/IgorMonad.hs 80
-addIO :: Rules -> IM (Bool,Name)
+addIO :: Rules -> IM Name
hunk ./src/Data/IgorMonad.hs 83
-    let (b,n,iod') = insertRules rs iod
+    let (n,iod') = insertRules rs iod
hunk ./src/Data/IgorMonad.hs 85
-    return (b,n)
+    return n
hunk ./src/Data/Rules.hs 9
-    Rules, mkRules, rules, subrule, insertCall, subsumesAll,
+    Rules, mkRules, rules, subrule, mkCallAt, subsumesAll,
hunk ./src/Data/Rules.hs 21
-import Data.List (foldl', transpose, (\\))
+import Data.List (foldl', transpose, (\\), nub)
hunk ./src/Data/Rules.hs 85
-    let lhsvars = concatMap getVarNames $ lhs r
-        rhsvars = getVarNames.rhs $ r
-        diff    = (\\) rhsvars lhsvars
+    let lhsvars = nub $ concatMap getVarNames $ lhs r
+        rhsvars = nub.getVarNames.rhs $ r
+        diff    = rhsvars \\ lhsvars
hunk ./src/Data/Rules.hs 126
-insertCall :: RulePos -> Name -> Rule -> Rule
-insertCall (Body pos) n r = 
+mkCallAt :: RulePos -> Name -> Rule -> Rule
+mkCallAt (Body pos) n r = 
hunk ./src/Data/Rules.hs 129
-        subty   = typeOf . fromJust . (flip subtermAt pos) . rhs $ r
-    in replaceInRhs r (Body pos) (tPat2Call n subty callpat) 
+        resty   = typeOf . fromJust . (flip subtermAt pos) . rhs $ r
+    in replaceInRhs r (Body pos) (tPat2Call n resty callpat) 
hunk ./src/Data/Rules.hs 165
+matchRules :: Rule -> Rule -> LM Bool
+matchRules (R l1 r1) (R l2 r2) = matches2 (l1,r1) (l2,r2) tPat2TExp
+     
+   
hunk ./src/Data/Rules.hs 209
-tPat2Call n ty ps = foldTAppE (TConE n ty) (map tPat2TExp ps)    
+tPat2Call n resty ps =
+    let funty = mkArrowT $ (++ [resty]) $ map typeOf ps  
+    in  foldTAppE (TConE n funty) (map tPat2TExp ps)    
hunk ./src/Data/Rules.hs 270
-subsumesAll r1 r2 = 
-       trace ("DEBUG :" ++ (show.pretty $ r1) ++ " subsumes all " ++ (show.pretty $ r2) ++ "?" ++ (show (all (anySubsumes r1) (S.toAscList r2))))$
-       all (anySubsumes r1) (S.toAscList r2) 
+subsumesAll r1 r2 =  all (anySubsumes r1) (S.toAscList r2) 
hunk ./src/Logging/Logger.hs 151
+    where
+    traceIfDebug msg  = if _DEBUG then trace (show msg) else id          
+     
hunk ./src/Logging/Logger.hs 163
-traceIfDebug msg  = if _DEBUG then trace (show msg) else id          
-     
+
hunk ./src/Logging/PrettyPrinter.hs 136
-            text (show $ 24 * tdDay t + tdHour t) <> text "h" <>
-            text (show $ tdMin t) <> text "m" <>
+            text (show $ 24 * tdDay t + tdHour t) <> text "h" <+>
+            text (show $ tdMin t) <> text "m" <+>
hunk ./src/RuleDevelopment/Subfunction.hs 26
-    novarpos <- return $  posOfNoVarSubts rf
-    let ios = map (abduceIOAt covfrags) novarpos
-    (tags,subfnnms) <- liftM unzip $ mapM addIO ios
+    let novarpos = posOfNoVarSubts rf
+    let ios      = map (abduceIOAt covfrags) novarpos
+    subfnnms    <- mapM addIO ios
hunk ./src/RuleDevelopment/Subfunction.hs 32
-    rfsubs <- mapM (coverAll.snd) $ filter fst $ zip tags subfnnms
+    rfsubs <- mapM coverAll subfnnms
hunk ./src/RuleDevelopment/Subfunction.hs 37
-             text "abducdIOs:" <+> pretty (zip3 tags subfnnms ios) <^>
+             text "abdcdIOs:" <+> pretty (zip subfnnms ios) <^>
hunk ./src/RuleDevelopment/Subfunction.hs 42
-    return [(S.fromList (rfnew:rfsubs), calls) ]
+    return $ [(S.fromList (rfnew:rfsubs), calls) ]
hunk ./src/RuleDevelopment/Subfunction.hs 45
-    addCallAt rf (p,n) = modifyFrag rf $(uncurry insertCall) (p,n)
-    -- replace rhs-subterm of 'rf'  at position 'p' with call ti 'n' using th elhs of 'rf' 
-    posOfNoVarSubts = fst . unzip . filterNoVars . label . subtrms 
+    addCallAt rf (p,n) = modifyFrag rf $ mkCallAt p n
+    -- replace rhs-subterm of 'rf'  at position 'p' with call to 'n' using the lhs of 'rf' 
+    posOfNoVarSubts = fst.unzip.filterNoVars.label.subterms.rhs.frag 
hunk ./src/RuleDevelopment/Subfunction.hs 49
-    subtrms        =  subterms.rhs.frag             
-    -- get the immediate subterms on the rhs    
hunk ./src/RuleDevelopment/Subfunction.hs 54
-    
+-- Every RuleFrag in 'rfs' must be defined at position 'pos'    
hunk ./src/RuleDevelopment/Subfunction.hs 56
-abduceIOAt rfs p =  S.fromList $ map (fromJust.(subrule p).frag) rfs
+abduceIOAt rfs p =  S.fromList $ map (fromJust.(subrule p).frag) rfs 
hunk ./src/Syntax/Antiunifier.hs 100
-            return (ait,ait')    
+            return (ait,ait')   
hunk ./src/Syntax/Expressions.hs 172
-    subterms (TInfixE (Just e1) e2 (Just e3) _) = [e1, e2, e3]
-    subterms (TInfixE Nothing e2 (Just e3) _)   = [hole, e2, e3]
-    subterms (TInfixE (Just e1) e2 Nothing _)   = [e1, e2, hole]
-    subterms (TInfixE Nothing e2 Nothing _)     = [hole, e2, hole]
+    subterms (TInfixE (Just l) _c (Just r) _)   = [l, r]        -- _c is not a subterm, but the root
+    subterms (TInfixE Nothing _c (Just r) _)    = [hole, r]
+    subterms (TInfixE (Just l) _c Nothing _)    = [l, hole]
+    subterms (TInfixE Nothing _c Nothing _)     = [hole, hole]
hunk ./src/Syntax/Expressions.hs 973
-foldTAppE1 (x:xs) = foldTAppE x xs
-
+-- the first argument must have a function type
hunk ./src/Syntax/Patterns.hs 305
-                if null ragged 
-                  then return $ TListP straightai ty 
+                if null ragged then return $ TListP straightai ty 
hunk ./src/Syntax/Patterns.hs 307
-                          let tconp = flip (TConP '(:)) (mkArrowT [ety, ty, ty])
-                          return $ foldr1 (\p1 p2 -> tconp [p1,p2]) (straightai ++ [raggedai])                                     
+                          if (null straight) then return raggedai
+                           else do  
+                                let sections = map (mkTInfixP '(:) ty) straightai
+                                return $ foldTInfixP sections raggedai                                     
hunk ./src/Syntax/Patterns.hs 386
-     
+mkTInfixP c t l r =  TInfixP l c r t
+    
+foldTInfixP [] _ = error "foldTInfixP: empty list of sections!"    
+foldTInfixP sections lastarg = foldr1 (.) sections lastarg     
hunk ./src/Syntax/Terms.hs 171
-varAtPos t p = isJust $ liftM isVar $ subtermAt t p 
+varAtPos t p = fromMaybe False $ liftM isVar $ subtermAt t p
+ 
hunk ./src/Syntax/Types.hs 22
+import Logging
hunk ./src/Syntax/Types.hs 89
-sectionType  = mkArrowT . tail . unArrowT
+sectionType  t =
+    case tail . unArrowT $ t of 
+        [] -> error $ "Types.sectionType: no function type " ++ (show . pretty $ t)
+        tl -> mkArrowT tl
+        
hunk ./src/Syntax/Types.hs 102
+mkArrowT []  = error "Types.mkArrowT: empty list of types"
hunk ./src/Syntax/Unifier.hs 8
-    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, matchVar, flush
+    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, 
+    matchVar, flush,
+    
+    mgu2, matchesWithSubs2, matches2,
hunk ./src/Syntax/Unifier.hs 61
+    
+    unify ::  t -> t -> U t
+    
hunk ./src/Syntax/Unifier.hs 72
-    
-    unify ::  t -> t -> U t
-    
hunk ./src/Syntax/Unifier.hs 88
-    
-    
--- | returns True if both lists are of the same length and each element of
---   the first list pairwise 'matches' its colleague in the second list
-matchesLs :: (Unifieable t) => [t] -> [t] -> Bool
-matchesLs xs ys = 
-    case (zipWithM matches xs ys) of
-        (Just r) -> and r
-        _owise   -> False
-    where    
-    zipWithM _  [] [] = Just  []
-    zipWithM _ _ []  = Nothing
-    zipWithM _ [] _  = Nothing
-    zipWithM f (x:xs) (y:ys) = do 
-        done <- zipWithM f xs ys
-        return $ (f x y):done
-    
-
-            
-
-
hunk ./src/Syntax/Unifier.hs 89
--- | returns True if both lists are of the same length and the elements are 
---   pairwise 'equal'
-equalLs :: (Unifieable t) => [t] -> [t] -> Bool
-equalLs l1 l2 = (matchesLs l1 l2) && (matchesLs l2 l1)
-
- 
--- | Returns True if 'matchesWithSubs' does not 'fail', False if it does.
-matches ::  (Unifieable t) => t -> t -> Bool
-matches t1 t2 = unLM $ do{matchesWithSubs t1 t2 >> return True} 
-                         `catchError` (const.return $ False)
-
-                         
--- | subsumes = flip matches
-subsumes :: (Unifieable t) =>  t -> t -> Bool
-subsumes = flip matches
-
--- | subsumesLs = flip matchesLs
-subsumesLs ::  (Unifieable t) => [t] -> [t] -> Bool
-subsumesLs = flip matchesLs
-    
-    
-    
+   
hunk ./src/Syntax/Unifier.hs 96
-            		 pretty var <+> text " <~ " <+> pretty val <$>
-            		 text "but need to match:" <^>
-            		 pretty var <+> text " <~ " <+> pretty t
-				   )
-			>> flush "No Match!"
-        Nothing  -> put (insert (var <~ t) unifier)    
+                     pretty var <+> text " <~ " <+> pretty val <$>
+                     text "but need to match:" <^>
+                     pretty var <+> text " <~ " <+> pretty t
+                   )
+            >> flush "No Match!"
+        Nothing  -> put (insert (var <~ t) unifier)
+    
hunk ./src/Syntax/Unifier.hs 110
-				text "X is:" <^> (pretty x) <$>
-				text "Current unifier is:" <^> pretty unifier
-			  ) 
+                text "X is:" <^> (pretty x) <$>
+                text "Current unifier is:" <^> pretty unifier
+              ) 
hunk ./src/Syntax/Unifier.hs 116
-            		 indent 2 (pretty var) <+> text " <~ " <+> pretty val <$>
-            		 indent 2 (text "continue unify val x")
-            		) >>
+                     indent 2 (pretty var) <+> text " <~ " <+> pretty val <$>
+                     indent 2 (text "continue unify val x")
+                    ) >>
hunk ./src/Syntax/Unifier.hs 123
-                            		 (pretty x) <+> text "<~" <+> pretty val <^>
-                            		 text "continue unify var val"
+                                     (pretty x) <+> text "<~" <+> pretty val <^>
+                                     text "continue unify var val"
hunk ./src/Syntax/Unifier.hs 130
-                                        				 pretty var <+> text "<~" <+> pretty x
-                                        			   ) 
+                                                         pretty var <+> text "<~" <+> pretty x
+                                                       ) 
hunk ./src/Syntax/Unifier.hs 133
+    
+  
+-- | Returns True if 'matchesWithSubs' does not 'fail', False if it does.
+matches ::  (Unifieable t) => t -> t -> Bool
+matches t1 t2 = unLM $ do{matchesWithSubs t1 t2 >> return True} 
+                         `catchError` (const.return $ False)
+                         
+-- | subsumes = flip matches
+subsumes :: (Unifieable t) =>  t -> t -> Bool
+subsumes = flip matches  
hunk ./src/Syntax/Unifier.hs 145
+-- | returns True if both lists are of the same length and the elements are 
+--   pairwise 'equal'
+equalLs :: (Unifieable t) => [t] -> [t] -> Bool
+equalLs l1 l2 = (matchesLs l1 l2) && (matchesLs l2 l1)
+
+    
+-- | returns True if both lists are of the same length and each element of
+--   the first list pairwise 'matches' its colleague in the second list
+matchesLs :: (Unifieable t) => [t] -> [t] -> Bool
+matchesLs xs ys = 
+    case (zipPairsWithM matches xs ys) of
+        Just r    -> and r
+        Nothing   -> False
+ 
+-- | subsumesLs = flip matchesLs
+subsumesLs ::  (Unifieable t) => [t] -> [t] -> Bool
+subsumesLs = flip matchesLs
+    
+matchLs :: (Unifieable t) => [t] -> [t] -> U t
+matchLs l1 l2 = 
+    case zipPairsWithM (,) l1 l2 of
+        Just ps   -> mapM_ (uncurry match) ps
+        Nothing   -> flush "No Match!"
+             
+unifyLs :: (Unifieable t) => [t] -> [t] -> U t
+unifyLs l1 l2 = 
+    case zipPairsWithM (,) l1 l2 of
+        Just ps -> mapM_ (uncurry unify) ps
+        Nothing -> flush "Not unifieable" 
+ 
+
+
+    
+{- | Convenience function to unify different kind of terms, but keeping 
+     track of the Substitution. @unify2 t1 t2@ corresponds approximately to 
+     @liftM2 (,) (mapM unify t1) (unify t2)@, where the latter 
+     unify uses the Substitution of the further. 
+     This is needed to unify all patterns on the lhs and the rhs of 
+     multiple rules.
+-}
+mgu2        :: (Ord t', Unifieable t', Unifieable t) => ([t],t') -> ([t],t') -> (t -> t') -> LM (Substitution t')
+mgu2 (t1,t1') (t2,t2') trans = do
+        subs  <- execStateT (unifyLs t1 t2) []
+        subs' <- execStateT (unify t1' t2') (transSubs trans subs)
+        return subs' 
+        where
+        transSubs f =  map (\(a,b) -> on (,) f a b)  
hunk ./src/Syntax/Unifier.hs 193
+matchesWithSubs2 :: (Ord t', Unifieable t', Unifieable t) => ([t],t') -> ([t],t') -> (t -> t') -> LM (Substitution t')
+matchesWithSubs2 (t1,t1') (t2,t2') trans = do
+        subs  <- execStateT (matchLs t1 t2) []
+        subs' <- execStateT (match t1' t2') (transSubs trans subs)
+        return subs' 
+        where
+        transSubs f =  map (\(a,b) -> on (,) f a b)
+          
+matches2 t1 t2 f = do{matchesWithSubs2 t1 t2 f >> return True} 
+                         `catchError` (const.return $ False)
+                         
+zipPairsWithM :: (Monad m) => (a -> b -> c) -> [a] -> [b] -> m [c]       
+zipPairsWithM _  [] [] = return  []
+zipPairsWithM _ _ []   = fail "zipPairWithM: Lists have different lengths"
+zipPairsWithM _ [] _   = fail "zipPairWithM: Lists have different lengths"
+zipPairsWithM f (x:xs) (y:ys) = do 
+    done <- zipPairsWithM f xs ys
+    return $ (f x y):done
+            
hunk ./src/UI/UIStarter.hs 223
-             return $ (shows y) . (shows m). (shows d) $ show s
+             return $ (shows y).(addzero m).(shows m).(addzero d).(shows d) $ show s
+             where
+             addzero m = if m <= 9 then shows 0 else id
hunk ./src/UI/UIStarter.hs 233
-    when (debug s) $ hPutDoc stdout doc
-    hPutDoc stdout $ linebreak <> res <$> elt
+    hPutDoc stdout $ linebreak <> res <$$> elt