diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/compiler.sig | 2 | ||||
| -rw-r--r-- | src/compiler.sml | 37 | ||||
| -rw-r--r-- | src/elab.sml | 2 | ||||
| -rw-r--r-- | src/elab_env.sig | 1 | ||||
| -rw-r--r-- | src/elab_env.sml | 12 | ||||
| -rw-r--r-- | src/elab_print.sml | 32 | ||||
| -rw-r--r-- | src/elab_util.sml | 2 | ||||
| -rw-r--r-- | src/elaborate.sig | 2 | ||||
| -rw-r--r-- | src/elaborate.sml | 70 | ||||
| -rw-r--r-- | src/list_util.sig | 33 | ||||
| -rw-r--r-- | src/list_util.sml | 45 | ||||
| -rw-r--r-- | src/print.sml | 2 | ||||
| -rw-r--r-- | src/sources | 3 |
13 files changed, 179 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 |