Mercurial > urweb

comparison src/mod_db.sml @ 1732:4a03aa3251cb

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