diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/evalLib.sml | 73 |
1 files changed, 50 insertions, 23 deletions
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 |