summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml37
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml12
-rw-r--r--src/elab_print.sml32
-rw-r--r--src/elab_util.sml2
-rw-r--r--src/elaborate.sig2
-rw-r--r--src/elaborate.sml70
-rw-r--r--src/list_util.sig33
-rw-r--r--src/list_util.sml45
-rw-r--r--src/print.sml2
-rw-r--r--src/sources3
-rw-r--r--tests/stuff.lac2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 00:30:21 +0000