adam@1732: (* Copyright (c) 2012, Adam Chlipala adam@1732: * All rights reserved. adam@1732: * adam@1732: * Redistribution and use in source and binary forms, with or without adam@1732: * modification, are permitted provided that the following conditions are met: adam@1732: * adam@1732: * - Redistributions of source code must retain the above copyright notice, adam@1732: * this list of conditions and the following disclaimer. adam@1732: * - Redistributions in binary form must reproduce the above copyright notice, adam@1732: * this list of conditions and the following disclaimer in the documentation adam@1732: * and/or other materials provided with the distribution. adam@1732: * - The names of contributors may not be used to endorse or promote products adam@1732: * derived from this software without specific prior written permission. adam@1732: * adam@1732: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adam@1732: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adam@1732: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adam@1732: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adam@1732: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adam@1732: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adam@1732: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adam@1732: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adam@1732: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adam@1732: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adam@1732: * POSSIBILITY OF SUCH DAMAGE. adam@1732: *) adam@1732: adam@1732: (* Cache of module code, with dependency information *) adam@1732: adam@1732: structure ModDb :> MOD_DB = struct adam@1732: adam@1732: open Elab adam@1732: adam@1732: structure SK = struct adam@1732: type ord_key = string adam@1732: val compare = String.compare adam@1732: end adam@1732: adam@1732: structure SS = BinarySetFn(SK) adam@1732: structure SM = BinaryMapFn(SK) adam@1732: structure IM = IntBinaryMap adam@1732: adam@1732: type oneMod = {Decl : decl, adam@1732: When : Time.time, adam@1732: Deps : SS.set} adam@1732: adam@1732: val byName = ref (SM.empty : oneMod SM.map) adam@1732: val byId = ref (IM.empty : string IM.map) adam@1732: adam@1732: fun reset () = (byName := SM.empty; adam@1732: byId := IM.empty) adam@1732: adam@1732: fun insert (d, tm) = adam@1732: let adam@1732: val xn = adam@1732: case #1 d of adam@1732: DStr (x, n, _, _) => SOME (x, n) adam@1732: | DFfiStr (x, n, _) => SOME (x, n) adam@1732: | _ => NONE adam@1732: in adam@1732: case xn of adam@1732: NONE => () adam@1732: | SOME (x, n) => adam@1732: let adam@1732: val skipIt = adam@1732: case SM.find (!byName, x) of adam@1732: NONE => false adam@1732: | SOME r => #When r = tm adam@1732: in adam@1732: if skipIt then adam@1732: () adam@1732: else adam@1732: let adam@1732: fun doMod (n', deps) = adam@1732: case IM.find (!byId, n') of adam@1732: NONE => deps adam@1732: | SOME x' => adam@1732: SS.union (deps, adam@1732: SS.add (case SM.find (!byName, x') of adam@1732: NONE => SS.empty adam@1732: | SOME {Deps = ds, ...} => ds, x')) adam@1732: adam@1732: val deps = ElabUtil.Decl.fold {kind = #2, adam@1732: con = fn (c, deps) => adam@1732: case c of adam@1732: CModProj (n', _, _) => doMod (n', deps) adam@1732: | _ => deps, adam@1732: exp = fn (e, deps) => adam@1732: case e of adam@1732: EModProj (n', _, _) => doMod (n', deps) adam@1732: | _ => deps, adam@1732: sgn_item = #2, adam@1732: sgn = fn (sg, deps) => adam@1732: case sg of adam@1732: SgnProj (n', _, _) => doMod (n', deps) adam@1732: | _ => deps, adam@1732: str = fn (st, deps) => adam@1732: case st of adam@1732: StrVar n' => doMod (n', deps) adam@1732: | _ => deps, adam@1732: decl = fn (d, deps) => adam@1732: case d of adam@1732: DDatatypeImp (_, _, n', _, _, _, _) => doMod (n', deps) adam@1732: | _ => deps} adam@1732: SS.empty d adam@1732: in adam@1732: byName := SM.insert (SM.filter (fn r => if SS.member (#Deps r, x) then adam@1732: case #1 (#Decl r) of adam@1732: DStr (_, n', _, _) => adam@1732: (byId := #1 (IM.remove (!byId, n')); adam@1732: false) adam@1757: | DFfiStr (_, n', _) => adam@1757: (byId := #1 (IM.remove (!byId, n')); adam@1757: false) adam@1732: | _ => raise Fail "ModDb: Impossible decl" adam@1732: else adam@1732: true) (!byName), adam@1732: x, adam@1732: {Decl = d, adam@1732: When = tm, adam@1732: Deps = deps}); adam@1732: byId := IM.insert (!byId, n, x) adam@1732: end adam@1732: end adam@1732: end adam@1732: adam@1732: fun lookup (d : Source.decl) = adam@1732: case #1 d of adam@1868: Source.DStr (x, _, SOME tm, _, _) => adam@1732: (case SM.find (!byName, x) of adam@1732: NONE => NONE adam@1732: | SOME r => adam@1732: if tm = #When r then adam@1732: SOME (#Decl r) adam@1732: else adam@1732: NONE) adam@1733: | Source.DFfiStr (x, _, SOME tm) => adam@1732: (case SM.find (!byName, x) of adam@1732: NONE => NONE adam@1732: | SOME r => adam@1732: if tm = #When r then adam@1732: SOME (#Decl r) adam@1732: else adam@1732: NONE) adam@1732: | _ => NONE adam@1732: adam@1737: val byNameBackup = ref (!byName) adam@1737: val byIdBackup = ref (!byId) adam@1737: adam@1737: fun snapshot () = (byNameBackup := !byName; byIdBackup := !byId) adam@1737: fun revert () = (byName := !byNameBackup; byId := !byIdBackup) adam@1737: adam@1732: end