Theory Dynamic_Array

section ‹Arrays with Dynamic Resizing›
theory Dynamic_Array
imports "Refine_Imperative_HOL.IICF_List" "Separation_Logic_Imperative_HOL.Array_Blit" "Refine_Imperative_HOL.IICF_Array" "Refine_Imperative_HOL.IICF_Map"
begin

(* TODO: Move to Array_Blit *)
definition "array_grow' a n x ≡ do {
  l←Array.len a;
  a'←Array.new (l+n) x;
  blit a 0 a' 0 l;
  return a'
}"

lemma array_grow'_rule[sep_heap_rules]:
  shows "
    < a↦⇩ala > 
      array_grow' a n x 
    <λa'. a'↦⇩a (la @ replicate n x)>⇩t"
  unfolding array_grow'_def
  by sep_auto

(* TODO: Move to IICF_List *)
sepref_decl_op list_grow: 
  "λxs n x. xs@replicate n x" :: "⟨A⟩list_rel → nat_rel → A → ⟨A⟩list_rel" .


definition "nff_α dflt l i ≡ if i<length l then l!i else dflt"
definition "is_nff dflt f a ≡ ∃⇩Al. a ↦⇩a l * ↑(f = nff_α dflt l)"

definition [code_unfold]: "dyn_array_new_sz dflt n ≡ Array.new n dflt"

lemma dyn_array_new_sz_rl[sep_heap_rules]: 
  "<emp> dyn_array_new_sz dflt n <λr. is_nff dflt (λ_. dflt) r>"
  unfolding dyn_array_new_sz_def is_nff_def nff_α_def
  by sep_auto

definition "array_get_dyn dflt a i ≡ do {
  ⌦‹‹nth_oo dflt a i››
  l ← Array.len a;
  if i<l then Array.nth a i else return dflt
  }"

lemma array_get_dyn_rule[sep_heap_rules]: "
  < is_nff dflt f a > 
    array_get_dyn dflt a i 
  < λr. is_nff dflt f a * ↑(r = f i) >"
  unfolding array_get_dyn_def nth_oo_def
  by (sep_auto simp: nff_α_def is_nff_def)

definition "array_set_dyn dflt a i v ≡ do {
  l ← Array.len a;
  if i<l then 
    Array.upd i v a 
  else do {
    let ns = max (2*l) (i+1);
    a ← array_grow a ns dflt;
    Array.upd i v a
  }
}"

lemma nff_α_upd: "⟦i < length l⟧ ⟹ nff_α dflt (l[i := v]) = (nff_α dflt l)(i := v)"
  by (auto simp: nff_α_def)

lemma nff_α_append_default: "nff_α dflt (l@replicate n dflt) = nff_α dflt l"
  by (auto simp: nff_α_def nth_append intro!: ext)

lemma array_set_dyn_rule[sep_heap_rules]: "
  < is_nff dflt f a >
    array_set_dyn dflt a i v
  <λr. is_nff dflt (f(i:=v)) r >⇩t  
  "
  unfolding array_set_dyn_def is_nff_def upd_oo_def
  by (sep_auto simp: nff_α_upd nff_α_append_default)

end