hi

[cc1516.git] / sem.icl

diff --git a/sem.icl b/sem.icl
index 3b5d15d..1c4f345 100644 (file)
--- a/sem.icl
+++ b/sem.icl
@@ -7,6 +7,7 @@ from StdFunc import o, flip, const, id
 
 import Control.Monad
 import Control.Monad.Trans
+//import Control.Monad.State
 import Data.Either
 import Data.Maybe
 import Data.Monoid
@@ -33,6 +34,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
@@ -43,7 +45,7 @@ import AST
 instance zero Gamma where
        zero = 'Map'.newMap
 
-variableStream :: [String]
+variableStream :: [TVar]
 variableStream = map toString [1..]
 
 sem :: AST -> Either [SemError] Constraints
@@ -141,12 +143,40 @@ 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
+
+//// ------------------------
+//// Algorithm M, Inference and Solving
+//// ------------------------
+//:: Typing a :== StateT (Gamma, [TVar]) Either a
+
+//map a schemes type variables to variables with fresh names
+//i.e. a->[b] becomes c->[d]
+