interpret

[minfp.git] / check.icl

diff --git a/check.icl b/check.icl
index 3800632..68d258a 100644 (file)
--- a/check.icl
+++ b/check.icl
@@ -22,7 +22,7 @@ check fs
                ([], _) = Left ["No start function defined"]
                ([Function _ [] e], fs)
                        # e = foldr (\(Function i a e)->Let i (foldr ((o) o Lambda) id a e)) e fs
-                       = (\x->(e, x)) <$> runInfer (infer newMap e)
+                       = (\x->(e, x)) <$> runInfer (infer preamble e)
                ([Function _ _ _], _) = Left ["Start cannot have arguments"]
 
 instance toString Scheme where
@@ -32,9 +32,18 @@ instance toString Type where
        toString (TVar a) = toString a
        toString TInt = "Int"
        toString TBool = "Bool"
-       toString (TFun a b) = concat ["(", toString a, ") -> ", toString b]
+       toString (a --> b) = concat ["(", toString a, ") -> ", toString b]
 
 :: TypeEnv :== Map [Char] Scheme
+preamble :: TypeEnv
+preamble = fromList
+       [(['_if'],  Forall [['_ift']]
+               $ TBool --> TVar ['_ift'] --> TVar ['_ift'] --> TVar ['_ift'])
+       ,(['_eq'],  Forall [['_eq']] $ TInt --> TInt --> TBool)
+       ,(['_mul'], Forall [['_mul']] $ TInt --> TInt --> TInt)
+       ,(['_add'], Forall [['_add']] $ TInt --> TInt --> TInt)
+       ,(['_sub'], Forall [['_sub']] $ TInt --> TInt --> TInt)
+       ]
 :: Subst   :== Map [Char] Type
 
 :: Infer a :== StateT [Int] (Either [String]) a
@@ -45,8 +54,8 @@ runInfer i = uncurry ((o) (generalize newMap) o apply)
 fresh :: Infer Type
 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
 
-compose :: Subst Subst -> Subst
-compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
+(oo) infixr 9 :: Subst Subst -> Subst
+(oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
 
 class Substitutable a where
        apply :: Subst a -> a
@@ -54,11 +63,11 @@ class Substitutable a where
 
 instance Substitutable Type where
        apply s t=:(TVar v) = fromMaybe t (get v s)
-       apply s (TFun t1 t2) = on TFun (apply s) t1 t2
+       apply s (t1 --> t2) = apply s t1 --> apply s t2
        apply _ x = x
        
        ftv (TVar v) = [v]
-       ftv (TFun t1 t2) = on union ftv t1 t2
+       ftv (t1 --> t2) = on union ftv t1 t2
        ftv _ = []
 
 instance Substitutable Scheme where
@@ -77,22 +86,20 @@ occursCheck :: [Char] -> (a -> Bool) | Substitutable a
 occursCheck a = isMember a o ftv
 
 unify :: Type Type -> Infer Subst
-unify (TFun l r) (TFun l` r`)
+unify (l --> r) (l` --> r`)
        =        unify l l`
        >>= \s1->on unify (apply s1) r r`
-       >>= \s2->pure (compose s1 s2)
-unify (TVar a) t = bind a t
-unify t (TVar a) = bind a t
+       >>= \s2->pure (s1 oo s2)
+unify (TVar a) (TVar t)
+       | a == t = pure newMap
+unify (TVar a) t
+       | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " to ", toString t])
+       = pure (singleton a t)
+unify t (TVar a) = unify (TVar a) t
 unify TInt TInt = pure newMap
 unify TBool TBool = pure newMap
 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
 
-bind :: [Char] Type -> Infer Subst
-bind a (TVar t) | a == t = pure newMap
-bind a t
-       | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
-       = pure (singleton a t)
-
 instantiate :: Scheme -> Infer Type
 instantiate (Forall as t)
        =         sequence [fresh\\_<-as]
@@ -111,14 +118,18 @@ infer env (App e1 e2)
        =              fresh
        >>= \tv->      infer env e1
        >>= \(s1, t1)->infer (apply s1 env) e2
-       >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
-       >>= \s3->      pure (compose (compose s3 s2) s1, apply s3 tv)
+       >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
+       >>= \s3->      pure (s1 oo s2 oo s3, apply s3 tv)
 infer env (Lambda x b)
        =              fresh
        >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
-       >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
-infer env (Builtin c a) = undef
+       >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
+//infer env (Let x e1 e2)
+//     =              infer env e1
+//     >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
+//     >>= \(s2, t2)->pure (s1 oo s2, t2)
 infer env (Let x e1 e2)
-       =              infer env e1
-       >>= \(s1, t1)->let env` = apply s1 env in infer ('Data.Map'.put x (generalize env` t1) env) e2
-       >>= \(s2, t2)->pure (compose s1 s2, t2)
+       =              fresh
+       >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) e1
+       >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
+       >>= \(s2, t2)->pure (s1 oo s2, t2)