Theory Refine_Imperative_HOL.IICF_Array_List

theory IICF_Array_List
imports 
  "../Intf/IICF_List" 
  Separation_Logic_Imperative_HOL.Array_Blit
begin

  type_synonym 'a array_list = "'a Heap.array × nat"

  definition "is_array_list l  λ(a,n). Al'. a a l' * (n  length l'  l = take n l'  length l'>0)"

  lemma is_array_list_prec[safe_constraint_rules]: "precise is_array_list"
    unfolding is_array_list_def[abs_def]
    apply(rule preciseI)
    apply(simp split: prod.splits) 
  	using preciseD snga_prec by fastforce

  definition "initial_capacity  16::nat"
  definition "minimum_capacity  16::nat"

  definition "arl_empty  do {
    a  Array.new initial_capacity default;
    return (a,0)
  }"

  definition "arl_empty_sz init_cap  do {
    a  Array.new (max init_cap minimum_capacity) default;
    return (a,0)
  }"

  definition "arl_append  λ(a,n) x. do {
    len  Array.len a;

    if n<len then do {
      a  Array.upd n x a;
      return (a,n+1)
    } else do {
      let newcap = 2 * len;
      a  array_grow a newcap default;
      a  Array.upd n x a;
      return (a,n+1)
    }
  }"

  definition "arl_copy  λ(a,n). do {
    a  array_copy a;
    return (a,n)
  }"

  definition arl_length :: "'a::heap array_list  nat Heap" where
    "arl_length  λ(a,n). return (n)"

  definition arl_is_empty :: "'a::heap array_list  bool Heap" where
    "arl_is_empty  λ(a,n). return (n=0)"

  definition arl_last :: "'a::heap array_list  'a Heap" where
    "arl_last  λ(a,n). do {
      Array.nth a (n - 1)
    }"

  definition arl_butlast :: "'a::heap array_list  'a array_list Heap" where
    "arl_butlast  λ(a,n). do {
      let n = n - 1;
      len  Array.len a;
      if (n*4 < len  n*2minimum_capacity) then do {
        a  array_shrink a (n*2);
        return (a,n)
      } else
        return (a,n)
    }"

  definition arl_get :: "'a::heap array_list  nat  'a Heap" where
    "arl_get  λ(a,n) i. Array.nth a i"

  definition arl_set :: "'a::heap array_list  nat  'a  'a array_list Heap" where
    "arl_set  λ(a,n) i x. do { a  Array.upd i x a; return (a,n)}"


  lemma arl_empty_rule[sep_heap_rules]: "< emp > arl_empty <is_array_list []>"
    by (sep_auto simp: arl_empty_def is_array_list_def initial_capacity_def)

  lemma arl_empty_sz_rule[sep_heap_rules]: "< emp > arl_empty_sz N <is_array_list []>"
    by (sep_auto simp: arl_empty_sz_def is_array_list_def minimum_capacity_def)

  lemma arl_copy_rule[sep_heap_rules]: "< is_array_list l a > arl_copy a <λr. is_array_list l a * is_array_list l r>"  
    by (sep_auto simp: arl_copy_def is_array_list_def)

  lemma arl_append_rule[sep_heap_rules]: "
    < is_array_list l a > 
      arl_append a x 
    <λa. is_array_list (l@[x]) a >t"  
    by (sep_auto 
      simp: arl_append_def is_array_list_def take_update_last neq_Nil_conv
      split: prod.splits nat.split)
    
  lemma arl_length_rule[sep_heap_rules]: "
    <is_array_list l a> 
      arl_length a
    <λr. is_array_list l a * (r=length l)>"
    by (sep_auto simp: arl_length_def is_array_list_def)
    
  lemma arl_is_empty_rule[sep_heap_rules]: "
    <is_array_list l a> 
      arl_is_empty a
    <λr. is_array_list l a * (r(l=[]))>"
    by (sep_auto simp: arl_is_empty_def is_array_list_def)

  lemma arl_last_rule[sep_heap_rules]: "
    l[] 
    <is_array_list l a> 
      arl_last a
    <λr. is_array_list l a * (r=last l)>"
    by (sep_auto simp: arl_last_def is_array_list_def last_take_nth_conv)
    
  lemma arl_butlast_rule[sep_heap_rules]: "
    l[] 
    <is_array_list l a> 
      arl_butlast a
    <is_array_list (butlast l)>t"
  proof -
    assume [simp]: "l[]"
  
    have [simp]: "x. min (x-Suc 0) ((x-Suc 0)*2) = x-Suc 0" by auto

    show ?thesis
      by (sep_auto 
        split: prod.splits
        simp: arl_butlast_def is_array_list_def butlast_take minimum_capacity_def)
  qed  

  lemma arl_get_rule[sep_heap_rules]: "
    i<length l 
    <is_array_list l a> 
      arl_get a i
    <λr. is_array_list l a * (r=l!i)>"
    by (sep_auto simp: arl_get_def is_array_list_def split: prod.split)

  lemma arl_set_rule[sep_heap_rules]: "
    i<length l 
    <is_array_list l a> 
      arl_set a i x
    <is_array_list (l[i:=x])>"
    by (sep_auto simp: arl_set_def is_array_list_def split: prod.split)

  definition "arl_assn A  hr_comp is_array_list (the_pure Alist_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "arl_assn A" for A]


  lemma arl_assn_comp: "is_pure A  hr_comp (arl_assn A) (Blist_rel) = arl_assn (hr_comp A B)"
    unfolding arl_assn_def
    by (auto simp: hr_comp_the_pure hr_comp_assoc list_rel_compp)

  lemma arl_assn_comp': "hr_comp (arl_assn id_assn) (Blist_rel) = arl_assn (pure B)"
    by (simp add: arl_assn_comp)

context 
  notes [fcomp_norm_unfold] = arl_assn_def[symmetric] arl_assn_comp'
  notes [intro!] = hfrefI hn_refineI[THEN hn_refine_preI]
  notes [simp] = pure_def hn_ctxt_def invalid_assn_def
begin  


  lemma arl_empty_hnr_aux: "(uncurry0 arl_empty,uncurry0 (RETURN op_list_empty))  unit_assnk a is_array_list"  
    by sep_auto
  sepref_decl_impl (no_register) arl_empty: arl_empty_hnr_aux .

  lemma arl_empty_sz_hnr_aux: "(uncurry0 (arl_empty_sz N),uncurry0 (RETURN op_list_empty))  unit_assnk a is_array_list"  
    by sep_auto
  sepref_decl_impl (no_register) arl_empty_sz: arl_empty_sz_hnr_aux .

  definition "op_arl_empty  op_list_empty"
  definition "op_arl_empty_sz (N::nat)  op_list_empty"

  lemma arl_copy_hnr_aux: "(arl_copy,RETURN o op_list_copy)  is_array_listk a is_array_list"
    by sep_auto
  sepref_decl_impl arl_copy: arl_copy_hnr_aux .  

  lemma arl_append_hnr_aux: "(uncurry arl_append,uncurry (RETURN oo op_list_append))  (is_array_listd *a id_assnk) a is_array_list"
    by sep_auto
  sepref_decl_impl arl_append: arl_append_hnr_aux .

  lemma arl_length_hnr_aux: "(arl_length,RETURN o op_list_length)  is_array_listk a nat_assn"
    by sep_auto
  sepref_decl_impl arl_length: arl_length_hnr_aux .

  lemma arl_is_empty_hnr_aux: "(arl_is_empty,RETURN o op_list_is_empty)  is_array_listk a bool_assn"
    by sep_auto
  sepref_decl_impl arl_is_empty: arl_is_empty_hnr_aux .  

  lemma arl_last_hnr_aux: "(arl_last,RETURN o op_list_last)  [pre_list_last]a is_array_listk  id_assn"
    by sep_auto
  sepref_decl_impl arl_last: arl_last_hnr_aux . 

  lemma arl_butlast_hnr_aux: "(arl_butlast,RETURN o op_list_butlast)  [pre_list_butlast]a is_array_listd  is_array_list"
    by sep_auto
  sepref_decl_impl arl_butlast: arl_butlast_hnr_aux .

  lemma arl_get_hnr_aux: "(uncurry arl_get,uncurry (RETURN oo op_list_get))  [λ(l,i). i<length l]a (is_array_listk *a nat_assnk)  id_assn"
    by sep_auto
  sepref_decl_impl arl_get: arl_get_hnr_aux .

  lemma arl_set_hnr_aux: "(uncurry2 arl_set,uncurry2 (RETURN ooo op_list_set))  [λ((l,i),_). i<length l]a (is_array_listd *a nat_assnk *a id_assnk)  is_array_list"
    by sep_auto
  sepref_decl_impl arl_set: arl_set_hnr_aux .

  sepref_definition arl_swap is "uncurry2 mop_list_swap" :: "((arl_assn id_assn)d *a nat_assnk *a nat_assnk a arl_assn id_assn)"
    unfolding gen_mop_list_swap[abs_def]
    by sepref
  sepref_decl_impl (ismop) arl_swap: arl_swap.refine .  
end


interpretation arl: list_custom_empty "arl_assn A" arl_empty op_arl_empty
  apply unfold_locales
  apply (rule arl_empty_hnr)
  by (auto simp: op_arl_empty_def)

lemma [def_pat_rules]: "op_arl_empty_sz$N  UNPROTECT (op_arl_empty_sz N)" by simp
interpretation arl_sz: list_custom_empty "arl_assn A" "arl_empty_sz N" "PR_CONST (op_arl_empty_sz N)"
  apply unfold_locales
  apply (rule arl_empty_sz_hnr)
  by (auto simp: op_arl_empty_sz_def)

end