Elaborating cons and decls

10 files changed, 427 insertions, 15 deletions

diff --git a/src/elab_print.sig b/src/elab_print.sig
new file mode 100644
index 00000000..489b0756
--- /dev/null
+++ b/src/elab_print.sig
@@ -0,0 +1,37 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Pretty-printing Laconic/Web *)
+
+signature ELAB_PRINT = sig
+    val p_kind : Elab.kind Print.printer
+    val p_explicitness : Elab.explicitness Print.printer
+    val p_con : ElabEnv.env -> Elab.con Print.printer
+    val p_decl : ElabEnv.env -> Elab.decl Print.printer
+    val p_file : ElabEnv.env -> Elab.file Print.printer
+end
+
diff --git a/src/elab_print.sml b/src/elab_print.sml
new file mode 100644
index 00000000..18d01695
--- /dev/null
+++ b/src/elab_print.sml
@@ -0,0 +1,153 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Pretty-printing elaborated Laconic/Web *)
+
+structure ElabPrint :> ELAB_PRINT = struct
+
+open Print.PD
+open Print
+
+open Elab
+
+structure E = ElabEnv
+
+fun p_kind' par (k, _) =
+    case k of
+        KType => string "Type"
+      | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
+                                             space,
+                                             string "->",
+                                             space,
+                                             p_kind k2])
+      | KName => string "Name"
+      | KRecord k => box [string "{", p_kind k, string "}"]
+
+      | KError => string "<ERROR>"
+      | KUnif (_, ref (SOME k)) => p_kind' par k
+      | KUnif (s, _) => string ("<UNIF:" ^ s ^ ">")
+
+and p_kind k = p_kind' false k
+
+fun p_explicitness e =
+    case e of
+        Explicit => string "::"
+      | Implicit => string ":::"
+
+fun p_con' par env (c, _) =
+    case c of
+        TFun (t1, t2) => parenIf par (box [p_con' true env t1,
+                                           space,
+                                           string "->",
+                                           space,
+                                           p_con env t2])
+      | TCFun (e, x, k, c) => parenIf par (box [string x,
+                                                space,
+                                                p_explicitness e,
+                                                space,
+                                                p_kind k,
+                                                space,
+                                                string "->",
+                                                space,
+                                                p_con (E.pushCRel env x k) c])
+      | TRecord (CRecord (_, xcs), _) => box [string "{",
+                                              p_list (fn (x, c) =>
+                                                         box [p_con env x,
+                                                              space,
+                                                              string ":",
+                                                              space,
+                                                              p_con env c]) xcs,
+                                              string "}"]
+      | TRecord c => box [string "$",
+                          p_con' true env c]
+
+      | CRel n => string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
+      | CNamed n => string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
+
+      | CApp (c1, c2) => parenIf par (box [p_con env c1,
+                                           space,
+                                           p_con' true env c2])
+      | CAbs (e, x, k, c) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               p_explicitness e,
+                                               space,
+                                               p_kind k,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_con (E.pushCRel env x k) c])
+
+      | CName s => box [string "#", string s]
+
+      | CRecord (k, xcs) => parenIf par (box [string "[",
+                                              p_list (fn (x, c) =>
+                                                         box [p_con env x,
+                                                              space,
+                                                              string "=",
+                                                              space,
+                                                              p_con env c]) xcs,
+                                              string "]::",
+                                              p_kind k])
+      | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
+                                              space,
+                                              string "++",
+                                              space,
+                                              p_con env c2])
+
+      | CError => string "<ERROR>"
+      | CUnif (_, ref (SOME c)) => p_con' par env c
+      | CUnif (s, _) => string ("<UNIF:" ^ s ^ ">")
+        
+and p_con env = p_con' false env
+
+fun p_decl env ((d, _) : decl) =
+    case d of
+        DCon (x, k, c) => box [string "con",
+                                    space,
+                                    string x,
+                                    space,
+                                    string "::",
+                                    space,
+                                    p_kind k,
+                                    space,
+                                    string "=",
+                                    space,
+                                    p_con env c]
+
+fun p_file env file =
+    let
+        val (_, pds) = foldr (fn (d, (env, pds)) =>
+                                 (ElabUtil.declBinds env d,
+                                  p_decl env d :: pds))
+                             (env, []) file
+    in
+        p_list_sep newline (fn x => x) pds
+    end
+
+end
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 0190b576..da1a02f4 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -33,4 +33,6 @@ structure Kind : sig
     val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
 end
 
+val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env
+
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 8a0463cf..f5640d15 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -75,4 +75,10 @@ fun exists f k =
 
 end
 
+structure E = ElabEnv
+
+fun declBinds env (d, _) =
+    case d of
+        DCon (x, k, _) => #1 (E.pushCNamed env x k)
+
 end
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
diff --git a/src/errormsg.sig b/src/errormsg.sig
index 24bc8205..92425842 100644
--- a/src/errormsg.sig
+++ b/src/errormsg.sig
@@ -39,6 +39,9 @@ signature ERROR_MSG = sig
     val posToString : pos -> string
     val spanToString : span -> string
 
+    val dummyPos : pos
+    val dummySpan : span
+
     val resetPositioning : string -> unit
     val newline : int -> unit
     val lastLineStart : unit -> int
diff --git a/src/errormsg.sml b/src/errormsg.sml
index 0f5b9b61..e816b9a2 100644
--- a/src/errormsg.sml
+++ b/src/errormsg.sml
@@ -43,6 +43,12 @@ fun posToString {line, char} =
 fun spanToString {file, first, last} =
     String.concat [file, ":", posToString first, "-", posToString last]
 
+val dummyPos = {line = 0,
+                char = 0}
+val dummySpan = {file = "",
+                 first = dummyPos,
+                 last = dummyPos}
+
 
 val file = ref ""
 val numLines = ref 1
diff --git a/src/print.sig b/src/print.sig
index 5bf3fcd8..39daf5d0 100644
--- a/src/print.sig
+++ b/src/print.sig
@@ -48,7 +48,11 @@ signature PRINT = sig
     val preface : string * PD.pp_desc -> unit
     val epreface : string * PD.pp_desc -> unit
 
-    val fprefaces : PD.PPS.stream -> (string * PD.pp_desc) list -> unit
-    val prefaces : (string * PD.pp_desc) list -> unit
-    val eprefaces : (string * PD.pp_desc) list -> unit
+    val fprefaces : PD.PPS.stream -> string -> (string * PD.pp_desc) list -> unit
+    val prefaces : string -> (string * PD.pp_desc) list -> unit
+    val eprefaces : string -> (string * PD.pp_desc) list -> unit
+
+    val fprefaces' : PD.PPS.stream -> (string * PD.pp_desc) list -> unit
+    val prefaces' : (string * PD.pp_desc) list -> unit
+    val eprefaces' : (string * PD.pp_desc) list -> unit
 end
diff --git a/src/print.sml b/src/print.sml
index 6d9019d2..22387090 100644
--- a/src/print.sml
+++ b/src/print.sml
@@ -71,11 +71,13 @@ fun fpreface f (s, d) =
 val preface = fpreface out
 val epreface = fpreface err
 
-fun fprefaces f ls =
+fun fprefaces f s ls =
     let
         val len = foldl (fn ((s, _), best) =>
                             Int.max (size s, best)) 0 ls
     in
+        fprint f (PD.string s);
+        fprint f PD.newline;
         app (fn (s, d) =>
                 let
                     val s = CharVector.tabulate (len - size s,
@@ -89,4 +91,22 @@ fun fprefaces f ls =
 val prefaces = fprefaces out
 val eprefaces = fprefaces err
 
+fun fprefaces' f ls =
+    let
+        val len = foldl (fn ((s, _), best) =>
+                            Int.max (size s, best)) 0 ls
+    in
+        app (fn (s, d) =>
+                let
+                    val s = CharVector.tabulate (len - size s,
+                                                 fn _ => #" ")
+                            ^ s ^ ": "
+                in
+                    fpreface f (s, d)
+                end) ls
+    end
+
+val prefaces' = fprefaces' out
+val eprefaces' = fprefaces' err
+
 end
diff --git a/src/sources b/src/sources
index 6270b1ea..e82c0c7e 100644
--- a/src/sources
+++ b/src/sources
@@ -23,6 +23,9 @@ elab_util.sml
 elab_env.sig
 elab_env.sml
 
+elab_print.sig
+elab_print.sml
+
 elaborate.sig
 elaborate.sml