diff options
Diffstat (limited to 'backends/hol4/saveThmsLib.sml')
-rw-r--r-- | backends/hol4/saveThmsLib.sml | 275 |
1 files changed, 93 insertions, 182 deletions
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 |