Initial support for reusing elaboration results

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));