Mercurial > urweb

changeset 5:258261a53842

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating files
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 16:02:47 -0500
parents 5c3cc348e9e6
children 38bf996e1c2e
files src/compiler.sig src/compiler.sml src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sig src/elaborate.sml src/list_util.sig src/list_util.sml src/print.sml src/sources tests/stuff.lac
diffstat 14 files changed, 179 insertions(+), 62 deletions(-) [+]
line wrap: on
line diff
--- a/src/compiler.sig	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/compiler.sig	Sat Jan 26 16:02:47 2008 -0500
@@ -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
--- a/src/compiler.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/compiler.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -47,18 +47,41 @@
 	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
--- a/src/elab.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -65,7 +65,7 @@
 withtype con = con' located
 
 datatype decl' =
-         DCon of string * kind * con
+         DCon of string * int * kind * con
 
 withtype decl = decl' located
 
--- a/src/elab_env.sig	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab_env.sig	Sat Jan 26 16:02:47 2008 -0500
@@ -38,6 +38,7 @@
     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 =
--- a/src/elab_env.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab_env.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -75,15 +75,17 @@
     (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 =
--- a/src/elab_print.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab_print.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -128,24 +128,26 @@
 
 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
--- a/src/elab_util.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab_util.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -79,6 +79,6 @@
 
 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
--- a/src/elaborate.sig	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elaborate.sig	Sat Jan 26 16:02:47 2008 -0500
@@ -27,6 +27,6 @@
 
 signature ELABORATE = sig
 
-    val elabFile : Source.file -> Elab.file
+    val elabFile : ElabEnv.env -> Source.file -> ElabEnv.env * Elab.file
 
 end
--- a/src/elaborate.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elaborate.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -116,20 +116,21 @@
          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 @@
             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 @@
             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 @@
             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 @@
             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 @@
             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 @@
                                    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 @@
             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
+    (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
-        in
-            checkKind c' ck k';
-            (E.pushCNamed env x k',
-             L'.DCon (x, k', c'))
-        end
+             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 _ = raise Fail ""
+fun elabFile env ds =
+    ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
 
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/list_util.sig	Sat Jan 26 16:02:47 2008 -0500
@@ -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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/list_util.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -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
--- a/src/print.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/print.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -66,7 +66,7 @@
 
 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
--- a/src/sources	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/sources	Sat Jan 26 16:02:47 2008 -0500
@@ -1,3 +1,6 @@
+list_util.sig
+list_util.sml
+
 errormsg.sig
 errormsg.sml
 
--- a/tests/stuff.lac	Sat Jan 26 15:29:09 2008 -0500
+++ b/tests/stuff.lac	Sat Jan 26 16:02:47 2008 -0500
@@ -8,3 +8,5 @@
 
 con c6 = {A : c1, name : c2}
 con c7 = [A = c1, name = c2]
+
+con c8 = fn t :: Type => t