[TExp is now instamce of Substitutable, Unifieable, Term, Antiunifieable (plus a lot of reorganising modules)
martin.hofmann@uni-bamberg.de**20090415145937] hunk ./src/Data/Rules.hs 15
-    module Syntax.Unifier    
+    module Syntax.Unifier       
hunk ./src/Data/Rules.hs 35
+import Syntax.Expressions
+import Syntax.Patterns
+
hunk ./src/Data/Rules.hs 148
-        (left,right)<-  antiunify2 tlhss rhss
+        (left,right)<-  antiunify2 tlhss rhss pat2Exp
hunk ./src/Language/Haskell/Meta/Syntax/Translate.hs 18
-import Data.List (foldl')
+import Data.List (foldl', nub)
hunk ./src/Language/Haskell/Meta/Syntax/Translate.hs 23
+
hunk ./src/Logging/Logger.hs 5
-    runELT,  runLM, unLM,
+    runELT,  runLM, unLM, noLog,
hunk ./src/Logging/Logger.hs 7
-    LM, 
+    LM, ELT,
hunk ./src/Syntax/Antiunifier.hs 11
-        antiunify2        -- :: (Antiunifieable k v t') => [[t]] -> [t'] -> LM ([t],t')
-      )
+        antiunify2,        -- :: (Antiunifieable k v t') => [[t]] -> [t'] -> LM ([t],t')
+        aunify,
+        mkVar
+      ),
+    computeAntiInstance, checkforAntiInstance,updateVarTable
hunk ./src/Syntax/Antiunifier.hs 22
+import Control.Monad.State (get, runStateT, put)
+import Data.List (transpose)
+
hunk ./src/Syntax/Antiunifier.hs 26
-import Control.Monad.State
-import Data.List
-import Syntax.Terms
-import Syntax.Expressions
-import Syntax.Patterns
+
hunk ./src/Syntax/Antiunifier.hs 29
-     A map from keys 'k' to values 'v' which is used in the 'AU' monad. In fact,
-     it is a many-to-one mapping to model generalisation from many terms to a 
-     variable. So, a list of keys is always mapped to the same value.
+     This is a many-to-one mapping to model generalisation from many terms to a 
+     variable (here its name). 
hunk ./src/Syntax/Antiunifier.hs 32
-type VarMap k v = (M.Map [k] v)
+type VarMap t = (M.Map [t] Name)
hunk ./src/Syntax/Antiunifier.hs 35
-     The 'AU' monad which is rewuired for antiunification. It is just a state 
-     monad 'StateT' to keep track of the replacements in a 'VarMap'. The type 
-     parameters are:
-        * the type of the keys 'k' in 'VarMap'
-        * the type of the variables 'v' in 'VarMap'
-        * the type of term 't' to antiunify
-     The value is wrapped into the 'Identity' monad to be felxible enought to
-     allow for extensions for probable logging, error handling, etc. later
+     The 'AU t' monad which is required for antiunification. It is just a state 
+     monad 'StateT' to keep track of the replacements in a 'VarMap t'. The type 
+     parameter is the type of term 't' to antiunify. The value is wrapped into 
+     the 'Identity' monad to be felxible enought to allow for extensions for 
+     probable logging, error handling, etc. later
hunk ./src/Syntax/Antiunifier.hs 41
-type AU k v t = StateT (VarMap k v) LM t
+type AU t = StateT (VarMap t) LM t
hunk ./src/Syntax/Antiunifier.hs 47
--- Shotcut to evaluate the 'AU' monad, yielding the result value and the result 
+-- Shortcut to evaluate the 'AU' monad, yielding the result value and the result 
hunk ./src/Syntax/Antiunifier.hs 79
-    
-    The parameters 'k' and 'v' specify 
-    
-        * the types of the keys 'k' 
hunk ./src/Syntax/Antiunifier.hs 80
-        * and variables 'v' 
-        
-    used in the internal representation to keep track which terms were
-    antiunified into which variable. This might be counter-intuitive, but allows
-    the variable images be of different type as the terms to antiunify. This is 
-    especially necessary when the variable image of one antiunifcation is needed
-    in another, but the terms are of different types. Consider for example the
-    terms of the previous @tail@. The terms @xs@ and @2:xs@ on the left-hand 
-    side as well as on the right-hand side should be replaced with the same 
-    variable. If the terms are of type 'Language.Haskell.TH.Clause' the left-hand
-    side is of type 'Language.Haskell.TH.Pat' whereas the right-hand side is of 
-    type 'Language.Haskell.TH.Exp' 
-    (see <http://www.haskell.org/ghc/docs/latest/html/libraries/template-haskell/Language-Haskell-TH.html> for 
-    details of the Template Haskell syntax.    
hunk ./src/Syntax/Antiunifier.hs 81
-class (Term v, Term k, Term t) => Antiunifieable k v t |t -> k v where
+class Antiunifieable t where
hunk ./src/Syntax/Antiunifier.hs 87
-    antiunifyWithMap ::  (Antiunifieable k v t) => (VarMap k v) -> [t] -> LM t
+    antiunifyWithMap ::  (Antiunifieable t) => (VarMap t) -> [t] -> LM t
hunk ./src/Syntax/Antiunifier.hs 97
-    antiunify2        :: (Antiunifieable k v t') => [[t]] -> [t'] -> LM ([t],t')
-    antiunify2 ts ts' = do
+    antiunify2        :: (Ord t', Antiunifieable t', Antiunifieable t) => [[t]] -> [t'] -> (t -> t') -> LM ([t],t')
+    antiunify2 ts ts' trans = do
hunk ./src/Syntax/Antiunifier.hs 100
-            ait'         <- antiunifyWithMap varmap ts'
+            ait'         <- antiunifyWithMap (M.mapKeys (map trans) varmap) ts'
hunk ./src/Syntax/Antiunifier.hs 102
-        
-    -- | Translator function to transform a term 't' into its representation as
-    --   a key of type 'k'
-    toKey            :: t -> k    
-    
-    -- | Translator function to transform a variable 'v' into its representation
-    --   as term of type 't'
-    fromVal          :: v -> t
hunk ./src/Syntax/Antiunifier.hs 103
-    -- | Given a term 't' and an Integer, returns a variable of type 'v'
+    -- | Given a term 't' and a Name 'n', returns a variable of type 'v' with name 'n'
hunk ./src/Syntax/Antiunifier.hs 106
-    mkVar            :: t -> Integer -> v   
+    mkVar            :: t -> Name -> t
hunk ./src/Syntax/Antiunifier.hs 110
-    aunify           :: (Antiunifieable k v t) => [t] -> AU k v t
+    aunify           :: (Antiunifieable t) => [t] -> AU t
hunk ./src/Syntax/Antiunifier.hs 230
-    
-instance Antiunifieable Exp Exp Pat where
-
-    toKey (LitP lit)              = LitE lit
-    toKey (VarP name)             = VarE name
-    toKey (TupP pats)             = TupE $ map toKey pats
-    toKey (ConP name pats)        = let keys = map toKey pats
-                                    in foldr AppE (ConE name) keys
-    toKey (InfixP p1 name p2)     = let e1 = toKey p1
-                                        e2 = toKey p2
-                                    in InfixE (Just e1)(ConE name)(Just e2)
-    toKey (ListP pats)            = ListE $ map toKey pats
-    
-    fromVal = \(VarE n) -> VarP n
-    mkVar = (\_d i -> VarE $ mkName $ "x" ++ (show i))
-
-    -- antiunifying (TupP [Pat])
-    aunify l@((TupP _):xs) = 
-        case collectSubtermsP l of
-            Just subterms -> do                
-                ai_subterms <- mapM aunify subterms
-                return $ TupP ai_subterms
-            Nothing       -> 
-                computeAntiInstance l
-    
-    -- antiunifying (ConP Name [Pat])
-    aunify l@((ConP nm _ ):xs) = 
-        case collectSubtermsP l of
-            Just subterms -> do           
-                ai_subterms <- mapM aunify subterms
-                return $ ConP nm ai_subterms
-            Nothing       -> 
-                computeAntiInstance l
-                
-    -- antiunifying (InfixP Pat Name Pat)
-    aunify l@((InfixP _ nm _):xs) =
-        case collectSubtermsP l of
-            Just subterms -> do 
-                fstai <- aunify (subterms !! 0)
-                sndai <- aunify (subterms !! 1)
-                return $ InfixP fstai nm sndai
-            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@((ListP _):xs) = 
-        case collectSubtermsP 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 $ ListP straightai 
-                  else do raggedai <- computeAntiInstance $ map ListP ragged
-                          return $ (foldr1 (\p1 p2 -> ConP '(:) [p1,p2]) (straightai ++ [raggedai]))                                     
-            Nothing     ->
-                computeAntiInstance l 
-    
-    -- antiunifying (VarP Name)              
-    aunify l@((VarP _):xs) =  
-        checkforAntiInstance l     
-    -- antiunifying (LitP Lit)
-    aunify l@((LitP _):xs) =
-        checkforAntiInstance l
-    aunify [] = 
-        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
-    
-    -- NOT IMPLEMENTED !!!
-    --    TildeP Pat  
-    --    AsP Name Pat    
-    --    WildP   
-    --    RecP Name [FieldPat] 
-    --    SigP Pat Type 
-    aunify (x:_) = 
-        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
-                "of Type Pat is not implemented!"
-                
-instance Antiunifieable Exp Exp Exp where
-    fromVal = id
-    toKey = id
-    mkVar = (\_d i -> VarE $ mkName $ "x" ++ (show i))
-    -- antiunifying (AppE Exp Exp)
-    aunify l@((AppE _ _):xs) =
-        case collectSubtermsE l of
-            Just subterms -> do
-                args1ai <- aunify (subterms !! 0)
-                args2ai <- aunify (subterms !! 1)
-                table <- get
-                if args1ai `elem` (M.elems table) -- no AppE (VarE _) _
-                  then return args1ai
-                  else return $ AppE args1ai args2ai
-            Nothing             ->
-                computeAntiInstance l
-                
-    -- antiunifying (ListE [Exp])
-    aunify l@((ListE _):xs) =
---        lift (setCurrentLogger "Terms.Antiunifier.aunify") >>
---        llogEnterDE >>
---        llogDE (text "Input arguments are :" <> pretty l) >>
-        case collectSubtermsE l of            
-            Just subterms  -> do
---                llogDE (text "Subterms are :" <> pretty subterms) 
-                let len = length l
-                    -- This is necessary for lists as eg. [[1,3],[1,2,3]] 
-                    -- after collecting subterms we get [[1,1],[3,2],[3]] which 
-                    -- must yield  (1:x:xs)
-                    -- So compute anti-instance up to minimum list length and 
-                    -- then add the anti-instance of thge rest lists
-                    straight = takeWhile (\l -> length l == len) subterms 
-                    ragged   = dropWhile (\l -> length l == len) subterms 
-                straightai <- mapM aunify straight
---                llogDE (text "Antinunified subterms (straight) are :" <> pretty straightai) 
-                if null ragged -- check if we have ragged liss at all
-                  then return $ ListE straightai -- we can keep the f*** ListE
-                          -- convert back to lists, to get correct variable image
-                  else do raggedai <- computeAntiInstance $ map ListE ragged
---                          llogDE $ text "List have different length"
---                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
-                          -- here we need the the prefix style
-                          let apps = map (AppE (ConE '(:))) straightai
-                          return $ (foldr1 AppE (apps ++ [raggedai]))                                     
-            Nothing     ->
-                computeAntiInstance l 
-                
-    -- antiunifying (TupE [Exp])        
-    aunify l@((TupE _):xs) =  
-        case collectSubtermsE l of
-            Just subterms -> do                
-                ai_subterms <- mapM aunify subterms
-                return $ TupE ai_subterms
-            Nothing       -> 
-                computeAntiInstance l         
-
-    -- antiunifying (InfixE (Maybe Exp) Exp (Maybe Exp))
-    aunify l@((InfixE _ _ _):xs) =
-        case collectSubtermsE l of
-            Just subterms -> do 
-                fstai <- aunify (subterms !! 0)
-                sndai <- aunify (subterms !! 1)
-                thrai <- aunify (subterms !! 2)
-                -- here we have to check if we there is a DummyExp in there
-                -- If so, all expressions we antiunified were sections, so put
-                -- Nothing back at place
-                let fstai' = if fstai == dexp then Nothing else Just fstai
-                let thrai' = if thrai == dexp then Nothing else Just thrai
-                return $ InfixE fstai' sndai thrai'
-            Nothing       -> 
-                  computeAntiInstance l           
-
-   -- antiunifying (CondE Exp Exp Exp)
-    aunify l@((CondE _ _ _):xs) =
-        case collectSubtermsE l of
-            Just subterms -> do 
-                fstai <- aunify (subterms !! 0)
-                sndai <- aunify (subterms !! 1)
-                thrai <- aunify (subterms !! 2)
-                return $ CondE fstai sndai thrai
-            Nothing       -> 
-                  computeAntiInstance l       
-    
-    -- antiunifying (VarE Name)              
-    aunify l@((VarE _):xs) =  
-        checkforAntiInstance l         
-    -- antiunifying (ConE Name)
-    aunify l@((ConE _):xs) =
-        checkforAntiInstance l     
-    -- antiunifying (LitE Lit)
-    aunify l@((LitE _):xs) =
-        checkforAntiInstance l
-    aunify [] = 
-        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
-        
-    -- NOT IMPLEMENTED !!!
-    --LamE [Pat] Exp  
-    --LetE [Dec] Exp  
-    --CaseE Exp [Match]   
-    --DoE [Stmt]  
-    --CompE [Stmt]    
-    --ArithSeqE Range 
-    --SigE Exp Type   
-    --RecConE Name [FieldExp] 
-    --RecUpdE Exp [FieldExp]
-    aunify (x:_) = 
-        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
-                "of Type Exp is not implemented!"
-
-    
-
-
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Exp
--------------------------------------------------------------------------------}
-
-{-|
-   A dummy data type to model antiunification of InfixE (see below). This is not 
-   very nice, but I have no clue how to do it in a more elegant way.
--}
-data DummyExp = DummyExp  
-dexp = ConE 'DummyExp
-
-{-|
-   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.
--}
-collectSubtermsE :: [Exp] -> Maybe [[Exp]]
-collectSubtermsE l = liftM transpose $ sequence $ map collector l 
-    where
-    collector = case head l of 
-        (TupE _)         -> collectSubtermsTupE
-        (AppE _ _)       -> collectSubtermsAppE
-        (ListE _)        -> collectSubtermsListE
-        (InfixE _ _ _)   -> collectSubtermsInfixE
-        (CondE _ _ _)    -> collectSubtermsCondE
-        
-    collectSubtermsTupE :: Exp -> Maybe [Exp]        
-    collectSubtermsTupE (TupE vals)         = Just vals 
-    collectSubTermsTupE _                   = Nothing
-    
-    collectSubtermsAppE :: Exp -> Maybe [Exp]
-    collectSubtermsAppE (AppE e1 e2)        = Just [e1,e2]
-    collectSubtermsAppE _                   = Nothing
-    
-    collectSubtermsListE :: Exp -> Maybe [Exp]
-    collectSubtermsListE (ListE l)          = Just l
-    collectSubtermsListE _                  = Nothing
-    
-    collectSubtermsCondE :: Exp -> Maybe [Exp]
-    collectSubtermsCondE (CondE e1 e2 e3)   = Just [e1, e2, e3]
-    collectSubtermsCondE _                  = Nothing
-    
-    -- If the expression is a section e.g. (+1) we have to substitute the value
-    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
-    collectSubtermsInfixE :: Exp -> Maybe [Exp]
-    collectSubtermsInfixE (InfixE (Just e1) e2 (Just e3)) = Just [e1, e2, e3]
-    collectSubtermsInfixE (InfixE Nothing e2 (Just e3))   = Just [dexp, e2, e3]
-    collectSubtermsInfixE (InfixE (Just e1) e2 Nothing)   = Just [e1, e2, dexp]
-    collectSubtermsInfixE (InfixE Nothing e2 Nothing)     = Just [dexp, e2, dexp]
-    collectSubtermsInfixE _                               = Nothing
-
-
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Pat 
--------------------------------------------------------------------------------}
-
-{-|
-  See 'collectSubtermsE'
--}
-collectSubtermsP :: [Pat] -> Maybe [[Pat]]
-collectSubtermsP l = liftM transpose $ sequence $ map collector l 
-    where
-    collector = case head l of 
-        (ConP nm _)     -> collectSubtermsConP nm
-        (InfixP _ nm _) -> collectSubtermsInfixP nm
-        (ListP _ )      -> collectSubtermsListP
-        (TupP _ )       -> collectSubtermsTupP
-        _owise          -> fail $ "No match for " ++ ( show l)
-
-    collectSubtermsConP nm (ConP nm' pats) 
-        | nm == nm'          = Just pats  --  always [p1,p2]
-        | otherwise          = Nothing
-    collectSubtermsConP _ _  = Nothing
-    
-    collectSubtermsInfixP nm (InfixP p1 nm' p2) 
-        | nm == nm'              = Just [p1,p2]
-        | otherwise              = Nothing
-    collectSubtermsInfixP _ _    = Nothing    
-
-    collectSubtermsListP (ListP l)          = Just l
-    collectSubtermsListP _                  = Nothing    
-     
-    collectSubtermsTupP (TupP pats)         = Just pats -- [fst,snd]
-    collectSubTermsTupP _                   = Nothing    
+   
hunk ./src/Syntax/Antiunifier.hs 232
-    
+   
hunk ./src/Syntax/Antiunifier.hs 271
-checkforAntiInstance :: (Ord k, Pretty t, Antiunifieable k v t) => [t] -> AU k v t
+checkforAntiInstance :: (Ord t, Antiunifieable t) => [t] -> AU t
hunk ./src/Syntax/Antiunifier.hs 284
-computeAntiInstance :: (Ord k, Antiunifieable k v t) => [t] -> AU k v t
+computeAntiInstance :: (Ord t, Antiunifieable t) => [t] -> AU t
hunk ./src/Syntax/Antiunifier.hs 302
-updateVarTable :: (Ord k, Antiunifieable k v t) => 
-                    (VarMap k v) -> [t] -> ((VarMap k v) , t)
+updateVarTable :: (Ord t, Antiunifieable t) => (VarMap t) -> [t] -> ((VarMap t) , t)
hunk ./src/Syntax/Antiunifier.hs 304
-    let img' = map toKey img
-    in case M.lookup img' table of
-        (Just v)    -> (table, fromVal v)
-        Nothing     -> let newval = mkVar (head img) $ toInteger(M.size table)
-                       in (M.insert img' newval table , fromVal newval)
+    case M.lookup img table of
+        (Just v)    -> (table, mkVar (head img) v)
+        Nothing     -> let name   = mkName ("x" ++ (show $ toInteger(M.size table)))
+                           newval = mkVar (head img) name
+                       in (M.insert img name table , newval)
hunk ./src/Syntax/Antiunifier.hs 310
- 
+                                  
+   
hunk ./src/Syntax/Expressions.hs 4
-import Language.Haskell.TH --(Name, mkName, Lit)
-import Syntax.Patterns
+import Language.Haskell.TH (Exp(..))
+
hunk ./src/Syntax/Expressions.hs 8
+import Syntax.Unifier
+import Syntax.Antiunifier
+
hunk ./src/Syntax/Expressions.hs 12
-import Data.List (union)
+import Data.List (union, transpose)
hunk ./src/Syntax/Expressions.hs 14
+import qualified Data.Map as M
+import qualified Data.Traversable as T
hunk ./src/Syntax/Expressions.hs 18
-import Logging
+import Control.Monad.State (get, runStateT, put)
hunk ./src/Syntax/Expressions.hs 22
+import Logging
+
hunk ./src/Syntax/Expressions.hs 33
---    | TLamE [TPat] TExp Type
-    -- | LetE [Dec] Exp
-    -- | CaseE Exp [Match]
-    -- | DoE [Stmt]
-    -- | CompE [Stmt]
-    -- | ArithSeqE Range
-    -- | SigE Exp Type
-    -- | RecConE Name [FieldExp]
-    -- | RecUpdE Exp [FieldExp]
-    deriving(Show)
-    
+--     | LamE [Pat] Exp Type
+--     | LetE [Dec] Exp
+--     | CaseE Exp [Match]
+--     | DoE [Stmt]
+--     | CompE [Stmt]
+--     | ArithSeqE Range
+--     | SigE Exp Type
+--     | RecConE Name [FieldExp]
+--     | RecUpdE Exp [FieldExp]
+    deriving(Eq, Ord, Show) -- TODO Eq should consider type equivalences
+
+--------------------------------------------------------------------------------
+-- Instance Declarations
+--------------------------------------------------------------------------------
+
hunk ./src/Syntax/Expressions.hs 68
+
+
+
+
+    
+--------------------------------------------------------------------------------
+-- 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
+
+
+
+instance Term TExp where
+    sameSymAtRoot (TVarE _ _ ) (TVarE _ _)                      = True
+    sameSymAtRoot (TConE n1 _) (TConE n2 _)                     = n1 == n2
+    sameSymAtRoot (TLitE l1 _) (TLitE l2 _)                     = l1 == l2
+--    sameSymAtRoot (TCondE c1 t1 e1) (TCondE c2 t2 e2)        = True     
+    sameSymAtRoot (TInfixE _ e1 _ _) (TInfixE _ e2 _ _)         = e1 == e2
+    -- tuples
+    sameSymAtRoot (TTupE v1s _)(TTupE v2s _)                    = on (==) length  v1s v2s
+    sameSymAtRoot t@(TAppE _ _ _ )(TTupE vs _)                  = 
+        case head.unfoldTAppE $ t of
+            (TConE n _) -> isTuple n (length vs)
+            _owise      -> False
+    sameSymAtRoot (TTupE vs _) t@(TAppE _ _ _)                  = 
+        case head.unfoldTAppE $ t of 
+            (TConE n _) -> isTuple n (length vs)
+            _owise      -> False
+    sameSymAtRoot t1@(TAppE _ _ _) t2@(TAppE _ _ _)            = 
+        on (==) (head.unfoldTAppE) t1 t2
+    -- empty Lists
+    sameSymAtRoot (TListE [] _) (TListE [] _)                    = True
+    sameSymAtRoot (TConE n _) (TListE [] _)                      = isNil n
+    sameSymAtRoot (TListE [] _)(TConE n _)                       = isNil n
+    -- empty list and other (if other is a (:) list it matches default clause)
+    sameSymAtRoot (TListE _ _)  (TListE [] _)                    = False
+    sameSymAtRoot (TListE [] _) (TListE _ _)                     = False
+    -- non-empty lists
+    sameSymAtRoot (TListE _ _) (TListE _ _)                      = True
+    sameSymAtRoot (TListE _ _) t@(TAppE _ _ _)                  = 
+        case head.unfoldTAppE $  t of
+            (TConE n _) -> isCons n
+            _owise      -> False
+    sameSymAtRoot t@(TAppE _ _ _)(TListE _ _)                   = 
+        case head.unfoldTAppE $ t of
+            (TConE n _) -> isCons n
+            _owise      -> False 
+    sameSymAtRoot  _ _                                     = False
+    
+    substitute s Root _ = s
+    substitute s pos t =
+        case pos of
+            (P i)     -> maybe t id $  moveToSubtermTE t i (Just.(substitute s Root))
+            (Dot p i) -> maybe t id $  moveToSubtermTE t i (Just.(substitute s p))
+            
+    subterms (TVarE _ _)                        = []
+    subterms (TConE _ _)                        = []
+    subterms (TLitE _ _)                        = []
+    subterms (TTupE vals _)                     = vals
+    subterms t@(TAppE _ _ _)                    = unfoldTAppEargs t
+    subterms (TListE [] _)                      = []
+    subterms (TListE (l:ls) t)                  = [l, TListE ls t] 
+--    subterms (TCondE e1 e2 e3 _)                = [e1, e2, e3]    
+    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    e                               = 
+        error $ "Terms.subterms: Not implemented for TExp " ++ (show e)
+       
+    isVar (TVarE _ _) = True
+    isVar _           = False
+                        
+    getVarNames t = map (\(TVarE n _) -> n)  $ getVars t
+        
+    hole = TConE 'Hole (ConT ''Hole)
+
+
+    
+instance Unifieable TExp where
+
+    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" 
+        
+--    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@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) = 
+--        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)
+
+
+
+instance Substitutable TExp where
+    -- | Straight forward walking down TExp-terms, pass the function call to
+    --   subterms and replace variables as specified by the Unifier.
+    --   Well, and of course some necessary lifting. 
+    apply u v@(TVarE _ _)        = 
+        case lookup v u of
+            Just val -> checkTys sameTy fail v val >> return val
+            Nothing  -> return v
+    apply u t@(TConE _ _)     = return t
+    apply u t@(TLitE _ _)     = return t
+    apply u (TListE ts ty)        = liftM2 TListE (mapM (apply u) ts) (return ty)
+    apply u (TTupE ts ty)         = liftM2 TTupE (mapM (apply u) ts) (return ty)
+    apply u (TAppE a1 a2 ty)      = liftM3 TAppE (apply u a1) (apply u a2) (return ty)
+    apply u (TInfixE e1 op e2 ty) = 
+        do subs1 <- T.sequence $ liftM (apply []) e1 -- Monad juggling because of Maybe
+           subs2 <- T.sequence $ liftM (apply []) e2 -- Maybe (m a) ~~> m (Maybe a)
+           return $ TInfixE subs1 op subs2 ty
+--    apply u (TCondE e1 e2 e3 ty)  = 
+--        liftM4 TCondE (apply u e1) (apply u e1) (apply u e1) (return ty)
+    apply u t                               =   
+        let msg =  patternNotDef [pretty u, pretty t]
+        in setCurrentLogger "Terms.Terms.apply of TExp" >>
+           logWA msg >> fail (show msg)       
+
+instance Antiunifieable TExp where
+
+    mkVar t n = TVarE n (typeOf t)
+    
+    -- antiunifying (TAppE TExp TExp Type)
+    aunify l@((TAppE _ _ ty):xs) =
+        case collectSubtermsTE l of
+            Just subterms -> do
+                args1ai <- aunify (subterms !! 0)
+                args2ai <- aunify (subterms !! 1)
+                table <- get
+                case args1ai of
+                    (TVarE n _) -> if n `elem` (M.elems table) -- no AppE (VarE _) _
+                                     then return args1ai
+                                     else return $ TAppE args1ai args2ai ty
+                    _owise   -> return $ TAppE args1ai args2ai ty
+            Nothing             ->
+                computeAntiInstance l
+                
+    -- antiunifying (TListE [TExp] Type)
+    aunify l@((TListE _ ty@(AppT _ ety)):xs) =
+--        lift (setCurrentLogger "Terms.Antiunifier.aunify") >>
+--        llogEnterDE >>
+--        llogDE (text "Input arguments are :" <> pretty l) >>
+        case collectSubtermsTE l of            
+            Just subterms  -> do
+--                llogDE (text "Subterms are :" <> pretty subterms) 
+                let len = length l
+                    -- This is necessary for lists as eg. [[1,3],[1,2,3]] 
+                    -- after collecting subterms we get [[1,1],[3,2],[3]] which 
+                    -- must yield  (1:x:xs)
+                    -- So compute anti-instance up to minimum list length and 
+                    -- then add the anti-instance of thge rest lists
+                    straight = takeWhile (\l -> length l == len) subterms 
+                    ragged   = dropWhile (\l -> length l == len) subterms 
+                straightai <- mapM aunify straight
+--                llogDE (text "Antinunified subterms (straight) are :" <> pretty straightai) 
+                if null ragged -- check if we have ragged liss at all
+                  then return $ TListE straightai ty -- we can keep the f*** ListE
+                          -- convert back to lists, to get correct variable image
+                  else do raggedai <- computeAntiInstance $ map (flip TListE ty) ragged
+--                          llogDE $ text "List have different length"
+--                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
+                          -- here we need the the prefix style
+                          let tcone = TConE '(:) (addArrowT [ety, ty, ty]) 
+                          let apps = map (\a -> TAppE tcone a ty) straightai
+                          
+                          return $ foldTAppE1 (apps ++ [raggedai])                                     
+            Nothing     ->
+                computeAntiInstance l 
+                
+    -- antiunifying (TTupE [TExp] Type)        
+    aunify l@((TTupE _ ty):xs) =  
+        case collectSubtermsTE l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TTupE ai_subterms ty
+            Nothing       -> 
+                computeAntiInstance l         
+
+    -- antiunifying (TInfixE (Maybe TExp) TExp (Maybe TExp) Type)
+    aunify l@((TInfixE _ _ _ ty):xs) =
+        case collectSubtermsTE l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                thrai <- aunify (subterms !! 2)
+                -- here we have to check if we there is a DummyExp in there
+                -- If so, all expressions we antiunified were sections, so put
+                -- Nothing back at place
+                let fstai' = if fstai == dummy then Nothing else Just fstai
+                let thrai' = if thrai == dummy then Nothing else Just thrai
+                return $ TInfixE fstai' sndai thrai' ty
+            Nothing       -> 
+                  computeAntiInstance l           
+
+--   -- antiunifying (TCondE TExp TExp TExp Type)
+--    aunify l@((TCondE _ _ _ ty):xs) =
+--        case collectSubtermsTE l of
+--            Just subterms -> do 
+--                fstai <- aunify (subterms !! 0)
+--                sndai <- aunify (subterms !! 1)
+--                thrai <- aunify (subterms !! 2)
+--                return $ TCondE fstai sndai thrai ty
+--            Nothing       -> 
+--                  computeAntiInstance l       
+    
+    -- antiunifying (VarE Name)              
+    aunify l@((TVarE _ _):xs) =  
+        checkforAntiInstance l         
+    -- antiunifying (ConE Name)
+    aunify l@((TConE _ _):xs) =
+        checkforAntiInstance l     
+    -- antiunifying (LitE Lit)
+    aunify l@((TLitE _ _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify at TExp: empty list, no terms to antiunify"
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify at TExp: Antiunification for " ++ show x ++
+                "of Type TExp is not implemented!"
+----------------------
+-- Unification and Matching
+----------------------
+
+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 
+
+walkerTExp wf s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = 
+    (check wf) flush s t >> walkerTExp wf s1 t1 >> walkerTExp wf s2 t2
+
+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)
+----------------------------------------------------------------------------------
+
+-- | Helper for lifting a walker (Unifieable t) => (Maybe t) (Maybe t)
+liftUnify :: (Unifieable t) => Maybe t -> Maybe t -> U t
+liftUnify = (\u v -> maybe (return ()) (\(s,t) -> unify s t) (liftM2 (,) u v))
+
+-- | Helper for matching (Unifieable t) => (Maybe t) (Maybe t)
+liftMatch :: (Unifieable t) => Maybe t -> Maybe t -> U t
+liftMatch = (\u v -> maybe (return ()) (\(s,t) -> match s t) (liftM2 (,) u v))     
+   
+-- | 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
+
+
+----------------------
+-- Antiunification
+----------------------
+{-|
+   A dummy data type to model antiunification of InfixE (see below). This is not 
+   very nice, but I have no clue how to do it in a more elegant way.
+-}
+data DummyTExp = DummyTExp  
+dummy = TConE 'DummyExp (ConT ''DummyExp)
+
+{-|
+   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.
+-}
+collectSubtermsTE :: [TExp] -> Maybe [[TExp]]
+collectSubtermsTE l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = collectSubterms (head l)
+        
+    collectSubterms :: (Monad m) => TExp -> TExp -> m [TExp]        
+    collectSubterms s@(TTupE _ _) t@(TTupE vals _) = 
+        checkTys sameTy fail s t >> return vals        
+    collectSubterms s@(TAppE _ _ _) t@(TAppE e1 e2 _) = 
+        checkTys sameTy fail s t >> return [e1,e2]      
+    collectSubterms s@(TListE _ _) t@(TListE l _) = 
+        checkTys sameTy fail s t >> return l      
+--    collectSubterms s@(TCondE _ _ _ _) t@(TCondE e1 e2 e3 _) = 
+--        check fail s t >> return [e1, e2, e3]    
+    -- If the expression is a section e.g. (+1) we have to substitute the value
+    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
+    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE (Just e1) e2 (Just e3) _) = 
+        checkTys sameTy fail s t >> return [e1, e2, e3]
+    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE Nothing e2 (Just e3) _)   = 
+        checkTys sameTy fail s t >> return [dummy, e2, e3]
+    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE (Just e1) e2 Nothing _)   = 
+        checkTys sameTy fail s t >> return [e1, e2, dummy]
+    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE Nothing e2 Nothing _)     = 
+        checkTys sameTy fail s t >> return [dummy, e2, dummy]
+    collectSubterms _ _                               = fail ""
+
+    
+-- |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.
+moveToSubtermTE :: (Monad m) => TExp -> Int -> (TExp -> m TExp) -> m TExp
+moveToSubtermTE (TVarE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"        
+moveToSubtermTE (TLitE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"    
+moveToSubtermTE (TConE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"
+    
+moveToSubtermTE t@(TAppE _ _ _ ) i f  = do
+    let (op:args) = (unfoldTAppE t)     
+    -- the first element is the operator name
+    liftM  (foldTAppE op) (applyAtIndex args i f)
+    
+moveToSubtermTE (TTupE es ty) i f      = 
+   liftM2 TTupE (applyAtIndex es i f) (return ty)
+    
+moveToSubtermTE (TListE (e:es) ty) i f = do
+    let elist = [e, TListE es ty]
+    [e', TListE es' ty'] <- (applyAtIndex elist i f)
+    return $ TListE (e':es') ty'
+    
+moveToSubtermTE (TInfixE (Just e1) op e2 ty) 0 f = 
+    do { e <- f e1; return $ (TInfixE (Just e) op e2 ty)}
+moveToSubtermTE (TInfixE e1 op (Just e2) ty) 1 f = 
+    do { e <- f e2; return $ (TInfixE e1 op (Just e) ty)}
+moveToSubtermTE (TInfixE _ op _ _) i _          = 
+    fail $ "Terms.moveToSubtermE: No subterm at position " ++ (show i) ++ 
+           " of operator " ++ (show op)
+
+{-
+################################################################################
+            DEPRECATED STUFF I DON'T WANT TO DELETE YET !
+################################################################################
+-}
+--------------------------------------------------------------------------------
+-- Deprecated Exp instance declarations
+--------------------------------------------------------------------------------    
+
+           
+
+--------------------------------------------------------------------------------
+-- Exp
+--------------------------------------------------------------------------------
+
hunk ./src/Syntax/Expressions.hs 677
-
+                                
+    getVarNames t = map (\(VarE n) -> n)  $ getVars t
+        
+    hole = ConE 'Hole 
hunk ./src/Syntax/Expressions.hs 720
-                        
-    getVarNames t = map (\(VarE n) -> n)  $ getVars t
-        
-    hole = ConE 'Hole
hunk ./src/Syntax/Expressions.hs 721
---------------------------------------------------------------------------------
--- Auxiliary functions for 'Exp' as 'Term's
---------------------------------------------------------------------------------
+ 
hunk ./src/Syntax/Expressions.hs 723
--- | Returns only the arguments of an 'AppE'xpression.
-unfoldAppEargs = tail . unfoldAppE
+instance Substitutable Exp where
+        -- | Straight forward walking down Exp-terms, pass the function call to
+    --   subterms and replace variables as specified by the Unifier.
+    --   Well, and of course some necessary lifting. 
+    apply u v@(VarE _)        = case lookup v u of 
+                                     Just val -> return val
+                                     Nothing  -> return v
+    apply u t@(ConE _ )       = return t
+    apply u t@(LitE _)        = return t
+    apply u (ListE ts)        = liftM ListE (mapM (apply u) ts)
+    apply u (TupE ts)         = liftM TupE (mapM (apply u) ts)
+    apply u (AppE a1 a2)      = liftM2 AppE (apply u a1) (apply u a2)
+    apply u (InfixE e1 op e2) = 
+        do subs1 <- T.sequence $ liftM (apply []) e1 -- Monad juggling because of Maybe
+           subs2 <- T.sequence $ liftM (apply []) e2 -- Maybe (m a) ~~> m (Maybe a)
+           return $ InfixE subs1 op subs2
+    apply u (CondE e1 e2 e3)  = 
+        liftM3 CondE (apply u e1) (apply u e1) (apply u e1)
+    apply u t                               =   
+        let msg =  patternNotDef [pretty u, pretty t]
+        in setCurrentLogger "Terms.Unifier.applyMgu" >>
+           logWA msg >> fail (show msg)
hunk ./src/Syntax/Expressions.hs 746
--- | 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
+      
+                        
+instance Unifieable Exp where
hunk ./src/Syntax/Expressions.hs 751
--- |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"
+    -- matching variables
+    match s@(VarE i1) t@(VarE i2)
+        | i1 == i2                          = return ()
+        | otherwise                         = matchVar s t
+    match s@(VarE _) t                      = matchVar s t
+    match s          t@(VarE _)             = flush "No Match!"
+    -- matching constructors    
+    match s@(ConE _) t@(ConE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush "No Match!"  
+    -- matching literals          
+    match s@(LitE _) t@(LitE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush "No Match!" 
+    -- matching tuples
+    match (TupE s) (TupE t) 
+        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
+        | otherwise                         = flush "No Match!"
+    match (TupE s) t@(AppE _ _)             = 
+        case unfoldAppE t of
+            ((ConE n):args) ->
+                if isTuple n  (length s)  
+                  then mapM_ (uncurry match) (zip s args)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
+    match t@(AppE _ _)(TupE s)              =      
+        case unfoldAppE t of
+            ((ConE n):args) ->
+                if isTuple n  (length s) 
+                  then mapM_ (uncurry match) (zip args s)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
+        
+    match (ListE [])(ListE [])              = return ()
+    match (ListE (s:ss))(ListE (t:ts))      = match s t >> match (ListE ss) (ListE ts)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    match (ListE [])c@(ConE n)               
+        | isNil n                           = return ()
+        | otherwise                         = flush "No Match!"  
+    match c@(ConE n)(ListE [])              
+        | isNil n                           = return ()
+        | otherwise                         = flush "No Match!"  
+    match (ListE (s:ss)) t@(AppE _ _)       =
+        case unfoldAppE t of
+            ((ConE n):a1:[a2]) ->
+                if isCons n
+                  then match s a1 >> match (ListE ss) a2
+                  else flush "No Match!"  
+            _owise       -> flush "No Match!"  
+    match t@(AppE _ _) (ListE (s:ss))       =
+        case unfoldAppE t of
+            ((ConE n):a1:[a2]) ->
+                if isCons n
+                  then match s a1 >> match (ListE ss) a2
+                  else flush "No Match!"  
+            _owise       -> flush "No Match!"  
hunk ./src/Syntax/Expressions.hs 809
-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)
+    match (AppE s1 s2)(AppE t1 t2)          = match s1 t1 >> match s2 t2
hunk ./src/Syntax/Expressions.hs 811
-moveToSubtermE (TupE es) i f      = 
-   liftM TupE (applyAtIndex es i f)
+    match (InfixE s1 s2 s3)(InfixE t1 t2 t3)
+        | s2 == t2                          = liftMatch s1 t1 >> liftMatch s3 t3
+        | otherwise                         = flush "No Match!"        
+    match (CondE s1 s2 s3) (CondE t1 t2 t3) = 
+        match s1 t1 >> match s2 t2 >> match s3 t3    
+    match s t                               =
+        let msg =  patternNotDef [pretty s, pretty t]
+        in lift (setCurrentLogger "Terms.Unifier.match") >>
+           llogWA msg >> llogDE (hsep (map pretty (unfoldAppE t))) >>
+           fail (show msg)
+         
hunk ./src/Syntax/Expressions.hs 823
-moveToSubtermE (ListE (e:es)) i f = do
-    let elist = [e, ListE es]
-    [e', ListE es'] <- (applyAtIndex elist i f)
-    return $ ListE (e':es')
+    unify s@(VarE _) t@(VarE _)
+        |(s == t)                           = return ()
+        | otherwise                         = unifyVar s t
+    unify s@(VarE _) t                      = unifyVar s t
+    unify s          t@(VarE _)             = unifyVar t s    
hunk ./src/Syntax/Expressions.hs 829
-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)
-                                    
+    unify s@(ConE _) t@(ConE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush "Not unifieable" 
+        
+    unify s@(LitE _) t@(LitE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush "Not unifieable"
+         
+    unify (TupE s) (TupE t) 
+        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
+        | otherwise                         = flush "Not unifieable"
+    unify (TupE s) t@(AppE _ _)             = 
+        case unfoldAppE t of
+            ((ConE n):args) ->
+                if isTuple n  (length s) 
+                  then mapM_ (uncurry unify) (zip s args)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
+    unify t@(AppE _ _)(TupE s)              = 
+        case unfoldAppE t of
+            ((ConE n):args) ->
+                if isTuple n  (length s) 
+                  then mapM_ (uncurry unify) (zip s args)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"
+    unify (ListE [])(ListE [])              = return ()
+    unify (ListE (s:ss))(ListE (t:ts))      = 
+        unify s t >> unify (ListE ss) (ListE ts)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    unify (ListE [])c@(ConE n)             
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "Not unifieable!"  
+    unify c@(ConE n)(ListE [])              
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "Not unifieable!"  
+    unify (ListE (s:ss)) t@(AppE _ _)       = 
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then unify s a1 >> unify (ListE ss) a2
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable" 
+    unify t@(AppE _ _) (ListE (s:ss))       =
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then unify s a1 >> unify (ListE ss) a2
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable" 
+    
+    unify (AppE s1 s2)(AppE t1 t2)          = unify s1 t1 >> unify s2 t2
+    
+    unify (InfixE s1 s2 s3)(InfixE t1 t2 t3)
+        | s2 == t2                          = liftUnify s1 t1 >> liftUnify s3 t3
+        | otherwise                         = flush "Not unifieable" 
+        
+    unify (CondE s1 s2 s3) (CondE t1 t2 t3) = 
+        unify s1 t1 >> unify s2 t2 >> unify s3 t3
+    
+    unify s t                               =   
+        let msg =  patternNotDef [pretty s, pretty t]
+        in lift (setCurrentLogger "Terms.Unifier.unify") >>
+           llogWA msg >> llogDE (hsep (map pretty (unfoldAppE t))) >>
+           fail ( show msg)            
+           
hunk ./src/Syntax/Expressions.hs 896
---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 897
+instance Antiunifieable Exp where
+
+    mkVar _ n = VarE n
+    
+    -- antiunifying (AppE Exp Exp)
+    aunify l@((AppE _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do
+                args1ai <- aunify (subterms !! 0)
+                args2ai <- aunify (subterms !! 1)
+                table <- get
+                case args1ai of
+                    (VarE n) -> if n `elem` (M.elems table) -- no AppE (VarE _) _
+                                  then return args1ai
+                                  else return $ AppE args1ai args2ai
+                    _owise   -> return $ AppE args1ai args2ai
+            Nothing             ->
+                computeAntiInstance l
+                
+    -- antiunifying (ListE [Exp])
+    aunify l@((ListE _):xs) =
+--        lift (setCurrentLogger "Terms.Antiunifier.aunify") >>
+--        llogEnterDE >>
+--        llogDE (text "Input arguments are :" <> pretty l) >>
+        case collectSubtermsE l of            
+            Just subterms  -> do
+--                llogDE (text "Subterms are :" <> pretty subterms) 
+                let len = length l
+                    -- This is necessary for lists as eg. [[1,3],[1,2,3]] 
+                    -- after collecting subterms we get [[1,1],[3,2],[3]] which 
+                    -- must yield  (1:x:xs)
+                    -- So compute anti-instance up to minimum list length and 
+                    -- then add the anti-instance of thge rest lists
+                    straight = takeWhile (\l -> length l == len) subterms 
+                    ragged   = dropWhile (\l -> length l == len) subterms 
+                straightai <- mapM aunify straight
+--                llogDE (text "Antinunified subterms (straight) are :" <> pretty straightai) 
+                if null ragged -- check if we have ragged liss at all
+                  then return $ ListE straightai -- we can keep the f*** ListE
+                          -- convert back to lists, to get correct variable image
+                  else do raggedai <- computeAntiInstance $ map ListE ragged
+--                          llogDE $ text "List have different length"
+--                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
+                          -- here we need the the prefix style
+                          let apps = map (AppE (ConE '(:))) straightai
+                          return $ (foldr1 AppE (apps ++ [raggedai]))                                     
+            Nothing     ->
+                computeAntiInstance l 
+                
+    -- antiunifying (TupE [Exp])        
+    aunify l@((TupE _):xs) =  
+        case collectSubtermsE l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TupE ai_subterms
+            Nothing       -> 
+                computeAntiInstance l         
+
+    -- antiunifying (InfixE (Maybe Exp) Exp (Maybe Exp))
+    aunify l@((InfixE _ _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                thrai <- aunify (subterms !! 2)
+                -- here we have to check if we there is a DummyExp in there
+                -- If so, all expressions we antiunified were sections, so put
+                -- Nothing back at place
+                let fstai' = if fstai == dexp then Nothing else Just fstai
+                let thrai' = if thrai == dexp then Nothing else Just thrai
+                return $ InfixE fstai' sndai thrai'
+            Nothing       -> 
+                  computeAntiInstance l           
+
+   -- antiunifying (CondE Exp Exp Exp)
+    aunify l@((CondE _ _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                thrai <- aunify (subterms !! 2)
+                return $ CondE fstai sndai thrai
+            Nothing       -> 
+                  computeAntiInstance l       
+    
+    -- antiunifying (VarE Name)              
+    aunify l@((VarE _):xs) =  
+        checkforAntiInstance l         
+    -- antiunifying (ConE Name)
+    aunify l@((ConE _):xs) =
+        checkforAntiInstance l     
+    -- antiunifying (LitE Lit)
+    aunify l@((LitE _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
+        
+    -- NOT IMPLEMENTED !!!
+    --LamE [Pat] Exp  
+    --LetE [Dec] Exp  
+    --CaseE Exp [Match]   
+    --DoE [Stmt]  
+    --CompE [Stmt]    
+    --ArithSeqE Range 
+    --SigE Exp Type   
+    --RecConE Name [FieldExp] 
+    --RecUpdE Exp [FieldExp]
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Exp is not implemented!"
+
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Exp
+-------------------------------------------------------------------------------}
+
+{-|
+   A dummy data type to model antiunification of InfixE (see below). This is not 
+   very nice, but I have no clue how to do it in a more elegant way.
+-}
+data DummyExp = DummyExp  
+dexp = ConE 'DummyExp
+
+{-|
+   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.
+-}
+collectSubtermsE :: [Exp] -> Maybe [[Exp]]
+collectSubtermsE l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = case head l of
+        (TupE _)         -> collectSubtermsTupE
+         -- TODO what about mixed terms with ListE and AppE (ConE "GHC.Types.[]") _)?
+        (AppE _ _)       -> collectSubtermsAppE
+        (ListE _)        -> collectSubtermsListE
+        (InfixE _ _ _)   -> collectSubtermsInfixE
+        (CondE _ _ _)    -> collectSubtermsCondE
+        
+    collectSubtermsTupE :: Exp -> Maybe [Exp]        
+    collectSubtermsTupE (TupE vals)         = Just vals 
+    collectSubTermsTupE _                   = Nothing
+    
+    collectSubtermsAppE :: Exp -> Maybe [Exp]
+    collectSubtermsAppE (AppE e1 e2)        = Just [e1,e2]
+    collectSubtermsAppE _                   = Nothing
+    
+    collectSubtermsListE :: Exp -> Maybe [Exp]
+    collectSubtermsListE (ListE l)          = Just l
+    collectSubtermsListE _                  = Nothing
+    
+    collectSubtermsCondE :: Exp -> Maybe [Exp]
+    collectSubtermsCondE (CondE e1 e2 e3)   = Just [e1, e2, e3]
+    collectSubtermsCondE _                  = Nothing
+    
+    -- If the expression is a section e.g. (+1) we have to substitute the value
+    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
+    collectSubtermsInfixE :: Exp -> Maybe [Exp]
+    collectSubtermsInfixE (InfixE (Just e1) e2 (Just e3)) = Just [e1, e2, e3]
+    collectSubtermsInfixE (InfixE Nothing e2 (Just e3))   = Just [dexp, e2, e3]
+    collectSubtermsInfixE (InfixE (Just e1) e2 Nothing)   = Just [e1, e2, dexp]
+    collectSubtermsInfixE (InfixE Nothing e2 Nothing)     = Just [dexp, e2, dexp]
+    collectSubtermsInfixE _                               = Nothing
hunk ./src/Syntax/Expressions.hs 1061
+           
hunk ./src/Syntax/Patterns.hs 4
-import Language.Haskell.TH 
+ 
hunk ./src/Syntax/Patterns.hs 7
+import Syntax.Unifier
+import Syntax.Antiunifier
+
hunk ./src/Syntax/Patterns.hs 12
+import Control.Monad.State (get, runStateT, put)
hunk ./src/Syntax/Patterns.hs 14
-import Data.List (union)
+import Data.List (union, transpose)
hunk ./src/Syntax/Patterns.hs 113
- 
hunk ./src/Syntax/Patterns.hs 114
+instance Substitutable Pat where
+    apply u v@(VarP _)        = case lookup v u of 
+                                     Just val -> return val
+                                     Nothing  -> return v
+    apply u (ConP n ps)       = liftM (ConP n) (mapM (apply u) ps )
+    apply u t@(LitP _)        = return t
+    apply u (ListP ts)        = liftM ListP (mapM (apply u) ts)
+    apply u (TupP ts)         = liftM TupP (mapM (apply u) ts)
+    apply u (InfixP e1 op e2) =
+        liftM3 InfixP (apply u e1) (return op) (apply u e2)
+    apply u t                 =   
+        let msg =  patternNotDef [ pretty u, pretty t]
+        in  setCurrentLogger "Terms.Unifier.applyMgu" >>
+            logWA msg >> fail ( show msg)  
+
+instance Unifieable Pat where
+    
+
+    match s@(VarP _) t@(VarP _ )           
+        | s == t                          = return ()
+        | otherwise                       = matchVar s t
+    match s@(VarP _) t                    = matchVar s t
+    match s          t@(VarP _)           = matchVar t s          
+    match s@(LitP _) t@(LitP _) 
+        | (s == t)                        = return () 
+        | otherwise                       = flush  "No Match!"         
+    match (ListP [])(ListP [])            = return ()
+    match (ListP (s:ss))(ListP (t:ts))    = match s t >> match (ListP ss) (ListP ts) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    match (ListP [])(ConP n [])
+        | isNil n                       = return ()
+        | otherwise                       = flush  "No Match!"  
+    match(ConP n []) (ListP [])
+        | isNil n                         = return ()
+        | otherwise                       = flush  "No Match!"  
+    match (ListP (s:ss))(ConP n ([p,ps]))
+        | isCons n                        = match s p >> match (ListP ss) ps
+        | otherwise                       = flush  "No Match!"  
+    match(ConP n ([p,ps])) (ListP (s:ss))
+        | isCons n                        = match s p >> match (ListP ss) ps
+        | otherwise                       = flush  "No Match!"  
+    match s@(ListP _) t@(ConP _ _)        = match t s    
+    match s@(ConP n1 p1) t@(ConP n2 p2) 
+        | n1 == n2                        = mapM_ (uncurry match) (zip p1 p2)
+        | otherwise                       = flush  "No Match!"          
+    match (TupP s) (TupP t) 
+        | (length s) == (length t)        = mapM_ (uncurry match) (zip s t)
+        | otherwise                       = flush  "No Match!"       
+    match (ConP n p) (TupP t)              
+        | isTuple n (length t)            = mapM_ (uncurry match) (zip p t)
+        | otherwise                       = flush "No Match!"      
+    match (TupP t)(ConP n p)               
+        | isTuple n (length t)            = mapM_ (uncurry match) (zip p t)
+        | otherwise                       = flush "No Match!"      
+    match (InfixP s1 s2 s3)(InfixP t1 t2 t3)
+        | s2 == t2                        = match s1 t1 >> match s3 t3
+        | otherwise = flush  "No Match!"          
+    match s t                             =    
+        flush  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))
+        
+    
+    unify s@(VarP _) t@(VarP _ )        
+        | s == t                       = return ()
+        | otherwise                    = unifyVar s t
+    unify s@(VarP _) t                 = unifyVar s t
+    unify s          t@(VarP _)        = unifyVar t s         
+    unify s@(LitP _) t@(LitP _) 
+        | (s == t)                     = return () 
+        | otherwise                    = flush  "Not unifieable"         
+    unify (ListP [])(ListP [])         = return ()
+    unify (ListP (s:ss))(ListP (t:ts)) = unify s t >> unify (ListP ss) (ListP ts) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    unify (ListP [])(ConP n [])        
+        | isNil n                      = return ()
+        | otherwise                    = flush "Not unifieable"
+    unify(ConP n []) (ListP [])
+        | isNil n                       = return ()
+        | otherwise                    = flush  "Not unifieable"
+    unify (ListP (s:ss))(ConP n ([p,ps]))
+        | isCons n                     = unify s p >> unify (ListP ss) ps
+        | otherwise                    = flush "Not unifieable"
+    unify(ConP n ([p,ps])) (ListP (s:ss))
+        | isCons n                    = unify s p >> unify (ListP ss) ps
+        | otherwise                    = flush "Not unifieable"    
+    unify s@(ConP n1 p1) t@(ConP n2 p2) 
+        | n1 == n2                     = mapM_ (uncurry unify) (zip p1 p2)
+        | otherwise                    = flush  "Not unifieable"        
+    unify (TupP s) (TupP t) 
+        | (length s) == (length t)     = mapM_ (uncurry unify) (zip s t)
+        | otherwise                    = flush  "Not unifieable"       
+    unify (ConP n p) (TupP t) 
+        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
+        | otherwise                    = flush  "Not unifieable"       
+    unify (TupP t)(ConP n p) 
+        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
+        | otherwise                    = flush  "Not unifieable" 
+    unify (InfixP s1 s2 s3)(InfixP t1 t2 t3)
+        | s2 == t2                     = unify s1 t1 >> unify s3 t3
+        | otherwise = flush  "Not unifieable"        
+    unify s t                          = 
+        flush  ("Term " ++ (show s) ++ "not unifieable with " ++ (show t))
+        
hunk ./src/Syntax/Patterns.hs 241
+  
+instance Antiunifieable Pat where
+
+--    toKey (LitP lit)              = LitE lit
+--    toKey (VarP name)             = VarE name
+--    toKey (TupP pats)             = TupE $ map toKey pats
+--    toKey (ConP name pats)        = let keys = map toKey pats
+--                                    in foldr AppE (ConE name) keys
+--    toKey (InfixP p1 name p2)     = let e1 = toKey p1
+--                                        e2 = toKey p2
+--                                    in InfixE (Just e1)(ConE name)(Just e2)
+--    toKey (ListP pats)            = ListE $ map toKey pats
+--    
+--    fromVal = \(VarE n) -> VarP n
+    mkVar _ n = VarP n
+
+    -- antiunifying (TupP [Pat])
+    aunify l@((TupP _):xs) = 
+        case collectSubtermsP l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TupP ai_subterms
+            Nothing       -> 
+                computeAntiInstance l
+    
+    -- antiunifying (ConP Name [Pat])
+    aunify l@((ConP nm _ ):xs) = 
+        case collectSubtermsP l of
+            Just subterms -> do           
+                ai_subterms <- mapM aunify subterms
+                return $ ConP nm ai_subterms
+            Nothing       -> 
+                computeAntiInstance l
+                
+    -- antiunifying (InfixP Pat Name Pat)
+    aunify l@((InfixP _ nm _):xs) =
+        case collectSubtermsP l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                return $ InfixP fstai nm sndai
+            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@((ListP _):xs) = 
+        case collectSubtermsP 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 $ ListP straightai 
+                  else do raggedai <- computeAntiInstance $ map ListP ragged
+                          return $ (foldr1 (\p1 p2 -> ConP '(:) [p1,p2]) (straightai ++ [raggedai]))                                     
+            Nothing     ->
+                computeAntiInstance l 
+    
+    -- antiunifying (VarP Name)              
+    aunify l@((VarP _):xs) =  
+        checkforAntiInstance l     
+    -- antiunifying (LitP Lit)
+    aunify l@((LitP _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
+    
+    -- NOT IMPLEMENTED !!!
+    --    TildeP Pat  
+    --    AsP Name Pat    
+    --    WildP   
+    --    RecP Name [FieldPat] 
+    --    SigP Pat Type 
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Pat is not implemented!"
+                
+
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Pat 
+-------------------------------------------------------------------------------}
+
+{-|
+  See 'collectSubtermsE'
+-}
+collectSubtermsP :: [Pat] -> Maybe [[Pat]]
+collectSubtermsP l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = case head l of 
+        (ConP nm _)     -> collectSubtermsConP nm
+        (InfixP _ nm _) -> collectSubtermsInfixP nm
+        (ListP _ )      -> collectSubtermsListP
+        (TupP _ )       -> collectSubtermsTupP
+        _owise          -> fail $ "No match for " ++ ( show l)
+
+    collectSubtermsConP nm (ConP nm' pats) 
+        | nm == nm'          = Just pats  --  always [p1,p2]
+        | otherwise          = Nothing
+    collectSubtermsConP _ _  = Nothing
+    
+    collectSubtermsInfixP nm (InfixP p1 nm' p2) 
+        | nm == nm'              = Just [p1,p2]
+        | otherwise              = Nothing
+    collectSubtermsInfixP _ _    = Nothing    
+
+    collectSubtermsListP (ListP l)          = Just l
+    collectSubtermsListP _                  = Nothing    
+     
+    collectSubtermsTupP (TupP pats)         = Just pats -- [fst,snd]
+    collectSubTermsTupP _                   = Nothing    
hunk ./src/Syntax/Patterns.hs 359
+    
hunk ./src/Syntax/Terms.hs 11
-    Substitution, Replacement, nullSubst, (<~), insertApply,
+--    Substitutable(..),
+--    Substitution, Replacement, nullSubst, (<~), insertApply,
hunk ./src/Syntax/Terms.hs 20
+    pat2Exp,
hunk ./src/Syntax/Terms.hs 24
-import Language.Haskell.TH ( Dec (FunD)
-                           , Clause (Clause)
-                           , Body (NormalB)
-                         --  , Exp (VarE, ConE, LitE, ListE, TupE, InfixE, AppE, CondE)
-                         --  , Pat (VarP, ConP, LitP, ListP, TupP, InfixP) 
-                           , Q(..)
-                           , Name, mkName) 
-import Language.Haskell.TH.Syntax
-import Language.Haskell.TH.Ppr
+--import Language.Haskell.TH ( Dec (FunD)
+--                           , Clause (Clause)
+--                           , Body (NormalB)
+--                         --  , Exp (VarE, ConE, LitE, ListE, TupE, InfixE, AppE, CondE)
+--                         --  , Pat (VarP, ConP, LitP, ListP, TupP, InfixP) 
+--                           , Q(..)
+--                           , Name, mkName) 
+--import Language.Haskell.TH.Syntax
+--import Language.Haskell.TH.Ppr
hunk ./src/Syntax/Terms.hs 41
-
hunk ./src/Syntax/Terms.hs 221
---------------------------------------------------------------------------------
--- 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]
hunk ./src/Syntax/Terms.hs 222
-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)
-
-class Substitute a where
-    apply :: (Substitution a) -> a -> a
-    
hunk ./src/Syntax/Types.hs 2
-module Syntax.Types where
+module Syntax.Types (
hunk ./src/Syntax/Types.hs 4
-import Language.Haskell.TH --(Type(..), Cxt)
+    sameTy, isGenTy, equalTys,
+    Typed(..),
+    splitArrowT, reduceArrowT, unArrowT, addArrowT, addPredicates, 
+    unfoldAppTargs, fixType,
+    module Language.Haskell.TH
+    ) where
+
+import Language.Haskell.TH (Type(..), Cxt)
hunk ./src/Syntax/Types.hs 13
+import Syntax.Unifier
+import Syntax.Antiunifier
hunk ./src/Syntax/Types.hs 18
-import Logging
- 
+
+--import UI.Context
+
hunk ./src/Syntax/Types.hs 33
+sameTy :: (Typed t) => t -> t -> Bool
+sameTy = equalTys `on` typeOf
hunk ./src/Syntax/Types.hs 36
+-- TODO 
+isGenTy :: (Typed t) => t -> t -> Bool
+isGenTy = sameTy 
+    
+equalTys :: Type -> Type -> Bool
+equalTys (VarT _) (VarT _)           = True
+equalTys (ConT n1) (ConT n2)         = n1 == n2
+-- tuples
+equalTys (TupleT i1) (TupleT i2)     = i1 == i2
+equalTys (TupleT i) (ConT n)         = isTuple n i
+equalTys (ConT n)(TupleT i)          = isTuple n i
+-- lists
+equalTys ListT ListT                 = True
+equalTys ListT (ConT n)              = isNil n
+equalTys (ConT n) ListT              = isNil n
+
+equalTys ArrowT ArrowT               = True
+equalTys (ForallT n1 c1 t1) (ForallT n2 c2 t2)  = -- TODO how to compare contexts
+    all (uncurry equalTys) (zip c1 c2) && equalTys t1 t2
+equalTys (AppT t11 t12) (AppT t21 t22) = 
+    (equalTys t11 t21) && (equalTys t12 t22)
+equalTys _ _                         = False
hunk ./src/Syntax/Types.hs 60
-instance Term Type where
-    sameSymAtRoot (VarT _) (VarT _)           = True
-    sameSymAtRoot (ConT n1) (ConT n2)         = n1 == n2
-    -- tuples
-    sameSymAtRoot (TupleT i1) (TupleT i2)     = i1 == i2
-    sameSymAtRoot (TupleT i) (ConT n)         = isTuple n i
-    sameSymAtRoot (ConT n)(TupleT i)          = isTuple n i
-    -- lists
-    sameSymAtRoot ListT ListT                 = True
-    sameSymAtRoot 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
-    
-    
-    subterms (ForallT _ _ t) = subterms t
-    subterms t@(AppT _ _)    = unfoldAppTargs t
-    subterms _               = []
-    
-    substitute _ _ _ =  error "substitute for Type not imlemented"
-    
-    isVar (VarT _) = True
-    isVar _        = False
-    
-    getVarNames = (map (\(VarT n) -> n)) . getVars 
-    
-    hole =  ConT ''Hole
hunk ./src/Syntax/Types.hs 78
+addArrowT :: [Type] -> Type
+addArrowT ts = foldl1 AppT $ map (AppT ArrowT) ts 
hunk ./src/Syntax/Types.hs 116
+instance Term Type where
+    sameSymAtRoot (VarT _) (VarT _)           = True
+    sameSymAtRoot (ConT n1) (ConT n2)         = n1 == n2
+    -- tuples
+    sameSymAtRoot (TupleT i1) (TupleT i2)     = i1 == i2
+    sameSymAtRoot (TupleT i) (ConT n)         = isTuple n i
+    sameSymAtRoot (ConT n)(TupleT i)          = isTuple n i
+    -- lists
+    sameSymAtRoot ListT ListT                 = True
+    sameSymAtRoot 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
+    
+    
+    subterms (ForallT _ _ t) = subterms t
+    subterms t@(AppT _ _)    = unfoldAppTargs t
+    subterms _               = []
+    
+    substitute _ _ _ =  error "substitute for Type not imlemented"
+    
+    isVar (VarT _) = True
+    isVar _        = False
+    
+    getVarNames = (map (\(VarT n) -> n)) . getVars 
+    
+    hole =  ConT ''Hole  
+
hunk ./src/Syntax/Types.hs 149
+
+instance Unifieable Type where
+
+    unify t1@(VarT _) t2@(VarT _)   = unifyVar t1 t2
+    unify (ConT n1) (ConT n2)       
+        | n1 == n2  = return ()
+        | otherwise = fail "Not Unifieable!"
+    -- tuples
+    unify (TupleT i1) (TupleT i2)     
+        | i1 == i2  = return ()
+        | otherwise = fail "Not Unifieable!"
+    unify (TupleT i) (ConT n)
+        | isTuple n i  = return ()
+        | otherwise = fail "Not Unifieable!"
+    unify (ConT n)(TupleT i)
+        | isTuple n i  = return ()
+        | otherwise = fail "Not Unifieable!"
+    -- lists
+--    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 ()        
hunk ./src/Syntax/Unifier.hs 2
-module Syntax.Unifier (
-
-    Replacement,
-    Substitution,
-    Unifieable(mgu, applyMgu, matchesLs),
-    matches, equal, equalLs, subsumes, subsumesLs
+module Syntax.Unifier
+ (
+    U,
+    Substitutable(..),
+    Substitution, Replacement, nullSubst, (<~), insertApply,
+    Unifieable(mgu, unify, match),
+    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, matchVar, flush
hunk ./src/Syntax/Unifier.hs 10
-    )where
+    )
+    where
hunk ./src/Syntax/Unifier.hs 13
-import Language.Haskell.TH (Pat(..), Exp(..))
hunk ./src/Syntax/Unifier.hs 17
-import Syntax.Terms --(subtermOf, Term, isNil, isCons, isTuple, Substitution(:)
-import Syntax.Expressions (unfoldAppE)
-import Syntax.Patterns
+
hunk ./src/Syntax/Unifier.hs 19
+import Data.Maybe (isJust)
hunk ./src/Syntax/Unifier.hs 21
-import Logging
hunk ./src/Syntax/Unifier.hs 23
+import Logging
+import Syntax.Terms
+
hunk ./src/Syntax/Unifier.hs 30
+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)
+
+class Substitutable a where
+    -- applys a substitution to a term. May fail inside LM when an type mismatch
+    -- occurs.
+    apply :: (Substitution a) -> a -> LM a
+  
+  
hunk ./src/Syntax/Unifier.hs 69
-    applyMgu :: (Substitution t) -> t -> LM t    
+    --applyMgu :: (Substitution t) -> t -> LM t    
hunk ./src/Syntax/Unifier.hs 87
-    -- | 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 :: [t] -> [t] -> Bool
+-- | 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 127
+    
+    
hunk ./src/Syntax/Unifier.hs 172
-    
-instance Unifieable Exp where
-    -- | Straight forward walking down Exp-terms, pass the function call to
-    --   subterms and replace variables as specified by the Unifier.
-    --   Well, and of course some necessary lifting. 
-    applyMgu u v@(VarE _)        = case lookup v u of 
-                                     Just val -> return val
-                                     Nothing  -> return v
-    applyMgu u t@(ConE _ )       = return t
-    applyMgu u t@(LitE _)        = return t
-    applyMgu u (ListE ts)        = liftM ListE (mapM (applyMgu u) ts)
-    applyMgu u (TupE ts)         = liftM TupE (mapM (applyMgu u) ts)
-    applyMgu u (AppE a1 a2)      = liftM2 AppE (applyMgu u a1) (applyMgu u a2)
-    applyMgu u (InfixE e1 op e2) = 
-        do subs1 <- T.sequence $ liftM (applyMgu []) e1 -- Monad juggling because of Maybe
-           subs2 <- T.sequence $ liftM (applyMgu []) e2 -- Maybe (m a) ~~> m (Maybe a)
-           return $ InfixE subs1 op subs2
-    applyMgu u (CondE e1 e2 e3)  = 
-        liftM3 CondE (applyMgu u e1) (applyMgu u e1) (applyMgu u e1)
-    applyMgu u t                               =   
-        let msg =  patternNotDef [pretty u, pretty t]
-        in setCurrentLogger "Terms.Unifier.applyMgu" >>
-           logWA msg >> fail (show msg)
-         
-    matchesLs = matches `on` ListE
-    
-    -- matching variables
-    match s@(VarE i1) t@(VarE i2)
-        | i1 == i2                          = return ()
-        | otherwise                         = matchVar s t
-    match s@(VarE _) t                      = matchVar s t
-    match s          t@(VarE _)             = flush "No Match!"
-    -- matching constructors    
-    match s@(ConE _) t@(ConE _) 
-        | (s == t)                          = return () 
-        | otherwise                         = flush "No Match!"  
-    -- matching literals          
-    match s@(LitE _) t@(LitE _) 
-        | (s == t)                          = return () 
-        | otherwise                         = flush "No Match!" 
-    -- matching tuples
-    match (TupE s) (TupE t) 
-        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
-        | otherwise                         = flush "No Match!"
-    match (TupE s) t@(AppE _ _)             = 
-        case unfoldAppE t of
-            ((ConE n):args) ->
-                if isTuple n  (length s)  
-                  then mapM_ (uncurry match) (zip s args)
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable"  
-    match t@(AppE _ _)(TupE s)              =      
-        case unfoldAppE t of
-            ((ConE n):args) ->
-                if isTuple n  (length s) 
-                  then mapM_ (uncurry match) (zip args s)
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable"  
-        
-    match (ListE [])(ListE [])              = return ()
-    match (ListE (s:ss))(ListE (t:ts))      = match s t >> match (ListE ss) (ListE ts)
-    -- as usual, something special for lists, so check whether the AppE is of 
-    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
-    match (ListE [])c@(ConE n)               
-        | isNil n                           = return ()
-        | otherwise                         = flush "No Match!"  
-    match c@(ConE n)(ListE [])              
-        | isNil n                           = return ()
-        | otherwise                         = flush "No Match!"  
-    match (ListE (s:ss)) t@(AppE _ _)       =
-        case unfoldAppE t of
-            ((ConE n):a1:[a2]) ->
-                if isCons n
-                  then match s a1 >> match (ListE ss) a2
-                  else flush "No Match!"  
-            _owise       -> flush "No Match!"  
-    match t@(AppE _ _) (ListE (s:ss))       =
-        case unfoldAppE t of
-            ((ConE n):a1:[a2]) ->
-                if isCons n
-                  then match s a1 >> match (ListE ss) a2
-                  else flush "No Match!"  
-            _owise       -> flush "No Match!"  
-    
-    match (AppE s1 s2)(AppE t1 t2)          = match s1 t1 >> match s2 t2
-    
-    match (InfixE s1 s2 s3)(InfixE t1 t2 t3)
-        | s2 == t2                          = liftMatch s1 t1 >> liftMatch s3 t3
-        | otherwise                         = flush "No Match!"        
-    match (CondE s1 s2 s3) (CondE t1 t2 t3) = 
-        match s1 t1 >> match s2 t2 >> match s3 t3    
-    match s t                               =
-        let msg =  patternNotDef [pretty s, pretty t]
-        in lift (setCurrentLogger "Terms.Unifier.match") >>
-           llogWA msg >> llogDE (hsep (map pretty (unfoldAppE t))) >>
-           fail (show msg)
-         
-    
-    unify s@(VarE _) t@(VarE _)
-        |(s == t)                           = return ()
-        | otherwise                         = unifyVar s t
-    unify s@(VarE _) t                      = unifyVar s t
-    unify s          t@(VarE _)             = unifyVar t s    
-    
-    unify s@(ConE _) t@(ConE _) 
-        | (s == t)                          = return () 
-        | otherwise                         = flush "Not unifieable" 
-        
-    unify s@(LitE _) t@(LitE _) 
-        | (s == t)                          = return () 
-        | otherwise                         = flush "Not unifieable"
-         
-    unify (TupE s) (TupE t) 
-        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
-        | otherwise                         = flush "Not unifieable"
-    unify (TupE s) t@(AppE _ _)             = 
-        case unfoldAppE t of
-            ((ConE n):args) ->
-                if isTuple n  (length s) 
-                  then mapM_ (uncurry unify) (zip s args)
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable"  
-    unify t@(AppE _ _)(TupE s)              = 
-        case unfoldAppE t of
-            ((ConE n):args) ->
-                if isTuple n  (length s) 
-                  then mapM_ (uncurry unify) (zip s args)
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable"
-    unify (ListE [])(ListE [])              = return ()
-    unify (ListE (s:ss))(ListE (t:ts))      = 
-        unify s t >> unify (ListE ss) (ListE ts)
-    -- as usual, something special for lists, so check whether the AppE is of 
-    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
-    unify (ListE [])c@(ConE n)             
-        | c == (ConE '[])                   = return ()
-        | otherwise                         = flush "Not unifieable!"  
-    unify c@(ConE n)(ListE [])              
-        | c == (ConE '[])                   = return ()
-        | otherwise                         = flush "Not unifieable!"  
-    unify (ListE (s:ss)) t@(AppE _ _)       = 
-        case unfoldAppE t of
-            (op:a1:[a2]) ->
-                if op == (ConE '(:))
-                  then unify s a1 >> unify (ListE ss) a2
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable" 
-    unify t@(AppE _ _) (ListE (s:ss))       =
-        case unfoldAppE t of
-            (op:a1:[a2]) ->
-                if op == (ConE '(:))
-                  then unify s a1 >> unify (ListE ss) a2
-                  else flush "Not unifieable" 
-            _owise       -> flush "Not unifieable" 
-    
-    unify (AppE s1 s2)(AppE t1 t2)          = unify s1 t1 >> unify s2 t2
-    
-    unify (InfixE s1 s2 s3)(InfixE t1 t2 t3)
-        | s2 == t2                          = liftUnify s1 t1 >> liftUnify s3 t3
-        | otherwise                         = flush "Not unifieable" 
-        
-    unify (CondE s1 s2 s3) (CondE t1 t2 t3) = 
-        unify s1 t1 >> unify s2 t2 >> unify s3 t3
-    
-    unify s t                               =   
-        let msg =  patternNotDef [pretty s, pretty t]
-        in lift (setCurrentLogger "Terms.Unifier.unify") >>
-           llogWA msg >> llogDE (hsep (map pretty (unfoldAppE t))) >>
-           fail ( show msg)
hunk ./src/Syntax/Unifier.hs 173
--- | Helper for unifying (InfixE Maybe Exp) Exp (Maybe Exp))
-liftUnify :: Maybe Exp -> Maybe Exp -> U Exp
-liftUnify = (\u v -> maybe (return ()) (\(s,t) -> unify s t) (liftM2 (,) u v))
-
--- | Helper for matching (InfixE Maybe Exp) Exp (Maybe Exp))
-liftMatch :: Maybe Exp -> Maybe Exp -> U Exp
-liftMatch = (\u v -> maybe (return ()) (\(s,t) -> match s t) (liftM2 (,) u v))     
-   
-instance Unifieable Pat where
-
-    applyMgu u v@(VarP _)        = case lookup v u of 
-                                     Just val -> return val
-                                     Nothing  -> return v
-    applyMgu u (ConP n ps)       = liftM (ConP n) (mapM (applyMgu u) ps )
-    applyMgu u t@(LitP _)        = return t
-    applyMgu u (ListP ts)        = liftM ListP (mapM (applyMgu u) ts)
-    applyMgu u (TupP ts)         = liftM TupP (mapM (applyMgu u) ts)
-    applyMgu u (InfixP e1 op e2) =
-        liftM3 InfixP (applyMgu u e1) (return op) (applyMgu u e2)
-    applyMgu u t                 =   
-        let msg =  patternNotDef [ pretty u, pretty t]
-        in  setCurrentLogger "Terms.Unifier.applyMgu" >>
-            logWA msg >> fail ( show msg) 
-    
-    matchesLs = matches `on` ListP
-    
-    match s@(VarP _) t@(VarP _ )           
-        | s == t                          = return ()
-        | otherwise                       = matchVar s t
-    match s@(VarP _) t                    = matchVar s t
-    match s          t@(VarP _)           = matchVar t s          
-    match s@(LitP _) t@(LitP _) 
-        | (s == t)                        = return () 
-        | otherwise                       = flush  "No Match!"         
-    match (ListP [])(ListP [])            = return ()
-    match (ListP (s:ss))(ListP (t:ts))    = match s t >> match (ListP ss) (ListP ts) 
-    -- as usual, something special for lists, so check whether the ConP is of 
-    -- the form (ConP GHC.Base.: [elem, restlist])
-    match (ListP [])(ConP n [])
-        | isNil n                       = return ()
-        | otherwise                       = flush  "No Match!"  
-    match(ConP n []) (ListP [])
-        | isNil n                         = return ()
-        | otherwise                       = flush  "No Match!"  
-    match (ListP (s:ss))(ConP n ([p,ps]))
-        | isCons n                        = match s p >> match (ListP ss) ps
-        | otherwise                       = flush  "No Match!"  
-    match(ConP n ([p,ps])) (ListP (s:ss))
-        | isCons n                        = match s p >> match (ListP ss) ps
-        | otherwise                       = flush  "No Match!"  
-    match s@(ListP _) t@(ConP _ _)        = match t s    
-    match s@(ConP n1 p1) t@(ConP n2 p2) 
-        | n1 == n2                        = mapM_ (uncurry match) (zip p1 p2)
-        | otherwise                       = flush  "No Match!"          
-    match (TupP s) (TupP t) 
-        | (length s) == (length t)        = mapM_ (uncurry match) (zip s t)
-        | otherwise                       = flush  "No Match!"       
-    match (ConP n p) (TupP t)              
-        | isTuple n (length t)            = mapM_ (uncurry match) (zip p t)
-        | otherwise                       = flush "No Match!"      
-    match (TupP t)(ConP n p)               
-        | isTuple n (length t)            = mapM_ (uncurry match) (zip p t)
-        | otherwise                       = flush "No Match!"      
-    match (InfixP s1 s2 s3)(InfixP t1 t2 t3)
-        | s2 == t2                        = match s1 t1 >> match s3 t3
-        | otherwise = flush  "No Match!"          
-    match s t                             =    
-        flush  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))
-        
-    
-    unify s@(VarP _) t@(VarP _ )        
-        | s == t                       = return ()
-        | otherwise                    = unifyVar s t
-    unify s@(VarP _) t                 = unifyVar s t
-    unify s          t@(VarP _)        = unifyVar t s         
-    unify s@(LitP _) t@(LitP _) 
-        | (s == t)                     = return () 
-        | otherwise                    = flush  "Not unifieable"         
-    unify (ListP [])(ListP [])         = return ()
-    unify (ListP (s:ss))(ListP (t:ts)) = unify s t >> unify (ListP ss) (ListP ts) 
-    -- as usual, something special for lists, so check whether the ConP is of 
-    -- the form (ConP GHC.Base.: [elem, restlist])
-    unify (ListP [])(ConP n [])        
-        | isNil n                      = return ()
-        | otherwise                    = flush "Not unifieable"
-    unify(ConP n []) (ListP [])
-        | isNil n                       = return ()
-        | otherwise                    = flush  "Not unifieable"
-    unify (ListP (s:ss))(ConP n ([p,ps]))
-        | isCons n                     = unify s p >> unify (ListP ss) ps
-        | otherwise                    = flush "Not unifieable"
-    unify(ConP n ([p,ps])) (ListP (s:ss))
-        | isCons n                    = unify s p >> unify (ListP ss) ps
-        | otherwise                    = flush "Not unifieable"    
-    unify s@(ConP n1 p1) t@(ConP n2 p2) 
-        | n1 == n2                     = mapM_ (uncurry unify) (zip p1 p2)
-        | otherwise                    = flush  "Not unifieable"        
-    unify (TupP s) (TupP t) 
-        | (length s) == (length t)     = mapM_ (uncurry unify) (zip s t)
-        | otherwise                    = flush  "Not unifieable"       
-    unify (ConP n p) (TupP t) 
-        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
-        | otherwise                    = flush  "Not unifieable"       
-    unify (TupP t)(ConP n p) 
-        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
-        | otherwise                    = flush  "Not unifieable" 
-    unify (InfixP s1 s2 s3)(InfixP t1 t2 t3)
-        | s2 == t2                     = unify s1 t1 >> unify s3 t3
-        | otherwise = flush  "Not unifieable"        
-    unify s t                          = 
-        flush  ("Term " ++ (show s) ++ "not unifieable with " ++ (show t))
hunk ./src/Syntax/Unifier.hs 176
+
+
+      
hunk ./src/Terms.hs 20
-import Syntax.Unifier (Replacement, Substitution, Unifieable(..))
+import Syntax.Unifier --(Replacement, Substitution, Unifieable(..))
hunk ./src/UI/Context.hs 2
-module UI.Context where
+module UI.Context (
+    C, getVarType, getConType, getSubClasses, getInstances,
+    Context(..), emptyCtx, defaultContext,
+    parseContext, buildCtx, 
+
+    )where
hunk ./src/UI/Context.hs 9
-import Language.Haskell.Meta.Parse
-import qualified Language.Haskell.Meta.Syntax.Translate as T
hunk ./src/UI/Context.hs 10
-import Language.Haskell.Exts.Parser hiding (parseModule)
-import qualified Language.Haskell.Exts.Syntax as Hs
hunk ./src/UI/Context.hs 12
-import Data.List (partition, union)
+import Data.List (partition, union,foldl', nub)
hunk ./src/UI/Context.hs 16
-import Syntax.Terms
-import Syntax.Expressions
-import Syntax.Patterns
+import Logging.Logger
+
+--import Syntax.TempRules
hunk ./src/UI/Context.hs 20
-import Logging hiding (trace)
+import Syntax.Patterns
+import Syntax.Expressions
+--import Syntax.Unifier
+import Syntax.Terms
+
+import Language.Haskell.Meta.Parse
+--import qualified Language.Haskell.Meta.Syntax.Translate as T
hunk ./src/UI/Context.hs 28
+import qualified Data.Typeable as T
+import Data.Generics 
+import Language.Haskell.TH.Syntax
+import Language.Haskell.Exts.Parser hiding (parseModule)
+import qualified Language.Haskell.Exts.Syntax as Hs
hunk ./src/UI/Context.hs 34
+
+type Rule = ([TPat],TExp)
+type Rules = [Rule]
hunk ./src/UI/Context.hs 59
-    let pSynTy = map (\(TySynD n args t) ->  ((mkAppT n args), fixType t) ) $ T.toDec d
+    let pSynTy = map (\(TySynD n args t) ->  ((mkAppT n args), fixType t) ) $ toDec d
hunk ./src/UI/Context.hs 65
-        ctorty = \ty -> (mkForallT assts (T.toType $ mkHsTyFun (ty ++ [dataty])))
+        ctorty = \ty -> (mkForallT assts (toType $ mkHsTyFun (ty ++ [dataty])))
hunk ./src/UI/Context.hs 68
-            (Hs.QualConDecl _ _ _ (Hs.ConDecl n tys)) ->  return ( T.toName n, ctorty $ map unBang tys);
+            (Hs.QualConDecl _ _ _ (Hs.ConDecl n tys)) ->  return ( toName n, ctorty $ map unBang tys);
hunk ./src/UI/Context.hs 73
-    let pTysClass = map (\(n,_) ->  ((mkForallT assts (T.toType dataty)), (T.toName n))) derive
+    let pTysClass = map (\(n,_) ->  ((mkForallT assts (toType dataty)), (toName n))) derive
hunk ./src/UI/Context.hs 85
-    let sigds        = concatMap T.toDec $ filter isTypeDecl $ clsdecls
+    let sigds        = concatMap toDec $ filter isTypeDecl $ clsdecls
hunk ./src/UI/Context.hs 93
-        pClssFuns     = [(T.toName cname,[ n | (SigD n _) <- sigds])]
+        pClssFuns     = [(toName cname,[ n | (SigD n _) <- sigds])]
hunk ./src/UI/Context.hs 95
-        pClssSupr   = [(T.toName cname,[ T.toName n | (Hs.ClassA n _vars) <- assts])]
+        pClssSupr   = [(toName cname,[ toName n | (Hs.ClassA n _vars) <- assts])]
hunk ./src/UI/Context.hs 102
-    let ty = mkForallT assts (T.toType t)
+    let ty = mkForallT assts (toType t)
hunk ./src/UI/Context.hs 104
-        n = T.toName qname
+        n = toName qname
hunk ./src/UI/Context.hs 109
-    let pNmsTys  = map (\(SigD n t) -> (n, t)) $ T.toDec d  
+    let pNmsTys  = map (\(SigD n t) -> (n, t)) $ toDec d  
hunk ./src/UI/Context.hs 113
-    let [(FunD n cls)] = T.toDec d
-    case clauses2rules ctx n cls of
+    let [(FunD n cls)] = toDec d
+    case (clauses2rules ctx n cls) of
hunk ./src/UI/Context.hs 183
---toDec (Hs.TypeSig _ ns t) =  [SigD (T.toName n) (T.toType t) | n <- ns]
---toDec decs                = [T.toDec decs] 
+--toDec (Hs.TypeSig _ ns t) =  [SigD (toName n) (toType t) | n <- ns]
+--toDec decs                = [toDec decs] 
hunk ./src/UI/Context.hs 207
-    fixType $ ForallT (concatMap getVName assts) (map T.toType assts) ty
+    fixType $ ForallT (concatMap getVName assts) (map toType assts) ty
hunk ./src/UI/Context.hs 209
-    getVName (Hs.ClassA _ tys) = map (\(Hs.TyVar n) -> T.toName n) tys             
-
--------------------------------------------------------------------------------
--- Using Context
---------------------------------------------------------------------------------
-
-type C a = StateT Context (Either String) a
+    getVName (Hs.ClassA _ tys) = map (\(Hs.TyVar n) -> toName n) tys             
hunk ./src/UI/Context.hs 211
-getVarType :: Name -> C Type
-getVarType n = do
-    m <- gets ctx_types
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Variable not in context: " ++ (show n) 
hunk ./src/UI/Context.hs 212
-getConType :: Name -> C Type
-getConType n = do
-    m <- gets ctx_ctors 
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Ctor not in context: " ++ (show n)
-        
-getSubClasses :: Name -> C [Name]        
-getSubClasses n = do
-    m <- gets ctx_classes
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Class not in context: " ++ (show n)
-        
-getInstances :: Type -> C [Name]        
-getInstances n = do
-    m <- gets ctx_instances
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Type not in context: " ++ (show n)
+-- | specialising Type 't2' using Type 't1', where 't2' contains type variables
+--   which are to instantiate using 't1'. E.g.
+--   @specialise '[Int]' '(b,a) -> (a,String) -> [a]' is '(b,Int) -> (Int,String) -> [Int]@ 
+--   so 't1' is always more general the 't2'
+specialise :: Type -> Type -> StateT Context (Either String) Type
+specialise t1 t2 = do --return t1
+    subst <- instantiate (last . unArrowT $ t2) t1
+    return $ applySubs t2 subst
hunk ./src/UI/Context.hs 221
+applySubs :: Type -> [(Type,Type)] -> Type
+applySubs t@(VarT n) s = 
+    case lookup t s of
+       (Just t') -> t'
+       _owise    -> t
+applySubs t@(ForallT _ _ (VarT n)) s =  
+    case lookup (VarT n) s  of
+       (Just t') -> t'
+       _owise    -> t
+applySubs (ForallT ns ctx t) s = (ForallT ns ctx (applySubs t s))
+applySubs (AppT t1 t2) s =
+    AppT (applySubs t1 s) (applySubs t2 s)
+applySubs t _     =  t
+       
+instantiate :: Type -> Type -> StateT Context (Either String) [(Type,Type)]
+instantiate v@(VarT n) t  = return [(v,t)]
+instantiate (ForallT ns ctx t1) t2 = instantiate t1 t2    
+instantiate t1@(AppT a11 a12) t2@(AppT a21 a22) =
+    liftM2 union (instantiate a11 a21) (instantiate a12 a22)
+    --liftM concat $ mapM (uncurry instantiate) $ zip (unfoldAppT t1) (unfoldAppT t2)
+instantiate (ConT n1) (ConT n2) 
+    | n1 == n2            = return []
+    | otherwise           = fail "types do not unify1"
+instantiate (TupleT i1) (TupleT i2) 
+    | i1 == i2            = return []
+    | otherwise           = fail "types do not unify2"
+instantiate (TupleT i) (ConT n) 
+    | isTuple n i         = return []
+    | otherwise           = fail "types do not unify3"
+instantiate (ConT n)(TupleT i)  
+    | isTuple n i         = return []
+    | otherwise           = fail "types do not unify4"
+instantiate ArrowT ArrowT = return []
+instantiate ListT ListT   = return []
+instantiate ListT (ConT n)
+    | isNil n             = return []
+    | otherwise           = fail "types do not unify5"
+instantiate (ConT n) ListT 
+    | isNil n             = return []
+    | otherwise           = fail "types do not unify6"
+instantiate a b           = fail $ "types do not unify" ++ (show (a,b))
hunk ./src/UI/Context.hs 263
+ 
hunk ./src/UI/Context.hs 341
--- | specialising Type 't2' using Type 't1', where 't2' contains type variables
---   which are to instantiate using 't1'. E.g.
---   @specialise '[Int]' '(b,a) -> (a,String) -> [a]' is '(b,Int) -> (Int,String) -> [Int]@ 
---   so 't1' is always more general the 't2'
-specialise t1 t2 = do --return t1
-    subst <- instantiate (last . unArrowT $ t2) t1
-    return $ applySubs t2 subst
-
-applySubs :: Type -> ( Substitution Type) -> Type
-applySubs t@(VarT n) s = 
-    case lookup t s of
-       (Just t') -> t'
-       _owise    -> t
-applySubs t@(ForallT _ _ (VarT n)) s =  
-    case lookup (VarT n) s  of
-       (Just t') -> t'
-       _owise    -> t
-applySubs (ForallT ns ctx t) s = (ForallT ns ctx (applySubs t s))
-applySubs (AppT t1 t2) s =
-    AppT (applySubs t1 s) (applySubs t2 s)
-applySubs t _     =  t
-       
-instantiate :: Type -> Type -> C (Substitution Type)
-instantiate v@(VarT n) t  = return [v <~ t]
-instantiate (ForallT ns ctx t1) t2 = instantiate t1 t2    
-instantiate t1@(AppT a11 a12) t2@(AppT a21 a22) =
-    liftM2 union (instantiate a11 a21) (instantiate a12 a22)
-    --liftM concat $ mapM (uncurry instantiate) $ zip (unfoldAppT t1) (unfoldAppT t2)
-instantiate (ConT n1) (ConT n2) 
-    | n1 == n2            = return nullSubst
-    | otherwise           = fail "types do not unify1"
-instantiate (TupleT i1) (TupleT i2) 
-    | i1 == i2            = return nullSubst
-    | otherwise           = fail "types do not unify2"
-instantiate (TupleT i) (ConT n) 
-    | isTuple n i         = return nullSubst
-    | otherwise           = fail "types do not unify3"
-instantiate (ConT n)(TupleT i)  
-    | isTuple n i         = return nullSubst
-    | otherwise           = fail "types do not unify4"
-instantiate ArrowT ArrowT = return nullSubst
-instantiate ListT ListT   = return nullSubst
-instantiate ListT (ConT n)
-    | isNil n             = return nullSubst
-    | otherwise           = fail "types do not unify5"
-instantiate (ConT n) ListT 
-    | isNil n             = return nullSubst
-    | otherwise           = fail "types do not unify6"
-instantiate a b           = fail $ "types do not unify" ++ (show (a,b))
-
- 
hunk ./src/UI/Context.hs 350
-foldTAppE :: TExp -> [TExp] -> TExp
-foldTAppE e [] = e 
-foldTAppE et (e:es) = foldTAppE (TAppE et e (reduceArrowT . typeOf $ et)) es
hunk ./src/UI/Context.hs 352
-type Rule = ([TPat],TExp)
-type Rules = [Rule]
hunk ./src/UI/Context.hs 365
-        return (ls', rs')
+        return (ls', rs')    
+        
+
+-----------------------------------------------------------------------------
+
+
+class ToName a where toName :: a -> Name
+class ToLit  a where toLit  :: a -> Lit
+class ToType a where toType :: a -> Type
+class ToPat  a where toPat  :: a -> Pat
+class ToExp  a where toExp  :: a -> Exp
+class ToDec  a where toDec  :: a -> [Dec]
+class ToStmt a where toStmt :: a -> Stmt
+class ToLoc  a where toLoc  :: a -> Loc
+
+
+errorMsg :: (Typeable a) => String -> a -> String
+errorMsg fun a = concat
+  [ fun,": "
+  , show . typeRepTyCon . T.typeOf $ a
+  , " not (yet?) implemented"
+  ]
+
+
+-- stolen from Language.Haskell.Meta.Syntax.Translate from package haskell.src.meta
+-----------------------------------------------------------------------------
+
+
+instance ToExp Lit where
+  toExp = LitE
+instance (ToExp a) => ToExp [a] where
+  toExp = ListE . fmap toExp
+instance (ToExp a, ToExp b) => ToExp (a,b) where
+  toExp (a,b) = TupE [toExp a, toExp b]
+instance (ToExp a, ToExp b, ToExp c) => ToExp (a,b,c) where
+  toExp (a,b,c) = TupE [toExp a, toExp b, toExp c]
+instance (ToExp a, ToExp b, ToExp c, ToExp d) => ToExp (a,b,c,d) where
+  toExp (a,b,c,d) = TupE [toExp a, toExp b, toExp c, toExp d]
+
+
+instance ToPat Lit where
+  toPat = LitP
+instance (ToPat a) => ToPat [a] where
+  toPat = ListP . fmap toPat
+instance (ToPat a, ToPat b) => ToPat (a,b) where
+  toPat (a,b) = TupP [toPat a, toPat b]
+instance (ToPat a, ToPat b, ToPat c) => ToPat (a,b,c) where
+  toPat (a,b,c) = TupP [toPat a, toPat b, toPat c]
+instance (ToPat a, ToPat b, ToPat c, ToPat d) => ToPat (a,b,c,d) where
+  toPat (a,b,c,d) = TupP [toPat a, toPat b, toPat c, toPat d]
+
+
+instance ToLit Char where
+  toLit = CharL
+instance ToLit String where
+  toLit = StringL
+instance ToLit Integer where
+  toLit = IntegerL
+instance ToLit Int where
+  toLit = IntegerL . toInteger
+instance ToLit Float where
+  toLit = RationalL . toRational
+instance ToLit Double where
+  toLit = RationalL . toRational
+
+
+-----------------------------------------------------------------------------
+
+
+-- * ToName {String,HsName,Module,HsSpecialCon,HsQName}
+
+
+instance ToName String where
+  toName = mkName
+
+instance ToName Hs.Name where
+  toName (Hs.Ident s) = toName s
+  toName (Hs.Symbol s) = toName s
+
+instance ToName Hs.Module where
+  toName (Hs.Module _ (Hs.ModuleName s) _ _ _ _ _) = toName s
+
+
+instance ToName Hs.SpecialCon where
+  toName Hs.UnitCon = '()
+  toName Hs.ListCon = '[]
+  toName Hs.FunCon  = ''(->)
+  toName (Hs.TupleCon n)
+    | n<2 = '()
+    | otherwise =
+      let x = maybe [] (++".") (nameModule '())
+      in toName . concat $ x : ["(",replicate (n-1) ',',")"]
+  toName Hs.Cons    = '(:)
+
+
+instance ToName Hs.QName where
+--  toName (Hs.Qual (Hs.Module []) n) = toName n
+  toName (Hs.Qual (Hs.ModuleName []) n) = toName n
+  toName (Hs.Qual (Hs.ModuleName m) n) =
+    let m' = show . toName $ m
+        n' = show . toName $ n
+    in toName . concat $ [m',".",n']
+  toName (Hs.UnQual n) = toName n
+  toName (Hs.Special s) = toName s
+
+
+
+-----------------------------------------------------------------------------
+
+-- * ToLit HsLiteral
+
+
+instance ToLit Hs.Literal where
+  toLit (Hs.Char a) = CharL a
+  toLit (Hs.String a) = StringL a
+  toLit (Hs.Int a) = IntegerL a
+  toLit (Hs.Frac a) = RationalL a
+  toLit (Hs.PrimChar a) = CharL a      -- XXX
+  toLit (Hs.PrimString a) = StringL a  -- XXX
+  toLit (Hs.PrimInt a) = IntPrimL a
+  toLit (Hs.PrimFloat a) = FloatPrimL a
+  toLit (Hs.PrimDouble a) = DoublePrimL a
+
+
+-----------------------------------------------------------------------------
+
+-- * ToPat HsPat
+
+
+instance ToPat Hs.Pat where
+  toPat (Hs.PVar n)
+    = VarP (toName n)
+  toPat (Hs.PLit l)
+    = LitP (toLit l)
+{-
+ghci> parseHsPat "-2"
+Right (HsPParen (HsPNeg (HsPLit (HsInt 2))))
+-}
+  toPat (Hs.PNeg p) = error "toPat: HsPNeg not supported"
+  toPat (Hs.PInfixApp p n q)= InfixP (toPat p) (toName n) (toPat q)
+  toPat (Hs.PApp n ps) = ConP (toName n) (fmap toPat ps)
+  toPat (Hs.PTuple ps) = TupP (fmap toPat ps)
+  toPat (Hs.PList ps) = ListP (fmap toPat ps)
+  toPat (Hs.PParen p) = toPat p
+  toPat (Hs.PRec n pfs) = let toFieldPat (Hs.PFieldPat n p) = (toName n, toPat p)
+                          in RecP (toName n) (fmap toFieldPat pfs)
+  toPat (Hs.PAsPat n p) = AsP (toName n) (toPat p)
+  toPat (Hs.PWildCard) = WildP
+  toPat (Hs.PIrrPat p) = TildeP (toPat p)
+  toPat (Hs.PatTypeSig _ p t) = SigP (toPat p) (toType t)
+  toPat (Hs.PRPat rps) = error "toPat: HsRPat not supported"
+  toPat (Hs.PXTag _ _ _ pM p) = error "toPat: HsPXTag not supported"
+  toPat (Hs.PXETag _ _ _ pM) = error "toPat: HsPXETag not supported"
+  toPat (Hs.PXPcdata _) = error "toPat: HsPXPcdata not supported"
+  toPat (Hs.PXPatTag p) = error "toPat: HsPXPatTag not supported"
+
+-----------------------------------------------------------------------------
+
+-- * ToExp HsExp
+
+instance ToExp Hs.QOp where
+  toExp (Hs.QVarOp n) = VarE (toName n)
+  toExp (Hs.QConOp n) = ConE (toName n)
+
+toFieldExp :: Hs.FieldUpdate -> FieldExp
+toFieldExp (Hs.FieldUpdate n e) = (toName n, toExp e)
+
+
+
+instance ToExp Hs.Exp where
+{-
+data HsExp
+  = HsVar HsQName
+-}
+--  | HsIPVar HsIPName
+{-
+  | HsLet HsBinds HsExp
+  | HsDLet [HsIPBind] HsExp
+  | HsWith HsExp [HsIPBind]
+  | HsCase HsExp [HsAlt]
+  | HsDo [HsStmt]
+  -- use mfix somehow
+  | HsMDo [HsStmt]
+-}
+  toExp (Hs.Var n)                 = VarE (toName n)
+  toExp (Hs.Con n)                 = ConE (toName n)
+  toExp (Hs.Lit l)                 = LitE (toLit l)
+  
+{-
+Hs.InfixApp is left assocative
+(InfixApp (InfixApp (InfixApp (Lit (Int 1)) (QConOp (Special Cons)) (Lit (Int 2))) (QConOp (Special Cons)) (Lit (Int 3))) (QConOp (Special Cons)) (List []))
+
+TH.InfixE is right associativ
+InfixE (Just (LitE (IntegerL 1))) (ConE GHC.Types.:) (Just (InfixE (Just (LitE (IntegerL 2))) (ConE GHC.Types.:) (Just (InfixE (Just (LitE (IntegerL 3))) (ConE GHC.Types.:) (Just (ConE GHC.Types.[]))))))
+
+-}  
+  toExp (Hs.InfixApp e o f)        = toRightAssoc (mkInfix o (toExp f)) e
+    where
+    toRightAssoc done (Hs.InfixApp e o f) = toRightAssoc (mkInfix o (done . toExp $ f) ) e
+    toRightAssoc done e = done (toExp e)
+    mkInfix = (\o r l  -> InfixE (Just l) (toExp o) (Just r))
+  --InfixE (Just . toExp $ e) (toExp o) (Just . toExp $ f)
+  toExp (Hs.LeftSection e o)       = InfixE (Just . toExp $ e) (toExp o) Nothing
+  toExp (Hs.RightSection o f)      = InfixE Nothing (toExp o) (Just . toExp $ f)
+  toExp (Hs.App e f)               = AppE (toExp e) (toExp f)
+  toExp (Hs.NegApp e)              = AppE (VarE 'negate) (toExp e)
+  toExp (Hs.Lambda _ ps e)         = LamE (fmap toPat ps) (toExp e)
+  toExp (Hs.Let bs e)              = LetE (hsBindsToDecs bs) (toExp e)
+  -- toExp (HsWith e bs
+  toExp (Hs.If a b c)              = CondE (toExp a) (toExp b) (toExp c)
+  -- toExp (HsCase e xs)
+  -- toExp (HsDo ss)
+  -- toExp (HsMDo ss)
+  toExp (Hs.Tuple xs)              = TupE (fmap toExp xs)
+  toExp (Hs.List xs)               = ListE (fmap toExp xs)
+  toExp (Hs.Paren e)               = toExp e
+  toExp (Hs.RecConstr n xs)        = RecConE (toName n) (fmap toFieldExp xs)
+  toExp (Hs.RecUpdate e xs)        = RecUpdE (toExp e) (fmap toFieldExp xs)
+  toExp (Hs.EnumFrom e)            = ArithSeqE $ FromR (toExp e)
+  toExp (Hs.EnumFromTo e f)        = ArithSeqE $ FromToR (toExp e) (toExp f)
+  toExp (Hs.EnumFromThen e f)      = ArithSeqE $ FromThenR (toExp e) (toExp f)
+  toExp (Hs.EnumFromThenTo e f g)  = ArithSeqE $ FromThenToR (toExp e) (toExp f) (toExp g)
+  toExp (Hs.ExpTypeSig _ e t)      = SigE (toExp e) (toType t)
+  --  HsListComp HsExp [HsStmt]
+  -- toExp (HsListComp e ss) = CompE 
+  -- NEED: a way to go e -> Stmt
+  toExp a@(Hs.ListComp e ss)       = error $ errorMsg "toExp" a
+{- HsVarQuote HsQName
+  | HsTypQuote HsQName
+  | HsBracketExp HsBracket
+  | HsSpliceExp HsSplice
+data HsBracket
+  = HsExpBracket HsExp
+  | HsPatBracket HsPat
+  | HsTypeBracket HsType
+  | HsDeclBracket [HsDecl]
+data HsSplice = HsIdSplice String | HsParenSplice HsExp -}
+  toExp (Hs.SpliceExp spl) = toExp spl
+  toExp e = error $ errorMsg "toExp" e
+
+
+instance ToExp Hs.Splice where
+  toExp (Hs.IdSplice s) = VarE (toName s)
+  toExp (Hs.ParenSplice e) = toExp e
+
+
+-----------------------------------------------------------------------------
+
+{-
+class ToName a where toName :: a -> Name
+class ToLit  a where toLit  :: a -> Lit
+class ToType a where toType :: a -> Type
+class ToPat  a where toPat  :: a -> Pat
+class ToExp  a where toExp  :: a -> Exp
+class ToDec  a where toDec  :: a -> Dec
+class ToStmt a where toStmt :: a -> Stmt
+class ToLoc  a where toLoc  :: a -> Loc
+-}
+
+{-
+TODO:
+  []
+
+PARTIAL:
+  * ToExp HsExp
+  * ToStmt HsStmt
+  * ToDec HsDecl
+
+DONE:
+  * ToLit HsLiteral
+  * ToName {..}
+  * ToPat HsPat
+  * ToLoc SrcLoc
+  * ToType HsType
+
+-}
+-----------------------------------------------------------------------------
+
+-- * ToLoc SrcLoc
+
+instance ToLoc Hs.SrcLoc where
+  toLoc (Hs.SrcLoc fn l c) =
+    Loc fn [] [] (l,c) (-1,-1)
+
+-----------------------------------------------------------------------------
+
+-- * ToType HsType
+
+instance ToName Hs.TyVarBind where
+  toName (Hs.KindedVar n _) = toName n
+  toName (Hs.UnkindedVar n) = toName n
+
+{- |
+TH does't handle
+  * unboxed tuples
+  * implicit params
+  * infix type constructors
+  * kind signatures
+-}
+instance ToType Hs.Type where
+  toType (Hs.TyForall tvbM cxt t) = fixType $ ForallT (maybe [] (fmap toName) tvbM) (fmap toType cxt) (toType t)
+  toType (Hs.TyFun a b) = toType a .->. toType b
+  toType (Hs.TyTuple _ ts) = foldAppT (TupleT . length $ ts) (fmap toType ts)
+  toType (Hs.TyApp a b) = fixType $ AppT (toType a) (toType b)
+  toType (Hs.TyVar n) = VarT (toName n)
+  toType (Hs.TyCon qn) = ConT (toName qn)
+  toType a@(Hs.TyPred _) = error $ errorMsg "toType" a
+
+  -- XXX: need to wrap the name in parens!
+  toType (Hs.TyInfix a qn b) = foldAppT (ConT . toName $ qn) (fmap toType [a,b])
+  toType (Hs.TyKind t _) = toType t
+
+(.->.) :: Type -> Type -> Type
+a .->. b = AppT (AppT ArrowT a) b
+
+{- |
+TH doesn't handle:
+  * implicit params
+  * equality constraints
+-}
+instance ToType Hs.Asst where
+  toType (Hs.ClassA n ts) = foldAppT (ConT . toName $ n) (fmap toType ts)
+  toType a@(Hs.IParam _ _) = error $ errorMsg "toType" a
+  toType a@(Hs.EqualP _ _) = error $ errorMsg "toType" a
+
+foldAppT :: Type -> [Type] -> Type
+foldAppT t ts = foldl' AppT t ts
+
+-----------------------------------------------------------------------------
+
+-- * ToStmt HsStmt
+
+instance ToStmt Hs.Stmt where
+  toStmt (Hs.Generator _ p e)  = BindS (toPat p) (toExp e)
+  toStmt (Hs.Qualifier e)      = NoBindS (toExp e)
+  toStmt a@(Hs.LetStmt bnds)   = LetS (hsBindsToDecs bnds)
+
+
+-----------------------------------------------------------------------------
+
+-- * ToDec HsDecl
+
+-- data HsBinds = HsBDecls [HsDecl] | HsIPBinds [HsIPBind]
+hsBindsToDecs :: Hs.Binds -> [Dec]
+hsBindsToDecs (Hs.BDecls ds) = concatMap toDec ds
+hsBindsToDecs a@(Hs.IPBinds ipbs) = error $ errorMsg "hsBindsToDecs" a
+-- data HsIPBind = HsIPBind SrcLoc HsIPName HsExp
+
+
+hsBangTypeToStrictType :: Hs.BangType -> (Strict, Type)
+hsBangTypeToStrictType (Hs.BangedTy t)   = (IsStrict, toType t)
+hsBangTypeToStrictType (Hs.UnBangedTy t) = (NotStrict, toType t)
+
+
+{-
+data HsTyVarBind = HsKindedVar HsName HsKind | HsUnkindedVar HsName
+data HsConDecl
+  = HsConDecl HsName [HsBangType]
+  | HsRecDecl HsName [([HsName], HsBangType)]
+-}
+{-
+hsQualConDeclToCon :: HsQualConDecl -> Con
+hsQualConDeclToCon (HsQualConDecl _ tvbs cxt condec) =
+  case condec of
+    HsConDecl n bangs ->
+    HsRecDecl n assocs ->
+-}
+
+instance ToDec Hs.Decl where
+  toDec (Hs.TypeDecl _ n ns t) = [TySynD (toName n) (fmap toName ns) (toType t)]
+  toDec a@(Hs.DataDecl  _ dOrN cxt n ns qcds qns) = error $ errorMsg "toDec" a
+{-
+data HsQualConDecl
+    = HsQualConDecl SrcLoc 
+        [HsTyVarBind] HsContext
+         HsConDecl
+-}
+{-
+    case dOrN of
+      DataType -> DataD
+                    (fmap toType cxt)
+                    (toName n)
+                    (fmap toName ns)
+      NewType  ->
+-}
+  toDec a@(Hs.GDataDecl _ dOrN cxt n ns kM gadtDecs _) = error $ errorMsg "toDec" a
+  toDec a@(Hs.TypeFamDecl _ n ns kM)                   = error $ errorMsg "toDec" a
+  toDec a@(Hs.DataFamDecl _ cxt n ns kM)               = error $ errorMsg "toDec" a
+  toDec a@(Hs.TypeInsDecl _ ta tb)                     = error $ errorMsg "toDec" a
+  toDec a@(Hs.DataInsDecl _ dOrN t qcds qns)           = error $ errorMsg "toDec" a
+  toDec a@(Hs.GDataInsDecl _ dOrN t kM gadtDecs _)     = error $ errorMsg "toDec" a
+-- data HsOp = HsVarOp HsName | HsConOp HsName
+  toDec a@(Hs.InfixDecl _ asst i ops)                  = error $ errorMsg "toDec" a
+  toDec a@(Hs.ClassDecl _ cxt n ns funDeps cDecs)      = error $ errorMsg "toDec" a
+  toDec a@(Hs.InstDecl _ cxt qn ts instDecs)           = error $ errorMsg "toDec" a
+  toDec a@(Hs.DerivDecl _ cxt qn ts)                   = error $ errorMsg "toDec" a  
+  toDec a@(Hs.DefaultDecl _ ts)                        = error $ errorMsg "toDec" a
+  toDec a@(Hs.SpliceDecl _ s)                          = error $ errorMsg "toDec" a
+  toDec a@(Hs.TypeSig _ ns t)                          = [SigD (toName n) (toType t) | n <- ns]
+{- data HsDecl = ... | HsFunBind [HsMatch] | ...
+data HsMatch = HsMatch SrcLoc HsName [HsPat] HsRhs HsBinds
+data Dec = FunD Name [Clause] | ...
+data Clause = Clause [Pat] Body [Dec] -}
+  toDec a@(Hs.FunBind mtchs)                           = [hsMatchesToFunD mtchs]
+{- ghci> parseExp "let x = 2 in x"
+LetE [ValD (VarP x) (NormalB (LitE (IntegerL 2))) []] (VarE x)
+ghci> unQ[| let x = 2 in x |]
+LetE [ValD (VarP x_0) (NormalB (LitE (IntegerL 2))) []] (VarE x_0) -}
+  toDec (Hs.PatBind _ p tM rhs bnds)                   = [ValD ((maybe id
+                                                                      (flip SigP . toType)
+                                                                      tM) (toPat p))
+                                                              (hsRhsToBody rhs)
+                                                              (hsBindsToDecs bnds)]
+  toDec a@(Hs.ForImp _ cconv safe str n t)             = error $ errorMsg "toDec" a
+  toDec a@(Hs.ForExp _ cconv      str n t)             = error $ errorMsg "toDec" a
+
+
+
+hsMatchesToFunD :: [Hs.Match] -> Dec
+hsMatchesToFunD [] = FunD (mkName []) []   -- errorish
+hsMatchesToFunD xs@(Hs.Match _ n _ _ _ _:_) = FunD (toName n) (fmap hsMatchToClause xs)
+
+
+hsMatchToClause :: Hs.Match -> Clause
+hsMatchToClause (Hs.Match _ _ ps _ rhs bnds) = Clause
+                                                (fmap toPat ps)
+                                                (hsRhsToBody rhs)
+                                                (hsBindsToDecs bnds)
+
+
+
+-- data HsRhs = HsUnGuardedRhs HsExp | HsGuardedRhs [HsGuardedRhs]
+-- data HsGuardedRhs = HsGuardedRhs SrcLoc [HsStmt] HsExp
+-- data Body = GuardedB [(Guard, Exp)] | NormalB Exp
+-- data Guard = NormalG Exp | PatG [Stmt]
+hsRhsToBody :: Hs.Rhs -> Body
+hsRhsToBody (Hs.UnGuardedRhs e) = NormalB (toExp e)
+hsRhsToBody (Hs.GuardedRhss hsgrhs) = let fromGuardedB (GuardedB a) = a
+                                      in GuardedB . concat
+                                          . fmap (fromGuardedB . hsGuardedRhsToBody)
+                                              $ hsgrhs
+
+
+
+hsGuardedRhsToBody :: Hs.GuardedRhs -> Body
+hsGuardedRhsToBody (Hs.GuardedRhs _ [] e)  = NormalB (toExp e)
+hsGuardedRhsToBody (Hs.GuardedRhs _ [s] e) = GuardedB [(hsStmtToGuard s, toExp e)]
+hsGuardedRhsToBody (Hs.GuardedRhs _ ss e)  = let ss' = fmap hsStmtToGuard ss
+                                                 (pgs,ngs) = unzip [(p,n)
+                                                               | (PatG p) <- ss'
+                                                               , n@(NormalG _) <- ss']
+                                                 e' = toExp e
+                                                 patg = PatG (concat pgs)
+                                            in GuardedB $ (patg,e') : zip ngs (repeat e')
+
+
+
+hsStmtToGuard :: Hs.Stmt -> Guard
+hsStmtToGuard (Hs.Generator _ p e) = PatG [BindS (toPat p) (toExp e)]
+hsStmtToGuard (Hs.Qualifier e)     = NormalG (toExp e)
+hsStmtToGuard a@(Hs.LetStmt _)     = error $ errorMsg "hsStmtToGuardExp" a
+
+
+-----------------------------------------------------------------------------
+        
+
+-------------------------------------------------------------------------------
+-- Using Context
+--------------------------------------------------------------------------------
+
+type C a = (StateT Context (Either String)) a
+
+getVarType :: Name -> C Type
+getVarType n = do
+    m <- gets ctx_types
+    case Map.lookup n m of
+        (Just t) -> return t
+        _owise   -> fail $ "Variable not in context: " ++ (show n) 
+
+getConType :: Name -> C Type
+getConType n = do
+    m <- gets ctx_ctors 
+    case Map.lookup n m of
+        (Just t) -> return t
+        _owise   -> fail $ "Ctor not in context: " ++ (show n)
+        
+getSubClasses :: Name -> C [Name]        
+getSubClasses n = do
+    m <- gets ctx_classes
+    case Map.lookup n m of
+        (Just t) -> return t
+        _owise   -> fail $ "Class not in context: " ++ (show n)
+        
+getInstances :: Type -> C [Name]        
+getInstances n = do
+    m <- gets ctx_instances
+    case Map.lookup n m of
+        (Just t) -> return t
+        _owise   -> fail $ "Type not in context: " ++ (show n)
+
+