From d3ca5469085b22eb6d627484894a094116b922a8 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 14 Mar 2019 14:03:21 +0100
Subject: [PATCH] typing

---
 ast.dcl            |  3 ++-
 ast.icl            |  6 +++---
 check.icl          | 24 ++++++++++++++++++------
 int.icl            | 46 ++++++++++++++++++++++++----------------------
 tests/preamble.mfp | 10 +++++++++-
 5 files changed, 56 insertions(+), 33 deletions(-)

diff --git a/ast.dcl b/ast.dcl
index 7dd17d7..4dfad17 100644
--- a/ast.dcl
+++ b/ast.dcl
@@ -17,6 +17,7 @@ from int import :: Eval
 :: Value
 	= Int Int
 	| Bool Bool
-	| Func (Expression -> Eval Value)
+	| Lambda` [Char] Expression
+	| Builtin (Expression -> Eval Expression)
 
 instance toString Function, Expression, Value
diff --git a/ast.icl b/ast.icl
index 1a4d7c1..5579c3b 100644
--- a/ast.icl
+++ b/ast.icl
@@ -14,12 +14,12 @@ instance toString Expression where
 	toString (App l r) = concat ["(", toString l, " ", toString r, ")"]
 	toString (Lambda a e) = concat ["(\\", toString a, ".", toString e, ")"]
 	toString (Let ns r) = concat
-		[ "let\n"
-		, concat [concat ["\t", toString n, " = ", toString v, "\n"]\\(n, v)<-ns]
+		[ "let ", concat [concat ["\t", toString n, " = ", toString v, "\n"]\\(n, v)<-ns]
 		, "in\n", toString r]
 	toString _ = abort "toString Expression not implemented"
 
 instance toString Value where
 	toString (Int i) = toString i
 	toString (Bool b) = toString b
-	toString (Func a) = concat ["Function "]
+	toString (Lambda` v a) = toString (Lambda v a)
+	toString (Builtin a) = "builtin"
diff --git a/check.icl b/check.icl
index abff97a..2cc76ac 100644
--- a/check.icl
+++ b/check.icl
@@ -129,9 +129,21 @@ infer env (Lambda x b)
 //	=              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)
-	=              fresh
-	>>= \tv->      let env` = 'Data.Map'.put x (Forall [] tv) env
-	               in 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)
+//	=              fresh
+//	>>= \tv->      let env` = 'Data.Map'.put x (Forall [] tv) env
+//	               in infer env` e1
+//	>>= \(s1,t1)-> unify t1 tv
+//	>>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
+//	>>= \(s2, t2)->pure (s1 oo s2, t2)
+infer env (Let xs e2)
+	# (ns, bs) = unzip xs
+	=              sequence [fresh\\_<-ns]
+	>>= \tvs->     let env` = foldr (uncurry putenv) env (zip2 ns tvs)
+	               in unzip <$> sequence (map infer env`) bs
+	>>= \(ss,ts)-> unify t1 tv
+//	>>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
+//	>>= \(s2, t2)->pure (s1 oo s2, t2)
+where
+	putenv :: [Char] -> (Type TypeEnv -> TypeEnv)
+	putenv k = 'Data.Map'.put k o Forall []
diff --git a/int.icl b/int.icl
index 475e9b4..5467559 100644
--- a/int.icl
+++ b/int.icl
@@ -13,35 +13,37 @@ import Control.Monad.Trans
 
 import ast
 
-:: Eval a :== StateT EvalState (Either [String]) a
-:: EvalState :== [([Char], Value)]
+:: Eval a :== StateT [([Char], Value)] (Either [String]) a
 
 int :: Expression -> Either [String] Value
 int e = evalStateT (eval e)
-	[(['_if'], Func \i->pure (Func \t->pure (Func \e->eval i >>= \(Bool b)->if b (eval t) (eval e))))
-	,(['_eq'],  binop \(Int i) (Int j)->Bool (i==j))
-	,(['_sub'], binop \(Int i) (Int j)->Int  (i-j))
-	,(['_add'], binop \(Int i) (Int j)->Int  (i+j))
-	,(['_mul'], binop \(Int i) (Int j)->Int  (i*j))
-	,(['_div'], binop \(Int i) (Int j)->Int  (i/j))
+	[(['_if'], Builtin \i->pure (Lit (Builtin \t->pure (Lit (Builtin \e->
+		eval i >>= \(Bool b)->pure (if b t e))))))
+	,(['_eq'],  binop \(Int i) (Int j)->Bool (i == j))
+	,(['_sub'], binop \(Int i) (Int j)->Int  (i - j))
+	,(['_add'], binop \(Int i) (Int j)->Int  (i + j))
+	,(['_mul'], binop \(Int i) (Int j)->Int  (i * j))
+	,(['_div'], binop \(Int i) (Int j)->Int  (i / j))
 	]
 where
-	binop op = Func \l->pure (Func \r->op <$> eval l <*> eval r)
-
-sub :: [Char] Expression Expression -> Expression
-sub ident subst (Let ns rest)
-	| not (isMember ident (map fst ns))
-		= Let (fmap (sub ident subst) <$> ns) (sub ident subst rest)
-sub ident subst (Var v)
-	| ident == v = subst
-sub ident subst (App e1 e2) = App (sub ident subst e1) (sub ident subst e2)
-sub ident subst (Lambda v b)
-	| ident <> v = Lambda v (sub ident b subst)
-sub _ _ x = x
+	binop :: (Value Value -> Value) -> Value
+	binop op = Builtin \l->pure (Lit (Builtin \r->(o) Lit o op <$> eval l <*> eval r))
 
 eval :: Expression -> Eval Value
 eval (Let ns rest) = sequence [eval v >>= \v->modify (\vs->[(n, v):vs])\\(n, v)<-ns] >>| eval rest
 eval (Lit v) = pure v
 eval (Var v) = gets (lookup v) >>= maybe (liftT (Left [toString v +++ " not found"])) pure
-eval (App e1 e2) = eval e1 >>= \(Func v)->v e2
-eval (Lambda a b) = pure (Func \arg->eval (sub a arg b))
+eval (Lambda a b) = pure (Lambda` a b)
+eval (App e1 e2) = eval e1 >>= \v->case v of
+	(Lambda` v b) = eval (sub v e2 b)
+	(Builtin f) = f e2 >>= eval
+where
+	sub :: [Char] Expression Expression -> Expression
+	sub i subs (Let ns rest)
+		| not (isMember i (map fst ns)) = Let (fmap (sub i subs) <$> ns) (sub i subs rest)
+	sub i subs (Var v)
+		| i == v = subs
+	sub i subs (App e1 e2) = App (sub i subs e1) (sub i subs e2)
+	sub i subs (Lambda v b)
+		| i <> v = Lambda v (sub i subs b)
+	sub _ _ x = x
diff --git a/tests/preamble.mfp b/tests/preamble.mfp
index 120f93f..e219460 100644
--- a/tests/preamble.mfp
+++ b/tests/preamble.mfp
@@ -1,9 +1,17 @@
+//Function application
 $ ifxr 0 x y = x y;
+//Reverse function application
 & ifxr 0 x y = y x;
+
+//Arithmetic operators
 == ifxl 7 = code eq;
 * ifxl 7 = code mul;
 - ifxl 6 = code sub;
 + ifxl 6 = code add;
+
+//Conditional operators
 if = code if;
-fac i = if (i == 0) 1 (i * fac (i - 1));
+
+fac i = if (i == 0) 1 $ i * fac (i - 1);
+id x = x;
 start = fac 10;
-- 
2.20.1