Commit saveThmsLib.sig

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