Add structured types for parsing and type checking
[minfp.git] / check.icl
index 62a43a9..cbd58f6 100644 (file)
--- a/check.icl
+++ b/check.icl
@@ -16,22 +16,25 @@ import Text
 
 import ast, scc
 
+import StdDebug
+
 check :: [Either TypeDef Function] -> Either [String] (Expression, [([Char], Scheme)])
-check fs
-       # fs = [v\\(Right v)<-fs]
-       # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
+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'])
-               ,(['_fst'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['a'])
-               ,(['_snd'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['b'])
                ,(['_eq'],  Forall [] $ TInt --> TInt --> TBool)
                ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
                ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
@@ -84,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
@@ -121,7 +126,7 @@ unify (TVar a) t
 unify t (TVar a) = unify (TVar a) t
 unify TInt TInt = pure newMap
 unify TBool TBool = pure newMap
-unify (TTuple l r) (TTuple l` r`)
+unify (TApp l r) (TApp l` r`)
        = unify l l`
        >>= \s1->on unify (apply s1) r r`
        >>= \s2->pure (s1 oo s2)
@@ -150,10 +155,6 @@ infer env (App e1 e2)
        >>= \(s1, t1)->infer (apply s1 env) e2
        >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
        >>= \s3->      pure (s3 oo s2 oo s1, apply s3 tv)
-infer env (Tuple a b)
-       =              infer env a
-       >>= \(s1, t1)->infer env b
-       >>= \(s2, t2)->pure (s1 oo s2, TTuple t1 t2)
 infer env (Lambda x b)
        =              fresh
        >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b