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"
// = 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 []
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