Elaborating files

14 files changed, 181 insertions, 64 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index ede5d8b5..612933b7 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -30,7 +30,9 @@
 signature COMPILER = sig
 
     val parse : string -> Source.file option
+    val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option
 
     val testParse : string -> unit
+    val testElaborate : string -> unit
 
 end
diff --git a/src/compiler.sml b/src/compiler.sml
index 967fcf3d..3e39dcc9 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -47,18 +47,41 @@ fun parse filename =
 	val (absyn, _) = LacwebP.parse (30, lexer, parseerror, ())
     in
         TextIO.closeIn file;
-        SOME absyn
+        if ErrorMsg.anyErrors () then
+            NONE
+        else
+            SOME absyn
     end
     handle LrParser.ParseError => NONE
 
+fun elaborate env filename =
+    case parse filename of
+        NONE => NONE
+      | SOME file =>
+        let
+            val out = Elaborate.elabFile env file
+        in
+            if ErrorMsg.anyErrors () then
+                NONE
+            else
+                SOME out
+        end
+            
+
 fun testParse filename =
     case parse filename of
-        NONE => print "Parse error\n"
+        NONE => print "Failed\n"
       | SOME file =>
-        if ErrorMsg.anyErrors () then
-            print "Recoverable parse error\n"
-        else
-            (Print.print (SourcePrint.p_file file);
-             print "\n")
+        (Print.print (SourcePrint.p_file file);
+         print "\n")
+
+fun testElaborate filename =
+    (case elaborate ElabEnv.empty filename of
+         NONE => print "Failed\n"
+       | SOME (_, file) =>
+         (Print.print (ElabPrint.p_file ElabEnv.empty file);
+          print "\n"))
+    handle ElabEnv.UnboundNamed n =>
+           print ("Unbound named " ^ Int.toString n ^ "\n")
 
 end
diff --git a/src/elab.sml b/src/elab.sml
index 3c339190..89d25c26 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -65,7 +65,7 @@ datatype con' =
 withtype con = con' located
 
 datatype decl' =
-         DCon of string * kind * con
+         DCon of string * int * kind * con
 
 withtype decl = decl' located
 
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 8300c2a9..c4e5ae5a 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -38,6 +38,7 @@ signature ELAB_ENV = sig
     val lookupCRel : env -> int -> string * Elab.kind
 
     val pushCNamed : env -> string -> Elab.kind -> env * int
+    val pushCNamedAs : env -> string -> int -> Elab.kind -> env
     val lookupCNamed : env -> int -> string * Elab.kind
                                                  
     datatype var =
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 7b932aad..9a2655e4 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -75,15 +75,17 @@ fun lookupCRel (env : env) n =
     (List.nth (#relC env, n))
     handle Subscript => raise UnboundRel n
 
-fun pushCNamed (env : env) x k =
+fun pushCNamedAs (env : env) x n k =
+    {renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
+     relC = #relC env,
+     namedC = IM.insert (#namedC env, n, (x, k))}
+
+fun pushCNamed env x k =
     let
         val n = !namedCounter
     in
         namedCounter := n + 1;
-        ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
-          relC = #relC env,
-          namedC = IM.insert (#namedC env, n, (x, k))},
-         n)
+        (pushCNamedAs env x n k, n)
     end
 
 fun lookupCNamed (env : env) n =
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 18d01695..58a342e2 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -128,24 +128,26 @@ 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]
+        DCon (x, n, k, c) => box [string "con",
+                                  space,
+                                  string x,
+                                  string "__",
+                                  string (Int.toString n),
+                                  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
+        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
+                                             (ElabUtil.declBinds env d,
+                                              p_decl env d))
+                             env file
     in
         p_list_sep newline (fn x => x) pds
     end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index f5640d15..f889db30 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -79,6 +79,6 @@ structure E = ElabEnv
 
 fun declBinds env (d, _) =
     case d of
-        DCon (x, k, _) => #1 (E.pushCNamed env x k)
+        DCon (x, n, k, _) => E.pushCNamedAs env x n k
 
 end
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 519e5689..655df86c 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -27,6 +27,6 @@
 
 signature ELABORATE = sig
 
-    val elabFile : Source.file -> Elab.file
+    val elabFile : ElabEnv.env -> Source.file -> ElabEnv.env * Elab.file
 
 end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ed290d55..14fe47e1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -116,20 +116,21 @@ datatype con_error =
          UnboundCon of ErrorMsg.span * string
        | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
 
-fun conError err =
+fun conError env 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)];
+         eprefaces' [("Constructor", p_con env c),
+                     ("Have kind", p_kind k1),
+                     ("Need kind", p_kind k2)];
          kunifyError kerr)
 
-fun checkKind c k1 k2 =
+fun checkKind env c k1 k2 =
     unifyKinds k1 k2
     handle KUnify (k1, k2, err) =>
-           conError (WrongKind (c, k1, k2, err))
+           conError env (WrongKind (c, k1, k2, err))
 
 val dummy = ErrorMsg.dummySpan
 
@@ -166,7 +167,7 @@ fun elabCon env (c, loc) =
             val k' = elabKind k
             val (c', ck) = elabCon env c
         in
-            checkKind c' ck k';
+            checkKind env c' ck k';
             (c', k')
         end
 
@@ -175,8 +176,8 @@ fun elabCon env (c, loc) =
             val (t1', k1) = elabCon env t1
             val (t2', k2) = elabCon env t2
         in
-            checkKind t1' k1 ktype;
-            checkKind t2' k2 ktype;
+            checkKind env t1' k1 ktype;
+            checkKind env t2' k2 ktype;
             ((L'.TFun (t1', t2'), loc), ktype)
         end
       | L.TCFun (e, x, k, t) =>
@@ -186,7 +187,7 @@ fun elabCon env (c, loc) =
             val env' = E.pushCRel env x k'
             val (t', tk) = elabCon env' t
         in
-            checkKind t' tk ktype;
+            checkKind env t' tk ktype;
             ((L'.TCFun (e', x, k', t'), loc), ktype)
         end
       | L.TRecord c =>
@@ -194,14 +195,14 @@ fun elabCon env (c, loc) =
             val (c', ck) = elabCon env c
             val k = (L'.KRecord ktype, loc)
         in
-            checkKind c' ck k;
+            checkKind env c' ck k;
             ((L'.TRecord c', loc), ktype)
         end
 
       | L.CVar s =>
         (case E.lookupC env s of
              E.CNotBound =>
-             (conError (UnboundCon (loc, s));
+             (conError env (UnboundCon (loc, s));
               (cerror, kerror))
            | E.CRel (n, k) =>
              ((L'.CRel n, loc), k)
@@ -214,8 +215,8 @@ fun elabCon env (c, loc) =
             val dom = kunif ()
             val ran = kunif ()
         in
-            checkKind c1' k1 (L'.KArrow (dom, ran), loc);
-            checkKind c2' k2 dom;
+            checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
+            checkKind env c2' k2 dom;
             ((L'.CApp (c1', c2'), loc), ran)
         end
       | L.CAbs (e, x, k, t) =>
@@ -241,12 +242,12 @@ fun elabCon env (c, loc) =
                                    val (x', xk) = elabCon env x
                                    val (c', ck) = elabCon env c
                                in
-                                   checkKind x' xk kname;
-                                   checkKind c' ck k;
+                                   checkKind env x' xk kname;
+                                   checkKind env c' ck k;
                                    (x', c')
                                end) xcs
         in
-            ((L'.CRecord (k, xcs'), loc), k)
+            ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc))
         end
       | L.CConcat (c1, c2) =>
         let
@@ -255,26 +256,29 @@ fun elabCon env (c, loc) =
             val ku = kunif ()
             val k = (L'.KRecord ku, loc)
         in
-            checkKind c1' k1 k;
-            checkKind c2' k2 k;
+            checkKind env c1' k1 k;
+            checkKind env 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 ""
+    (resetKunif ();
+     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
+             val (env', n) = E.pushCNamed env x k'
+         in
+             checkKind env c' ck k';
+             (env',
+              (L'.DCon (x, n, k', c'), loc))
+         end)
+
+fun elabFile env ds =
+    ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
 
 end
diff --git a/src/list_util.sig b/src/list_util.sig
new file mode 100644
index 00000000..4c4aa955
--- /dev/null
+++ b/src/list_util.sig
@@ -0,0 +1,33 @@
+(* 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.
+ *)
+
+signature LIST_UTIL = sig
+
+    val mapfoldl : ('data1 * 'state -> 'state * 'data2) -> 'state -> 'data1 list
+                   -> 'state * 'data2 list
+
+end
diff --git a/src/list_util.sml b/src/list_util.sml
new file mode 100644
index 00000000..fdc1ac55
--- /dev/null
+++ b/src/list_util.sml
@@ -0,0 +1,45 @@
+(* 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.
+ *)
+
+structure ListUtil :> LIST_UTIL = struct
+
+fun mapfoldl f i =
+    let
+        fun mf s ls' ls =
+            case ls of
+                nil => (s, rev ls')
+              | h :: t =>
+                let
+                    val (s, h') = f (h, s)
+                in
+                    mf s (h' :: ls') t
+                end
+    in
+        mf i []
+    end
+
+end
diff --git a/src/print.sml b/src/print.sml
index 22387090..a1efdb96 100644
--- a/src/print.sml
+++ b/src/print.sml
@@ -66,7 +66,7 @@ val eprint = fprint err
 
 fun fpreface f (s, d) =
     fprint f (PD.hovBox (PD.PPS.Rel 0,
-		         [PD.string s, PD.space 1, d]))
+		         [PD.string s, PD.space 1, d, PD.newline]))
 
 val preface = fpreface out
 val epreface = fpreface err
diff --git a/src/sources b/src/sources
index 9c879139..8cc24a1e 100644
--- a/src/sources
+++ b/src/sources
@@ -1,3 +1,6 @@
+list_util.sig
+list_util.sml
+
 errormsg.sig
 errormsg.sml
 
diff --git a/tests/stuff.lac b/tests/stuff.lac
index 076698ce..c5d5852e 100644
--- a/tests/stuff.lac
+++ b/tests/stuff.lac
@@ -8,3 +8,5 @@ con name = #MyName
 
 con c6 = {A : c1, name : c2}
 con c7 = [A = c1, name = c2]
+
+con c8 = fn t :: Type => t