Theory Array_of_Array_List
section ‹Array of Array Lists›
theory Array_of_Array_List
imports LLVM_DS_Array_List
begin
subsection ‹Arrays that own their Elements›
definition "idxe_map l i ≡ if i<length l then Some (l!i) else None"
lemma idxe_map_empty[simp]: "idxe_map [] = Map.empty" unfolding idxe_map_def by auto
lemma idxe_map_dom[simp]: "dom (idxe_map l) = {0..<length l}" unfolding idxe_map_def by (auto split: if_splits)
lemma le_idxe_map_updI: "i<length l ⟹ m ⊆⇩m idxe_map l ⟹ m(i↦l!i) ⊆⇩m idxe_map l"
unfolding idxe_map_def map_le_def by (auto split: if_splits)
lemma le_idxe_map_delD: "m ⊆⇩m idxe_map l ⟹ m(i:=None) ⊆⇩m idxe_map (l[i:=x])"
unfolding idxe_map_def map_le_def by (auto split: if_splits)
lemma le_idxe_map_delD': "m ⊆⇩m idxe_map l ⟹ m(i:=None) ⊆⇩m idxe_map l"
unfolding idxe_map_def map_le_def by (auto split: if_splits)
lemma le_idxe_mapD: "m ⊆⇩m idxe_map l ⟹ i<length l ⟹ m i = Some xi ⟹ l!i = xi"
unfolding idxe_map_def map_le_def
apply (clarsimp split: if_splits) by (metis domI option.inject)
definition "nao_assn A R ≡ mk_assn (λxss a. EXS xs.
↿narray_assn xs a
** ↑(length xs = length xss)
** ↑(R ⊆⇩m idxe_map xs)
** (⋃*i∈{0..<length xss} - dom R. ↿A (xss!i) (xs!i))
)"
definition [llvm_inline]: "nao_new TYPE('a::llvm_rep) n ≡ narray_new TYPE('a) n"
lemma nao_repl_init_aux:
assumes [fri_rules]: "□ ⊢ ↿A x init"
shows "□ ⊢ (⋃*i∈{0..<n::nat}. ↿A x init)"
unfolding vcg_tag_defs
apply (induction n)
subgoal by simp
subgoal for n
proof (simp add: atLeast0_lessThan_Suc del: replicate_Suc, goal_cases)
case 1 note [fri_rules] = 1(1)
show ?case by (rule ENTAILSD) vcg
qed
done
lemma nao_new_init_rl:
assumes "□ ⊢ ↿A x init"
shows "llvm_htriple (↿snat.assn n ni) (nao_new TYPE('a::llvm_rep) ni) (λa. ↿(nao_assn A Map.empty) (replicate n x) a)"
unfolding nao_assn_def nao_new_def
supply [fri_rules] = nao_repl_init_aux[OF assms]
by vcg
definition [llvm_code, llvm_inline]: "nao_nth a i ≡ array_nth a i"
lemma nao_nth_aux:
assumes "i<length xs" "i∉R"
shows "sep_set_img ({0..<length xs} - R) P
= (P i ** sep_set_img ({0..<length xs} - insert i R) P)"
proof -
from assms have 1: "{0..<length xs} - R = insert i ({0..<length xs} - insert i R)" by auto
show ?thesis
by (subst 1) auto
qed
lemma ndomIff: "i∉dom m ⟷ m i = None" by auto
lemma nao_nth_rule[vcg_rules]: "llvm_htriple
(↿(nao_assn A R) xs a ** ↿snat.assn i ii ** ↑(i<length xs ∧ i∉dom R))
(nao_nth a ii)
(λxi. ↿(nao_assn A (R(i↦xi))) xs a ** ↿A (xs!i) xi)"
unfolding nao_assn_def nao_nth_def
supply fri_red_img[fri_red_rules]
supply nao_nth_aux[simp]
supply ndomIff[simp] le_idxe_map_updI[simp]
by vcg
definition [llvm_code, llvm_inline]: "nao_upd a i x ≡ array_upd a i x"
lemma nao_upd_aux:
fixes I xs
defines "I ≡ {0..<length xs}"
assumes "i∈I" "i∈R" and [simp]: "length xsi = length xs"
shows "(⋃*j∈I - (R - {i}). ↿A (xs[i := x] ! j) (xsi[i := xi] ! j)) = (↿A x xi ** (⋃*j∈I - R. ↿A (xs ! j) (xsi ! j)))"
proof -
from assms have 1: "I - (R - {i}) = insert i (I-R)" by auto
from assms have [simplified,simp]: "i∉I-R" by auto
have [simp]: "i<length xs" using ‹i∈I› unfolding I_def by auto
have [simp]: "j∈I-R ⟹ i≠j" for j using ‹i∈R› by auto
show ?thesis apply (subst 1) by simp
qed
term restrict_map
lemma nao_upd_rule[vcg_rules]: "llvm_htriple
(↿(nao_assn A R) xs a ** ↿A x xi ** ↿snat.assn i ii ** ↑(i<length xs ∧ i∈dom R))
(nao_upd a ii xi)
(λa'. ↑(a'=a) ** ↿(nao_assn A (R(i:=None))) (xs[i:=x]) a)"
unfolding nao_assn_def nao_upd_def
supply nao_upd_aux[simp] le_idxe_map_delD[simp] domI[simp]
by vcg
definition [llvm_code, llvm_inline]: "nao_rejoin a i ≡ Mreturn ()"
lemma nao_rejoin_aux: "i<length xs ⟹ {0..<length xs} - (dom R - {i}) = insert i ({0..<length xs} - dom R)" by auto
lemma nao_rejoin_rule[vcg_rules]: "llvm_htriple
(↿(nao_assn A R) xs a ** ↿A x xi ** ↑(x=xs!i) ** ↿snat.assn i ii ** ↑(i<length xs ∧ R i = Some xi))
(nao_rejoin a ii)
(λ_. ↿(nao_assn A (R(i:=None))) xs a)"
unfolding nao_rejoin_def nao_assn_def
supply [simp] = le_idxe_map_delD' nao_rejoin_aux domI le_idxe_mapD
by vcg
lemma nao_rejoin_rule': "llvm_htriple
(↿(nao_assn A R) xs a ** ↿snat.assn i ii ** ↿A (xs!i) xi ** ↑(i<length xs ∧ R i = Some xi))
(nao_rejoin a ii)
(λ_. ↿(nao_assn A (R(i:=None))) xs a)"
unfolding nao_rejoin_def nao_assn_def
supply [simp] = le_idxe_map_delD' nao_rejoin_aux domI le_idxe_mapD
by vcg
definition [llvm_inline]: "nao_open a ≡ Mreturn ()"
lemma nao_open_rl[vcg_rules]: "llvm_htriple (↿(nao_assn A R) xss a) (nao_open a) (λ_.
EXS xs.
↿narray_assn xs a
** ↑(length xs = length xss)
** ↑(R ⊆⇩m idxe_map xs)
** (⋃*i∈{0..<length xss} - dom R. ↿A (xss!i) (xs!i))
)"
unfolding nao_open_def nao_assn_def by vcg
definition [llvm_inline]: "nao_free free a len ≡ doM {
llc_while
(λi. ll_icmp_slt i len)
(λi. doM {
x ← nao_nth a i;
free x;
i ← ll_add i (signed_nat 1);
Mreturn i
})
(signed_nat 0);
nao_open a;
narray_free a
}"
definition "iseg_map n f (i::nat) ≡ if i<n then Some (f i) else None"
lemma iseg_mapZ[simp]: "iseg_map 0 f = Map.empty" unfolding iseg_map_def by (intro ext) (auto)
lemma iseg_map_upd_end_eq: "iseg_map n f(n ↦ x) = iseg_map (Suc n) (f(n:=x))"
apply (intro ext)
by (auto simp: iseg_map_def restrict_map_def)
lemma iseg_map_dom[simp]: "dom (iseg_map n f) = {0..<n}"
by (auto simp: iseg_map_def split: if_splits)
lemma nao_free_rl:
assumes [vcg_rules]: "⋀x xi. llvm_htriple (↿A x xi) (free xi) (λ_. □)"
shows "llvm_htriple
(↿(nao_assn A Map.empty) xs a ** ↿snat.assn l li ** ↑(l = length xs))
(nao_free free a li)
(λ_. □)"
unfolding nao_free_def
apply (rewrite annotate_llc_while[where
I="λii t. EXS f i. ↿snat.assn i ii ** ↿(nao_assn A (iseg_map i f)) xs a ** ↑(i≤length xs) ** ↑⇩!(t = length xs - i)"
and R="less_than"]
)
supply [simp] = iseg_map_upd_end_eq
apply vcg_monadify
by vcg
subsection ‹Array of Array Lists›
type_synonym ('ll,'a,'l) array_array_list = "'ll word × ('a,'l) array_list ptr"
definition "aal_assn ≡ mk_assn (λxs (ni,a).
↿snat.assn (length xs) ni ** ↿(nao_assn arl_assn Map.empty) xs a)"
abbreviation "aal_assn' TYPE('ll::len2) TYPE('a::llvm_rep) TYPE('l::len2) ≡ aal_assn :: (_,('ll,'a,'l) array_array_list) dr_assn"
definition [llvm_code,llvm_inline]: "aal_new_raw n ≡ doM {
a←nao_new TYPE(('a::llvm_rep,'l::len2) array_list) n;
Mreturn (n,a)
}"
lemma snat_z_z_init[fri_rules]: "□ ⊢ ↿⇩psnat.assn 0 0"
unfolding snat.assn_def
by (auto simp: snat_invar_def sep_algebra_simps)
lemma narray_assn_null_init[fri_rules]: "□ ⊢ ↿narray_assn [] null"
unfolding narray_assn_def
by (auto simp: sep_algebra_simps)
thm fri_rules
lemma arl_init: "PRECOND (SOLVE_AUTO (4<LENGTH('l)))
⟹ □ ⊢ ↿arl_assn [] (init::('a::llvm_rep,'l::len2) array_list)"
unfolding arl_assn_def arl_assn'_def vcg_tag_defs
apply simp
apply (rule ENTAILSD)
apply vcg
done
lemma aal_new_rl[vcg_rules]: "llvm_htriple
(↿snat.assn n ni ** ↑(4<LENGTH('l::len2)))
(aal_new_raw ni)
(λp. ↿(aal_assn' TYPE('ll::len2) TYPE('a::llvm_rep) TYPE('l::len2)) (replicate n []) p)
"
unfolding aal_assn_def aal_new_raw_def
supply [vcg_rules] = nao_new_init_rl[OF arl_init]
by vcg
definition aal_push_back :: "('l::len2,'a::llvm_rep,'ll::len2) array_array_list ⇒ 'li::len word ⇒ 'a ⇒ ('l,'a,'ll) array_array_list llM"
where [llvm_code, llvm_inline]: "aal_push_back na i x ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
aa ← arl_push_back aa x;
a ← nao_upd a i aa;
Mreturn (n,a)
}"
lemma aal_push_back_rl[vcg_rules]:
fixes a :: "('ll::len2,'a::llvm_rep,'l::len2) array_array_list"
shows "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↑(i<length xss ∧ length (xss!i) + 1 < max_snat LENGTH('l)))
(aal_push_back a ii x)
(λa. ↿aal_assn (xss[i:=(xss!i) @ [x]]) a)
"
unfolding aal_assn_def aal_push_back_def
by vcg
definition [llvm_code, llvm_inline]: "aal_pop_back na i ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
(r,aa) ← arl_pop_back aa;
a ← nao_upd a i aa;
Mreturn (r,(n,a))
}"
lemma aal_pop_back_rl[vcg_rules]:
fixes a :: "('ll::len2,'a::llvm_rep,'l::len2) array_array_list"
shows "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↑(i<length xss ∧ xss!i ≠ []))
(aal_pop_back a ii)
(λ(x,a). ↿aal_assn (xss[i:=butlast (xss!i)]) a ** ↑(x = last (xss!i)))
"
unfolding aal_assn_def aal_pop_back_def
by vcg
definition [llvm_code, llvm_inline]: "aal_idx na i j ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
r ← arl_nth aa j;
nao_rejoin a i;
Mreturn r
}"
lemma aal_idx_rl[vcg_rules]: "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↿snat.assn j jj ** ↑(i<length xss ∧ j<length (xss!i)))
(aal_idx a ii jj)
(λx. ↿aal_assn xss a ** ↑(x = xss!i!j))"
unfolding aal_assn_def aal_idx_def
by vcg
definition [llvm_code, llvm_inline]: "aal_upd na i j x ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
aa ← arl_upd aa j x;
a ← nao_upd a i aa;
Mreturn (n,a)
}"
lemma aal_upd_rl[vcg_rules]:
fixes a :: "('ll::len2,'a::llvm_rep,'l::len2) array_array_list"
shows "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↿snat.assn j jj ** ↑(i<length xss ∧ j < length (xss!i)))
(aal_upd a ii jj x)
(λa. ↿aal_assn (xss[i:=(xss!i)[j:=x]]) a)
"
unfolding aal_assn_def aal_upd_def
by vcg
definition [llvm_code, llvm_inline]: "aal_llen na i ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
r ← arl_len aa;
nao_rejoin a i;
Mreturn r
}"
lemma aal_llen_rl[vcg_rules]: "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↑(i<length xss))
(aal_llen a ii)
(λxi. EXS x. ↿aal_assn xss a **↿snat.assn x xi ** ↑(x = length (xss!i)))"
unfolding aal_assn_def aal_llen_def
by vcg
definition [llvm_code, llvm_inline]: "aal_len na ≡ doM {
let (n,a) = na;
Mreturn n
}"
lemma aal_len_rl[vcg_rules]: "llvm_htriple
(↿aal_assn xss a)
(aal_len a)
(λni. ↿aal_assn xss a ** ↿snat.assn (length xss) ni)"
unfolding aal_len_def aal_assn_def
by vcg
definition [llvm_code, llvm_inline]: "aal_take na i l ≡ doM {
let (n,a) = na;
aa ← nao_nth a i;
aa ← arl_take l aa;
a ← nao_upd a i aa;
Mreturn (n,a)
}"
lemma aal_take_rl[vcg_rules]: "llvm_htriple
(↿aal_assn xss a ** ↿snat.assn i ii ** ↿snat.assn l li ** ↑(i<length xss ∧ l ≤ length (xss!i)))
(aal_take a ii li)
(λa. ↿aal_assn (xss[i := take l (xss!i)]) a)"
unfolding aal_assn_def aal_take_def
by vcg
definition [llvm_code]: "aal_free na ≡ doM {
let (n,a) = na;
nao_free arl_free a n
}"
lemma aal_free_rl[vcg_rules]: "llvm_htriple
(↿aal_assn xss a)
(aal_free a)
(λ_. □)"
unfolding aal_assn_def aal_free_def
supply [vcg_rules] = nao_free_rl[OF arl_free_rule]
by vcg
export_llvm
"aal_new_raw :: 64 word ⇒ (64,8 word,64) array_array_list llM"
"aal_push_back :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ 8 word ⇒ (64,8 word,64) array_array_list llM"
"aal_pop_back :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ (8 word × (64,8 word,64) array_array_list) llM"
"aal_idx :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ 64 word ⇒ 8 word llM"
"aal_upd :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ 64 word ⇒ 8 word ⇒ (64,8 word,64) array_array_list llM"
"aal_llen :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ 64 word llM"
"aal_len :: (64,8 word,64) array_array_list ⇒ 64 word llM"
"aal_free :: (64,8 word,64) array_array_list ⇒ unit llM"
"aal_take :: (64,8 word,64) array_array_list ⇒ 64 word ⇒ 64 word ⇒ ((64,8 word,64) array_array_list) llM"
end