typing
authorMart Lubbers <mart@martlubbers.net>
Thu, 14 Mar 2019 13:03:21 +0000 (14:03 +0100)
committerMart Lubbers <mart@martlubbers.net>
Thu, 14 Mar 2019 13:03:21 +0000 (14:03 +0100)
ast.dcl
ast.icl
check.icl
int.icl
tests/preamble.mfp

diff --git a/ast.dcl b/ast.dcl
index 7dd17d7..4dfad17 100644 (file)
--- 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 (file)
--- 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"
index abff97a..2cc76ac 100644 (file)
--- 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 (file)
--- 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
index 120f93f..e219460 100644 (file)
@@ -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;