# HG changeset patch # User Adam Chlipala # Date 1335719851 14400 # Node ID 4a03aa3251cbfa691787c16edf84ac884fb0804d # Parent 27e731a659349d73df5dd5ca6f40ce326a09fa9c Initial support for reusing elaboration results diff -r 27e731a65934 -r 4a03aa3251cb src/compiler.sml --- a/src/compiler.sml Sat Apr 28 12:00:35 2012 -0400 +++ b/src/compiler.sml Sun Apr 29 13:17:31 2012 -0400 @@ -917,7 +917,7 @@ val sgn = (Source.SgnConst (#func parseUrs urs), loc) in checkErrors (); - (Source.DFfiStr (mname, sgn), loc) + (Source.DFfiStr (mname, sgn, OS.FileSys.modTime urs), loc) end val defed = ref SS.empty @@ -944,7 +944,7 @@ last = ErrorMsg.dummyPos} val ds = #func parseUr ur - val d = (Source.DStr (mname, sgnO, (Source.StrConst ds, loc)), loc) + val d = (Source.DStr (mname, sgnO, SOME (OS.FileSys.modTime ur), (Source.StrConst ds, loc)), loc) val fname = OS.Path.mkCanonical fname val d = case List.find (fn (root, name) => @@ -1002,14 +1002,14 @@ else (Source.StrVar part, loc) in - (Source.DStr (part, NONE, imp), + (Source.DStr (part, NONE, NONE, imp), loc) :: ds end else ds) [] (!fulls) in defed := SS.add (!defed, this); - (Source.DStr (piece, NONE, + (Source.DStr (piece, NONE, NONE, (Source.StrConst (if old then simOpen () @ [makeD this pieces] @@ -1092,11 +1092,20 @@ val elaborate = { func = fn file => let - val basis = #func parseUrs (libFile "basis.urs") - val topSgn = #func parseUrs (libFile "top.urs") - val topStr = #func parseUr (libFile "top.ur") + val basisF = libFile "basis.urs" + val topF = libFile "top.urs" + val topF' = libFile "top.ur" + + val basis = #func parseUrs basisF + val topSgn = #func parseUrs topF + val topStr = #func parseUr topF' + + val tm1 = OS.FileSys.modTime topF + val tm2 = OS.FileSys.modTime topF' in - Elaborate.elabFile basis topStr topSgn ElabEnv.empty file + Elaborate.elabFile basis (OS.FileSys.modTime basisF) + topStr topSgn (if Time.< (tm1, tm2) then tm2 else tm1) + ElabEnv.empty file end, print = ElabPrint.p_file ElabEnv.empty } diff -r 27e731a65934 -r 4a03aa3251cb src/elab_util.sig --- a/src/elab_util.sig Sat Apr 28 12:00:35 2012 -0400 +++ b/src/elab_util.sig Sun Apr 29 13:17:31 2012 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2010, 2012, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -229,6 +229,15 @@ decl : 'context -> Elab.decl' -> Elab.decl', bind : 'context * binder -> 'context} -> 'context -> Elab.decl -> Elab.decl + + val fold : {kind : Elab.kind' * 'state -> 'state, + con : Elab.con' * 'state -> 'state, + exp : Elab.exp' * 'state -> 'state, + sgn_item : Elab.sgn_item' * 'state -> 'state, + sgn : Elab.sgn' * 'state -> 'state, + str : Elab.str' * 'state -> 'state, + decl : Elab.decl' * 'state -> 'state} + -> 'state -> Elab.decl -> 'state end structure File : sig diff -r 27e731a65934 -r 4a03aa3251cb src/elab_util.sml --- a/src/elab_util.sml Sat Apr 28 12:00:35 2012 -0400 +++ b/src/elab_util.sml Sun Apr 29 13:17:31 2012 -0400 @@ -1180,6 +1180,17 @@ S.Continue (s, ()) => s | S.Return _ => raise Fail "ElabUtil.Decl.mapB: Impossible" +fun fold {kind, con, exp, sgn_item, sgn, str, decl} (st : 'a) d : 'a = + case mapfold {kind = fn k => fn st => S.Continue (k, kind (k, st)), + con = fn c => fn st => S.Continue (c, con (c, st)), + exp = fn e => fn st => S.Continue (e, exp (e, st)), + sgn_item = fn sgi => fn st => S.Continue (sgi, sgn_item (sgi, st)), + sgn = fn s => fn st => S.Continue (s, sgn (s, st)), + str = fn str' => fn st => S.Continue (str', str (str', st)), + decl = fn d => fn st => S.Continue (d, decl (d, st))} d st of + S.Continue (_, st) => st + | S.Return _ => raise Fail "ElabUtil.Decl.fold: Impossible" + end structure File = struct diff -r 27e731a65934 -r 4a03aa3251cb src/elaborate.sig --- a/src/elaborate.sig Sat Apr 28 12:00:35 2012 -0400 +++ b/src/elaborate.sig Sun Apr 29 13:17:31 2012 -0400 @@ -27,7 +27,8 @@ signature ELABORATE = sig - val elabFile : Source.sgn_item list -> Source.decl list -> Source.sgn_item list + val elabFile : Source.sgn_item list -> Time.time + -> Source.decl list -> Source.sgn_item list -> Time.time -> ElabEnv.env -> Source.file -> Elab.file val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option diff -r 27e731a65934 -r 4a03aa3251cb src/elaborate.sml --- a/src/elaborate.sml Sat Apr 28 12:00:35 2012 -0400 +++ b/src/elaborate.sml Sun Apr 29 13:17:31 2012 -0400 @@ -3641,7 +3641,7 @@ | L.DClass (x, _, _) => ndelCon (nd, x) | L.DVal (x, _, _) => ndelVal (nd, x) | L.DOpen _ => nempty - | L.DStr (x, _, (L.StrConst ds', _)) => + | L.DStr (x, _, _, (L.StrConst ds', _)) => (case SM.find (nmods nd, x) of NONE => nd | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds')))) @@ -3711,11 +3711,11 @@ val ds = ds @ ds' in - map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => + map (fn d as (L.DStr (x, s, tm, (L.StrConst ds', loc')), loc) => (case SM.find (nmods nd, x) of NONE => d | SOME (env, nd') => - (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc)) + (L.DStr (x, s, tm, (L.StrConst (extend (env, nd', ds')), loc')), loc)) | d => d) ds end in @@ -3923,56 +3923,80 @@ ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) end - | L.DStr (x, sgno, str) => - let - val () = if x = "Basis" then - raise Fail "Not allowed to redefine structure 'Basis'" - else - () - - val formal = Option.map (elabSgn (env, denv)) sgno - - val (str', sgn', gs') = - case formal of - NONE => - let - val (str', actual, gs') = elabStr (env, denv) str - in - (str', selfifyAt env {str = str', sgn = actual}, gs') - end - | SOME (formal, gs1) => - let - val str = wildifyStr env (str, formal) - val (str', actual, gs2) = elabStr (env, denv) str - in - subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; - (str', formal, enD gs1 @ gs2) - end - - val (env', n) = E.pushStrNamed env x sgn' - val denv' = - case #1 str' of - L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} - | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} - | _ => denv - in - case #1 (hnormSgn env sgn') of - L'.SgnFun _ => - (case #1 str' of - L'.StrFun _ => () - | _ => strError env (FunctorRebind loc)) - | _ => (); - ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs)) - end - - | L.DFfiStr (x, sgn) => - let - val (sgn', gs') = elabSgn (env, denv) sgn - - val (env', n) = E.pushStrNamed env x sgn' - in - ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) - end + | L.DStr (x, sgno, tmo, str) => + (case ModDb.lookup dAll of + SOME d => + let + val env' = E.declBinds env d + val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} + in + ([d], (env', denv', [])) + end + | NONE => + let + val () = if x = "Basis" then + raise Fail "Not allowed to redefine structure 'Basis'" + else + () + + val formal = Option.map (elabSgn (env, denv)) sgno + + val (str', sgn', gs') = + case formal of + NONE => + let + val (str', actual, gs') = elabStr (env, denv) str + in + (str', selfifyAt env {str = str', sgn = actual}, gs') + end + | SOME (formal, gs1) => + let + val str = wildifyStr env (str, formal) + val (str', actual, gs2) = elabStr (env, denv) str + in + subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; + (str', formal, enD gs1 @ gs2) + end + + val (env', n) = E.pushStrNamed env x sgn' + val denv' = + case #1 str' of + L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} + | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} + | _ => denv + + val dNew = (L'.DStr (x, n, sgn', str'), loc) + in + case #1 (hnormSgn env sgn') of + L'.SgnFun _ => + (case #1 str' of + L'.StrFun _ => () + | _ => strError env (FunctorRebind loc)) + | _ => (); + Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; + ([dNew], (env', denv', gs' @ gs)) + end) + + | L.DFfiStr (x, sgn, tm) => + (case ModDb.lookup dAll of + SOME d => + let + val env' = E.declBinds env d + val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} + in + ([d], (env', denv', [])) + end + | NONE => + let + val (sgn', gs') = elabSgn (env, denv) sgn + + val (env', n) = E.pushStrNamed env x sgn' + + val dNew = (L'.DFfiStr (x, n, sgn'), loc) + in + ModDb.insert (dNew, tm); + ([dNew], (env', denv, enD gs' @ gs)) + end) | L.DOpen (m, ms) => (case E.lookupStr env m of @@ -4431,24 +4455,36 @@ fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env -fun elabFile basis topStr topSgn env file = +fun elabFile basis basis_tm topStr topSgn top_tm env file = let val () = mayDelay := true val () = delayedUnifs := [] val () = delayedExhaustives := [] - val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) - val () = case gs of - [] => () - | _ => (app (fn (_, env, _, c1, c2) => - prefaces "Unresolved" - [("c1", p_con env c1), - ("c2", p_con env c2)]) gs; - raise Fail "Unresolved disjointness constraints in Basis") - - val (env', basis_n) = E.pushStrNamed env "Basis" sgn + val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), basis_tm), ErrorMsg.dummySpan) + val (basis_n, env', sgn) = + case ModDb.lookup d of + NONE => + let + val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) + val () = case gs of + [] => () + | _ => (app (fn (_, env, _, c1, c2) => + prefaces "Unresolved" + [("c1", p_con env c1), + ("c2", p_con env c2)]) gs; + raise Fail "Unresolved disjointness constraints in Basis") + + val (env', basis_n) = E.pushStrNamed env "Basis" sgn + in + ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm); + (basis_n, env', sgn) + end + | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) => + (basis_n, E.pushStrNamedAs env "Basis" basis_n sgn, sgn) + | _ => raise Fail "Elaborate: Basis impossible" + val () = basis_r := basis_n - val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} fun discoverC r x = @@ -4463,34 +4499,50 @@ val () = discoverC char "char" val () = discoverC table "sql_table" - val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) - val () = case gs of - [] => () - | _ => raise Fail "Unresolved disjointness constraints in top.urs" - val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) - val () = case gs of - [] => () - | _ => app (fn Disjoint (loc, env, denv, c1, c2) => - (case D.prove env denv (c1, c2, loc) of - [] => () - | _ => - (prefaces "Unresolved constraint in top.ur" - [("loc", PD.string (ErrorMsg.spanToString loc)), - ("c1", p_con env c1), - ("c2", p_con env c2)]; - raise Fail "Unresolved constraint in top.ur")) - | TypeClass (env, c, r, loc) => - let - val c = normClassKey env c - in - case resolveClass env c of - SOME e => r := SOME e - | NONE => expError env (Unresolvable (loc, c)) - end) gs - - val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn - - val (env', top_n) = E.pushStrNamed env' "Top" topSgn + val d = (L.DStr ("Top", SOME (L.SgnConst topSgn, ErrorMsg.dummySpan), + SOME (if Time.< (top_tm, basis_tm) then basis_tm else top_tm), + (L.StrConst topStr, ErrorMsg.dummySpan)), ErrorMsg.dummySpan) + val (top_n, env', topSgn, topStr) = + case ModDb.lookup d of + NONE => + let + val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) + val () = case gs of + [] => () + | _ => raise Fail "Unresolved disjointness constraints in top.urs" + val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) + + val () = case gs of + [] => () + | _ => app (fn Disjoint (loc, env, denv, c1, c2) => + (case D.prove env denv (c1, c2, loc) of + [] => () + | _ => + (prefaces "Unresolved constraint in top.ur" + [("loc", PD.string (ErrorMsg.spanToString loc)), + ("c1", p_con env c1), + ("c2", p_con env c2)]; + raise Fail "Unresolved constraint in top.ur")) + | TypeClass (env, c, r, loc) => + let + val c = normClassKey env c + in + case resolveClass env c of + SOME e => r := SOME e + | NONE => expError env (Unresolvable (loc, c)) + end) gs + + val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn + + val (env', top_n) = E.pushStrNamed env' "Top" topSgn + in + ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm); + (top_n, env', topSgn, topStr) + end + | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) => + (top_n, E.declBinds env' d', topSgn, topStr) + | _ => raise Fail "Elaborate: Top impossible" + val () = top_r := top_n val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} diff -r 27e731a65934 -r 4a03aa3251cb src/mod_db.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/mod_db.sig Sun Apr 29 13:17:31 2012 -0400 @@ -0,0 +1,38 @@ +(* Copyright (c) 2012, 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. + *) + +(* Cache of module code, with dependency information *) + +signature MOD_DB = sig + val reset : unit -> unit + + val insert : Elab.decl * Time.time -> unit + (* Here's a declaration, including the modification timestamp of the file it came from. + * We might invalidate other declarations that depend on this one, if the timestamp has changed. *) + + val lookup : Source.decl -> Elab.decl option +end diff -r 27e731a65934 -r 4a03aa3251cb src/mod_db.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/mod_db.sml Sun Apr 29 13:17:31 2012 -0400 @@ -0,0 +1,144 @@ +(* Copyright (c) 2012, 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. + *) + +(* Cache of module code, with dependency information *) + +structure ModDb :> MOD_DB = struct + +open Elab + +structure SK = struct +type ord_key = string +val compare = String.compare +end + +structure SS = BinarySetFn(SK) +structure SM = BinaryMapFn(SK) +structure IM = IntBinaryMap + +type oneMod = {Decl : decl, + When : Time.time, + Deps : SS.set} + +val byName = ref (SM.empty : oneMod SM.map) +val byId = ref (IM.empty : string IM.map) + +fun reset () = (byName := SM.empty; + byId := IM.empty) + +fun insert (d, tm) = + let + val xn = + case #1 d of + DStr (x, n, _, _) => SOME (x, n) + | DFfiStr (x, n, _) => SOME (x, n) + | _ => NONE + in + case xn of + NONE => () + | SOME (x, n) => + let + val skipIt = + case SM.find (!byName, x) of + NONE => false + | SOME r => #When r = tm + in + if skipIt then + () + else + let + fun doMod (n', deps) = + case IM.find (!byId, n') of + NONE => deps + | SOME x' => + SS.union (deps, + SS.add (case SM.find (!byName, x') of + NONE => SS.empty + | SOME {Deps = ds, ...} => ds, x')) + + val deps = ElabUtil.Decl.fold {kind = #2, + con = fn (c, deps) => + case c of + CModProj (n', _, _) => doMod (n', deps) + | _ => deps, + exp = fn (e, deps) => + case e of + EModProj (n', _, _) => doMod (n', deps) + | _ => deps, + sgn_item = #2, + sgn = fn (sg, deps) => + case sg of + SgnProj (n', _, _) => doMod (n', deps) + | _ => deps, + str = fn (st, deps) => + case st of + StrVar n' => doMod (n', deps) + | _ => deps, + decl = fn (d, deps) => + case d of + DDatatypeImp (_, _, n', _, _, _, _) => doMod (n', deps) + | _ => deps} + SS.empty d + in + byName := SM.insert (SM.filter (fn r => if SS.member (#Deps r, x) then + case #1 (#Decl r) of + DStr (_, n', _, _) => + (byId := #1 (IM.remove (!byId, n')); + false) + | _ => raise Fail "ModDb: Impossible decl" + else + true) (!byName), + x, + {Decl = d, + When = tm, + Deps = deps}); + byId := IM.insert (!byId, n, x) + end + end + end + +fun lookup (d : Source.decl) = + case #1 d of + Source.DStr (x, _, SOME tm, _) => + (case SM.find (!byName, x) of + NONE => NONE + | SOME r => + if tm = #When r then + SOME (#Decl r) + else + NONE) + | Source.DFfiStr (x, _, tm) => + (case SM.find (!byName, x) of + NONE => NONE + | SOME r => + if tm = #When r then + SOME (#Decl r) + else + NONE) + | _ => NONE + +end diff -r 27e731a65934 -r 4a03aa3251cb src/source.sml --- a/src/source.sml Sat Apr 28 12:00:35 2012 -0400 +++ b/src/source.sml Sun Apr 29 13:17:31 2012 -0400 @@ -154,8 +154,8 @@ | DVal of string * con option * exp | DValRec of (string * con option * exp) list | DSgn of string * sgn - | DStr of string * sgn option * str - | DFfiStr of string * sgn + | DStr of string * sgn option * Time.time option * str + | DFfiStr of string * sgn * Time.time | DOpen of string * string list | DConstraint of con * con | DOpenConstraints of string * string list diff -r 27e731a65934 -r 4a03aa3251cb src/source_print.sml --- a/src/source_print.sml Sat Apr 28 12:00:35 2012 -0400 +++ b/src/source_print.sml Sun Apr 29 13:17:31 2012 -0400 @@ -569,33 +569,33 @@ string "=", space, p_sgn sgn] - | DStr (x, NONE, str) => box [string "structure", + | DStr (x, NONE, _, str) => box [string "structure", + space, + string x, + space, + string "=", + space, + p_str str] + | DStr (x, SOME sgn, _, str) => box [string "structure", + space, + string x, + space, + string ":", + space, + p_sgn sgn, + space, + string "=", + space, + p_str str] + | DFfiStr (x, sgn, _) => box [string "extern", + space, + string "structure", space, string x, space, - string "=", + string ":", space, - p_str str] - | DStr (x, SOME sgn, str) => box [string "structure", - space, - string x, - space, - string ":", - space, - p_sgn sgn, - space, - string "=", - space, - p_str str] - | DFfiStr (x, sgn) => box [string "extern", - space, - string "structure", - space, - string x, - space, - string ":", - space, - p_sgn sgn] + p_sgn sgn] | DOpen (m, ms) => box [string "open", space, p_list_sep (string ".") string (m :: ms)] diff -r 27e731a65934 -r 4a03aa3251cb src/sources --- a/src/sources Sat Apr 28 12:00:35 2012 -0400 +++ b/src/sources Sun Apr 29 13:17:31 2012 -0400 @@ -78,6 +78,9 @@ elab_err.sig elab_err.sml +mod_db.sig +mod_db.sml + elaborate.sig elaborate.sml diff -r 27e731a65934 -r 4a03aa3251cb src/urweb.grm --- a/src/urweb.grm Sat Apr 28 12:00:35 2012 -0400 +++ b/src/urweb.grm Sun Apr 29 13:17:31 2012 -0400 @@ -262,7 +262,7 @@ | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | CARET | LET | IN - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | SELECT1 + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | SQL | SELECT1 | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE | VIEW | COOKIE | STYLE | TASK | POLICY | CASE | IF | THEN | ELSE | ANDALSO | ORELSE @@ -493,17 +493,16 @@ | FUN valis ([(DValRec valis, s (FUNleft, valisright))]) | SIGNATURE CSYMBOL EQ sgn ([(DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))]) - | STRUCTURE CSYMBOL EQ str ([(DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))]) - | STRUCTURE CSYMBOL COLON sgn EQ str ([(DStr (CSYMBOL, SOME sgn, str), s (STRUCTUREleft, strright))]) + | STRUCTURE CSYMBOL EQ str ([(DStr (CSYMBOL, NONE, NONE, str), s (STRUCTUREleft, strright))]) + | STRUCTURE CSYMBOL COLON sgn EQ str ([(DStr (CSYMBOL, SOME sgn, NONE, str), s (STRUCTUREleft, strright))]) | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN EQ str - ([(DStr (CSYMBOL1, NONE, + ([(DStr (CSYMBOL1, NONE, NONE, (StrFun (CSYMBOL2, sgn1, NONE, str), s (FUNCTORleft, strright))), s (FUNCTORleft, strright))]) | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn EQ str - ([(DStr (CSYMBOL1, NONE, + ([(DStr (CSYMBOL1, NONE, NONE, (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))), s (FUNCTORleft, strright))]) - | EXTERN STRUCTURE CSYMBOL COLON sgn ([(DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright))]) | OPEN mpath (case mpath of [] => raise Fail "Impossible mpath parse [1]" | m :: ms => [(DOpen (m, ms), s (OPENleft, mpathright))]) @@ -516,7 +515,7 @@ foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms in - [(DStr ("anon", NONE, (StrApp (m, str), loc)), loc), + [(DStr ("anon", NONE, NONE, (StrApp (m, str), loc)), loc), (DOpen ("anon", []), loc)] end) | OPEN CONSTRAINTS mpath (case mpath of diff -r 27e731a65934 -r 4a03aa3251cb src/urweb.lex --- a/src/urweb.lex Sat Apr 28 12:00:35 2012 -0400 +++ b/src/urweb.lex Sun Apr 29 13:17:31 2012 -0400 @@ -426,7 +426,6 @@ "end" => (Tokens.END (pos yypos, pos yypos + size yytext)); "functor" => (Tokens.FUNCTOR (pos yypos, pos yypos + size yytext)); "where" => (Tokens.WHERE (pos yypos, pos yypos + size yytext)); - "extern" => (Tokens.EXTERN (pos yypos, pos yypos + size yytext)); "include" => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext)); "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext)); "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));