[TPat, Type, TExp are now Terms, Unifieable, Antiunifieable, Substitutable
martin.hofmann@uni-bamberg.de**20090416125906] hunk ./src/Syntax/Expressions.hs 42
-    deriving(Eq, Ord, Show) -- TODO Eq should consider type equivalences
+    deriving(Ord, Show) -- TODO Eq should consider type equivalences
hunk ./src/Syntax/Expressions.hs 48
+instance Eq TExp where 
+    (==) s@(TVarE sn _ ) t@(TVarE tn _) = (sameTy s t) && (sn == tn)
+    (==) s@(TConE sn _) t@(TConE tn _)  = (sameTy s t) && (sn == tn)
+    (==) s@(TLitE sl _) t@(TLitE tl _)  = (sameTy s t) && (sl == tl)
+--    sameSymAtRoot (TCondE c1 t1 e1) (TCondE c2 t2 e2)        = True     
+    (==) s@(TInfixE sl so sr _) t@(TInfixE tl to tr _) =
+        (sameTy s t) && (sl == tl) && (so == to) && (sr == tr)
+    -- tuples
+    (==) s@(TTupE sv _) t@(TTupE tv _)   = 
+        (sameTy s t) && (tv == sv)
+    (==) t@(TAppE _ _ _ ) s@(TTupE sv _) = 
+        case unfoldTAppE $ t of
+            ((TConE n _):tv) -> (isTuple n (length sv)) && 
+                                (sameTy s t) && (tv == sv) 
+            _owise           -> False
+    (==) s@(TTupE sv _) t@(TAppE _ _ _) = 
+        case unfoldTAppE $ t of
+            ((TConE n _):tv) -> (isTuple n (length sv)) && 
+                                (sameTy s t) && (tv == sv) 
+            _owise           -> False
+    (==) s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)            =
+         (sameTy s t) && (s1 == t2) && (s2 == t2)
+    -- empty Lists
+    (==) s@(TListE [] _) t@(TListE [] _)      = (sameTy s t)
+    (==) s@(TConE n _) t@(TListE [] _)        = (sameTy s t) && isNil n
+    (==) s@(TListE [] _) t@(TConE n _)        = (sameTy s t) && isNil n
+    -- empty list and other (if other is a (:) list it matches default clause)
+    (==) s@(TListE _ _) t@(TListE [] _)       = False
+    (==) s@(TListE [] _) t@(TListE _ _)       = False
+    -- non-empty lists
+    (==) s@(TListE sl _) t@(TListE tl _)      = (sameTy s t) && (sl == tl)
+    (==) s@(TListE sl _) t@(TAppE _ _ _)      = 
+        case unfoldTAppE $ t of
+            ((TConE n _):tl) -> (isCons n) && (sameTy s t) && (tl == sl) 
+            _owise           -> False
+    (==) t@(TAppE _ _ _)s@(TListE sl _)       = 
+        case unfoldTAppE $ t of
+            ((TConE n _):tl) -> (isCons n) && (sameTy s t) && (tl == sl) 
+            _owise           -> False
+    (==)  _ _                                 = False
+    
hunk ./src/Syntax/Expressions.hs 90
-    pretty (TVarE n t) = braces $ pretty (VarE n) <+> colon <> colon <+> pretty t
-    pretty (TConE n t) = braces $ pretty (ConE n) <+> colon <> colon <+> pretty t
-    pretty (TLitE l t) = braces $ pretty (LitE l) <+> colon <> colon <+> pretty t
-    pretty (TAppE e1 e2 t) =  braces $ pretty e1 <+> pretty e2  <+> colon <> colon <+> pretty t
-    pretty (TInfixE p1 n p2 t) = braces $ hsep (catMaybes [liftM pretty p1, Just (pretty n), liftM pretty p2]) <+> colon <> colon <+> pretty t
-    pretty (TTupE es t) = braces $ (tupled (map pretty es)) <+> colon <> colon <+> pretty t
-    pretty (TListE l t) = braces $ (list (map pretty l)) <+> colon <> colon <+> pretty t
+    pretty (TVarE n t)         = 
+        braces $ pretty (VarE n) <+> colon <> colon <+> pretty t
+    pretty (TConE n t)         = 
+        braces $ pretty (ConE n) <+> colon <> colon <+> pretty t
+    pretty (TLitE l t)         = 
+        braces $ pretty (LitE l) <+> colon <> colon <+> pretty t
+    pretty (TAppE e1 e2 t)     =  
+        braces $ pretty e1 <+> pretty e2  <+> colon <> colon <+> pretty t
+    pretty (TInfixE p1 n p2 t) = 
+        braces $ hsep (catMaybes [ liftM pretty p1
+                                 , Just (pretty n)
+                                 , liftM pretty p2]) <+> 
+                 colon <> colon <+> pretty t
+    pretty (TTupE es t)        = 
+        braces $ (tupled (map pretty es)) <+> colon <> colon <+> pretty t
+    pretty (TListE l t)        = 
+        braces $ (list (map pretty l)) <+> colon <> colon <+> pretty t
hunk ./src/Syntax/Expressions.hs 121
-
-
-    
---------------------------------------------------------------------------------
--- Auxiliary functions for 'TExp'
---------------------------------------------------------------------------------
-
-----------------------
--- General
-----------------------
-
--- | Returns only the arguments of an 'AppE'xpression.
-unfoldTAppEargs = tail . unfoldTAppE
-
--- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
---   @ConE@ of the function name or the constructor.
-unfoldTAppE :: TExp -> [TExp]
-unfoldTAppE e = f [] e
-    where 
-    f done e =
-        case e of
-            (TAppE e1@(TVarE _ _) e2 _) -> e1:e2:done
-            (TAppE e1@(TConE _ _) e2 _) -> e1:e2:done
-            (TAppE e1 e2 _)             -> f (e2:done) e1
-            _owise                      -> e:done
-            
-foldTAppE1 (x:xs) = foldTAppE x xs
-
-foldTAppE :: TExp -> [TExp] -> TExp
-foldTAppE e [] = e 
-foldTAppE et (e:es) = foldTAppE (TAppE et e (reduceArrowT . typeOf $ et)) es
-
-
-
hunk ./src/Syntax/Expressions.hs 189
-
-    match s t = walkerTExp wf s t
-        where wf = WF matchVar (checkTys isGenTy)"No Match!" "Unifier.match of TExp" 
-    unify s t = walkerTExp wf s t
-        where wf = WF unifyVar (checkTys sameTy) "Not Unifieable!" "Unifier.unify of TExp" 
hunk ./src/Syntax/Expressions.hs 190
---    match s@(TVarE i1 _) t@(TVarE i2 _)     = do
---        check s t
---        if  i1 == i2 then return () else matchVar s t
---    match s@(TVarE _ _) t                   = check s t >> matchVar s t
---    match s          t@(TVarE _ _)          = flush "No Match!"
---    -- matching constructors    
---    match s@(TConE ns _) t@(TConE nt _)     = do
---        check s t 
---        if (ns == nt) then return () else flush "No Match!"  
---    -- matching literals          
---    match s@(TLitE l1 _) t@(TLitE l2 _)     = do
---        check s t
---        if (l1 == l2) then return () else flush "No Match!" 
---    -- matching tuples
---    match s@(TTupE sl _) t@(TTupE tl _)     = do
---        check s t
---        mapM_ (uncurry unify) (zip sl tl)
---    match s@(TTupE sl _) t@(TAppE _ _ _)    = do
---        check s t 
---        case unfoldTAppE t of
---            ((TConE n _):args) -> mapM_ (uncurry match) (zip sl args)
---            _owise               -> flush "Not unifieable"  
---    match t@(TAppE _ _ _) s@(TTupE sl _)    = do
---        check s t      
---        case unfoldTAppE t of
---            ((TConE _ _):args) -> mapM_ (uncurry match) (zip args sl)
---            _owise             -> flush "Not unifieable"  
---        
---    match s@(TListE [] _) t@(TListE [] _)    = check s t >> return ()
---    match s@(TListE (se:sl) st) t@(TListE (te:tl) tt)  = 
---        check s t >> match se te >> match (TListE sl st) (TListE tl tt)
---    -- as usual, something special for lists, so check whether the AppE is of 
---    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
---    match s@(TListE [] _) t@(TConE n _)        = do
---        check s t >> if isNil n then return () else flush "No Match!"  
---    match s@(TConE n _) t@(TListE [] _)        = do
---        check s t >> if isNil n then return () else flush "No Match!" 
---    match s@(TListE (se:sl) st) t@(TAppE _ _ _) = do
---        check s t
---        case unfoldTAppE t of
---            ((TConE n _):a1:[a2]) ->
---                match se a1 >> match (TListE sl st) a2
---            _owise       -> flush "No Match!"  
---    match t@(TAppE _ _ _) s@(TListE (se:sl) st)       = do
---        check s t
---        case unfoldTAppE t of
---            ((TConE n _):a1:[a2]) ->
---                match se a1 >> match (TListE sl st) a2
---            _owise       -> flush "No Match!"  
---    
---    match s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = 
---        check s t >> match s1 t1 >> match s2 t2
---    
---    match s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
---        check s t
---        if ( equal s2 t2) then liftMatch s1 t1 >> liftMatch s3 t3
---          else flush "No Match!"        
+    match s@(TVarE i1 _) t@(TVarE i2 _)     = do
+        checkMatch s t
+        if  i1 == i2 then return () else matchVar s t
+    match s@(TVarE _ _) t                   = checkMatch s t >> matchVar s t
+    match s          t@(TVarE _ _)          = flush "No Match!"
+    -- matching constructors    
+    match s@(TConE ns _) t@(TConE nt _)     = do
+        checkMatch s t 
+        if (ns == nt) then return () else flush "No Match!"  
+    -- matching literals          
+    match s@(TLitE l1 _) t@(TLitE l2 _)     = do
+        checkMatch s t
+        if (l1 == l2) then return () else flush "No Match!" 
+    -- matching tuples
+    match s@(TTupE sl _)         t@(TTupE tl _)     = do
+        checkMatch s t
+        mapM_ (uncurry unify) (zip sl tl)
+    match s@(TTupE sl _)         t@(TAppE _ _ _)    = do
+        checkMatch s t 
+        case unfoldTAppE t of
+            ((TConE n _):args) -> mapM_ (uncurry match) (zip sl args)
+            _owise               -> flush "No Match!" 
+    match t@(TAppE _ _ _)        s@(TTupE sl _)    = do
+        checkMatch s t      
+        case unfoldTAppE t of
+            ((TConE _ _):args) -> mapM_ (uncurry match) (zip args sl)
+            _owise             -> flush "No Match!" 
+        
+    match s@(TListE [] _)        t@(TListE [] _)    = checkMatch s t >> return ()
+    match s@(TListE (se:sl) st)  t@(TListE (te:tl) tt)  = 
+        checkMatch s t >> match se te >> match (TListE sl st) (TListE tl tt)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    match s@(TListE [] _)        t@(TConE n _)        = do
+        checkMatch s t >> if isNil n then return () else flush "No Match!"  
+    match s@(TConE n _)          t@(TListE [] _)        = do
+        checkMatch s t >> if isNil n then return () else flush "No Match!" 
+    match s@(TListE (se:sl) st)  t@(TAppE _ _ _) = do
+        checkMatch s t
+        case unfoldTAppE t of
+            ((TConE n _):a1:[a2]) ->
+                match se a1 >> match (TListE sl st) a2
+            _owise       -> flush "No Match!"  
+    match t@(TAppE _ _ _)        s@(TListE (se:sl) st)       = do
+        checkMatch s t
+        case unfoldTAppE t of
+            ((TConE n _):a1:[a2]) ->
+                match se a1 >> match (TListE sl st) a2
+            _owise       -> flush "No Match!"  
+    
+    match s@(TAppE s1 s2 _)      t@(TAppE t1 t2 _)     = 
+        checkMatch s t >> match s1 t1 >> match s2 t2
+    
+    match s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
+        checkMatch s t
+        if ( equal s2 t2) then liftMatch s1 t1 >> liftMatch s3 t3
+          else flush "No Match!"        
hunk ./src/Syntax/Expressions.hs 248
---        check s t >> match s1 t1 >> match s2 t2 >> match s3 t3    
---    match s t                               =
---        let msg =  patternNotDef [pretty s, pretty t]
---        in lift (setCurrentLogger "Unifier.match of Expression") >>
---           llogWA msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
---           fail (show msg)
+--        checkMatch s t >> match s1 t1 >> match s2 t2 >> match s3 t3    
+    match s t                               =
+        let msg =  patternNotDef [pretty s, pretty t]
+        in lift (setCurrentLogger "Unifier.match of TExp") >>
+           llogWA msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
+           fail (show msg)
hunk ./src/Syntax/Expressions.hs 255
+        
+    unify s@(TVarE i1 _) t@(TVarE i2 _)     = do
+        checkUnify s t
+        if  i1 == i2 then return () else unifyVar s t
+    unify s@(TVarE _ _) t                   = checkUnify s t >> unifyVar s t
+    unify s          t@(TVarE _ _)          = flush "Not unifieable"  
+    -- unifying constructors    
+    unify s@(TConE ns _) t@(TConE nt _)     = do
+        checkUnify s t 
+        if (ns == nt) then return () else flush "Not unifieable"  
+    -- unifying literals          
+    unify s@(TLitE l1 _) t@(TLitE l2 _)     = do
+        checkUnify s t
+        if (l1 == l2) then return () else flush "Not unifieable"  
+    -- unifying tuples
+    unify s@(TTupE sl _) t@(TTupE tl _)     = do
+        checkUnify s t
+        mapM_ (uncurry unify) (zip sl tl)
+    unify s@(TTupE sl _) t@(TAppE _ _ _)    = do
+        checkUnify s t 
+        case unfoldTAppE t of
+            ((TConE n _):args) -> mapM_ (uncurry unify) (zip sl args)
+            _owise               -> flush "Not unifieable"  
+    unify t@(TAppE _ _ _) s@(TTupE sl _)    = do
+        checkUnify s t      
+        case unfoldTAppE t of
+            ((TConE _ _):args) -> mapM_ (uncurry unify) (zip args sl)
+            _owise             -> flush "Not unifieable"  
+        
+    unify s@(TListE [] _) t@(TListE [] _)    = checkUnify s t >> return ()
+    unify s@(TListE (se:sl) st) t@(TListE (te:tl) tt)  = 
+        checkUnify s t >> unify se te >> unify (TListE sl st) (TListE tl tt)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    unify s@(TListE [] _) t@(TConE n _)        = do
+        checkUnify s t >> if isNil n then return () else flush "Not unifieable"    
+    unify s@(TConE n _) t@(TListE [] _)        = do
+        checkUnify s t >> if isNil n then return () else flush "Not unifieable"   
+    unify s@(TListE (se:sl) st) t@(TAppE _ _ _) = do
+        checkUnify s t
+        case unfoldTAppE t of
+            ((TConE n _):a1:[a2]) ->
+                unify se a1 >> unify (TListE sl st) a2
+            _owise       -> flush "Not unifieable"  
+    unify t@(TAppE _ _ _) s@(TListE (se:sl) st)       = do
+        checkUnify s t
+        case unfoldTAppE t of
+            ((TConE n _):a1:[a2]) ->
+                unify se a1 >> unify (TListE sl st) a2
+            _owise       -> flush "No Match!"  
+    
+    unify s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = 
+        checkUnify s t >> unify s1 t1 >> unify s2 t2
+    
+    unify s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
+        checkUnify s t
+        if ( equal s2 t2) then liftUnify s1 t1 >> liftUnify s3 t3
+          else flush "Not unifieable"         
+    unify s@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) = 
+        checkUnify s t >> unify s1 t1 >> unify s2 t2 >> unify s3 t3    
+    unify s t                               =
+        let msg =  patternNotDef [pretty s, pretty t]
+        in lift (setCurrentLogger "Unifier.unify of TExp") >>
+           llogWA msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
+           fail (show msg)
hunk ./src/Syntax/Expressions.hs 328
-            Just val -> checkTys sameTy fail v val >> return val
+            Just val -> checkSame v val >> return val
hunk ./src/Syntax/Expressions.hs 451
-data WalkerFuns = WF { var :: (Unifieable t) => t -> t -> U t
-                     , check :: (Typed t, Monad m) =>
-                         (String -> m ()) -> t -> t -> m () 
-                     , loc :: String
-                     , msg :: String
-                     }
-                     
--- | Helper for lifting a walker (Unifieable t) => (Maybe t) (Maybe t)
-liftWalker :: (Unifieable t) => (t -> t -> U t) -> Maybe t -> Maybe t -> U t
-liftWalker = (\w u v -> maybe (return ()) (\(s,t) -> w s t) (liftM2 (,) u v))
-                     
-walkerTExp :: WalkerFuns -> TExp -> TExp -> StateT (Substitution TExp) LM ()
-                 
-walkerTExp wf s@(TVarE i1 _) t@(TVarE i2 _)     = do
-    (check wf) flush s t
-    if  i1 == i2 then return () else (var wf) s t
-walkerTExp wf s@(TVarE _ _) t                   = (check wf) flush s t >> (var wf) s t
-walkerTExp wf s          t@(TVarE _ _)          = flush . msg $ wf
--- matching constructors    
-walkerTExp wf s@(TConE ns _) t@(TConE nt _)     = do
-    (check wf) flush s t 
-    if (ns == nt) then return () else flush . msg $ wf
--- matching literals          
-walkerTExp wf s@(TLitE l1 _) t@(TLitE l2 _)     = do
-    (check wf) flush s t
-    if (l1 == l2) then return () else flush . msg $ wf
--- matching tuples
-walkerTExp wf s@(TTupE sl _) t@(TTupE tl _)     = do
-    (check wf) flush s t
-    mapM_ (uncurry (walkerTExp wf)) (zip sl tl)
-walkerTExp wf s@(TTupE sl _) t@(TAppE _ _ _)    = do
-    (check wf) flush s t 
-    case unfoldTAppE t of
-        ((TConE n _):args) -> mapM_ (uncurry (walkerTExp wf)) (zip sl args)
-        _owise               -> flush . msg $ wf
-walkerTExp wf t@(TAppE _ _ _) s@(TTupE sl _)    = do
-    (check wf) flush s t      
-    case unfoldTAppE t of
-        ((TConE _ _):args) -> mapM_ (uncurry (walkerTExp wf)) (zip args sl)
-        _owise             -> flush . msg $ wf  
-    
-walkerTExp wf s@(TListE [] _) t@(TListE [] _)    = (check wf) flush s t >> return ()
-walkerTExp wf s@(TListE (se:sl) st) t@(TListE (te:tl) tt)  = 
-    (check wf) flush s t >> walkerTExp wf se te >> walkerTExp wf (TListE sl st) (TListE tl tt)
--- as usual, something special for lists, so check whether the AppE is of 
--- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
-walkerTExp wf s@(TListE [] _) t@(TConE n _)        = do
-    (check wf) flush s t >> if isNil n then return () else flush . msg $ wf
-walkerTExp wf s@(TConE n _) t@(TListE [] _)        = do
-    (check wf) flush s t >> if isNil n then return () else flush . msg $ wf
-walkerTExp wf s@(TListE (se:sl) st) t@(TAppE _ _ _) = do
-    (check wf) flush s t
-    case unfoldTAppE t of
-        ((TConE n _):a1:[a2]) ->
-            walkerTExp wf se a1 >> walkerTExp wf (TListE sl st) a2
-        _owise       -> flush . msg $ wf 
-walkerTExp wf t@(TAppE _ _ _) s@(TListE (se:sl) st)       = do
-    (check wf) flush s t
-    case unfoldTAppE t of
-        ((TConE n _):a1:[a2]) ->
-            walkerTExp wf se a1 >> walkerTExp wf (TListE sl st) a2
-        _owise       -> flush . msg $ wf 
hunk ./src/Syntax/Expressions.hs 452
-walkerTExp wf s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = 
-    (check wf) flush s t >> walkerTExp wf s1 t1 >> walkerTExp wf s2 t2
hunk ./src/Syntax/Expressions.hs 453
-walkerTExp wf s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
-    (check wf) flush s t
-    if (equal s2 t2) then liftWalker (walkerTExp wf) s1 t1 >> liftWalker (walkerTExp wf) s3 t3
-      else flush . msg $ wf        
-walkerTExp wf s@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) = 
-    (check wf) flush s t >> walkerTExp wf s1 t1 >> walkerTExp wf s2 t2 >> walkerTExp wf s3 t3    
-walkerTExp wf s t                               =
-    let msg =  patternNotDef [pretty s, pretty t]
-    in lift (setCurrentLogger (loc wf)) >>
-       llogWA msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
-       fail (show msg)
-          
-checkTys :: (Typed t, Monad m) =>
-         (t -> t -> Bool) -> (String -> m ()) -> t -> t -> m ()        
-checkTys c f s t
-    | c t s = return ()
-    | otherwise  = f "Type mismatch"
-        
---------------------------------------------------------------------------------
--- general Auxiliary functions for 'Term's (deprecated)
-----------------------------------------------------------------------------------
hunk ./src/Syntax/Expressions.hs 461
-   
--- | Returns only the arguments of an 'AppE'xpression.
-unfoldAppEargs = tail . unfoldAppE
-
--- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
---   @ConE@ of the function name or the constructor.
-unfoldAppE :: Exp -> [Exp]
-unfoldAppE e = f [] e
-    where 
-    f done e =
-        case e of
-            (AppE e1@(VarE _) e2) -> e1:e2:done
-            (AppE e1@(ConE _) e2) -> e1:e2:done
-            (AppE e1 e2)       -> f (e2:done) e1
-            _owise             -> e:done
hunk ./src/Syntax/Expressions.hs 462
-foldAppE :: [Exp] -> Exp
-foldAppE es = foldl1 AppE es
-
-
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It assures, that everything is put back at place when returning the result.
-moveToSubtermE :: (Monad m) => Exp -> Int -> (Exp -> m Exp) -> m Exp
-moveToSubtermE (VarE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"        
-moveToSubtermE (LitE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"    
-moveToSubtermE (ConE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"
-    
-moveToSubtermE t@(AppE _ _ ) i f  = do
-    let (op:args) = (unfoldAppE t)     
-    -- the first element is the operator name
-    liftM (foldAppE.(op:)) (applyAtIndex args i f)
-    
-moveToSubtermE (TupE es) i f      = 
-   liftM TupE (applyAtIndex es i f)
-    
-moveToSubtermE (ListE (e:es)) i f = do
-    let elist = [e, ListE es]
-    [e', ListE es'] <- (applyAtIndex elist i f)
-    return $ ListE (e':es')
-    
-moveToSubtermE (InfixE (Just e1) op e2) 0 f = 
-    do { e <- f e1; return $ (InfixE (Just e) op e2)}
-moveToSubtermE (InfixE e1 op (Just e2)) 1 f = 
-    do { e <- f e2; return $ (InfixE e1 op (Just e))}
-moveToSubtermE (InfixE _ op _ ) i _          = 
-    fail $ "Terms.moveToSubtermE: No subterm at position " ++ (show i) ++ 
-           " of operator " ++ (show op)
-                                    
-
---compareAtRootE :: Exp -> Exp -> Bool
---compareAtRootE (VarE _) (VarE _)                        = True
---compareAtRootE (ConE n1) (ConE n2)                      = n1 == n2
---compareAtRootE (LitE l1) (LitE l2)                      = l1 == l2
---compareAtRootE (TupE v1s)(TupE v2s)                     = (length v1s) == (length v2s)
---compareAtRootE t1@(AppE _ _ ) t2@(AppE _ _ )            = compareAtRootE (head (unfoldAppE t1))(head (unfoldAppE t2))
---compareAtRootE (ListE []) (ListE [])                    = True
---compareAtRootE (ListE []) (ListE _)                     = False
---compareAtRootE (ListE _)  (ListE [])                    = False
---compareAtRootE (ListE _)  (ListE _)                     = True
---compareAtRootE (CondE _ _ _) (CondE _ _ _)              = True    
---compareAtRootE (InfixE _ e1 _) (InfixE _ e2 _)          = compareAtRootE e1 e2
---compareAtRootE  _ _                                     = False
-
hunk ./src/Syntax/Expressions.hs 486
-        checkTys sameTy fail s t >> return vals        
+        checkSame s t >> return vals        
hunk ./src/Syntax/Expressions.hs 488
-        checkTys sameTy fail s t >> return [e1,e2]      
+        checkSame s t >> return [e1,e2]      
hunk ./src/Syntax/Expressions.hs 490
-        checkTys sameTy fail s t >> return l      
+        checkSame s t >> return l      
hunk ./src/Syntax/Expressions.hs 496
-        checkTys sameTy fail s t >> return [e1, e2, e3]
+        checkSame s t >> return [e1, e2, e3]
hunk ./src/Syntax/Expressions.hs 498
-        checkTys sameTy fail s t >> return [dummy, e2, e3]
+        checkSame s t >> return [dummy, e2, e3]
hunk ./src/Syntax/Expressions.hs 500
-        checkTys sameTy fail s t >> return [e1, e2, dummy]
+        checkSame s t >> return [e1, e2, dummy]
hunk ./src/Syntax/Expressions.hs 502
-        checkTys sameTy fail s t >> return [dummy, e2, dummy]
+        checkSame s t >> return [dummy, e2, dummy]
hunk ./src/Syntax/Expressions.hs 679
-
hunk ./src/Syntax/Expressions.hs 936
+
+
+
+    
+--------------------------------------------------------------------------------
+-- Auxiliary functions for 'TExp'
+--------------------------------------------------------------------------------
+
+----------------------
+-- General
+----------------------
+
+-- | Returns only the arguments of an 'AppE'xpression.
+unfoldTAppEargs = tail . unfoldTAppE
+
+-- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
+--   @ConE@ of the function name or the constructor.
+unfoldTAppE :: TExp -> [TExp]
+unfoldTAppE e = f [] e
+    where 
+    f done e =
+        case e of
+            (TAppE e1@(TVarE _ _) e2 _) -> e1:e2:done
+            (TAppE e1@(TConE _ _) e2 _) -> e1:e2:done
+            (TAppE e1 e2 _)             -> f (e2:done) e1
+            _owise                      -> e:done
+            
+foldTAppE1 (x:xs) = foldTAppE x xs
+
+foldTAppE :: TExp -> [TExp] -> TExp
+foldTAppE e [] = e 
+foldTAppE et (e:es) = foldTAppE (TAppE et e (reduceArrowT . typeOf $ et)) es
+
+
+
hunk ./src/Syntax/Expressions.hs 1024
+   
+--------------------------------------------------------------------------------
+-- general Auxiliary functions for 'Term's (deprecated)
+----------------------------------------------------------------------------------
+
+-- | Returns only the arguments of an 'AppE'xpression.
+unfoldAppEargs = tail . unfoldAppE
+
+-- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
+--   @ConE@ of the function name or the constructor.
+unfoldAppE :: Exp -> [Exp]
+unfoldAppE e = f [] e
+    where 
+    f done e =
+        case e of
+            (AppE e1@(VarE _) e2) -> e1:e2:done
+            (AppE e1@(ConE _) e2) -> e1:e2:done
+            (AppE e1 e2)       -> f (e2:done) e1
+            _owise             -> e:done
+ 
+foldAppE :: [Exp] -> Exp
+foldAppE es = foldl1 AppE es
+
+
+-- |Moves to the specified subterm in the term @t@ and applies function @f@.
+--  The result is term @t@ with modified @i@th subterm
+--  It assures, that everything is put back at place when returning the result.
+moveToSubtermE :: (Monad m) => Exp -> Int -> (Exp -> m Exp) -> m Exp
+moveToSubtermE (VarE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"        
+moveToSubtermE (LitE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"    
+moveToSubtermE (ConE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"
+    
+moveToSubtermE t@(AppE _ _ ) i f  = do
+    let (op:args) = (unfoldAppE t)     
+    -- the first element is the operator name
+    liftM (foldAppE.(op:)) (applyAtIndex args i f)
+    
+moveToSubtermE (TupE es) i f      = 
+   liftM TupE (applyAtIndex es i f)
+    
+moveToSubtermE (ListE (e:es)) i f = do
+    let elist = [e, ListE es]
+    [e', ListE es'] <- (applyAtIndex elist i f)
+    return $ ListE (e':es')
+    
+moveToSubtermE (InfixE (Just e1) op e2) 0 f = 
+    do { e <- f e1; return $ (InfixE (Just e) op e2)}
+moveToSubtermE (InfixE e1 op (Just e2)) 1 f = 
+    do { e <- f e2; return $ (InfixE e1 op (Just e))}
+moveToSubtermE (InfixE _ op _ ) i _          = 
+    fail $ "Terms.moveToSubtermE: No subterm at position " ++ (show i) ++ 
+           " of operator " ++ (show op)
+                                    
+
+--compareAtRootE :: Exp -> Exp -> Bool
+--compareAtRootE (VarE _) (VarE _)                        = True
+--compareAtRootE (ConE n1) (ConE n2)                      = n1 == n2
+--compareAtRootE (LitE l1) (LitE l2)                      = l1 == l2
+--compareAtRootE (TupE v1s)(TupE v2s)                     = (length v1s) == (length v2s)
+--compareAtRootE t1@(AppE _ _ ) t2@(AppE _ _ )            = compareAtRootE (head (unfoldAppE t1))(head (unfoldAppE t2))
+--compareAtRootE (ListE []) (ListE [])                    = True
+--compareAtRootE (ListE []) (ListE _)                     = False
+--compareAtRootE (ListE _)  (ListE [])                    = False
+--compareAtRootE (ListE _)  (ListE _)                     = True
+--compareAtRootE (CondE _ _ _) (CondE _ _ _)              = True    
+--compareAtRootE (InfixE _ e1 _) (InfixE _ e2 _)          = compareAtRootE e1 e2
+--compareAtRootE  _ _                                     = False
hunk ./src/Syntax/Patterns.hs 29
-        deriving (Show)
-        
+        deriving (Ord,Show)
+
+
+instance Eq TPat where
+
+    (==) s@(TVarP sn _)         t@(TVarP tn _)         = sameTy s t && sn == tn
+    (==) s@(TConP sn _ _)       t@(TConP tn _ _)       = sameTy s t && sn == tn
+    (==) s@(TLitP sl _)         t@(TLitP tl _)         = sameTy s t && sl == tl
+    (==) s@(TTupP sv _)         t@(TTupP tv _)         = sameTy s t && sv == tv
+    (==) s@(TConP n sl _)       t@(TTupP tl _)         = sameTy s t && sl == tl
+    (==) s@(TTupP sl _)         t@(TConP n tl _)       = sameTy s t && sl == tl
+    -- empty Lists    
+    (==) s@(TListP [] _)        t@(TListP [] _)        = sameTy s t
+    (==) s@(TListP [] _)        t@(TConP n [] _)       = sameTy s t && isNil n
+    (==) s@(TConP n [] _)       t@(TListP [] _)        = sameTy s t && isNil n
+    -- empty and other
+    (==) s@(TListP [] _)        t@(TListP _ _)         = False     
+    (==) s@(TListP _ _)         t@(TListP [] _)        = False   
+    -- cons lists
+    (==) s@(TListP sl _)        t@(TListP tl _)        = sameTy s t && sl == tl   
+    (==) s@(TListP sl _)        t@(TConP n tl _)       = 
+        sameTy s t && isCons n && sl == tl  
+    (==) s@(TConP n sl _)       t@(TListP tl _)        = 
+        sameTy s t && isCons n && sl == tl           
+    (==) s@(TInfixP sl so sr _) t@(TInfixP tl to tr _) = 
+        sameTy s t && so == to && [sl,sr] == [tl,tr]
+    (==)  _ _                                          = False
+            
hunk ./src/Syntax/Patterns.hs 66
-    pretty (TLitP l t) = pretty (LitP l) <+> colon <> colon <+> pretty t
-    pretty (TVarP n t) = pretty (VarP n) <+> colon <> colon <+> pretty t
-    pretty (TTupP ps t) = tupled (map pretty ps) <+> colon <> colon <+> pretty t
-    pretty (TConP n ps t) = pretty (ConP n []) <> hcat (map pretty ps)  <+> colon <> colon <+> pretty t
-    pretty (TInfixP p1 n p2 t) = hcat [pretty p1, pretty n,pretty p2] <> colon <+> pretty t 
-    pretty (TListP ps t) = list (map pretty ps)  <+> colon <> colon <+> pretty t
+    pretty (TLitP l t)         = 
+        braces $ pretty (LitP l) <+> colon <> colon <+> pretty t
+    pretty (TVarP n t)         = 
+        braces $ pretty (VarP n) <+> colon <> colon <+> pretty t
+    pretty (TTupP ps t)        = 
+        braces $ tupled (map pretty ps) <+> colon <> colon <+> pretty t
+    pretty (TConP n ps t)      = 
+        braces $ pretty (ConP n []) <> hcat (map pretty ps)  <+> 
+                 colon <> colon <+> pretty t
+    pretty (TInfixP p1 n p2 t) = 
+        braces $ hcat [pretty p1, pretty n,pretty p2] <> colon <+> pretty t 
+    pretty (TListP ps t)       = 
+        braces $ list (map pretty ps)  <+> colon <> colon <+> pretty t
+
+instance Term TPat where
+
+    sameSymAtRoot (TVarP _ _)       (TVarP _ _)        = True
+    sameSymAtRoot (TConP c1 _ _)    (TConP c2 _ _)     = (c1 == c2)
+    sameSymAtRoot (TLitP l1 _)      (TLitP l2 _)       = l1 == l2
+    sameSymAtRoot (TTupP v1s _)     (TTupP v2s _)      = (length v1s) == (length v2s)
+    sameSymAtRoot (TConP n _ _)     (TTupP l _)        = isTuple n (length l)
+    sameSymAtRoot (TTupP l _)       (TConP n _ _)      = isTuple n (length l)
+    -- empty Lists    
+    sameSymAtRoot (TListP [] _)     (TListP [] _)      = True
+    sameSymAtRoot (TListP [] _)     (TConP n [] _)     = isNil n
+    sameSymAtRoot (TConP n [] _)    (TListP [] _)      = isNil n
+    -- empty and other
+    sameSymAtRoot (TListP [] _)     (TListP _ _)       = False     
+    sameSymAtRoot (TListP _ _)      (TListP [] _)      = False   
+    -- cons lists
+    sameSymAtRoot (TListP _ _)      (TListP _ _)       = True   
+    sameSymAtRoot (TListP _ _)      (TConP n _ _)      = isCons n   
+    sameSymAtRoot (TConP n _ _)     (TListP _ _)       = isCons n
+         
+    sameSymAtRoot (TInfixP _ n1 _ _)(TInfixP _ n2 _ _) = n1 ==  n2
+    sameSymAtRoot  _ _                                 = False
+            
+    substitute s Root _ = s
+    substitute s pos  t =
+        case pos of
+         (P i)     -> maybe t id $  moveToSubtermTP t i (Just.(substitute s Root))
+         (Dot p i) -> maybe t id $  moveToSubtermTP t i (Just.(substitute s p))
+       
+    subterms (TVarP _ _)         = []
+    subterms (TLitP _ _)         = []
+    --subterms (TConP _ pats _)    = pats
+    subterms (TInfixP p1 _ p2 _) = [p1,p2] 
+    subterms (TListP [] _)       = []
+    subterms (TListP (p:ps) ty)  = [p, TListP ps ty]
+    subterms (TTupP pats _)      = pats
+    subterms    p                = 
+        error $ "Terms.subterms at TPat: Not implemented for Pattern " ++ (show p)
+    
+    isVar (TVarP _ _) = True
+    isVar _           = False
+
+    getVarNames t     = map (\(TVarP n _) -> n)  $ getVars t
+        
+    hole              = TConP 'Hole [] (ConT ''Hole) 
+
+
+instance Substitutable TPat where
+    apply u v@(TVarP _ _)         = case lookup v u of 
+                                     Just val -> return val
+                                     Nothing  -> return v
+    --apply u (TConP n ps ty)       = liftM (flip (TConP n) ty) (mapM (apply u) ps)
+    apply u t@(TLitP _ _)         = return t
+    apply u (TListP ts ty)        = liftM (flip TListP ty) (mapM (apply u) ts)
+    apply u (TTupP ts ty)         = liftM (flip TTupP ty) (mapM (apply u) ts)
+    apply u (TInfixP e1 op e2 ty) =
+        liftM4 TInfixP (apply u e1) (return op) (apply u e2) (return ty)
+    apply u t                     =   
+        let msg =  patternNotDef [ pretty u, pretty t]
+        in  setCurrentLogger "Terms.Terms.apply at TPat" >>
+            logWA msg >> fail ( show msg)      
+
+
+instance Unifieable TPat where    
+
+    match s@(TVarP sn _)           t@(TVarP tn _)          = do
+        checkMatch s t 
+        if sn == tn then return () else matchVar s t
+    match s@(TVarP _ _)            t                       = matchVar s t
+    match s                        t@(TVarP _ _)           = flush  "No Match!"             
+    match s@(TLitP sl _)           t@(TLitP tl _)          = do
+        checkMatch s t
+        if sl == tl then return () else flush  "No Match!"         
+    match s@(TListP [] _)          t@(TListP [] _)         = do 
+        checkMatch s t ; return ()
+    match s@(TListP (se:ss) st)    t@(TListP (te:ts) tt)   = 
+        checkMatch s t >> match se te >> match (TListP ss st) (TListP ts tt) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    match s@(TListP [] _)          t@(TConP n [] _)        = do
+        checkMatch s t 
+        if isNil n then return () else flush  "No Match!"  
+    match s@(TConP n [] _) t@(TListP [] _)                 = do
+        checkMatch s t 
+        if isNil n then return () else flush  "No Match!"  
+    match s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = do
+        checkMatch s t
+        if isCons n 
+          then match se te >> match (TListP ss st) ts 
+          else flush "No Match!"  
+    match s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   = do
+        checkMatch s t
+        if isCons n 
+          then match se te >> match ss (TListP ts tt) 
+          else flush "No Match!"
+    match s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       = do
+        checkMatch s t
+        if n1 == n2 
+          then mapM_ (uncurry match) (zip p1 p2) 
+          else flush "No Match!"          
+    match s@(TTupP sl _)           t@(TTupP tl _)          = do
+        checkMatch s t
+        mapM_ (uncurry match) (zip sl tl)       
+    match s@(TConP n sl _)         t@(TTupP tl _)          = do
+        checkMatch s t
+        if isTuple n (length tl) 
+          then mapM_ (uncurry match) (zip sl tl)
+          else flush "No Match!"      
+    match s@(TTupP sl _)           t@(TConP n tl _)        = do
+        checkMatch s t
+        if isTuple n (length sl) 
+          then mapM_ (uncurry match) (zip sl tl)
+          else flush "No Match!"         
+    match s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  = do
+        checkMatch s t
+        if s2 == t2
+          then match s1 t1 >> match s3 t3
+          else flush  "No Match!"          
+    match s t                                              =    
+        flush  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))  
+       
+
+    unify s@(TVarP sn _)           t@(TVarP tn _)          = do
+        checkUnify s t 
+        if sn == tn then return () else unifyVar s t
+    unify s@(TVarP _ _)            t                       = unifyVar s t
+    unify s                        t@(TVarP _ _)           = unifyVar s t             
+    unify s@(TLitP sl _)           t@(TLitP tl _)          = do
+        checkUnify s t
+        if sl == tl then return () else flush  "Not unifieable!"         
+    unify s@(TListP [] _)          t@(TListP [] _)         = do 
+        checkUnify s t ; return ()
+    unify s@(TListP (se:ss) st)    t@(TListP (te:ts) tt)   = 
+        checkUnify s t >> unify se te >> unify (TListP ss st) (TListP ts tt) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    unify s@(TListP [] _)          t@(TConP n [] _)        = do
+        checkUnify s t 
+        if isNil n then return () else flush  "Not unifieable!"  
+    unify s@(TConP n [] _) t@(TListP [] _)                 = do
+        checkUnify s t 
+        if isNil n then return () else flush  "Not unifieable!"  
+    unify s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = do
+        checkUnify s t
+        if isCons n 
+          then unify se te >> unify (TListP ss st) ts 
+          else flush "Not unifieable!"  
+    unify s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   = do
+        checkUnify s t
+        if isCons n 
+          then unify se te >> unify ss (TListP ts tt) 
+          else flush "Not unifieable!"
+    unify s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       = do
+        checkUnify s t
+        if n1 == n2 
+          then mapM_ (uncurry unify) (zip p1 p2) 
+          else flush "Not unifieable!"          
+    unify s@(TTupP sl _)           t@(TTupP tl _)          = do
+        checkUnify s t
+        mapM_ (uncurry unify) (zip sl tl)       
+    unify s@(TConP n sl _)         t@(TTupP tl _)          = do
+        checkUnify s t
+        if isTuple n (length tl) 
+          then mapM_ (uncurry unify) (zip sl tl)
+          else flush "Not unifieable!"      
+    unify s@(TTupP sl _)           t@(TConP n tl _)        = do
+        checkUnify s t
+        if isTuple n (length sl) 
+          then mapM_ (uncurry unify) (zip sl tl)
+          else flush "Not unifieable!"         
+    unify s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  = do
+        checkUnify s t
+        if s2 == t2
+          then unify s1 t1 >> unify s3 t3
+          else flush  "Not unifieable!"          
+    unify s t                                              =    
+        flush  ("Term " ++ (show s) ++ "does not unify with term " ++ (show t))
+        
+  
+instance Antiunifieable TPat where
+
+    mkVar t n = TVarP n (typeOf t)
+
+    -- antiunifying (TupP [Pat])
+    aunify l@((TTupP _ ty):xs) = 
+        case collectSubtermsTP l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TTupP ai_subterms ty
+            Nothing       -> 
+                computeAntiInstance l
hunk ./src/Syntax/Patterns.hs 272
+    -- antiunifying (ConP Name [Pat])
+    aunify l@((TConP nm _ ty):xs) = 
+        case collectSubtermsTP l of
+            Just subterms -> do           
+                ai_subterms <- mapM aunify subterms
+                return $ TConP nm ai_subterms ty
+            Nothing       -> 
+                computeAntiInstance l
+                
+    -- antiunifying (InfixP Pat Name Pat)
+    aunify l@((TInfixP _ nm _ ty):xs) =
+        case collectSubtermsTP l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                return $ TInfixP fstai nm sndai ty
+            Nothing       -> 
+                  computeAntiInstance l 
+    
+    -- antiunifying (ListP [Pat])
+    -- Here some hack is necessary, because of Haskell's inconsistent way of
+    -- representing lists. If the pattern lists have different lengths, we
+    -- antiunify argument-wise starting with the first arguments until some 
+    -- pattern has no nth argument. If so, the whole rest is antiunified
+    -- and the ouput is constructed as a (:)-List with a variable as tail.
+    -- (see also @aunify (ListE _)@ )
+    aunify l@((TListP _ ty@(AppT _ ety)):xs) = 
+        case collectSubtermsTP l of
+            Just subterms  -> do
+                let len = length l
+                    straight = takeWhile (\l -> length l == len) subterms 
+                    ragged   = dropWhile (\l -> length l == len) subterms 
+                straightai <- mapM aunify straight
+                if null ragged 
+                  then return $ TListP straightai ty 
+                  else do raggedai <- computeAntiInstance $ map (flip TListP ty) ragged
+                          let tconp = flip (TConP '(:)) (addArrowT [ety, ty, ty])
+                          return $ foldr1 (\p1 p2 -> tconp [p1,p2]) (straightai ++ [raggedai])                                     
+            Nothing     ->
+                computeAntiInstance l 
+    
+    -- antiunifying (VarP Name)              
+    aunify l@((TVarP _ _):xs) =  
+        checkforAntiInstance l     
+    -- antiunifying (LitP Lit)
+    aunify l@((TLitP _ _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
+
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Pat is not implemented!"            
+--------------------------------------------------------------------------------
+-- Auxiliary functions for 'TPat' as 'Term's
+--------------------------------------------------------------------------------
+
+-- |Moves to the specified subterm in the term @t@ and applies function @f@.
+--  The result is term @t@ with modified @i@th subterm
+--  It is assured, that everything is put back in place when returning the result.
+moveToSubtermTP :: (Monad m) => TPat ->Int ->  (TPat -> m TPat) -> m TPat
+moveToSubtermTP (TVarP _ _) _ _ = fail "Terms.moveToSubtermTP. No subterm at position"        
+moveToSubtermTP (TLitP _ _) _ _ = fail "Terms.moveToSubtermTP. No subterm at position"    
+moveToSubtermTP (TConP n ps ty) i f = liftM (\ps ->TConP n ps ty) (applyAtIndex ps i f)
+   
+moveToSubtermTP (TTupP ps ty) i f      = 
+    liftM (flip TTupP ty) (applyAtIndex ps i f)
+    
+moveToSubtermTP (TListP (p:ps) ty) i f = do
+    let plist = [p,  TListP ps ty]
+    [p', TListP ps' ty'] <- (applyAtIndex plist i f)
+    return $  TListP (p':ps') ty'
+    
+moveToSubtermTP (TInfixP p1 op p2 ty) i f = do
+    [p1',p2'] <- applyAtIndex [p1,p2] i f
+    return $ (TInfixP p1' op p2' ty)
+
+{-|
+   Determine the collector function by means of the first element. The 
+   collector, which is fixed to a certain data constructor and collects the 
+   subterms or returns 'Nothing' if one element does not match with the fixed 
+   data constructor.
+-}
+collectSubtermsTP :: [TPat] -> Maybe [[TPat]]
+collectSubtermsTP l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = collectSubterms (head l)
+        
+    collectSubterms :: (Monad m) => TPat -> TPat -> m [TPat]
+    collectSubterms s@(TConP sn _ _)     t@(TConP tn pats _) 
+        | sn == tn  = checkSame s t >> return pats
+        | otherwise = fail ""
+    collectSubterms s@(TTupP _ _)        t@(TTupP vals _)    = 
+        checkSame s t >> return vals        
+    collectSubterms s@(TListP _ _)       t@(TListP l _)      = 
+        checkSame s t >> return l      
+    collectSubterms s@(TInfixP _ sn _ _) t@(TInfixP l st r _)
+        | sn == st  = checkSame s t >> return [l, r]
+        | otherwise = fail ""
+    collectSubterms _ _                                      = fail ""
+
+     
+--------------------------------------------------------------------------------
+-- TH.Exp
+--------------------------------------------------------------------------------
hunk ./src/Syntax/Patterns.hs 466
-    match s          t@(VarP _)           = matchVar t s          
+    match s          t@(VarP _)           = flush  "No Match!"           
hunk ./src/Syntax/Patterns.hs 485
-        | otherwise                       = flush  "No Match!"  
-    match s@(ListP _) t@(ConP _ _)        = match t s    
+        | otherwise                       = flush  "No Match!" 
hunk ./src/Syntax/Patterns.hs 546
-        
---------------------------------------------------------------------------------
--- Auxiliary functions for 'Pat' as 'Term's
---------------------------------------------------------------------------------
hunk ./src/Syntax/Patterns.hs 547
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It is assured, that everything is put back in place when returning the result.
-moveToSubtermP :: (Monad m) => Int -> Pat -> (Pat -> m Pat) -> m Pat
-moveToSubtermP _ (VarP _) _ = fail "Terms.moveToSubtermE. No subterm at position"        
-moveToSubtermP _ (LitP _) _ = fail "Terms.moveToSubtermE. No subterm at position"    
-moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndex ps i f)
-   
-moveToSubtermP i (TupP ps) f      = 
-    liftM TupP (applyAtIndex ps i f)
-    
-moveToSubtermP i (ListP (p:ps)) f = do
-    let plist = [p,  ListP ps]
-    [p', ListP ps'] <- (applyAtIndex plist i f)
-    return $  ListP (p':ps')
-    
-moveToSubtermP i (InfixP p1 op p2) f = do
-    [p1',p2'] <- applyAtIndex [p1,p2] i f
-    return $ (InfixP p1' op p2')
hunk ./src/Syntax/Patterns.hs 630
-                
+                        
+--------------------------------------------------------------------------------
+-- Auxiliary functions for 'Pat' as 'Term's
+--------------------------------------------------------------------------------
+
+-- |Moves to the specified subterm in the term @t@ and applies function @f@.
+--  The result is term @t@ with modified @i@th subterm
+--  It is assured, that everything is put back in place when returning the result.
+moveToSubtermP :: (Monad m) => Int -> Pat -> (Pat -> m Pat) -> m Pat
+moveToSubtermP _ (VarP _) _ = fail "Terms.moveToSubtermE. No subterm at position"        
+moveToSubtermP _ (LitP _) _ = fail "Terms.moveToSubtermE. No subterm at position"    
+moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndex ps i f)
+   
+moveToSubtermP i (TupP ps) f      = 
+    liftM TupP (applyAtIndex ps i f)
+    
+moveToSubtermP i (ListP (p:ps)) f = do
+    let plist = [p,  ListP ps]
+    [p', ListP ps'] <- (applyAtIndex plist i f)
+    return $  ListP (p':ps')
+    
+moveToSubtermP i (InfixP p1 op p2) f = do
+    [p1',p2'] <- applyAtIndex [p1,p2] i f
+    return $ (InfixP p1' op p2')
+
hunk ./src/Syntax/Types.hs 4
-    sameTy, isGenTy, equalTys,
+    sameTy,
+    -- isGenTy, equalTys,
+    
+    checkMatch, checkUnify, checkSame,
hunk ./src/Syntax/Types.hs 62
+          
+checkTys :: (Typed t, Monad m) =>
+         (t -> t -> Bool) -> (String -> m ()) -> t -> t -> m ()        
+checkTys c f s t
+    | c t s = return ()
+    | otherwise  = f "Type mismatch"
hunk ./src/Syntax/Types.hs 69
-
+-- TODO: These should be more sophisticated, when dealing with type classes,
+-- now only monomorphic t ypes are allowed.
+checkMatch,checkUnify,checkSame :: (Typed t, Monad m) => t -> t -> m ()   
+checkMatch = checkTys sameTy fail
+checkUnify = checkTys sameTy fail       
+checkSame  = checkTys sameTy fail
hunk ./src/Syntax/Types.hs 162
-
+-- Unification ignores ForallT , i.e. type classes. Otherwise I would have to 
+-- make 'unify' and 'match' statefull w.r.t. to type classes, but this causes 
+-- trouble when evaluating Hypotheses
hunk ./src/Syntax/Types.hs 167
-    unify t1@(VarT _) t2@(VarT _)   = unifyVar t1 t2
+    unify s@(VarT _) t@(VarT _)
+        |(s == t)                           = return ()
+        | otherwise                         = unifyVar s t
+    unify s@(VarT _) t                      = unifyVar s t
+    unify s          t@(VarT _)             = unifyVar t s
hunk ./src/Syntax/Types.hs 174
-        | otherwise = fail "Not Unifieable!"
+        | otherwise = flush "Not Unifieable!"
hunk ./src/Syntax/Types.hs 178
-        | otherwise = fail "Not Unifieable!"
+        | otherwise = flush "Not Unifieable!"
hunk ./src/Syntax/Types.hs 181
-        | otherwise = fail "Not Unifieable!"
+        | otherwise = flush "Not Unifieable!"
hunk ./src/Syntax/Types.hs 184
-        | otherwise = fail "Not Unifieable!"
+        | otherwise    = flush "Not Unifieable!"
+    -- lists
+    unify ListT ListT                 = return ()
+    unify ListT (ConT n)              
+        | isNil n      = return ()
+        | otherwise    = flush "Not Unifieable!"
+        
+    unify (ConT n) ListT              
+        | isNil n      = return ()
+        | otherwise    = flush "Not Unifieable!"
+    
+    unify ArrowT ArrowT               = return ()
+    unify (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
+    unify t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
+    unify (AppT a1 b1) (AppT a2 b2)   = 
+        unify a1 a2 >> unify b1 b2
+    unify _ _                         =  flush "Not Unifieable!"
+
+    match s@(VarT _) t@(VarT _)
+        |(s == t)                           = return ()
+        | otherwise                         = matchVar s t
+    match s@(VarT _) t                      = matchVar s t
+    match s          t@(VarT _)             = flush "No Match!"
+    match (ConT n1) (ConT n2)       
+        | n1 == n2  = return ()
+        | otherwise = flush "Not Unifieable!"
+    -- tuples
+    match (TupleT i1) (TupleT i2)     
+        | i1 == i2  = return ()
+        | otherwise = flush "Not Unifieable!"
+    match (TupleT i) (ConT n)
+        | isTuple n i  = return ()
+        | otherwise = flush "Not Unifieable!"
+    match (ConT n)(TupleT i)
+        | isTuple n i  = return ()
+        | otherwise    = flush "Not Unifieable!"
hunk ./src/Syntax/Types.hs 221
---    unify ListT ListT                 = True
---    unify ListT (ConT n)              = isNil n
---    sameSymAtRoot (ConT n) ListT              = isNil n
---    
---    sameSymAtRoot ArrowT ArrowT               = True
---    sameSymAtRoot (ForallT _ _ t1) t2         = sameSymAtRoot t1 t2
---    sameSymAtRoot t1 (ForallT _ _ t2)         = sameSymAtRoot t1 t2
---    sameSymAtRoot t1@(AppT _ _) t2@(AppT _ _) = on (==) (head.unfoldAppT) t1 t2
---    sameSymAtRoot _ _                         = False
-    match _ _ = return ()        
+    match ListT ListT                 = return ()
+    match ListT (ConT n)              
+        | isNil n      = return ()
+        | otherwise    = flush "Not Unifieable!"
+        
+    match (ConT n) ListT              
+        | isNil n      = return ()
+        | otherwise    = flush "Not Unifieable!"
+    
+    match ArrowT ArrowT               = return ()
+    match (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
+    match t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
+    match (AppT a1 b1) (AppT a2 b2)   = 
+        unify a1 a2 >> unify b1 b2
+    match _ _                         =  flush "Not Unifieable!"