1(* ------------------------------------------------------------------------- *)
2(*                                                                           *)
3(*   A database of lemmas. This is currently accessible in the               *)
4(*   following ways:                                                         *)
5(*                                                                           *)
6(*     - strings used to denote (part of) the name of the binding,           *)
7(*       or the full name of the theory of interest. Case is not             *)
8(*       significant.                                                        *)
9(*                                                                           *)
10(*     - a general matcher on the term structure of theorems.                *)
11(*                                                                           *)
12(*     - matching (higher order) on the term structure of theorems.          *)
13(*                                                                           *)
14(*     - looking up a specific theorem in a specific segment.                *)
15(*                                                                           *)
16(* ------------------------------------------------------------------------- *)
17
18structure DB :> DB =
19struct
20
21open HolKernel DB_dtype;
22
23val ERR = mk_HOL_ERR "DB";
24
25fun indef_class2string Thm = "a theorem"
26  | indef_class2string Axm = "an axiom"
27  | indef_class2string Def = "a definition"
28
29
30(*---------------------------------------------------------------------------
31    The pair of strings is theory * bindname
32 ---------------------------------------------------------------------------*)
33
34type data    = (string * string) * (thm * class)
35
36fun dataName (((_, nm), _) : data) = nm
37fun dataThy (((thy, _), _) : data) = thy
38fun dataNameEq s d = dataName d = s
39
40
41(*---------------------------------------------------------------------------
42   Map keys to canonical case
43 ---------------------------------------------------------------------------*)
44
45fun toLower s =
46 let open Char CharVector in tabulate(size s, fn i => toLower(sub(s,i))) end
47
48(*---------------------------------------------------------------------------
49     Persistence: bindl is used to populate the database when a theory
50     is loaded.
51 ---------------------------------------------------------------------------*)
52
53structure Map = Redblackmap
54(* the keys are lower-cased, but the data also stores the keys, and there
55   the key infomration is kept in its original case *)
56
57fun updexisting key f m =
58    case Map.peek(m,key) of
59        NONE => m
60      | SOME v => Map.insert(m,key,f v)
61
62(* the submap is a map from lowercased item-name to those items with the
63   same name.  There is a list of them because item-names are really
64   case-sensitive *)
65type submap = (string, data list) Map.dict
66val empty_sdata_map = Map.mkDict String.compare
67
68(* the dbmap contains:
69    - a map from theory-name to a submap (as above)
70*)
71datatype dbmap = DB of { namemap : (string, submap) Map.dict,
72                         revmap : location list Termtab.table,
73                         localmap : thm Symtab.table
74                       }
75
76fun namemap (DB{namemap,...}) = namemap
77fun revmap (DB{revmap,...}) = revmap
78fun localmap (DB{localmap,...}) = localmap
79fun updnamemap f (DB{namemap,revmap,localmap}) =
80    DB {namemap = f namemap, revmap = revmap, localmap = localmap}
81fun updrevmap f (DB{namemap,revmap,localmap}) =
82    DB {namemap = namemap, revmap = f revmap, localmap=localmap}
83fun updlocalmap f (DB{namemap,revmap,localmap}) =
84    DB {namemap = namemap, revmap = revmap, localmap = f localmap}
85
86val empty_dbmap = DB {namemap = Map.mkDict String.compare,
87                      localmap = Symtab.empty, revmap = Termtab.empty}
88
89local val DBref = ref empty_dbmap
90      fun lemmas() = !DBref
91      fun add_to_submap m (newdata as ((s1, s2), x)) =
92          let val s2key = toLower s2
93              val oldvalue = case Map.peek(m, s2key) of
94                               NONE => []
95                             | SOME items => items
96          in
97            Map.insert(m, s2key,
98                       newdata :: List.filter (not o dataNameEq s2) oldvalue)
99          end
100      fun functional_bindl_names thy blist namemap =
101          (* used when a theory is loaded from disk *)
102          let val submap =
103                  case Map.peek(namemap, thy) of
104                    NONE => empty_sdata_map
105                  | SOME m => m
106              fun foldthis ((n,th,cl), m) = add_to_submap m ((thy,n), (th,cl))
107              val submap' = List.foldl foldthis submap blist
108          in
109            Map.insert(namemap, thy, submap')
110          end
111      fun functional_bindl_revmap thy blist revmap =
112          List.foldl
113            (fn ((n,th,cl), A) =>
114                Termtab.cons_list(concl th,Stored {Thy = thy,Name = n}) A)
115            revmap
116            blist
117      fun functional_bindl db thy blist =
118          db |> updnamemap (functional_bindl_names thy blist)
119             |> updrevmap (functional_bindl_revmap thy blist)
120
121      fun purge_stale_bindings() =
122          let
123            open Map
124            fun foldthis (n, datas : data list, m) =
125                let
126                  val data' = List.filter (fn (_, (th, _)) => uptodate_thm th)
127                                          datas
128                in
129                  insert(m,n,data')
130                end
131            fun purge_stale ttab =
132                let open Termtab
133                in
134                  fold (fn (t,d) => fn A =>
135                           if uptodate_term t then update (t,d) A else A)
136                       ttab
137                       empty
138                end
139            val ct = current_theory()
140          in
141            DBref := ((!DBref)
142                       |> updnamemap
143                            (updexisting ct (foldl foldthis empty_sdata_map))
144                       |> updrevmap purge_stale)
145          end
146
147      fun delete_binding bnm =
148          let
149            open Map
150            val ct = current_theory()
151            fun smdelbinding bnm sm =
152                case peek (sm, toLower bnm) of
153                    NONE => sm
154                  | SOME datas =>
155                    insert(sm,toLower bnm,
156                           List.filter(not o dataNameEq bnm) datas)
157          in
158            DBref := updnamemap (updexisting ct (smdelbinding bnm)) (!DBref)
159          end
160
161
162      fun hook thydelta =
163          let
164            open TheoryDelta
165            fun toThmClass (s, ThmKind_dtype.Thm th) = (s, th, Thm)
166              | toThmClass (s, ThmKind_dtype.Axiom(sn,th)) = (s, th, Axm)
167              | toThmClass (s, ThmKind_dtype.Defn th) = (s, th, Def)
168          in
169            case thydelta of
170                DelConstant _ => purge_stale_bindings()
171              | DelTypeOp _ => purge_stale_bindings()
172              | NewBinding nb =>
173                (
174                  if Theory.is_temp_binding (#1 nb) then ()
175                  else
176                    DBref := functional_bindl (!DBref) (current_theory())
177                                              [toThmClass nb]
178                )
179              | DelBinding s => delete_binding s
180              | _ => ()
181          end
182      val _ = Theory.register_hook("DB", hook)
183in
184fun bindl thy blist = DBref := functional_bindl (lemmas()) thy blist
185fun revlookup th = Termtab.lookup_list (revmap (!DBref)) (concl th)
186(*---------------------------------------------------------------------------
187    To the database representing all ancestor theories, add the
188    entries in the current theory segment.
189 ---------------------------------------------------------------------------*)
190fun CT() = !DBref
191
192fun store_local s th =
193    DBref := (!DBref |> updlocalmap (Symtab.update(s,th))
194                     |> updrevmap (Termtab.cons_list(concl th, Local s)))
195fun local_thm s = Symtab.lookup (localmap (!DBref)) s
196
197end (* local *)
198
199
200
201(*---------------------------------------------------------------------------
202     Misc. support
203 ---------------------------------------------------------------------------*)
204
205val occurs = String.isSubstring
206
207fun norm_thyname "-" = current_theory()
208  | norm_thyname s = s;
209
210
211(*---------------------------------------------------------------------------
212     thy  : All entries in a specified theory
213     find : Look up something by name fragment
214 ---------------------------------------------------------------------------*)
215
216fun thy s =
217    let
218      val DB{namemap,...} = CT()
219    in
220      case Map.peek(namemap, norm_thyname s) of
221          NONE => []
222        | SOME m => Map.foldl (fn (lcnm, datas, A) => datas @ A) [] m
223    end
224
225fun findpred pat s =
226    let
227      val pat = toLower pat and s = toLower s
228      val orparts = String.tokens (equal #"|") pat
229      val subparts = map (String.tokens (equal #"~")) orparts
230      val subpred = List.all (C occurs s)
231    in
232      List.exists subpred subparts
233    end
234
235fun find s =
236    let
237      val DB{namemap,...} = CT()
238      fun subfold (k, v, acc) = if findpred s k then v @ acc else acc
239      fun fold (thy, m, acc) = Map.foldr subfold acc m
240    in
241      Map.foldr fold [] namemap
242    end
243
244
245(*---------------------------------------------------------------------------
246      Look up something by matching. Parameterized by the matcher.
247 ---------------------------------------------------------------------------*)
248
249fun matchp P thylist =
250    let fun data_P (_, (th, _)) = P th
251        fun subfold (k, v, acc) = List.filter data_P v @ acc
252    in
253      case thylist of
254        [] => let fun fold (k, m, acc) = Map.foldr subfold acc m
255              in
256                Map.foldr fold [] (namemap (CT()))
257              end
258      | _ => let val db = namemap (CT())
259                 fun fold (thyn, acc) =
260                     case Map.peek(db, norm_thyname thyn) of
261                       NONE => acc
262                     | SOME m => Map.foldr subfold acc m
263             in
264               List.foldr fold [] thylist
265             end
266    end
267
268
269fun matcher f thyl pat =
270  matchp (fn th => can (find_term (can (f pat))) (concl th)) thyl;
271
272val match = matcher (ho_match_term [] empty_tmset);
273val apropos = match [];
274
275(* matches : term -> thm -> bool
276  tests whether theorem matches pattern *)
277fun matches pat th =
278  can (find_term (can (ho_match_term [] empty_tmset pat))) (concl th) ;
279
280fun apropos_in pat dbdata =
281  List.filter (fn (_, (th, _)) => matches pat th) dbdata ;
282
283fun find_in s = List.filter (findpred s o dataName)
284
285fun listDB () =
286    let fun subfold (k,v,acc) = v @ acc
287        fun fold (_, m, acc) = Map.foldr subfold acc m
288    in
289      Map.foldr fold [] (namemap (CT()))
290    end
291
292fun selectDB sels =
293    let
294      fun selfn (SelTM pat) = apropos_in pat
295        | selfn (SelNM s) = find_in s
296        | selfn (SelTHY s) = List.filter (equal (norm_thyname s) o dataThy)
297      fun recurse sels d =
298          case sels of
299              [] => d
300            | s::rest => recurse rest (selfn s d)
301    in
302      recurse sels (listDB())
303    end
304
305
306(*---------------------------------------------------------------------------
307      Some other lookup functions
308 ---------------------------------------------------------------------------*)
309
310fun thm_class origf thy name = let
311  val db = namemap (CT())
312  val thy = norm_thyname thy
313  val nosuchthm = ("theorem "^thy^"$"^name^" not found")
314  val thymap = Map.find(db, thy)
315               handle Map.NotFound => raise ERR origf ("no such theory: "^thy)
316  val result = Map.find(thymap, toLower name)
317               handle Map.NotFound => raise ERR origf nosuchthm
318in
319  case filter (equal (norm_thyname thy,name) o fst) result of
320    [(_,p)] => p
321  | [] => raise ERR origf nosuchthm
322  | other => raise ERR origf
323                       ("multiple things in theory "^thy^" with name "^name)
324end
325
326fun fetch s1 s2 = fst (thm_class "fetch" s1 s2);
327
328fun thm_of ((_,n),(th,_)) = (n,th);
329fun is x (_,(_,cl)) = (cl=x)
330
331val thms        = List.map thm_of o thy
332val theorems    = List.map thm_of o Lib.filter (is Thm) o thy
333val definitions = List.map thm_of o Lib.filter (is Def) o thy
334val axioms      = List.map thm_of o Lib.filter (is Axm) o thy
335
336fun theorem s = let
337  val (thm,c) = thm_class "theorem" "-" s
338in
339  if c = Thm then thm
340  else raise ERR "theorem" ("No theorem in current theory of name "^s^
341                            " (but there is "^indef_class2string c^")")
342end
343
344fun definition s = let
345  val (thm,c) = thm_class "definition" "-" s
346in
347  if c = Def then thm
348  else raise ERR "theorem" ("No definition in current theory of name "^s^
349                            " (but there is "^indef_class2string c^")")
350end
351
352fun axiom s = let
353  val (thm,c) = thm_class "axiom" "-" s
354in
355  if c = Axm then thm
356  else raise ERR "axiom" ("No axiom in current theory of name "^s^
357                          " (but there is "^indef_class2string c^")")
358end
359
360fun dest_theory s =
361 let val thyname = if s = "-" then Theory.current_theory () else s
362 in
363   THEORY (thyname,
364    {types = rev (Theory.types thyname),
365     consts = rev (map dest_const (Theory.constants thyname)),
366     parents = Theory.parents thyname,
367     axioms = axioms thyname,
368     definitions = definitions thyname,
369     theorems = theorems thyname})
370 end
371 handle e => raise ERR "dest_theory" (Lib.quote s^" is not a known theory");
372
373end
374