blob: bbdc080bdc8521c6cd37df7a3fc7cc6059ff7325 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
signature saveThmsLib =
sig
(* This library provides utilities to persistently store maps from terms to theorems.
The issue is that theory files (i.e., Script.sml files) have no effects: it is
not possible to update the content of a reference in a Script.sml file and see
the effect of this change elsewhere. This is a problem because several tactics
and utilities require to maintain data bases of theorems in which we perform
lookups, and we generally add those theorems to the data bases right after we
proved them.
This file provides utilities to set up and maintain such a collection. An
important point is that we need to be able to derive, from a theorem, a
"term" that will be used as a key. We remember with a reference whether
the map from "terms" to theorems has been initialized: if not, we initialize
it before we perform any operation such as lookup or insert.
*)
include Abbrev
(* Helper *)
type thname = KernelSig.kernelname
val lookup_thm : string -> thname * thm
(* The user-provided functions *)
type 'key key_fns = {
compare : 'key * 'key -> order,
(* Retrieve the key from the theorem and normalize it at the same time *)
get_key_normalize_thm : thm -> ('key * thm)
}
(* The functions we return to the user to manipulate the map *)
type 'key map_fns = {
(* Persistently save a theorem *)
save_thm : string -> unit,
(* Persistently delete a theorem *)
delete_thm : string -> unit,
(* Temporarily save a theorem *)
temp_save_thm : thm -> unit,
(* Temporarily delete a theorem *)
temp_delete_thm : thm -> unit,
(* Get the key set *)
get_keys : unit -> 'key Redblackset.set,
(* Get the theorems map *)
get_map : unit -> ('key, thm) Redblackmap.dict
}
(* Initialize a persistent map *)
val create_map : 'key key_fns -> string -> 'key map_fns
end
|
