From 05b7d79819dd5f006527bef7679b06868b3e0da7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 29 Apr 2012 13:17:31 -0400 Subject: Initial support for reusing elaboration results --- src/mod_db.sml | 144 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 src/mod_db.sml (limited to 'src/mod_db.sml') 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 -- cgit v1.2.3