From: pimjager <pim@pimjager.nl>
Date: Thu, 28 Apr 2016 14:51:52 +0000 (+0200)
Subject: Finished algorithm U
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=920ef953a2db44169bd34805233fecbbe334d10e;p=cc1516.git

Finished algorithm U
---

diff --git a/AST.dcl b/AST.dcl
index 5b2bfad..4f65b0e 100644
--- a/AST.dcl
+++ b/AST.dcl
@@ -48,3 +48,4 @@ instance == Op1
 instance == Op2
 instance < Op1
 instance < Op2
+instance == Type
diff --git a/AST.icl b/AST.icl
index 3679b36..68def61 100644
--- a/AST.icl
+++ b/AST.icl
@@ -122,3 +122,6 @@ derive gEq Op1
 instance == Op1 where (==) o1 o2 = gEq{|*|} o1 o2
 instance < Op2 where (<) o1 o2 = toString o1 < toString o2
 instance < Op1 where (<) o1 o2 = toString o1 < toString o2
+
+derive gEq Type
+instance == Type where (==) t1 t2 = gEq{|*|} t1 t2
\ No newline at end of file
diff --git a/sem.icl b/sem.icl
index 3b5d15d..17c9040 100644
--- a/sem.icl
+++ b/sem.icl
@@ -33,6 +33,7 @@ import AST
 :: SemError
 	= ParseError Pos String 
 	| UnifyError Pos Type Type 
+    | InfiniteTypeError Pos Type
     | FieldSelectorError Pos Type FieldSelector 
 	| OperatorError Pos Op2 Type
     | UndeclaredVariableError Pos String
@@ -141,12 +142,33 @@ instance Typeable Gamma where
     subst s gamma   = Mapmap (subst s) gamma
 
 //// ------------------------
-//// algorithm U, Unification (outside of Monad)
+//// algorithm U, Unification 
 //// ------------------------
 instance zero Substitution where zero = 'Map'.newMap
+
 compose :: Substitution Substitution -> Substitution
-compose s1 s2 = undef
-//unify :: 
+compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
+//Note: unlike function composition, compose prefers left!
+
+occurs :: TVar a -> Bool | Typeable a
+occurs tvar a = elem tvar (ftv a)
+
+unify :: Type Type -> Either SemError Substitution
+unify t1=:(IdType tv) t2 = unify t2 t1
+unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
+                            | occurs tv t1 = Left $ InfiniteTypeError zero t1
+                            | otherwise = Right $ 'Map'.singleton tv t1
+unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
+                                unify tb1 tb2 >>= \s2->
+                                Right $ compose s1 s2
+unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
+                                                    unify ta2 tb2 >>= \s2->
+                                                    Right $ compose s1 s2
+unify (ListType t1) (ListType t2) = unify t1 t2
+unify t1 t2 | t1 == t2  = Right zero
+            | otherwise = Left $ UnifyError zero t1 t2
+
+