[polymorphic type matching (hacked), buggy partitioning with predicates (hacked, too)
martin.hofmann@uni-bamberg.de**20090717113631] move ./src/UI/IOInterpreter.hs ./src/IOInterpreter.hs
hunk ./expl/Examples.hs 258
+mem :: Int -> [Int] -> Bool
+mem 1 [] = False
+mem 2 [] = False
+mem 1 [1] = True
+mem 1 [2] = False
+mem 2 [1] = False
+mem 2 [2] = True
+--member 1 [1,2] = [1,2]
+mem 1 [2,1] = True
+--member 2 [1,2] = [2]
+mem 2 [2,1] = True
+--member 1 [3,1,2] = [1,2]
+--member 1 [1,2,3] = [1,2,3]
+mem 1 [3,2,1] = True
hunk ./src/Context/SynthesisContext.hs 158
-defaultinstances = Map.empty
+defaultinstances = Map.fromList
+    [(ConT ''Bool,[''Eq, ''Ord])
+    ,(ForallT [mkName "a"] 
+             [AppT (ConT ''Eq) (mkVarT "a")
+             ,AppT (ConT ''Ord) (mkVarT "a")   
+             ]
+             (AppT (ConT ''Maybe) (mkVarT "a"))
+     ,[''Eq, ''Ord])
+    ,(ForallT [mkName "a", mkName "b"] 
+             [AppT (ConT ''Eq) (mkVarT "a")
+             ,AppT (ConT ''Ord) (mkVarT "a")  
+             ,AppT (ConT ''Eq) (mkVarT "b")  
+             ,AppT (ConT ''Ord) (mkVarT "b")  
+             ]
+             (AppT 
+                (AppT (ConT ''Either) (mkVarT "a")) 
+                (mkVarT "b"))
+     ,[''Eq, ''Ord])
+    ,(ForallT [mkName "a"] 
+             [AppT (ConT ''Eq) (mkVarT "a")
+             ,AppT (ConT ''Ord) (mkVarT "a")   
+             ]
+             (AppT ListT (mkVarT "a"))
+     ,[''Eq, ''Ord])
+    ]
hunk ./src/Data/GlobalConfig.hs 8
-    setMaxLoops, setCmpRecArg, setTargtes, addTargtes, delTargtes, setBackground,
-    addBackground, delBackground, setPredicates, addPredicates, delPredicates,
+    setMaxLoops, setCmpRecArg, setTargets, addTargets, delTargets, setBackground,
+    addBackground, delBackground, setPredicates, addPredicates, setCtxFile, delPredicates,
hunk ./src/Data/GlobalConfig.hs 33
+    , scr_ctxFile    :: FilePath
hunk ./src/Data/GlobalConfig.hs 39
-defaultSCR = SCR False False False False False NOTICE (-1) Linear [] [] defaultPredicates
+defaultSCR = SCR False False False False False NOTICE (-1) Linear [] [] defaultPredicates ""
hunk ./src/Data/GlobalConfig.hs 82
-setTargtes    v scr = scr{scr_tgts = v}
-addTargtes    v scr = scr{scr_tgts = (scr_tgts scr) ++ v}
-delTargtes    v scr = scr{scr_tgts = (scr_tgts scr) \\ v}
+setTargets    v scr = scr{scr_tgts = v}
+setCtxFile    v scr = scr{scr_ctxFile = v}
+addTargets    v scr = scr{scr_tgts = (scr_tgts scr) ++ v}
+delTargets    v scr = scr{scr_tgts = (scr_tgts scr) \\ v}
hunk ./src/Data/Hypotheses.hs 31
-import Data.Rules
+import Data.Rules hiding (sameSymAt)
hunk ./src/Data/IgorMonad.hs 7
+    -- Igor Monad
hunk ./src/Data/IgorMonad.hs 9
+    
+    --Context
+    context, instances, ctxFile,
+    
hunk ./src/Data/IgorMonad.hs 25
-import Data.List (transpose)
+
hunk ./src/Data/IgorMonad.hs 39
-import Data.List ( (\\) )
+import Data.List ( (\\), transpose )
+import Data.Map (toList)
hunk ./src/Data/IgorMonad.hs 95
+
+instances :: IM [(Type,[Name])]
+instances = gets $ toList . sctx_instances . igor_ctx
+
hunk ./src/Data/IgorMonad.hs 146
+    
+ctxFile :: IM FilePath
+ctxFile = gets $ scr_ctxFile . igor_cnf
+
hunk ./src/IOInterpreter.hs 2
-module UI.IOInterpreter (interprete, typecheck, checkFile, checkDir) where
+module IOInterpreter (interprete, typecheck, checkFile, checkDir) where
hunk ./src/RuleDevelopment/Matching.hs 85
-                    mapM (mkIndirectCall cr n) $ (oneFromEachCol m)
+                    mapM (mkIndirectCall cr n) $ sequence m
+     -- sequence computes all possibilities taking one from each list                    
hunk ./src/RuleDevelopment/Matching.hs 181
-makeIOMatrix tgtrs o cllrs =
-    liftM sequence $ sequence [ anyResult [abduceIO t o c | t <- tgtrs ] | c <- cllrs]
-
-anyResult :: [IM (Maybe a)] -> IM (Maybe [a])
-anyResult = (liftM ((\l -> if (null l) then Nothing else (Just l)).catMaybes)).sequence
-
-oneFromEachCol []    = [[]]
-oneFromEachCol (x:xs)= [e:es | e <- x, es <- (oneFromEachCol xs)]
+makeIOMatrix tgtrs o cllrs = nothingIfAnyEmpty
+    [ nothingIfAnyEmpty [abduceIO t o c | t <- tgtrs ] | c <- cllrs]
+    where
+    nothingIfAnyEmpty = (liftM sequence) . sequence
hunk ./src/RuleDevelopment/Partition.hs 9
---import Data.IOData
+import Syntax
+import qualified Data.Rules as R (sameSymAt)
hunk ./src/RuleDevelopment/Partition.hs 12
-import Data.List (foldl')
+import Data.List (foldl', nub, intersperse)
+import qualified Data.List as L (partition)
+import Data.Maybe (isJust, mapMaybe)
+import Control.Monad (ap)
+import IOInterpreter
hunk ./src/RuleDevelopment/Partition.hs 20
+-- FOR TESTING ONLY
hunk ./src/RuleDevelopment/Partition.hs 29
--- creates new partitions (i.e. CovrRuleements) from one CovrRuleement
+-- creates new partitions (i.e. CovrRules) from one CovrRule
hunk ./src/RuleDevelopment/Partition.hs 32
--- --> closing pairwise with functionCall and subfunction
+-- --> closing pairwise with functionCall and subfunction (not yet implemented
+-- but maybe a good improvement?)
hunk ./src/RuleDevelopment/Partition.hs 35
-partition rf = do
+partition cr = do
hunk ./src/RuleDevelopment/Partition.hs 38
-    let cruls    = breakup rf iod
-    let partpos  = concat.init.ruleVarPos $ crul rf
+    let cruls    = breakup cr iod
+    let partpos  = concat.init.ruleVarPos $ crul cr
hunk ./src/RuleDevelopment/Partition.hs 42
-    llogIN ( text "Rule:" <+> pretty rf )
+    llogIN ( text "Rule:" <+> pretty cr )
hunk ./src/RuleDevelopment/Partition.hs 46
+    ps <- predicates
+    parts' <- partitionWith cr
+    llogIN (text "Partition with" <+> pretty ps <^>
+            text "Into:" <+> pretty parts'
+            )
hunk ./src/RuleDevelopment/Partition.hs 52
-
--- EXPONENTIELLER AUFWAND -- SCHLECHT IMPLEMENTIERT
+ 
+    
+-- complexity should be O(n*m) where n is the number of rules and m the number 
+-- of partitions. To reduce it, an ordering of partitions is necessary
hunk ./src/RuleDevelopment/Partition.hs 57
-partitionAt crs p = 
-    --return $ S.fromList $ map fuse bins
-    -- reverse is only for nicer output 
-    liftM  S.fromList $ mapM fuse bins
+partitionAt crs p =  liftM  S.fromList $ mapM fuse bins
hunk ./src/RuleDevelopment/Partition.hs 64
-   cmpAtPos = (sameSymAt p) `on` crul
-   bin [] e              = [[e]]
-   bin ((x:xs):done) e   = 
-    if (cmpAtPos e x)
-      then (e:x:xs):done
-      else (x:xs):(bin done e)  
+   cmpAtPos = (R.sameSymAt p) `on` crul
+   bin [] e            = [[e]]
+   bin ((x:xs):done) e
+    | cmpAtPos e x     =  (e:x:xs):done
+    | otherwise        =  (x:xs):(bin done e)  
hunk ./src/RuleDevelopment/Partition.hs 71
- 
-
+   
+partitionWith :: CovrRule -> IM [(CovrRules,[Call])]
+partitionWith cr = do
+    let vars = concatMap (uncurry (map . (,))) $ (concatMap getVarPos) . lhs . crul $ cr
+    -- all variables on the lhs of 'cr' paired with their position
+    rs <- liftM (breakup cr) getEvidence
+    ps <- predicates
+    liftM concat $  mapM (tryWith vars rs) ps
+     
+    
+tryWith :: [(TExp,Position)] -> [CovrRule] -> (Name,Type) -> IM [(CovrRules,[Call])]
+tryWith varPos rules (fn,ft) = do
+    i <- instances
+    p <- ctxFile
+    let argpos = (mapMaybe =<< flip lookup . tyPosList i) (argTyList ft)
+    -- argpos :: [[Position]], for each argument of the function 'f', get those
+    -- positions which variables are of a compatible type
+    let crulExprs =  mapMaybe pos2strExpr $ sequence argpos
+    -- crulExprs :: [[(CovrRule,String)]]
+    rawparts <- lift4 $  mapM ((liftM (L.partition snd)) .(mapM (evaluate p))) crulExprs
+    -- parts :: [([(CovrRule,Bool)],[(CovrRule,Bool)])]
+    lift $ mapM mkParts $ filter (\(a,b) -> not (null a || null b)) rawparts
+    
+    where
+    nothingIf f a = if f a then Nothing else Just a
+    argTyList = init . unArrowT
+    -- atys :: [Type], get the argument types as a list
+    tyPosList i = (maybe [] id) . sequence . (map (mbTyPos i)) . nub
+    -- tyPos :: [(Type,[Positions])]
+    -- for each different argument type get the positions of a matching type
+    -- if any argument type has no matching type, [] is returned
+    
+    mbTyPos i = (nothingIf (null . snd)) . (ap (,) (posWithMatchTy i))
+    -- maybe returns the input type paired with the position of compatible variables    
+    posWithMatchTy i t = map snd $ filter (isJust . (matchT i t) . typeOf . fst) varPos
+    -- get all positions from 'varPos' which match the given type 't'
+    
+    pos2strExpr ps = mapM (\r -> liftM (((,) r) . mkStrExpr) (getSubterms ps r)) rules
+    -- pos2Terms :: Maybe [(CovrRule,String)]
+    -- maybe make pairs of rule and the test epression as a string, made from the
+    -- function name and the the terms at the provided positions 'ps'
+    getSubterms ps = (tp "SUBTERMS") . (maybe Nothing (nothingIf null)) . flip mapM ps .  (nothingIfHasVars .) . subtermAt . rhs . crul
+    -- get the subterms at positions in 'ps', return Nothing if either one
+    -- is undefined, or a subterms ontains a variable
+    mkStrExpr = foldl'  (flip ((. (' ' :)) . (++) . showp)) (show . parens . pretty $ fn)
+              -- equal to @(intersperse " ") . ((show fn):) . (map show)@
+              -- but more efficient (?)
+    nothingIfHasVars = maybe Nothing (nothingIf hasVars)
+    mergeCovRs = fuse . fst . unzip
+    mkParts (a,b) = do a' <- mergeCovRs a
+                       b' <- mergeCovRs b
+                       return (covrRules [a',b'],[])
+    lift4 = lift . lift . lift . lift
+    
+    
+evaluate :: FilePath -> (a,String) -> IO (a,Bool)
+evaluate p (a,s) = interprete p s >>= return . ((,) a) . read . (tp $ "XXX\n" ++ (show p) ++ "\n" ++ (show s) ++ "\n")
hunk ./src/RuleDevelopment/Subfunction.hs 4
-import Syntax.Terms (openPositions)
hunk ./src/RuleDevelopment/Subfunction.hs 45
-    posOfVarSubts = map (\(_,i `Dot` _) -> Body (i°Root)) $ openPosition.crul $  cr 
+    posOfVarSubts = map (\(_,i `Dot` _) -> Body (i°Root)) $ openPositions.crul $  cr 
hunk ./src/Syntax/Expressions.hs 241
-    match s@(TWildE i1 _) t     = checkMatch s t >> return ()
+    match s@(TWildE i1 _) t     = nomatch "match" --checkMatch s t >> return ()
hunk ./src/Syntax/Expressions.hs 247
-        matchVar t s
+        matchVar s t
hunk ./src/Syntax/Expressions.hs 249
-    match s          t@(TVarE _ _)          = checkMatch s t >> matchVar t s
+    match s          t@(TVarE _ _)          = checkMatch s t >> matchVar s t
hunk ./src/Syntax/Expressions.hs 657
-{-
-################################################################################
-            DEPRECATED STUFF I DON'T WANT TO DELETE YET !
-################################################################################
--}
---------------------------------------------------------------------------------
--- Deprecated Exp instance declarations
---------------------------------------------------------------------------------    
-
-           
-
---------------------------------------------------------------------------------
--- Exp
---------------------------------------------------------------------------------
-
---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 
---    
---    getPos t s | s == t     = [Root]
---               | otherwise  = 
---                    case t of
---                      (AppE e1 e2)                    -> let args = unfoldAppEargs t 
---                                                         in mapGetPos args s
---                      -- | _e is the operator (see <http://haskell.org/ghc/docs/latest/html/libraries/template-haskell/src/Language-Haskell-TH-Syntax.html#Exp>)
---                      (InfixE Nothing _e Nothing)     -> []
---                      (InfixE (Just e1) _e Nothing)   -> map (°0) (getPos e1 s)
---                      (InfixE Nothing _e (Just e2))   -> map (°1) (getPos e2 s)
---                      (InfixE (Just e1) _e (Just e2)) -> 
---                            let pos1 = map (°0) (getPos e1 s)
---                                pos2 = map (°1) (getPos e2 s)
---                            in pos1 ++ pos2
---                      (ListE [])                      -> [Root ° 0]
---                      (ListE (e1:es))                 -> mapGetPos [e1, ListE es] s  -- I HATE SYNTACTIC SUGAR!!!
---                      (TupE es)                       -> mapGetPos es s                                    
---                      _owise                          -> [] --  VarE Name, ConE Name, LitE Lit          
---                      -- These parts of the TH syntax are ignored:                      
---                      --LamE [Pat] Exp  
---                      --CondE Exp Exp Exp   
---                      --LetE [Dec] Exp  
---                      --CaseE Exp [Match]   
---                      --DoE [Stmt]  
---                      --CompE [Stmt]    
---                      --ArithSeqE Range 
---                      --SigE Exp Type   
---                      --RecConE Name [FieldExp] 
---                      --RecUpdE Exp [FieldExp]
-                          
---    getVars t@(VarE _)                = [t]
---    getVars (ConE _)                  = []
---    getVars (LitE _)                  = []
---    getVars (TupE vals)               = foldl1 union $ map getVars vals
---    getVars (AppE a1 a2)              = on union getVars a1 a2                                            
---    getVars (ListE l)                 = foldl1 union $ map getVars l
---    getVars (CondE e1 e2 e3)          = foldl1 union $ map getVars [e1, e2, e3]
---    getVars (InfixE e1 e2 e3)         = 
---        foldl1 union $ map getVars $ (maybeToList e1) ++ [e2] ++ (maybeToList e3)
-
--- 
---
---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 Unifiable 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 unifiable" 
---            _owise       -> flush "Not unifiable"  
---    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 unifiable" 
---            _owise       -> flush "Not unifiable"  
---        
---    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 unifiable" 
---        
---    unify s@(LitE _) t@(LitE _) 
---        | (s == t)                          = return () 
---        | otherwise                         = flush "Not unifiable"
---         
---    unify (TupE s) (TupE t) 
---        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
---        | otherwise                         = flush "Not unifiable"
---    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 unifiable" 
---            _owise       -> flush "Not unifiable"  
---    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 unifiable" 
---            _owise       -> flush "Not unifiable"
---    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 unifiable!"  
---    unify c@(ConE n)(ListE [])              
---        | c == (ConE '[])                   = return ()
---        | otherwise                         = flush "Not unifiable!"  
---    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 unifiable" 
---            _owise       -> flush "Not unifiable" 
---    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 unifiable" 
---            _owise       -> flush "Not unifiable" 
---    
---    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 unifiable" 
---        
---    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 Antiunifiable 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 156
-    match s@(TVarP _ _)            t                       = matchVar s t
-    match s                        t@(TVarP _ _)           = flush  "No Match!"             
+    match s@(TVarP _ _)            t                       = flush  "No Match!"
+    match s                        t@(TVarP _ _)           = matchVar s t            
hunk ./src/Syntax/Patterns.hs 470
-        
-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 Unifiable 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 _)           = flush  "No Match!"           
-    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@(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 unifiable"         
-    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 unifiable"
-    unify(ConP n []) (ListP [])
-        | isNil n                       = return ()
-        | otherwise                    = flush  "Not unifiable"
-    unify (ListP (s:ss))(ConP n ([p,ps]))
-        | isCons n                     = unify s p >> unify (ListP ss) ps
-        | otherwise                    = flush "Not unifiable"
-    unify(ConP n ([p,ps])) (ListP (s:ss))
-        | isCons n                    = unify s p >> unify (ListP ss) ps
-        | otherwise                    = flush "Not unifiable"    
-    unify s@(ConP n1 p1) t@(ConP n2 p2) 
-        | n1 == n2                     = mapM_ (uncurry unify) (zip p1 p2)
-        | otherwise                    = flush  "Not unifiable"        
-    unify (TupP s) (TupP t) 
-        | (length s) == (length t)     = mapM_ (uncurry unify) (zip s t)
-        | otherwise                    = flush  "Not unifiable"       
-    unify (ConP n p) (TupP t) 
-        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
-        | otherwise                    = flush  "Not unifiable"       
-    unify (TupP t)(ConP n p) 
-        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
-        | otherwise                    = flush  "Not unifiable" 
-    unify (InfixP s1 s2 s3)(InfixP t1 t2 t3)
-        | s2 == t2                     = unify s1 t1 >> unify s3 t3
-        | otherwise = flush  "Not unifiable"        
-    unify s t                          = 
-        flush  ("Term " ++ (show s) ++ "not unifiable with " ++ (show t))
-
-  
-instance Antiunifiable 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
+--        
+--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 Unifiable Pat where
hunk ./src/Syntax/Patterns.hs 489
---    fromVal = \(VarE 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!"
+--
+--    match s@(VarP _) t@(VarP _ )           
+--        | s == t                          = return ()
+--        | otherwise                       = matchVar s t
+--    match s@(VarP _) t                    = matchVar s t
+--    match s          t@(VarP _)           = flush  "No Match!"           
+--    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@(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 unifiable"         
+--    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 unifiable"
+--    unify(ConP n []) (ListP [])
+--        | isNil n                       = return ()
+--        | otherwise                    = flush  "Not unifiable"
+--    unify (ListP (s:ss))(ConP n ([p,ps]))
+--        | isCons n                     = unify s p >> unify (ListP ss) ps
+--        | otherwise                    = flush "Not unifiable"
+--    unify(ConP n ([p,ps])) (ListP (s:ss))
+--        | isCons n                    = unify s p >> unify (ListP ss) ps
+--        | otherwise                    = flush "Not unifiable"    
+--    unify s@(ConP n1 p1) t@(ConP n2 p2) 
+--        | n1 == n2                     = mapM_ (uncurry unify) (zip p1 p2)
+--        | otherwise                    = flush  "Not unifiable"        
+--    unify (TupP s) (TupP t) 
+--        | (length s) == (length t)     = mapM_ (uncurry unify) (zip s t)
+--        | otherwise                    = flush  "Not unifiable"       
+--    unify (ConP n p) (TupP t) 
+--        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
+--        | otherwise                    = flush  "Not unifiable"       
+--    unify (TupP t)(ConP n p) 
+--        | isTuple n (length t) = mapM_ (uncurry unify) (zip p t)
+--        | otherwise                    = flush  "Not unifiable" 
+--    unify (InfixP s1 s2 s3)(InfixP t1 t2 t3)
+--        | s2 == t2                     = unify s1 t1 >> unify s3 t3
+--        | otherwise = flush  "Not unifiable"        
+--    unify s t                          = 
+--        flush  ("Term " ++ (show s) ++ "not unifiable with " ++ (show t))
+--
+--  
+--instance Antiunifiable 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
+--
+--    -- 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!"
hunk ./src/Syntax/Types.hs 8
+    matchT,
+    
hunk ./src/Syntax/Types.hs 19
-import Syntax.Unifier
+import Syntax.Unifier hiding (apply, nullSubst)
hunk ./src/Syntax/Types.hs 22
-import Data.List (union, nub, intersect, intersectBy)
+import Data.List (union, nub, intersect, intersectBy, (\\), find)
+import Data.Maybe (isJust, mapMaybe, maybe)
hunk ./src/Syntax/Types.hs 64
-isGenTy :: (Typed t) => t -> t -> Bool
-isGenTy = sameTy 
-    
+--isGeneralTy :: (Typed t) => t -> t -> Bool
+--isGeneralTy = sameTy 
+
+   
hunk ./src/Syntax/Types.hs 137
+
hunk ./src/Syntax/Types.hs 147
-addPredicates cxt t = 
+addPredicates cxt t =
hunk ./src/Syntax/Types.hs 210
-        
hunk ./src/Syntax/Types.hs 212
--- Unification ignores ForallT , i.e. type classes. Otherwise I would have to 
--- make 'unify' and 'match' statefull w.r.t. to type classes, but this causes 
--- trouble when evaluating Hypotheses
-instance Unifiable Type where
hunk ./src/Syntax/Types.hs 213
-    unify s@(VarT _) t@(VarT _)
-        |(s == t)                           = return ()
-        | otherwise                         = unifyVar s t
-    unify s@(VarT _) t                      = unifyVar s t
-    unify s          t@(VarT _)             = unifyVar t s
-    unify (ConT n1) (ConT n2)       
-        | n1 == n2  = return ()
-        | otherwise = flush "Not Unifiable!"
-    -- tuples
-    unify (TupleT i1) (TupleT i2)     
-        | i1 == i2  = return ()
-        | otherwise = flush "Not Unifiable!"
-    unify (TupleT i) (ConT n)
-        | isTuple n i  = return ()
-        | otherwise = flush "Not Unifiable!"
-    unify (ConT n)(TupleT i)
-        | isTuple n i  = return ()
-        | otherwise    = flush "Not Unifiable!"
-    -- lists
-    unify ListT ListT                 = return ()
-    unify ListT (ConT n)              
-        | isNil n      = return ()
-        | otherwise    = flush "Not Unifiable!"
-        
-    unify (ConT n) ListT              
-        | isNil n      = return ()
-        | otherwise    = flush "Not Unifiable!"
+
+
+
+
+--------------------------------------------------------------------------------   
+-- Matching of polymorphic types (should be implemented consistently with Unifier instead!
+--------------------------------------------------------------------------------   
+type TySubs = [(Type,Type)]  
+
+nullSubst :: TySubs
+nullSubst = []      
+
+class Types t where
+    apply :: TySubs -> t -> t
+    tvars :: t -> [Type]
hunk ./src/Syntax/Types.hs 229
-    unify ArrowT ArrowT               = return ()
-    unify (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
-    unify t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
-    unify (AppT a1 b1) (AppT a2 b2)   = 
-        unify a1 a2 >> unify b1 b2
-    unify _ _                         =  flush "Not Unifiable!"
+instance  (Types a) => Types [a] where
+    apply s = map (apply s)
+    tvars   = nub . concat . map tvars   
+
+instance Types Type where
+    apply s t@(VarT n) = maybe t id (lookup t s)
+    apply s (AppT l r) = AppT (apply s l ) (apply s r)
+    apply s t@(ForallT n c (VarT _)) = maybe t id (lookup t s)
+    apply s (ForallT n c (AppT l r)) = ForallT n c (AppT (apply s l)(apply s r))
+    apply s t = t
+    tvars t@(VarT u) = [t]
+    tvars (AppT l r) = tvars l `union` tvars r
+    tvars t = []
+
+--infxr 4 @@
+--(@@) :: Subst -> Subst -> Subst
+--s1@@s2 = [(u; apply s1 t) j (u; t) s2]++s1
+
+mergeTySubs :: (Monad m) => TySubs -> TySubs -> m TySubs
+mergeTySubs s1 s2 = 
+    if agree then return (s1 ++ s2) 
+      else fail "Merge failed! TySubs not compatible"
+    where 
+    dom = map fst
+    agree = all (\v -> apply s1 v ==
+                       apply s2 v)
+                (dom s1 `intersect` dom s2)
+                
+-- a <-: substitute variable by term b
+(<-:) :: Type -> Type -> TySubs
+(<-:) a b = [(a,b)]
hunk ./src/Syntax/Types.hs 261
-    match s@(VarT _) t@(VarT _)
-        |(s == t)                           = return ()
-        | otherwise                         = matchVar s t
-    match s@(VarT _) t                      = matchVar s t
-    match s          t@(VarT _)             = flush "No Match!"
-    match (ConT n1) (ConT n2)       
-        | n1 == n2  = return ()
-        | otherwise = flush "Not Unifiable!"
+matchT :: (Monad m) =>  [(Type,[Name])] -> Type -> Type -> m TySubs
+matchT _ ty tv@(VarT _) = return $ tv <-: ty
+matchT c ty t@(ForallT _ ps tv@(VarT _))
+    | satisfiesWith c ty t = return $ ty <-: t
+    | otherwise            = fail "Type constraints not satisifieable"
+matchT c (AppT l1 r1) (ForallT n ctx (AppT l2 r2)) = do
+    s1 <- matchT c l1 (ForallT n ctx l2) 
+    s2 <- matchT c r1 (ForallT n ctx r2)
+    mergeTySubs s1 s2
+matchT c (ForallT n ctx (AppT l1 r1))(AppT l2 r2)  = do
+    s1 <- matchT c (ForallT n ctx l1) l2
+    s2 <- matchT c (ForallT n ctx r1) r2
+    mergeTySubs s1 s2
+-- now it should be save to drop the forall, because any types with variables 
+-- are subsumed by patterns below, Haskell does not allow overlapping pattern
+matchT c (ForallT _ _ t1) t2 = matchT c t1 t2
+matchT c t1 (ForallT _ _ t2) = matchT c t1 t2
+matchT c (ConT n1) (ConT n2)       
+    | n1 == n2  = return nullSubst
+    | otherwise = fail "Types don't match!"
hunk ./src/Syntax/Types.hs 282
-    match (TupleT i1) (TupleT i2)     
-        | i1 == i2  = return ()
-        | otherwise = flush "Not Unifiable!"
-    match (TupleT i) (ConT n)
-        | isTuple n i  = return ()
-        | otherwise = flush "Not Unifiable!"
-    match (ConT n)(TupleT i)
-        | isTuple n i  = return ()
-        | otherwise    = flush "Not Unifiable!"
+matchT c (TupleT i1) (TupleT i2)     
+    | i1 == i2  =return nullSubst
+    | otherwise = fail "Types don't match!"
+matchT c (TupleT i) (ConT n)
+    | isTuple n i  = return nullSubst
+    | otherwise = fail "Types don't match!"
+matchT c (ConT n)(TupleT i)
+    | isTuple n i  = return nullSubst
+    | otherwise    = fail "Types don't match!"
hunk ./src/Syntax/Types.hs 292
-    match ListT ListT                 = return ()
-    match ListT (ConT n)              
-        | isNil n      = return ()
-        | otherwise    = flush "Not Unifiable!"
-        
-    match (ConT n) ListT              
-        | isNil n      = return ()
-        | otherwise    = flush "Not Unifiable!"
+matchT c ListT ListT         = return nullSubst
+matchT c ListT (ConT n)          
+    | isNil n      = return nullSubst
+    | otherwise    = fail "Types don't match!"
+    
+matchT c (ConT n) ListT          
+    | isNil n      = return nullSubst
+    | otherwise    = fail "Types don't match!"    
+matchT c ArrowT ArrowT               = return nullSubst
+matchT c _ _                         =  fail "Types don't match!"
hunk ./src/Syntax/Types.hs 303
-    match ArrowT ArrowT               = return ()
-    match (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
-    match t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
-    match (AppT a1 b1) (AppT a2 b2)   = 
-        unify a1 a2 >> unify b1 b2
-    match _ _                         =  flush "Not Unifiable!"
+satisfiesWith :: [(Type,[Name])] -> Type -> Type -> Bool
+satisfiesWith ctx t1 (ForallT _ ps tv) = 
+    let ct = liftM snd $ find (isJust.(matchT ctx t1).fst) ctx
+    -- get names of classes the given type is in
+        cv = constrOf tv ps
+    -- name of classes the type variable is constraint by
+    in maybe False null $ liftM (cv \\) ct
+
+    where
+    constrOf tv = mapMaybe (\(AppT (ConT c) tv') -> if (tv == tv') then Just c else Nothing)
+
+
+---- Unification ignores ForallT , i.e. type classes. Otherwise I would have to 
+---- make 'unify' and 'match' statefull w.r.t. to type classes, but this causes 
+---- trouble when evaluating Hypotheses
+--instance Unifiable Type where
+--
+--    unify s@(VarT _) t@(VarT _)
+--        |(s == t)                           = return ()
+--        | otherwise                         = unifyVar s t
+--    unify s@(VarT _) t                      = unifyVar s t
+--    unify s          t@(VarT _)             = unifyVar t s
+--    unify (ConT n1) (ConT n2)       
+--        | n1 == n2  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    -- tuples
+--    unify (TupleT i1) (TupleT i2)     
+--        | i1 == i2  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    unify (TupleT i) (ConT n)
+--        | isTuple n i  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    unify (ConT n)(TupleT i)
+--        | isTuple n i  = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--    -- lists
+--    unify ListT ListT                 = return ()
+--    unify ListT (ConT n)              
+--        | isNil n      = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--        
+--    unify (ConT n) ListT              
+--        | isNil n      = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--    
+--    unify ArrowT ArrowT               = return ()
+--    unify (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
+--    unify t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
+--    unify (AppT a1 b1) (AppT a2 b2)   = 
+--        unify a1 a2 >> unify b1 b2
+--    unify _ _                         =  flush "Not Unifiable!"
+--
+--    match s@(VarT _) t@(VarT _)
+--        |(s == t)                           = return ()
+--        | otherwise                         = matchVar s t
+--    match s@(VarT _) t                      = matchVar s t
+--    match s          t@(VarT _)             = flush "No Match!"
+--    match (ConT n1) (ConT n2)       
+--        | n1 == n2  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    -- tuples
+--    match (TupleT i1) (TupleT i2)     
+--        | i1 == i2  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    match (TupleT i) (ConT n)
+--        | isTuple n i  = return ()
+--        | otherwise = flush "Not Unifiable!"
+--    match (ConT n)(TupleT i)
+--        | isTuple n i  = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--    -- lists
+--    match ListT ListT                 = return ()
+--    match ListT (ConT n)              
+--        | isNil n      = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--        
+--    match (ConT n) ListT              
+--        | isNil n      = return ()
+--        | otherwise    = flush "Not Unifiable!"
+--    
+--    match ArrowT ArrowT               = return ()
+--    match (ForallT _ _ t1) t2         = unify t1 t2 -- ignoring type classes
+--    match t1 (ForallT _ _ t2)         = unify t1 t2 -- ignoring type classes
+--    match (AppT a1 b1) (AppT a2 b2)   = 
+--        unify a1 a2 >> unify b1 b2
+--    match _ _                         =  flush "Not Unifiable!"
hunk ./src/Syntax/Unifier.hs 28
+
hunk ./src/Syntax/Unifier.hs 83
-    -- | The matching algorithm. Note, that different from unify, where
+    -- | The matching algorithm. @t1 `match` t2@ iff t2 is more general than t1
+    --   Note, that different from unify, where
hunk ./src/Syntax/Unifier.hs 101
-    
---test l r = match l r >> match r l  >> return True
---    `catchError` \_ -> return False
+--     
+--class (Unifieable t, Term t, Ord t, Show t, Pretty t) => UnifiableP t where
+--    
+--    
+--    unifyP ::  (Monad m) => SynCtx -> t -> t -> U m t
+--    
+--    mguP ::  (Monad m) => SynCtx -> t -> t -> m (Substitution t)
+--    mguP c x y = 
+--              -- Logging stuff
+----              setCurrentLogger "Terms.Unifier.mgu" >>
+----              logDE (text "Unifying terms:" <+> pretty x <+> pretty y) >> 
+--              -- 
+--              execStateT (unifyP c x y) []
+--    
+--    --applyMgu :: (Substitution t) -> t -> LM t    
+--    
+--    -- | The matching algorithm. Note, that different from unify, where
+--    --   'unify t1 t2 == unify t2 t1', 'match t1 t2 == match t2 t1' iff 
+--    --   't1 == t2'
+--    matchP :: (Monad m) => SynCtx -> t -> t -> U m t
+--    
+--    -- | @matchesWithSubs t1 t2@ returns a 'Substitution` with which 't1' matches 't2'. If the 
+--    --   'Substitution' is empty, both terms are identical. If the terms do not
+--    --   match, 'fail' is invoked in LM.
+--    matchesWithSubsP :: (Monad m) =>  SynCtx -> t -> t -> m (Substitution t)  
+--    matchesWithSubsP c x y = execStateT (matchP c x y) []
+--    
+----    -- | returns True, if 't1 `matches` t2' and vice versa.
+----    -- TODO think about
+----    -- it should be suffiecient for equality when the resulting substitution is empty    
+----    equal :: (Unifiable t) => t -> t -> Bool
+----    equal = ((maybe False null) . ) . matchesWithSubs 
hunk ./src/Syntax/Unifier.hs 134
-   
+
+     
hunk ./src/Syntax/Unifier.hs 137
-matchVar var t = 
+matchVar t var = 
hunk ./src/UI/UIStarter.hs 30
-import UI.IOInterpreter
+import IOInterpreter
hunk ./src/UI/UIStarter.hs 270
-                (addPredicates [])
+                (addPredicates []) .
+                (setCtxFile . ctxtFile $ s)