diff options
| -rw-r--r-- | backends/hol4/saveThmsLib.sig | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/backends/hol4/saveThmsLib.sig b/backends/hol4/saveThmsLib.sig new file mode 100644 index 00000000..9cbac1c7 --- /dev/null +++ b/backends/hol4/saveThmsLib.sig @@ -0,0 +1,46 @@ +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, + get_key_from_thm : thm -> 'key + } + + (* The functions we return to the user to manipulate the map *) + type 'key map_fns = { + (* Persistently save a theorem *) + save_thm : string -> unit, + (* Temporarily save a theorem *) + temp_save_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 |