[keep track of types when unify Expressions
martin.hofmann@uni-bamberg.de**20091007092044
 Only check for type consistency when variables are involved. Improved matching/unification of types implemented. However, this is far from beeing perfect.
] hunk ./src/Syntax/Expressions.hs 239
+    -- TODO: checkMatch should keep track of which type matches which type
+    --       variable!! (Int,Bool,Int) -//-> (a,b,b), also polymorphic types are+
+    --       not considered
hunk ./src/Syntax/Expressions.hs 243
-    -- TODO: ?create subst
-    match s@(TWildE i1 _) t     = nomatch "match" --checkMatch s t >> return ()
-    match s t@(TWildE i1 _)     = checkMatch s t >> return ()
+    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 ()
hunk ./src/Syntax/Expressions.hs 247
-        checkMatch s t
+        checkMatch s t >> matchVar s t
hunk ./src/Syntax/Expressions.hs 249
-        matchVar s t
-    match s@(TVarE _ _) t                   = nomatch "match"
-    match s          t@(TVarE _ _)          = checkMatch s t >> 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
hunk ./src/Syntax/Expressions.hs 253
-        checkMatch s t 
-        if (ns == nt) then return () else nomatch "match" 
+        if (ns == nt) then return () else nomatch "match (253)" 
hunk ./src/Syntax/Expressions.hs 257
-        if (l1 == l2) then return () else nomatch "match"
+        if (l1 == l2) then return () else nomatch "match (257)"
hunk ./src/Syntax/Expressions.hs 259
-    match s@(TTupE sl _)         t@(TTupE tl _)     = do
-        checkMatch s t
+    match s@(TTupE sl _)         t@(TTupE tl _)     =
hunk ./src/Syntax/Expressions.hs 261
-    match s@(TTupE sl _)         t@(TAppE _ _ _)    = do
-        checkMatch s t 
+    match s@(TTupE sl _)         t@(TAppE _ _ _)    = 
hunk ./src/Syntax/Expressions.hs 264
-            _owise               -> nomatch "match"
-    match t@(TAppE _ _ _)        s@(TTupE sl _)    = do
-        checkMatch s t      
+            _owise               -> nomatch "match (263)"
+    match t@(TAppE _ _ _)        s@(TTupE sl _)    =
hunk ./src/Syntax/Expressions.hs 268
-            _owise             -> nomatch "match"
+            _owise             -> nomatch "match (268)"
hunk ./src/Syntax/Expressions.hs 270
-    match s@(TListE [] _)        t@(TListE [] _)    = checkMatch s t >> return ()
-    match s@(TListE (se:sl) st)  t@(TListE (te:tl) tt)  = 
-        checkMatch s t >> match se te >> match (TListE sl st) (TListE tl tt)
+    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)
hunk ./src/Syntax/Expressions.hs 275
-    match s@(TListE [] _)        t@(TConE n _)        = do
-        checkMatch s t >> if isNil n then return () else nomatch "match"
-    match s@(TConE n _)          t@(TListE [] _)        = do
-        checkMatch s t >> if isNil n then return () else nomatch "match"
-    match s@(TListE (se:sl) st)  t@(TAppE _ _ _) = do
-        checkMatch s t
+    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 _ _ _) =
hunk ./src/Syntax/Expressions.hs 283
-            _owise       -> flush "No Match!"  
-    match t@(TAppE _ _ _)        s@(TListE (se:sl) st)       = do
-        checkMatch s t
+            _owise       -> nomatch "match (282)"
+    match t@(TAppE _ _ _)        s@(TListE (se:sl) st)       =
hunk ./src/Syntax/Expressions.hs 288
-            _owise       -> nomatch "match"
-    match s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  = do
-        checkMatch s t
+            _owise       -> nomatch "match (288)"
+    match s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  =
hunk ./src/Syntax/Expressions.hs 292
-           else nomatch ("match1" ++ (show.pretty $  n))
-    match t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  = do
-        checkMatch t s
+           else nomatch ("match (292)" ++ (show.pretty $  n))
+    match t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  =
hunk ./src/Syntax/Expressions.hs 295
-           then match te se >> match tl (TListE sl st)
-           else nomatch "match2"
+          then match te se >> match tl (TListE sl st)
+          else nomatch "match (296)"
hunk ./src/Syntax/Expressions.hs 299
-        checkMatch s t >> match s1 t1 >> match s2 t2
+        match s1 t1 >> match s2 t2
hunk ./src/Syntax/Expressions.hs 301
-    match s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
-        checkMatch s t
-        if ( equal s2 t2) then match s1 t1 >> match s3 t3
-          else nomatch "match"
+    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"
hunk ./src/Syntax/Expressions.hs 305
-    match s t = nomatch $ "match\n" ++ (show s) ++ "\n" ++ (show t)
+    match s t = nomatch $ "match\n" ++ (showp s) ++ "\n" ++ (showp t)
hunk ./src/Syntax/Expressions.hs 313
-    unify s@(TWildE i1 _) t     = checkUnify s t >> return ()
-    unify s t@(TWildE i1 _)     = checkUnify s t >> return ()    
+    unify s@(TWildE i1 _) t     = checkSubsume s t >> return ()
+    unify s t@(TWildE i1 _)     = checkMatch s t >> return ()    
hunk ./src/Syntax/Expressions.hs 316
-        checkUnify s t
+        (checkSubsume s t) `mplus` (checkMatch s t)
hunk ./src/Syntax/Expressions.hs 318
-    unify s@(TVarE _ _) t                   = checkUnify s t >> unifyVar s t
-    unify s          t@(TVarE _ _)          = flush "Not unifiable"  
+    unify s@(TVarE _ _) t                   = checkSubsume s t >> unifyVar s t
+    unify s          t@(TVarE _ _)          = checkMatch s t >> unifyVar s t 
hunk ./src/Syntax/Expressions.hs 321
-    unify s@(TConE ns _) t@(TConE nt _)     = do
-        checkUnify s t 
-        if (ns == nt) then return () else flush "Not unifiable"  
+    unify s@(TConE ns _) t@(TConE nt _)     =
+        if (ns == nt) then return () else flush "Not unifiable (322)"  
hunk ./src/Syntax/Expressions.hs 324
-    unify s@(TLitE l1 _) t@(TLitE l2 _)     = do
-        checkUnify s t
-        if (l1 == l2) then return () else flush "Not unifiable"  
+    unify s@(TLitE l1 _) t@(TLitE l2 _)     =
+        if (l1 == l2) then return () else flush "Not unifiable (325)"  
hunk ./src/Syntax/Expressions.hs 327
-    unify s@(TTupE sl _) t@(TTupE tl _)     = do
-        checkUnify s t
-        mapM_ (uncurry unify) (zip sl tl)
-    unify s@(TTupE sl _) t@(TAppE _ _ _)    = do
-        checkUnify s t 
+    unify s@(TTupE sl _) t@(TTupE tl _)     = mapM_ (uncurry unify) (zip sl tl)
+    unify s@(TTupE sl _) t@(TAppE _ _ _)    =
hunk ./src/Syntax/Expressions.hs 331
-            _owise               -> flush "Not unifiable"  
-    unify t@(TAppE _ _ _) s@(TTupE sl _)    = do
-        checkUnify s t      
+            _owise               -> flush "Not unifiable (345)"  
+    unify t@(TAppE _ _ _) s@(TTupE sl _)    =
hunk ./src/Syntax/Expressions.hs 335
-            _owise             -> flush "Not unifiable"  
+            _owise             -> flush "Not unifiable (345)"  
hunk ./src/Syntax/Expressions.hs 337
-    unify s@(TListE [] _) t@(TListE [] _)    = checkUnify s t >> return ()
-    unify s@(TListE (se:sl) st) t@(TListE (te:tl) tt)  = 
-        checkUnify s t >> unify se te >> unify (TListE sl st) (TListE tl tt)
+    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)
hunk ./src/Syntax/Expressions.hs 342
-    unify s@(TListE [] _) t@(TConE n _)        = do
-        checkUnify s t >> if isNil n then return () else flush "Not unifiable"    
-    unify s@(TConE n _) t@(TListE [] _)        = do
-        checkUnify s t >> if isNil n then return () else flush "Not unifiable"   
-    unify s@(TListE (se:sl) st) t@(TAppE _ _ _) = do
-        checkUnify s t
+    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 _ _ _) =
hunk ./src/Syntax/Expressions.hs 350
-            _owise       -> flush "Not unifiable"  
-    unify t@(TAppE _ _ _) s@(TListE (se:sl) st)       = do
-        checkUnify s t
+            _owise       -> flush "Not unifiable (354)"  
+    unify t@(TAppE _ _ _) s@(TListE (se:sl) st)       =
hunk ./src/Syntax/Expressions.hs 355
-            _owise       -> flush "No unifiable!"  
-    unify s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  = do
-        checkUnify s t
+            _owise       -> flush "No unifiable (355)"  
+    unify s@(TListE (se:sl) st) t@(TInfixE te (TConE n _) tl _)  =
hunk ./src/Syntax/Expressions.hs 359
-           else flush "Not unifiable"
-    unify t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  = do
-        checkUnify s t
+           else flush "Not unifiable (359)"
+    unify t@(TInfixE te (TConE n _) tl _) s@(TListE (se:sl) st)  =
hunk ./src/Syntax/Expressions.hs 363
-           else flush "Not unifiable"
+           else flush "Not unifiable (363)"
hunk ./src/Syntax/Expressions.hs 365
-    unify s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = 
-        checkUnify s t >> unify s1 t1 >> unify s2 t2
+    unify s@(TAppE s1 s2 _) t@(TAppE t1 t2 _)     = unify s1 t1 >> unify s2 t2
hunk ./src/Syntax/Expressions.hs 367
-    unify s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = do
-        checkUnify s t
+    unify s@(TInfixE s1 s2 s3 _) t@(TInfixE t1 t2 t3 _) = 
hunk ./src/Syntax/Expressions.hs 369
-          else flush "Not unifiable"         
-    unify s@(TCondE s1 s2 s3 _) t@(TCondE t1 t2 t3 _) = 
-        checkUnify s t >> unify s1 t1 >> unify s2 t2 >> unify s3 t3    
-    unify s t                               = flush "Not unifiable!"
+          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)"
hunk ./src/Syntax/Expressions.hs 384
-            Just val -> checkSame v val >> return val
+            Just val -> return val -- checkSame v val >> return val
hunk ./src/Syntax/Expressions.hs 520
-liftUnify :: (Unifiable t, Monad m) => Maybe t -> Maybe t -> U m t
+liftUnify :: (Unifiable t, MonadPlus m) => Maybe t -> Maybe t -> U m t
hunk ./src/Syntax/Expressions.hs 524
-liftMatch :: (Unifiable t, Monad m) => Maybe t -> Maybe t -> U m t
+liftMatch :: (Unifiable t, MonadPlus m) => Maybe t -> Maybe t -> U m t
hunk ./src/Syntax/Expressions.hs 558
-    collectSubterms :: (Monad m) => TExp -> TExp -> m [TExp]        
+    collectSubterms :: (MonadPlus m) => TExp -> TExp -> m [TExp]        
hunk ./src/Syntax/Expressions.hs 565
-    collectSubterms s@(TListE (x:xs) _) t@(TListE (l:ls) ty) = 
+    collectSubterms s@(TListE (x:xs) _) t@(TListE (l:ls) ty) =  
hunk ./src/Syntax/Expressions.hs 816
-
+-- [a]::[a]
hunk ./src/Syntax/Expressions.hs 818
-rhs1 = TListE [TVarE (mkName "b") (VarT (mkName "a")),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]
hunk ./src/Syntax/Expressions.hs 822
+-- (x0:x1)::[a]
hunk ./src/Syntax/Expressions.hs 831
-               
+
+-- [[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")))) 
hunk ./src/Syntax/Patterns.hs 211
-        checkUnify s t 
+        (checkSubsume s t) `mplus` (checkMatch s t)
hunk ./src/Syntax/Patterns.hs 215
-    unify s@(TLitP sl _)           t@(TLitP tl _)          = do
-        checkUnify s t
+    unify s@(TLitP sl _)           t@(TLitP tl _)          =
hunk ./src/Syntax/Patterns.hs 217
-    unify s@(TListP [] _)          t@(TListP [] _)         = do 
-        checkUnify s t ; return ()
+    unify s@(TListP [] _)          t@(TListP [] _)         = return ()
hunk ./src/Syntax/Patterns.hs 219
-        checkUnify s t >> unify se te >> unify (TListP ss st) (TListP ts tt) 
+        unify se te >> unify (TListP ss st) (TListP ts tt) 
hunk ./src/Syntax/Patterns.hs 222
-    unify s@(TListP [] _)          t@(TConP n [] _)        = do
-        checkUnify s t 
+    unify s@(TListP [] _)          t@(TConP n [] _)        =
hunk ./src/Syntax/Patterns.hs 224
-    unify s@(TConP n [] _) t@(TListP [] _)                 = do
-        checkUnify s t 
+    unify s@(TConP n [] _) t@(TListP [] _)                 =
hunk ./src/Syntax/Patterns.hs 226
-    unify s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = do
-        checkUnify s t
+    unify s@(TListP (se:ss) st)    t@(TConP n ([te,ts]) _) = 
hunk ./src/Syntax/Patterns.hs 230
-    unify s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   = do
-        checkUnify s t
+    unify s@(TConP n ([se,ss]) _)  t@(TListP (te:ts) tt)   =
hunk ./src/Syntax/Patterns.hs 234
-    unify s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       = do
-        checkUnify s t
+    unify s@(TConP n1 p1 _)        t@(TConP n2 p2 _)       =
hunk ./src/Syntax/Patterns.hs 238
-    unify s@(TTupP sl _)           t@(TTupP tl _)          = do
-        checkUnify s t
+    unify s@(TTupP sl _)           t@(TTupP tl _)          =
hunk ./src/Syntax/Patterns.hs 240
-    unify s@(TConP n sl _)         t@(TTupP tl _)          = do
-        checkUnify s t
+    unify s@(TConP n sl _)         t@(TTupP tl _)          =
hunk ./src/Syntax/Patterns.hs 244
-    unify s@(TTupP sl _)           t@(TConP n tl _)        = do
-        checkUnify s t
+    unify s@(TTupP sl _)           t@(TConP n tl _)        =
hunk ./src/Syntax/Patterns.hs 248
-    unify s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  = do
-        checkUnify s t
+    unify s@(TInfixP s1 s2 s3 _)   t@(TInfixP t1 t2 t3 _)  =
hunk ./src/Syntax/Patterns.hs 356
-    collectSubterms :: (Monad m) => TPat -> TPat -> m [TPat]
+    collectSubterms :: (MonadPlus m) => TPat -> TPat -> m [TPat]
hunk ./src/Syntax/Types.hs 10
-    checkMatch, checkUnify, checkSame,
+    checkMatch, checkSubsume, checkSame,
hunk ./src/Syntax/Types.hs 21
+import Control.Monad
hunk ./src/Syntax/Types.hs 65
---isGeneralTy :: (Typed t) => t -> t -> Bool
---isGeneralTy = sameTy 
+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
+
hunk ./src/Syntax/Types.hs 102
-checkTys :: (Typed t, Monad m) =>
+checkTys :: (Show t, Pretty t, Typed t, Monad m) =>
hunk ./src/Syntax/Types.hs 105
-    | c t s = return ()
-    | otherwise  = f "Type mismatch"
+    | c s t = return ()
+    | otherwise  = f $ "Type mismatch " ++ 
+                       ((showp $ s)) ++ "  " ++ 
+                       ((showp $ t))
hunk ./src/Syntax/Types.hs 112
-checkMatch,checkUnify,checkSame :: (Typed t, Monad m) => t -> t -> m ()   
-checkMatch = checkTys sameTy fail
-checkUnify = checkTys sameTy fail       
+checkMatch,checkSubsume,checkSame :: (Show t, Pretty t, Typed t, MonadPlus m) => t -> t -> m ()   
+checkMatch = checkTys ((flip subsumesTy) `on` typeOf)  fail
+checkSubsume = checkTys (subsumesTy `on` typeOf)  fail -- (subsumesTy `on` typeOf) fail       
hunk ./src/Syntax/Unifier.hs 71
-    unify ::  (Monad m) => t -> t -> U m t
+    unify ::  (MonadPlus m) => t -> t -> U m t
hunk ./src/Syntax/Unifier.hs 73
-    mgu ::  (Monad m) => t -> t -> m (Substitution t)
+    mgu ::  (MonadPlus m) => t -> t -> m (Substitution t)
hunk ./src/Syntax/Unifier.hs 87
-    match :: (Monad m) =>  t -> t -> U m t
+    match :: (MonadPlus m) =>  t -> t -> U m t
hunk ./src/Syntax/Unifier.hs 92
-    matchesWithSubs :: (Monad m) =>  t -> t -> m (Substitution t)  
+    matchesWithSubs :: (MonadPlus m) =>  t -> t -> m (Substitution t)  
hunk ./src/Syntax/Unifier.hs 136
-matchVar :: (Unifiable t, Monad m) => t -> t -> U m t
+matchVar :: (Unifiable t, MonadPlus m) => t -> t -> U m t
hunk ./src/Syntax/Unifier.hs 150
-unifyVar :: (Unifiable t, Monad m) => t -> t -> U m t
+unifyVar :: (Unifiable t, MonadPlus m) => t -> t -> U m t
hunk ./src/Syntax/Unifier.hs 174
-                                        then flush "Not unifiable"
+                                        then flush "unifyVar:Not unifiable"
hunk ./src/Syntax/Unifier.hs 206
-matchLs :: (Unifiable t, Monad m) => [t] -> [t] -> U m t
+matchLs :: (Unifiable t, MonadPlus m) => [t] -> [t] -> U m t
hunk ./src/Syntax/Unifier.hs 212
-unifyLs :: (Unifiable t, Monad m) => [t] -> [t] -> U m t
+unifyLs :: (Unifiable t, MonadPlus m) => [t] -> [t] -> U m t
hunk ./src/Syntax/Unifier.hs 218
-matchesWithSubsLs :: (Unifiable t, Monad m ) => [t] -> [t]  -> m (Substitution t)
+matchesWithSubsLs :: (Unifiable t, MonadPlus m ) => [t] -> [t]  -> m (Substitution t)