Theory IICF_Array_List
theory IICF_Array_List
imports "../Intf/IICF_List" "../../../ds/LLVM_DS_Array_List"
begin
abbreviation (input) "raw_al_assn ≡ ↿arl_assn"
definition "al_assn R ≡ hr_comp raw_al_assn (⟨the_pure R⟩list_rel)"
abbreviation "al_assn' TYPE('l::len2) R ≡ al_assn R :: (_ ⇒ (_,'l)array_list ⇒ _)"
lemma arl_assn_free[sepref_frame_free_rules]: "MK_FREE (↿arl_assn) arl_free"
apply rule by vcg
lemma al_assn_free[sepref_frame_free_rules]: "MK_FREE (al_assn R) arl_free"
unfolding al_assn_def by (rule sepref_frame_free_rules)+
lemma al_assn_boundD[sepref_bounds_dest]:
"rdomp (al_assn' TYPE('l::len2) A) xs ⟹ length xs < max_snat LENGTH('l)"
unfolding al_assn_def arl_assn_def arl_assn'_def
apply (simp add: rdomp_hrcomp_conv sep_algebra_simps split: prod.splits)
by (auto
simp: rdomp_def snat.assn_def sep_algebra_simps pred_lift_extract_simps
list_rel_imp_same_length[symmetric]
)
lemma rdomp_al_dest':
"rdomp (al_assn' TYPE('l::len2) A) xs ⟹ is_pure A ⟹ length xs < max_snat LENGTH('l) ∧ (∀i<length xs. rdomp A (xs!i))"
unfolding al_assn_def arl_assn_def arl_assn'_def
apply (simp add: rdomp_hrcomp_conv sep_algebra_simps split: prod.splits)
apply (auto
simp: rdomp_def snat.assn_def sep_algebra_simps pred_lift_extract_simps
list_rel_imp_same_length[symmetric]
)
by (auto 0 3 simp: list_rel_def list_all2_conv_all_nth is_pure_conv pure_app_eq pred_lift_extract_simps)
text ‹This functions deletes all elements of a resizable array, without resizing it.›
sepref_decl_op emptied_list: "λ_::'a list. []::'a list" :: "⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op al_custom_replicate: op_list_replicate :: "nat_rel → A → ⟨A⟩list_rel" .
lemma al_fold_custom_replicate:
"replicate = op_al_custom_replicate"
"op_list_replicate = op_al_custom_replicate"
"mop_list_replicate = mop_al_custom_replicate"
by (auto simp: fun_eq_iff)
context
fixes l_dummy :: "'l::len2 itself"
and L AA
defines [simp]: "L ≡ (LENGTH ('l))"
defines [simp]: "AA ≡ raw_al_assn :: _ ⇒ (_,'l) array_list ⇒ _"
begin
private lemma n_unf: "hr_comp AA (⟨the_pure A⟩list_rel) = al_assn A" unfolding al_assn_def AA_def ..
private lemma params:
"(max_snat, max_snat) ∈ Id → Id"
"(L,L)∈nat_rel"
by auto
context
notes [fcomp_norm_unfold] = n_unf
notes [param] = params
notes [simp] = refine_pw_simps
begin
thm bool1_rel_def bool.assn_is_rel[symmetric]
private method m_ref =
((unfold snat_rel_def snat.assn_is_rel[symmetric] bool1_rel_def bool.assn_is_rel[symmetric])?,
sepref_to_hoare, vcg_monadify,
vcg')
lemma al_empty_hnr_aux:
"(uncurry0 (arl_new_raw::(_,'l::len2)array_list llM), uncurry0 (RETURN op_list_empty))
∈ [λ_. 4 < L]⇩a unit_assn⇧k → AA"
by m_ref
sepref_decl_impl (no_register) al_empty: al_empty_hnr_aux .
lemma al_replicate_hnr_aux:
"(uncurry arl_new_repl, uncurry (RETURN oo op_al_custom_replicate))
∈ [λ_. 4 < L]⇩a (snat_assn' TYPE('l))⇧k *⇩a id_assn⇧k → AA"
by m_ref
sepref_decl_impl al_replicate: al_replicate_hnr_aux .
lemma al_nth_hnr_aux: "(uncurry arl_nth, uncurry mop_list_get)
∈ AA⇧k *⇩a snat_assn⇧k →⇩a id_assn"
by m_ref
sepref_decl_impl (ismop) al_nth: al_nth_hnr_aux .
lemma al_upd_hnr_aux: "(uncurry2 arl_upd, uncurry2 mop_list_set)
∈ AA⇧d *⇩a snat_assn⇧k *⇩a id_assn⇧k →⇩a AA"
by m_ref
sepref_decl_impl (ismop) al_upd: al_upd_hnr_aux .
lemma al_append_hnr_aux: "(uncurry arl_push_back, uncurry mop_list_append)
∈ [λ(xs,_). length xs + 1 < max_snat L]⇩a AA⇧d *⇩a id_assn⇧k → AA"
by m_ref
sepref_decl_impl (ismop) al_append: al_append_hnr_aux .
lemma al_take_hnr_aux: "(uncurry arl_take, uncurry mop_list_take)
∈ snat_assn⇧k *⇩a AA⇧d →⇩a AA"
by m_ref
sepref_decl_impl (ismop) al_take: al_take_hnr_aux .
lemma al_pop_last_hnr_aux: "(arl_pop_back, mop_list_pop_last)
∈ AA⇧d →⇩a id_assn ×⇩a AA"
by m_ref
sepref_decl_impl (ismop) al_pop_last: al_pop_last_hnr_aux .
lemma al_butlast_hnr_aux: "(arl_butlast, mop_list_butlast) ∈ AA⇧d →⇩a AA"
by m_ref
sepref_decl_impl (ismop) al_butlast: al_butlast_hnr_aux .
lemma al_last_hnr_aux: "(arl_last, mop_list_last) ∈ AA⇧k →⇩a id_assn"
by m_ref
sepref_decl_impl (ismop) al_last: al_last_hnr_aux .
lemma al_len_hnr_aux: "(arl_len, mop_list_length) ∈ AA⇧k →⇩a snat_assn"
by m_ref
sepref_decl_impl (ismop) al_len: al_len_hnr_aux .
lemma al_is_empty_hnr_aux:
"(λal. doM { l←arl_len al; ll_icmp_eq l (signed_nat 0) }, mop_list_is_empty) ∈ AA⇧k →⇩a bool1_assn"
by m_ref
sepref_decl_impl (ismop) al_is_empty: al_is_empty_hnr_aux .
lemma al_emptied_hnr_aux: "(arl_clear,mop_emptied_list)∈AA⇧d→⇩aAA"
by m_ref
sepref_decl_impl (ismop) al_emptied_hnr_aux .
end
end
definition [simp]: "op_al_empty TYPE('l::len2) ≡ op_list_empty"
sepref_register "op_al_empty TYPE('l::len2)"
lemma al_custom_empty_hnr[sepref_fr_rules]:
"(uncurry0 arl_new_raw, uncurry0 (RETURN (PR_CONST (op_al_empty TYPE('l::len2)))))
∈ [λ_. 4<LENGTH('l)]⇩a unit_assn⇧k → al_assn' TYPE('l) A"
apply simp
apply (rule al_empty_hnr[simplified])
done
lemma al_fold_custom_empty:
"[] = op_al_empty TYPE('l::len2)"
"op_list_empty = op_al_empty TYPE('l::len2)"
"mop_list_empty = RETURN (op_al_empty TYPE('l::len2))"
by auto
subsection ‹Ad-Hoc Regression Tests›
experiment
begin
sepref_definition example [llvm_code] is "λn. do {
let l = op_list_empty;
l ← mop_list_append l 42;
l ← mop_emptied_list l;
l ← mop_list_append l 43;
l ← mop_list_append l 44;
l ← mop_list_append l 45;
l ← mop_list_append l 46;
let x = l!2;
let l = l[2:=l!3];
l ← mop_list_set l 3 x;
let (_,l) = op_list_pop_last l;
l2 ← mop_list_replicate 100 False;
l2 ← mop_list_append l2 True;
l2 ← mop_list_append l2 True;
l2 ← mop_list_append l2 False;
l2 ← mop_list_set l2 3 True;
RETURN l
}" :: "(snat_assn' TYPE(32))⇧k →⇩a al_assn' TYPE(32) (snat_assn' TYPE(32))"
apply (annot_snat_const "TYPE(32)")
apply (rewrite al_fold_custom_empty[where 'l=32])
apply (rewrite al_fold_custom_replicate)
by sepref
export_llvm example
end
end