summaryrefslogtreecommitdiff
path: root/backends/hol4/testHashmapScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/testHashmapScript.sml')
-rw-r--r--backends/hol4/testHashmapScript.sml550
1 files changed, 2 insertions, 548 deletions
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 71b0109d..249bc0bf 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -2,556 +2,10 @@ open HolKernel boolLib bossLib Parse
open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
val _ = new_theory "testHashmap"
-val primitives_theory_name = "primitives"
-
-(* Small utility: compute the set of assumptions in the context.
-
- We isolate this code in a utility in order to be able to improve it:
- for now we simply put all the assumptions in a set, but in the future
- we might want to split the assumptions which are conjunctions in order
- to be more precise.
- *)
-fun compute_asms_set ((asms,g) : goal) : term Redblackset.set =
- Redblackset.fromList Term.compare asms
-
-val integer_bounds_defs_list = [
- i8_min_def,
- i8_max_def,
- i16_min_def,
- i16_max_def,
- i32_min_def,
- i32_max_def,
- i64_min_def,
- i64_max_def,
- i128_min_def,
- i128_max_def,
- u8_max_def,
- u16_max_def,
- u32_max_def,
- u64_max_def,
- u128_max_def
-]
-
-val integer_bounds_lemmas =
- Redblackmap.fromList String.compare
- [
- ("isize", isize_to_int_bounds),
- ("i8", i8_to_int_bounds),
- ("i16", i16_to_int_bounds),
- ("i32", i32_to_int_bounds),
- ("i64", i64_to_int_bounds),
- ("i128", i128_to_int_bounds),
- ("usize", usize_to_int_bounds),
- ("u8", u8_to_int_bounds),
- ("u16", u16_to_int_bounds),
- ("u32", u32_to_int_bounds),
- ("u64", u64_to_int_bounds),
- ("u128", u128_to_int_bounds)
- ]
-
-val integer_types_names =
- Redblackset.fromList String.compare
- (map fst (Redblackmap.listItems integer_bounds_lemmas))
-
-(* See {!assume_bounds_for_all_int_vars}.
-
- This tactic is in charge of adding assumptions for one variable.
- *)
-fun assume_bounds_for_int_var
- (asms_set: term Redblackset.set) (var : string) (ty : string) :
- tactic =
- let
- (* Lookup the lemma to apply *)
- val lemma = Redblackmap.find (integer_bounds_lemmas, ty);
- (* Instantiate the lemma *)
- val ty_t = mk_type (ty, []);
- val var_t = mk_var (var, ty_t);
- val lemma = SPEC var_t lemma;
- (* Split the theorem into a list of conjuncts.
-
- The bounds are typically a conjunction:
- {[
- ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm
- ]}
- *)
- val lemmas = CONJUNCTS lemma;
- (* Filter the conjuncts: some of them might already be in the context,
- we don't want to introduce them again, as it would pollute it.
- *)
- val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas;
- in
- (* Introduce the assumptions in the context *)
- assume_tacl lemmas
- end
-
-(* Introduce bound assumptions for all the machine integers in the context.
-
- Exemple:
- ========
- If there is “x : u32” in the input set, then we introduce:
- {[
- 0 <= u32_to_int x
- u32_to_int x <= u32_max
- ]}
- *)
-fun assume_bounds_for_all_int_vars (asms, g) =
- let
- (* Compute the set of integer variables in the context *)
- val vars = free_varsl (g :: asms);
- (* Compute the set of assumptions already present in the context *)
- val asms_set = compute_asms_set (asms, g);
- val vartys_set = ref (Redblackset.empty String.compare);
- (* Filter the variables to keep only the ones with type machine integer,
- decompose the types at the same time *)
- fun decompose_var (v : term) : (string * string) =
- let
- val (v, ty) = dest_var v;
- val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty;
- val _ = assert null args;
- val _ = assert (fn thy => thy = primitives_theory_name) thy;
- val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty;
- val _ = vartys_set := Redblackset.add (!vartys_set, ty);
- in (v, ty) end;
- val vars = mapfilter decompose_var vars;
- (* Add assumptions for one variable *)
- fun add_var_asm (v, ty) : tactic =
- assume_bounds_for_int_var asms_set v ty;
- (* Add the bounds for isize, usize *)
- val size_bounds =
- append
- (if Redblackset.member (!vartys_set, "usize") then CONJUNCTS usize_bounds else [])
- (if Redblackset.member (!vartys_set, "isize") then CONJUNCTS isize_bounds else []);
- val size_bounds =
- filter (fn th => not (Redblackset.member (asms_set, concl th))) size_bounds;
- in
- ((* Add assumptions for all the variables *)
- map_every_tac add_var_asm vars >>
- (* Add assumptions about the size bounds *)
- assume_tacl size_bounds) (asms, g)
- end
-
-val integer_conversion_lemmas_list = [
- isize_to_int_int_to_isize,
- i8_to_int_int_to_i8,
- i16_to_int_int_to_i16,
- i32_to_int_int_to_i32,
- i64_to_int_int_to_i64,
- i128_to_int_int_to_i128,
- usize_to_int_int_to_usize,
- u8_to_int_int_to_u8,
- u16_to_int_int_to_u16,
- u32_to_int_int_to_u32,
- u64_to_int_int_to_u64,
- u128_to_int_int_to_u128
-]
-
-(* Look for conversions from integers to machine integers and back.
- {[
- u32_to_int (int_to_u32 x)
- ]}
-
- Attempts to prove and apply equalities of the form:
- {[
- u32_to_int (int_to_u32 x) = x
- ]}
- *)
-val rewrite_with_dep_int_lemmas : tactic =
- (* We're not trying to be smart: we just try to rewrite with each theorem at
- a time *)
- let
- val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> cooper_tac;
- val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th]);
- val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1;
- val then_tac2 = (fn th => full_simp_tac simpLib.empty_ss [th]);
- val rewr_tac2 = apply_dep_rewrites_match_first_premise_with_all_tac (fn _ => true) prove_premise then_tac2;
- in
- map_every_tac rewr_tac1 integer_conversion_lemmas_list >>
- map_every_tac rewr_tac2 []
- end
-
-(* Massage a bit the goal, for instance by introducing integer bounds in the
- assumptions.
-*)
-val massage : tactic =
- assume_bounds_for_all_int_vars >>
- rewrite_with_dep_int_lemmas
-
-(* Lexicographic order over pairs *)
-fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
- ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
- let
- val (x1, y1) = p1;
- val (x2, y2) = p2;
- in
- case comp1 (x1, x2) of
- LESS => LESS
- | GREATER => GREATER
- | EQUAL => comp2 (y1, y2)
- end
-
-(* A constant name (theory, constant name) *)
-type const_name = string * string
-
-val const_name_compare = pair_compare String.compare String.compare
-
-(* 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:
- {[
- !x0 ... xn.
- H0 ==> ... Hm ==>
- (exists ...
- (exists ... . f y0 ... yp = ... /\ ...) \/
- (exists ... . f y0 ... yp = ... /\ ...) \/
- ...
- ]}
-
- Or:
- {[
- !x0 ... xn.
- H0 ==> ... Hm ==>
- case f y0 ... yp of
- ... => ...
- | ... => ...
- ]}
-
- We return: [f y0 ... yp]
-*)
-fun get_spec_app (t : term) : term =
- let
- (* Remove the universally quantified variables, the premises and
- the existentially quantified variables *)
- val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t;
- (* Remove the exists, take the first disjunct *)
- val t = (hd o strip_disj o snd o strip_exists) t;
- (* Split the conjunctions and take the first conjunct *)
- val t = (hd o strip_conj) t;
- (* Remove the case if there is, otherwise destruct the equality *)
- val t =
- if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end
- else (fst o dest_eq) t;
- in t end
-
-(* Given a function call [f y0 ... yn] return the name of the function *)
-fun get_fun_name_from_app (t : term) : const_name =
- let
- val f = (fst o strip_comb) t;
- val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
- val cn = (thy, name);
- in cn end
-
-(* Register a spec theorem in the spec database.
-
- For the shape of spec theorems, see {!get_spec_thm_app}.
- *)
-fun register_spec_thm (th: thm) : unit =
- let
- (* Transform the theroem a bit before storing it *)
- val th = SPEC_ALL th;
- (* Retrieve the app ([f x0 ... xn]) *)
- val f = get_spec_app (concl th);
- (* Retrieve the function name *)
- val cn = get_fun_name_from_app f;
- in
- (* Store *)
- reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th)
- end
-
-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
-]
-val _ = app register_spec_thm 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
-]
-val _ = app register_spec_thm 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
-]
-val _ = app register_spec_thm 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
-]
-val _ = app register_spec_thm 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
-]
-val _ = app register_spec_thm all_rem_eqs
-
-val all_vec_lems = [
- vec_len_spec,
- vec_insert_back_spec
-]
-val _ = app register_spec_thm all_vec_lems
-
-(* Repeatedly destruct cases and return the last scrutinee we get *)
-fun strip_all_cases_get_scrutinee (t : term) : term =
- if TypeBase.is_case t
- then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t
- else t
-
-(*
-TypeBase.dest_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
-TypeBase.strip_case “3”
-TypeBase.dest_case “3”
-
-strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
-strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
-strip_all_cases_get_scrutinee “3”
-*)
-
-
-(* Provided the goal contains a call to a monadic function, return this function call.
-
- The goal should be of the shape:
- 1.
- {[
- case (* potentially expanded function body *) of
- ... => ...
- | ... => ...
- ]}
-
- 2. Or:
- {[
- exists ... .
- ... (* potentially expanded function body *) = Return ... /\
- ... (* Various properties *)
- ]}
-
- 3. Or a disjunction of cases like the one above, below existential binders
- (actually: note sure this last case exists in practice):
- {[
- exists ... .
- (exists ... . (* body *) = Return ... /\ ...) \/
- ...
- ]}
-
- The function body should be of the shape:
- {[
- x <- f y0 ... yn;
- ...
- ]}
-
- Or (typically if we expanded the monadic binds):
- {[
- case f y0 ... yn of
- ...
- ]}
-
- Or simply (typically if we reached the end of the function we're analyzing):
- {[
- f y0 ... yn
- ]}
-
- For all the above cases we would return [f y0 ... yn].
- *)
-fun get_monadic_app_call (t : term) : term =
- (* We do something slightly imprecise but hopefully general and robut *)
- let
- (* Case 3.: strip the existential binders, and take the first disjuntion *)
- val t = (hd o strip_disj o snd o strip_exists) t;
- (* Case 2.: strip the existential binders, and take the first conjunction *)
- val t = (hd o strip_conj o snd o strip_exists) t;
- (* If it is an equality, take the lhs *)
- val t = if is_eq t then lhs t else t;
- (* Expand the binders to transform them to cases *)
- val t =
- (rhs o concl) (REWRITE_CONV [bind_def] t)
- handle UNCHANGED => t;
- (* Strip all the cases *)
- val t = strip_all_cases_get_scrutinee t;
- in t end
-
-(* Use the given theorem to progress by one step (we use this when
- analyzing a function body: this goes forward by one call to a monadic function).
-
- We transform the goal by:
- - pushing the theorem premises to a subgoal
- - adding the theorem conclusion in the assumptions in another goal, and
- getting rid of the monadic call
-
- Then [then_tac] receives as paramter the monadic call on which we applied
- the lemma. This can be useful, for instance, to make a case disjunction.
-
- This function is the most primitive of the [progress...] functions.
- *)
-fun pure_progress_with (premise_tac : tactic)
- (then_tac : term -> thm_tactic) (th : thm) : tactic =
- fn (asms,g) =>
- let
- (* Remove all the universally quantified variables from the theorem *)
- val th = SPEC_ALL th;
- (* Retrieve the monadic call from the goal *)
- val fgoal = get_monadic_app_call g;
- (* Retrieve the app call from the theroem *)
- val gth = get_spec_app (concl th);
- (* Match and instantiate *)
- val (var_s, ty_s) = match_term gth fgoal;
- (* Instantiate the theorem *)
- val th = INST var_s (INST_TYPE ty_s th);
- (* Retrieve the premises of the theorem *)
- val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
- in
- (* Apply the theorem *)
- sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
- end
-
-(*
-val (asms, g) = top_goal ()
-val t = g
-
-val th = U32_SUB_EQ
-
-val premise_tac = massage >> TRY COOPER_TAC
-fun then_tac fgoal =
- fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
- rw [] >> fs [st_ex_bind_def] >> massage >> fs []
-
-pure_progress_with premise_tac then_tac th
-*)
-
-fun progress_with (th : thm) : tactic =
- let
- val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC;
- fun then_tac fgoal thm =
- ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
- rw [] >> fs [bind_def] >> massage >> fs [];
- in
- pure_progress_with premise_tac then_tac th
- end
-
-(*
-progress_with U32_SUB_EQ
-*)
-
-(* This function lookups the theorem to use to make progress *)
-val progress : tactic =
- fn (asms, g) =>
- let
- (* Retrieve the monadic call from the goal *)
- val fgoal = get_monadic_app_call g;
- val fname = get_fun_name_from_app fgoal;
- (* Lookup the theorem: first look in the assumptions (we might want to
- use the inductive hypothesis for instance) *)
- fun asm_to_spec asm =
- let
- (* Fail if there are no universal quantifiers *)
- val _ =
- if is_forall asm then asm
- else assert is_forall ((snd o strip_imp) asm);
- val asm_fname = (get_fun_name_from_app o get_spec_app) asm;
- (* Fail if the name is not the one we're looking for *)
- val _ = assert (fn n => fname = n) asm_fname;
- in
- ASSUME asm
- end
- val asms_thl = mapfilter asm_to_spec asms;
- (* Lookup a spec in the database *)
- val thl =
- case Redblackmap.peek (!reg_spec_thms, fname) of
- NONE => asms_thl
- | SOME spec => spec :: asms_thl;
- val _ =
- if null thl then
- raise (failwith "progress: could not find a suitable theorem to apply")
- else ();
- in
- (* Attempt to use the theorems one by one *)
- map_first_tac progress_with thl (asms, g)
- end
-
(*
* Examples of proofs
*)
@@ -594,7 +48,7 @@ Proof
exfalso >> cooper_tac
QED
-Theorem nth_mut_fwd_lem:
+Theorem nth_mut_fwd_spec:
!(ls : 't list_t) (i : u32).
u32_to_int i < len (list_t_v ls) ==>
case nth_mut_fwd ls i of
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 15:41:30 +0000