summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-29 13:17:31 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-29 13:17:31 -0400
commit47202985bda927a7504ee484565ebd2ff0e55963 (patch)
tree0ecad148d41060d9728486fd61309de6e8cb561e
parent626d7f93ab6873961e6b8c64f28ad36c808efd38 (diff)
Initial support for reusing elaboration results
-rw-r--r--src/compiler.sml25
-rw-r--r--src/elab_util.sig11
-rw-r--r--src/elab_util.sml11
-rw-r--r--src/elaborate.sig3
-rw-r--r--src/elaborate.sml224
-rw-r--r--src/mod_db.sig38
-rw-r--r--src/mod_db.sml144
-rw-r--r--src/source.sml4
-rw-r--r--src/source_print.sml46
-rw-r--r--src/sources3
-rw-r--r--src/urweb.grm13
-rw-r--r--src/urweb.lex1
12 files changed, 394 insertions, 129 deletions
diff --git a/src/compiler.sml b/src/compiler.sml
index ce6f95af..c30c2a04 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -917,7 +917,7 @@ val parse = {
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 @@ val parse = {
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 @@ val parse = {
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 @@ fun clibFile s = OS.Path.joinDirFile {dir = Config.libC,
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 --git a/src/elab_util.sig b/src/elab_util.sig
index 8a013554..b63d9b7f 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -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 @@ structure Decl : sig
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 --git a/src/elab_util.sml b/src/elab_util.sml
index df78616a..b799bbc4 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -1180,6 +1180,17 @@ fun mapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx s =
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 --git a/src/elaborate.sig b/src/elaborate.sig
index cc83b213..db325340 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -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 --git a/src/elaborate.sml b/src/elaborate.sml
index 71f5196f..c712ee2a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3641,7 +3641,7 @@ and wildifyStr env (str, sgn) =
| 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 @@ and wildifyStr env (str, sgn) =
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 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
([(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
- ()
+ | 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 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 (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
+ 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
- | L.DFfiStr (x, sgn) =>
- let
- val (sgn', gs') = elabSgn (env, denv) sgn
+ 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)
- val (env', n) = E.pushStrNamed env x sgn'
- in
- ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD 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 @@ and elabStr (env, denv) (str, loc) =
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 @@ fun elabFile basis topStr topSgn env file =
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 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 () = 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 (env', top_n) = E.pushStrNamed env' "Top" topSgn
val () = top_r := top_n
val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
diff --git a/src/mod_db.sig b/src/mod_db.sig
new file mode 100644
index 00000000..2b98ae6f
--- /dev/null
+++ b/src/mod_db.sig
@@ -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 --git a/src/mod_db.sml b/src/mod_db.sml
new file mode 100644
index 00000000..ba9bcc3a
--- /dev/null
+++ b/src/mod_db.sml
@@ -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 --git a/src/source.sml b/src/source.sml
index b85384ab..ce29904d 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -154,8 +154,8 @@ datatype decl' =
| 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 --git a/src/source_print.sml b/src/source_print.sml
index f6218d22..aad673f3 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -569,33 +569,33 @@ fun p_decl ((d, _) : decl) =
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 --git a/src/sources b/src/sources
index 4011ce3b..551d4ca5 100644
--- a/src/sources
+++ b/src/sources
@@ -78,6 +78,9 @@ disjoint.sml
elab_err.sig
elab_err.sml
+mod_db.sig
+mod_db.sml
+
elaborate.sig
elaborate.sml
diff --git a/src/urweb.grm b/src/urweb.grm
index c81ca9e6..0fe9b987 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -262,7 +262,7 @@ fun tnamesOf (e, _) =
| 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 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
| 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 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
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 --git a/src/urweb.lex b/src/urweb.lex
index 50ebe843..55fe4216 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -426,7 +426,6 @@ xint = x[0-9a-fA-F][0-9a-fA-F];
<INITIAL> "end" => (Tokens.END (pos yypos, pos yypos + size yytext));
<INITIAL> "functor" => (Tokens.FUNCTOR (pos yypos, pos yypos + size yytext));
<INITIAL> "where" => (Tokens.WHERE (pos yypos, pos yypos + size yytext));
-<INITIAL> "extern" => (Tokens.EXTERN (pos yypos, pos yypos + size yytext));
<INITIAL> "include" => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext));
<INITIAL> "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext));
<INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));