Fix bug in apply checking

[minfp.git] / check.icl

diff --git a/check.icl b/check.icl
index 5b0cc18..76cde8c 100644 (file)
--- a/check.icl
+++ b/check.icl
@@ -9,35 +9,30 @@ import Control.Monad.Writer
 import Data.Either
 import Data.Func
 import Data.List
+import Data.Tuple
 import Data.Map => qualified put, union, difference, find, updateAt
 import Data.Maybe
-import Data.Tuple
 import Text
 
 import ast, scc
 
-import Text.GenPrint
-import StdDebug
-
 check :: [Function] -> Either [String] (Expression, [([Char], Scheme)])
 check fs
        # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
        | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
        = case partition (\a->a=:(Function ['start'] _ _)) fs of
                ([], _) = Left ["No start function defined"]
-               ([Function _ [] e], fs)
-                       = (\x->(e, x)) <$> runInfer (infer preamble (makeExpression fs e))
-               ([Function _ _ _], _) = Left ["Start cannot have arguments"]
+               ([Function _ [] e:_], fs) = (\x->(e, x)) <$> runInfer (infer preamble (makeExpression fs e))
+               ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
 
 makeExpression :: [Function] Expression -> Expression
-makeExpression fs start
-       = foldr mkExpr start $ scc [(l, vars e [])\\(l, e)<-nicefuns]
+makeExpression fs start = foldr mkExpr start $ scc [(l, vars e [])\\(l, e)<-nicefuns]
 where
        mkExpr :: [[Char]] -> (Expression -> Expression)
        mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
 
        nicefuns :: [([Char], Expression)]
-       nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
+       nicefuns = [(l, foldr (\x c->Lambda x o c) id i e)\\(Function l i e)<-fs]
 
        vars :: Expression [[Char]] -> [[Char]]
        vars (Var v=:[m:_]) c = [v:c]
@@ -56,7 +51,7 @@ instance toString Type where
        toString (TVar a) = toString a
        toString TInt = "Int"
        toString TBool = "Bool"
-       toString (a --> b) = concat ["(", toString a, ") -> ", toString b]
+       toString (a --> b) = concat ["(", toString a, " -> ", toString b, ")"]
 
 :: TypeEnv :== Map [Char] Scheme
 preamble :: TypeEnv
@@ -71,6 +66,7 @@ preamble = fromList
 :: Subst :== Map [Char] Type
 
 :: Infer a :== StateT [Int] (WriterT [([Char], Scheme)] (Either [String])) a
+
 runInfer :: (Infer (Subst, Type)) -> Either [String] [([Char], Scheme)]
 runInfer i = case runWriterT (evalStateT i [0..]) of
        Left e = Left e
@@ -143,15 +139,14 @@ generalize env t = Forall (difference (ftv t) (ftv env)) t
 infer :: TypeEnv Expression -> Infer (Subst, Type)
 infer env (Lit (Int _)) = pure (newMap, TInt)
 infer env (Lit (Bool _)) = pure (newMap, TBool)
-infer env (Var x) = case get x env of
-       Nothing = err ["Unbound variable: ", toString x]
-       Just s = (\x->(newMap, x)) <$> instantiate s
+infer env (Var x) = maybe (err ["Unbound variable: ", toString x])
+       (\s->tuple newMap <$> instantiate s) $ get x env
 infer env (App e1 e2)
        =              fresh
        >>= \tv->      infer env e1
        >>= \(s1, t1)->infer (apply s1 env) e2
        >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
-       >>= \s3->      pure (s1 oo s2 oo s3, apply s3 tv)
+       >>= \s3->      pure (s3 oo s2 oo s1, apply s3 tv)
 infer env (Lambda x b)
        =              fresh
        >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
@@ -160,7 +155,8 @@ infer env (Lambda x b)
 //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)
+//     >>= \(s2, t2)->liftT (tell [(x, Forall [] t1)])
+//     >>|            pure (s1 oo s2, t2)
 //Single recursion
 //infer env (Let [(x, e1)] e2)
 //     =              fresh
@@ -176,6 +172,6 @@ infer env (Let xs e2)
                       in  unzip <$> sequence (map (infer env`) bs)
        >>= \(ss,ts)-> unifyl ts
        >>= \s->       liftT (tell [(n, generalize (apply s env`) t)\\t<-ts & n<-ns])
-       >>|            let env`` = foldr (\(n, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip2 ns ts)
+       >>|            let env`` = foldr (\(n, s, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip3 ns ss ts)
                       in infer env`` e2
        >>= \(s2, t2)->pure (s oo s2, t2)