Theory Partially_Filled_Array

theory Partially_Filled_Array
  imports
    "Refine_Imperative_HOL.IICF_Array_List"
    Array_SBlit
begin

section "Partially Filled Arrays"

text ‹An array that is only partially filled.
The number of actual elements contained is kept in a second element.
This represents a weakened version of the array\_list from IICF.›

type_synonym 'a pfarray = "'a array_list"


subsection "Operations on Partly Filled Arrays"


definition is_pfa where
  "is_pfa c l ≡ λ(a,n). ∃⇩A l'. a ↦⇩a l' *  ↑(c = length l' ∧ n ≤ c ∧ l = (take n l'))"

abbreviation "len :: 'a pfarray ⇒ nat ≡ snd"
abbreviation "arr :: 'a pfarray ⇒ 'a array ≡ fst"

lemma is_pfa_prec[safe_constraint_rules]: "precise (is_pfa c)"
  unfolding is_pfa_def[abs_def]
  apply(rule preciseI)
  apply(simp split: prod.splits) 
  using preciseD snga_prec by fastforce

definition pfa_init where
  "pfa_init cap v n ≡ do {
  a ← Array.new cap v;
  return (a,n)
}"

lemma pfa_init_rule[sep_heap_rules]: "n ≤ N ⟹ < emp > pfa_init N x n <is_pfa N (replicate n x)>"
  by (sep_auto simp: pfa_init_def is_pfa_def)

definition pfa_empty where
  "pfa_empty cap ≡ pfa_init cap default 0"



lemma pfa_empty_rule[sep_heap_rules]: "< emp > pfa_empty N <is_pfa N []>"
  by (sep_auto simp: pfa_empty_def is_pfa_def)


definition "pfa_length ≡ arl_length"

lemma pfa_length_rule[sep_heap_rules]: "
  <is_pfa c l a> 
    pfa_length a
  <λr. is_pfa c l a * ↑(r=length l)>"
  by (sep_auto simp: pfa_length_def arl_length_def is_pfa_def)


definition "pfa_capacity ≡ λ(a,n). Array.len a
"


lemma pfa_capacity_rule[sep_heap_rules]: "
  <is_pfa c l a> 
    pfa_capacity a
  <λr. is_pfa c l a * ↑(c=r)>"
  by (sep_auto simp: pfa_capacity_def arl_length_def is_pfa_def)



definition "pfa_is_empty ≡ arl_is_empty"

lemma pfa_is_empty_rule[sep_heap_rules]: "
  <is_pfa c l a> 
    pfa_is_empty a
  <λr. is_pfa c l a * ↑(r⟷(l=[]))>"
  by (sep_auto simp: pfa_is_empty_def arl_is_empty_def is_pfa_def)



definition "pfa_append ≡ λ(a,n) x. do {
  Array.upd n x a;
  return (a,n+1)
}"


lemma pfa_append_rule[sep_heap_rules]:
   "len a < c  ⟹
    <is_pfa c l a> 
      pfa_append a x 
    <λ(a',n'). is_pfa c (l@[x]) (a',n') * ↑(a' = arr a ∧ n' = (len a)+1) >"  
  by (sep_auto
      simp: pfa_append_def arl_append_def is_pfa_def take_update_last neq_Nil_conv
      split: prod.splits nat.split)


definition "pfa_last ≡ arl_last"


lemma pfa_last_rule[sep_heap_rules]: "
  l≠[] ⟹
  <is_pfa c l a> 
    pfa_last a
  <λr. is_pfa c l a * ↑(r=last l)>"
  by (sep_auto simp: pfa_last_def arl_last_def is_pfa_def last_take_nth_conv)


definition pfa_butlast :: "'a::heap pfarray ⇒ 'a pfarray Heap" where
  "pfa_butlast ≡ λ(a,n).
    return (a,n-1)
  "


lemma pfa_butlast_rule[sep_heap_rules]: "
  <is_pfa c l a> 
    pfa_butlast a
  <λ(a',n'). is_pfa c (butlast l) (a',n') * ↑(a' = arr a)>"
  by (sep_auto 
      split: prod.splits
      simp: pfa_butlast_def is_pfa_def butlast_take)  


definition "pfa_get ≡ arl_get"

lemma pfa_get_rule[sep_heap_rules]: "
  i < length l ⟹
  < is_pfa c l a> 
    pfa_get a i
  <λr. is_pfa c l a * ↑((l!i) = r)>"
  by (sep_auto simp: is_pfa_def pfa_get_def arl_get_def  split: prod.split)


definition "pfa_set ≡ arl_set"

lemma pfa_set_rule[sep_heap_rules]: "
    i<length l ⟹
    <is_pfa c l a> 
      pfa_set a i x
    <λa'. is_pfa c (l[i:=x]) a' * ↑(a' = a)>"
  by (sep_auto simp: pfa_set_def arl_set_def is_pfa_def split: prod.split)





definition pfa_shrink :: "nat ⇒ 'a::heap pfarray ⇒ 'a pfarray Heap" where
  "pfa_shrink k ≡ λ(a,n).
  return (a,k)
"


lemma pfa_shrink_rule[sep_heap_rules]: "
   k ≤ length xs ⟹
    < is_pfa c xs a > 
      pfa_shrink k a
    <λ(a',n'). is_pfa c (take k xs) (a',n') * ↑(n' = k ∧ a'=arr a) >"  
  by (sep_auto 
      simp: pfa_shrink_def is_pfa_def min.absorb1
      split: prod.splits nat.split)


definition pfa_shrink_cap :: "nat ⇒ 'a::heap pfarray ⇒ 'a pfarray Heap" where
  "pfa_shrink_cap k ≡ λ(a,n). do {
  a' ← array_shrink a k;
  return (a',min k n)
}
"

lemma pfa_shrink_cap_rule_preserve[sep_heap_rules]: "
   ⟦len a ≤ k; k ≤ c⟧ ⟹
    < is_pfa c l a > 
      pfa_shrink_cap k a
    <λa'. is_pfa k l a' >⇩t"
  by (sep_auto 
      simp: pfa_shrink_cap_def is_pfa_def min.absorb1 min.absorb2
      split: prod.splits nat.split)



lemma pfa_shrink_cap_rule: "
   ⟦k ≤ c⟧ ⟹
    < is_pfa c l a > 
      pfa_shrink_cap k a
    <λa'. is_pfa k (take k l) a' >⇩t"  
  by (sep_auto 
      simp: pfa_shrink_cap_def is_pfa_def min.absorb1 min.absorb2
      split: prod.splits nat.split dest: mod_starD)


definition "array_ensure a s x ≡ do {
    l←Array.len a;
    if l≥s then 
      return a
    else do {
      a'←Array.new s x;
      blit a 0 a' 0 l;
      return a'
    }
  }"

lemma array_ensure_rule[sep_heap_rules]:
  shows "
      < a↦⇩ala > 
        array_ensure a s x 
      <λa'. a'↦⇩a (la @ replicate (s-length la) x)>⇩t"
  unfolding array_ensure_def
  by sep_auto

(* Ensure a certain capacity *)
definition pfa_ensure :: "'a::{heap,default} pfarray ⇒ nat ⇒ 'a pfarray Heap" where
  "pfa_ensure ≡ λ(a,n) k. do {
  a' ← array_ensure a k default;
  return (a',n)
}
"

lemma pfa_ensure_rule[sep_heap_rules]: "
    < is_pfa c l a > 
      pfa_ensure a k
    <λ(a',n'). is_pfa (max c k) l (a',n') * ↑(n' = len a ∧ c ≥ len a)>⇩t"  
  by (sep_auto 
      simp: pfa_ensure_def is_pfa_def split!: prod.splits)


definition "pfa_copy ≡ arl_copy"


lemma pfa_copy_rule[sep_heap_rules]:
  "< is_pfa c l a >
   pfa_copy a
   <λr. is_pfa c l a * is_pfa c l r>⇩t"  
  by (sep_auto simp: pfa_copy_def arl_copy_def is_pfa_def)

definition pfa_blit :: "'a::heap pfarray ⇒ nat ⇒ 'a::heap pfarray ⇒ nat ⇒ nat ⇒ unit Heap" where
  "pfa_blit ≡ λ(src,sn) si (dst,dn) di l. blit src si dst di l"


lemma min_nat: "min a (a+b) = (a::nat)"
  by auto


lemma pfa_blit_rule[sep_heap_rules]:
  assumes LEN: "si+l ≤ sn" "di ≤ dn" "di+l ≤ dc"
  shows
    "< is_pfa sc src (srci,sn)
      * is_pfa dc dst (dsti,dn) >
    pfa_blit (srci,sn) si (dsti,dn) di l
    <λ_. is_pfa sc src (srci,sn)
      * is_pfa dc (take di dst @ take l (drop si src) @ drop (di+l) dst) (dsti,max (di+l) dn)
    >"
  using LEN apply(sep_auto simp add: min_nat is_pfa_def pfa_blit_def min.commute min.absorb1 heap: blit_rule)
   apply (simp add: min.absorb1 take_drop)
  apply (simp add: drop_take max_def)
  done

definition pfa_drop :: "('a::heap) pfarray ⇒ nat ⇒ 'a pfarray ⇒ 'a pfarray Heap" where
  "pfa_drop ≡ λ(src,sn) si (dst,dn). do {
   blit src si dst 0 (sn-si);
   return (dst,(sn-si))
}
"


lemma pfa_drop_rule_pair[sep_heap_rules]:
  assumes LEN: "k ≤ sn" "(sn-k) ≤ dc"
  shows
    "< is_pfa sc src (srci,sn)
      * is_pfa dc dst (dsti,dn) >
    pfa_drop (srci,sn) k (dsti,dn)
    <λ(dsti',dn'). is_pfa sc src (srci,sn)
      * is_pfa dc (drop k src) (dsti',dn')
      * ↑(dsti' = dsti)
    >"
  using LEN apply (sep_auto simp add: drop_take is_pfa_def pfa_drop_def dest!: mod_starD heap: pfa_blit_rule)
  done

lemma pfa_drop_rule[sep_heap_rules]:
  assumes LEN: "k ≤ len srci" "(len srci-k) ≤ dc"
  shows
    "< is_pfa sc src srci
      * is_pfa dc dst dsti >
    pfa_drop srci k dsti
    <λ(dsti',dn'). is_pfa sc src srci
      * is_pfa dc (drop k src) (dsti',dn')
      * ↑(dsti' = arr dsti)
    >"
  using LEN apply (sep_auto simp add: drop_take is_pfa_def pfa_drop_def dest!: mod_starD heap: pfa_blit_rule split!: prod.splits)
  done


definition "pfa_append_grow ≡ λ(a,n) x. do {
  l ← pfa_capacity (a,n);
  a' ← if l = n 
  then array_grow a (l+1) x
  else Array.upd n x a;
  return (a',n+1)
}"



lemma pfa_append_grow_full_rule[sep_heap_rules]: "n = c ⟹
     <is_pfa c l (a,n)>
  array_grow a (c+1) x
      <λa'. is_pfa (c+1) (l@[x]) (a',n+1)>⇩t"
  apply(sep_auto simp add: is_pfa_def 
      heap del: array_grow_rule)
  apply(vcg heap del: array_grow_rule heap add: array_grow_rule[of l "(Suc (length l))" a x])
   apply simp
  apply(rule ent_ex_postI[where ?x="l@[x]"])
  apply sep_auto
  done


lemma pfa_append_grow_less_rule: "n < c ⟹
 <is_pfa c l (a,n)>
    Array.upd n x a
<λa'. is_pfa c (l@[x]) (a',n+1)>⇩t"
  apply(sep_auto simp add: is_pfa_def take_update_last)
  done

lemma pfa_append_grow_rule[sep_heap_rules]: "
  <is_pfa c l (a,n)>
  pfa_append_grow (a,n) x 
  <λ(a',n'). is_pfa (if c = n then c+1 else c) (l@[x]) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
  apply(subst pfa_append_grow_def)
  apply(rule hoare_triple_preI)
  apply (sep_auto
      heap add: pfa_append_grow_full_rule pfa_append_grow_less_rule)
   apply(sep_auto simp add: is_pfa_def)
  apply(sep_auto simp add: is_pfa_def)
  done

(* This definition has only one access to the array length *)
definition "pfa_append_grow' ≡ λ(a,n) x. do {
  a' ← pfa_ensure (a,n) (n+1);
  a'' ← pfa_append a' x;
  return a''
}"

lemma pfa_append_grow'_rule[sep_heap_rules]: "
  <is_pfa c l (a,n)>
  pfa_append_grow' (a,n) x 
  <λ(a',n'). is_pfa (max (n+1) c) (l@[x]) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
  unfolding pfa_append_grow'_def
  by (sep_auto simp add: max_def)


definition "pfa_insert ≡ λ(a,n) i x. do {
  a' ← array_shr a i 1;
  a'' ← Array.upd i x a;
  return (a'',n+1)
}"


lemma list_update_last: "length ls = Suc i ⟹ ls[i:=x] = (take i ls)@[x]"
  by (metis append_eq_conv_conj length_Suc_rev_conv list_update_length)

lemma pfa_insert_rule[sep_heap_rules]:
  "⟦i ≤ n; n < c⟧ ⟹
  <is_pfa c l (a,n)>
  pfa_insert (a,n) i x 
  <λ(a',n'). is_pfa c (take i l@x#drop i l) (a',n') * ↑(n' = n+1 ∧ a=a')>"
  unfolding pfa_insert_def is_pfa_def 
  by (sep_auto simp add: list_update_append1 list_update_last
      Suc_diff_le drop_take min_def)

definition pfa_insert_grow ::  "'a::{heap,default} pfarray ⇒ nat ⇒ 'a ⇒ 'a pfarray Heap" 
  where "pfa_insert_grow ≡ λ(a,n) i x. do {
  a' ← pfa_ensure (a,n) (n+1);
  a'' ← pfa_insert a' i x;
  return a''
}"

lemma pfa_insert_grow_rule[sep_heap_rules]: 
  "i ≤ n ⟹
  <is_pfa c l (a,n)>
  pfa_insert_grow (a,n) i x 
  <λ(a',n'). is_pfa (max c (n+1)) (take i l@x#drop i l) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
  unfolding pfa_insert_grow_def  
  by (sep_auto heap add: pfa_insert_rule[of i n "max c (Suc n)"])


definition pfa_extend where
  "pfa_extend ≡ λ (a,n) (b,m). do{
  blit b 0 a n m;
  return (a,n+m)
}"

lemma pfa_extend_rule[sep_heap_rules]: 
  "n+m ≤ c ⟹
  <is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
  pfa_extend (a,n) (b,m) 
  <λ(a',n'). is_pfa c (l1@l2) (a',n') * ↑(a' = a ∧ n'=n+m) * is_pfa d l2 (b,m)>⇩t"
  unfolding pfa_extend_def  
  by (sep_auto simp add: is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)


definition pfa_extend_grow where
  "pfa_extend_grow ≡ λ (a,n) (b,m). do{
  a' ← array_ensure a (n+m) default;
  blit b 0 a' n m;
  return (a',n+m)
}"

lemma pfa_extend_grow_rule[sep_heap_rules]: 
  "<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
  pfa_extend_grow (a,n) (b,m) 
  <λ(a',n'). is_pfa (max c (n+m)) (l1@l2) (a',n') * ↑(n'=n+m ∧ c ≥ n) * is_pfa d l2 (b,m)>⇩t"
  unfolding pfa_extend_grow_def  
  by (sep_auto simp add: is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)

definition pfa_append_extend_grow where
  "pfa_append_extend_grow ≡ λ (a,n) x (b,m). do{
  a' ← array_ensure a (n+m+1) default;
  a'' ← Array.upd n x a';
  blit b 0 a'' (n+1) m;
  return (a'',n+m+1)
}"

lemma pfa_append_extend_grow_rule[sep_heap_rules]: 
  "<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
  pfa_append_extend_grow (a,n) x (b,m) 
  <λ(a',n'). is_pfa (max c (n+m+1)) (l1@x#l2) (a',n') * ↑(n'=n+m+1 ∧ c ≥ n) * is_pfa d l2 (b,m)>⇩t"
  unfolding pfa_append_extend_grow_def  
  by (sep_auto simp add: list_update_last is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)


definition "pfa_delete ≡ λ(a,n) i. do {
  array_shl a (i+1) 1;
  return (a,n-1)
}"

lemma pfa_delete_rule[sep_heap_rules]:
  "i < n ⟹
  <is_pfa c l (a,n)>
  pfa_delete (a,n) i
  <λ(a',n'). is_pfa c (take i l@drop (i+1) l) (a',n') * ↑(n' = n-1 ∧ a=a')>"
  unfolding pfa_delete_def is_pfa_def 
  apply (sep_auto simp add: drop_take min_def)
  by (metis Suc_diff_Suc diff_zero dual_order.strict_trans2 le_less_Suc_eq zero_le)



end