From: pimjager 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 + +