Make the unfolding theorems collection from evalLib persistent

10 files changed, 235 insertions, 251 deletions

diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 1e95b6c5..c9d8806d 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -904,6 +904,8 @@ fun DefineDiv (def_qt : term quotation) =
        (we still do it: it doesn't cost much). *)
     val _ = app delete_binding thm_names
     val _ = map store_definition (zip thm_names def_eqs)
+    (* Also save the custom unfoldings, for evaluation (unit tests) *)
+    val _ = evalLib.add_unfold_thms thm_names
   in
     def_eqs
   end
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml
index 2e6d56b6..b01ec053 100644
--- a/backends/hol4/divDefLibTestScript.sml
+++ b/backends/hol4/divDefLibTestScript.sml
@@ -13,6 +13,21 @@ Datatype:
   | ListNil
 End
 
+(* A version of [nth] which doesn't use machine integers *)
+val [nth0_def] = DefineDiv ‘
+  nth0 (ls : 't list_t) (i : int) : 't result =
+    case ls of
+    | ListCons x tl =>
+      if i = (0:int)
+      then (Return x)
+      else
+        do
+        nth0 tl (i - 1)
+        od
+    | ListNil => Fail Failure
+’
+val _ = primitivesLib.assert_return “nth0 (ListCons 0 ListNil) 0”
+
 val [nth_def] = DefineDiv ‘
   nth (ls : 't list_t) (i : u32) : 't result =
     case ls of
@@ -26,6 +41,7 @@ val [nth_def] = DefineDiv ‘
         od
     | ListNil => Fail Failure
 ’
+val _ = primitivesLib.assert_return “nth (ListCons 0 ListNil) (int_to_u32 0)”
 
 (* even, odd *)
 
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index 526f74a6..d8cc4ab5 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -13,6 +13,7 @@ sig
     val list_t_size_def : thm
     val node_TY_DEF : thm
     val node_case_def : thm
+    val nth0_def : thm
     val nth_def : thm
     val odd_def : thm
     val tree_TY_DEF : thm
@@ -180,6 +181,14 @@ sig
       
       ⊢ ∀a f. node_CASE (Node a) f = f a
    
+   [nth0_def]  Definition
+      
+      ⊢ ∀ls i.
+          nth0 ls i =
+          case ls of
+            ListCons x tl => if i = 0 then Return x else nth0 tl (i − 1)
+          | ListNil => Fail Failure
+   
    [nth_def]  Definition
       
       ⊢ ∀ls i.
diff --git a/backends/hol4/evalLib.sig b/backends/hol4/evalLib.sig
index d045d3bb..f44cff13 100644
--- a/backends/hol4/evalLib.sig
+++ b/backends/hol4/evalLib.sig
@@ -8,10 +8,7 @@ sig
 
   include Abbrev
 
-  (* The following functions allow to register custom unfolding theorems *)
-  (* TODO: permanence of theorems? *)
-  val add_unfold : term * thm -> unit
-  val add_unfolds : (term * thm) list -> unit
+  (* The following functions allow to *persistently* register custom unfolding theorems *)
   val add_unfold_thm : thm -> unit
   val add_unfold_thms : thm list -> unit
 
diff --git a/backends/hol4/evalLib.sml b/backends/hol4/evalLib.sml
index 30e28eed..85a6b94a 100644
--- a/backends/hol4/evalLib.sml
+++ b/backends/hol4/evalLib.sml
@@ -27,37 +27,61 @@ fun get_const_name (tm : term) : const_name =
     (thy, name)
   end
 
-(* TODO: should we rather use srw_ss ()?
-   TODO: permanence of saved theorems? (see BasicProvers.export_rewrites) *)
-val custom_rewrites : ssfrag ref = ref empty_ssfrag
-val custom_unfolds : ((const_name, thm) Redblackmap.dict) ref = ref (Redblackmap.mkDict const_name_compare)
-val custom_unfolds_consts : (term Redblackset.set) ref = ref (Redblackset.empty Term.compare)
+(* Create the persistent collection, which is a pair:
+   (set of constants, map from constant name to theorem)
+ *)
+type state = term Redblackset.set * (const_name, thm) Redblackmap.dict
+fun get_custom_unfold_const (th : thm) : term = (fst o strip_comb o lhs o snd o strip_forall o concl) th
 
-fun add_rewrites (thms : thm list) : unit =
+(* Small helper *)
+fun add_to_state (th : thm) (s, m) =
   let
-    val rewrs = frag_rewrites (!custom_rewrites)
-    val _ = custom_rewrites := rewrites (List.@ (thms,  rewrs))
+    val k = get_custom_unfold_const th
+    val name = get_const_name k
+    val s = Redblackset.add (s, k)
+    val m = Redblackmap.insert (m, name, th)
   in
-    ()
+    (s, m)
   end
 
-fun add_unfold (tm : term, th : thm) : unit =
+(* Persistently update the maps given a delta  *)
+fun apply_delta (delta : ThmSetData.setdelta) st =
+  case delta of
+    ThmSetData.ADD (_, th) => add_to_state th st
+  | ThmSetData.REMOVE _ =>
+    raise mk_HOL_ERR "saveThmsLib" "create_map" ("Unexpected REMOVE")
+
+(* Initialize the collection *)
+val init_state = (Redblackset.empty compare, Redblackmap.mkDict const_name_compare)
+val {update_global_value, (* Local update *)
+     record_delta, (* Global update *)
+     get_global_value,
+     ...} =
+    ThmSetData.export_with_ancestry {
+      settype = "custom_unfold_theorems",
+      delta_ops = {apply_to_global = apply_delta,
+                   uptodate_delta = K true,
+                   thy_finaliser = NONE,
+                   initial_value = init_state,
+                   apply_delta = apply_delta}
+    }
+
+fun add_unfold_thm (s : string) : unit =
   let
-    val _ = custom_unfolds := Redblackmap.insert (!custom_unfolds, get_const_name tm, th)
-    val _ = custom_unfolds_consts := Redblackset.add (!custom_unfolds_consts, tm)
+    val th = saveThmsLib.lookup_thm s
   in
-    ()
+    (* Record the delta - for persistence for the future sessions *)
+      record_delta (ThmSetData.ADD th);
+    (* Update the global value - for the current session: record_delta
+       doesn't update the state of the current session *)
+    update_global_value (add_to_state (snd th))
   end
 
-fun add_unfolds (ls : (term * thm) list) : unit =
-  app add_unfold ls
-
-fun get_custom_unfold_const (th : thm) : term = (fst o strip_comb o lhs o snd o strip_forall o concl) th
-fun add_unfold_thm (th : thm) : unit = add_unfold (get_custom_unfold_const th, th)
-fun add_unfold_thms (ls : thm list) : unit = app add_unfold_thm ls
+fun add_unfold_thms (ls : string list) : unit =
+  app add_unfold_thm ls
 
 fun get_unfold_thms () : thm list =
-  map snd (Redblackmap.listItems (!custom_unfolds))
+  map snd (Redblackmap.listItems (snd (get_global_value ())))
 
 (* Apply a custom unfolding to the term, if possible.
 
@@ -65,6 +89,9 @@ fun get_unfold_thms () : thm list =
  *)
 fun apply_custom_unfold (tm : term) : thm =
   let
+    (* Retrieve the custom unfoldings *)
+    val custom_unfolds = snd (get_global_value ())
+
     (* Remove all the matches to find the top-most scrutinee *)
     val scrut = strip_all_cases_get_scrutinee tm
     (* Find an unfolding to apply: we look at the application itself, then
@@ -80,7 +107,7 @@ fun apply_custom_unfold (tm : term) : thm =
            theorem *)
         val c = (fst o strip_comb) tm
         val cname = get_const_name c
-        val unfold_th = Redblackmap.find (!custom_unfolds, cname)
+        val unfold_th = Redblackmap.find (custom_unfolds, cname)
           handle Redblackmap.NotFound => failwith "No theorem found"
         (* Instantiate the theorem *)
         val unfold_th = SPEC_ALL unfold_th
@@ -121,7 +148,7 @@ fun apply_custom_unfold (tm : term) : thm =
 fun eval_conv tm =
   let
     (* TODO: optimize: we recompute the list each time... *)
-    val restr_tms = Redblackset.listItems (!custom_unfolds_consts)
+    val restr_tms = Redblackset.listItems (fst (get_global_value ()))
     (* We do the following:
        - use the standard EVAL conv, but restrains it from unfolding terms for
          which we have custom unfolding theorems
@@ -129,7 +156,7 @@ fun eval_conv tm =
        - simplify
      *)
     val standard_eval = RESTR_EVAL_CONV restr_tms
-    val simp_no_fail_conv = (fn x => SIMP_CONV (srw_ss () ++ !custom_rewrites) [] x handle UNCHANGED => REFL x)
+    val simp_no_fail_conv = (fn x => SIMP_CONV (srw_ss ()) [] x handle UNCHANGED => REFL x)
     val one_step_conv = standard_eval THENC (apply_custom_unfold THENC simp_no_fail_conv)
     (* Wrap the conversion such that it fails if the term is unchanged *)
     fun one_step_changed_conv tm = (CHANGED_CONV one_step_conv) tm
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 3d6d9e3e..143e25ce 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -648,9 +648,27 @@ fun strip_all_cases_get_scrutinee (t : term) : term =
        For instance: (fst o strip_case) “if i = 0 then ... else ...”
        returns “i” while we want to get “i = 0”.
 
-       We use [dest_case] for this reason.
+       Also, [dest_case] sometimes fails.
+       
+       Ex.:
+       {[
+         val t = “result_CASE (if T then Return 0 else Fail Failure) (λy. Return ()) Fail Diverge”
+         dest_case t
+       ]}
+       TODO: file an issue
+
+       We use a custom function [get_case_scrutinee] instead of [dest_case] for this reason.
      *)
-    (strip_all_cases_get_scrutinee o (fn (_, x, _) => x) o TypeBase.dest_case) t
+    let
+      fun get_case_scrutinee t =
+        let
+          val (_, tms) = strip_comb t
+        in
+          hd tms
+        end
+    in
+    (strip_all_cases_get_scrutinee o get_case_scrutinee) t
+    end
   else t
 
 (*
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index eed50e25..776843bf 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -511,4 +511,19 @@ val progress : tactic =
     map_first_tac progress_with thl (asms, g)
   end
 
+(* Small utility: check that a term evaluates to “Return” (used by the unit tests) *)
+fun assert_return (tm0 : term) : unit =
+  let
+    (* Evaluate the term *)
+    val tm = evalLib.eval tm0
+    (* Deconstruct it *)
+    val (app, _) = strip_comb tm
+    val {Thy, Name, ...} = dest_thy_const app
+    handle HOL_ERR _ => raise (mk_HOL_ERR "primitivesLib" "assert_return" ("The term doesn't evaluate to “Return ...”: " ^ term_to_string tm ^ "\n, final result: " ^ term_to_string tm))
+  in
+    if Thy = "primitives" andalso Name = "Return" then ()
+    else
+      raise (mk_HOL_ERR "primitivesLib" "assert_return" ("The term doesn't evaluate to “Return ...”: " ^ term_to_string tm ^ "\n, final result: " ^ term_to_string tm))
+  end
+
 end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 6f54fbfc..e10ce7e5 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -368,7 +368,21 @@ val all_int_to_scalar_to_int_unfold_lemmas = [
   u64_to_int_int_to_u64_unfold,
   u128_to_int_int_to_u128_unfold
 ]
-val _ = evalLib.add_unfold_thms (all_int_to_scalar_to_int_unfold_lemmas)
+
+val _ = evalLib.add_unfold_thms [
+  "isize_to_int_int_to_isize_unfold",
+  "i8_to_int_int_to_i8_unfold",
+  "i16_to_int_int_to_i16_unfold",
+  "i32_to_int_int_to_i32_unfold",
+  "i64_to_int_int_to_i64_unfold",
+  "i128_to_int_int_to_i128_unfold",
+  "usize_to_int_int_to_usize_unfold",
+  "u8_to_int_int_to_u8_unfold",
+  "u16_to_int_int_to_u16_unfold",
+  "u32_to_int_int_to_u32_unfold",
+  "u64_to_int_int_to_u64_unfold",
+  "u128_to_int_int_to_u128_unfold"
+]
 
 val int_to_i8_i8_to_int       = new_axiom ("int_to_i8_i8_to_int",       “∀i. int_to_i8 (i8_to_int i) = i”)
 val int_to_i16_i16_to_int     = new_axiom ("int_to_i16_i16_to_int",     “∀i. int_to_i16 (i16_to_int i) = i”)
@@ -1614,7 +1628,7 @@ Theorem mk_vec_unfold:
 Proof
   metis_tac [mk_vec_axiom]
 QED
-val _ = evalLib.add_unfold_thm mk_vec_unfold
+val _ = evalLib.add_unfold_thm "mk_vec_unfold"
 
 (* Defining ‘vec_insert_back’ *)
 val vec_insert_back_def = Define ‘
@@ -1645,33 +1659,4 @@ Proof
   sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
 QED
 
-(* TODO: add theorems to the rewriting theorems
-from listSimps.sml:
-
-val LIST_ss = BasicProvers.thy_ssfrag "list"
-val _ = BasicProvers.logged_addfrags {thyname="list"} [LIST_EQ_ss]
-
-val list_rws = computeLib.add_thms
-  [
-   ALL_DISTINCT, APPEND, APPEND_NIL, CONS_11, DROP_compute, EL_restricted,
-   EL_simp_restricted, EVERY_DEF, EXISTS_DEF, FILTER, FIND_def, FLAT, FOLDL,
-   FOLDR, FRONT_DEF, GENLIST_AUX_compute, GENLIST_NUMERALS, HD, INDEX_FIND_def,
-   INDEX_OF_def, LAST_compute, LENGTH, LEN_DEF, LIST_APPLY_def, LIST_BIND_def,
-   LIST_IGNORE_BIND_def, LIST_LIFT2_def, LIST_TO_SET_THM, LLEX_def, LRC_def,
-   LUPDATE_compute, MAP, MAP2, NOT_CONS_NIL, NOT_NIL_CONS, NULL_DEF, oEL_def,
-   oHD_def,
-   PAD_LEFT, PAD_RIGHT, REVERSE_REV, REV_DEF, SHORTLEX_def, SNOC, SUM_ACC_DEF,
-   SUM_SUM_ACC,
-   TAKE_compute, TL, UNZIP, ZIP, computeLib.lazyfy_thm list_case_compute,
-   dropWhile_def, isPREFIX, list_size_def, nub_def, splitAtPki_def
-  ]
-
-fun list_compset () =
-   let
-      val base = reduceLib.num_compset()
-   in
-      list_rws base; base
-   end
-*)
-
 val _ = export_theory ()
diff --git a/backends/hol4/saveThmsLib.sml b/backends/hol4/saveThmsLib.sml
index d2523eeb..76b428cf 100644
--- a/backends/hol4/saveThmsLib.sml
+++ b/backends/hol4/saveThmsLib.sml
@@ -1,196 +1,107 @@
-structure saveThmsLib =
+structure saveThmsLib :> saveThmsLib =
 struct
 
-type simpset = simpLib.simpset;
+open HolKernel Abbrev
 
-open HolKernel boolLib markerLib;
+type thname = KernelSig.kernelname
 
-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 -> simpLib.ssfrag,
-    thy_simpset : string -> simpset option,
-    get_ss      : unit -> simpset,
-    export_thms : string list -> unit
+(* The user-provided functions *)
+type 'key key_fns = {
+  compare : 'key * 'key -> order,
+  get_key_from_thm : thm -> 'key
 }
 
-(* Create a stateful theorems collection *)
-fun create_stateful_theorem_set (stc_name : string) =
-  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
+(* 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
+}
 
-    (* 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
+(* This function is adapted from ThmSetData.sml.
 
-    fun thy_simpset s = Option.map (#1 o init_state) (DB {thyname=s})
+   It raises an exception if it can't find a theorem.
+ *)
+fun lookup_thm (s : string) : thname * thm =
+  let
+    val name =
+     case String.fields (equal #".") s of
+         [s0] => {Thy = current_theory(), Name = s}
+       | [s1,s2] => {Thy = s1, Name = s2}
+       | _ => raise mk_HOL_ERR "saveThmsLib" "lookup_thm" ("Malformed name: " ^ s)
+    fun lookup_exn {Thy,Name} = DB.fetch Thy Name
   in
-    STC_CON { name = stc_name, thy_ssfrag = thy_ssfrag, thy_simpset = thy_simpset,
-              get_ss = get_ss, export_thms = export_thms }
+    (name, lookup_exn name)
   end
 
-fun rewrite_thms_of_simpset (ss : simpset) : thm list =
-  List.concat (map simpLib.frag_rewrites (simpLib.ssfrags_of ss))
-
-(*
-(* 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"
+(* The state, a pair (set of keys, map from keys to theorems) *)
+type 'key state = 'key Redblackset.set * ('key, thm) Redblackmap.dict
 
-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 ())
-*)
-
-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"
+(* Initialize a persistent map *)
+fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns =
+  let
+     val { compare, get_key_from_thm } = kf
+     
+     (* Small helper *)
+     fun add_to_state (th : thm) (s, m) =
+       let
+         val k = get_key_from_thm th
+         val s = Redblackset.add (s, k)
+         val m = Redblackmap.insert (m, k, th)
+       in
+         (s, m)
+       end
+  
+     (* Persistently update the map given a delta  *)
+     fun apply_delta (delta : ThmSetData.setdelta) st =
+       case delta of
+         ThmSetData.ADD (_, th) => add_to_state th st
+       | ThmSetData.REMOVE _ =>
+         raise mk_HOL_ERR "saveThmsLib" "create_map" ("Unexpected REMOVE")
+
+     (* Initialize the dictionary *)
+     val init_state = (Redblackset.empty compare, Redblackmap.mkDict compare)
+     val {update_global_value, (* Local update *)
+          record_delta, (* Global update *)
+          get_deltas,
+          get_global_value,
+          DB = eval_ruleuction_map_by_theory,...} =
+         ThmSetData.export_with_ancestry {
+           settype = name,
+           delta_ops = {apply_to_global = apply_delta,
+                        uptodate_delta = K true,
+                        thy_finaliser = NONE,
+                        initial_value = init_state,
+                        apply_delta = apply_delta}
+         }
+
+     (* Temporarily save a theorem: update the current session, but don't
+        save the delta for the future sessions. *)
+     fun temp_save_thm (th : thm) : unit =
+       update_global_value (add_to_state th)
+
+     (* Persistently save a theorem *)
+     fun save_thm (s : string) : unit =
+       let
+         val th = lookup_thm s
+       in
+         (* Record delta saves a delta for the future sessions, but doesn't
+            update the current sessions, which is why we also call [temp_save_thm] *)
+           record_delta (ThmSetData.ADD th);
+           temp_save_thm (snd th)
+       end
+
+     (* *)
+     val get_keys = fst o get_global_value
+     val get_map = snd o get_global_value
+  in
+    { save_thm = save_thm, temp_save_thm = temp_save_thm,
+      get_keys = get_keys, get_map = get_map }
+  end
 
 end
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0decbff1..2f1898b3 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -791,7 +791,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             else Z.pp_print fmt sv.value;
             F.pp_print_string fmt " (by intlit))")
     | Bool b ->
-        let b = if b then "true" else "false" in
+        let b =
+          match !backend with
+          | HOL4 -> if b then "T" else "F"
+          | Coq | FStar | Lean -> if b then "true" else "false"
+        in
         F.pp_print_string fmt b
     | Char c -> (
         match !backend with
@@ -2262,14 +2266,15 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
        *   let* x = y in // monadic
        *   ...
        * ]}
+       * TODO: cleanup
        * *)
-      if monadic && !backend = Coq then (
+      if monadic && (!backend = Coq || !backend = HOL4) then (
         let ctx = extract_typed_pattern ctx fmt true lv in
         F.pp_print_space fmt ();
         let arrow =
           match !backend with
-          | Coq -> "<-"
-          | FStar | Lean | HOL4 -> raise (Failure "impossible")
+          | Coq | HOL4 -> "<-"
+          | FStar | Lean -> raise (Failure "impossible")
         in
         F.pp_print_string fmt arrow;
         F.pp_print_space fmt ();
@@ -2304,15 +2309,14 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
         extract_texpression ctx fmt false re;
-        (* End the monadic let-binding *)
+        (* End the let-binding *)
         (match !backend with
         | Lean ->
-            (* In Lean, monadic let-bindings don't require to end with anything *)
+            (* In Lean, (monadic) let-bindings don't require to end with anything *)
             ()
-        | Coq | FStar ->
+        | Coq | FStar | HOL4 ->
             F.pp_print_space fmt ();
-            F.pp_print_string fmt "in"
-        | HOL4 -> F.pp_print_string fmt ";");
+            F.pp_print_string fmt "in");
         ctx)
     in
     (* Close the box for the let-binding *)