Theory IICF_MS_Array_List
theory IICF_MS_Array_List
imports
"../Intf/IICF_List" IICF_Array
begin
definition "ms_irel M N ≡ br (λ(l,xs). take l xs) (λ(l,xs). l≤N ∧ N = length xs ∧ N<M)"
definition "ms_empty N ≡ RETURN (0::nat,replicate N init)"
definition "ms_is_empty ≡ λ(l,_). RETURN (l=0)"
definition "ms_length ≡ λ(l,_). RETURN l"
definition "ms_push_back ≡ λ(l,xs) x. doN {ASSERT (l < length xs); RETURN (l+1,xs[l:=x])}"
definition "ms_last ≡ λ(l,xs). doN {ASSERT (0<l ∧ l≤length xs); RETURN (xs!(l-1))}"
definition "ms_butlast ≡ λ(l,xs). doN {ASSERT (l>0); RETURN (l-1,xs)}"
definition "ms_get ≡ λ(l,xs) i. doN {ASSERT (i<length xs); RETURN (xs!i)}"
definition "ms_set ≡ λ(l,xs) i x. doN {ASSERT (i<length xs); RETURN (l,xs[i:=x])}"
context begin
private method ms_prove_refine =
(unfold ms_irel_def curry0_def;
intro nres_relI fun_relI frefI;
simp?;
refine_vcg?;
(auto simp: in_br_conv)
)
lemma ms_empty_correct: "N<M ⟹ (ms_empty N,mop_list_empty) ∈ ⟨ms_irel M N⟩nres_rel"
unfolding ms_empty_def by ms_prove_refine
lemma ms_is_empty_correct: "(ms_is_empty,mop_list_is_empty) ∈ ms_irel M N → ⟨bool_rel⟩nres_rel"
unfolding ms_is_empty_def by ms_prove_refine
lemma ms_length_correct: "(ms_length,mop_list_length) ∈ ms_irel M N → ⟨nat_rel⟩nres_rel"
unfolding ms_length_def by ms_prove_refine
lemma ms_push_back_correct: "(uncurry ms_push_back,uncurry mop_list_append)
∈ [λ(xs,x). length xs < N]⇩f (ms_irel M N ×⇩r Id) → ⟨ms_irel M N⟩nres_rel"
unfolding ms_push_back_def
supply [simp] = take_update_last
by ms_prove_refine
lemma ms_last_correct: "(ms_last,mop_list_last)∈ms_irel M N → ⟨Id⟩nres_rel"
unfolding ms_last_def supply [simp] = last_take_nth_conv by ms_prove_refine
lemma ms_butlast_correct: "(ms_butlast,mop_list_butlast)∈ms_irel M N → ⟨ms_irel M N⟩nres_rel"
unfolding ms_butlast_def supply [simp] = butlast_take by ms_prove_refine
lemma ms_get_correct: "(ms_get,mop_list_get)∈ms_irel M N → nat_rel → ⟨Id⟩nres_rel"
unfolding ms_get_def by ms_prove_refine
lemma ms_set_correct: "(ms_set,mop_list_set)∈ms_irel M N → nat_rel → Id → ⟨ms_irel M N⟩nres_rel"
unfolding ms_set_def by ms_prove_refine
end
type_synonym ('l,'a) marl = "'l word × 'a ptr"
lemma ms_irel_prenorm:
assumes "((l,xs),xs')∈ms_irel M N"
shows "length xs = N ∧ l=length xs' ∧ length xs'≤N ∧ N < M"
using assms
unfolding ms_irel_def
by (auto simp: in_br_conv)
context
fixes M :: nat
defines "M ≡ max_snat (LENGTH ('l::len2))"
notes [fcomp_prenorm_simps] = ms_irel_prenorm[where M=M]
begin
abbreviation "marl2_assn ≡ snat_assn' TYPE('l) ×⇩a array_assn id_assn"
sepref_definition marl_empty_impl [llvm_inline] is "ms_empty" :: "(snat_assn' TYPE('l))⇧k →⇩a marl2_assn"
unfolding ms_empty_def
supply [sepref_import_param] = IdI[of init]
apply (annot_snat_const "TYPE('l)")
apply (rewrite array_fold_custom_replicate)
by sepref
definition [simp]: "marl_empty_aux (N::nat) ≡ op_list_empty"
sepref_decl_op marl_empty: marl_empty_aux :: "nat_rel → ⟨A⟩list_rel" .
lemma ms_empty_correct': "(ms_empty,RETURN o op_marl_empty)
∈ [λN. N<M]⇩f⇩d nat_rel → (λN. ⟨ms_irel M N⟩nres_rel)"
apply (rule frefI) using ms_empty_correct by auto
definition "marl_assn' TYPE('l) A N ≡ hrr_comp nat_rel
(λN. hr_comp marl2_assn (ms_irel M N))
(λ_. ⟨the_pure A⟩list_rel) N"
lemmas [fcomp_norm_unfold] = marl_assn'_def[symmetric, abs_def]
lemma marl_assn'_fold''[fcomp_norm_unfold]:
"hrr_comp nat_rel (λx. hr_comp (snat_assn ×⇩a array_assn id_assn) (ms_irel M x)) (λx. ⟨the_pure A⟩list_rel)
= (λN. marl_assn' TYPE('l) A N)"
unfolding marl_assn'_def
by auto
lemma marl_assn'_fold'[fcomp_norm_unfold]:
"hr_comp (hr_comp (snat_assn ×⇩a array_assn id_assn) (ms_irel M N)) (⟨the_pure A⟩list_rel)
= marl_assn' TYPE('l) A N"
unfolding marl_assn'_def
unfolding hrr_comp_def
apply (auto simp: fun_eq_iff sep_algebra_simps)
unfolding non_dep_def by metis+
sepref_decl_impl marl_empty: marl_empty_impl.refine[FCOMP ms_empty_correct'] by simp
sepref_definition marl_is_empty_impl [llvm_inline] is ms_is_empty :: "marl2_assn⇧k →⇩a bool1_assn"
unfolding ms_is_empty_def
apply (annot_snat_const "TYPE('l)")
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_is_empty_impl.refine[FCOMP ms_is_empty_correct[of M]] .
sepref_definition marl_length_impl [llvm_inline] is ms_length :: "marl2_assn⇧k →⇩a snat_assn' TYPE('l)"
unfolding ms_length_def
by sepref
sepref_decl_impl (ismop) marl_length_impl.refine[FCOMP ms_length_correct[of M]] .
sepref_definition marl_push_back_impl [llvm_code] is
"uncurry ms_push_back" :: "[λ((l,a),_). length a < M ]⇩a marl2_assn⇧d*⇩aid_assn⇧k → marl2_assn"
unfolding ms_push_back_def M_def
apply (annot_snat_const "TYPE('l)")
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_push_back_impl.refine[FCOMP ms_push_back_correct[where M=M]]
by (parametricity add: IdI[of N])
sepref_definition marl_last_impl [llvm_code] is
"ms_last" :: "marl2_assn⇧k →⇩a id_assn"
unfolding ms_last_def M_def
apply (annot_snat_const "TYPE('l)")
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_last_impl.refine[FCOMP ms_last_correct[where M=M]] .
sepref_definition marl_butlast_impl [llvm_code] is
"ms_butlast" :: "marl2_assn⇧d →⇩a marl2_assn"
unfolding ms_butlast_def M_def
apply (annot_snat_const "TYPE('l)")
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_butlast_impl.refine[FCOMP ms_butlast_correct[where M=M]] .
sepref_definition marl_get_impl [llvm_inline] is
"uncurry ms_get" :: "marl2_assn⇧k *⇩a (snat_assn' TYPE('l))⇧k →⇩a id_assn"
unfolding ms_get_def M_def
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_get_impl.refine[FCOMP ms_get_correct[where M=M]] .
sepref_definition marl_set_impl [llvm_inline] is
"uncurry2 ms_set" :: "marl2_assn⇧d *⇩a (snat_assn' TYPE('l))⇧k *⇩a id_assn⇧k →⇩a marl2_assn"
unfolding ms_set_def M_def
apply sepref_dbg_keep
done
sepref_decl_impl (ismop) marl_set_impl.refine[FCOMP ms_set_correct[where M=M]] .
end
lemma fold_marl_empty:
"[] = op_marl_empty N"
"RETURN [] = mop_marl_empty N"
"op_list_empty = op_marl_empty N"
"mop_list_empty = mop_marl_empty N"
by auto
schematic_goal [sepref_frame_free_rules]: "MK_FREE (marl_assn' TYPE('l::len2) A N) ?f"
unfolding marl_assn'_fold'[symmetric]
by sepref_dbg_side
lemma marl_assn'_boundsD[sepref_bounds_dest]:
"rdomp (marl_assn' TYPE('l::len2) A N) xs ⟹ length xs ≤ N ∧ N < max_snat LENGTH('l)"
unfolding marl_assn'_def
supply [sepref_bounds_dest] = ms_irel_prenorm
by sepref_bounds
lemma bind_assoc_tagged: "bind$(bind$m$f)$g = bind$m$(λ⇩2x. bind$(f$x)$g)"
unfolding autoref_tag_defs by simp
experiment begin
sepref_definition test is "λN. (do {
let x = op_marl_empty N;
RETURN (x@[1::nat])
})" :: "[λN. N≥10]⇩a (snat_assn' TYPE(64))⇧k →⇩d (λN. marl_assn' TYPE(64) (snat_assn' TYPE(64)) N)"
apply (annot_snat_const "TYPE(64)")
by sepref
end
end