[restructuring the Syntax package, implementation of polymorphic matching, hacked application to rest of prog
martin.hofmann@uni-bamberg.de**20091126102828] move ./src/Context/ContextBuilder.hs ./src/Syntax/Builder.hs
move ./src/Context/ModuleContext.hs ./src/Syntax/Specification.hs
move ./src/Context/SynthesisContext.hs ./src/Syntax/Context.hs
move ./src/Logging/PrettyPrinter.hs ./src/PrettyPrinter.hs
rmdir ./src/Context
adddir ./src/Syntax/Class
move ./src/Syntax/Antiunifier.hs ./src/Syntax/Class/Antiunifier.hs
move ./src/Syntax/Terms.hs ./src/Syntax/Class/Term.hs
move ./src/Syntax/Types.hs ./src/Syntax/Type.hs
move ./src/Syntax/Unifier.hs ./src/Syntax/Class/Unifier.hs
hunk ./src/Data/CallDependencies.hs 34
-import Logging hiding (group)
+import Logging
+import PrettyPrinter hiding (group)
hunk ./src/Data/GlobalConfig.hs 12
-import Syntax.IFTemplateHaskell
hunk ./src/Data/GlobalConfig.hs 13
+
+import Syntax
+import PrettyPrinter
hunk ./src/Data/GlobalConfig.hs 90
-mkVarT = VarT . mkName   
+   
hunk ./src/Data/HypoSpace.hs 19
+import Syntax.Context
hunk ./src/Data/HypoSpace.hs 21
+import PrettyPrinter
hunk ./src/Data/HypoSpace.hs 24
+import Control.Monad.Error
hunk ./src/Data/HypoSpace.hs 46
-initHSpace :: CovrRule ->  HSpace  
+initHSpace :: (MonadError e m) => CovrRule -> C m HSpace  
hunk ./src/Data/HypoSpace.hs 67
-pushHypo :: HSpace -> Hypo -> HSpace
-pushHypo = (incCntr . ) . pushUnsafe
+pushHypo :: (MonadError e m) => HSpace -> Hypo -> C m HSpace
+pushHypo hs h = liftM incCntr $ pushUnsafe hs h
hunk ./src/Data/HypoSpace.hs 70
-pushHypos :: [Hypo] -> HSpace ->  HSpace
-pushHypos h hsp  = foldl pushHypo hsp h
+pushHypos :: (MonadError e m) => [Hypo] -> HSpace -> C m HSpace
+pushHypos h hsp  = foldM pushHypo hsp h
hunk ./src/Data/HypoSpace.hs 91
-pushUnsafe :: HSpace -> Hypo -> HSpace
-pushUnsafe (HS c hp) h = HS c (H.insert (rate h) h hp)     
+pushUnsafe :: (MonadError e m) => HSpace -> Hypo -> C m HSpace
+pushUnsafe (HS c hp) h = do rh <- rate h; return $ HS c (H.insert rh h hp)     
hunk ./src/Data/HypoSpace_propagate.hs 13
-
hunk ./src/Data/Hypotheses.hs 20
-import Syntax.IFTemplateHaskell
+import Syntax
+import PrettyPrinter
+
hunk ./src/Data/Hypotheses.hs 24
+import Control.Monad.Error
hunk ./src/Data/Hypotheses.hs 72
-	pretty h = let (cds,bnds) = simplifiedBindings h
-               in  text "Hypo" <+> ( align . vcat $ ((pretty . rate $ h) <> colon) :
-                                             (map pretty $ rules2decs bnds) )
+	pretty h = text "No Pretty implemented"
+--               let pbnds = either (const [text "No Bindings"]) ((map pretty) . rules2decs . snd ) (runC $ simplifiedBindings h)
+--               in text "Hypo" <+> ( align . vcat $ ( (either (const $ text "NoData") pretty $ runC (rate  h)) <> colon): pbnds)
hunk ./src/Data/Hypotheses.hs 80
+bla = let x = 1
+          y = 2
+          z = 3 in
+          x + y + z
+          
hunk ./src/Data/Hypotheses.hs 115
-simplifiedBindings :: Hypo -> (CallDep, [(Name,Rules)])
+simplifiedBindings :: (MonadError e m) => Hypo -> C m (CallDep, [(Name,Rules)])
hunk ./src/Data/Hypotheses.hs 123
-            []      -> (cd,bnds)
-            l@(_:_) -> let (is,nis) = partition (isInjectable bnds) l 
-                       in  sbnds (blckl++nis) (foldl (flip annexFun) cd is)(foldl inject bnds is)
+            []      -> return (cd,bnds)
+            l@(_:_) -> let (is,nis) = partition (isInjectable bnds) l in 
+                       (foldM inject bnds is) >>= sbnds (blckl++nis) (foldl (flip annexFun) cd is)
hunk ./src/Data/Hypotheses.hs 269
-    rate h       =
-     let numPartitions  = numberOfPartitions h
-         numClosedPartitions  = numberOfClosedPartitions h
-         numOpenRules   = numberOfOpenRules h
-         numFreeVars    = numberOfFreeVars h
-         numTotalRules   = numberOfTotalRules h
-         numCycles = cycles . callings $ h
-         numFVarPerRule  = if (numOpenRules == 0) then 0.0 else on (/) fromIntegral numFreeVars numOpenRules
-     in ( mkRatingData
-         --numPartitions + numCycles + numOpenRules,
-          numPartitions
-         -- numCycles,
-          numOpenRules
-          numFreeVars
-          numTotalRules
-          (heuristic h)
-          -- numFVarPerRule
-        )
+    rate h       = do 
+         numPartitions   <- numberOfPartitions h
+         numClosedPartitions <- numberOfClosedPartitions h
+         heu <- heuristic h
+         let numOpenRules   = numberOfOpenRules h
+         let numFreeVars    = numberOfFreeVars h
+         let numTotalRules   = numberOfTotalRules h
+         let numCycles = cycles . callings $ h         
+         let numFVarPerRule  = if (numOpenRules == 0) then 0.0 else on (/) fromIntegral numFreeVars numOpenRules
+         return ( mkRatingData
+                 --numPartitions + numCycles + numOpenRules,
+                  numPartitions
+                 -- numCycles,
+                  numOpenRules
+                  numFreeVars
+                  numTotalRules
+                  heu
+                  -- numFVarPerRule
+                )
hunk ./src/Data/Hypotheses.hs 303
-numberOfPartitions :: Hypo -> Int
-numberOfPartitions = length . (foldl' leastPatterns []) . (filter (not . hasHO)) . S.toList . allRules
-    where
-    leastPatterns [] p = [p]
-    leastPatterns (p1:ps) p2
-        | matchLhss p1 p2 = p1:ps
-        | matchLhss p2 p1 = p2:ps
-        | otherwise       = p1:(leastPatterns ps p2)
+numberOfPartitions ::  (MonadError e m) => Hypo -> C m Int
+numberOfPartitions = numberOfLeastPatterns . allRules
hunk ./src/Data/Hypotheses.hs 306
-numberOfClosedPartitions :: Hypo -> Int
-numberOfClosedPartitions = length . (foldl' leastPatterns []) . (filter (not . hasHO)) . S.toList . closedRules 
+numberOfClosedPartitions :: (MonadError e m) => Hypo -> C m Int
+numberOfClosedPartitions = numberOfLeastPatterns . closedRules 
+          
+numberOfLeastPatterns :: (MonadError e m) => Rules -> C m Int
+numberOfLeastPatterns rs = liftM length $ (foldM leastPatterns []) ((filter (not . hasHO)) . S.toList $ rs) 
hunk ./src/Data/Hypotheses.hs 312
-    leastPatterns [] p = [p]
-    leastPatterns (p1:ps) p2
-        | matchLhss p1 p2 = p1:ps
-        | matchLhss p2 p1 = p2:ps
-        | otherwise       = p1:(leastPatterns ps p2)
+    leastPatterns [] p = return [p]
+    leastPatterns (p1:ps) p2 = do        
+        b1 <- matchLhss p1 p2
+        b2 <- matchLhss p2 p1
+        if b1 then return (p1:ps)
+         else if b2 then return (p2:ps)
+          else liftM (p1:) (leastPatterns ps p2)
hunk ./src/Data/Hypotheses.hs 321
-heuristic h = let (cd,bs) = simplifiedBindings h
-                  allRs = concatMap (S.toList . snd) bs
-                  numFs  = length bs
-                  numRs  = length allRs
-                  numPs  = numberOfPartitions h         
-                  numCs = cycles cd
-                  numLs = loops cd
-                  fracs = map divide [(numFs,numRs) -- rules per function
-                                     ,(numPs,numRs) -- rules per partition
---                                   ,(numCs,numFs) -- cycles per function
-                          --         ,(numLs,numFs) -- loops per function
+heuristic h = do 
+    (cd,bs) <- simplifiedBindings h
+    let allRs = concatMap (S.toList . snd) bs
+    let numFs  = length bs
+    let numRs  = length allRs
+    numPs <- numberOfPartitions h         
+    let numCs = cycles cd
+    let numLs = loops cd
+    let fracs = map divide [(numFs,numRs) -- rules per function
+                           ,(numPs,numRs) -- rules per partition
+--                         ,(numCs,numFs) -- cycles per function
+--                         ,(numLs,numFs) -- loops per function
hunk ./src/Data/Hypotheses.hs 334
-              in (fracs , ((sum fracs)/fromIntegral(length fracs)))
+    return $ (fracs , ((sum fracs)/fromIntegral(length fracs)))
hunk ./src/Data/IOData.hs 15
-import Syntax.Terms (subterms)
-import Syntax.IFTemplateHaskell
+import Syntax (subterms, Name, mkName)
hunk ./src/Data/IOData.hs 18
+import PrettyPrinter
hunk ./src/Data/IOData.hs 147
-    rule <- antiunifyRules rules
+    rule <- lggRules rules
hunk ./src/Data/IOData.hs 154
---    rule         = unLM $ antiunifyRules rules
hunk ./src/Data/IgorMonad.hs 28
-import Context.SynthesisContext 
-
hunk ./src/Data/IgorMonad.hs 33
-import Syntax.Terms
-import Syntax.IFTemplateHaskell
+
+import Syntax
+import PrettyPrinter
hunk ./src/Data/IgorMonad.hs 49
-    , igor_ctx :: SynCtx
+    , igor_ctx :: Context
hunk ./src/Data/IgorMonad.hs 84
-initIgor :: [(Name,Rules)] -> SCR -> SynCtx -> Igor
+initIgor :: [(Name,Rules)] -> SCR -> Context -> Igor
hunk ./src/Data/IgorMonad.hs 91
-context :: IM SynCtx
+context :: IM Context
hunk ./src/Data/IgorMonad.hs 94
-instances :: IM [(Type,[Name])]
-instances = gets $ toList . sctx_instances . igor_ctx
+instances :: IM [(Name,[Type])]
+instances = gets $ toList . ctx_instances . igor_ctx
hunk ./src/Data/IgorMonad.hs 226
-    return $ msum $ map ((matchEval e).crul) ios
+    evls <- lift . lift . lift . lift $ mapM ((matchEval e).crul) ios
+    return $ msum evls
hunk ./src/Data/Rules.hs 7
-    hasHO, freeVars, hasFreeVars, openPositions, antiunifyRules, matchLhss, 
+    hasHO, freeVars, hasFreeVars, openPositions, lggRules, matchLhss, 
hunk ./src/Data/Rules.hs 14
-    tPat2TExp,
+    -- tPat2TExp,
hunk ./src/Data/Rules.hs 38
-
+import Language.Haskell.TH.Syntax (Exp(..), Pat(..), Dec(..), Clause(..), Body(..))
hunk ./src/Data/Rules.hs 43
+import PrettyPrinter
hunk ./src/Data/Rules.hs 62
-    (==) a b = (&&) ((equalLs `on` lhs) a b)((equal `on` rhs) a b)
+    (==) a b = (&&) (((==) `on` lhs) a b) (((==) `on` rhs) a b)
hunk ./src/Data/Rules.hs 179
-antiunifyRules :: [Rule] -> LM Rule
-antiunifyRules rules  = do
+lggRules :: [Rule] -> LM Rule
+lggRules rules  = do
hunk ./src/Data/Rules.hs 184
-        (l,r)<-  antiunify2 tlhss rhss id
-        return $ rule l r
+        r <-  lift . lift . lift $  lggL (rhss:tlhss)
+        return $ rule (tail r)(head r)
hunk ./src/Data/Rules.hs 199
-matchEval :: LHS -> Rule -> Maybe TExp
+matchEval :: (MonadError e m) => LHS -> Rule -> C m (Maybe TExp)
hunk ./src/Data/Rules.hs 201
-    matchesWithSubsLs args (lhs r) >>= flip apply (rhs r)
+    (matchL args (lhs r) >>= return . Just . (flip apply (rhs r)))
+     `catchError` \_ -> return Nothing 
hunk ./src/Data/Rules.hs 204
-matchEvals :: LHS -> [Rule] -> Maybe TExp
-matchEvals = ((listToMaybe . catMaybes) .) . map . matchEval
+matchEvals :: (MonadError e m) => LHS -> [Rule] -> C m (Maybe TExp)
+matchEvals l rs = mapM (matchEval l) rs >>= return . listToMaybe . catMaybes 
hunk ./src/Data/Rules.hs 207
-matchesLhs :: Rule -> Rule -> LM (Substitution TExp)
-matchesLhs = matchesWithSubsLs `on` lhs
+matchesLhs :: (MonadError e m) => Rule -> Rule -> C m (Subst TExp)
+matchesLhs = matchL `on` lhs
hunk ./src/Data/Rules.hs 210
-matchesRhs :: Rule -> Rule -> LM (Substitution TExp)
-matchesRhs = matchesWithSubs `on` rhs
+matchesRhs :: (MonadError e m) => Rule -> Rule -> C m (Subst TExp)
+matchesRhs = match `on` rhs
hunk ./src/Data/Rules.hs 213
-matchLhss :: Rule -> Rule -> Bool
-matchLhss = matchesLs `on` lhs
+matchLhss :: (MonadError e m) => Rule -> Rule -> C m Bool
+matchLhss = matchesL `on` lhs
hunk ./src/Data/Rules.hs 216
-matchRhs :: Rule -> Rule -> Bool
+matchRhs :: (MonadError e m) => Rule -> Rule -> C m Bool
hunk ./src/Data/Rules.hs 219
-subsumeLhss :: Rule -> Rule -> Bool
+subsumeLhss :: (MonadError e m) => Rule -> Rule -> C m Bool
hunk ./src/Data/Rules.hs 222
-subsumeRhs :: Rule -> Rule -> Bool
+subsumeRhs :: (MonadError e m) => Rule -> Rule -> C m Bool
hunk ./src/Data/Rules.hs 285
-tPat2TExp :: TPat -> TExp
-tPat2TExp (TVarP i t) = (TVarE i t)
-tPat2TExp (TLitP l t) = (TLitE l t) 
-tPat2TExp (TConP n ps t) = let ty = mkArrowT ((map typeOf ps) ++ [t])
-                           -- build the arrow type from all args and the target type
-                           in foldTAppE (TConE n ty) (map tPat2TExp ps)
-tPat2TExp (TInfixP l n r t) =
-    TInfixE (tPat2TExp $ l)
-            (TConE n $ mkArrowT [typeOf l, typeOf r, t])
-            (tPat2TExp $ r)            
-            t 
-tPat2TExp (TListP l t) = TListE (map tPat2TExp l) t
-tPat2TExp (TTupP ps t) = TTupE  (map tPat2TExp ps) t
---tPat2TExp p = error $ "Syntax.IFTemplateHaskell.tPat2TExp: Pattern " ++ show p ++
---                  " cannot be transformed into an Expression!" 
+--tPat2TExp :: TPat -> TExp
+--tPat2TExp (TVarP i t) = (TVarE i t)
+--tPat2TExp (TLitP l t) = (TLitE l t) 
+--tPat2TExp (TConP n ps t) = let ty = mkArrowT ((map typeOf ps) ++ [t])
+--                           -- build the arrow type from all args and the target type
+--                           in foldTAppE (TConE n ty) (map tPat2TExp ps)
+--tPat2TExp (TInfixP l n r t) =
+--    TInfixE (tPat2TExp $ l)
+--            (TConE n $ mkArrowT [typeOf l, typeOf r, t])
+--            (tPat2TExp $ r)            
+--            t 
+--tPat2TExp (TListP l t) = TListE (map tPat2TExp l) t
+--tPat2TExp (TTupP ps t) = TTupE  (map tPat2TExp ps) t
+----tPat2TExp p = error $ "Syntax.IFTemplateHaskell.tPat2TExp: Pattern " ++ show p ++
+----                  " cannot be transformed into an Expression!" 
hunk ./src/Data/Rules.hs 307
-simplify :: [Name] -> [(Name,Rules)] -> [(Name,Rules)]
-simplify blckl l = 
-    case partition isRec l of
-        (r,[])     -> r
-        (rec,nrec) -> let r = (getOneWhich hasNoCalls nrec)
-                               `mplus`
-                              (getOneWhich hasOneCall nrec)
+--simplify :: (MonadError e m) => [Name] -> [(Name,Rules)] -> C m [(Name,Rules)]
+--simplify blckl l = 
+--    case partition isRec l of
+--        (r,[])     -> return r
+--        (rec,nrec) -> let r = (getOneWhich hasNoCalls nrec)
hunk ./src/Data/Rules.hs 313
---                              (getOneWhich hasTwoCall nrec)
-                      in maybe (rec ++ nrec) (simplify_ rec nrec) r
-                              
-    where
-    simplify_ rec nrec r = simplify blckl $ uncurry replaceInAll (buildCall r) (rec ++ (deleteBy ((==) `on` fst) r nrec))
-    hasNoCalls = ((==0).(countCalls blckl).rhs.head.S.toList.snd)
-    hasOneCall = ((==1).(countCalls blckl).rhs.head.S.toList.snd)
-    hasTwoCall = ((==2).(countCalls blckl).rhs.head.S.toList.snd)
-    buildCall (n,r) = let cr = head . S.toList $ r
-                      in (mkCall n (typeOf.rhs $ cr) (lhs cr), rhs cr)
-    isRec (n,r)     = (elem n blckl) || ((>1).S.size $ r)
+--                              (getOneWhich hasOneCall nrec)
+----                               `mplus`
+----                              (getOneWhich hasTwoCall nrec)
+--                      in maybe (return $ rec ++ nrec) (simplify_ rec nrec) r
+--                              
+--    where
+--    simplify_ rec nrec r = liftM (simplify blckl) $ uncurry replaceInAll (buildCall r) (rec ++ (deleteBy ((==) `on` fst) r nrec))
+--    hasNoCalls = ((==0).(countCalls blckl).rhs.head.S.toList.snd)
+--    hasOneCall = ((==1).(countCalls blckl).rhs.head.S.toList.snd)
+--    hasTwoCall = ((==2).(countCalls blckl).rhs.head.S.toList.snd)
+--    buildCall (n,r) = let cr = head . S.toList $ r
+--                      in (mkCall n (typeOf.rhs $ cr) (lhs cr), rhs cr)
+--    isRec (n,r)     = (elem n blckl) || ((>1).S.size $ r)
hunk ./src/Data/Rules.hs 333
-replaceInAll :: TExp -> TExp -> [(Name,Rules)] -> [(Name,Rules)]
+replaceInAll :: (MonadError e m) => TExp -> TExp -> [(Name,Rules)] -> C m [(Name,Rules)]
hunk ./src/Data/Rules.hs 335
-    map (\(n,rs) -> (n, S.map repCall rs))
+    mapM (\(n,rs) -> mapM repCall (S.toList rs) >>= return . ((,) n) . rules )
hunk ./src/Data/Rules.hs 337
-    repCall r = r{rhs= replaceCall (rule [cc] ct) (rhs r)}
+    repCall r = do rhs' <- replaceCall (rule [cc] ct) (rhs r)
+                   return r{rhs=rhs'}
hunk ./src/Data/Rules.hs 341
-replaceCall :: Rule -> RHS -> RHS
+replaceCall :: (MonadError e m) => Rule -> RHS -> C m RHS
hunk ./src/Data/Rules.hs 344
-    replaceCall' _ t@(TVarE _ _)       = t
-    replaceCall' _ t@(TLitE _ _)       = t
-    replaceCall' _ t@(TWildE _ _)      = t
-    replaceCall' _ t@(TConE n _)       = t
-    replaceCall' r t = maybe (repSubterms t) id $ matchEval [t] r
-    repSubterms t = (root t $ map (replaceCall' r) $ subterms t)
+    replaceCall' _ t@(TVarE _ _)       = return t
+    replaceCall' _ t@(TLitE _ _)       = return t
+    replaceCall' _ t@(TWildE _ _)      = return t
+    replaceCall' _ t@(TConE n _)       = return t
+    replaceCall' r t =  matchEval [t] r >>= maybe (repSubterms t) return
+    repSubterms t = liftM (root t) $ mapM (replaceCall' r) (subterms t)
hunk ./src/Logging.hs 4
-       module Logging.Logger,
-       module Logging.PrettyPrinter
+       module Logging.Logger
hunk ./src/Logging.hs 9
-import Logging.PrettyPrinter
hunk ./src/Logging/Log.hs 10
-import Logging.PrettyPrinter
+import PrettyPrinter
hunk ./src/Logging/Logger.hs 4
-    tp,ts,lift3, lputStrLn,lputDoc,
+    tp,ts,lift4, lputStrLn,lputDoc,
hunk ./src/Logging/Logger.hs 36
-
+import Syntax.Context
hunk ./src/Logging/Logger.hs 38
-import Logging.PrettyPrinter
+import PrettyPrinter
hunk ./src/Logging/Logger.hs 49
-lift3 = lift . lift . lift
-lputStrLn = lift3 . putStrLn
-lputDoc = lift3 . putDoc
+lift4 = lift . lift . lift . lift
+lputStrLn = lift4 . putStrLn
+lputDoc = lift4 . putDoc
hunk ./src/Logging/Logger.hs 168
-type LM = ELT IO -- (ReaderT IO)
-runLM :: ELT IO a -> LogState -> IO (Either String a, Log)
+type LM = ELT (C IO) -- (ReaderT IO)
+runLM :: ELT (C IO) a -> LogState -> C IO (Either String a, Log)
hunk ./src/Logging/MockLog.hs 10
-import Logging.PrettyPrinter
+import PrettyPrinter
hunk ./src/PrettyPrinter.hs 2
-module Logging.PrettyPrinter  (
+module PrettyPrinter  (
hunk ./src/Rating/Rateable.hs 10
-import Syntax.Terms
-import Syntax.Unifier
-import Syntax.Types
+
+import Syntax
hunk ./src/Rating/Rateable.hs 13
+import PrettyPrinter
hunk ./src/Rating/Rateable.hs 15
+import Control.Monad.Error
hunk ./src/Rating/Rateable.hs 17
+import Data.Function (on)
hunk ./src/Rating/Rateable.hs 20
-import Data.Function (on)
hunk ./src/Rating/Rateable.hs 33
-    rate :: r -> RatingData
+    rate :: (MonadError e m) => r -> C m RatingData
hunk ./src/RuleDevelopment.hs 15
+import PrettyPrinter
hunk ./src/RuleDevelopment/Matching.hs 12
+import Syntax
hunk ./src/RuleDevelopment/Matching.hs 15
-import Syntax
-import Language.Haskell.TH
-import Syntax.Unifier
hunk ./src/RuleDevelopment/Matching.hs 18
+import PrettyPrinter
hunk ./src/RuleDevelopment/Matching.hs 103
-     subs     <- lift $ (on matchesLhs crul scio cr) `catchError`
+     subs     <- lift . lift . lift . lift $ (on matchesLhs crul scio cr) `catchError`
hunk ./src/RuleDevelopment/Matching.hs 109
-     pats  <-  mapM (testPat n cllrs (lhs.crul $ cr)) $ (map . buildPat) subs tgtlhs
+     let subs' = map (\(n,t) -> (toVar t n,t)) subs
+     pats  <-  mapM (testPat n cllrs (lhs.crul $ cr)) $ (map . buildPat) subs' tgtlhs
hunk ./src/RuleDevelopment/Matching.hs 123
-        let rside = mapM (matchEval.lhs $ cr) rs
-        rside' <- maybe (return Nothing) (evalIO n) rside
+        rside <- lift . lift . lift . lift $  mapM (matchEval.lhs $ cr) rs
+        rside' <- maybe (return Nothing) (evalIO n) (sequence rside)
hunk ./src/RuleDevelopment/Matching.hs 143
-normalPat cll tgt =
-    (matchesRhs cll tgt >>=  flip applyL (lhs tgt) >>= return.Just)
+normalPat cll tgt = lift . lift . lift $ 
+    (matchesRhs cll tgt >>=  return . (flip applyL (lhs tgt)) >>= return.Just)
hunk ./src/RuleDevelopment/Matching.hs 211
-       else do s <- lift $ (liftM Just $ on matchesRhs crul cll tgt) `catchError`
+       else do s <- lift . lift . lift . lift $ (liftM Just $ on matchesRhs crul cll tgt) `catchError`
hunk ./src/RuleDevelopment/Matching.hs 223
-                               let unaffectedvars = cllvars \\ (map fst s)
-                               let s' = s ++ [ v <~ (TWildE n t) | v@(TVarE n t) <- unaffectedvars]
+                               let unaffectedvars = cllvars \\ (map (\(n,t) -> toVar t n) s)
+                               let s' = s ++ [ (n , (TWildE n t)) | v@(TVarE n t) <- unaffectedvars]
hunk ./src/RuleDevelopment/Matching.hs 227
-                               rhss' <- lift $ mapM (apply s') (lhs.crul $ tgt)
+                               let rhss' = map (apply s') (lhs.crul $ tgt)
hunk ./src/RuleDevelopment/Partition.hs 19
+import PrettyPrinter
hunk ./src/RuleDevelopment/Partition.hs 71
-    
-   
-partitionWith :: CovrRule -> IM [(CovrRules,[Call])]
-partitionWith cr = do
-    let vars = (tp $ "VARPOS" ++ (showp cr)) . concatMap (uncurry (map . (,))) $ (concatMap getVarPos) . lhs . crul $ cr
-    -- all variables on the lhs of 'cr' paired with their position
-    -- TODO What about constant term, e.g. partitioning whether the first arg
-    -- of a list is '1' ?
-    rs <- liftM (breakup cr) getEvidence
-    ps <- predicates
-    liftM concat $  mapM (tryWith vars rs) ps
-     
--- TODO: It is sufficient to use Type instead of TExp in first arg, and it is 
---       necessary t ouse RulePos instead of Position, or at least keep track 
---       of the argumet position
-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 = (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")
-
-    
+-- TODO: Patition using predicates
+--   
+--partitionWith :: CovrRule -> IM [(CovrRules,[Call])]
+--partitionWith cr = do
+--    let vars = (tp $ "VARPOS" ++ (showp cr)) . concatMap (uncurry (map . (,))) $ (concatMap getVarPos) . lhs . crul $ cr
+--    -- all variables on the lhs of 'cr' paired with their position
+--    -- TODO What about constant term, e.g. partitioning whether the first arg
+--    -- of a list is '1' ?
+--    rs <- liftM (breakup cr) getEvidence
+--    ps <- predicates
+--    liftM concat $  mapM (tryWith vars rs) ps
+--     
+---- TODO: It is sufficient to use Type instead of TExp in first arg, and it is 
+----       necessary t ouse RulePos instead of Position, or at least keep track 
+----       of the argumet position
+--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 = (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 10
-import Logging
hunk ./src/RuleDevelopment/Subfunction.hs 11
+import Logging
+import PrettyPrinter
hunk ./src/RuleDevelopment/UniProp.hs 8
+import Control.Monad.Error
hunk ./src/RuleDevelopment/UniProp.hs 16
-import Syntax.Expressions
-import Syntax.Terms
-import Syntax.Types
-import Syntax.IFTemplateHaskell
+
+import Syntax
+import PrettyPrinter
hunk ./src/RuleDevelopment/UniProp.hs 27
-    maybe (naiveMap cr evi) (mkFoldCall cr)(checkUniPropAndMkIOs $ evi)
+    mbios <- lift . lift . lift . lift $ (checkUniPropAndMkIOs $ evi)
+    maybe (naiveMap cr evi) (mkFoldCall cr)mbios
hunk ./src/RuleDevelopment/UniProp.hs 181
-    subs <- lift $ matchesLhs vr (crul cr)
+    subs <- lift . lift . lift . lift $ matchesLhs vr (crul cr)
hunk ./src/RuleDevelopment/UniProp.hs 207
-    replaceInverseIn = (flip (uncurry . flip $ replaceTerm))
+    replaceInverseIn t (n,s)= (flip (uncurry . flip $ replaceTerm)) t (toVar t n, t)
hunk ./src/RuleDevelopment/UniProp.hs 217
-checkUniPropAndMkIOs :: [Rule] -> Maybe (Rule,[Rule])
+checkUniPropAndMkIOs :: (MonadError e m) => [Rule] -> C m (Maybe (Rule,[Rule]))
hunk ./src/RuleDevelopment/UniProp.hs 219
-    definedOnNil evi >>= \(r,rs) -> 
-     mapM (abduceIO evi) rs >>= 
-      return . (,) r 
+    case definedOnNil evi of
+        Just (r,rs) -> do ios <- mapM (abduceIO evi) rs
+                          return $ case (sequence ios) of
+                                    Just rs' -> Just (r,rs')
+                                    Nothing   -> Nothing
+        Nothing -> return Nothing 
hunk ./src/RuleDevelopment/UniProp.hs 279
-abduceIO :: [Rule] -> Rule -> Maybe Rule
-abduceIO evi r = do
-    (as,(x,xs)) <- liftM ((,) (init . lhs $ r)) $ headTail . (:[]) . last. lhs $ r
-    xs'    <- matchEvals (as ++ [xs]) evi
-    let io = rule (as ++ [x,xs']) (rhs r)
-    if not . hasFreeVars $ io then Just io else Nothing         
+abduceIO :: (MonadError e m) => [Rule] -> Rule -> C m (Maybe Rule)
+abduceIO evi r =
+    let temp = liftM ((,) (init . lhs $ r)) $ headTail . (:[]) . last. lhs $ r in 
+    case temp of 
+        (Just (as,(x,xs))) -> do mbxs'    <- matchEvals (as ++ [xs]) evi
+                                 case mbxs' of 
+                                    Just xs' -> let io = rule (as ++ [x,xs']) (rhs r) in
+                                                return $ if not . hasFreeVars $ io then Just io else Nothing
+                                    _owise -> return Nothing
+        _owise -> return Nothing
+--         _owise     -> return Nothing         
hunk ./src/Syntax.hs 4
-    module Syntax.Terms,
-    module Syntax.Unifier,
-    module Syntax.Antiunifier,
-    module Syntax.Patterns,
+    module Syntax.Class,
hunk ./src/Syntax.hs 6
-    module Syntax.Types,
-    module Syntax.IFTemplateHaskell
+--    module Syntax.UnifyExp,
+    module Syntax.Type,
+--    module Syntax.UnifyTy,
+    module Syntax.Context,
+    module Syntax.Builder,
hunk ./src/Syntax.hs 14
-import Language.Haskell.TH 
-                           ( Dec (FunD)
-                           , Clause (Clause)
-                           , Body (NormalB)
-                           , Name, mkName
-                        --   , Exp (VarE, ConE, LitE, ListE, TupE, InfixE, AppE, CondE)
-                        --   , Pat (VarP, ConP, LitP, ListP, TupP, InfixP)
-                           , Q(..))
-import Syntax.Terms
-import Syntax.Unifier
-import Syntax.Antiunifier
-import Syntax.Expressions
-import Syntax.Patterns
-import Syntax.Types
-
-import Syntax.IFTemplateHaskell
hunk ./src/Syntax.hs 15
+import Syntax.Class
+import Syntax.Expressions
+import Syntax.UnifyExp
+import Syntax.Type
+import Syntax.UnifyTy
+import Syntax.Context
+import Syntax.Builder
hunk ./src/Syntax/Builder.hs 2
-module Context.ContextBuilder (
+module Syntax.Builder (
hunk ./src/Syntax/Builder.hs 4
-    parseContext, buildCtx,
-    
-    module Context.ModuleContext 
+    parseSpec
+     
hunk ./src/Syntax/Builder.hs 19
+import Language.Haskell.TH.Syntax hiding (Type(..))
+import qualified Language.Haskell.TH.Syntax as TH (Type(..))
hunk ./src/Syntax/Builder.hs 24
-import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Error
hunk ./src/Syntax/Builder.hs 27
-import Logging.Logger
+import PrettyPrinter
+import Logging
hunk ./src/Syntax/Builder.hs 30
-import Syntax.Types hiding (mkAppT)
-import Syntax.Patterns
+import Syntax.Type hiding (mkAppT)
+import Syntax.UnifyTy
hunk ./src/Syntax/Builder.hs 33
-import Syntax.Terms
-
-import Data.Rules
-
---import Context.SynthesisContext
-import Context.ModuleContext
-
+--import Syntax.Class.Unifier
+--
+import Syntax.Specification
+import Syntax.Context ( Context(..), emptyContext, defaultContext, C, 
+                         getConType, getVarType, withC) 
hunk ./src/Syntax/Builder.hs 45
-parseContext :: ModuleCtx -> String ->  IO ModuleCtx
-parseContext ctx s = do 
-    mdule <- parse s
-    foldM buildCtx ctx  (funBindsLast mdule) 
+parseSpec :: String ->  IO Specification
+parseSpec s = do 
+    (bnds,decls) <- liftM bindsNdecls $ parse s
+    spec <- foldM updateCtx (emptySpec defaultContext) decls
+    spec' <- foldM processBnd spec bnds
+    return  spec'
hunk ./src/Syntax/Builder.hs 53
-    funBindsLast = uncurry (++) . (partition noFunBind) . moduleDecls
-    moduleDecls (HsModule _ _ _ _ d) = d
-    noFunBind (HsFunBind _ ) = False
-    noFunBind _               = True
hunk ./src/Syntax/Builder.hs 60
-
-buildCtx :: ModuleCtx -> HsDecl -> IO ModuleCtx
-buildCtx ctx d@(HsTypeDecl _  _ _ _) = 
-    let pSynTy = map (\(TySynD n args t) ->  ((mkAppT n args), fixType t) ) $ toDec d
+bindsNdecls = (partition isFunBind) . moduleDecls
+    where    
+    isFunBind e = case e of (HsFunBind _ ) -> True; _ -> False
+    moduleDecls (HsModule _ _ _ _ d) = d
+ 
+processBnd ctx d@(HsFunBind _ ) = do
+    let [(FunD n cls)] = toDec d
+    case (clauses2rules (spec_ctx ctx) n cls) of
+        Right rs -> return $ addToBindings [rs] ctx
+        Left msg -> fail  msg
+processBnd ctx _ = do
+    putStrLn $ "processBnd: Skipping something that is not a HsFunBind."
+    return ctx     
+        
+updateCtx :: Specification -> HsDecl -> IO Specification
+updateCtx ctx d@(HsTypeDecl _  _ _ _) = 
+    let pSynTy = map (\(TySynD n args t) -> ((mkAppT n args), fixType $ fromTH t) ) $ toDec d
hunk ./src/Syntax/Builder.hs 79
-buildCtx ctx (HsDataDecl _ assts tname args condecls derive) = do
+updateCtx ctx (HsDataDecl _ assts tname args condecls derive) = do
hunk ./src/Syntax/Builder.hs 93
---buildCtx ctx (HsClassDecl sloc _ _ [] _ _) = can never be
-buildCtx ctx (HsClassDecl sloc _ _ (_:_:_) _) =
+--updateCtx ctx (HsClassDecl sloc _ _ [] _ _) = can never be
+updateCtx ctx (HsClassDecl sloc _ _ (_:_:_) _) =
hunk ./src/Syntax/Builder.hs 96
-buildCtx ctx (HsClassDecl sloc assts cname anames decls) = do
+updateCtx ctx (HsClassDecl sloc assts cname anames decls) = do
hunk ./src/Syntax/Builder.hs 108
-        pNameTy     = map (\(SigD n t) -> (n, (mkForallT assts' t))) sigds
+        pNameTy     = map (\(SigD n t) -> (n, (mkForallT assts' $ fromTH t))) sigds
hunk ./src/Syntax/Builder.hs 115
---buildCtx _ (HsInstDecl sloc _ _ [] _) -- can never be 
-buildCtx _ (HsInstDecl sloc _ _ (_:_:_) _) =      
+--updateCtx _ (HsInstDecl sloc _ _ [] _) -- can never be 
+updateCtx _ (HsInstDecl sloc _ _ (_:_:_) _) =      
hunk ./src/Syntax/Builder.hs 118
-buildCtx ctx (HsInstDecl sloc assts qname [t] _) = do 
+updateCtx ctx (HsInstDecl sloc assts qname [t] _) = do 
hunk ./src/Syntax/Builder.hs 125
-buildCtx ctx d@(HsTypeSig _ _ _ ) =
-    let pNmsTys  = map (\(SigD n t) -> (n, fixType t)) $ toDec d  
+updateCtx ctx d@(HsTypeSig _ _ _ ) =
+    let pNmsTys  = map (\(SigD n t) -> (n, fixType $ fromTH t)) $ toDec d  
hunk ./src/Syntax/Builder.hs 129
-buildCtx ctx d@(HsFunBind _ ) = do 
-    let [(FunD n cls)] = toDec d
-    case (clauses2rules ctx n cls) of
-        Right rs -> return $ addToBindings [rs] ctx
-        Left msg -> fail  msg
-    
---buildCtx e (HsGDataDecl sloc _ _ _ _ _ _ _ ) = do
+updateCtx ctx d@(HsFunBind _ ) = do
+    putStrLn $ "updateCtx: Skipping HsFunBind."
+    return ctx     
+        
+--updateCtx e (HsGDataDecl sloc _ _ _ _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 136
---buildCtx e (HsTypeFamDecl sloc _ _ _ ) = do
+--updateCtx e (HsTypeFamDecl sloc _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 139
---buildCtx e (HsDataFamDecl sloc _ _ _ _ ) = do
+--updateCtx e (HsDataFamDecl sloc _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 142
---buildCtx e (HsTypeInsDecl sloc _ _ ) = do
+--updateCtx e (HsTypeInsDecl sloc _ _ ) = do
hunk ./src/Syntax/Builder.hs 145
---buildCtx e (HsDataInsDecl sloc _ _ _ _ ) = do
+--updateCtx e (HsDataInsDecl sloc _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 148
---buildCtx e (HsGDataInsDecl sloc _ _ _ _ _ ) = do
+--updateCtx e (HsGDataInsDecl sloc _ _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 151
-buildCtx e (HsInfixDecl sloc _ _ _ ) = do
+updateCtx e (HsInfixDecl sloc _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 154
---buildCtx e (HsDerivDecl sloc _ _ _ ) = do
+--updateCtx e (HsDerivDecl sloc _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 157
-buildCtx e (HsDefaultDecl sloc _ ) = do
+updateCtx e (HsDefaultDecl sloc _ ) = do
hunk ./src/Syntax/Builder.hs 160
---buildCtx e (HsSpliceDecl sloc _ ) = do
+--updateCtx e (HsSpliceDecl sloc _ ) = do
hunk ./src/Syntax/Builder.hs 163
-buildCtx e (HsPatBind sloc _ _ _) = do
+updateCtx e (HsPatBind sloc _ _ _) = do
hunk ./src/Syntax/Builder.hs 166
---buildCtx e (HsForImp sloc _ _ _ _ _ ) = do
+--updateCtx e (HsForImp sloc _ _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 169
---buildCtx e (HsForExp sloc _ _ _ _ ) = do
+--updateCtx e (HsForExp sloc _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 172
---buildCtx e (HsRulePragmaDecl sloc _ ) = do
+--updateCtx e (HsRulePragmaDecl sloc _ ) = do
hunk ./src/Syntax/Builder.hs 175
---buildCtx e (HsDeprPragmaDecl sloc _ ) = do
+--updateCtx e (HsDeprPragmaDecl sloc _ ) = do
hunk ./src/Syntax/Builder.hs 178
---buildCtx e (HsWarnPragmaDecl sloc _ ) = do
+--updateCtx e (HsWarnPragmaDecl sloc _ ) = do
hunk ./src/Syntax/Builder.hs 181
---buildCtx e (HsInlineSig sloc _ _ _ ) = do
+--updateCtx e (HsInlineSig sloc _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 184
---buildCtx e (HsSpecSig sloc _ _ ) = do
+--updateCtx e (HsSpecSig sloc _ _ ) = do
hunk ./src/Syntax/Builder.hs 187
---buildCtx e (HsSpecInlineSig sloc _ _ _ _ ) = do
+--updateCtx e (HsSpecInlineSig sloc _ _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 190
---buildCtx e (HsInstSig sloc _ _ _ ) = do
+--updateCtx e (HsInstSig sloc _ _ _ ) = do
hunk ./src/Syntax/Builder.hs 193
---buildCtx e (HsUnknownDeclPragma sloc _ _ ) = do
+--updateCtx e (HsUnknownDeclPragma sloc _ _ ) = do
hunk ./src/Syntax/Builder.hs 225
--- +++++++++++++++++
--- This should be rather imlemented with 'unify', however, I have not solved 
--- unification of polymorphic types with type classes. Using 'unify' will also
--- cause a module cycle at the moment. So this just instantiates variables 
---  in the fsecond type, ignornig 'ForallT' 
--- | specialising Type 't2' using Type 't1', where 't2' contains type variables
---   which are to instantiate using 't1'. E.g.
---   @specialise '[Int]' '(b,a) -> (a,String) -> [a]' is '(b,Int) -> (Int,String) -> [Int]@ 
---   so 't1' is always more general the 't2'
-specialise :: Type -> Type -> StateT ModuleCtx (Either String) Type
-specialise t1 t2 = do --return t1
-    subst <- instantiate (last . unArrowT $ t2) t1
-    return $ applySubs t2 subst
-
-applySubs :: Type -> [(Type,Type)] -> Type
-applySubs t@(VarT n) s = 
-    case lookup t s of
-       (Just t') -> t'
-       _owise    -> t
-applySubs t@(ForallT _ _ (VarT n)) s =  
-    case lookup (VarT n) s  of
-       (Just t') -> t'
-       _owise    -> t
-applySubs (ForallT ns ctx t) s = (ForallT ns ctx (applySubs t s))
-applySubs (AppT t1 t2) s =
-    AppT (applySubs t1 s) (applySubs t2 s)
-applySubs t _     =  t
-       
--- This is a quick-and-dirty-kind-of-unification function       
-instantiate :: Type -> Type -> StateT ModuleCtx (Either String) [(Type,Type)]
-instantiate v@(VarT n) t  = return [(v,t)]
-instantiate (ForallT ns ctx t1) t2 = instantiate t1 t2    
-instantiate t1@(AppT a11 a12) t2@(AppT a21 a22) =
-    liftM2 union (instantiate a11 a21) (instantiate a12 a22)
-    --liftM concat $ mapM (uncurry instantiate) $ zip (unfoldAppT t1) (unfoldAppT t2)
-instantiate (ConT n1) (ConT n2) 
-    | n1 == n2            = return []
-    | otherwise           = fail "types do not unify"
-instantiate (TupleT i1) (TupleT i2) 
-    | i1 == i2            = return []
-    | otherwise           = fail "types do not unify"
-instantiate (TupleT i) (ConT n) 
-    | isTuple n i         = return []
-    | otherwise           = fail "types do not unify"
-instantiate (ConT n)(TupleT i)  
-    | isTuple n i         = return []
-    | otherwise           = fail "types do not unify"
-instantiate ArrowT ArrowT = return []
-instantiate ListT ListT   = return []
-instantiate ListT (ConT n)
-    | isNil n             = return []
-    | otherwise           = fail "types do not unify"
-instantiate (ConT n) ListT 
-    | isNil n             = return []
-    | otherwise           = fail "types do not unify"
-instantiate a b           = fail $ "types do not unify " ++ (show (a,b))
--- +++++++++++++++++
-       
hunk ./src/Syntax/Builder.hs 233
-    toTExp   :: Type -> t -> C TExp
-    
+    toTExp   :: (MonadError e m) => Type -> t -> C m TExp
+        
hunk ./src/Syntax/Builder.hs 237
-class ToTPat t where
-    toTPat   :: Type -> t -> C TPat
+--class ToTPat t where
+--    toTPat   :: Type -> t -> C TPat
hunk ./src/Syntax/Builder.hs 256
-                ty <- getVarType n >>= specialise t
+                ty <- getVarType n >>= maybe (fail "Fun not in Context") (specialise t)
hunk ./src/Syntax/Builder.hs 262
-                ty <- getConType n >>= specialise t
+                ty <- getConType n >>= maybe (fail "Ctor not in Context") (specialise t)
hunk ./src/Syntax/Builder.hs 268
-                ty <- getConType n >>=  specialise t
+                ty <- getConType n >>=  maybe (fail "Ctor not in Context") (specialise t)
hunk ./src/Syntax/Builder.hs 278
-instance ToTPat Pat where
-    toTPat t (LitP l) = return $ TLitP l t
-    toTPat t (VarP n) = return $ TVarP n t
-    toTPat tupty (TupP l) = do
+
+instance ToTExp Pat where
+    toTExp t (LitP l) = return $ TLitE l t
+    toTExp t (VarP n) = return $ TVarE n t
+    toTExp tupty (TupP l) = do
hunk ./src/Syntax/Builder.hs 284
-        tes <- zipWithM toTPat tuptys l 
-        return $ TTupP tes tupty
-    toTPat t (ConP n args) = do 
-        ty <- getConType n >>= specialise t
+        tes <- zipWithM toTExp tuptys l 
+        return $ TTupE tes tupty
+    toTExp t (ConP n args) = do 
+        ty <- getConType n >>= maybe (fail "Ctor not in Context") (specialise t)
hunk ./src/Syntax/Builder.hs 289
-        teargs <- zipWithM toTPat tyargs args
-        return $ TConP n teargs t
-    toTPat lstty (ListP l) = do
+        teargs <- zipWithM toTExp tyargs args
+        return $ foldTAppE (mkTConE n tyargs) teargs
+    toTExp lstty (ListP l) = do
hunk ./src/Syntax/Builder.hs 293
-        tes <- mapM (toTPat elemty) l
-        return $ TListP  tes lstty                 
-    toTPat t (InfixP a1 n a2) = do
-                ty <- getConType n >>= specialise t
+        tes <- mapM (toTExp elemty) l
+        return $ TListE  tes lstty                 
+    toTExp t (InfixP a1 n a2) = do
+                ty <- getConType n >>= maybe (fail "Ctor not in Context") (specialise t)
hunk ./src/Syntax/Builder.hs 298
-                a1' <- toTPat tya1 a1
-                a2' <- toTPat tya2 a2
-                return $ TInfixP a1' n a2' t     
-    toTPat _ p = fail $ "No Translation defined for " ++ (show p)
+                a1' <- toTExp tya1 a1
+                a2' <- toTExp tya2 a2
+                return $ TInfixE a1' (TConE n ty) a2' t     
+    toTExp _ p = fail $ "No Translation defined for " ++ (show p)
hunk ./src/Syntax/Builder.hs 304
-clauses2rules :: ModuleCtx -> Name -> [Clause] -> Either String (Name, Rules)
+clauses2rules :: (Monad m) => Context -> Name -> [Clause] -> m (Name, [Equation])
hunk ./src/Syntax/Builder.hs 306
-    case Map.lookup n (mctx_types cxt)of
-        (Just ty) -> do rs <- evalStateT (mapM (clause2rule ty) cls) cxt
-                        return (n, mkRules rs)
+    case Map.lookup n (ctx_types cxt)of
+        (Just ty) -> either fail (return . ((,) n)) $ withC (mapM (clause2rule ty) cls) cxt
hunk ./src/Syntax/Builder.hs 313
-        ls' <- zipWithM toTPat (init argty) ls
+        ls' <- zipWithM toTExp (init argty) ls
hunk ./src/Syntax/Builder.hs 315
-        return ((map tPat2TExp ls'), rs')    -- TODO quick and dirty, dont convert to Pat in the first place
+        return (ls', rs')  
hunk ./src/Syntax/Builder.hs 318
+     
hunk ./src/Syntax/Builder.hs 510
-TH.InfixE is right associativ
+InfixE is right associativ
hunk ./src/Syntax/Builder.hs 540
-  toExp (HsExpTypeSig _ e t)      = SigE (toExp e) (toType t)
+  toExp (HsExpTypeSig _ e t)      = SigE (toExp e) (toTH $ toType t)
hunk ./src/Syntax/Builder.hs 629
+fromTH (TH.ForallT ns cxt t) = ForallT ns (map fromTH cxt)(fromTH t)
+fromTH (TH.VarT n)           = VarT n
+fromTH (TH.ConT n)           = ConT n
+fromTH (TH.TupleT i)         = TupleT i
+fromTH TH.ArrowT             = ArrowT
+fromTH TH.ListT              = ListT
+fromTH (TH.AppT l r)         = AppT (fromTH l)(fromTH r)
+
+toTH (ForallT ns cxt t) = TH.ForallT ns (map toTH cxt)(toTH t)
+toTH (VarT n)           = TH.VarT n
+toTH (ConT n)           = TH.ConT n
+toTH (TupleT i)         = TH.TupleT i
+toTH ArrowT             = TH.ArrowT
+toTH ListT              = TH.ListT
+toTH (AppT l r)         = TH.AppT (toTH l)(toTH r)
+     
hunk ./src/Syntax/Builder.hs 666
-hsBangTypeToStrictType :: HsBangType -> (Strict, Type)
-hsBangTypeToStrictType (HsBangedTy t)   = (IsStrict, toType t)
-hsBangTypeToStrictType (HsUnBangedTy t) = (NotStrict, toType t)
+hsBangTypeToStrictType :: HsBangType -> (Strict, TH.Type)
+hsBangTypeToStrictType (HsBangedTy t)   = (IsStrict, toTH $ toType t)
+hsBangTypeToStrictType (HsUnBangedTy t) = (NotStrict, toTH $ toType t)
hunk ./src/Syntax/Builder.hs 686
-  toDec (HsTypeDecl _ n ns t) = [TySynD (toName n) (fmap toName ns) (toType t)]
+  toDec (HsTypeDecl _ n ns t) = [TySynD (toName n) (fmap toName ns) (toTH $ toType t)]
hunk ./src/Syntax/Builder.hs 715
-  toDec a@(HsTypeSig _ ns t)                          = [SigD (toName n) (toType t) | n <- ns]
+  toDec a@(HsTypeSig _ ns t)                          = [SigD (toName n) (toTH $ toType t) | n <- ns]
hunk ./src/Syntax/Builder.hs 778
+-- | Returns only the arguments of an 'AppE'xpression.
+unfoldAppEargs = tail . unfoldAppE
+
+-- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
+--   @ConE@ of the function name or the constructor.
+unfoldAppE :: Exp -> [Exp]
+unfoldAppE e = f [] e
+    where 
+    f done e =
+        case e of
+            (AppE e1@(VarE _) e2) -> e1:e2:done
+            (AppE e1@(ConE _) e2) -> e1:e2:done
+            (AppE e1 e2)       -> f (e2:done) e1
+            _owise             -> e:done
+ 
+foldAppE :: [Exp] -> Exp
+foldAppE es = foldl1 AppE es
+
+
addfile ./src/Syntax/Class.hs
hunk ./src/Syntax/Class.hs 1
-
+
+module Syntax.Class (
+
+    module Syntax.Class.Subst,
+    module Syntax.Class.Antiunifier,
+    module Syntax.Class.Unifier,
+    module Syntax.Class.Term,
+    module Syntax.IFTemplateHaskell,
+
+) where
+
+
+import Syntax.Class.Subst
+import Syntax.Class.Antiunifier
+import Syntax.Class.Unifier
+import Syntax.Class.Term
+import Syntax.IFTemplateHaskell
hunk ./src/Syntax/Class/Antiunifier.hs 5
-module Syntax.Antiunifier
+module Syntax.Class.Antiunifier
hunk ./src/Syntax/Class/Antiunifier.hs 8
-    Antiunifiable (
-        antiunify,        -- :: (Antiunifiable k v t) => [t] -> t
-        antiunifyWithMap, -- ::  (Antiunifiable k v t) => (VarMap k v) -> [t] -> LM t
-        antiunify2,        -- :: (Antiunifiable k v t') => [[t]] -> [t'] -> LM ([t],t')
-        aunify
-      ),
-    computeAntiInstance, checkforAntiInstance,updateVarTable
-      
+    AU, getMap, incrCnt, getCnt, putImg,
+    AUnify(aunify, lgg),
+    lggL, -- aunify2,
+   
+    roots, sameRoots,
+--    Antiunifiable (
+--        antiunify,        -- :: (Antiunifiable k v t) => [t] -> t
+--        antiunifyWithMap, -- ::  (Antiunifiable k v t) => (VarMap k v) -> [t] -> LM t
+--        antiunify2,        -- :: (Antiunifiable k v t') => [[t]] -> [t'] -> LM ([t],t')
+--        aunify
+--      ),
+--    computeAntiInstance, checkforAntiInstance,updateVarTable
+--      
hunk ./src/Syntax/Class/Antiunifier.hs 24
-import qualified Data.Map as M
hunk ./src/Syntax/Class/Antiunifier.hs 25
-import Control.Monad.State (get, runStateT, put)
+import Syntax.Class.Term
+import Syntax.Context
+
+import Control.Monad.State 
+import Control.Monad.Error
+
+import qualified Data.Map as M
hunk ./src/Syntax/Class/Antiunifier.hs 34
-import Syntax.Terms
-import Logging
hunk ./src/Syntax/Class/Antiunifier.hs 35
+import PrettyPrinter
+import Debug.Trace
hunk ./src/Syntax/Class/Antiunifier.hs 38
-{- | 
-     This is a many-to-one mapping to model generalisation from many terms to a 
-     variable (here its name). 
--}
-type VarMap t = (M.Map [t] Name)
+data (Pretty t) => VIMap t = VI { unVI :: (Int,[([t],t)]) } deriving (Show)
hunk ./src/Syntax/Class/Antiunifier.hs 40
-{- | 
-     The 'AU t' monad which is required for antiunification. It is just a state 
-     monad 'StateT' to keep track of the replacements in a 'VarMap t'. The type 
-     parameter is the type of term 't' to antiunify. The value is wrapped into 
-     the 'Identity' monad to be felxible enought to allow for extensions for 
-     probable logging, error handling, etc. later
--}
-type AU m t = StateT (VarMap t) m t
+instance (Pretty t) => Pretty (VIMap t) where
+    pretty (VI (i,l)) = text "VIMAP" <$> int i <$> vsep (map pretty l)
+ 
+emptyVIMap :: (Pretty t) => VIMap t 
+emptyVIMap = VI (0,[])  
hunk ./src/Syntax/Class/Antiunifier.hs 46
--- Shotcut to evaluate the 'AU' monad, yielding the result value
-evalAU :: (Monad m) => StateT s m a -> s -> m a
-evalAU = evalStateT
+type AU m t = StateT (VIMap t) (C m)
hunk ./src/Syntax/Class/Antiunifier.hs 48
--- Shortcut to evaluate the 'AU' monad, yielding the result value and the result 
--- state
-runAU :: (Monad m) => StateT s m a -> s -> m (a, s)
-runAU  = runStateT
+getMap :: (MonadError e m, Pretty t) => AU m t [([t],t)]
+getMap = gets $ snd . unVI
hunk ./src/Syntax/Class/Antiunifier.hs 51
---------------------------------------------------------------------------------
--- The Antiunifiable class definition  
---------------------------------------------------------------------------------
-{-|
-    The class 'Antiunifiable' defines the antiunifcation in a quite general 
-    way. It generalises a list of types 't' into a single term of the same type,
-    probably intorducing variables. Different subterms are hereby always 
-    replaced with the same variable if antiunified twice. This mapping is called
-    the /image of a variable/.For example:
-    
-    >   tail (1:xs)   = xs
-    >   tail (1:2:xs) = (2:xs)
-    
-    would yield
-    
-    >   tail (1:x1) = x1
-    
-    with image [[xs, 2:xs] ~> x1], whereas the anti-instance of
-    
-    >   last (1:[]) = 1
-    >   last (1:xs) = last xs
-    
-    is
-    
-    >   last (1:x1) = x2
-    
-    with image [ [[], xs] ~> x1, [1,last xs] ~> x2 ].
-        
--}      
-class (Term t) => Antiunifiable t where
-    -- | Computes the anti-instance 't' of all terms in '[t]'
-    antiunify        :: (Monad m) => [t] -> m t
-    antiunify         = (\t -> evalAU (aunify t) M.empty)
-        
-    -- | The actual state transforming function, doing the anti-unification and 
-    --   keeping track of the variables in the state.
-    aunify           :: (Antiunifiable t, Monad m) => [t] -> AU m t
+getCnt :: (MonadError e m, Pretty t) =>  AU m t Int
+getCnt = gets $ fst . unVI
+
+incrCnt ::  (MonadError e m, Pretty t) => AU m t ()
+incrCnt = do (VI (c,m)) <- get; put $ VI (c+1,m)
hunk ./src/Syntax/Class/Antiunifier.hs 57
--- DEAD CODE       
-    -- | Same as 'antiunify' but uses a 'VarMap' as initial state
-    antiunifyWithMap ::  (Antiunifiable t, Monad m) => (VarMap t) -> [t] -> m t
-    antiunifyWithMap  = (\m t -> evalAU (aunify t) m)
+putImg ::  (MonadError e m, Pretty t) => t -> [t] -> AU m t ()
+putImg t i = do (VI (c,m)) <- get; put (VI (c,(i,t):m)); incrCnt
+
+class AUnify t where
+    aunify :: (MonadError e m) => [t] -> AU m t t
+   
+    lgg :: (MonadError e m, Pretty t) =>  [t] -> C m t
+    lgg  ts = evalStateT (aunify ts) emptyVIMap
hunk ./src/Syntax/Class/Antiunifier.hs 66
--- DEAD CODE    
---    {- | Convenience function to antiunify different kind of terms, but keeping 
---         track of the VarMap. @antiunify2 t1 t2@ corresponds approcimately to 
---         @liftM2 (,) (mapM antiunify t1) (antiunify t2)@, where the latter 
---         antiunify uses the VarMap of the further. 
---         This is needed to antiunify all patterns on the lhs and the rhs of 
---         multiple rules.
---    -}
-    antiunify2        :: (Ord t', Antiunifiable t', Antiunifiable t, Monad m) 
-                      => [[t]] -> [t'] -> (t -> t') -> m ([t],t')
-    antiunify2 ts ts' trans = do
-            (ait,varmap) <- runAU ((mapM aunify) ts) M.empty
-            ait'         <- antiunifyWithMap (M.mapKeys (map trans) varmap) ts'
-            return (ait,ait')   
hunk ./src/Syntax/Class/Antiunifier.hs 67
---------------------------------------------------------------------------------
--- The Antiunifiable instance declarations
---------------------------------------------------------------------------------
-{- |
-  This is more or less for convenience and aunify simply calls 'antiunify' with 
-  the clauses list as argument. All other functions are undefined and yield in 
-  a 'fail'. 
+
+lggL :: (Pretty t, AUnify t, MonadError e m) => [[t]] -> C m [t]
+lggL ls = do (r,s) <- runStateT (mapM aunify ls)  emptyVIMap
+             return $ (trace $ "AUNIL" ++ "\n " ++ (show $ pretty $ ls) ++ "\n " ++ (show $ pretty $ r)  ++ "\n " ++ (show $ pretty $  s) ) r
hunk ./src/Syntax/Class/Antiunifier.hs 72
-  TODO: good coding style??? NO, Dec, body etc are not terms!!
+                        
+roots :: (Term t) => [t] -> ([t] -> t)
+roots = root . head 
hunk ./src/Syntax/Class/Antiunifier.hs 76
--}    
---instance Antiunifiable Exp Exp Dec where    
---    toKey                      = 
---        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
---                   "function definitions!"
---    fromVal  = 
---        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
---               "function definitions!"
---    mkVar                      = 
---        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
---               "function definitions!"
---    aunify [FunD name clauses] = 
---        do ai_clauses <- lift $ antiunify clauses
---           return $ FunD name [ai_clauses]
---    aunify [] = 
---        fail $ "Antiunifier.aunify: empty list of Dec, no terms to antiunify"
---    aunify (_:_)               =
---        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
---                "function definitions!"
+sameRoots :: (Term t) => [t] -> Bool
+sameRoots []  = error "sameRoot: empty List"
+sameRoots [x] = True
+sameRoots (x1:x2:xs) = (&&) (sameSymAtRoot x1 x2) $! sameRoots (x2:xs)                
+--    
+--bindVar :: VImg -> AU Type
+--bindVar img =  getMap >>= (maybe (mkVar img) (return)) . (lookup img)
+--     
+--mkVar :: VImg -> AU Type
+--mkVar vimg = do 
+--    vnm <- getCnt >>= return . ('a':) . show
+--    cxt <- lift $ cmpCxt vnm vimg
+--    var <- return . (flip quantify cxt)  . mkVarT $ vnm
+--    putImg var vimg
+--    return var
+--      
+--cmpCxt :: String -> VImg -> C TyCxt
+--cmpCxt vnm vimg = do 
+--    insts <- allInstances
+--    nms   <- mapM (collectPreds vnm insts) vimg
+--    reduce . (foldl1 intersect) $ nms
+--    
+--collectPreds :: String -> [(Name,[Type])] -> Type -> C [Pred] 
+--collectPreds vnm is (ForallT _ c (VarT _)) = mapM (\(AppT (ConT n) _) -> bySuper $ mkPred n vnm) c >>= return . concat 
+--collectPreds vnm is (VarT _) = return . map ((flip mkPred vnm) . fst) $ is 
+--collectPreds vnm is t =    
+--    filterM ( (anyM (`matches` t)) . snd ) is >>=
+--    return . map ((flip mkPred vnm) . fst)
hunk ./src/Syntax/Class/Antiunifier.hs 105
---{-
---   The result state of anitunifying the patterns is passed to the 
---   antiunification of the expression on the right-hand side. This is necessary 
---   because the same terms may occur both on the lhs and on the rhs, here as 
---   patterns 'Pat' there as expressions 'Exp'.
+--lgg :: [Type] -> C (Maybe Type)
+--lgg ts = ( evalStateT (aunify ts) emptyVIMap >>= return . Just ) 
+--            `catchError` \_ -> return Nothing
hunk ./src/Syntax/Class/Antiunifier.hs 109
---   Same as with 'Antiunifiable Exp Exp Dec', all other functions yield a 
---   'fail'.   
---    
----}        
---instance Antiunifiable Exp Exp Clause where 
---    toKey = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Clause!"
---    fromVal = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Clause!"
---    mkVar = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Clause!"
---                
---    {- If all elements in the provided list are 'Clauses's the result is just 
---       a tuple with their patterns 'pat' i.e. a list of patern lists, their 
---       'bodies' and their declarations 'dec', 'Nothing' otherwise.
---       To antiunify the patterns we transpose the pattern list, to antiunify
---       all nth pattern of the clauses. 
---       We don't care about the 'dec' so we just put them all together. 
---       After antiunifying all patterns we pss the result state to the 
---       antiunification of the expressions.
---    -}
---    aunify l@((Clause _ _ _):xs)  =
---        case collectSubtermsC  l of
---            Just (pats,bodies,decs) -> 
---                do let tpats   = transpose pats
---                   let alldecs = concat decs
---                   (ai_pats,varmap) <- lift $ runAU ((mapM aunify) tpats) M.empty
---                   ai_bodies <- lift $ antiunifyWithMap varmap bodies
---                   return $ Clause ai_pats ai_bodies alldecs
---            Nothing   ->  
---                fail "Antiunifier.aunify: Cannot generalise over arbitrary clauses!"
---  
---  
+--hRoot :: (Term t) => [t] -> ([t] -> t)
+--hRoot = root . head 
hunk ./src/Syntax/Class/Antiunifier.hs 112
---                
---{-|
---  Same as in the previous instance declarations. Here the state of antiunifying 
---  'Body's is simply passed to antiunifying 'Exp's.
----}                
---instance Antiunifiable Exp Exp Body where  
---    toKey (NormalB e)         = e
---    fromVal e                 = (NormalB e)
---    mkVar                     = (\_d i -> VarE $ mkName $ "x" ++ (show i))
---    
---    {-|
---       Same as above. Collect subterms, and antiunify them with the current 
---       state.
---    -}
---    aunify l@((NormalB _):xs) =
---        case collectSubtermsB l computeAntiInstance lof
---            Just subterms -> 
---                do varmap <- get 
---                   ai_exps <- lift $ antiunifyWithMap varmap  subterms
---                   return $ NormalB ai_exps
---            Nothing       -> 
---                computeAntiInstance l
---    aunify [] = fail "Antiunifier.aunify: empty list, no terms to antiunify"
---    aunify (x:_) = 
---        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
---                "of Type Body is not implemented!"
---                
---instance Antiunifiable Exp Exp Rule where 
---    toKey = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Rule!"
---    fromVal = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Rule!"
---    mkVar = 
---        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
---                "number of patterns in Rule!"
---       
---    aunify rules  = do
---        let tlhss   = transpose $ map lhs rules
---        let rhss    = map rhs rules
---        (ailhs,varmap) <- lift $ runAU ((mapM aunify) tlhss) M.empty
---        airhs         <- lift $ antiunifyWithMap varmap rhss
---        return $ rule ailhs airhs                
-   
- 
-   
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Body 
--------------------------------------------------------------------------------}  
+--sameRoot :: (Term t) => [Type] -> Bool
+--sameRoot []  = error "sameRoot: empty List"
+--sameRoot [x] = True
+--sameRoot (x1:x2:xs) = (&&) (sameSymAtRoot x1 x2) $! sameRoot (x2:xs)
+-- 
hunk ./src/Syntax/Class/Antiunifier.hs 118
-{-|
-  See 'collectSubtermsE'
--}
-collectSubtermsB l = sequence $ map collector l 
-    where
-    collector = case head l of 
-        (NormalB _)      -> collectSubtermsNormalB
-    collectSubtermsNormalB (NormalB expr)      = Just expr
-    collectSubtermsNormalB _                   = Nothing
hunk ./src/Syntax/Class/Antiunifier.hs 119
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Clause 
--------------------------------------------------------------------------------}  
hunk ./src/Syntax/Class/Antiunifier.hs 120
-{-|
-  See 'collectSubtermsE'
--}
-collectSubtermsC l = liftM unzip3 $ sequence $ map collector $ l 
-    where
-    collector = case head l of 
-        (Clause pats _ _ ) -> collectSubtermsClause (length pats)
-    collectSubtermsClause l (Clause ps b ds) = 
-        if (length ps) == l
-           then Just (ps,b,ds)
-           else  Nothing
hunk ./src/Syntax/Class/Antiunifier.hs 121
-{-------------------------------------------------------------------------------
-  General Auxiliary Functions for Antiunification 
--------------------------------------------------------------------------------} 
hunk ./src/Syntax/Class/Antiunifier.hs 122
-{-|
-  Checks if in the provided list all terms are equal. If so, the first element 
-  is returned, otherwise a variable.
--}            
-checkforAntiInstance :: (Ord t, Antiunifiable t, Monad m) => [t] -> AU m t
--- checkforAntiInstance [x] = return x -- is implied when condition below is True
-checkforAntiInstance l@(x:xs) =   
-    if (all (== x) l) && not (any isWild l || all isVar l)
-    -- all terms are equal, but they are not all variables or one is a wildcard
-       then return x 
-       else computeAntiInstance l
-       -- If all terms are wildcards or variables, they are anti-unified 
-       -- nevertheless. This is necessary to bind wildcards by a variable in the
-       -- pattern, so also images with the same variable must occur in the 
-       -- table. Thus variables are renamed. 
-       -- Even, iff all are wildcards, there should never be a new and unbound 
-       -- variable introduced for them, because there should always be some 
-       -- pattern which binds the wildcard. Hopefully! 
hunk ./src/Syntax/Class/Antiunifier.hs 123
-{-|
-   Computes the anti-instance for a list of expressions. It is assumed that the 
-   expressions do not anti-unify, so the result is simply a variable. This is 
-   either a fresh variable if the image of the provided terms does not yet 
-   exists in the the Monad 'AU' or it just returns the previously generated 
-   variable.
--}       
-computeAntiInstance :: (Ord t, Antiunifiable t, Monad m) => [t] -> AU m t
-computeAntiInstance l@(x:xs) =  do 
---    lift (setCurrentLogger "Terms.Antiunifier.computeAntiInstance")
---    llogEnterDE
---    llogDE $ text "Term Image is:" <> pretty l
-    table <- get
---    llogDE $ text "Current varTable is:" <> pretty table
---    llogDE $ text "isIn?" <+> (pretty $ M.member l table)
---    llogDE $ text "isIn?" <+> (pretty $ lookup l (M.toList table))
---    llogDE $ text "map (==)?" <+> (pretty $ map (\ll -> l ==(fst ll)) (M.toList table))
-    (newTable, var) <- return $ updateVarTable table l
---    llogDE $ text "update varTable with var:" <> pretty var
---    llogDE $ text "Updated varTable is:" <> pretty newTable
-    put newTable
-    return var
hunk ./src/Syntax/Class/Antiunifier.hs 124
-{-|
-  If the provided list of terms does not yet exists in the variable table of the
-  'AU' Monad a fresh variable is generated and the variable table is updated.  
-  Otherwise, the previously generated variable is returned.
--}              
-updateVarTable :: (Ord t, Antiunifiable t) => (VarMap t) -> [t] -> ((VarMap t) , t)
-updateVarTable table img = 
-    case lookup img (M.toList table) of
-    -- This is a hack!! Damn! Wildcards equal everything, this messes up the 
-    -- retrieval! So I look up in the list, which is searched linear.
-        (Just v)    -> (table, toVar (head img) v)
-        Nothing     -> let name   = mkName ("x" ++ (show $ toInteger(M.size table)))
-                           newval = toVar (head img) name
-                       in (M.insert img name table , newval)
hunk ./src/Syntax/Class/Antiunifier.hs 125
-                                  
-   
+
+
+
+
+
+
+---------------------------------------------------------------------
+---------------------------------------------------------------------
+--------------------------------------------------------------------
+
+---------------------------------------------------------------------
+---------------------------------------------------------------------
+--------------------------------------------------------------------
+
+--
+--{- | 
+--     This is a many-to-one mapping to model generalisation from many terms to a 
+--     variable (here its name). 
+---}
+--type VarMap t = (M.Map [t] Name)
+--
+--{- | 
+--     The 'AU t' monad which is required for antiunification. It is just a state 
+--     monad 'StateT' to keep track of the replacements in a 'VarMap t'. The type 
+--     parameter is the type of term 't' to antiunify. The value is wrapped into 
+--     the 'Identity' monad to be felxible enought to allow for extensions for 
+--     probable logging, error handling, etc. later
+---}
+--type AU m t = StateT (VarMap t) m t
+--
+---- Shotcut to evaluate the 'AU' monad, yielding the result value
+--evalAU :: (Monad m) => StateT s m a -> s -> m a
+--evalAU = evalStateT
+--
+---- Shortcut to evaluate the 'AU' monad, yielding the result value and the result 
+---- state
+--runAU :: (Monad m) => StateT s m a -> s -> m (a, s)
+--runAU  = runStateT
+--
+----------------------------------------------------------------------------------
+---- The Antiunifiable class definition  
+----------------------------------------------------------------------------------
+--{-|
+--    The class 'Antiunifiable' defines the antiunifcation in a quite general 
+--    way. It generalises a list of types 't' into a single term of the same type,
+--    probably intorducing variables. Different subterms are hereby always 
+--    replaced with the same variable if antiunified twice. This mapping is called
+--    the /image of a variable/.For example:
+--    
+--    >   tail (1:xs)   = xs
+--    >   tail (1:2:xs) = (2:xs)
+--    
+--    would yield
+--    
+--    >   tail (1:x1) = x1
+--    
+--    with image [[xs, 2:xs] ~> x1], whereas the anti-instance of
+--    
+--    >   last (1:[]) = 1
+--    >   last (1:xs) = last xs
+--    
+--    is
+--    
+--    >   last (1:x1) = x2
+--    
+--    with image [ [[], xs] ~> x1, [1,last xs] ~> x2 ].
+--        
+---}      
+--class (Term t) => Antiunifiable t where
+--    -- | Computes the anti-instance 't' of all terms in '[t]'
+--    antiunify        :: (Monad m) => [t] -> m t
+--    antiunify         = (\t -> evalAU (aunify t) M.empty)
+--        
+--    -- | The actual state transforming function, doing the anti-unification and 
+--    --   keeping track of the variables in the state.
+--    aunify           :: (Antiunifiable t, Monad m) => [t] -> AU m t
+--
+---- DEAD CODE       
+--    -- | Same as 'antiunify' but uses a 'VarMap' as initial state
+--    antiunifyWithMap ::  (Antiunifiable t, Monad m) => (VarMap t) -> [t] -> m t
+--    antiunifyWithMap  = (\m t -> evalAU (aunify t) m)
+--    
+---- DEAD CODE    
+----    {- | Convenience function to antiunify different kind of terms, but keeping 
+----         track of the VarMap. @antiunify2 t1 t2@ corresponds approcimately to 
+----         @liftM2 (,) (mapM antiunify t1) (antiunify t2)@, where the latter 
+----         antiunify uses the VarMap of the further. 
+----         This is needed to antiunify all patterns on the lhs and the rhs of 
+----         multiple rules.
+----    -}
+--    antiunify2        :: (Ord t', Antiunifiable t', Antiunifiable t, Monad m) 
+--                      => [[t]] -> [t'] -> (t -> t') -> m ([t],t')
+--    antiunify2 ts ts' trans = do
+--            (ait,varmap) <- runAU ((mapM aunify) ts) M.empty
+--            ait'         <- antiunifyWithMap (M.mapKeys (map trans) varmap) ts'
+--            return (ait,ait')   
+--
+----------------------------------------------------------------------------------
+---- The Antiunifiable instance declarations
+----------------------------------------------------------------------------------
+--{- |
+--  This is more or less for convenience and aunify simply calls 'antiunify' with 
+--  the clauses list as argument. All other functions are undefined and yield in 
+--  a 'fail'. 
+--  
+--  TODO: good coding style??? NO, Dec, body etc are not terms!!
+--
+---}    
+----instance Antiunifiable Exp Exp Dec where    
+----    toKey                      = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+----                   "function definitions!"
+----    fromVal  = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+----               "function definitions!"
+----    mkVar                      = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+----               "function definitions!"
+----    aunify [FunD name clauses] = 
+----        do ai_clauses <- lift $ antiunify clauses
+----           return $ FunD name [ai_clauses]
+----    aunify [] = 
+----        fail $ "Antiunifier.aunify: empty list of Dec, no terms to antiunify"
+----    aunify (_:_)               =
+----        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+----                "function definitions!"
+----
+----{-
+----   The result state of anitunifying the patterns is passed to the 
+----   antiunification of the expression on the right-hand side. This is necessary 
+----   because the same terms may occur both on the lhs and on the rhs, here as 
+----   patterns 'Pat' there as expressions 'Exp'.
+----   
+----   Same as with 'Antiunifiable Exp Exp Dec', all other functions yield a 
+----   'fail'.   
+----    
+-----}        
+----instance Antiunifiable Exp Exp Clause where 
+----    toKey = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Clause!"
+----    fromVal = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Clause!"
+----    mkVar = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Clause!"
+----                
+----    {- If all elements in the provided list are 'Clauses's the result is just 
+----       a tuple with their patterns 'pat' i.e. a list of patern lists, their 
+----       'bodies' and their declarations 'dec', 'Nothing' otherwise.
+----       To antiunify the patterns we transpose the pattern list, to antiunify
+----       all nth pattern of the clauses. 
+----       We don't care about the 'dec' so we just put them all together. 
+----       After antiunifying all patterns we pss the result state to the 
+----       antiunification of the expressions.
+----    -}
+----    aunify l@((Clause _ _ _):xs)  =
+----        case collectSubtermsC  l of
+----            Just (pats,bodies,decs) -> 
+----                do let tpats   = transpose pats
+----                   let alldecs = concat decs
+----                   (ai_pats,varmap) <- lift $ runAU ((mapM aunify) tpats) M.empty
+----                   ai_bodies <- lift $ antiunifyWithMap varmap bodies
+----                   return $ Clause ai_pats ai_bodies alldecs
+----            Nothing   ->  
+----                fail "Antiunifier.aunify: Cannot generalise over arbitrary clauses!"
+----  
+----  
+----
+----                
+----{-|
+----  Same as in the previous instance declarations. Here the state of antiunifying 
+----  'Body's is simply passed to antiunifying 'Exp's.
+-----}                
+----instance Antiunifiable Exp Exp Body where  
+----    toKey (NormalB e)         = e
+----    fromVal e                 = (NormalB e)
+----    mkVar                     = (\_d i -> VarE $ mkName $ "x" ++ (show i))
+----    
+----    {-|
+----       Same as above. Collect subterms, and antiunify them with the current 
+----       state.
+----    -}
+----    aunify l@((NormalB _):xs) =
+----        case collectSubtermsB l computeAntiInstance lof
+----            Just subterms -> 
+----                do varmap <- get 
+----                   ai_exps <- lift $ antiunifyWithMap varmap  subterms
+----                   return $ NormalB ai_exps
+----            Nothing       -> 
+----                computeAntiInstance l
+----    aunify [] = fail "Antiunifier.aunify: empty list, no terms to antiunify"
+----    aunify (x:_) = 
+----        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+----                "of Type Body is not implemented!"
+----                
+----instance Antiunifiable Exp Exp Rule where 
+----    toKey = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Rule!"
+----    fromVal = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Rule!"
+----    mkVar = 
+----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+----                "number of patterns in Rule!"
+----       
+----    aunify rules  = do
+----        let tlhss   = transpose $ map lhs rules
+----        let rhss    = map rhs rules
+----        (ailhs,varmap) <- lift $ runAU ((mapM aunify) tlhss) M.empty
+----        airhs         <- lift $ antiunifyWithMap varmap rhss
+----        return $ rule ailhs airhs                
+--   
+-- 
+--   
+--{-------------------------------------------------------------------------------
+--  Auxiliary Functions for antiunifying expressions of type Body 
+---------------------------------------------------------------------------------}  
+--
+--{-|
+--  See 'collectSubtermsE'
+---}
+--collectSubtermsB l = sequence $ map collector l 
+--    where
+--    collector = case head l of 
+--        (NormalB _)      -> collectSubtermsNormalB
+--    collectSubtermsNormalB (NormalB expr)      = Just expr
+--    collectSubtermsNormalB _                   = Nothing
+--
+--{-------------------------------------------------------------------------------
+--  Auxiliary Functions for antiunifying expressions of type Clause 
+---------------------------------------------------------------------------------}  
+--
+--{-|
+--  See 'collectSubtermsE'
+---}
+--collectSubtermsC l = liftM unzip3 $ sequence $ map collector $ l 
+--    where
+--    collector = case head l of 
+--        (Clause pats _ _ ) -> collectSubtermsClause (length pats)
+--    collectSubtermsClause l (Clause ps b ds) = 
+--        if (length ps) == l
+--           then Just (ps,b,ds)
+--           else  Nothing
+--
+--{-------------------------------------------------------------------------------
+--  General Auxiliary Functions for Antiunification 
+---------------------------------------------------------------------------------} 
+--
+--{-|
+--  Checks if in the provided list all terms are equal. If so, the first element 
+--  is returned, otherwise a variable.
+---}            
+--checkforAntiInstance :: (Ord t, Antiunifiable t, Monad m) => [t] -> AU m t
+---- checkforAntiInstance [x] = return x -- is implied when condition below is True
+--checkforAntiInstance l@(x:xs) =   
+--    if (all (== x) l) && not (any isWild l || all isVar l)
+--    -- all terms are equal, but they are not all variables or one is a wildcard
+--       then return x 
+--       else computeAntiInstance l
+--       -- If all terms are wildcards or variables, they are anti-unified 
+--       -- nevertheless. This is necessary to bind wildcards by a variable in the
+--       -- pattern, so also images with the same variable must occur in the 
+--       -- table. Thus variables are renamed. 
+--       -- Even, iff all are wildcards, there should never be a new and unbound 
+--       -- variable introduced for them, because there should always be some 
+--       -- pattern which binds the wildcard. Hopefully! 
+--
+--{-|
+--   Computes the anti-instance for a list of expressions. It is assumed that the 
+--   expressions do not anti-unify, so the result is simply a variable. This is 
+--   either a fresh variable if the image of the provided terms does not yet 
+--   exists in the the Monad 'AU' or it just returns the previously generated 
+--   variable.
+---}       
+--computeAntiInstance :: (Ord t, Antiunifiable t, Monad m) => [t] -> AU m t
+--computeAntiInstance l@(x:xs) =  do 
+----    lift (setCurrentLogger "Terms.Antiunifier.computeAntiInstance")
+----    llogEnterDE
+----    llogDE $ text "Term Image is:" <> pretty l
+--    table <- get
+----    llogDE $ text "Current varTable is:" <> pretty table
+----    llogDE $ text "isIn?" <+> (pretty $ M.member l table)
+----    llogDE $ text "isIn?" <+> (pretty $ lookup l (M.toList table))
+----    llogDE $ text "map (==)?" <+> (pretty $ map (\ll -> l ==(fst ll)) (M.toList table))
+--    (newTable, var) <- return $ updateVarTable table l
+----    llogDE $ text "update varTable with var:" <> pretty var
+----    llogDE $ text "Updated varTable is:" <> pretty newTable
+--    put newTable
+--    return var
+--
+--{-|
+--  If the provided list of terms does not yet exists in the variable table of the
+--  'AU' Monad a fresh variable is generated and the variable table is updated.  
+--  Otherwise, the previously generated variable is returned.
+---}              
+--updateVarTable :: (Ord t, Antiunifiable t) => (VarMap t) -> [t] -> ((VarMap t) , t)
+--updateVarTable table img = 
+--    case lookup img (M.toList table) of
+--    -- This is a hack!! Damn! Wildcards equal everything, this messes up the 
+--    -- retrieval! So I look up in the list, which is searched linear.
+--        (Just v)    -> (table, toVar (head img) v)
+--        Nothing     -> let name   = mkName ("x" ++ (show $ toInteger(M.size table)))
+--                           newval = toVar (head img) name
+--                       in (M.insert img name table , newval)
+--
+--                                  
+--   
addfile ./src/Syntax/Class/Subst.hs
hunk ./src/Syntax/Class/Subst.hs 1
-
+
+-- | Term substitutions, application of substitutions to terms, and 
+--   modifications of substitutions.
+module Syntax.Class.Subst (
+    -- * The class
+    Substitutable(..),
+    
+    -- * The data type 
+    -- ** Definition 
+    Subst,
+    -- ** Constructors
+    nullSubst, (<~),
+    
+    -- * Functions over substitutions
+    (@@), merge,
+    
+
+) where
+
+import Syntax.Class.Term
+import Syntax.IFTemplateHaskell (Name)
+
+import Data.List (nub, intersect, union)
+import Data.Function (on)
+
+-- | The class of all subtitutables
+class (Term t) => Substitutable t where
+  -- | applies a subtituion to a term
+  apply :: (Subst t) -> t -> t
+  
+  applyL :: (Subst t) -> [t] -> [t]
+  applyL s = map (apply s)
+  
+-- | Associating 'Term's with variable 'Name's as a list of replacements
+type Subst t = [(Name,t)]
+
+-- | The empty Substitution
+nullSubst  :: (Substitutable t) => (Subst t)
+nullSubst   = []
+
+-- | Constructing a substitution from a single replacement 
+(<~)      :: (Substitutable t) => Name -> t -> (Subst t)
+n <~ t     = [(n, t)]
+
+
+infixr 4 @@
+-- | Composing substitutions 's1' and 's2', s.t.  
+--        @ apply s1 .apply s2 == apply (s1 @@ s2) @
+(@@)       :: (Substitutable t) => (Subst t) -> (Subst t) -> (Subst t)
+s1 @@ s2    = [ (n, apply s1 t) | (n,t) <- s2 ] ++ s1
+
+
+-- | Parallel composition of substitutions, which checks that the two 
+--   substitutions agree  at every variable in the domain of both, thus
+--   guarantees that @ apply (merge s1 s2) = apply (merge s2 s1)@.
+merge      :: (Substitutable t,Monad m) => (Subst t) -> (Subst t) -> m (Subst t)
+merge s1 s2 = if agree then return (s1++s2) else fail "merge fails"
+    where 
+    agree = all (\v -> apply s1 (var v) == apply s2 (var v))
+                   (on intersect (map fst) s1 s2)
+    var = toVar . snd . head $ s1 
+ 
hunk ./src/Syntax/Class/Term.hs 2
-module Syntax.Terms (
+module Syntax.Class.Term (
hunk ./src/Syntax/Class/Term.hs 9
-    Hole(..),
+--    Hole(..),
hunk ./src/Syntax/Class/Term.hs 20
-    isTuple, isNil, isCons
+    
hunk ./src/Syntax/Class/Term.hs 27
-import Control.Monad
hunk ./src/Syntax/Class/Term.hs 28
+import Control.Monad
hunk ./src/Syntax/Class/Term.hs 30
-import Logging
+import PrettyPrinter
hunk ./src/Syntax/Class/Term.hs 54
--- | @isSubPos p1 p2 == Trueq iff there is a direct path downwards in the term 
+-- | @isSubPos p1 p2 == True@ iff there is a direct path downwards in the term 
hunk ./src/Syntax/Class/Term.hs 60
--- | Data type for holes in terms
-data Hole = Hole
+---- | Data type for holes in terms
+--data Hole = Hole
hunk ./src/Syntax/Class/Term.hs 113
+    -- | semantical equivalence of terms, may take different syntactic representations
+    --   of semantically equivalent terms in account. Eg. infix vs prefix
+    equal :: t -> t -> Bool
+    
hunk ./src/Syntax/Class/Term.hs 254
-isTuple :: Name -> Int -> Bool
-isTuple n i
-    | i == 2  = n == '(,)
-    | i == 3  = n == '(,,)
-    | i == 4  = n == '(,,,)
-    | i == 5  = n == '(,,,,)
-    | i == 6  = n == '(,,,,,)
-    | i == 7  = n == '(,,,,,,)
-    | i == 8  = n == '(,,,,,,,)
-    | i == 9  = n == '(,,,,,,,,)
-    | i == 10  = n == '(,,,,,,,,,)
-    | i == 11  = n == '(,,,,,,,,,,)
-    | i == 12  = n == '(,,,,,,,,,,,)
-    | i == 13  = n == '(,,,,,,,,,,,,)
-    | i == 14  = n == '(,,,,,,,,,,,,,)
-    | i == 15  = n == '(,,,,,,,,,,,,,,)
-    
-isNil :: Name -> Bool
-isNil = (==) '[]
-
-isCons :: Name -> Bool
-isCons = (==) '(:)
-   
hunk ./src/Syntax/Class/Unifier.hs 2
-module Syntax.Unifier
+module Syntax.Class.Unifier
hunk ./src/Syntax/Class/Unifier.hs 4
-    U,
-    Substitutable(..),
-    Substitution, Replacement, nullSubst, (<~), insertApply,
-    Unifiable(mgu, unify, match, matchesWithSubs),
-    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, 
-    matchesWithSubsLs,
-    matchVar, flush,
-    
-    
-    zipPairsWithM, 
+    Unify(..)
+--    U,
+--    Substitutable(..),
+--    Substitution, Replacement, nullSubst, (<~), insertApply,
+--    Unifiable(mgu, unify, match, matchesWithSubs),
+--    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, 
+--    matchesWithSubsLs,
+--    matchVar, flush,
+--    
+--    
+--    zipPairsWithM,
hunk ./src/Syntax/Class/Unifier.hs 31
-import Syntax.Terms 
- 
-type U m a = StateT (Substitution a) m ()
-
+import PrettyPrinter
hunk ./src/Syntax/Class/Unifier.hs 33
-infixr 0 <~
-(<~) :: (Term a, Term b ) => a -> b -> (a, b)
-(<~) = (,)  
+import Syntax.Context
+import Syntax.Class.Term
+import Syntax.Class.Subst
hunk ./src/Syntax/Class/Unifier.hs 37
--- | 'a <~ b' denotes the replacement of 'a' by 'b' where usually 'a' is a 
---   variable and 'b' is a term
-type Replacement a = (a,a)
-   
-type Substitution t = [Replacement t]
hunk ./src/Syntax/Class/Unifier.hs 38
-nullSubst :: Substitution t
-nullSubst = []
hunk ./src/Syntax/Class/Unifier.hs 39
-insertApply :: (Eq a, Term a) =>  (Replacement a) -> (Substitution a) -> (Substitution a)
-insertApply s [] = [s]
-insertApply s@(x,v) (u@(y,w):us) 
-    | (w == x) && (y == v) = (insertApply s us)
-    | w == x               = (y <~ v):(insertApply s us)
-    | otherwise            =  u:(insertApply s us)
-
---infixr 4 @@
---(@@) :: (Substitutable a) => (Substitution a) -> (Substitution a) -> LM (Substitution a)
---s1 @@ s2 = liftM (++s1) $ sequence [liftM  (\v -> (u, v)) (apply s1 t) | (u,t) <- s2]
---
-class Substitutable a where
-    -- applys a substitution to a term. May fail inside LM when an type mismatch
-    -- occurs.
-    apply :: (Monad m) => (Substitution a) -> a -> m a
-    
-    applyL :: (Substitutable a, Monad m) => (Substitution a) -> [a] -> m [a]
-    applyL s = mapM (apply s)
hunk ./src/Syntax/Class/Unifier.hs 40
-  
-class (Term t, Ord t, Show t, Pretty t) => Unifiable t where
-    
-    
-    unify ::  (MonadPlus m) => t -> t -> U m t
-    
-    mgu ::  (MonadPlus m) => t -> t -> m (Substitution t)
-    mgu x y = 
-              -- Logging stuff
---              setCurrentLogger "Terms.Unifier.mgu" >>
---              logDE (text "Unifying terms:" <+> pretty x <+> pretty y) >> 
-              -- 
-              execStateT (unify x y) []
-    
-    --applyMgu :: (Substitution t) -> t -> LM t    
+class (Term t, Substitutable t) => Unify t where
hunk ./src/Syntax/Class/Unifier.hs 42
+                    
hunk ./src/Syntax/Class/Unifier.hs 47
-    match :: (MonadPlus m) =>  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.
-    matchesWithSubs :: (MonadPlus m) =>  t -> t -> m (Substitution t)  
-    matchesWithSubs x y = execStateT (match 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
-
---     
---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 
-
-
-     
-matchVar :: (Unifiable t, MonadPlus m) => t -> t -> U m t
-matchVar t var = 
-    do unifier <- get  
-       case (lookup var unifier) of
-        Just val -> 
---            llogDE ( text "Found (Var <~ Val) in current unifier:" <^>
---                     pretty var <+> text " <~ " <+> pretty val <$>
---                     text "but need to match:" <^>
---                     pretty var <+> text " <~ " <+> pretty t
---                   ) >>
-            if (val == t) then return () else flush "matchVar: No Match!"
-        Nothing  -> put (insert (var <~ t) unifier)
+    match :: (MonadError e m) => t -> t -> C m (Subst t) 
hunk ./src/Syntax/Class/Unifier.hs 49
-         
-unifyVar :: (Unifiable t, MonadPlus m) => t -> t -> U m t
-unifyVar var x = 
-    do unifier <- get  
---       lift $ setCurrentLogger "Terms.Unifier.unifyVar"
---       llogEnterDE
---       llogDE ( text "Var is:" <^> (pretty var) <$>
---                text "X is:" <^> (pretty x) <$>
---                text "Current unifier is:" <^> pretty unifier
---              ) 
-       case (lookup var unifier) of
-        Just val -> 
---            llogDE ( text "Found (Var <~ Val) in current unifier:" <$>
---                     indent 2 (pretty var) <+> text " <~ " <+> pretty val <$>
---                     indent 2 (text "continue unify val x")
---                    ) >>
-            unify val x
-        Nothing  -> do case (lookup x unifier) of
-                         Just val -> 
---                            llogDE ( text "Found (X <~ Val) in current unifier:" <^>
---                                     (pretty x) <+> text "<~" <+> pretty val <^>
---                                     text "continue unify var val"
---                                    ) >>
-                            unify var val
-                         Nothing  -> if var `subtermOf` x
-                                        then flush "unifyVar:Not unifiable"
-                                        else do 
---                                               llogDE ( text "Apply (Var <~ X) to current Unifier and Insert:" <^>
---                                                         pretty var <+> text "<~" <+> pretty x
---                                                       ) 
-                                                put (insertApply (var <~ x) unifier)
+    matches :: (MonadError e m) => t -> t -> C m Bool
+    matches t1 t2 = ( match t1 t2 >>= return . (const True) )
+                      `catchError` \_ -> return False
hunk ./src/Syntax/Class/Unifier.hs 53
-  
--- | Returns True if 'matchesWithSubs' does not 'fail', False if it does.
-matches ::  (Unifiable t) => t -> t -> Bool
-matches = (isJust .) . matchesWithSubs
-                         
--- | subsumes = flip matches
-subsumes :: (Unifiable t) =>  t -> t -> Bool
-subsumes = flip matches  
-
-
--- | returns True if both lists are of the same length and the elements are 
---   pairwise 'equal'
-equalLs :: (Unifiable t) => [t] -> [t] -> Bool
-equalLs = ap (ap . ((&&) .) . subsumesLs) matchesLs
-
+    matchL :: (MonadError e m) => [t] -> [t] -> C m (Subst t)
+    matchL tl sl = mapM (uncurry match) (zip tl sl) >>= foldM merge nullSubst
hunk ./src/Syntax/Class/Unifier.hs 56
--- | returns True if both lists are of the same length and each element of
---   the first list pairwise 'matches' its colleague in the second list
-matchesLs :: (Unifiable t) => [t] -> [t] -> Bool
-matchesLs = (isJust .) .  matchesWithSubsLs
- 
--- | subsumesLs = flip matchesLs
-subsumesLs ::  (Unifiable t) => [t] -> [t] -> Bool
-subsumesLs = flip matchesLs
+    matchesL :: (MonadError e m) => [t] -> [t] -> C m Bool
+    matchesL t1 t2 = ( matchL t1 t2 >>= return . (const True) )
+                      `catchError` \_ -> return False 
+                                   
+    mgu ::  (MonadError e m) => t -> t -> C m (Subst t)
hunk ./src/Syntax/Class/Unifier.hs 62
-matchLs :: (Unifiable t, MonadPlus m) => [t] -> [t] -> U m t
-matchLs  = ((maybe cancel proceed) . ) . (zipPairsWithM (,))
-    where
-    cancel = flush "unifyLs: No Match!" 
-    proceed = mapM_ (uncurry match)
-             
-unifyLs :: (Unifiable t, MonadPlus m) => [t] -> [t] -> U m t
-unifyLs = ((maybe cancel proceed) . ) . (zipPairsWithM (,))
-    where
-    cancel = flush "unifyLs: Not unifiable" 
-    proceed = mapM_ (uncurry unify)
- 
-matchesWithSubsLs :: (Unifiable t, MonadPlus m ) => [t] -> [t]  -> m (Substitution t)
-matchesWithSubsLs l1 l2 = mws l1 l2 nullSubst
-    where
-    mws [] [] s = return s
-    mws [] _ s  = fail "matchesWithSubsLs: No Match!"
-    mws _ [] s  = fail "matchesWithSubsLs: No Match!"
-    mws (x:xs) (y:ys) s = execStateT (match x y) s >>= mws xs ys
+    mguL :: (MonadError e m) => [t] -> [t] -> C m (Subst t)
+    mguL   []   []    = return nullSubst
+    mguL (t:ts)(u:us) = do s1 <- mgu t u
+                           s2 <- mguL (applyL s1 ts)(applyL s1 us)
+                           return (s1@@s2)
hunk ./src/Syntax/Class/Unifier.hs 68
--- DEAD CODE 
---{- | Convenience function to unify different kind of terms, but keeping 
---     track of the Substitution. @unify2 t1 t2@ corresponds approximately to 
---     @liftM2 (,) (mapM unify t1) (unify t2)@, where the latter 
---     unify uses the Substitution of the further. 
---     This is needed to unify all patterns on the lhs and the rhs of 
---     multiple rules.
----}
---mgu2        :: (Ord t', Unifiable t', Unifiable t) => ([t],t') -> ([t],t') -> (t -> t') -> LM (Substitution t')
---mgu2 (t1,t1') (t2,t2') trans =
---        execStateT (unifyLs t1 t2) [] >>= 
---        (execStateT $ unify t1' t2') . (transSubs trans)
---        where
---        transSubs f =  map $ uncurry (on (,) f)
---        
--- DEAD CODE
---matchesWithSubs2 :: (Ord t', Unifiable t', Unifiable t) => ([t],t') -> ([t],t') -> (t -> t') -> LM (Substitution t')
---matchesWithSubs2 (t1,t1') (t2,t2') trans = do
---        subs  <- execStateT (matchLs t1 t2) []
---        subs' <- execStateT (match t1' t2') (transSubs trans subs)
---        return subs' 
---        where
---        transSubs f =  map (\(a,b) -> on (,) f a b)
---          
--- DEAD CODE
---matches2 t1 t2 f = do{matchesWithSubs2 t1 t2 f >> return True} 
---                         `catchError` (const.return $ False)
+    unify :: (MonadError e m) => t -> t -> C m t
+    unify t1 t2 = mgu t1 t2 >>= return . (flip apply t1)
hunk ./src/Syntax/Class/Unifier.hs 71
-                         
-zipPairsWithM :: (Monad m) => (a -> b -> c) -> [a] -> [b] -> m [c]       
+    
+zipPairsWithM :: (MonadError e m) => (a -> b -> m c) -> [a] -> [b] -> m [c]       
hunk ./src/Syntax/Class/Unifier.hs 76
-zipPairsWithM f (x:xs) (y:ys) = do 
-    done <- zipPairsWithM f xs ys
-    return $ (f x y):done
-            
-flush :: (MonadState (Substitution t) m) => String -> m () 
-flush s = put [] >> fail s
-
-
-      
+zipPairsWithM f (x:xs) (y:ys) =  liftM2 (:) (f x y) (zipPairsWithM f xs ys)
+             
hunk ./src/Syntax/Context.hs 2
-module Context.SynthesisContext  where
+module Syntax.Context (
+    
+    Context(..),
+    emptyContext, defaultContext,
+    addToTypes, addToConstructors, addToClasses, addToMembers, addToInstances, 
+    addToTypeSyns, 
+    
+    C, withC, runC, lookIn, getConType, getVarType, getSuperClasses, getInstances,
+    allInstances,
+
+    module Control.Monad.Reader
+    ) where
hunk ./src/Syntax/Context.hs 16
+
hunk ./src/Syntax/Context.hs 18
-import Syntax.Types
-import Logging.PrettyPrinter
+import Syntax.Type
+import Syntax.Expressions
+
+import PrettyPrinter
hunk ./src/Syntax/Context.hs 23
+import Control.Monad.Error
+import Control.Monad.Identity
+import Data.Maybe (catMaybes)
+
hunk ./src/Syntax/Context.hs 32
-data SynCtx = SCtx
-    { sctx_types    :: !(Map.Map Name Type)
+data Context = Ctx
+    { ctx_types    :: !(Map.Map Name Type)
hunk ./src/Syntax/Context.hs 35
-    , sctx_ctors    :: !(Map.Map Name Type)
+    , ctx_ctors    :: !(Map.Map Name Type)
hunk ./src/Syntax/Context.hs 37
-    , sctx_classes  :: !(Map.Map Name [Name])
+    , ctx_classes  :: !(Map.Map Name [Name])
hunk ./src/Syntax/Context.hs 39
-    , sctx_members  :: !(Map.Map Name [Name])
+    , ctx_members  :: !(Map.Map Name [Name])
hunk ./src/Syntax/Context.hs 41
-    , sctx_instances  :: !(Map.Map Type [Name])
-    -- mapping a type to its classes, of which it is a member   
-    , sctx_typesyns  :: !(Map.Map  Type Type)
+    , ctx_instances  :: !(Map.Map Name [Type])
+    -- mapping a class name to its member types
+--    , ctx_instances  :: !(Map.Map Type [Name])
+-- mapping a type to its classes, of which it is a member   
+    , ctx_typesyns  :: !(Map.Map  Type Type)
hunk ./src/Syntax/Context.hs 48
-
-addToTypes :: [(Name, Type)] -> SynCtx -> SynCtx
+emptyContext = Ctx 
+    { ctx_types     = Map.empty
+    , ctx_ctors     = Map.empty
+    , ctx_classes   = Map.empty
+    , ctx_members   = Map.empty
+    , ctx_instances = Map.empty
+    , ctx_typesyns  = Map.empty
+} 
+addToTypes :: [(Name, Type)] -> Context -> Context
hunk ./src/Syntax/Context.hs 60
-        let types = sctx_types ctx 
-        in ctx{sctx_types = Map.insert n ty types}    
+        let types = ctx_types ctx 
+        in ctx{ctx_types = Map.insert n ty types}    
hunk ./src/Syntax/Context.hs 63
-addToConstructors :: [(Name, Type)] -> SynCtx -> SynCtx
+addToConstructors :: [(Name, Type)] -> Context -> Context
hunk ./src/Syntax/Context.hs 67
-        let ctors = sctx_ctors ctx 
-        in ctx{sctx_ctors = Map.insert n ty ctors}
+        let ctors = ctx_ctors ctx 
+        in ctx{ctx_ctors = Map.insert n ty ctors}
hunk ./src/Syntax/Context.hs 70
-addToClasses :: [(Name, [Name])] -> SynCtx -> SynCtx
+addToClasses :: [(Name, [Name])] -> Context -> Context
hunk ./src/Syntax/Context.hs 74
-        let classes = sctx_classes ctx 
-        in ctx{sctx_classes = Map.insert n ns classes} 
+        let classes = ctx_classes ctx 
+        in ctx{ctx_classes = Map.insert n ns classes} 
hunk ./src/Syntax/Context.hs 77
-addToMembers :: [(Name, [Name])] -> SynCtx -> SynCtx
+addToMembers :: [(Name, [Name])] -> Context -> Context
hunk ./src/Syntax/Context.hs 81
-        let members = sctx_members ctx 
-        in ctx{sctx_members = Map.insert n ns members}       
+        let members = ctx_members ctx 
+        in ctx{ctx_members = Map.insert n ns members}       
hunk ./src/Syntax/Context.hs 84
-addToInstances :: [(Type, Name)] -> SynCtx -> SynCtx
+addToInstances :: [(Type, Name)] -> Context -> Context
hunk ./src/Syntax/Context.hs 88
-        let insts = sctx_instances ctx
-        in ctx{sctx_instances = Map.insertWith (++) ty [n] insts}    
+        let insts = ctx_instances ctx
+        in ctx{ctx_instances = Map.insertWith (++) n [ty] insts}    
hunk ./src/Syntax/Context.hs 91
-addToTypeSyns :: [(Type, Type)] -> SynCtx -> SynCtx
+addToTypeSyns :: [(Type, Type)] -> Context -> Context
hunk ./src/Syntax/Context.hs 95
-        let tysyns = sctx_typesyns ctx
+        let tysyns = ctx_typesyns ctx
hunk ./src/Syntax/Context.hs 97
-        ctx{sctx_typesyns = Map.insert syn ty tysyns}    
+        ctx{ctx_typesyns = Map.insert syn ty tysyns}    
hunk ./src/Syntax/Context.hs 99
-
hunk ./src/Syntax/Context.hs 100
-instance Pretty SynCtx where
-    pretty ctx = linebreak <$> text "SynCtx: " <$>
-               (indent 2 $ text "Types   : " <$> pretty (sctx_types ctx) <$>
-                           text "Ctors   : " <$> pretty (sctx_ctors ctx) <$>
-                           text "Classes : " <$> pretty (sctx_classes ctx) <$>
-                           text "Members : " <$> pretty (sctx_members ctx) <$>
-                           text "Instancs: " <$> pretty (sctx_instances ctx) <$>
-                           text "Synonyms: " <$> pretty (sctx_typesyns ctx))
+instance Pretty Context where
+    pretty ctx = linebreak <$> text "Context: " <$>
+               (indent 2 $ text "Types   : " <$> pretty (ctx_types ctx) <$>
+                           text "Ctors   : " <$> pretty (ctx_ctors ctx) <$>
+                           text "Classes : " <$> pretty (ctx_classes ctx) <$>
+                           text "Members : " <$> pretty (ctx_members ctx) <$>
+                           text "Instancs: " <$> pretty (ctx_instances ctx) <$>
+                           text "Synonyms: " <$> pretty (ctx_typesyns ctx))
hunk ./src/Syntax/Context.hs 110
-defaultSynCtx = SCtx 
-    { sctx_types     = defaulttypes
-    , sctx_ctors     = defaultctors
-    , sctx_classes   = defaultclasses
-    , sctx_members   = defaultmembers
-    , sctx_instances = defaultinstances
-    , sctx_typesyns = defaulttypesyns
+defaultContext = Ctx 
+    { ctx_types     = defaulttypes
+    , ctx_ctors     = defaultctors
+    , ctx_classes   = defaultclasses
+    , ctx_members   = defaultmembers
+    , ctx_instances = defaultinstances
+    , ctx_typesyns = defaulttypesyns
hunk ./src/Syntax/Context.hs 184
+--    
+--defaultinstances = Map.fromList
+--    [(ConT ''Bool,[''Eq, ''Ord])
+--    ,(ConT ''Int,[''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 ListT (mkVarT "a"))
+--     ,[''Eq])
+--    ,(ForallT [mkName "a"] 
+--             [AppT (ConT ''Ord) (mkVarT "a")]
+--             (AppT ListT (mkVarT "a"))
+--     ,[''Ord])
+--    ]
+    
hunk ./src/Syntax/Context.hs 215
-    [(ConT ''Bool,[''Eq, ''Ord])
-    ,(ConT ''Int,[''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])
+    [(''Eq, [ ConT ''Bool
+            , ConT ''Int
+             , ForallT [mkName "a"][mkPred ''Eq "a"] $ AppT ListT (mkVarT "a")
+             , ForallT [mkName "a"][mkPred ''Eq "a"] $ AppT (ConT ''Maybe) (mkVarT "a")
+            ]) 
+    ,(''Ord, [ ConT ''Bool
+             , ConT ''Int
+             , ForallT [mkName "a"][mkPred ''Ord "a"] $ AppT ListT (mkVarT "a")
+             , ForallT [mkName "a"][mkPred ''Ord "a"] $ AppT (ConT ''Maybe) (mkVarT "a")
+             ])
hunk ./src/Syntax/Context.hs 228
-mkVarT = VarT . mkName
-             
-emptySynCtx = SCtx 
-    { sctx_types     = Map.empty
-    , sctx_ctors     = Map.empty
-    , sctx_classes   = Map.empty
-    , sctx_members   = Map.empty
-    , sctx_instances = Map.empty
-    , sctx_typesyns = Map.empty
-} 
hunk ./src/Syntax/Context.hs 229
---mergeCtx :: SynCtx -> SynCtx -> SynCtx
+--mergeCtx :: Context -> Context -> Context
hunk ./src/Syntax/Context.hs 231
---    { sctx_bindings  = (Map.union `on` sctx_bindings) c1 c2
---    , sctx_types     = (Map.union `on` sctx_types) c1 c2
---    , sctx_ctors     = (Map.union `on` sctx_ctors) c1 c2
---    , sctx_classes   = ((Map.unionWith (++)) `on` sctx_classes) c1 c2
---    , sctx_members   = (Map.union `on` sctx_members) c1 c2
---    , sctx_instances = ((Map.unionWith (++)) `on` sctx_instances) c1 c2
---    , sctx_typesyns  = (Map.union `on` sctx_typesyns) c1 c2 
+--    { ctx_bindings  = (Map.union `on` ctx_bindings) c1 c2
+--    , ctx_types     = (Map.union `on` ctx_types) c1 c2
+--    , ctx_ctors     = (Map.union `on` ctx_ctors) c1 c2
+--    , ctx_classes   = ((Map.unionWith (++)) `on` ctx_classes) c1 c2
+--    , ctx_members   = (Map.union `on` ctx_members) c1 c2
+--    , ctx_instances = ((Map.unionWith (++)) `on` ctx_instances) c1 c2
+--    , ctx_typesyns  = (Map.union `on` ctx_typesyns) c1 c2 
hunk ./src/Syntax/Context.hs 243
--- a Monad with SynCtx
+-- a MonadTransformer with Context
hunk ./src/Syntax/Context.hs 246
-type C m = (ReaderT SynCtx m) 
+type C m = ReaderT Context m
+
+withC :: (Monad m) => C m a -> Context -> m a
+withC  c = (runReaderT c)
hunk ./src/Syntax/Context.hs 251
-withC :: (Monad m) => C m a -> SynCtx -> m a
-withC = runReaderT
+runC ::  (Monad m) => C m a -> m a
+runC = (flip withC defaultContext)
hunk ./src/Syntax/Context.hs 254
-lookIn :: (Ord a, Show a, MonadReader SynCtx m) => (SynCtx -> Map.Map a b) -> a -> m b
-lookIn f n = asks f >>= \m ->  
-    maybe (fail $ "Not in context: " ++ (show n))
-          return
-          (Map.lookup n m)
+lookIn :: (Ord a, Show a, MonadReader Context m) => (Context -> Map.Map a b) -> a -> m (Maybe b)
+lookIn f n = asks f >>= \m -> return (Map.lookup n m)
hunk ./src/Syntax/Context.hs 257
-getConType, getVarType :: (MonadReader SynCtx m) => Name -> m Type
-getVarType = lookIn sctx_types
-getConType = lookIn sctx_ctors
+getConType, getVarType :: (MonadReader Context m) => Name -> m (Maybe Type)
+getVarType = lookIn ctx_types
+getConType = lookIn ctx_ctors
hunk ./src/Syntax/Context.hs 261
-getSubClasses :: (MonadReader SynCtx m) => Name -> m [Name]        
-getSubClasses = lookIn sctx_classes
+getSuperClasses :: (MonadReader Context m) => Name -> m [Name]        
+getSuperClasses n = lookIn ctx_classes n >>= return . (maybe [] id)
hunk ./src/Syntax/Context.hs 264
-getInstances :: (MonadReader SynCtx m) => Type -> m [Name]        
-getInstances = lookIn sctx_instances
+--getSubClasses :: (MonadReader Context m) => Name -> m [Name]
+--getSubClasses n = asks ctx_classes >>= return . (map fst) . (filter ((elem n) . snd)) . Map.toList
+
+getInstances :: (MonadReader Context m) => Name -> m [Type]        
+getInstances n = lookIn ctx_instances n >>=  return . (maybe [] id)                
+
+allInstances :: (MonadReader Context m) => m [(Name,[Type])]
+allInstances = asks (Map.toList . ctx_instances)
hunk ./src/Syntax/Expressions.hs 8
-    unfoldAppE, toPat, fromTExp,
+    toPat, fromTExp,
hunk ./src/Syntax/Expressions.hs 10
+    -- checkMatch,
hunk ./src/Syntax/Expressions.hs 16
-import Syntax.Terms
-import Syntax.Types
-import Syntax.Unifier
-import Syntax.Antiunifier
+import Syntax.Class.Term
+import Syntax.Class.Subst
+import Syntax.Type
hunk ./src/Syntax/Expressions.hs 20
+import qualified Language.Haskell.TH.Syntax as TH
hunk ./src/Syntax/Expressions.hs 29
+import Control.Monad.Trans
hunk ./src/Syntax/Expressions.hs 34
-import Logging
+import PrettyPrinter
hunk ./src/Syntax/Expressions.hs 39
-    | TLitE Lit Type    
+    | TLitE TH.Lit Type    
hunk ./src/Syntax/Expressions.hs 61
-instance Eq TExp where 
-    (==) s@(TVarE  sn _ ) t@(TVarE tn _)  = (sameTy s t) && (sn == tn)
-    (==) s@(TWildE _ _ ) t                = (sameTy s t)
-    (==) s t@(TWildE _ _)                 = (sameTy s t) 
-    (==) s@(TConE sn _) t@(TConE tn _)    = (sameTy s t) && (sn == tn)
-    (==) s@(TLitE sl _) t@(TLitE tl _)    = (sameTy s t) && (sl == tl)
---    sameSymAtRoot (TCondE c1 t1 e1) (TCondE c2 t2 e2)        = True     
-    (==) s@(TInfixE sl so sr _) t@(TInfixE tl to tr _) =
-        (sameTy s t) && (sl == tl) && (so == to) && (sr == tr)
-    -- tuples
-    (==) s@(TTupE sv _) t@(TTupE tv _)   = 
-        (sameTy s t) && (tv == sv)
-    (==) t@(TAppE _ _ _ ) s@(TTupE sv _) = 
-        case unfoldTAppE $ t of
-            ((TConE n _):tv) -> (isTuple n (length sv)) && 
-                                (sameTy s t) && (tv == sv) 
-            _owise           -> False
-    (==) s@(TTupE sv _) t@(TAppE _ _ _) = 
-        case unfoldTAppE $ t of
-            ((TConE n _):tv) -> (isTuple n (length sv)) && 
-                                (sameTy s t) && (tv == sv) 
-            _owise           -> False
-    (==) s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)            =
-         (sameTy s t) && (s1 == t1) && (s2 == t2)
-    -- empty Lists
-    (==) s@(TListE [] _) t@(TListE [] _)      = (sameTy s t)
-    (==) s@(TConE n _) t@(TListE [] _)        = (sameTy s t) && isNil n
-    (==) s@(TListE [] _) t@(TConE n _)        = (sameTy s t) && isNil n
-    -- empty list and other (if other is a (:) list it matches default clause)
-    (==) s@(TListE _ _) t@(TListE [] _)       = False
-    (==) s@(TListE [] _) t@(TListE _ _)       = False
-    -- non-empty lists
-    (==) s@(TListE sl _) t@(TListE tl _)      = (sameTy s t) && (sl == tl)
-    (==) s@(TListE sl _) t@(TAppE _ _ _)      = 
-        case unfoldTAppE $ t of
-            ((TConE n _):tl) -> (isCons n) && (sameTy s t) && (tl == sl) 
-            _owise           -> False
-    (==) t@(TAppE _ _ _)s@(TListE sl _)       = 
-        case unfoldTAppE $ t of
-            ((TConE n _):tl) -> (isCons n) && (sameTy s t) && (tl == sl) 
-            _owise           -> False
-    (==)  _ _                                 = False
+instance Eq TExp where
+    (==) = equal 
hunk ./src/Syntax/Expressions.hs 65
-    pretty (TVarE n t)         = 
-        braces $ pretty (VarE n) <+> colon <> colon <+> pretty t
-    pretty (TConE n t)         = 
-        braces $ pretty (ConE n) <+> colon <> colon <+> pretty t
-    pretty (TLitE l t)         = 
-        braces $ pretty (LitE l) <+> colon <> colon <+> pretty t
-    pretty (TAppE e1 e2 t)     =  
-        braces $ pretty e1 <+> pretty e2 <+> colon <> colon <+> pretty t
-    pretty (TInfixE p1 n p2 t) = 
-        braces $ hsep [ pretty p1
-                      , pretty n
-                      , pretty p2] <+> 
-                 colon <> colon <+> pretty t
-    pretty (TTupE es t)        = 
-        braces $ (tupled (map pretty es)) <+> colon <> colon <+> pretty t
-    pretty (TListE l t)        = 
-        braces $ (list (map pretty l)) <+> colon <> colon <+> pretty t
-    pretty (TWildE n t)        = 
-        braces $ red $ pretty (VarE (mkName ('?':(show n)))) <+> colon <> colon <+> pretty t
---    pretty (TCondE TExp TExp TExp t
+    pretty e = pretty_ e <+> colon <> colon <+> pretty (typeOf e)    
+
+pretty_ (TVarE n t)         = pretty (VarE n)
+pretty_ (TConE n t)         = pretty (ConE n)
+pretty_ (TLitE l t)         = pretty (LitE l)
+pretty_ (TAppE e1 e2 t)     = pretty_ e1 <+> pretty_ e2
+pretty_ (TInfixE p1 n p2 t) = hsep [ pretty_ p1, pretty_ n, pretty_ p2]
+pretty_ (TTupE es t)        = tupled (map pretty_ es)
+pretty_ (TListE l t)        = list (map pretty_ l)
+pretty_ (TWildE n t)        = red $ pretty (VarE (mkName ('?':(show n))))    
hunk ./src/Syntax/Expressions.hs 92
-    sizeS (TAppE a1 a2 _)   = (sizeS a1).(sizeS a2)
-    sizeS (TInfixE l c r _) = (sizeS l).(sizeS c).(sizeS r)
+    sizeS (TAppE a1 a2 _)   = sizeS a1 . sizeS a2
+    sizeS (TInfixE l c r _) = sizeS l . sizeS c . sizeS r 
hunk ./src/Syntax/Expressions.hs 96
-    sizeS (TCondE c t e _)  = (sizeS c).(sizeS t).(sizeS e)
+    sizeS (TCondE c t e _)  = sizeS c . sizeS t . sizeS e
hunk ./src/Syntax/Expressions.hs 101
-    sameSymAtRoot (TVarE _ _ ) (TVarE _ _)                      = True
-    sameSymAtRoot (TWildE _ _ ) (TWildE _ _)                    = True
-    sameSymAtRoot (TConE n1 _) (TConE n2 _)                     = n1 == n2
-    sameSymAtRoot (TLitE l1 _) (TLitE l2 _)                     = l1 == l2
---    sameSymAtRoot (TCondE c1 t1 e1) (TCondE c2 t2 e2)        = True     
-    sameSymAtRoot (TInfixE _ e1 _ _) (TInfixE _ e2 _ _)         = e1 == e2
+    sameSymAtRoot (TVarE _ _ ) (TVarE _ _)              = True
+    sameSymAtRoot (TWildE _ _ ) (TWildE _ _)            = True
+    sameSymAtRoot (TConE n1 _) (TConE n2 _)             = n1 == n2
+    sameSymAtRoot (TLitE l1 _) (TLitE l2 _)             = l1 == l2 
+    sameSymAtRoot (TInfixE _ e1 _ _) (TInfixE _ e2 _ _) = e1 == e2
hunk ./src/Syntax/Expressions.hs 107
-    sameSymAtRoot (TTupE v1s _)(TTupE v2s _)                    = on (==) length  v1s v2s
-    sameSymAtRoot t@(TAppE _ _ _ )(TTupE vs _)                  = 
-        case head.unfoldTAppE $ t of
-            (TConE n _) -> isTuple n (length vs)
-            _owise      -> False
-    sameSymAtRoot (TTupE vs _) t@(TAppE _ _ _)                  = 
-        case head.unfoldTAppE $ t of 
-            (TConE n _) -> isTuple n (length vs)
-            _owise      -> False
-    sameSymAtRoot t1@(TAppE _ _ _) t2@(TAppE _ _ _)            = 
+    sameSymAtRoot (TTupE v1s _)(TTupE v2s _)            = on (==) length  v1s v2s
+    sameSymAtRoot t@(TAppE _ _ _ )(TTupE vs _)          = 
+        chkTConE (flip isTuple (length vs)) . head . unfoldTAppE $ t
+    sameSymAtRoot (TTupE vs _) t@(TAppE _ _ _)          = 
+        chkTConE (flip isTuple (length vs)) . head . unfoldTAppE $ t
+    sameSymAtRoot t1@(TAppE _ _ _) t2@(TAppE _ _ _)     =
hunk ./src/Syntax/Expressions.hs 115
-    sameSymAtRoot (TListE [] _) (TListE [] _)                    = True
-    sameSymAtRoot (TConE n _) (TListE [] _)                      = isNil n
-    sameSymAtRoot (TListE [] _)(TConE n _)                       = isNil n
-    -- empty list and other (if other is a (:) list it matches default clause)
-    sameSymAtRoot (TListE _ _)  (TListE [] _)                    = False
-    sameSymAtRoot (TListE [] _) (TListE _ _)                     = False
+    sameSymAtRoot (TListE [] _) (TListE [] _)           = True
+    sameSymAtRoot (TConE n _) (TListE [] _)             = isNil n
+    sameSymAtRoot (TListE [] _)(TConE n _)              = isNil n
+    -- empty list and other (if other is a (:)-list, it matches default clause)
+    sameSymAtRoot (TListE _ _)  (TListE [] _)           = False
+    sameSymAtRoot (TListE [] _) (TListE _ _)            = False
hunk ./src/Syntax/Expressions.hs 122
-    sameSymAtRoot (TListE _ _) (TListE _ _)                      = True
-    sameSymAtRoot (TListE _ _) t@(TAppE _ _ _)                  = 
-        case head.unfoldTAppE $  t of
-            (TConE n _) -> isCons n
-            _owise      -> False
-    sameSymAtRoot t@(TAppE _ _ _)(TListE _ _)                   = 
-        case head.unfoldTAppE $ t of
-            (TConE n _) -> isCons n
-            _owise      -> False 
-    sameSymAtRoot  _ _                                     = False
-    
---    substitute s Root _ = s
---    substitute s pos t =
---        case pos of
-----            (P i)     -> maybe t id $  moveToSubtermTE t i (Just.(substitute s Root))
---            (Dot i p) -> maybe t id $  moveToSubtermTE t i (Just.(substitute s p))
+    sameSymAtRoot (TListE _ _) (TListE _ _)             = True
+    sameSymAtRoot (TListE _ _) t@(TAppE _ _ _)          = 
+        chkTConE isCons . head . unfoldTAppE $ t
+    sameSymAtRoot t@(TAppE _ _ _)(TListE _ _)           = 
+        chkTConE isCons . head . unfoldTAppE $ t
+    sameSymAtRoot (TListE _ _)(TInfixE _ c _ _)         = chkTConE isCons c
+    sameSymAtRoot (TInfixE _ c _ _)(TListE _ _)         = chkTConE isCons c
+    sameSymAtRoot  _ _                                  = False
hunk ./src/Syntax/Expressions.hs 132
-    root e@(TWildE _ _)                      = const e
+    root e@(TWildE _ _)                     = const e
hunk ./src/Syntax/Expressions.hs 135
-    root (TTupE _ t)                        = flip TTupE t
+    root (TTupE _ _)                        = mkTTupE
hunk ./src/Syntax/Expressions.hs 138
-    root (TListE (l:ls) lt)                  = 
+    root (TListE _ lt)                  = 
hunk ./src/Syntax/Expressions.hs 143
-    root (TInfixE l c r t)                  = \[l, r] -> (TInfixE l c r t) 
---    root    e                               = 
---        error $ "Terms.root: Not implemented for TExp " ++ (show e)  
+    root (TInfixE l c r t)                  = \[l, r] -> mkTInfixE c l r 
hunk ./src/Syntax/Expressions.hs 155
---    subterms (TInfixE Nothing _c (Just r) _)    = [hole, r]
---    subterms (TInfixE (Just l) _c Nothing _)    = [l, hole]
---    subterms (TInfixE Nothing _c Nothing _)     = [hole, hole]
---    subterms    e                               = 
---        error $ "Terms.subterms: Not implemented for TExp " ++ (show e)
-     
+    
+    equal s@(TVarE  sn _ ) t@(TVarE tn _)  = (sameTy s t) && (sn == tn)
+    equal s@(TWildE _ _ ) t                = (sameTy s t)
+    equal s t@(TWildE _ _)                 = (sameTy s t) 
+    equal s t                              = 
+        and $ (sameTy s t)
+            : (sameSymAtRoot s t)
+            : ( ((zipWith equal) `on` subterms) s t )
+    
hunk ./src/Syntax/Expressions.hs 174
-            
---    hole = TConE 'Hole (ConT ''Hole)
-
-
-    
-instance Unifiable TExp where
-    -- TODO: checkMatch should keep track of which type matches which type
-    --       variable!! (Int,Bool,Int) -//-> (a,b,b), also polymorphic types are+
-    --       not considered
-    -- matching wildcards 
-    match s@(TWildE i1 _) t     = nomatch "match (243)" --checkMatch s t >> return ()
-    match s t@(TWildE i1 _)     = checkMatch s t >> return ()-- checkMatch s t >> return ()
-    -- matching variables    
-    match s@(TVarE i1 _) t@(TVarE i2 _)     = 
-        checkMatch s t >> if  i1 == i2 then return () else matchVar s t
-    match s@(TVarE _ _) t                   = nomatch "match (249)"
-    match s          t@(TVarE _ _)          = checkMatch s t >> matchVar s t -- checkMatch s t  >> matchVar s t
-    -- matching constructors    
-    match s@(TConE ns _) t@(TConE nt _)     = do
-        if (ns == nt) then return () else nomatch "match (253)" 
-    -- matching literals          
-    match s@(TLitE l1 _) t@(TLitE l2 _)     = do
-        checkMatch s t
-        if (l1 == l2) then return () else nomatch "match (257)"
-    -- matching tuples
-    match s@(TTupE sl _)         t@(TTupE tl _)     =
-        mapM_ (uncurry unify) (zip sl tl)
-    match s@(TTupE sl _)         t@(TAppE _ _ _)    = 
-        case unfoldTAppE t of
-            ((TConE n _):args) -> mapM_ (uncurry match) (zip sl args)
-            _owise               -> nomatch "match (263)"
-    match t@(TAppE _ _ _)        s@(TTupE sl _)    =
-        case unfoldTAppE t of
-            ((TConE _ _):args) -> mapM_ (uncurry match) (zip args sl)
-            _owise             -> nomatch "match (268)"
-        
-    match s@(TListE [] _)        t@(TListE [] _)    = return ()
-    match s@(TListE (se:sl) st)  t@(TListE (te:tl) tt)  =
-        match se te >> match (TListE sl st) (TListE tl tt)
-    -- as usual, something special for lists, so check whether the AppE is of 
-    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
-    match s@(TListE [] _)        t@(TConE n _)        =
-        if isNil n then return () else nomatch "match (276)"
-    match s@(TConE n _)          t@(TListE [] _)        =
-        if isNil n then return () else nomatch "match (278)"
-    match s@(TListE (se:sl) st)  t@(TAppE _ _ _) =
-        case unfoldTAppE t of
-            ((TConE n _):a1:[a2]) ->
-                match se a1 >> match (TListE sl st) a2
-            _owise       -> nomatch "match (282)"
-    match t@(TAppE _ _ _)        s@(TListE (se:sl) st)       =
-        case unfoldTAppE t of
-            ((TConE n _):a1:[a2]) ->
-                match se a1 >> match (TListE sl st) a2
-            _owise       -> nomatch "match (288)"
-    match s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  =
-        if isCons n 
-           then match se te >> match (TListE sl st) tl
-           else nomatch ("match (292)" ++ (show.pretty $  n))
-    match t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  =
-        if isCons n 
-          then match te se >> match tl (TListE sl st)
-          else nomatch "match (296)"
-    
-    match s@(TAppE s1 s2 _)      t@(TAppE t1 t2 _)     = 
-        match s1 t1 >> match s2 t2
-    
-    match s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = 
-        if (equal s2 t2) then match s1 t1 >> match s3 t3 else nomatch "match"
---    match s@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) = 
---        checkMatch s t >> match s1 t1 >> match s2 t2 >> match s3 t3    
-    match s t = nomatch $ "match\n" ++ (showp s) ++ "\n" ++ (showp t)
---        let msg =  patternNotDef [text.show $ s, pretty t]
---        in  llogDE msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
---            flush "No Match!"
-
-    
-    -- unifying wildcards 
-    -- TODO: ?create substitution?
-    unify s@(TWildE i1 _) t     = checkSubsume s t >> return ()
-    unify s t@(TWildE i1 _)     = checkMatch s t >> return ()    
-    unify s@(TVarE i1 _) t@(TVarE i2 _)     = do
-        (checkSubsume s t) `mplus` (checkMatch s t)
-        if  i1 == i2 then return () else unifyVar s t
-    unify s@(TVarE _ _) t                   = checkSubsume s t >> unifyVar s t
-    unify s          t@(TVarE _ _)          = checkMatch s t >> unifyVar s t 
-    -- unifying constructors    
-    unify s@(TConE ns _) t@(TConE nt _)     =
-        if (ns == nt) then return () else flush "Not unifiable (322)"  
-    -- unifying literals          
-    unify s@(TLitE l1 _) t@(TLitE l2 _)     =
-        if (l1 == l2) then return () else flush "Not unifiable (325)"  
-    -- unifying tuples
-    unify s@(TTupE sl _) t@(TTupE tl _)     = mapM_ (uncurry unify) (zip sl tl)
-    unify s@(TTupE sl _) t@(TAppE _ _ _)    =
-        case unfoldTAppE t of
-            ((TConE n _):args) -> mapM_ (uncurry unify) (zip sl args)
-            _owise               -> flush "Not unifiable (345)"  
-    unify t@(TAppE _ _ _) s@(TTupE sl _)    =
-        case unfoldTAppE t of
-            ((TConE _ _):args) -> mapM_ (uncurry unify) (zip args sl)
-            _owise             -> flush "Not unifiable (345)"  
-        
-    unify s@(TListE [] _) t@(TListE [] _)    = return ()
-    unify s@(TListE (se:sl) st) t@(TListE (te:tl) tt)  =
-        unify se te >> unify (TListE sl st) (TListE tl tt)
-    -- as usual, something special for lists, so check whether the AppE is of 
-    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
-    unify s@(TListE [] _) t@(TConE n _)        =
-        if isNil n then return () else flush "Not unifiable (343)"    
-    unify s@(TConE n _) t@(TListE [] _)        =
-        if isNil n then return () else flush "Not unifiable (345)"   
-    unify s@(TListE (se:sl) st) t@(TAppE _ _ _) =
-        case unfoldTAppE t of
-            ((TConE n _):a1:[a2]) ->
-                unify se a1 >> unify (TListE sl st) a2
-            _owise       -> flush "Not unifiable (354)"  
-    unify t@(TAppE _ _ _) s@(TListE (se:sl) st)       =
-        case unfoldTAppE t of
-            ((TConE n _):a1:[a2]) ->
-                unify se a1 >> unify (TListE sl st) a2
-            _owise       -> flush "No unifiable (355)"  
-    unify s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  =
-        if isCons n 
-           then unify se te >> unify (TListE sl st) tl
-           else flush "Not unifiable (359)"
-    unify t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  =
-        if isCons n 
-           then unify se te >> unify tl (TListE sl st)
-           else flush "Not unifiable (363)"
-    
-    unify s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = unify s1 t1 >> unify s2 t2
-    
-    unify s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = 
-        if ( equal s2 t2) then unify s1 t1 >> unify s3 t3
-          else flush "Not unifiable (369)"         
-    unify s@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) =
-        unify s1 t1 >> unify s2 t2 >> unify s3 t3    
-    unify s t                               = flush "Not unifiable (372)"
---        let msg =  patternNotDef [text.show $ s, pretty t]
---        in llogWA msg >> llogDE (hsep (map pretty (unfoldTAppE t))) >>
---           flush "Not unifiable!"
hunk ./src/Syntax/Expressions.hs 179
-    --   Well, and of course some necessary lifting. 
-    apply u v@(TVarE _ _)        = 
-        case lookup v u of
-            Just val -> return val -- checkSame v val >> return val
-            Nothing  -> return v
-    apply u t@(TConE _ _)     = return t
-    apply u t@(TWildE _ _)    = return t
-    apply u t@(TLitE _ _)     = return t
-    apply u t@(TListE [] _)   = return t
-    apply u (TListE ts ty)        = do 
-        ts' <- (mapM (apply u) ts)
-        return $ TListE ts' $ mkListT . typeOf . head $ ts'  -- DANGER!!! Correctness of Types is not checked
-    apply u (TTupE ts _)         = do 
-        ts' <- (mapM (apply u) ts)
-        return $ TTupE ts' $ mkTupT (map typeOf ts')
-    apply u (TAppE a1 a2 ty)      = do
-        a1' <- apply u a1
-        a2' <- apply u a2
-        return $ TAppE a1' a2' $ mkAppT (typeOf a1')(typeOf a2')  -- DANGER!!! Correctness of Types is not checked
-    apply u (TInfixE e1 op e2 ty) = 
-        do e1' <- (apply u) e1 
-           e2' <- (apply u) e2 
-           return $ TInfixE e1' op e2' $ mkInfixT (typeOf op)(typeOf e1')(typeOf e2')
---    apply u (TCondE e1 e2 e3 ty)  = 
---        liftM4 TCondE (apply u e1) (apply u e1) (apply u e1) (return ty)
-    apply u t                               =   
-        let msg =  patternNotDef [text.show $ u, pretty t]
-        in -- logWA msg >> 
-           fail (show msg)       
-
--- TODO: should rewrite antiunification usinf root and subterms from Terms 
--- instead of collectSubtermsTE. need to crefully check!!!
---    (mapM aunify) . transpose . (map subterms) l >>= return . (root . head $ l)
-instance Antiunifiable TExp where
-
+    apply u v@(TVarE n _) = maybe v id (lookup n u)
+    apply u     t         = root t $ applyL u (subterms t)
hunk ./src/Syntax/Expressions.hs 182
-    -- antiunifying (TAppE TExp TExp Type)
-    aunify l@((TAppE _ _ ty):xs) =
-        case collectSubtermsTE l of
-            Just subterms -> do
-                args1ai <- aunify (subterms !! 0)
-                args2ai <- aunify (subterms !! 1)
-                table <- get
-                case args1ai of
-                    (TVarE n _) -> if n `elem` (M.elems table) -- no AppE (VarE _) _
-                                     then return args1ai
-                                     else return $ TAppE args1ai args2ai ty
-                    _owise   -> return $ TAppE args1ai args2ai ty
-            Nothing             ->
-                computeAntiInstance l
-                
-    -- antiunifying (TListE [TExp] Type)
-    aunify ts@((TListE _ lty@(AppT _ ety)):xs) =
---        lift (setCurrentLogger "Terms.Antiunifier.aunify") >>
---        llogEnterDE >>
---        llogDE (text "Input arguments are :" <> pretty l) >>
-        case collectSubtermsTE ts of            
-            Just subterms  -> do
-                ai <- mapM aunify subterms
-                if(all null subterms) 
-                  then return $ TListE [] lty
-                  else case ai of
-                        [e,TListE l _] -> return $ TListE (e:l) lty
-                        _owise         -> do 
-                            let tcone = TConE '(:) (mkArrowT [ety, lty, lty]) 
-                            return $ mkTInfixE tcone (head ai) (last ai)
-----                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 the 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) then return $ TListE straightai ty
---                 -- check if we have ragged list at allm and if so we can keep the f***ing ListE
---                  else do raggedai <- computeAntiInstance $ map (flip TListE ty) ragged
---                          -- convert back to lists, to get correct variable image
---                          if (null straight) then return raggedai
---                            else do
---                              -- iff there are straight, we add them in 'cons' style 
---    --                          llogDE $ text "List have different length"
---    --                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
---                                let tcone = TConE '(:) (mkArrowT [ety, ty, ty]) 
---                                let sections = map (mkTInfixE tcone) straightai
---                                return $ foldTInfixE sections raggedai
-            Nothing     ->
-                computeAntiInstance ts
-                
-    -- antiunifying (TTupE [TExp] Type)        
-    aunify l@((TTupE _ ty):xs) =  
-        case collectSubtermsTE l of
-            Just subterms -> do                
-                ai_subterms <- mapM aunify subterms
-                return $ TTupE ai_subterms ty
-            Nothing       -> 
-                computeAntiInstance l         
-
-    -- antiunifying (TInfixE (Maybe TExp) TExp (Maybe TExp) Type)
-    aunify l@((TInfixE _ c _ ty):xs) =
-        case collectSubtermsTE l of
-            Just subterms -> do 
-                lai <- aunify (subterms !! 0)
-                rai <- aunify (subterms !! 1)
-                return $ TInfixE lai c rai ty
-            Nothing       -> 
-                  computeAntiInstance l           
-
---   -- antiunifying (TCondE TExp TExp TExp Type)
---    aunify l@((TCondE _ _ _ ty):xs) =
---        case collectSubtermsTE l of
---            Just subterms -> do 
---                fstai <- aunify (subterms !! 0)
---                sndai <- aunify (subterms !! 1)
---                thrai <- aunify (subterms !! 2)
---                return $ TCondE fstai sndai thrai ty
---            Nothing       -> 
---                  computeAntiInstance l       
hunk ./src/Syntax/Expressions.hs 183
-    -- antiunifying (VarE Name)              
-    aunify l@((TVarE _ _):xs) =  
-        checkforAntiInstance l   
-    -- antiunifying (VarE Name)              
-    aunify l@((TWildE _ _):xs) =  
-        checkforAntiInstance l         
-    -- antiunifying (ConE Name)
-    aunify l@((TConE _ _):xs) =
-        checkforAntiInstance l     
-    -- antiunifying (LitE Lit)
-    aunify l@((TLitE _ _):xs) =
-        checkforAntiInstance l
-    aunify [] = 
-        fail $ "Antiunifier.aunify at TExp: empty list, no terms to antiunify"
-    aunify (x:_) = 
-        fail $ "Antiunifier.aunify at TExp: Antiunification for " ++ show x ++
-                "of Type TExp is not implemented!"
-----------------------
--- Unification and Matching
-----------------------
-
-
-
-
--- | Helper for lifting a walker (Unifiable t) => (Maybe t) (Maybe t)
-liftUnify :: (Unifiable t, MonadPlus m) => Maybe t -> Maybe t -> U m t
-liftUnify = (\u v -> maybe (return ()) (\(s,t) -> unify s t) (liftM2 (,) u v))
-
--- | Helper for matching (Unifiable t) => (Maybe t) (Maybe t)
-liftMatch :: (Unifiable t, MonadPlus m) => Maybe t -> Maybe t -> U m t
-liftMatch = (\u v -> maybe (return ()) (\(s,t) -> match s t) (liftM2 (,) u v))     
- 
-
-----------------------
--- Antiunification
-----------------------
---{-|
---   A dummy data type to model antiunification of InfixE (see below). This is not 
---   very nice, but I have no clue how to do it in a more elegant way.
----}
---data DummyTExp = DummyTExp  
---dummy = TConE 'DummyExp (ConT ''DummyExp)
-
-{-|
-   Determine the collector function by means of the first element. The 
-   collector, which is fixed to a certain data constructor and collects the 
-   subterms or returns 'Nothing' if one element does not match with the fixed 
-   data constructor.   
--}
--- TODO:  should rewrite antiunification using root and subterms from Terms 
--- instead of collectSubtermsTE. need to carefully check (*)!!!
-collectSubtermsTE :: [TExp] -> Maybe [[TExp]]
-collectSubtermsTE l = liftM transpose $ sequence $ map collector l 
-  -- (*)  (allSame l) >> (return $ transpose . (map subterms) $ l )
-    where
-  -- (*) allSame (x:xs) = foldM_ (\a b -> checkSame a b >> return a) x xs
-    collector = collectSubterms (head l)
---    collectSubterms pivot t = 
---        if sameSymAtRoot pivot t then checkSame pivot t >> return $ subterms t
---           else fail ""
---    
-            
- 
-    collectSubterms :: (MonadPlus m) => TExp -> TExp -> m [TExp]        
-    collectSubterms s@(TTupE _ _) t@(TTupE vals _) = 
-        checkSame s t >> return vals        
-    collectSubterms s@(TAppE _ _ _) t@(TAppE e1 e2 _) = 
-        checkSame s t >> return [e1,e2] 
-    collectSubterms s@(TListE [] _) t@(TListE [] _) = 
-        checkSame s t >> return []     
-    collectSubterms s@(TListE (x:xs) _) t@(TListE (l:ls) ty) =  
-        checkSame s t >> return [l, TListE ls ty]      
---    collectSubterms s@(TListE _ _) t@(TListE l _) = 
---        checkSame s t >> return l      
---    collectSubterms s@(TCondE _ _ _ _) t@(TCondE e1 e2 e3 _) = 
---        check fail s t >> return [e1, e2, e3]    
-    -- If the expression is a section e.g. (+1) we have to substitute the value
-    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
-    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE l c r _) = 
-        checkSame s t >> return [l,r]
---    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE Nothing e2 (Just e3) _)   = 
---        checkSame s t >> return [dummy, e2, e3]
---    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE (Just e1) e2 Nothing _)   = 
---        checkSame s t >> return [e1, e2, dummy]
---    collectSubterms s@(TInfixE _ _ _ _) t@(TInfixE Nothing e2 Nothing _)     = 
---        checkSame s t >> return [dummy, e2, dummy]
-    collectSubterms _ _                               = fail ""
-
-    
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It assures, that everything is put back at place when returning the result.
-moveToSubtermTE :: (Monad m) => TExp -> Int -> (TExp -> m TExp) -> m TExp
-moveToSubtermTE (TVarE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"        
-moveToSubtermTE (TLitE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"    
-moveToSubtermTE (TConE _ _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"
-    
-moveToSubtermTE t@(TAppE _ _ _ ) i f  = do
-    let (op:args) = (unfoldTAppE t)     
-    -- the first element is the operator name
-    liftM (foldTAppE op) (applyAtIndexM args i f)
-    
-moveToSubtermTE (TTupE es ty) i f      = 
-   liftM2 TTupE (applyAtIndexM es i f) (return ty)
-    
-moveToSubtermTE (TListE (e:es) ty) i f = do
-    let elist = [e, TListE es ty]
-    [e', TListE es' ty'] <- (applyAtIndexM elist i f)
-    return $ TListE (e':es') ty'
-    
-moveToSubtermTE (TInfixE l op r ty) 0 f = 
-    do { e <- f l; return $ (TInfixE e op r ty)}
-moveToSubtermTE (TInfixE l op r ty) 1 f = 
-    do { e <- f r; return $ (TInfixE l op e ty)}
-moveToSubtermTE (TInfixE _ op _ _) i _          = 
-    fail $ "Terms.moveToSubtermE: No subterm at position " ++ (show i) ++ 
-           " of operator " ++ (show op)
hunk ./src/Syntax/Expressions.hs 195
-toPat (TVarE n _)         = VarP n
-toPat (TLitE l _)         = LitP l
-toPat (TConE n _)         = ConP n []
-toPat (TListE l _)        = ListP (map toPat l)
-toPat (TTupE l _)         = TupP (map toPat l)
+toPat (TVarE n _)         = TH.VarP n
+toPat (TLitE l _)         = TH.LitP l
+toPat (TConE n _)         = TH.ConP n []
+toPat (TListE l _)        = TH.ListP (map toPat l)
+toPat (TTupE l _)         = TH.TupP (map toPat l)
hunk ./src/Syntax/Expressions.hs 202
-    in  ConP n (map toPat as)                
+    in  TH.ConP n (map toPat as)                
hunk ./src/Syntax/Expressions.hs 204
-    InfixP (toPat l) n (toPat r)
+    TH.InfixP (toPat l) n (toPat r)
hunk ./src/Syntax/Expressions.hs 213
+
+-- DEPRECATED
+--          
+--checkTys :: (Typed t, Pretty t, Monad m) => (t -> t -> Bool) -> (String -> m ()) -> t -> t -> m ()        
+--checkTys c f s t
+--    | c s t = return ()
+--    | otherwise  = f $ "Type mismatch " ++ 
+--                       ((showp $ s)) ++ "  " ++ 
+--                       ((showp $ t))
+
+---- TODO: These should be more sophisticated, when dealing with type classes,
+---- now only monomorphic t ypes are allowed.
+--checkSubsume:: (Typed t, Pretty t, Monad m) => t -> t -> m ()
+--checkSubsume = checkSame -- checkTys (subsumesTy `on` typeOf)  fail -- (subsumesTy `on` typeOf) fail       
+
+   
+
+--checkSame :: (Typed t, Pretty t, Monad m) => t -> t -> m ()   
+--checkSame t1 t2 = 
+--    if on equal typeOf  t1 t2 then return () else fail "Type mismatch"
hunk ./src/Syntax/Expressions.hs 237
-nomatch s = flush $ "Expressions." ++ s ++ ": No Match!"
+
hunk ./src/Syntax/Expressions.hs 277
+mkTTupE as = TTupE as (mkTupT (map typeOf as))    
+
hunk ./src/Syntax/Expressions.hs 283
-mkListE l = TListE l (mkListT . typeOf . head $ l)
+mkTListE []     = error "mkTListE: empty List"
+mkTListE (e:es) = 
+    case es of 
+     []            -> TListE [e] (mkListT . typeOf $ e)
+     [TListE ls t] -> TListE (e:ls) t
+     [expr]        -> mkTInfixE (TConE '(:) $ mkArrowT [ typeOf e
+                                                       , (mkListT . typeOf $ e)
+                                                       , (mkListT . typeOf $ e)]
+                                 ) e expr
+     ls            -> TListE (e:ls)(mkListT . typeOf $ e)
+
hunk ./src/Syntax/Expressions.hs 297
+chkTConE f (TConE n _) = f n
+chkTConE _ _           = False 
+
hunk ./src/Syntax/Expressions.hs 306
-
-    
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Exp
--------------------------------------------------------------------------------}
-
-{-|
-   A dummy data type to model antiunification of InfixE (see below). This is not 
-   very nice, but I have no clue how to do it in a more elegant way.
--}
-data DummyExp = DummyExp  
-dexp = ConE 'DummyExp
-
-{-|
-   Determine the collector function by means of the first element. The 
-   collector, which is fixed to a certain data constructor and collects the 
-   subterms or returns 'Nothing' if one element does not match with the fixed 
-   data constructor.
--}
-collectSubtermsE :: [Exp] -> Maybe [[Exp]]
-collectSubtermsE l = liftM transpose $ sequence $ map collector l 
-    where
-    collector = case head l of
-        (TupE _)         -> collectSubtermsTupE
-         -- TODO what about mixed terms with ListE and AppE (ConE "GHC.Types.[]") _)?
-        (AppE _ _)       -> collectSubtermsAppE
-        (ListE _)        -> collectSubtermsListE
-        (InfixE _ _ _)   -> collectSubtermsInfixE
-        (CondE _ _ _)    -> collectSubtermsCondE
-        
-    collectSubtermsTupE :: Exp -> Maybe [Exp]        
-    collectSubtermsTupE (TupE vals)         = Just vals 
-    collectSubTermsTupE _                   = Nothing
-    
-    collectSubtermsAppE :: Exp -> Maybe [Exp]
-    collectSubtermsAppE (AppE e1 e2)        = Just [e1,e2]
-    collectSubtermsAppE _                   = Nothing
-    
-    collectSubtermsListE :: Exp -> Maybe [Exp]
-    collectSubtermsListE (ListE l)          = Just l
-    collectSubtermsListE _                  = Nothing
-    
-    collectSubtermsCondE :: Exp -> Maybe [Exp]
-    collectSubtermsCondE (CondE e1 e2 e3)   = Just [e1, e2, e3]
-    collectSubtermsCondE _                  = Nothing
-    
-    -- If the expression is a section e.g. (+1) we have to substitute the value
-    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
-    collectSubtermsInfixE :: Exp -> Maybe [Exp]
-    collectSubtermsInfixE (InfixE (Just e1) e2 (Just e3)) = Just [e1, e2, e3]
-    collectSubtermsInfixE (InfixE Nothing e2 (Just e3))   = Just [dexp, e2, e3]
-    collectSubtermsInfixE (InfixE (Just e1) e2 Nothing)   = Just [e1, e2, dexp]
-    collectSubtermsInfixE (InfixE Nothing e2 Nothing)     = Just [dexp, e2, dexp]
-    collectSubtermsInfixE _                               = Nothing
-
-   
---------------------------------------------------------------------------------
--- general Auxiliary functions for 'Term's (deprecated)
-----------------------------------------------------------------------------------
-
--- | Returns only the arguments of an 'AppE'xpression.
-unfoldAppEargs = tail . unfoldAppE
-
--- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
---   @ConE@ of the function name or the constructor.
-unfoldAppE :: Exp -> [Exp]
-unfoldAppE e = f [] e
-    where 
-    f done e =
-        case e of
-            (AppE e1@(VarE _) e2) -> e1:e2:done
-            (AppE e1@(ConE _) e2) -> e1:e2:done
-            (AppE e1 e2)       -> f (e2:done) e1
-            _owise             -> e:done
hunk ./src/Syntax/Expressions.hs 307
-foldAppE :: [Exp] -> Exp
-foldAppE es = foldl1 AppE es
-
-
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It assures, that everything is put back at place when returning the result.
-moveToSubtermE :: (Monad m) => Exp -> Int -> (Exp -> m Exp) -> m Exp
-moveToSubtermE (VarE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"        
-moveToSubtermE (LitE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"    
-moveToSubtermE (ConE _) _ _ = fail "Terms.moveToSubtermE. No subterm at position"
-    
-moveToSubtermE t@(AppE _ _ ) i f  = do
-    let (op:args) = (unfoldAppE t)     
-    -- the first element is the operator name
-    liftM (foldAppE.(op:)) (applyAtIndexM args i f)
-    
-moveToSubtermE (TupE es) i f      = 
-   liftM TupE (applyAtIndexM es i f)
-    
-moveToSubtermE (ListE (e:es)) i f = do
-    let elist = [e, ListE es]
-    [e', ListE es'] <- (applyAtIndexM elist i f)
-    return $ ListE (e':es')
-    
-moveToSubtermE (InfixE (Just e1) op e2) 0 f = 
-    do { e <- f e1; return $ (InfixE (Just e) op e2)}
-moveToSubtermE (InfixE e1 op (Just e2)) 1 f = 
-    do { e <- f e2; return $ (InfixE e1 op (Just e))}
-moveToSubtermE (InfixE _ op _ ) i _          = 
-    fail $ "Terms.moveToSubtermE: No subterm at position " ++ (show i) ++ 
-           " of operator " ++ (show op)
-                                    
-
---compareAtRootE :: Exp -> Exp -> Bool
---compareAtRootE (VarE _) (VarE _)                        = True
---compareAtRootE (ConE n1) (ConE n2)                      = n1 == n2
---compareAtRootE (LitE l1) (LitE l2)                      = l1 == l2
---compareAtRootE (TupE v1s)(TupE v2s)                     = (length v1s) == (length v2s)
---compareAtRootE t1@(AppE _ _ ) t2@(AppE _ _ )            = compareAtRootE (head (unfoldAppE t1))(head (unfoldAppE t2))
---compareAtRootE (ListE []) (ListE [])                    = True
---compareAtRootE (ListE []) (ListE _)                     = False
---compareAtRootE (ListE _)  (ListE [])                    = False
---compareAtRootE (ListE _)  (ListE _)                     = True
---compareAtRootE (CondE _ _ _) (CondE _ _ _)              = True    
---compareAtRootE (InfixE _ e1 _) (InfixE _ e2 _)          = compareAtRootE e1 e2
---compareAtRootE  _ _                                     = False
-           
-           
--- [a]::[a]
-rhs0 = TListE [TVarE (mkName "b") (VarT (mkName "a"))] (AppT ListT (VarT (mkName "a")))
--- [a,b]::[a]
-rhs1 = TListE [TVarE (mkName "a") (VarT (mkName "a")),TVarE (mkName "b") (VarT (mkName "a"))] (AppT ListT (VarT (mkName "a")))
--- [c,c]::[a]
-rhs2 = TListE [TVarE (mkName "c") (VarT (mkName "a")),TVarE (mkName "c") (VarT (mkName "a"))] (AppT ListT (VarT (mkName "a")))
--- (x0:x1)::[a]
-rhs3 = TInfixE (TVarE (mkName "x0") (VarT (mkName "a"))) 
-               (TConE '(:)
-                      (AppT (AppT ArrowT (VarT (mkName "a"))) 
-                            (AppT (AppT ArrowT 
-                                       (AppT ListT (VarT (mkName "a")))) 
-                                  (AppT ListT (VarT (mkName "a")))))) 
-               (TVarE (mkName "x1") (AppT ListT (VarT (mkName "a")))) 
-               (AppT ListT (VarT (mkName "a")))
-
--- [[c],[d]]::[[a]]
-rhs4 = TListE [ TListE [TVarE (mkName "c") (VarT (mkName "a"))](AppT ListT (VarT (mkName "a")))  
-              , TListE [TVarE (mkName "d") (VarT (mkName "a"))](AppT ListT (VarT (mkName "a")))
-              ]  
-              (AppT ListT (AppT ListT (VarT (mkName "a"))))
--- [[]]::[[a]]
-rhs5 = TListE [ TListE [](AppT ListT (VarT (mkName "a")))
-              ]  
-              (AppT ListT (AppT ListT (VarT (mkName "a")))) 
--- [[b],[]]::[[a]]
-rhs6 = TListE [ TListE [TVarE (mkName "b") (VarT (mkName "a"))](AppT ListT (VarT (mkName "a")))  
-              , TListE [](AppT ListT (VarT (mkName "a")))
-              ]  
-              (AppT ListT (AppT ListT (VarT (mkName "a"))))
-lhs0 = [TVarE (mkName "b") (VarT (mkName "a")),TListE [](AppT ListT (VarT (mkName "a"))) ]                   
-lhs1 = [TListE [](AppT ListT (VarT (mkName "a"))),TListE [](AppT ListT (VarT (mkName "a"))) ]               
-
-
-
-
hunk ./src/Syntax/IFTemplateHaskell.hs 3
-
+    
+       
+    isTuple, isNil, isCons, Name, mkName,
+    
hunk ./src/Syntax/IFTemplateHaskell.hs 8
-    module Language.Haskell.TH.Syntax,
+--    module Language.Haskell.TH.Syntax,
hunk ./src/Syntax/IFTemplateHaskell.hs 53
+
+isTuple :: Name -> Int -> Bool
+isTuple n i
+    | i == 2  = n == '(,)
+    | i == 3  = n == '(,,)
+    | i == 4  = n == '(,,,)
+    | i == 5  = n == '(,,,,)
+    | i == 6  = n == '(,,,,,)
+    | i == 7  = n == '(,,,,,,)
+    | i == 8  = n == '(,,,,,,,)
+    | i == 9  = n == '(,,,,,,,,)
+    | i == 10  = n == '(,,,,,,,,,)
+    | i == 11  = n == '(,,,,,,,,,,)
+    | i == 12  = n == '(,,,,,,,,,,,)
+    | i == 13  = n == '(,,,,,,,,,,,,)
+    | i == 14  = n == '(,,,,,,,,,,,,,)
+    | i == 15  = n == '(,,,,,,,,,,,,,,)
+    
+isNil :: Name -> Bool
+isNil = (==) '[]
+
+isCons :: Name -> Bool
+isCons = (==) '(:)
+   
+             
hunk ./src/Syntax/Patterns.hs 1
-{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
-module Syntax.Patterns where
-
- 
-import Syntax.Terms
-import Syntax.Types
-import Syntax.Unifier
-import Syntax.Antiunifier
-import Syntax.IFTemplateHaskell
-
-import qualified Data.Set as S
-import Control.Monad
-import Control.Monad.State (get, runStateT, put)
-import Data.Maybe (catMaybes)
-import Data.List (union, transpose)
-import Data.Function (on)
-import Logging
-
-data TPat = TLitP Lit Type
-          | TVarP Name Type
-          | TTupP [TPat] Type
-          | TConP Name [TPat] Type
-          | TInfixP TPat Name TPat Type
-          | TListP [TPat] Type
---          | TildeP Pat            -- no bang patterns
---          | AsP Name Pat          -- no as-patterns
---          | WildP                 -- no wildcards
---          | RecP Name [FieldPat]  -- no records
---          | SigP Pat Type         -- already made explicit
-        deriving (Ord,Show)
-
-
-instance Eq TPat where
-
-    (==) s@(TVarP sn _)         t@(TVarP tn _)         = sameTy s t && sn == tn
-    (==) s@(TConP sn _ _)       t@(TConP tn _ _)       = sameTy s t && sn == tn
-    (==) s@(TLitP sl _)         t@(TLitP tl _)         = sameTy s t && sl == tl
-    (==) s@(TTupP sv _)         t@(TTupP tv _)         = sameTy s t && sv == tv
-    (==) s@(TConP n sl _)       t@(TTupP tl _)         = sameTy s t && sl == tl
-    (==) s@(TTupP sl _)         t@(TConP n tl _)       = sameTy s t && sl == tl
-    -- empty Lists    
-    (==) s@(TListP [] _)        t@(TListP [] _)        = sameTy s t
-    (==) s@(TListP [] _)        t@(TConP n [] _)       = sameTy s t && isNil n
-    (==) s@(TConP n [] _)       t@(TListP [] _)        = sameTy s t && isNil n
-    -- empty and other
-    (==) s@(TListP [] _)        t@(TListP _ _)         = False     
-    (==) s@(TListP _ _)         t@(TListP [] _)        = False   
-    -- cons lists
-    (==) s@(TListP sl _)        t@(TListP tl _)        = sameTy s t && sl == tl   
-    (==) s@(TListP sl _)        t@(TConP n tl _)       = 
-        sameTy s t && isCons n && sl == tl  
-    (==) s@(TConP n sl _)       t@(TListP tl _)        = 
-        sameTy s t && isCons n && sl == tl           
-    (==) s@(TInfixP sl so sr _) t@(TInfixP tl to tr _) = 
-        sameTy s t && so == to && [sl,sr] == [tl,tr]
-    (==)  _ _                                          = False
-            
-instance Typed TPat where
-    typeOf (TLitP _ t)          = t
-    typeOf (TVarP _ t)          = t
-    typeOf (TTupP _ t)          = t
-    typeOf (TConP _ _ t)        = t
-    typeOf (TInfixP _ _ _ t)    = t
-    typeOf (TListP _ t)         = t
-    
-instance Pretty TPat where
-    pretty (TLitP l t)         = 
-        braces $ pretty (LitP l) <+> colon <> colon <+> pretty t
-    pretty (TVarP n t)         = 
-        braces $ pretty (VarP n) <+> colon <> colon <+> pretty t
-    pretty (TTupP ps t)        = 
-        braces $ tupled (map pretty ps) <+> colon <> colon <+> pretty t
-    pretty (TConP n ps t)      = 
-        braces $ pretty (ConP n []) <> hcat (map pretty ps)  <+> 
-                 colon <> colon <+> pretty t
-    pretty (TInfixP p1 n p2 t) = 
-        braces $ hcat [pretty p1, pretty n,pretty p2] <> colon <+> pretty t 
-    pretty (TListP ps t)       = 
-        braces $ list (map pretty ps)  <+> colon <> colon <+> pretty t
-
-instance Term TPat where
-
-    sameSymAtRoot (TVarP _ _)       (TVarP _ _)        = True
-    sameSymAtRoot (TConP c1 _ _)    (TConP c2 _ _)     = (c1 == c2)
-    sameSymAtRoot (TLitP l1 _)      (TLitP l2 _)       = l1 == l2
-    sameSymAtRoot (TTupP v1s _)     (TTupP v2s _)      = (length v1s) == (length v2s)
-    sameSymAtRoot (TConP n _ _)     (TTupP l _)        = isTuple n (length l)
-    sameSymAtRoot (TTupP l _)       (TConP n _ _)      = isTuple n (length l)
-    -- empty Lists    
-    sameSymAtRoot (TListP [] _)     (TListP [] _)      = True
-    sameSymAtRoot (TListP [] _)     (TConP n [] _)     = isNil n
-    sameSymAtRoot (TConP n [] _)    (TListP [] _)      = isNil n
-    -- empty and other
-    sameSymAtRoot (TListP [] _)     (TListP _ _)       = False     
-    sameSymAtRoot (TListP _ _)      (TListP [] _)      = False   
-    -- cons lists
-    sameSymAtRoot (TListP _ _)      (TListP _ _)       = True   
-    sameSymAtRoot (TListP _ _)      (TConP n _ _)      = isCons n   
-    sameSymAtRoot (TConP n _ _)     (TListP _ _)       = isCons n
-         
-    sameSymAtRoot (TInfixP _ n1 _ _)(TInfixP _ n2 _ _) = n1 ==  n2
-    sameSymAtRoot  _ _                                 = False
-            
-    root _ = error "Syntax.Term.root for TPat not implemented"
---    substitute s Root _ = s
---    substitute s pos  t =
---        case pos of
---        -- (P i)     -> maybe t id $  moveToSubtermTP t i (Just.(substitute s Root))
---         (Dot i p) -> maybe t id $  moveToSubtermTP t i (Just.(substitute s p))
-       
-    subterms (TVarP _ _)         = []
-    subterms (TLitP _ _)         = []
-    subterms (TConP _ pats _)    = pats
-    subterms (TInfixP p1 _ p2 _) = [p1,p2] 
-    subterms (TListP [] _)       = []
-    subterms (TListP (p:ps) ty)  = [p, TListP ps ty]
-    subterms (TTupP pats _)      = pats
---    subterms    p                = 
---        error $ "Terms.subterms at TPat: Not implemented for Pattern " ++ (show p)
-    
-    isVar (TVarP _ _) = True
-    isVar _           = False
-    
-    fromVar (TVarP n _) = n
-    fromVar _ = error "Syntax.Terms.fromVar at Patterns: Not a Variable"
-    
-    toVar t n = TVarP n (typeOf t)
-    
-    isWild _ = False
-        
---    hole              = TConP 'Hole [] (ConT ''Hole) 
-
-
-instance Substitutable TPat where
-    apply u v@(TVarP _ _)         = case lookup v u of 
-                                     Just val -> return val
-                                     Nothing  -> return v
-    --apply u (TConP n ps ty)       = liftM (flip (TConP n) ty) (mapM (apply u) ps)
-    apply u t@(TLitP _ _)         = return t
-    apply u (TListP ts ty)        = liftM (flip TListP ty) (mapM (apply u) ts)
-    apply u (TTupP ts ty)         = liftM (flip TTupP ty) (mapM (apply u) ts)
-    apply u (TInfixP e1 op e2 ty) =
-        liftM4 TInfixP (apply u e1) (return op) (apply u e2) (return ty)
-    apply u t                     =   
-        let msg =  patternNotDef [ pretty u, pretty t]
-        in  --setCurrentLogger "Terms.Terms.apply at TPat" >>
-            --logWA msg >> 
-            fail ( show msg)      
-
-
-instance Unifiable TPat where    
-
-    match s@(TVarP sn _)           t@(TVarP tn _)          = do
-        checkMatch s t 
-        if sn == tn then return () else matchVar s t
-    match s@(TVarP _ _)            t                       = flush  "No Match!"
-    match s                        t@(TVarP _ _)           = matchVar s t            
-    match s@(TLitP sl _)           t@(TLitP tl _)          = do
-        checkMatch s t
-        if sl == tl then return () else flush  "No Match!"         
-    match s@(TListP [] _)          t@(TListP [] _)         = do 
-        checkMatch s t ; return ()
-    match s@(TListP (se:ss) st)    t@(TListP (te:ts) tt)   = 
-        checkMatch s t >> match se te >> match (TListP ss st) (TListP ts tt) 
-    -- as usual, something special for lists, so check whether the ConP is of 
-    -- the form (ConP GHC.Base.: [elem, restlist])
-    match s@(TListP [] _)          t@(TConP n [] _)        = do
-        checkMatch s t 
-        if isNil n then return () else flush  "No Match!"  
-    match s@(TConP n [] _) t@(TListP [] _)                 = do
-        checkMatch s t 
-        if isNil n then return () else flush  "No Match!"  
-    match s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = do
-        checkMatch s t
-        if isCons n 
-          then match se te >> match (TListP ss st) ts 
-          else flush "No Match!"  
-    match s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   = do
-        checkMatch s t
-        if isCons n 
-          then match se te >> match ss (TListP ts tt) 
-          else flush "No Match!"
-    match s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       = do
-        checkMatch s t
-        if n1 == n2 
-          then mapM_ (uncurry match) (zip p1 p2) 
-          else flush "No Match!"          
-    match s@(TTupP sl _)           t@(TTupP tl _)          = do
-        checkMatch s t
-        mapM_ (uncurry match) (zip sl tl)       
-    match s@(TConP n sl _)         t@(TTupP tl _)          = do
-        checkMatch s t
-        if isTuple n (length tl) 
-          then mapM_ (uncurry match) (zip sl tl)
-          else flush "No Match!"      
-    match s@(TTupP sl _)           t@(TConP n tl _)        = do
-        checkMatch s t
-        if isTuple n (length sl) 
-          then mapM_ (uncurry match) (zip sl tl)
-          else flush "No Match!"         
-    match s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  = do
-        checkMatch s t
-        if s2 == t2
-          then match s1 t1 >> match s3 t3
-          else flush  "No Match!"          
-    match s t                                              =    
-        flush  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))  
-       
-
-    unify s@(TVarP sn _)           t@(TVarP tn _)          = do
-        (checkSubsume s t) `mplus` (checkMatch s t)
-        if sn == tn then return () else unifyVar s t
-    unify s@(TVarP _ _)            t                       = unifyVar s t
-    unify s                        t@(TVarP _ _)           = unifyVar s t             
-    unify s@(TLitP sl _)           t@(TLitP tl _)          =
-        if sl == tl then return () else flush  "Not unifiable!"         
-    unify s@(TListP [] _)          t@(TListP [] _)         = return ()
-    unify s@(TListP (se:ss) st)    t@(TListP (te:ts) tt)   = 
-        unify se te >> unify (TListP ss st) (TListP ts tt) 
-    -- as usual, something special for lists, so check whether the ConP is of 
-    -- the form (ConP GHC.Base.: [elem, restlist])
-    unify s@(TListP [] _)          t@(TConP n [] _)        =
-        if isNil n then return () else flush  "Not unifiable!"  
-    unify s@(TConP n [] _) t@(TListP [] _)                 =
-        if isNil n then return () else flush  "Not unifiable!"  
-    unify s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = 
-        if isCons n 
-          then unify se te >> unify (TListP ss st) ts 
-          else flush "Not unifiable!"  
-    unify s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   =
-        if isCons n 
-          then unify se te >> unify ss (TListP ts tt) 
-          else flush "Not unifiable!"
-    unify s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       =
-        if n1 == n2 
-          then mapM_ (uncurry unify) (zip p1 p2) 
-          else flush "Not unifiable!"          
-    unify s@(TTupP sl _)           t@(TTupP tl _)          =
-        mapM_ (uncurry unify) (zip sl tl)       
-    unify s@(TConP n sl _)         t@(TTupP tl _)          =
-        if isTuple n (length tl) 
-          then mapM_ (uncurry unify) (zip sl tl)
-          else flush "Not unifiable!"      
-    unify s@(TTupP sl _)           t@(TConP n tl _)        =
-        if isTuple n (length sl) 
-          then mapM_ (uncurry unify) (zip sl tl)
-          else flush "Not unifiable!"         
-    unify s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  =
-        if s2 == t2
-          then unify s1 t1 >> unify s3 t3
-          else flush  "Not unifiable!"          
-    unify s t                                              =    
-        flush  ("Term " ++ (show s) ++ "does not unify with term " ++ (show t))
-        
-  
-instance Antiunifiable TPat where
-
-    -- antiunifying (TupP [Pat])
-    aunify l@((TTupP _ ty):xs) = 
-        case collectSubtermsTP l of
-            Just subterms -> do                
-                ai_subterms <- mapM aunify subterms
-                return $ TTupP ai_subterms ty
-            Nothing       -> 
-                computeAntiInstance l
-    
-    -- antiunifying (ConP Name [Pat])
-    aunify l@((TConP nm _ ty):xs) = 
-        case collectSubtermsTP l of
-            Just subterms -> do           
-                ai_subterms <- mapM aunify subterms
-                return $ TConP nm ai_subterms ty
-            Nothing       -> 
-                computeAntiInstance l
-                
-    -- antiunifying (InfixP Pat Name Pat)
-    aunify l@((TInfixP _ nm _ ty):xs) =
-        case collectSubtermsTP l of
-            Just subterms -> do 
-                fstai <- aunify (subterms !! 0)
-                sndai <- aunify (subterms !! 1)
-                return $ TInfixP fstai nm sndai ty
-            Nothing       -> 
-                  computeAntiInstance l 
-    
-    -- antiunifying (ListP [Pat])
-    -- Here some hack is necessary, because of Haskell's inconsistent way of
-    -- representing lists. If the pattern lists have different lengths, we
-    -- antiunify argument-wise starting with the first arguments until some 
-    -- pattern has no nth argument. If so, the whole rest is antiunified
-    -- and the ouput is constructed as a (:)-List with a variable as tail.
-    -- (see also @aunify (ListE _)@ )
-    aunify l@((TListP _ ty@(AppT _ ety)):xs) =  
-        case collectSubtermsTP l of
-            Just subterms  -> do
-                let len = length l
-                    straight = takeWhile (\l -> length l == len) subterms 
-                    ragged   = dropWhile (\l -> length l == len) subterms
-                straightai <- mapM aunify straight
-                if null ragged then return $ TListP straightai ty 
-                  else do raggedai <- computeAntiInstance $ map (flip TListP ty) ragged
-                          if (null straight) then return raggedai
-                           else do  
-                                let sections = map (mkTInfixP '(:) ty) straightai
-                                return $ foldTInfixP sections raggedai                                     
-            Nothing     ->
-                computeAntiInstance l 
-    
-    -- antiunifying (VarP Name)              
-    aunify l@((TVarP _ _):xs) =  
-        checkforAntiInstance l     
-    -- antiunifying (LitP Lit)
-    aunify l@((TLitP _ _):xs) =
-        checkforAntiInstance l
-    aunify [] = 
-        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
-
-    aunify (x:_) = 
-        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
-                "of Type Pat is not implemented!"            
---------------------------------------------------------------------------------
--- Auxiliary functions for 'TPat' as 'Term's
---------------------------------------------------------------------------------
-
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It is assured, that everything is put back in place when returning the result.
-moveToSubtermTP :: (Monad m) => TPat ->Int ->  (TPat -> m TPat) -> m TPat
-moveToSubtermTP (TVarP _ _) _ _ = fail "Terms.moveToSubtermTP. No subterm at position"        
-moveToSubtermTP (TLitP _ _) _ _ = fail "Terms.moveToSubtermTP. No subterm at position"    
-moveToSubtermTP (TConP n ps ty) i f = liftM (\ps ->TConP n ps ty) (applyAtIndexM ps i f)
-   
-moveToSubtermTP (TTupP ps ty) i f      = 
-    liftM (flip TTupP ty) (applyAtIndexM ps i f)
-    
-moveToSubtermTP (TListP (p:ps) ty) i f = do
-    let plist = [p,  TListP ps ty]
-    [p', TListP ps' ty'] <- (applyAtIndexM plist i f)
-    return $  TListP (p':ps') ty'
-    
-moveToSubtermTP (TInfixP p1 op p2 ty) i f = do
-    [p1',p2'] <- applyAtIndexM [p1,p2] i f
-    return $ (TInfixP p1' op p2' ty)
-
-{-|
-   Determine the collector function by means of the first element. The 
-   collector, which is fixed to a certain data constructor and collects the 
-   subterms or returns 'Nothing' if one element does not match with the fixed 
-   data constructor.
--}
-collectSubtermsTP :: [TPat] -> Maybe [[TPat]]
-collectSubtermsTP l = liftM transpose $ sequence $ map collector l 
-    where
-    collector = collectSubterms (head l)
-        
-    collectSubterms :: (MonadPlus m) => TPat -> TPat -> m [TPat]
-    collectSubterms s@(TConP sn _ _)     t@(TConP tn pats _) 
-        | sn == tn  = checkSame s t >> return pats
-        | otherwise = fail ""
-    collectSubterms s@(TTupP _ _)        t@(TTupP vals _)    = 
-        checkSame s t >> return vals        
-    collectSubterms s@(TListP _ _)       t@(TListP l _)      = 
-        checkSame s t >> return l      
-    collectSubterms s@(TInfixP _ sn _ _) t@(TInfixP l st r _)
-        | sn == st  = checkSame s t >> return [l, r]
-        | otherwise = fail ""
-    collectSubterms _ _                                      = fail ""
-
-
-    
-
-fromTPat (TVarP n _)   = VarP n
-fromTPat (TLitP n _)   = LitP n
-fromTPat (TTupP l _)   = TupP (map fromTPat l)
-fromTPat (TListP l _)  = ListP (map fromTPat l)
-fromTPat (TConP n l _) = ConP n (map fromTPat l)
-fromTPat (TInfixP l n r _) =
-    InfixP (fromTPat l) n (fromTPat r)
-
-
-mkTInfixP c t l r =  TInfixP l c r t
-    
-foldTInfixP [] _ = error "foldTInfixP: empty list of sections!"    
-foldTInfixP sections lastarg = foldr1 (.) sections lastarg     
---------------------------------------------------------------------------------
--- TH.Exp
---------------------------------------------------------------------------------
-instance Term Pat where
-
-    sameSymAtRoot (VarP _) (VarP _)                       = True
-    sameSymAtRoot (ConP c1 _) (ConP c2 _)                 = (c1 == c2)
-    sameSymAtRoot (LitP l1) (LitP l2)                     = l1 == l2
-    sameSymAtRoot (TupP v1s)(TupP v2s)                    = (length v1s) == (length v2s)
-    sameSymAtRoot (ConP n _) (TupP l)                     = isTuple n (length l)
-    sameSymAtRoot (TupP l)(ConP n _)                      = isTuple n (length l)
-    -- empty Lists    
-    sameSymAtRoot (ListP [])(ListP [])                    = True
-    sameSymAtRoot (ListP [])(ConP n [])                   = isNil n
-    sameSymAtRoot (ConP n [])(ListP [])                   = isNil n
-    -- empty and other
-    sameSymAtRoot (ListP [])(ListP _ )                    = False     
-    sameSymAtRoot (ListP _ )(ListP [])                    = False   
-    -- cons lists
-    sameSymAtRoot (ListP _ )(ListP _ )                    = True   
-    sameSymAtRoot (ListP _ )(ConP n _)                    = isCons n   
-    sameSymAtRoot (ConP n _)(ListP _ )                    = isCons n
-         
-    sameSymAtRoot (InfixP _ n1 _) (InfixP _ n2 _)         = n1 ==  n2
-    sameSymAtRoot  _ _                                    = False
-
---    getPos t s | s == t     = [Root]
---               | otherwise  = 
---                    case t of
---                      (ConP _ ps)                    -> mapGetPos ps s
---                      (InfixP p1 _ p2) -> 
---                            let pos1 = map (°0) (getPos p1 s)
---                                pos2 = map (°1) (getPos p2 s)
---                            in pos1 ++ pos2
---                      (ListP [])                      -> [Root ° 0]
---                      (ListP (p1:ps))                 -> mapGetPos [p1, ListP ps] s  -- I HATE SYNTACTIC SUGAR!!!
---                      (TupP ps)                       -> mapGetPos ps s                                    
---                      _owise                          -> [] --  VarP Name, LitP Lit 
---    
-            
---    substitute s Root _ = s
---    substitute s pos t =
---        case pos of
---        --    (P i)     -> maybe t id $  moveToSubtermP i t (Just.(substitute s Root))
---            (Dot i p) -> maybe t id $  moveToSubtermP i t (Just.(substitute s p))
-       
-    root _ = error "Syntax.Term.root for Pat not implemented"
-    subterms (VarP _)         = []
-    subterms (LitP _)         = []
-    subterms (ConP _ pats)    = pats
-    subterms (InfixP p1 _ p2) = [p1,p2] 
-    subterms (ListP [])       = []
-    subterms (ListP (p:ps))   = [p, ListP ps]
-    subterms (TupP pats)      = pats
-    subterms    p                            = 
-        error $ "Terms.subterms: Not implemented for Pattern " ++ (show p)
-    
-    isVar (VarP _) = True
-    isVar _        = False
-    
-    fromVar (VarP n) = n
-    fromVar _ = error "Syntax.Terms.fromVar at Patterns: Not a Variable"
-    
-    toVar _ = VarP
-    
-    isWild _ = False
-    
-                 
---    getVars t@(VarP _)                     = [t]
---    getVars (LitP _)                       = []
---    getVars (TupP ps)                      = foldl1 union $ map getVars ps
---    getVars (ConP _ ps)                    = foldl1 union $ map getVars ps
---    getVars (ListP l)                      = foldl1 union $ map getVars l
---    getVars (InfixP e1 _ e2)               = on union getVars e1 e2 
---        
---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
-----    
-----    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!"
-                        
---------------------------------------------------------------------------------
--- Auxiliary functions for 'Pat' as 'Term's
---------------------------------------------------------------------------------
-
--- |Moves to the specified subterm in the term @t@ and applies function @f@.
---  The result is term @t@ with modified @i@th subterm
---  It is assured, that everything is put back in place when returning the result.
-moveToSubtermP :: (Monad m) => Int -> Pat -> (Pat -> m Pat) -> m Pat
-moveToSubtermP _ (VarP _) _ = fail "Terms.moveToSubtermE. No subterm at position"        
-moveToSubtermP _ (LitP _) _ = fail "Terms.moveToSubtermE. No subterm at position"    
-moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndexM ps i f)
-   
-moveToSubtermP i (TupP ps) f      = 
-    liftM TupP (applyAtIndexM ps i f)
-    
-moveToSubtermP i (ListP (p:ps)) f = do
-    let plist = [p,  ListP ps]
-    [p', ListP ps'] <- (applyAtIndexM plist i f)
-    return $  ListP (p':ps')
-    
-moveToSubtermP i (InfixP p1 op p2) f = do
-    [p1',p2'] <- applyAtIndexM [p1,p2] i f
-    return $ (InfixP p1' op p2')
-
-
-{-------------------------------------------------------------------------------
-  Auxiliary Functions for antiunifying expressions of type Pat 
--------------------------------------------------------------------------------}
-
-{-|
-  See 'collectSubtermsE'
--}
-collectSubtermsP :: [Pat] -> Maybe [[Pat]]
-collectSubtermsP l = liftM transpose $ sequence $ map collector l 
-    where
-    collector = case head l of 
-        (ConP nm _)     -> collectSubtermsConP nm
-        (InfixP _ nm _) -> collectSubtermsInfixP nm
-        (ListP _ )      -> collectSubtermsListP
-        (TupP _ )       -> collectSubtermsTupP
-        _owise          -> fail $ "No match for " ++ ( show l)
-
-    collectSubtermsConP nm (ConP nm' pats) 
-        | nm == nm'          = Just pats  --  always [p1,p2]
-        | otherwise          = Nothing
-    collectSubtermsConP _ _  = Nothing
-    
-    collectSubtermsInfixP nm (InfixP p1 nm' p2) 
-        | nm == nm'              = Just [p1,p2]
-        | otherwise              = Nothing
-    collectSubtermsInfixP _ _    = Nothing    
-
-    collectSubtermsListP (ListP l)          = Just l
-    collectSubtermsListP _                  = Nothing    
-     
-    collectSubtermsTupP (TupP pats)         = Just pats -- [fst,snd]
-    collectSubTermsTupP _                   = Nothing    
- 
-    
+
rmfile ./src/Syntax/Patterns.hs
hunk ./src/Syntax/Specification.hs 2
-module Context.ModuleContext where
+module Syntax.Specification where
hunk ./src/Syntax/Specification.hs 6
-import Syntax
+import Syntax.Expressions
+import Syntax.Class
+import Syntax.Type
hunk ./src/Syntax/Specification.hs 10
-import Data.Rules
+-- import Data.Rules
hunk ./src/Syntax/Specification.hs 14
-import qualified Context.SynthesisContext as SC
+import Control.Monad.State
hunk ./src/Syntax/Specification.hs 16
-import Logging
+import qualified Syntax.Context as SC
+
+import PrettyPrinter
hunk ./src/Syntax/Specification.hs 23
---type Rule = ([TPat], TExp) 
---type Rules = [Rule]
+type Equation = ([TExp], TExp)
hunk ./src/Syntax/Specification.hs 25
-data ModuleCtx = MCtx
-    { mctx_bindings :: !(Map.Map Name Rules)
+data Specification = Spec
+    { spec_bindings :: !(Map.Map Name [Equation])
hunk ./src/Syntax/Specification.hs 28
-    , mctx_synctx   :: !SC.SynCtx
+    , spec_ctx   :: !SC.Context
hunk ./src/Syntax/Specification.hs 31
-mctx_types     = SC.sctx_types . mctx_synctx
-mctx_ctors     = SC.sctx_ctors . mctx_synctx
-mctx_classes   = SC.sctx_classes . mctx_synctx
-mctx_members   = SC.sctx_members . mctx_synctx
-mctx_instances = SC.sctx_instances . mctx_synctx
-mctx_typesyns  = SC.sctx_typesyns . mctx_synctx
+spec_types     = SC.ctx_types . spec_ctx
+spec_ctors     = SC.ctx_ctors . spec_ctx
+spec_classes   = SC.ctx_classes . spec_ctx
+spec_members   = SC.ctx_members . spec_ctx
+spec_instances = SC.ctx_instances . spec_ctx
+spec_typesyns  = SC.ctx_typesyns . spec_ctx
hunk ./src/Syntax/Specification.hs 38
-synCtxOnly :: ModuleCtx -> SC.SynCtx
-synCtxOnly = mctx_synctx
+synCtxOnly :: Specification -> SC.Context
+synCtxOnly = spec_ctx
hunk ./src/Syntax/Specification.hs 41
-getBindings :: [Name] -> ModuleCtx -> Either String [(Name, Rules)]
+getBindings :: [Name] -> Specification -> Either String [(Name, [Equation])]
hunk ./src/Syntax/Specification.hs 49
-               concat (intersperse ", " s) ++
-               "!"
+               concat (intersperse ", " s) ++ "!"
hunk ./src/Syntax/Specification.hs 51
-getBinding :: (Monad m) => ModuleCtx -> Name -> m (Name, Rules)
+getBinding :: (Monad m) => Specification -> Name -> m (Name, [Equation])
hunk ./src/Syntax/Specification.hs 53
-    case Map.lookup n (mctx_bindings ctx) of
+    case Map.lookup n (spec_bindings ctx) of
hunk ./src/Syntax/Specification.hs 57
-addToBindings :: [(Name, Rules)] -> ModuleCtx -> ModuleCtx
+addToBindings :: [(Name, [Equation])] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 61
-        let bindings = mctx_bindings ctx
-        in ctx{mctx_bindings = Map.insert n cs bindings}
+        let bindings = spec_bindings ctx
+        in ctx{spec_bindings = Map.insert n cs bindings}
hunk ./src/Syntax/Specification.hs 64
-addToTypes :: [(Name, Type)] -> ModuleCtx -> ModuleCtx
+addToTypes :: [(Name, Type)] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 66
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToTypes l sctx}   
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToTypes l sctx} 
hunk ./src/Syntax/Specification.hs 69
-addToConstructors :: [(Name, Type)] -> ModuleCtx -> ModuleCtx
+addToConstructors :: [(Name, Type)] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 71
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToConstructors l sctx}   
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToConstructors l sctx}   
hunk ./src/Syntax/Specification.hs 74
-addToClasses :: [(Name, [Name])] -> ModuleCtx -> ModuleCtx
+addToClasses :: [(Name, [Name])] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 76
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToClasses l sctx}   
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToClasses l sctx}   
hunk ./src/Syntax/Specification.hs 79
-addToMembers :: [(Name, [Name])] -> ModuleCtx -> ModuleCtx
+addToMembers :: [(Name, [Name])] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 81
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToMembers l sctx}       
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToMembers l sctx}       
hunk ./src/Syntax/Specification.hs 84
-addToInstances :: [(Type, Name)] -> ModuleCtx -> ModuleCtx
+addToInstances :: [(Type, Name)] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 86
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToInstances l sctx}   
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToInstances l sctx}   
hunk ./src/Syntax/Specification.hs 89
-addToTypeSyns :: [(Type, Type)] -> ModuleCtx -> ModuleCtx
+addToTypeSyns :: [(Type, Type)] -> Specification -> Specification
hunk ./src/Syntax/Specification.hs 91
-    let sctx = mctx_synctx c
-    in c{mctx_synctx = SC.addToTypeSyns l sctx}   
+    let sctx = spec_ctx c
+    in c{spec_ctx = SC.addToTypeSyns l sctx}  
hunk ./src/Syntax/Specification.hs 96
-instance Pretty ModuleCtx where
+instance Pretty Specification where
hunk ./src/Syntax/Specification.hs 98
-               (indent 2 $ text "Bindings: " <$> indent 2 (pretty (mctx_bindings ctx)) <$>
-                           text "Types   : " <$> indent 2 (pretty (mctx_types ctx)) <$>
-                           text "Ctors   : " <$> indent 2 (pretty (mctx_ctors ctx)) <$>
-                           text "Classes : " <$> indent 2 (pretty (mctx_classes ctx)) <$>
-                           text "Members : " <$> indent 2 (pretty (mctx_members ctx)) <$>
-                           text "Instancs: " <$> indent 2 (pretty (mctx_instances ctx)) <$>
-                           text "Synonyms: " <$> indent 2 (pretty (mctx_typesyns ctx)))
+               (indent 2 $ text "Bindings: " <$> indent 2 (pretty (spec_bindings ctx)) <$>
+                           text "Types   : " <$> indent 2 (pretty (spec_types ctx)) <$>
+                           text "Ctors   : " <$> indent 2 (pretty (spec_ctors ctx)) <$>
+                           text "Classes : " <$> indent 2 (pretty (spec_classes ctx)) <$>
+                           text "Members : " <$> indent 2 (pretty (spec_members ctx)) <$>
+                           text "Instancs: " <$> indent 2 (pretty (spec_instances ctx)) <$>
+                           text "Synonyms: " <$> indent 2 (pretty (spec_typesyns ctx)))
hunk ./src/Syntax/Specification.hs 107
-defaultContext = MCtx 
-    { mctx_bindings  = defaultbindings
-    , mctx_synctx    = SC.defaultSynCtx
+defaultSpec = Spec 
+    { spec_bindings  = defaultbindings
+    , spec_ctx    = SC.defaultContext
hunk ./src/Syntax/Specification.hs 111
+
hunk ./src/Syntax/Specification.hs 114
-emptyCtx = MCtx 
-    { mctx_bindings  = Map.empty
-    , mctx_synctx    = SC.emptySynCtx
+emptySpec ctx = Spec 
+    { spec_bindings  = Map.empty
+    , spec_ctx    = ctx
hunk ./src/Syntax/Specification.hs 119
-
--------------------------------------------------------------------------------
--- Using Context
---------------------------------------------------------------------------------
-
-type C a = (StateT ModuleCtx (Either String)) a
-
-getVarType :: (MonadState ModuleCtx m) => Name -> m Type
-getVarType n = do
-    m <- gets mctx_types
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Variable not in context: " ++ (show n) 
-
-getConType :: (MonadState ModuleCtx m) => Name -> m Type
-getConType n = do
-    m <- gets mctx_ctors 
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Ctor not in context: " ++ (show n)
-        
-getSubClasses :: (MonadState ModuleCtx m) => Name -> m [Name]        
-getSubClasses n = do
-    m <- gets mctx_classes
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Class not in context: " ++ (show n)
-        
-getInstances :: (MonadState ModuleCtx m) => Type -> m [Name]        
-getInstances n = do
-    m <- gets mctx_instances
-    case Map.lookup n m of
-        (Just t) -> return t
-        _owise   -> fail $ "Type not in context: " ++ (show n)
hunk ./src/Syntax/Type.hs 1
-{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
-module Syntax.Types (
+-----------------------------------------------------------------------------
+-- Type:        Types
+-- 
+-- Part of `Typing Haskell in Haskell', version of November 23, 2000
+-- Copyright (c) Mark P Jones and the Oregon Graduate Institute
+-- of Science and Technology, 1999-2000
+-- 
+-- This program is distributed as Free Software under the terms
+-- in the file "License" that is included in the distribution
+-- of this software, copies of which may be obtained from:
+--             http://www.cse.ogi.edu/~mpj/thih/
+-- 
+-----------------------------------------------------------------------------
hunk ./src/Syntax/Type.hs 15
+-- |
+module Syntax.Type (
+    -- * Data type 'Type'  
+    Type(..),
+     
+    -- ** Useful type synonyms
+    Pred, TyCxt, QualTy,
+    -- ** Constructors
+    mkAppT, mkArrowT, mkVarT, mkListT, mkTupT, mkInfixT, sectionType, 
+    foldAppT, mkPred,
+    -- ** Deconstructors
+    tyArgs, tyCtor, unArrowT,  unfoldAppTargs,
+    -- ** Modifiers
+    quantify, propCxt, fixType,
+    -- ** Inspectors
+    allPreds,isFunT, isHOT,
+    
hunk ./src/Syntax/Type.hs 33
-    -- isGenTy, equalTys,
-    isFunT, hasFunT, isHOT, hasHOT,
+    -- * Class for typed things
+    Typed(..),
+    -- ** Inspectors on 'Typed' things 
+    hasFunT,  hasHOT,   
hunk ./src/Syntax/Type.hs 38
-    matchT,
hunk ./src/Syntax/Type.hs 39
-    checkMatch, checkSubsume, checkSame,
-    Typed(..),
-    --splitArrowT, 
-    sectionType, argumentType, unArrowT, 
-    mkArrowT, mkListT, mkTupT, mkAppT, mkInfixT, 
-    foldAppT,
-    addPredicates, unfoldAppTargs, fixType
-    ) where
+)where 
hunk ./src/Syntax/Type.hs 41
-import Syntax.IFTemplateHaskell
-import Syntax.Terms
-import Syntax.Unifier hiding (apply, nullSubst)
-import Syntax.Antiunifier
+import Data.List (foldl', nub, intersect, intersectBy)
hunk ./src/Syntax/Type.hs 43
-import Control.Monad.State (MonadState, StateT, execStateT, put, get)
-import Data.List (union, nub, intersect, intersectBy, (\\), find, foldl')
-import Data.Maybe (isJust, mapMaybe, maybe)
hunk ./src/Syntax/Type.hs 45
-import Logging
---import UI.Context
+import Syntax.IFTemplateHaskell (isNil, isCons, isTuple,Name, mkName)
+import qualified Language.Haskell.TH.Syntax as TH( Type(..) )
hunk ./src/Syntax/Type.hs 48
-class Typed t where
-    typeOf :: t -> Type
+import Syntax.Class.Term (Term(..), getVarNames)
+import Syntax.Class.Subst
+
+import PrettyPrinter
+import Debug.Trace
+
+
+data Type = ForallT [Name] TyCxt Type
+ | VarT Name
+ | ConT Name
+ | TupleT Int
+ | ArrowT
+ | ListT
+ | AppT Type Type
+ deriving (Show, Ord, Eq)
hunk ./src/Syntax/Type.hs 64
---data Type
--- = ForallT [Name] Cxt Type
--- | VarT Name
--- | ConT Name
--- | TupleT Int
--- | ArrowT
--- | ListT
--- | AppT Type Type
+
+
+-- Type synonyms for our convenience. If we do this hacks on Type, at least let
+-- us try to spell the implicit assumptions out.
+type QualTy = Type -- assumes Type to be 'ForallT _ _ _'
+type Pred   = Type -- assumes Type to be 'AppT (ConT n) t', where 'n' is a class name
+type TyCxt = [Pred] 
+
+mkPred :: Name -> String -> Type
+mkPred n v = AppT (ConT n) (mkVarT v)
hunk ./src/Syntax/Type.hs 82
-hasFunT :: (Typed t) => t -> Bool
-hasFunT = isFunT . typeOf
-
hunk ./src/Syntax/Type.hs 85
-hasHOT :: (Typed t) => t -> Bool
-hasHOT = isHOT . typeOf
+
hunk ./src/Syntax/Type.hs 87
--- Comparing Types
+-- Typed Things
hunk ./src/Syntax/Type.hs 90
-sameTy :: (Typed t) => t -> t -> Bool
-sameTy = equalTys `on` typeOf
-
--- TODO 
-subsumesTy :: Type -> Type -> Bool
-subsumesTy (VarT _) _ = True 
-subsumesTy (AppT t11 t12) (AppT t21 t22) = 
-    (subsumesTy t11 t21) && (subsumesTy t12 t22)
-subsumesTy (ForallT n1 c1 t1) (ForallT n2 c2 t2)  = 
-    (n1 == (n1 `intersect` n2)) &&
-    (subsumesTy t1 t2) &&
-    (c1 == (intersectBy subsumesTy c1 c2))    
-subsumesTy t1 t2 = equalTys t1 t2
-
-
-   
--- | returns True if both Types are semantically equal, w.r.t. to different 
--- representations for tuple and list types
-equalTys :: Type -> Type -> Bool
-equalTys (VarT _) (VarT _)           = True
-equalTys (ConT n1) (ConT n2)         = n1 == n2
--- tuples
-equalTys (TupleT i1) (TupleT i2)     = i1 == i2
-equalTys (TupleT i) (ConT n)         = isTuple n i
-equalTys (ConT n)(TupleT i)          = isTuple n i
--- lists
-equalTys ListT ListT                 = True
-equalTys ListT (ConT n)              = isNil n
-equalTys (ConT n) ListT              = isNil n
-
-equalTys ArrowT ArrowT               = True
-equalTys (ForallT n1 c1 t1) (ForallT n2 c2 t2)  = 
-    (n1 == (n1 `intersect` n2)) &&
-    (equalTys t1 t2) &&
-    (c1 == (intersectBy equalTys c1 c2))
-equalTys (AppT t11 t12) (AppT t21 t22) = 
-    (equalTys t11 t21) && (equalTys t12 t22)
-equalTys _ _                         = False
+class Typed t where
+    typeOf :: t -> Type
hunk ./src/Syntax/Type.hs 93
+hasFunT :: (Typed t) => t -> Bool
+hasFunT = isFunT . typeOf
hunk ./src/Syntax/Type.hs 96
-          
-checkTys :: (Show t, Pretty t, Typed t, Monad m) =>
-         (t -> t -> Bool) -> (String -> m ()) -> t -> t -> m ()        
-checkTys c f s t
-    | c s t = return ()
-    | otherwise  = f $ "Type mismatch " ++ 
-                       ((showp $ s)) ++ "  " ++ 
-                       ((showp $ t))
+hasHOT :: (Typed t) => t -> Bool
+hasHOT = isHOT . typeOf
hunk ./src/Syntax/Type.hs 99
--- TODO: These should be more sophisticated, when dealing with type classes,
--- now only monomorphic t ypes are allowed.
-checkMatch,checkSubsume,checkSame :: (Show t, Pretty t, Typed t, MonadPlus m) => t -> t -> m ()   
-checkMatch   = checkSame -- checkTys ((flip subsumesTy) `on` typeOf)  fail
-checkSubsume = checkSame -- checkTys (subsumesTy `on` typeOf)  fail -- (subsumesTy `on` typeOf) fail       
-checkSame    = checkTys sameTy fail
hunk ./src/Syntax/Type.hs 101
--- Modifying Types
---------------------------------------------------------------------------------
- 
---equalTys (VarT _) = 
---equalTys (ConT n1) (ConT n2)         = n1 == n2
----- tuples
---equalTys (TupleT i1) (TupleT i2)     = i1 == i2
---equalTys (TupleT i) (ConT n)         = isTuple n i
---equalTys (ConT n)(TupleT i)          = isTuple n i
----- lists
---equalTys ListT ListT                 = True
---equalTys ListT (ConT n)              = isNil n
---equalTys (ConT n) ListT              = isNil n
---
---equalTys ArrowT ArrowT               = True
---equalTys (ForallT n1 c1 t1) (ForallT n2 c2 t2)  = 
---    (n1 == (n1 `intersect` n2)) &&
---    (equalTys t1 t2) &&
---    (c1 == (intersectBy equalTys c1 c2))
---equalTys (AppT t11 t12) (AppT t21 t22) = 
---    (equalTys t11 t21) && (equalTys t12 t22)
---equalTys _ _                         = False
---------------------------------------------------------------------------------
hunk ./src/Syntax/Type.hs 104
--- | splits an ArrowT in the type of a partial aplication and the type of 
---   the argument
-
--- erroneous
---splitArrowT :: Type -> (Type,Type)
---splitArrowT (AppT (AppT ArrowT a1) a2) = (a1,a2)
---splitArrowT t = error $ "Cannot split " ++ (show t)
hunk ./src/Syntax/Type.hs 110
-argumentType = head . unArrowT
+--argumentType = head . unArrowT
+
+mkVarT = VarT . mkName
hunk ./src/Syntax/Type.hs 116
-unArrowT (ForallT ns cxt t) = map (addPredicates cxt) $ unArrowT t
+unArrowT (ForallT ns cxt t) = map (flip quantify cxt) $ unArrowT t
hunk ./src/Syntax/Type.hs 135
-mkAppT :: Type -> Type -> Type
-mkAppT t1 t2 = sectionType t1
--- TODO: DANGER !!! correctness of types is not checked !!!
hunk ./src/Syntax/Type.hs 138
- 
-foldAppT :: Type -> [Type] -> Type
-foldAppT t ts = foldl' AppT t ts
+-- | Make a type application, keep track of quantified types
+mkAppT :: Type -> Type -> Type
+mkAppT (ForallT _ c1 t1)(ForallT _ c2 t2) = quantify (AppT t1 t2) (c1++c2)
+mkAppT  t1              (ForallT _ c t2)  = quantify (AppT t1 t2) c
+mkAppT (ForallT _ c t1)  t2               = quantify (AppT t1 t2) c
+mkAppT  t1               t2               = AppT t1 t2
hunk ./src/Syntax/Type.hs 145
-addPredicates :: Cxt -> Type -> Type
-addPredicates cxt t =
-    case getVarNames t of
-        [] -> t
-        vs -> ForallT vs (filter (isIn vs) cxt) t
-    where  
-    isIn vs (AppT _ (VarT n)) = n `elem` vs
+-- | Make a type with multiple arguments
+foldAppT :: Type -> [Type] -> Type
+foldAppT t ts = foldl' mkAppT t ts
hunk ./src/Syntax/Type.hs 149
+-- | Disassemble a type in its type constructor and its arguments    
+unfoldAppT :: Type -> [Type]
+unfoldAppT e = f [] e
+    where 
+    f done (ForallT ns cxt t) = map (flip quantify cxt) $ f done t
+    f done (AppT e1 e2)       = f (e2:done) e1
+    f done e                  = e:done
hunk ./src/Syntax/Type.hs 160
-    | null ns   = addPredicates cxt t
+    | null ns   = quantify t cxt
hunk ./src/Syntax/Type.hs 167
-unfoldAppT :: Type -> [Type]
-unfoldAppT e = f [] e
-    where 
-    f done (ForallT ns cxt t) = map (addPredicates cxt) $ f done t
-    f done (AppT e1 e2)       = f (e2:done) e1
-    f done e                  = e:done
-
+    
hunk ./src/Syntax/Type.hs 170
+
+--------------------------------------------------------------------------------
+-- Instance Declarations
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+-- PrettyPrinting Types
+
+--instance Pretty Type where
+--    pretty (VarT n)   = pretty $ TH.VarT n
+--    pretty (ConT n)   = pretty $ TH.ConT n
+--    pretty (TupleT i) = pretty $ TH.TupleT i
+--    pretty ArrowT     = pretty TH.ArrowT
+--    pretty ListT      = pretty TH.ListT
+--    pretty ty         = pprTyApp (split ty)
+    
+instance Pretty Type where
+    pretty (ForallT tvars ctxt ty) = 
+            text "forall" <+> hsep (map pretty tvars) <+> text "."
+                          <+> pprCxt ctxt <+> pretty ty
+    pretty ty = pprTyApp (split ty)
+
+-----------------------------------------
+-- PrettyPrinting Au
+-- Stolen from Language.Haskell.TH.PPr
+
+pprParendType :: Type -> Doc
+pprParendType (VarT v)   = pretty v
+pprParendType (ConT c)   = pretty c
+pprParendType (TupleT 0) = text "()"
+pprParendType (TupleT n) = parens (hcat (replicate (n-1) comma))
+pprParendType ArrowT     = parens (text "->")
+pprParendType ListT      = text "[]"
+pprParendType other      = parens (pretty other)
+
+pprTyApp :: (Type, [Type]) -> Doc
+pprTyApp (ArrowT, [arg1,arg2]) = sep [pprFunArgType arg1 <+> text "->", pretty arg2]
+pprTyApp (ListT, [arg]) = brackets (pretty arg)
+pprTyApp (TupleT n, args)
+ | length args == n = parens (sep (punctuate comma (map pretty args)))
+pprTyApp (fun, []) = pprParendType fun
+pprTyApp (fun, args) = pprParendType fun <+> sep (map pprParendType args)
+
+pprFunArgType :: Type -> Doc    -- Should really use a precedence argument
+-- Everything except forall and (->) binds more tightly than (->)
+pprFunArgType ty@(ForallT {})                 = parens (pretty ty)
+pprFunArgType ty@((ArrowT `AppT` _) `AppT` _) = parens (pretty ty)
+pprFunArgType ty                              = pretty ty
+
+split :: Type -> (Type, [Type])    -- Split into function and args
+split t = go t []
+    where go (AppT t1 t2) args = go t1 (t2:args)
+          go ty           args = (ty, args)
+          
+pprCxt :: TyCxt -> Doc
+pprCxt []  = empty
+pprCxt [t] = pretty t <+> text "=>"
+pprCxt ts  = parens (hsep $ punctuate comma $ map pretty ts) <+> text "=>"
+
+-----------------------------------------
+
hunk ./src/Syntax/Type.hs 244
-    sameSymAtRoot (ForallT _ _ t1) t2         = sameSymAtRoot t1 t2
-    sameSymAtRoot t1 (ForallT _ _ t2)         = sameSymAtRoot t1 t2
+    sameSymAtRoot (ForallT _ c1 t1)(ForallT _ c2 t2) = (sameSymAtRoot t1 t2) && ((c1 `intersect` c2) == c1) 
+--    sameSymAtRoot (ForallT _ c1 t1) t2        = sameSymAtRoot t1 t2 
+--    sameSymAtRoot t1 (ForallT _ _ t2)         = sameSymAtRoot t1 t2
hunk ./src/Syntax/Type.hs 249
-    
-    
-    subterms (ForallT _ _ t) = subterms t
-    subterms t@(AppT _ _)    = unfoldAppTargs t
+        
+    subterms (ForallT _ c t) = map (flip quantify c) (subterms t)
+    subterms (AppT l r)      = [l,r]
hunk ./src/Syntax/Type.hs 254
-    root (ForallT ns c t) = \[t] -> ForallT ns c t
-    root t@(AppT t_ _)    = foldl AppT t
+    equal s t = and $ ( sameSymAtRoot s t ):( on (zipWith equal) subterms s t )
+
+    root (ForallT ns c t) = \ts -> quantify (root t (map rmCxt ts)) (nub $ concatMap tyCxt ts)
+    root (AppT _ _)       = \[l,r] -> mkAppT l r
hunk ./src/Syntax/Type.hs 270
+instance Substitutable Type where
+  apply s (VarT u)        = case lookup u s of
+                             Just t  -> t
+                             Nothing -> VarT u
+  apply s (AppT l r)      = mkAppT (apply s l) (apply s r)  
+  apply s (ForallT _ c t) = quantify (apply s t) c
+  apply s t         = t
+  
+--
+-- Type Auxiliaries
+--
+-- |Add quantified type variables
+quantify :: Type -> TyCxt -> Type
+quantify (ForallT ns cxt t) qtys = 
+    let ns'  = nub . (ns++) . (quantifiedVars t) $ qtys
+        cxt' = nub . (allPreds ns') . (cxt++) $ qtys
+    in if null cxt' then t else (ForallT ns' cxt' t)
+    where
+    -- returns only those names of quantified type variables which actually
+    -- occur in both, the type and the context 
+    quantifiedVars :: Type -> TyCxt -> [Name]   
+    quantifiedVars t = (intersect (getVarNames t)) . (concatMap getVarNames)
+quantify t@(AppT _ _) qtys = quantify (ForallT [] [] t) qtys   
+quantify t@(VarT _) qtys = quantify (ForallT [] [] t) qtys
+quantify t _ = t
+
+-- | Gets the type context from a type, may be the empty type context
+tyCxt :: Type -> TyCxt
+tyCxt (ForallT _ cxt _) = cxt
+tyCxt         _         = []
hunk ./src/Syntax/Type.hs 301
+rmCxt :: Type -> Type
+rmCxt (ForallT _ _ t) = t
+rmCxt         t       = t
hunk ./src/Syntax/Type.hs 305
+propCxt :: Type -> Type
+propCxt t@(ForallT _ _ (VarT _))  = t
+propCxt (ForallT _ cxt (AppT l r)) = AppT (quantify l cxt)(quantify r cxt)
+propCxt t = t
hunk ./src/Syntax/Type.hs 310
+-- | returns all type predicates which qualify a variable with given name
+allPreds :: [Name] -> TyCxt -> TyCxt
+allPreds ns = filter (isIn ns) 
hunk ./src/Syntax/Type.hs 314
+-- | True if the type (used as a type repdicate) qualifies any of the given 
+--   variable names 
+isIn :: [Name] -> Pred -> Bool     
+isIn ns (AppT _ (VarT n)) = n `elem` ns
+        
hunk ./src/Syntax/Type.hs 321
---------------------------------------------------------------------------------   
--- Matching of polymorphic types (should be implemented consistently with Unifier instead!
---------------------------------------------------------------------------------   
-type TySubs = [(Type,Type)]  
+-- | Disassemble a type into its arguments    
+tyArgs t = case unfoldAppT t of [] -> []; l -> tail l
hunk ./src/Syntax/Type.hs 324
-nullSubst :: TySubs
-nullSubst = []      
+-- | Disassemble a type into its type constructor    
+tyCtor = head . unfoldAppT
hunk ./src/Syntax/Type.hs 327
-class Types t where
-    apply :: TySubs -> t -> t
-    tvars :: t -> [Type]
-    
-instance  (Types a) => Types [a] where
-    apply s = map (apply s)
-    tvars   = nub . concat . map tvars   
hunk ./src/Syntax/Type.hs 328
-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 = []
+--------------------------------------------------------------------------------
+-- Comparing Types
+--------------------------------------------------------------------------------
hunk ./src/Syntax/Type.hs 332
---infxr 4 @@
---(@@) :: Subst -> Subst -> Subst
---s1@@s2 = [(u; apply s1 t) j (u; t) s2]++s1
+sameTy :: (Typed t) => t -> t -> Bool
+sameTy = equal `on` typeOf
hunk ./src/Syntax/Type.hs 335
-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)]
+-- TODO : The following functions may not be correct, but it works for now. 
+-- they should use Unifieable, but then I have the Context. Maybe I use the 
+-- standard context as default
+ 
+subsumesTy :: Type -> Type -> Bool
+subsumesTy (VarT _) _ = True 
+subsumesTy (AppT t11 t12) (AppT t21 t22) = 
+    (subsumesTy t11 t21) && (subsumesTy t12 t22)
+subsumesTy (ForallT n1 c1 t1) (ForallT n2 c2 t2)  = 
+    (n1 == (n1 `intersect` n2)) &&
+    (subsumesTy t1 t2) &&
+    (c1 == (intersectBy subsumesTy c1 c2))    
+subsumesTy t1 t2 = equal t1 t2
+
+
+   
hunk ./src/Syntax/Type.hs 352
-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!"
-    -- tuples
-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!"
-    -- lists
-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!"
-    
-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
hunk ./src/Syntax/Type.hs 353
-    where
-    constrOf tv = mapMaybe (\(AppT (ConT c) tv') -> if (tv == tv') then Just c else Nothing)
hunk ./src/Syntax/Type.hs 355
----- 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!"
addfile ./src/Syntax/UnifyExp.hs
hunk ./src/Syntax/UnifyExp.hs 1
+
+module Syntax.UnifyExp (
+    
+    Unify(..), AUnify(..)
+    
+    )where
+
+import Data.Function (on)
+import Data.List (transpose)
+
+import Control.Monad.Error
+
+import Syntax.Class
+import Syntax.Context
+import Syntax.Expressions
+import Syntax.Type
+import Syntax.UnifyTy
+
+import Debug.Trace
+import PrettyPrinter
+
+instance Unify TExp where
+    -- TODO: checkMatch should keep track of which type matches which type
+    --       variable!! (Int,Bool,Int) -//-> (a,b,b), also polymorphic types are+
+    --       not considered
+    -- matching wildcards 
+    match s t@(TWildE i1 _)     = checkMatch s t >> return nullSubst
+    -- matching variables    
+    match s@(TVarE i1 _) t@(TVarE i2 _)     = do 
+        checkMatch s t
+        if i1 == i2 then return nullSubst else return (i2 <~ s)
+    match s          t@(TVarE i _)          = checkMatch s t >> return (i <~ s)    
+    match s t = if sameSymAtRoot s t 
+                  then (matchL `on` subterms) s t
+                  else nomatch "match (215)"  $ (show s) ++ "\n" ++(show t) ++ "\n"
+            
+
+
+    mgu v@(TWildE i1 _) t = checkUnify v t >> varBind v t
+    mgu t v@(TWildE i1 _) = checkUnify t v >> varBind v t
+    mgu v@(TVarE _ _) t   = checkUnify v t >> varBind v t
+    mgu t v@(TVarE _ _)   = checkUnify t v >> varBind v t
+    mgu s t               = if sameSymAtRoot s t 
+                             then (mguL `on` subterms) s t
+                             else nomatch "mgu (226)"  $ (show s) ++ "\n" ++
+                                                         (show t) ++ "\n"
+
+
+
+
+    
+-- | Auxiliary to bind terms to variable, check for consistency 
+varBind (TVarE n _ )(TVarE n' _)| n == n' = return nullSubst
+varBind (TWildE _ _) _                    = return nullSubst -- TODO: ?create substitution?
+varBind (TVarE n _)    t        
+    | n `elem` (getVarNames t)           = fail "varBind: Occurs check failed!"
+    | otherwise                          = return (n <~ t)   
+varBind _ _                              = fail "varBind: Cannot bind to non-variable term"   
+
+instance AUnify TExp where
+    aunify ts = do r <- aunify_ ts
+                   return $ (trace ("AUNI:" ++ "\n " ++ (showp ts) ++ "\n " ++ (showp r))) r
+        
+aunify_ [] = error "aunify: empty list"
+aunify_ t
+    | checkAU t = let l = (map subterms t) in
+                    if [] `elem` l then return . head $ t
+                     else mapM aunify (transpose l) >>= return . (roots t) 
+    | otherwise   = bindVarAU t
+
+checkAU l = (sameRoots l) && not (any isWild l || all isVar l)
+   
+bindVarAU :: (MonadError e m) => [TExp] -> AU m TExp TExp
+bindVarAU img =  getMap >>= (maybe (mkVar img) (return)) . (lookup img)
+     
+mkVar :: (MonadError e m) => [TExp] -> AU m TExp TExp
+mkVar vimg = do 
+    vnm <- getCnt >>= return . mkName . ('a':) . show
+    vty <- lift $ lgg (map typeOf vimg)
+    var <- return $ TVarE  vnm vty
+    putImg var vimg
+    return var  
+    
+nomatch l s = fail $ "Expressions." ++ l ++ ": No Match! " ++ s
addfile ./src/Syntax/UnifyTy.hs
hunk ./src/Syntax/UnifyTy.hs 1
+{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
+module Syntax.UnifyTy (
+
+    Unify(..), AUnify(..),
+    checkMatch, checkUnify, specialise,
+
+) where
+
+import Control.Monad (foldM)
+import Data.Foldable (foldlM)
+import Control.Monad.Error
+import Control.Monad.State
+import Data.Maybe (maybeToList)
+import Data.List (transpose, intersect)
+import Data.Function (on)
+
+import Syntax.Context
+import Syntax.Type
+import Syntax.Class
+
+import PrettyPrinter
+import Logging
+
+type TySubst = Subst Type
+
+
+checkMatch s t = on match typeOf s t >> return ()
+checkUnify s t = on unify typeOf s t >> return ()
+     
+specialise :: (MonadError e m) => Type -> Type -> C m Type
+specialise t1 t2 =
+    (mgu (last . unArrowT $ t2) t1 >>= return . (flip apply t2))
+     `catchError` \_ -> fail "Types not specialisable!"     
+--------------------------------------------------------------------------------
+-- Matching Types
+
+-- | @match t1 t2@ returns the substitution 's', s.t. @apply s t2 == t1@.  
+--   May fail inside 'C' if t2 is _not_ more general than t1.
+instance Unify Type where
+
+    match t (VarT n)                 = return $ n <~ t
+    match t (ForallT _ c (VarT n))   = check (n <~ t) c >> return (n <~ t)
+    match t (ForallT _ c (AppT l r)) = match t (AppT (quantify l c)(quantify r c))
+    match (ForallT _ c (AppT l r)) t = match (AppT (quantify l c)(quantify r c)) t
+    match (AppT l r)(AppT l' r')     = do sl <- match l l'
+                                          sr <- match r r'
+                                          merge sl sr
+    match (TupleT i)(TupleT i') 
+        | i == i'                    = return nullSubst
+    match (ConT n)(ConT n')     
+        | n == n'                    = return nullSubst
+    match ListT ListT                = return nullSubst
+    match ArrowT ArrowT              = return nullSubst
+    match t1 t2                      = fail $ "Type " ++ (show t1) ++
+                                              " does not match " ++ 
+                                              (show t2) ++ "."
+
+    mgu (VarT n) t                 = return $ n <~ t
+    mgu t (VarT n)                 = return $ n <~ t
+    mgu (ForallT _ c (VarT n)) t   = check (n <~ t) c >> return (n <~ t)
+    mgu t (ForallT _ c (VarT n))   = check (n <~ t) c >> return (n <~ t)
+    mgu (ForallT _ c (AppT l r)) t = mgu (AppT (quantify l c)(quantify r c)) t
+    mgu t (ForallT _ c (AppT l r)) = mgu t (AppT (quantify l c)(quantify r c))
+    mgu (AppT l r)(AppT l' r')     = do sl <- mgu l l'
+                                        sr <- mgu r r'
+                                        return $ sl @@ sr
+    mgu (TupleT i)(TupleT i') 
+        | i == i'                  = return nullSubst
+    mgu (ConT n)(ConT n')     
+        | n == n'                  = return nullSubst
+    mgu ListT ListT                = return nullSubst
+    mgu ArrowT ArrowT              = return nullSubst
+    mgu t1 t2                      = fail $ "Type " ++ (show t1) ++
+                                              " and type " ++ (show t2) ++ 
+                                              " do not unify"
+
+
+            
+{- | Check if the current substitution is satisfiable in the given type context.
+     Reduce the type context to head-normal forms first.
+-}
+check :: (MonadError e m) => TySubst -> TyCxt -> C m ()
+check s c = reduce c >>= \c' -> allM (checkit c') s >>= failIfFalse  -- . (ts $ "CHECK :\n" ++ (show s) ++ " in " ++ (show c'))
+    where
+    -- For each predicate in context, which imposes a restriction on the given
+    -- variable in the subtitution, check if the restriction still holds after 
+    -- substitution
+    checkit c (n,t) = allM (satisfies t) (allPreds [n] c)
+    failIfFalse True  = return () 
+    failIfFalse False = fail $ "Substitution " ++ (show s) ++ 
+                               " not satisifieable in " ++ (show c)
+    
+{- | Check if a types satisifies a predicate which is in head-normal form:
+      * a universal quantified variable satisfies any predicate    
+      * a quantified variable satisfies a predicate, if its context entails the 
+        predicate
+      * for any other type we need to check 
+-}        
+satisfies :: (MonadError e m) => Type -> Pred -> C m Bool
+satisfies t@(VarT _) p               = return True
+--    return . (ts $ (show t) ++ " ??1?? " ++ (show p) ++ " | ") $ True
+satisfies t@(ForallT _ c (VarT _)) p =  c `entails` p
+--    c `entails` p >>= return . (ts $ (show t) ++ " ??2?? " ++ (show p) ++ " | ")
+satisfies t p@(AppT (ConT n) _) = getInstances n >>= anyM (flip matches t)
+--    getInstances n >>=  anyM (matches t) >>= return . (ts $ (show t) ++ " ??3?? " ++ (show p) ++ " | ")
+
+
+--
+-- Context Reduction 
+-- e.g. '(Eq a, Eq a)' to 'Eq a' ot 'Eq a, Ord a' tp 'Ord a'
+-- 
+reduce :: (MonadError e m) => TyCxt -> C m TyCxt
+reduce ps = toHnfs ps >>= simplify
+    
+simplify :: (MonadError e m) => TyCxt -> C m TyCxt
+simplify = loop []
+    where
+    loop rs [] = return rs
+    loop rs (p:ps) = do b <- entails (rs ++ ps) p  
+                        if b then loop rs ps else loop (p:rs) ps
+
+toHnfs :: (MonadError e m) => TyCxt -> C m TyCxt
+toHnfs ps  = mapM toHnf ps >>= return . concat
+
+toHnf  :: (MonadError e m) => Pred -> C m TyCxt
+toHnf p
+    | inHnf p   = return [p]
+    | otherwise = byInst p >>= maybe (fail "context reduction") toHnfs
+                            
+inHnf :: Pred -> Bool
+inHnf (AppT (ConT n) t) = hnf t
+    where
+    hnf (VarT _)   = True
+    hnf (AppT t _) = hnf t
+    hnf _          = False
+    
+-- 
+-- Entailment 
+--  
+                           
+entails :: (MonadError e m) => TyCxt -> Pred -> C m Bool
+entails ctx p = do
+     b1 <- mapM bySuper ctx >>= (anyM (`matches` p)) . concat
+     b2 <- byInst p >>= maybe (return False) (allM (entails ctx)) 
+     return (b1 || b2)
+--     return $ (ts $ "CTX: " ++ (show ctx) ++ "\nPRED: " ++ (show p) ++ "\nENT:" ++ (show (b1,b2)) ) $ (b1 || b2)            
+
+-- Given a predicate compute all predicates derivable from SuperClass relations
+bySuper :: (MonadReader Context m) => Pred -> m [Pred]
+bySuper p@(AppT (ConT n) t) =  
+    getSuperClasses n >>= mapM (\n' -> bySuper (AppT (ConT n') t)) >>= 
+     return . (p:) . concat
+--     return $ (ts $ "BySuper: " ++ (show p) ++ " " ) $ p:concat sps
+
+byInst :: (MonadError e m) => Pred -> C m (Maybe [Pred])
+byInst p@(AppT (ConT n) t) = do
+    ins <- getInstances n
+    is <- mapM (tryInst t) ins
+    return $ msum is    
+    
+tryInst :: (MonadError e m) => Pred -> Type -> C m (Maybe [Pred])
+tryInst t (ForallT _ c t') = do u <- match t t'; return $ Just (map (apply u) c)
+                              `catchError` \_ -> return Nothing
+tryInst t        t'        = do _ <- match t t'; return $ Just []
+                              `catchError` \_ -> return Nothing                          
+                               
+ 
+--------------------------------------------------------------------------------
+-- Antiunifying Types
+
+
+instance AUnify Type where
+    aunify [] = error "aunify: empty list"
+    aunify t = let t' = map propCxt t in
+        if sameRoots t'
+        then let l = (map subterms t') in
+             if [] `elem` l then return . head $ t'
+             else mapM aunify (transpose l) >>= return . (roots t) 
+        else bindVar t
+    
+bindVar :: (MonadError e m) => [Type] -> AU m Type Type
+bindVar img =  getMap >>= (maybe (mkVar img) (return)) . (lookup img)
+     
+mkVar :: (MonadError e m) => [Type] -> AU m Type Type
+mkVar vimg = do 
+    vnm <- getCnt >>= return . ('a':) . show
+    cxt <- lift $ cmpCxt vnm vimg
+    var <- return . (flip quantify cxt)  . mkVarT $ vnm
+    putImg var vimg
+    return var
+      
+cmpCxt :: (MonadError e m) => String -> [Type] -> C m TyCxt
+cmpCxt vnm vimg = do
+    insts <- allInstances
+    nms   <- mapM (collectPreds vnm insts) vimg
+    reduce . (foldl1 intersect) $ nms
+    
+collectPreds :: (MonadError e m) => String -> [(Name,[Type])] -> Type -> C m [Pred] 
+collectPreds vnm is (ForallT _ c (VarT _)) = mapM (\(AppT (ConT n) _) -> bySuper $ mkPred n vnm) c >>= return . concat 
+collectPreds vnm is (VarT _) = return . map ((flip mkPred vnm) . fst) $ is 
+collectPreds vnm is t =    
+    filterM ( (anyM (`matches` t)) . snd ) is >>=
+    return . map ((flip mkPred vnm) . fst)
+ 
+--------------------------------------------------------------------------------
+--  Auxiliaries
+                        
+allM :: (Monad m) => (a -> m Bool) -> [a] -> m Bool
+allM p = foldlM (\b a -> liftM (b&&) (p a)) True
+
+anyM :: (Monad m) => (a -> m Bool) -> [a] -> m Bool
+anyM p = foldlM (\b a -> liftM (b||) (p a)) False
+
+
hunk ./src/SynthesisEngine.hs 21
-import Context.SynthesisContext
hunk ./src/SynthesisEngine.hs 24
-import Syntax.Antiunifier
-import Syntax.IFTemplateHaskell
-import Logging 
+
+import Syntax
+import Language.Haskell.TH.Syntax (Exp(..), Pat(..), Dec(..), Clause(..), Body(..))
+
+import Logging
+import PrettyPrinter 
hunk ./src/SynthesisEngine.hs 39
-startSynthesis :: SynCtx -> SCR -> [(Name,Rules)] -> [(Name,Rules)]
+startSynthesis :: Context  -> SCR -> [(Name,[([TExp], TExp)])] -> [(Name,[([TExp], TExp)])]
hunk ./src/SynthesisEngine.hs 42
-    (runLM (synthesise ctx conf tgt bgk) logstate)
+    (withC (runLM (synthesise ctx conf (toRbs tgt)(toRbs bgk)) logstate) ctx)
hunk ./src/SynthesisEngine.hs 46
+    toRbs = (map (\(m,es) -> (m, mkRules es)))
hunk ./src/SynthesisEngine.hs 48
-synthesise :: SynCtx -> SCR -> [(Name,Rules)] -> [(Name,Rules)] -> LM ([(Name,Int)],[[[Dec]]])
+synthesise :: Context -> SCR -> [(Name,Rules)] -> [(Name,Rules)] -> LM ([(Name,Int)],[[[Dec]]])
hunk ./src/SynthesisEngine.hs 60
-    let hs' =  take (fromInteger . scr_maxTiers $ conf) $ map (simplify (scr_simplify conf)) $ hs
+                       
+    bnds  <-  mapM (simplify (scr_simplify conf)) $ hs                 
+    let hs' =  take (fromInteger . scr_maxTiers $ conf) bnds
hunk ./src/SynthesisEngine.hs 66
-    simplify b = map $ concatMap $ if b then snd . simplifiedBindings else allBindings
+    simplify True hs  = lift . lift . lift $ mapM (\h -> mapM simplifiedBindings h >>= return . (map snd) >>= return . concat) hs
+    simplify False hs  = return  (map (concatMap allBindings) hs)
+--        | b = map $ concatMap $ if b then (liftM snd) .  simplifiedBindings else allBindings
+        
hunk ./src/SynthesisEngine.hs 87
-         doLoop . initHSpace
+         lift . lift . lift . lift . initHSpace >>= doLoop
hunk ./src/SynthesisEngine.hs 124
-finishTier ejcts cnds hsp = continue cnds $ pushHypos ejcts hsp
+finishTier ejcts cnds hsp = (lift . lift . lift . lift) (pushHypos ejcts hsp) >>= continue cnds
hunk ./src/SynthesisEngine.hs 128
-    doLoop $ pushHypos ahs $ pushHypos (tail cnds) $ hsp
+    hsp'  <- lift . lift . lift . lift $ (pushHypos (tail cnds) hsp >>= pushHypos ahs)  
+    doLoop hsp' 
hunk ./src/UI/Help.hs 4
+import PrettyPrinter
hunk ./src/UI/UIStarter.hs 27
-import Context.ContextBuilder
-import Syntax.IFTemplateHaskell
+import Syntax
+import Syntax.Specification
+import Language.Haskell.TH.Syntax ( Dec)
hunk ./src/UI/UIStarter.hs 35
-import Logging hiding (integer)
+import Logging
+import PrettyPrinter hiding (integer)
hunk ./src/UI/UIStarter.hs 67
-    , context   :: !ModuleCtx
+    , context   :: !Specification
hunk ./src/UI/UIStarter.hs 80
-examplesInScope = M.toList . mctx_bindings . context
+examplesInScope = (map (\(m,es) -> (m, mkRules es))) . M.toList . spec_bindings . context
hunk ./src/UI/UIStarter.hs 96
-    , context   = defaultContext
+    , context   = defaultSpec
hunk ./src/UI/UIStarter.hs 224
-                 parseContext (context s) p) >>= \(ctx,d) -> 
+                 parseSpec p) >>= \(ctx,d) -> 
hunk ./src/UI/UIStarter.hs 264
-            (res,t) <- time (startSynthesis (mctx_synctx $  context s) newConfig ts bs)
+            (res,t) <- time (startSynthesis (spec_ctx $  context s) newConfig ts bs)