[removed Syntax/Substitution.hs moved its content to Syntax/Terms.hs
martin.hofmann@uni-bamberg.de**20090409140821] hunk ./src/Syntax/Substitution.hs 1
-
-module Syntax.Substitution where
-
-import Syntax.Terms
-
-infixr 0 <~
-(<~) :: (Term a, Term b ) => a -> b -> (a, b)
-(<~) = (,)  
-
--- | 'a <~ b' denotes the replacement of 'a' by 'b' where usually 'a' is a 
---   variable and 'b' is a term
-type Replacement a = (a,a)
-   
-type Substitution t = [Replacement t]
-
-nullSubst :: Substitution t
-nullSubst = []
- 
-insertApply :: (Eq a, Term a) =>  (Replacement a) -> (Substitution a) -> (Substitution a)
-insertApply s [] = [s]
-insertApply s@(x,v) (u@(y,w):us) 
-    | (w == x) && (y == v) = (insertApply s us)
-    | w == x               = (y <~ v):(insertApply s us)
-    | otherwise            =  u:(insertApply s us)
-
---instance (Show a, Pretty a) => Pretty (Substitution a) where
---    view u =  "[" ++ ((concat.(intersperse ",")) (map view u)) ++ "]"
-    
---infixr 4 @@
---(@@) :: (Substitution a) -> (Substitution a) -> (Substitution a)
---s1 @@ s2 = [(u, apply s1 t) | (u,t) <- s2 ] ++ s1
-
---merge      :: Monad m => (Substitution a) -> (Substitution a) -> m (Substitution a)
---merge s1 s2 = if agree then return (s1++s2) else fail "merge fails"
--- where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v))
---                   (map fst s1 `intersect` map fst s2)
rmfile ./src/Syntax/Substitution.hs
hunk ./src/Syntax/Terms.hs 11
+    Substitution, Replacement, nullSubst, (<~), insertApply,
+    
hunk ./src/Syntax/Terms.hs 220
+--------------------------------------------------------------------------------
+-- Substitution
+--------------------------------------------------------------------------------
+
+infixr 0 <~
+(<~) :: (Term a, Term b ) => a -> b -> (a, b)
+(<~) = (,)  
+
+-- | 'a <~ b' denotes the replacement of 'a' by 'b' where usually 'a' is a 
+--   variable and 'b' is a term
+type Replacement a = (a,a)
+   
+type Substitution t = [Replacement t]
+
+nullSubst :: Substitution t
+nullSubst = []
+
+insertApply :: (Eq a, Term a) =>  (Replacement a) -> (Substitution a) -> (Substitution a)
+insertApply s [] = [s]
+insertApply s@(x,v) (u@(y,w):us) 
+    | (w == x) && (y == v) = (insertApply s us)
+    | w == x               = (y <~ v):(insertApply s us)
+    | otherwise            =  u:(insertApply s us)
+
+
hunk ./src/Syntax/Types.hs 5
-import Syntax.Substitution
hunk ./src/Syntax/Unifier.hs 16
-import Syntax.Terms (subtermOf, Term)
+import Syntax.Terms --(subtermOf, Term, isNil, isCons, isTuple, Substitution(:)
hunk ./src/Syntax/Unifier.hs 24
-import Syntax.Substitution
-