Start working on saveThmsLib

1 files changed, 190 insertions, 0 deletions

diff --git a/backends/hol4/saveThmsLib.sml b/backends/hol4/saveThmsLib.sml
new file mode 100644
index 00000000..df3a2b7a
--- /dev/null
+++ b/backends/hol4/saveThmsLib.sml
@@ -0,0 +1,190 @@
+structure saveThmsLib =
+struct
+
+type simpset = simpLib.simpset;
+
+open HolKernel boolLib markerLib;
+
+val op++ = simpLib.++;
+val op-* = simpLib.-*;
+
+val ERR = mk_HOL_ERR "saveThmsLib";
+
+fun add_simpls tyinfo ss =
+    (ss ++ simpLib.tyi_to_ssdata tyinfo) handle HOL_ERR _ => ss
+
+(* TODO: what is this? *)
+fun tyinfol() = TypeBasePure.listItems (TypeBase.theTypeBase())
+
+datatype stc_update = ADD_SSFRAG of simpLib.ssfrag | REMOVE_RWT of string
+type stc_state = simpset * bool * stc_update list
+  (* theorems, initialised-flag, update list (most recent first) *)
+
+val initial_simpset = simpLib.empty_ss
+fun ssf1 nth = simpLib.empty_ssfrag |> simpLib.add_named_rwt nth
+
+val state0 : stc_state = (initial_simpset, false, [])
+fun apply_delta d ((sset,initp,upds):stc_state) : stc_state =
+    case d of
+        ThmSetData.ADD nth =>
+        (sset ++ ssf1 nth, true, [])
+      | ThmSetData.REMOVE s => (sset -* [s], true, [])
+
+fun apply_stc_update (ADD_SSFRAG ssf, ss) = ss ++ ssf
+  | apply_stc_update (REMOVE_RWT n, ss) = ss -* [n]
+
+(* A stateful theorems collection *)
+datatype stc = STC_CON of {
+    name        : string,
+    thy_ssfrag  : (string -> ssfrag),
+    thy_simpset : (string -> simpset option),
+    get_ss      : (unit -> simpset),
+    export_thms : (string list -> unit)
+}
+
+(* Create a stateful theorems collection *)
+fun create_stateful_theorem_set (stc_name : string) : stc =
+  let
+(* val stc_name = "testStc" *)
+
+    fun init_state (st as (sset,initp,upds)) =
+        if initp then st
+        else
+          let fun init() =
+                  (List.foldl apply_stc_update sset (List.rev upds)
+                              |> rev_itlist add_simpls (tyinfol()),
+                   true, [])
+          in
+            HOL_PROGRESS_MESG ("Initialising STC simpset: " ^ stc_name ^ " ... ", "done") init ()
+          end
+
+    fun opt_partition f g ls =
+        let
+          fun recurse As Bs ls =
+              case ls of
+                  [] => (List.rev As, List.rev Bs)
+                | h::t => (case f h of
+                               SOME a => recurse (a::As) Bs t
+                             | NONE => (case g h of
+                                            SOME b => recurse As (b::Bs) t
+                                         | NONE => recurse As Bs t))
+        in
+          recurse [] [] ls
+        end
+
+    (* stale-ness is important for derived values. Derived values will get
+       re-calculated if their flag is true when the value is requested.
+    *)
+    val stale_flags = Sref.new ([] : bool Sref.t list)
+    fun notify () =
+        List.app (fn br => Sref.update br (K true)) (Sref.value stale_flags)
+
+    fun apply_to_global d (st as (sset,initp,upds):stc_state) : stc_state =
+        if not initp then
+          case d of
+              ThmSetData.ADD nth =>
+              let
+                open simpLib
+                val upds' =
+                    case upds of
+                        ADD_SSFRAG ssf :: rest =>
+                        ADD_SSFRAG (add_named_rwt nth ssf) :: rest
+                      | _ => ADD_SSFRAG (ssf1 nth) :: upds
+              in
+                (sset, initp, upds')
+              end
+            | ThmSetData.REMOVE s => (sset, initp, REMOVE_RWT s :: upds)
+        else
+          apply_delta d st before notify()
+
+    fun finaliser {thyname} deltas (sset,initp,upds) =
+      let
+        fun toNamedAdd (ThmSetData.ADD p) = SOME p | toNamedAdd _ = NONE
+        fun toRM (ThmSetData.REMOVE s) = SOME s | toRM _ = NONE
+        val (adds,rms) = opt_partition toNamedAdd toRM deltas
+        val ssfrag = simpLib.named_rewrites_with_names thyname (List.rev adds)
+          (* List.rev here preserves old behaviour wrt to the way theorems were
+             added to the global simpset; it will only make a difference when
+             overall rewrite system is not confluent *)
+        val new_upds = ADD_SSFRAG ssfrag :: map REMOVE_RWT rms
+      in
+        if initp then
+          (List.foldl apply_stc_update sset new_upds, true, []) before notify()
+        else (sset, false, List.revAppend(new_upds, upds))
+      end
+
+
+    val adresult as {DB,get_global_value,record_delta,update_global_value,...} =
+      ThmSetData.export_with_ancestry {
+        delta_ops = {
+          apply_delta = apply_delta,
+          apply_to_global = apply_to_global,
+          thy_finaliser = SOME finaliser,
+          initial_value = state0, uptodate_delta = K true
+        },
+        settype = stc_name
+      }
+
+    val get_deltas = #get_deltas adresult
+
+    (*
+    (* TODO: what is this? *)
+    fun update_fn tyi =
+      augment_stc_ss ([simpLib.tyi_to_ssdata tyi] handle HOL_ERR _ => [])
+
+    val () = TypeBase.register_update_fn (fn tyi => (update_fn tyi; tyi))
+    *)
+
+    fun get_ss () =
+        (update_global_value init_state;
+         #1 (get_global_value()))
+
+    fun export_thms slist =
+      let val ds = map ThmSetData.mk_add slist
+      in
+        List.app record_delta ds;
+        update_global_value (rev_itlist apply_to_global ds)
+      end
+
+    (* assume that there aren't any removes for things added in this theory;
+       it's not rational to do that; one should add it locally only, or not
+       add it at all
+    *)
+    fun mkfrag_from thy setdeltas =
+      let fun recurse ADDs [] = ADDs
+            | recurse ADDs (ThmSetData.ADD p :: rest) = recurse (p::ADDs) rest
+            | recurse ADDs (_ :: rest) = recurse ADDs rest
+          val ADDs = recurse [] setdeltas
+            (* order of addition is flipped; see above for why this is
+               "reasonable" *)
+      in
+        simpLib.named_rewrites_with_names thy ADDs
+      end
+    fun thy_ssfrag s = get_deltas {thyname=s} |> mkfrag_from s
+
+    fun thy_simpset s = Option.map (#1 o init_state) (DB {thyname=s})
+  in
+    STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset,
+              get_ss = get_ss, export_thms = export_thms }
+  end
+
+(*
+(* Create a stateful theorems collection *)
+val STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset, get_ss = get_ss, export_thms = export_thms } =
+  create_stateful_theorem_set "testStc1"
+
+Theorem th1:
+  T /\ (T /\ T)
+Proof
+  fs []
+QED
+
+export_thms ["th1"]
+
+fun rewrite_thms_of_simpset (ss : simpset) : thm list =
+  List.concat (map simpLib.frag_rewrites (simpLib.ssfrags_of ss))
+
+rewrite_thms_of_simpset (get_ss ())
+*)
+
+end