strictness, ci

[minfp.git] / check.icl

diff --git a/check.icl b/check.icl
index a18a378..e56d555 100644 (file)
--- a/check.icl
+++ b/check.icl
@@ -14,47 +14,56 @@ import Data.Map => qualified put, union, difference, find, updateAt
 import Data.Maybe
 import Text
 
-import ast, scc, builtin
+import ast, scc
 
-check :: [Function] -> Either [String] (Expression, [([Char], Scheme)])
-check fs
-       # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
+import StdDebug
+
+check :: ![Either TypeDef Function] -> Either [String] (Expression, [([Char], Scheme)])
+check tdfs
+       # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) functions)
        | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
-       = case partition (\a->a=:(Function ['start'] _ _)) fs of
+       = case partition (\a->a=:(Function ['start'] _ _)) functions of
                ([], _) = Left ["No start function defined"]
                ([Function _ [] e:_], fs)
                        # e = makeExpression fs e
-                       = (\x->(e, x)) <$> runInfer (infer (fromList builtin) e)
+                       = tuple e <$> runInfer (infer (fromList (conses ++ builtin)) e)
                ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
+where
+       functions = rights tdfs
+       conses = flatten $ map (\(TypeDef n t cs)->
+               let cons = Forall t o foldr (-->) (foldl TApp (TVar n) (map TVar t))
+               in map (appSnd cons) cs) $ lefts tdfs
+       builtin =
+               [(['_if'],  Forall [['a']] $ TBool --> TVar ['a'] --> TVar ['a'] --> TVar ['a'])
+               ,(['_eq'],  Forall [] $ TInt --> TInt --> TBool)
+               ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
+               ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
+               ,(['_sub'], Forall [] $ TInt --> TInt --> TInt)
+               ,(['_div'], Forall [] $ TInt --> TInt --> TInt)
+               ]
 
 makeExpression :: [Function] Expression -> Expression
-makeExpression fs start = foldr mkExpr start $ scc [(l, vars e [])\\(l, e)<-nicefuns]
+makeExpression fs start = foldr mkExpr start $ scc $ map (appSnd vars) nicefuns
 where
        mkExpr :: [[Char]] -> (Expression -> Expression)
        mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
 
        nicefuns :: [([Char], Expression)]
-       nicefuns = [(l, foldr (\x c->Lambda x o c) id i e)\\(Function l i e)<-fs]
+       nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
+
+       vars :: Expression -> [[Char]]
+       vars (Var v) = [v]
+       vars (App l r) = vars l ++ vars r
+       vars (Lambda l e) = flt l e
+       vars (Let ns e) = flatten [[v\\v<-vars e | not (isMember v (map fst ns))]:map (uncurry flt) ns]
+       vars _ = []
 
-       vars :: Expression [[Char]] -> [[Char]]
-       vars (Var v=:[m:_]) c = [v:c]
-       vars (App l r) c = vars l $ vars r c
-       vars (Lambda l e) c = [v\\v<-vars e c | v <> l]
-       vars (Let ns e) c = flatten
-               [ [v\\v<-vars e c | not (isMember v (map fst ns))]
-               : map (\(i, e)->[v\\v<-vars e [] | v <> i]) ns]
-       vars _ c = c
+       flt i e = [v\\v<-vars e | v <> i]
 
 instance toString Scheme where
        toString (Forall [] t) = toString t
        toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
 
-instance toString Type where
-       toString (TVar a) = toString a
-       toString TInt = "Int"
-       toString TBool = "Bool"
-       toString (a --> b) = concat ["(", toString a, " -> ", toString b, ")"]
-
 :: TypeEnv :== Map [Char] Scheme
 :: Subst :== Map [Char] Type
 
@@ -78,10 +87,12 @@ class Substitutable a where
 instance Substitutable Type where
        apply s t=:(TVar v) = fromMaybe t (get v s)
        apply s (t1 --> t2) = apply s t1 --> apply s t2
+       apply s (TApp t1 t2) = TApp (apply s t1) (apply s t2)
        apply _ x = x
        
        ftv (TVar v) = [v]
        ftv (t1 --> t2) = on union ftv t1 t2
+       ftv (TApp t1 t2) = on union ftv t1 t2
        ftv _ = []
 
 instance Substitutable Scheme where
@@ -115,6 +126,10 @@ unify (TVar a) t
 unify t (TVar a) = unify (TVar a) t
 unify TInt TInt = pure newMap
 unify TBool TBool = pure newMap
+unify (TApp l r) (TApp l` r`)
+       = unify l l`
+       >>= \s1->on unify (apply s1) r r`
+       >>= \s2->pure (s1 oo s2)
 unify t1 t2 = err ["Cannot unify: ", toString t1, " with ", toString t2]
 
 unifyl :: [Type] -> Infer Subst