Initial support for reusing elaboration results

1 files changed, 144 insertions, 0 deletions

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