[nasty hole-thing removed
martin.hofmann@uni-bamberg.de**20090428130755] hunk ./src/Syntax/Expressions.hs 187
-    hole = TConE 'Hole (ConT ''Hole)
+--    hole = TConE 'Hole (ConT ''Hole)
hunk ./src/Syntax/Expressions.hs 575
-instance Term Exp where
-
-    sameSymAtRoot (VarE _) (VarE _)                        = True
-    sameSymAtRoot (ConE n1) (ConE n2)                      = n1 == n2
-    sameSymAtRoot (LitE l1) (LitE l2)                      = l1 == l2
-    sameSymAtRoot (CondE c1 t1 e1) (CondE c2 t2 e2)        = True     
-    sameSymAtRoot (InfixE _ e1 _) (InfixE _ e2 _)          = e1 == e2
-    -- tuples
-    sameSymAtRoot (TupE v1s)(TupE v2s)                     = on (==) length  v1s v2s
-    sameSymAtRoot t@(AppE _ _ )(TupE vs)                   = case head.unfoldAppE $ t of
-                                                                (ConE n) -> isTuple n (length vs)
-                                                                _owise  -> False
-    sameSymAtRoot (TupE vs) t@(AppE _ _ )                 = case head.unfoldAppE $ t of
-                                                                (ConE n) -> isTuple n (length vs)
-                                                                _owise  -> False
-    sameSymAtRoot t1@(AppE _ _ ) t2@(AppE _ _ )            = on (==) (head.unfoldAppE) t1 t2
-    -- empty Lists
-    sameSymAtRoot (ListE []) (ListE [])                    = True
-    sameSymAtRoot (ConE n) (ListE [])                      = isNil n
-    sameSymAtRoot (ListE [])(ConE n)                       = isNil n
-    -- empty list and other (if other is a (:) list it matches default clause)
-    sameSymAtRoot (ListE _)  (ListE [])                    = False
-    sameSymAtRoot (ListE []) (ListE _)                     = False
-    -- non-empty lists
-    sameSymAtRoot (ListE _) (ListE _)                      = True
-    sameSymAtRoot (ListE _) t@(AppE _ _ )                  = case head.unfoldAppE $  t of
-                                                                (ConE n) -> isCons n
-                                                                _owise  -> False
-    sameSymAtRoot t@(AppE _ _ )(ListE _)                   = case head.unfoldAppE $ t of
-                                                                (ConE n) -> isCons n
-                                                                _owise  -> False 
-    sameSymAtRoot  _ _                                     = False
-    
-    substitute s Root _ = s
-    substitute s pos t =
-        case pos of
---            (P i)     -> maybe t id $  moveToSubtermE t i (Just.(substitute s Root))
-            (Dot i p) -> maybe t id $  moveToSubtermE t i (Just.(substitute s p))
-            
-    subterms (VarE _)                        = []
-    subterms (ConE _)                        = []
-    subterms (LitE _)                        = []
-    subterms (TupE vals)                     = vals
-    subterms t@(AppE _ _ )                   = unfoldAppEargs t
-    subterms (ListE [])                      = []
-    subterms (ListE (l:ls))                  = [l, ListE ls] 
-    subterms (CondE e1 e2 e3)                = [e1, e2, e3]    
-    subterms (InfixE (Just e1) e2 (Just e3)) = [e1, e2, e3]
-    subterms (InfixE Nothing e2 (Just e3))   = [hole, e2, e3]
-    subterms (InfixE (Just e1) e2 Nothing)   = [e1, e2, hole]
-    subterms (InfixE Nothing e2 Nothing)     = [hole, e2, hole]
-    subterms    e                            = 
-        error $ "Terms.subterms: Not implemented for Expression " ++ (show e)
-       
-    isVar (VarE _) = True
-    isVar _        = False                                
-    
-    fromVar (VarE n) = n
-    fromVar _ = error "Syntax.Terms.fromVar at Expressions: Not a Variable"
-    
-    toVar _ = VarE
-        
-    hole = ConE 'Hole 
+--instance Term Exp where
+--
+--    sameSymAtRoot (VarE _) (VarE _)                        = True
+--    sameSymAtRoot (ConE n1) (ConE n2)                      = n1 == n2
+--    sameSymAtRoot (LitE l1) (LitE l2)                      = l1 == l2
+--    sameSymAtRoot (CondE c1 t1 e1) (CondE c2 t2 e2)        = True     
+--    sameSymAtRoot (InfixE _ e1 _) (InfixE _ e2 _)          = e1 == e2
+--    -- tuples
+--    sameSymAtRoot (TupE v1s)(TupE v2s)                     = on (==) length  v1s v2s
+--    sameSymAtRoot t@(AppE _ _ )(TupE vs)                   = case head.unfoldAppE $ t of
+--                                                                (ConE n) -> isTuple n (length vs)
+--                                                                _owise  -> False
+--    sameSymAtRoot (TupE vs) t@(AppE _ _ )                 = case head.unfoldAppE $ t of
+--                                                                (ConE n) -> isTuple n (length vs)
+--                                                                _owise  -> False
+--    sameSymAtRoot t1@(AppE _ _ ) t2@(AppE _ _ )            = on (==) (head.unfoldAppE) t1 t2
+--    -- empty Lists
+--    sameSymAtRoot (ListE []) (ListE [])                    = True
+--    sameSymAtRoot (ConE n) (ListE [])                      = isNil n
+--    sameSymAtRoot (ListE [])(ConE n)                       = isNil n
+--    -- empty list and other (if other is a (:) list it matches default clause)
+--    sameSymAtRoot (ListE _)  (ListE [])                    = False
+--    sameSymAtRoot (ListE []) (ListE _)                     = False
+--    -- non-empty lists
+--    sameSymAtRoot (ListE _) (ListE _)                      = True
+--    sameSymAtRoot (ListE _) t@(AppE _ _ )                  = case head.unfoldAppE $  t of
+--                                                                (ConE n) -> isCons n
+--                                                                _owise  -> False
+--    sameSymAtRoot t@(AppE _ _ )(ListE _)                   = case head.unfoldAppE $ t of
+--                                                                (ConE n) -> isCons n
+--                                                                _owise  -> False 
+--    sameSymAtRoot  _ _                                     = False
+--    
+--    substitute s Root _ = s
+--    substitute s pos t =
+--        case pos of
+----            (P i)     -> maybe t id $  moveToSubtermE t i (Just.(substitute s Root))
+--            (Dot i p) -> maybe t id $  moveToSubtermE t i (Just.(substitute s p))
+--            
+--    root _ = error "Syntax.Term.root for Exp not implemented"
+--    subterms (VarE _)                        = []
+--    subterms (ConE _)                        = []
+--    subterms (LitE _)                        = []
+--    subterms (TupE vals)                     = vals
+--    subterms t@(AppE _ _ )                   = unfoldAppEargs t
+--    subterms (ListE [])                      = []
+--    subterms (ListE (l:ls))                  = [l, ListE ls] 
+--    subterms (CondE e1 e2 e3)                = [e1, e2, e3]    
+--    subterms (InfixE (Just e1) e2 (Just e3)) = [e1, e2, e3]
+--    subterms (InfixE Nothing e2 (Just e3))   = [hole, e2, e3]
+--    subterms (InfixE (Just e1) e2 Nothing)   = [e1, e2, hole]
+--    subterms (InfixE Nothing e2 Nothing)     = [hole, e2, hole]
+--    subterms    e                            = 
+--        error $ "Terms.subterms: Not implemented for Expression " ++ (show e)
+--       
+--    isVar (VarE _) = True
+--    isVar _        = False                                
+--    
+--    fromVar (VarE n) = n
+--    fromVar _ = error "Syntax.Terms.fromVar at Expressions: Not a Variable"
+--    
+--    toVar _ = VarE
+--        
+--    hole = ConE 'Hole 
hunk ./src/Syntax/Expressions.hs 679
- 
-
-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)
-
-      
-                        
-instance Unifieable Exp where
-
-    -- 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)            
-           
-
-
-instance Antiunifieable Exp where
-    
-    -- 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!"
-
-
+-- 
+--
+--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)
+--
+--      
+--                        
+--instance Unifieable Exp where
+--
+--    -- 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)            
+--           
+--
+--
+--instance Antiunifieable Exp where
+--    
+--    -- 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!"
+--
+--
hunk ./src/Syntax/Patterns.hs 128
-    hole              = TConP 'Hole [] (ConT ''Hole) 
+--    hole              = TConP 'Hole [] (ConT ''Hole) 
hunk ./src/Syntax/Patterns.hs 464
-    hole = ConP 'Hole []
-
hunk ./src/Syntax/Terms.hs 133
-    -- |The empty term. Especially to avoid the nasty 'Nothing' in 
-    --  'Language.Haskell.TH.InfixE' Not really sure if I need it. Should at 
-    --  least not be visible outside.
-    hole            :: (Term t) => t
+--    -- |The empty term. Especially to avoid the nasty 'Nothing' in 
+--    --  'Language.Haskell.TH.InfixE' Not really sure if I need it. Should at 
+--    --  least not be visible outside.
+--    hole            :: (Term t) => t
hunk ./src/Syntax/Types.hs 177
-    hole =  ConT ''Hole  