diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/hol4/evalLib.sig | 8 | ||||
| -rw-r--r-- | backends/hol4/evalLib.sml | 142 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 217 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 4 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 15 | ||||
| -rw-r--r-- | backends/hol4/saveThmsLib.sig | 7 | ||||
| -rw-r--r-- | backends/hol4/saveThmsLib.sml | 64 | ||||
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 14 |
8 files changed, 285 insertions, 186 deletions
diff --git a/backends/hol4/evalLib.sig b/backends/hol4/evalLib.sig index f44cff13..40183af8 100644 --- a/backends/hol4/evalLib.sig +++ b/backends/hol4/evalLib.sig @@ -8,6 +8,14 @@ sig include Abbrev + (* The following functions allow to *persistently* register custom rewriting theorems. + + Remark: it is important that we allow to save rewriting theorems without forcing + the user to save them in, say, srw_ss. + *) + val add_rewrite_thm : thm -> unit + val add_rewrite_thms : 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 85a6b94a..f9e758c9 100644 --- a/backends/hol4/evalLib.sml +++ b/backends/hol4/evalLib.sml @@ -27,61 +27,113 @@ fun get_const_name (tm : term) : const_name = (thy, name) end -(* Create the persistent collection, which is a pair: +(* Create the persistent collection of rewrite theorems - TODO: more efficient + collection than a list? *) +val (add_rewrite_thm, get_rewrite_thms) = + let + (* Small helper *) + fun add_to_state (th : thm) s = th :: s + + (* 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 "evalLib" "apply_delta" ("Unexpected REMOVE") + + (* Initialize the collection *) + val init_state = [] + val {update_global_value, (* Local update *) + record_delta, (* Global update *) + get_global_value = get_rewrite_thms, + ...} = + ThmSetData.export_with_ancestry { + settype = "evalLib_rewrite_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_rewrite_thm (s : string) : unit = + let + 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 + in + (add_rewrite_thm, get_rewrite_thms) + end + +fun add_rewrite_thms (ls : string list) : unit = + app add_rewrite_thm ls + + +(* Create the persistent collection of unfolding theorems, which is a pair: (set of constants, map from constant name to theorem) *) -type state = term Redblackset.set * (const_name, thm) Redblackmap.dict +type unfold_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 -(* Small helper *) -fun add_to_state (th : thm) (s, m) = +val (add_unfold_thm, get_unfold_thms_map) = let - 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 + (* Small helper *) + fun add_to_state (th : thm) (s, m) = + let + 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 -(* 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 th = saveThmsLib.lookup_thm s + (* 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 "evalLib" "apply_delta" ("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 = get_unfold_thms_map, + ...} = + ThmSetData.export_with_ancestry { + settype = "evalLib_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 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 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)) + (add_unfold_thm, get_unfold_thms_map) end fun add_unfold_thms (ls : string list) : unit = app add_unfold_thm ls fun get_unfold_thms () : thm list = - map snd (Redblackmap.listItems (snd (get_global_value ()))) + map snd (Redblackmap.listItems (snd (get_unfold_thms_map ()))) (* Apply a custom unfolding to the term, if possible. @@ -90,7 +142,7 @@ 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 ()) + val custom_unfolds = snd (get_unfold_thms_map ()) (* Remove all the matches to find the top-most scrutinee *) val scrut = strip_all_cases_get_scrutinee tm @@ -148,7 +200,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 (fst (get_global_value ())) + val restr_tms = Redblackset.listItems (fst (get_unfold_thms_map ())) (* We do the following: - use the standard EVAL conv, but restrains it from unfolding terms for which we have custom unfolding theorems @@ -156,7 +208,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 ()) [] x handle UNCHANGED => REFL x) + val simp_no_fail_conv = (fn x => SIMP_CONV (srw_ss ()) (get_rewrite_thms ()) 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/primitivesLib.sml b/backends/hol4/primitivesLib.sml index 776843bf..5339dec9 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -183,34 +183,6 @@ val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_with_dep_int_lemmas -(* The registered spec theorems, that {!progress} will automatically apply. - - The keys are the function names (it is a pair, because constant names - are made of the theory name and the name of the constant itself). - - Also note that we can store several specs per definition (in practice, when - looking up specs, we will try them all one by one, in a LIFO order). - - We store theorems where all the premises are in the goal, with implications - (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). - - We do this because, when doing proofs by induction, {!progress} might have to - handle *unregistered* theorems coming the current goal assumptions and of the shape - (the conclusion of the theorem is an assumption, and we want to ignore this assumption): - {[ - [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ...] - ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ... - ]} - *) -val reg_spec_thms: (const_name, thm) Redblackmap.dict ref = - ref (Redblackmap.mkDict const_name_compare) - (* Retrieve the specified application in a spec theorem. A spec theorem for a function [f] typically has the shape: @@ -249,11 +221,33 @@ fun get_spec_app (t : term) : term = else (fst o dest_eq) t; in t end -(* Register a spec theorem in the spec database. +(* Create the persistent collection of spec theorems, that {!progress} will automatically apply. - For the shape of spec theorems, see {!get_spec_thm_app}. + The keys are the function names (it is a pair, because constant names + are made of the theory name and the name of the constant itself). + + Also note that we can store several specs per definition (in practice, when + looking up specs, we will try them all one by one, in a LIFO order). + + We store theorems where all the premises are in the goal, with implications + (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). + + We do this because, when doing proofs by induction, {!progress} might have to + handle *unregistered* theorems coming from the current goal assumptions and of the shape + (the conclusion of the theorem is also present as an assumption, and we want to ignore + this assumption): + {[ + [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ...] + ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ... + ]} *) -fun register_spec_thm (th: thm) : unit = +fun get_key_normalize_thm (th : thm) : const_name * thm = let (* Transform the theroem a bit before storing it *) val th = SPEC_ALL th; @@ -262,95 +256,110 @@ fun register_spec_thm (th: thm) : unit = (* Retrieve the function name *) val cn = get_fun_name_from_app f; in - (* Store *) - reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th) + (* Return *) + (cn, th) end +val { save_thm = save_spec_thm, + delete_thm = delete_spec_thm, + temp_save_thm = temp_save_spec_thm, + temp_delete_thm = temp_delete_spec_thm, + get_map = get_spec_thms, ... } = + saveThmsLib.create_map { + compare = const_name_compare, + get_key_normalize_thm = get_key_normalize_thm + } "spec_theorems" + +val save_spec_thms = app save_spec_thm + val all_add_eqs = [ - isize_add_eq, - i8_add_eq, - i16_add_eq, - i32_add_eq, - i64_add_eq, - i128_add_eq, - usize_add_eq, - u8_add_eq, - u16_add_eq, - u32_add_eq, - u64_add_eq, - u128_add_eq + "primitives.isize_add_eq", + "primitives.i8_add_eq", + "primitives.i16_add_eq", + "primitives.i32_add_eq", + "primitives.i64_add_eq", + "primitives.i128_add_eq", + "primitives.usize_add_eq", + "primitives.u8_add_eq", + "primitives.u16_add_eq", + "primitives.u32_add_eq", + "primitives.u64_add_eq", + "primitives.u128_add_eq" ] -val _ = app register_spec_thm all_add_eqs +val _ = save_spec_thms all_add_eqs val all_sub_eqs = [ - isize_sub_eq, - i8_sub_eq, - i16_sub_eq, - i32_sub_eq, - i64_sub_eq, - i128_sub_eq, - usize_sub_eq, - u8_sub_eq, - u16_sub_eq, - u32_sub_eq, - u64_sub_eq, - u128_sub_eq + "primitives.isize_sub_eq", + "primitives.i8_sub_eq", + "primitives.i16_sub_eq", + "primitives.i32_sub_eq", + "primitives.i64_sub_eq", + "primitives.i128_sub_eq", + "primitives.usize_sub_eq", + "primitives.u8_sub_eq", + "primitives.u16_sub_eq", + "primitives.u32_sub_eq", + "primitives.u64_sub_eq", + "primitives.u128_sub_eq" ] -val _ = app register_spec_thm all_sub_eqs +val _ = save_spec_thms all_sub_eqs val all_mul_eqs = [ - isize_mul_eq, - i8_mul_eq, - i16_mul_eq, - i32_mul_eq, - i64_mul_eq, - i128_mul_eq, - usize_mul_eq, - u8_mul_eq, - u16_mul_eq, - u32_mul_eq, - u64_mul_eq, - u128_mul_eq + "primitives.isize_mul_eq", + "primitives.i8_mul_eq", + "primitives.i16_mul_eq", + "primitives.i32_mul_eq", + "primitives.i64_mul_eq", + "primitives.i128_mul_eq", + "primitives.usize_mul_eq", + "primitives.u8_mul_eq", + "primitives.u16_mul_eq", + "primitives.u32_mul_eq", + "primitives.u64_mul_eq", + "primitives.u128_mul_eq" ] -val _ = app register_spec_thm all_mul_eqs +val _ = save_spec_thms all_mul_eqs val all_div_eqs = [ - isize_div_eq, - i8_div_eq, - i16_div_eq, - i32_div_eq, - i64_div_eq, - i128_div_eq, - usize_div_eq, - u8_div_eq, - u16_div_eq, - u32_div_eq, - u64_div_eq, - u128_div_eq + "primitives.isize_div_eq", + "primitives.i8_div_eq", + "primitives.i16_div_eq", + "primitives.i32_div_eq", + "primitives.i64_div_eq", + "primitives.i128_div_eq", + "primitives.usize_div_eq", + "primitives.u8_div_eq", + "primitives.u16_div_eq", + "primitives.u32_div_eq", + "primitives.u64_div_eq", + "primitives.u128_div_eq" ] -val _ = app register_spec_thm all_div_eqs +val _ = save_spec_thms all_div_eqs val all_rem_eqs = [ - isize_rem_eq, - i8_rem_eq, - i16_rem_eq, - i32_rem_eq, - i64_rem_eq, - i128_rem_eq, - usize_rem_eq, - u8_rem_eq, - u16_rem_eq, - u32_rem_eq, - u64_rem_eq, - u128_rem_eq + "primitives.isize_rem_eq", + "primitives.i8_rem_eq", + "primitives.i16_rem_eq", + "primitives.i32_rem_eq", + "primitives.i64_rem_eq", + "primitives.i128_rem_eq", + "primitives.usize_rem_eq", + "primitives.u8_rem_eq", + "primitives.u16_rem_eq", + "primitives.u32_rem_eq", + "primitives.u64_rem_eq", + "primitives.u128_rem_eq" ] -val _ = app register_spec_thm all_rem_eqs - -val all_vec_lems = [ - vec_len_spec, - vec_insert_back_spec +val _ = save_spec_thms all_rem_eqs + +val _ = save_spec_thms [ + "primitives.vec_index_fwd_spec", + "primitives.vec_index_back_spec", + "primitives.vec_index_mut_fwd_spec", + "primitives.vec_index_mut_back_spec", + "primitives.vec_insert_back_spec", + "primitives.vec_push_back_spec" ] -val _ = app register_spec_thm all_vec_lems (* Provided the goal contains a call to a monadic function, return this function call. @@ -499,7 +508,7 @@ val progress : tactic = val asms_thl = mapfilter asm_to_spec asms; (* Lookup a spec in the database *) val thl = - case Redblackmap.peek (!reg_spec_thms, fname) of + case Redblackmap.peek (get_spec_thms (), fname) of NONE => asms_thl | SOME spec => spec :: asms_thl; val _ = diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 8cd54f33..7920454b 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1624,8 +1624,8 @@ Proof prove_scalar_eq_equiv_tac QED -(* Remark.: don't move this up, it will break some proofs *) -val _ = BasicProvers.export_rewrites [ + +val _ = evalLib.add_rewrite_thms [ "isize_eq_equiv", "i8_eq_equiv", "i16_eq_equiv", diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 2407e2f2..e4051212 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -2388,24 +2388,20 @@ sig [vec_len_spec] Theorem - [oracles: DISK_THM] - [axioms: int_to_usize_usize_to_int, usize_bounds, - vec_to_list_num_bounds] [] + [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] [] ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max [vec_len_vec_new] Theorem - [oracles: DISK_THM] - [axioms: mk_vec_axiom, int_to_usize_usize_to_int, - usize_to_int_int_to_usize, usize_bounds] [] + [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] [] ⊢ vec_len vec_new = int_to_usize 0 [vec_push_back_spec] Theorem [oracles: DISK_THM] - [axioms: usize_to_int_int_to_usize, mk_vec_axiom, - int_to_usize_usize_to_int, usize_bounds, vec_to_list_num_bounds] [] + [axioms: usize_to_int_int_to_usize, mk_vec_axiom, usize_bounds, + vec_to_list_num_bounds] [] ⊢ ∀v x. usize_to_int (vec_len v) < usize_max ⇒ ∃nv. @@ -2438,8 +2434,7 @@ sig [oracles: DISK_THM] [axioms: vec_to_list_num_bounds, usize_bounds, - int_to_usize_usize_to_int, usize_to_int_bounds, - usize_to_int_int_to_usize, mk_vec_axiom] [] + usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] [] ⊢ ∀v i x. usize_to_int i < usize_to_int (vec_len v) ⇒ (let diff --git a/backends/hol4/saveThmsLib.sig b/backends/hol4/saveThmsLib.sig index 9cbac1c7..bbdc080b 100644 --- a/backends/hol4/saveThmsLib.sig +++ b/backends/hol4/saveThmsLib.sig @@ -25,15 +25,20 @@ sig (* The user-provided functions *) type 'key key_fns = { compare : 'key * 'key -> order, - get_key_from_thm : thm -> 'key + (* Retrieve the key from the theorem and normalize it at the same time *) + get_key_normalize_thm : thm -> ('key * thm) } (* The functions we return to the user to manipulate the map *) type 'key map_fns = { (* Persistently save a theorem *) save_thm : string -> unit, + (* Persistently delete a theorem *) + delete_thm : string -> unit, (* Temporarily save a theorem *) temp_save_thm : thm -> unit, + (* Temporarily delete a theorem *) + temp_delete_thm : thm -> unit, (* Get the key set *) get_keys : unit -> 'key Redblackset.set, (* Get the theorems map *) diff --git a/backends/hol4/saveThmsLib.sml b/backends/hol4/saveThmsLib.sml index 76b428cf..e7b20055 100644 --- a/backends/hol4/saveThmsLib.sml +++ b/backends/hol4/saveThmsLib.sml @@ -8,32 +8,35 @@ type thname = KernelSig.kernelname (* The user-provided functions *) type 'key key_fns = { compare : 'key * 'key -> order, - get_key_from_thm : thm -> 'key + get_key_normalize_thm : thm -> ('key * thm) } (* The functions we return to the user to manipulate the map *) type 'key map_fns = { (* Persistently save a theorem *) save_thm : string -> unit, + (* Persistently delete a theorem *) + delete_thm : string -> unit, (* Temporarily save a theorem *) temp_save_thm : thm -> unit, + (* Temporarily delete a theorem *) + temp_delete_thm : thm -> unit, (* Get the key set *) get_keys : unit -> 'key Redblackset.set, (* Get the theorems map *) get_map : unit -> ('key, thm) Redblackmap.dict } -(* This function is adapted from ThmSetData.sml. +(* This function is adapted from ThmSetData.sml *) +fun get_Kname (s : string) : thname = + case String.fields (equal #".") s of + [s0] => {Thy = current_theory(), Name = s} + | [s1,s2] => {Thy = s1, Name = s2} + | _ => raise mk_HOL_ERR "saveThmsLib" "get_Kname" ("Malformed name: " ^ 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) + val name = get_Kname s fun lookup_exn {Thy,Name} = DB.fetch Thy Name in (name, lookup_exn name) @@ -45,24 +48,40 @@ type 'key state = 'key Redblackset.set * ('key, thm) Redblackmap.dict (* Initialize a persistent map *) fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns = let - val { compare, get_key_from_thm } = kf + val { compare, get_key_normalize_thm } = kf (* Small helper *) - fun add_to_state (th : thm) (s, m) = + fun add_to_state (th : thm) (s, m) : 'key state = let - val k = get_key_from_thm th + val (k, th) = get_key_normalize_thm th val s = Redblackset.add (s, k) val m = Redblackmap.insert (m, k, th) in (s, m) end + + (* Small helper *) + fun remove_from_state (th : thm) ((s, m) : 'key state) : 'key state = + let + val (k, _) = get_key_normalize_thm th + (* For deletion: we have to test whether the element/key is there or not, + because otherwise the functions raise the exception NotFound *) + val s = if Redblackset.member (s, k) then Redblackset.delete (s, k) else s + val m = if Option.isSome (Redblackmap.peek (m, k)) then fst (Redblackmap.remove (m, k)) else m + 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") + | ThmSetData.REMOVE th_name => + let + val (_, th) = lookup_thm th_name + in + remove_from_state th st + end (* Initialize the dictionary *) val init_state = (Redblackset.empty compare, Redblackmap.mkDict compare) @@ -85,6 +104,10 @@ fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns = fun temp_save_thm (th : thm) : unit = update_global_value (add_to_state th) + (* Temporarily delete theorem *) + fun temp_delete_thm (th : thm) : unit = + update_global_value (remove_from_state th) + (* Persistently save a theorem *) fun save_thm (s : string) : unit = let @@ -96,11 +119,22 @@ fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns = temp_save_thm (snd th) end + (* Persistently delete a theorem *) + fun delete_thm (s : string) : unit = + let + val (_, th) = lookup_thm s + in + (* Similar to [save_thm] *) + record_delta (ThmSetData.REMOVE s); + temp_delete_thm 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, + { save_thm = save_thm, delete_thm = delete_thm, + temp_save_thm = temp_save_thm, temp_delete_thm = temp_delete_thm, get_keys = get_keys, get_map = get_map } end diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml index 79026376..c3f04cca 100644 --- a/backends/hol4/testHashmapScript.sml +++ b/backends/hol4/testHashmapScript.sml @@ -51,7 +51,7 @@ Proof progress >> progress QED -val _ = register_spec_thm nth_mut_fwd_spec +val _ = save_spec_thm "nth_mut_fwd_spec" val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”) val insert_def = new_axiom ("insert_def", “ @@ -177,9 +177,7 @@ Proof Cases_on ‘q' = k’ >> rw [] >- (fs [list_t_v_def, index_eq]) >> Cases_on ‘insert k v ls0’ >> fs [] >> - (* TODO: would be good to have a tactic which inverts equalities of the - shape ‘ListCons (q',r) a = ls1’ *) - sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >> + gvs [list_t_v_def, index_eq] >> first_x_assum (qspec_assume ‘0’) >> fs [len_def] >> strip_tac >> @@ -193,7 +191,7 @@ Proof fs [list_t_v_def, index_eq, len_def] >> first_x_assum (qspec_assume ‘i’) >> rfs []) >> Cases_on ‘insert k v ls0’ >> fs [] >> - sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >> + gvs [list_t_v_def, index_eq] >> last_x_assum (qspec_assume ‘i - 1’) >> fs [len_def] >> sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >> @@ -250,13 +248,11 @@ Proof last_x_assum (qspecl_assume [‘i’, ‘j’]) >> rfs [list_t_v_def, len_def] >> sg ‘0 < j’ >- int_tac >> - Cases_on ‘i = 0’ >> fs [index_eq] >> - sg ‘0 < i’ >- int_tac >> fs []) >> + Cases_on ‘i = 0’ >> gvs [index_eq]) >> (* k ≠ q: recursion *) Cases_on ‘insert k v ls0’ >> fs [bind_def] >> last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >> - rfs [] >> - sg ‘ls1 = ListCons (q,r) a’ >- fs [] >> fs [list_t_v_def] >> + gvs [list_t_v_def] >> imp_res_tac distinct_keys_tail >> fs [] >> irule distinct_keys_cons >> rw [] >> metis_tac [distinct_keys_insert_index_neq] |