[implemented 'substitute' in terms of 'root', 'subterms' and 'applyAtPos'
martin.hofmann@uni-bamberg.de**20090428175300] hunk ./src/Syntax/Expressions.hs 158
-    substitute s Root _ = s
-    substitute s pos t =
-        case pos of
---            (P i)     -> maybe t id $  moveToSubtermTE t i (Just.(substitute s Root))
-            (Dot i p) -> maybe t id $  moveToSubtermTE t i (Just.(substitute s p))
+--    substitute s Root _ = s
+--    substitute s pos t =
+--        case pos of
+----            (P i)     -> maybe t id $  moveToSubtermTE t i (Just.(substitute s Root))
+--            (Dot i p) -> maybe t id $  moveToSubtermTE t i (Just.(substitute s p))
hunk ./src/Syntax/Expressions.hs 164
+    root e@(TVarE _ _)                      = const e
+    root e@(TConE _ _)                      = const e
+    root e@(TLitE _ _)                      = const e
+    root (TTupE _ t)                        = flip TTupE t
+    root (TAppE c _ _)                      = foldTAppE c
+    root e@(TListE [] _)                    = const e
+    root (TListE (l:ls) t)                  = \[l, TListE ls _] -> TListE (l:ls) t 
+--    subterms (TCondE e1 e2 e3 _)                = [e1, e2, e3]    
+    root (TInfixE l c r t)                  = \[l, r] -> (TInfixE l c r t) 
+    root    e                               = 
+        error $ "Terms.root: Not implemented for TExp " ++ (show e)  
+              
hunk ./src/Syntax/Expressions.hs 532
-    liftM (foldTAppE op) (applyAtIndex args i f)
+    liftM (foldTAppE op) (applyAtIndexM args i f)
hunk ./src/Syntax/Expressions.hs 535
-   liftM2 TTupE (applyAtIndex es i f) (return ty)
+   liftM2 TTupE (applyAtIndexM es i f) (return ty)
hunk ./src/Syntax/Expressions.hs 539
-    [e', TListE es' ty'] <- (applyAtIndex elist i f)
+    [e', TListE es' ty'] <- (applyAtIndexM elist i f)
hunk ./src/Syntax/Expressions.hs 1107
-    liftM (foldAppE.(op:)) (applyAtIndex args i f)
+    liftM (foldAppE.(op:)) (applyAtIndexM args i f)
hunk ./src/Syntax/Expressions.hs 1110
-   liftM TupE (applyAtIndex es i f)
+   liftM TupE (applyAtIndexM es i f)
hunk ./src/Syntax/Expressions.hs 1114
-    [e', ListE es'] <- (applyAtIndex elist i f)
+    [e', ListE es'] <- (applyAtIndexM elist i f)
hunk ./src/Syntax/Patterns.hs 338
-moveToSubtermTP (TConP n ps ty) i f = liftM (\ps ->TConP n ps ty) (applyAtIndex ps i f)
+moveToSubtermTP (TConP n ps ty) i f = liftM (\ps ->TConP n ps ty) (applyAtIndexM ps i f)
hunk ./src/Syntax/Patterns.hs 341
-    liftM (flip TTupP ty) (applyAtIndex ps i f)
+    liftM (flip TTupP ty) (applyAtIndexM ps i f)
hunk ./src/Syntax/Patterns.hs 345
-    [p', TListP ps' ty'] <- (applyAtIndex plist i f)
+    [p', TListP ps' ty'] <- (applyAtIndexM plist i f)
hunk ./src/Syntax/Patterns.hs 349
-    [p1',p2'] <- applyAtIndex [p1,p2] i f
+    [p1',p2'] <- applyAtIndexM [p1,p2] i f
hunk ./src/Syntax/Patterns.hs 432
-    substitute s Root _ = s
-    substitute s pos t =
-        case pos of
-        --    (P i)     -> maybe t id $  moveToSubtermP i t (Just.(substitute s Root))
-            (Dot i p) -> maybe t id $  moveToSubtermP i t (Just.(substitute s p))
+--    substitute s Root _ = s
+--    substitute s pos t =
+--        case pos of
+--        --    (P i)     -> maybe t id $  moveToSubtermP i t (Just.(substitute s Root))
+--            (Dot i p) -> maybe t id $  moveToSubtermP i t (Just.(substitute s p))
hunk ./src/Syntax/Patterns.hs 438
+    root _ = error "Syntax.Term.root for Pat not implemented"
hunk ./src/Syntax/Patterns.hs 661
-moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndex ps i f)
+moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndexM ps i f)
hunk ./src/Syntax/Patterns.hs 664
-    liftM TupP (applyAtIndex ps i f)
+    liftM TupP (applyAtIndexM ps i f)
hunk ./src/Syntax/Patterns.hs 668
-    [p', ListP ps'] <- (applyAtIndex plist i f)
+    [p', ListP ps'] <- (applyAtIndexM plist i f)
hunk ./src/Syntax/Patterns.hs 672
-    [p1',p2'] <- applyAtIndex [p1,p2] i f
+    [p1',p2'] <- applyAtIndexM [p1,p2] i f
hunk ./src/Syntax/Terms.hs 17
-    mapGetPos, applyAtIndex,
+    mapGetPos, applyAtIndex, applyAtIndexM,
hunk ./src/Syntax/Terms.hs 19
-    getVarNames,
+    getVarNames, substitute,
hunk ./src/Syntax/Terms.hs 112
+    
+    -- | Inverse of subterms, @root t $ subterms t = t@ 
+    root :: t -> ([t] -> t)
hunk ./src/Syntax/Terms.hs 119
-                    
-    -- |Subsitute subterm at position @p@ in term @t@ with term @s@
-    --  If there is no such position @p@, @t@ is returned.
-    substitute      :: t                 -- ^ the substitute @s@
-                    -> Position          -- ^ the postion @p@
-                    -> t                 -- ^ the initial term @t@
-                    -> t                 -- ^ the result
-        
-
hunk ./src/Syntax/Terms.hs 141
-subtermAt t (Dot i p) = do
-    r <- (subterms t) !?! i >>=  flip subtermAt p
-    noHole "Terms.subterm: No subterm at position" r
+subtermAt t (Dot i p) =
+    (subterms t) !?! i >>=  flip subtermAt p
+--    noHole "Terms.subterm: No subterm at position" r
+
+applyAtPos :: (Term t) => (t -> t) -> Position -> t -> t
+applyAtPos f Root t = f t
+applyAtPos f (i `Dot` pos) t = (root t)(applyAtIndex (subterms t) i (applyAtPos f pos))
hunk ./src/Syntax/Terms.hs 159
-subtermsNoHole :: (Term t) => t -> [t]
-subtermsNoHole t = filter (== hole) (subterms t)
+--subtermsNoHole :: (Term t) => t -> [t]
+--subtermsNoHole t = filter (== hole) (subterms t)
hunk ./src/Syntax/Terms.hs 194
+                    
+-- |Subsitute subterm at position @p@ in term @t@ with term @s@
+--  If there is no such position @p@, @t@ is returned.
+substitute      :: (Term t) =>
+                   t                 -- ^ the substitute @s@
+                -> Position          -- ^ the postion @p@
+                -> t                 -- ^ the initial term @t@
+                -> t                 -- ^ the result
+substitute s p t = applyAtPos (\_ -> s) p t        
hunk ./src/Syntax/Terms.hs 214
-applyAtIndex  :: (Monad m) => [a] -> Int -> (a -> m a) -> (m [a])
+applyAtIndexM  :: (Monad m) => [a] -> Int -> (a -> m a) -> (m [a])
+applyAtIndexM xs n _ | n < 0 = fail "Terms.applyAtIndex: negative index"
+applyAtIndexM [] _ _        =  fail "Terms.applyAtIndex: index too large"
+applyAtIndexM (x:xs) 0 f    =  do {fx <- (f x); return (fx:xs) }
+applyAtIndexM (x:xs) n f    =  do {fxs <- (applyAtIndexM xs (n-1) f); return (x:fxs)}
+     
+-- | Applys a function @f@ at the nth element i of a list (zero-based)
+applyAtIndex  :: [a] -> Int -> (a -> a) -> [a]
hunk ./src/Syntax/Terms.hs 224
-applyAtIndex (x:xs) 0 f    =  do {fx <- (f x); return (fx:xs) }
-applyAtIndex (x:xs) n f    =  do {fxs <- (applyAtIndex xs (n-1) f); return (x:fxs)}
+applyAtIndex (x:xs) 0 f    =  (f x):xs
+applyAtIndex (x:xs) n f    =  x:(applyAtIndex xs (n-1) f)
hunk ./src/Syntax/Types.hs 167
-    substitute _ _ _ =  error "substitute for Type not imlemented"
+    root (ForallT ns c t) = \[t] -> ForallT ns c t
+    root t@(AppT t_ _)    = foldl AppT t
+    root t                = const t
hunk ./src/Syntax/Unifier.hs 86
+    -- TODO think about
+    -- it should be suffiecient for equality when the resulting substitution is empty    
hunk ./src/Syntax/Unifier.hs 89
-    equal t1 t2 = (matches t1 t2) && (matches t2 t1)
+    equal t1 t2 = unLM $ do{matchesWithSubs t1 t2 >>= return . null} 
+                             `catchError` (const.return $ False)
+    
+--test l r = match l r >> match r l  >> return True
+--    `catchError` \_ -> return False