Mercurial > urweb

annotate src/mod_db.sml @ 2023:e4051315263e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix a bug in demos with 'rewrite all'
author Adam Chlipala <adam@chlipala.net>
date Wed, 11 Jun 2014 13:56:00 -0400
parents d6b0ee53dc93
children
rev   line source
adam@1732 1 (* Copyright (c) 2012, Adam Chlipala
adam@1732 2 * All rights reserved.
adam@1732 3 *
adam@1732 4 * Redistribution and use in source and binary forms, with or without
adam@1732 5 * modification, are permitted provided that the following conditions are met:
adam@1732 6 *
adam@1732 7 * - Redistributions of source code must retain the above copyright notice,
adam@1732 8 * this list of conditions and the following disclaimer.
adam@1732 9 * - Redistributions in binary form must reproduce the above copyright notice,
adam@1732 10 * this list of conditions and the following disclaimer in the documentation
adam@1732 11 * and/or other materials provided with the distribution.
adam@1732 12 * - The names of contributors may not be used to endorse or promote products
adam@1732 13 * derived from this software without specific prior written permission.
adam@1732 14 *
adam@1732 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1732 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1732 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1732 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adam@1732 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adam@1732 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1732 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1732 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1732 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1732 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1732 25 * POSSIBILITY OF SUCH DAMAGE.
adam@1732 26 *)
adam@1732 27
adam@1732 28 (* Cache of module code, with dependency information *)
adam@1732 29
adam@1732 30 structure ModDb :> MOD_DB = struct
adam@1732 31
adam@1732 32 open Elab
adam@1732 33
adam@1732 34 structure SK = struct
adam@1732 35 type ord_key = string
adam@1732 36 val compare = String.compare
adam@1732 37 end
adam@1732 38
adam@1732 39 structure SS = BinarySetFn(SK)
adam@1732 40 structure SM = BinaryMapFn(SK)
adam@1732 41 structure IM = IntBinaryMap
adam@1732 42
adam@1732 43 type oneMod = {Decl : decl,
adam@1732 44 When : Time.time,
adam@1732 45 Deps : SS.set}
adam@1732 46
adam@1732 47 val byName = ref (SM.empty : oneMod SM.map)
adam@1732 48 val byId = ref (IM.empty : string IM.map)
adam@1732 49
adam@1732 50 fun reset () = (byName := SM.empty;
adam@1732 51 byId := IM.empty)
adam@1732 52
adam@1732 53 fun insert (d, tm) =
adam@1732 54 let
adam@1732 55 val xn =
adam@1732 56 case #1 d of
adam@1732 57 DStr (x, n, _, _) => SOME (x, n)
adam@1732 58 | DFfiStr (x, n, _) => SOME (x, n)
adam@1732 59 | _ => NONE
adam@1732 60 in
adam@1732 61 case xn of
adam@1732 62 NONE => ()
adam@1732 63 | SOME (x, n) =>
adam@1732 64 let
adam@1732 65 val skipIt =
adam@1732 66 case SM.find (!byName, x) of
adam@1732 67 NONE => false
adam@1732 68 | SOME r => #When r = tm
adam@1732 69 in
adam@1732 70 if skipIt then
adam@1732 71 ()
adam@1732 72 else
adam@1732 73 let
adam@1732 74 fun doMod (n', deps) =
adam@1732 75 case IM.find (!byId, n') of
adam@1732 76 NONE => deps
adam@1732 77 | SOME x' =>
adam@1732 78 SS.union (deps,
adam@1732 79 SS.add (case SM.find (!byName, x') of
adam@1732 80 NONE => SS.empty
adam@1732 81 | SOME {Deps = ds, ...} => ds, x'))
adam@1732 82
adam@1732 83 val deps = ElabUtil.Decl.fold {kind = #2,
adam@1732 84 con = fn (c, deps) =>
adam@1732 85 case c of
adam@1732 86 CModProj (n', _, _) => doMod (n', deps)
adam@1732 87 | _ => deps,
adam@1732 88 exp = fn (e, deps) =>
adam@1732 89 case e of
adam@1732 90 EModProj (n', _, _) => doMod (n', deps)
adam@1732 91 | _ => deps,
adam@1732 92 sgn_item = #2,
adam@1732 93 sgn = fn (sg, deps) =>
adam@1732 94 case sg of
adam@1732 95 SgnProj (n', _, _) => doMod (n', deps)
adam@1732 96 | _ => deps,
adam@1732 97 str = fn (st, deps) =>
adam@1732 98 case st of
adam@1732 99 StrVar n' => doMod (n', deps)
adam@1732 100 | _ => deps,
adam@1732 101 decl = fn (d, deps) =>
adam@1732 102 case d of
adam@1732 103 DDatatypeImp (_, _, n', _, _, _, _) => doMod (n', deps)
adam@1732 104 | _ => deps}
adam@1732 105 SS.empty d
adam@1732 106 in
adam@1732 107 byName := SM.insert (SM.filter (fn r => if SS.member (#Deps r, x) then
adam@1732 108 case #1 (#Decl r) of
adam@1732 109 DStr (_, n', _, _) =>
adam@1732 110 (byId := #1 (IM.remove (!byId, n'));
adam@1732 111 false)
adam@1757 112 | DFfiStr (_, n', _) =>
adam@1757 113 (byId := #1 (IM.remove (!byId, n'));
adam@1757 114 false)
adam@1732 115 | _ => raise Fail "ModDb: Impossible decl"
adam@1732 116 else
adam@1732 117 true) (!byName),
adam@1732 118 x,
adam@1732 119 {Decl = d,
adam@1732 120 When = tm,
adam@1732 121 Deps = deps});
adam@1732 122 byId := IM.insert (!byId, n, x)
adam@1732 123 end
adam@1732 124 end
adam@1732 125 end
adam@1732 126
adam@1732 127 fun lookup (d : Source.decl) =
adam@1732 128 case #1 d of
adam@1868 129 Source.DStr (x, _, SOME tm, _, _) =>
adam@1732 130 (case SM.find (!byName, x) of
adam@1732 131 NONE => NONE
adam@1732 132 | SOME r =>
adam@1732 133 if tm = #When r then
adam@1732 134 SOME (#Decl r)
adam@1732 135 else
adam@1732 136 NONE)
adam@1733 137 | Source.DFfiStr (x, _, SOME tm) =>
adam@1732 138 (case SM.find (!byName, x) of
adam@1732 139 NONE => NONE
adam@1732 140 | SOME r =>
adam@1732 141 if tm = #When r then
adam@1732 142 SOME (#Decl r)
adam@1732 143 else
adam@1732 144 NONE)
adam@1732 145 | _ => NONE
adam@1732 146
adam@1737 147 val byNameBackup = ref (!byName)
adam@1737 148 val byIdBackup = ref (!byId)
adam@1737 149
adam@1737 150 fun snapshot () = (byNameBackup := !byName; byIdBackup := !byId)
adam@1737 151 fun revert () = (byName := !byNameBackup; byId := !byIdBackup)
adam@1737 152
adam@1732 153 end