Elaborating cons and decls

1 files changed, 189 insertions, 11 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index ca950de2..e6044e49 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -32,6 +32,9 @@ structure L' = Elab
 structure E = ElabEnv
 structure U = ElabUtil
 
+open Print
+open ElabPrint
+
 fun elabKind (k, loc) =
     case k of
         L.KType => (L'.KType, loc)
@@ -48,34 +51,40 @@ fun occursKind r =
     U.Kind.exists (fn L'.KUnif (_, r') => r = r'
                     | _ => false)
 
-datatype unify_error =
+datatype kunify_error =
          KOccursCheckFailed of L'.kind * L'.kind
        | KIncompatible of L'.kind * L'.kind
 
-fun unifyError err =
+exception KUnify' of kunify_error
+
+fun kunifyError err =
     case err of
         KOccursCheckFailed (k1, k2) =>
-        ErrorMsg.errorAt (#2 k1) "Kind occurs check failed"
+        eprefaces "Kind occurs check failed"
+        [("Kind 1", p_kind k1),
+         ("Kind 2", p_kind k2)]
       | KIncompatible (k1, k2) =>
-        ErrorMsg.errorAt (#2 k1) "Incompatible kinds"
+        eprefaces "Incompatible kinds"
+        [("Kind 1", p_kind k1),
+         ("Kind 2", p_kind k2)]
 
-fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) =
+fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
     let
-        fun err f = unifyError (f (k1All, k2All))
+        fun err f = raise KUnify' (f (k1All, k2All))
     in
         case (k1, k2) of
             (L'.KType, L'.KType) => ()
           | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
-            (unifyKinds d1 d2;
-             unifyKinds r1 r2)
+            (unifyKinds' d1 d2;
+             unifyKinds' r1 r2)
           | (L'.KName, L'.KName) => ()
-          | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2
+          | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
 
           | (L'.KError, _) => ()
           | (_, L'.KError) => ()
 
-          | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All
-          | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All
+          | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All
+          | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All
 
           | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
             if r1 = r2 then
@@ -97,6 +106,175 @@ fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) =
           | _ => err KIncompatible
     end
 
+exception KUnify of L'.kind * L'.kind * kunify_error
+
+fun unifyKinds k1 k2 =
+    unifyKinds' k1 k2
+    handle KUnify' err => raise KUnify (k1, k2, err)
+
+datatype con_error =
+         UnboundCon of ErrorMsg.span * string
+       | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
+
+fun conError err =
+    case err of
+        UnboundCon (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
+      | WrongKind (c, k1, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 c) "Wrong kind";
+         eprefaces' [("Have", p_kind k1),
+                     ("Need", p_kind k2)];
+         kunifyError kerr)
+
+fun checkKind c k1 k2 =
+    unifyKinds k1 k2
+    handle KUnify (k1, k2, err) =>
+           conError (WrongKind (c, k1, k2, err))
+
+val dummy = ErrorMsg.dummySpan
+
+val ktype = (L'.KType, dummy)
+val kname = (L'.KName, dummy)
+
+val cerror = (L'.CError, dummy)
+val kerror = (L'.KError, dummy)
+
+local
+    val count = ref 0
+in
+
+fun resetKunif () = count := 0
+
+fun kunif () =
+    let
+        val n = !count
+        val s = if n <= 26 then
+                    str (chr (ord #"A" + n))
+                else
+                    "U" ^ Int.toString (n - 26)
+    in
+        count := n + 1;
+        (L'.KUnif (s, ref NONE), dummy)
+    end
+
+end
+
+fun elabCon env (c, loc) =
+    case c of
+        L.CAnnot (c, k) =>
+        let
+            val k' = elabKind k
+            val (c', ck) = elabCon env c
+        in
+            checkKind c' ck k';
+            (c', k')
+        end
+
+      | L.TFun (t1, t2) =>
+        let
+            val (t1', k1) = elabCon env t1
+            val (t2', k2) = elabCon env t2
+        in
+            checkKind t1' k1 ktype;
+            checkKind t2' k2 ktype;
+            ((L'.TFun (t1', t2'), loc), ktype)
+        end
+      | L.TCFun (e, x, k, t) =>
+        let
+            val e' = elabExplicitness e
+            val k' = elabKind k
+            val env' = E.pushCRel env x k'
+            val (t', tk) = elabCon env' t
+        in
+            checkKind t' tk ktype;
+            ((L'.TCFun (e', x, k', t'), loc), ktype)
+        end
+      | L.TRecord c =>
+        let
+            val (c', ck) = elabCon env c
+            val k = (L'.KRecord ktype, loc)
+        in
+            checkKind c' ck k;
+            ((L'.TRecord c', loc), ktype)
+        end
+
+      | L.CVar s =>
+        (case E.lookupC env s of
+             E.CNotBound =>
+             (conError (UnboundCon (loc, s));
+              (cerror, kerror))
+           | E.CRel (n, k) =>
+             ((L'.CRel n, loc), k)
+           | E.CNamed (n, k) =>
+             ((L'.CNamed n, loc), k))
+      | L.CApp (c1, c2) =>
+        let
+            val (c1', k1) = elabCon env c1
+            val (c2', k2) = elabCon env c2
+            val dom = kunif ()
+            val ran = kunif ()
+        in
+            checkKind c1' k1 (L'.KArrow (dom, ran), loc);
+            checkKind c2' k2 dom;
+            ((L'.CApp (c1', c2'), loc), ran)
+        end
+      | L.CAbs (e, x, k, t) =>
+        let
+            val e' = elabExplicitness e
+            val k' = elabKind k
+            val env' = E.pushCRel env x k'
+            val (t', tk) = elabCon env' t
+        in
+            ((L'.CAbs (e', x, k', t'), loc),
+             (L'.KArrow (k', tk), loc))
+        end
+
+      | L.CName s =>
+        ((L'.CName s, loc), kname)
+
+      | L.CRecord xcs =>
+        let
+            val k = kunif ()
+
+            val xcs' = map (fn (x, c) =>
+                               let
+                                   val (x', xk) = elabCon env x
+                                   val (c', ck) = elabCon env c
+                               in
+                                   checkKind x' xk kname;
+                                   checkKind c' ck k;
+                                   (x', c')
+                               end) xcs
+        in
+            ((L'.CRecord (k, xcs'), loc), k)
+        end
+      | L.CConcat (c1, c2) =>
+        let
+            val (c1', k1) = elabCon env c1
+            val (c2', k2) = elabCon env c2
+            val ku = kunif ()
+            val k = (L'.KRecord ku, loc)
+        in
+            checkKind c1' k1 k;
+            checkKind c2' k2 k;
+            ((L'.CConcat (c1', c2'), loc), k)
+        end
+
+fun elabDecl env (d, loc) =
+    case d of
+        L.DCon (x, ko, c) =>
+        let
+            val k' = case ko of
+                         NONE => kunif ()
+                       | SOME k => elabKind k
+
+            val (c', ck) = elabCon env c
+        in
+            checkKind c' ck k';
+            (E.pushCNamed env x k',
+             L'.DCon (x, k', c'))
+        end
+
 fun elabFile _ = raise Fail ""
 
 end