From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 19 Mar 2019 07:37:20 +0000 (+0100)
Subject: Fix bug in apply checking
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4c442297f7f0eff966e60e31597d73b2a1ba0f79;p=minfp.git

Fix bug in apply checking
---

diff --git a/check.icl b/check.icl
index 5b0cc18..76cde8c 100644
--- 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)
diff --git a/parse.icl b/parse.icl
index a2c3103..8dc29af 100644
--- a/parse.icl
+++ b/parse.icl
@@ -86,7 +86,7 @@ pChainr :: (Parser (a a -> a)) (Parser a) -> Parser a
 pChainr op p = flip ($) <$> p <*> (flip <$> op <*> pChainr op p) <|> p
 
 parse :: [Token] -> Either [String] [Function]
-parse ts = fst <$> runStateT (pAST <* pEof) {tokens=ts, ifxs=[]}
+parse ts = fst <$> runStateT (reverse <$> pAST <* pEof) {tokens=ts, ifxs=[]}
 where
 	pAST :: Parser [Function]
 	pAST = many pFunction >>= mapM \(id, args, body)->Function id args <$
diff --git a/tests/preamble.mfp b/tests/preamble.mfp
index b06bc68..8f579a1 100644
--- a/tests/preamble.mfp
+++ b/tests/preamble.mfp
@@ -10,6 +10,7 @@ $ ifxr 0 x y = x y;
 + ifxl 6 = code add;
 
 on f g a b = f (g a) (g b);
+onn = \f. \g. \a. \b. f (g a) (g b);
 
 //Conditional operators
 if = code if;
@@ -20,4 +21,5 @@ id x = x;
 even i = if (i == 0) True (odd (i - 1));
 odd i = if (i == 0) False (even (i - 1));
 
-start = on;
+//start = on;
+start = \f. \g. \a. \b. f (g a) (g b);