# HG changeset patch # User Adam Chlipala # Date 1201381367 18000 # Node ID 258261a538428380b9c2e92c6bb749885772c49f # Parent 5c3cc348e9e66f2b30a8421992a4acfed353ee72 Elaborating files diff -r 5c3cc348e9e6 -r 258261a53842 src/compiler.sig --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/compiler.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/elab.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/elab_env.sig --- 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 = diff -r 5c3cc348e9e6 -r 258261a53842 src/elab_env.sml --- 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 = diff -r 5c3cc348e9e6 -r 258261a53842 src/elab_print.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/elab_util.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/elaborate.sig --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/elaborate.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/list_util.sig --- /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 diff -r 5c3cc348e9e6 -r 258261a53842 src/list_util.sml --- /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 diff -r 5c3cc348e9e6 -r 258261a53842 src/print.sml --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 src/sources --- 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 diff -r 5c3cc348e9e6 -r 258261a53842 tests/stuff.lac --- 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