Theory LLVM_DS_Array_List

section ‹Array-Lists›
theory LLVM_DS_Array_List
imports LLVM_DS_NArray
begin
  type_synonym ('a,'l) array_list = "'l word × 'l word × 'a narray"

  subsection ‹Auxiliary Functions›

  definition [llvm_inline]: "arl_initial_size ≡ Mreturn ((signed_nat (8::_::len word)))"

  definition arl_push_back' :: "('a::llvm_rep,'l::len2) array_list ⇒ 'a ⇒ ('a,'l) array_list llM"    
    where [llvm_inline]: "arl_push_back' al x ≡ doM {
      let (l,c,a) = al;
      array_upd a l x;
      l ← ll_add l (signed_nat 1);
      Mreturn (l,c,a)
    }"
  
      
  definition arl_aux_compute_size :: "'l::len2 word ⇒ 'l word ⇒ 'l word llM" 
  where [llvm_inline]:   
    "arl_aux_compute_size c c' ≡ doM {
      max::'l word ← ll_max_snat;
      max ← ll_udiv max (signed_nat 2);
      b ← ll_icmp_ule c max;
      llc_if b (doM {
          c ← ll_mul c (signed_nat 2);
          cok ← ll_icmp_sle c' c;
          llc_if cok (Mreturn c) (Mreturn c')
        }) 
        (Mreturn c')
    }"
  
  
  definition arl_resize :: "'l word ⇒ ('a::llvm_rep,'l::len2) array_list ⇒ ('a,'l) array_list llM"
    where [llvm_code]: "arl_resize c' al ≡ doM {
      let (l,c,a) = al;
      c ← arl_aux_compute_size c c';
      a' ← narray_new TYPE('a) c;
      arraycpy a' a l;
      narray_free a;
      Mreturn (l,c,a')
    }"    
  
      
  definition arl_ensure_capacity :: "'l word ⇒ ('a::llvm_rep,'l::len2) array_list ⇒ ('a,'l) array_list llM"  
    where [llvm_inline]: "arl_ensure_capacity c' al ≡ doM {
      let (l,c,a) = al;
      cok ← ll_icmp_sle c' c;
      llc_if cok (Mreturn (l,c,a)) (arl_resize c' (l,c,a))
    }"

  
  
  subsection ‹Interface Functions›

  definition arl_new_raw :: "('a::llvm_rep,'l::len2) array_list llM"
  where [llvm_code,llvm_inline]: "arl_new_raw ≡ doM {
    c ← arl_initial_size;
    a ← narray_new TYPE('a) c;
    Mreturn (signed_nat 0,c,a)
  }"
    
  definition arl_new :: "'a::llvm_rep itself ⇒ 'l::len2 itself ⇒ ('a,'l) array_list llM"
  where [llvm_inline]: "arl_new TYPE('a::llvm_rep) TYPE('l::len2) ≡ arl_new_raw"

  
  definition arl_new_sz_raw :: "'l::len2 word ⇒ ('a::llvm_rep,'l) array_list llM"
  where [llvm_code,llvm_inline]: "arl_new_sz_raw n ≡ doM {
    a ← narray_new TYPE('a) n;
    Mreturn (n,n,a)
  }"

  definition arl_new_sz :: "'a::llvm_rep itself ⇒ 'l::len2 word ⇒ ('a,'l) array_list llM" 
    where [llvm_inline]: "arl_new_sz TYPE('a) n ≡ arl_new_sz_raw n"

  definition arl_new_repl :: "'l::len2 word ⇒ 'a::llvm_rep ⇒ ('a,'l) array_list llM" 
    where [llvm_inline]: "arl_new_repl n x ≡ doM {
      a ← narray_new_init n x;
      Mreturn (n,n,a)
    }"
    
          
  definition arl_clear :: "('a::llvm_rep,'l::len2) array_list ⇒ ('a::llvm_rep,'l) array_list llM"
    where [llvm_code,llvm_inline]: "arl_clear al ≡ doM {
      let (l,c,a) = al;
      Mreturn (signed_nat 0,c,a)
    }"  
    
  definition arl_free :: "('a::llvm_rep,'l::len) array_list ⇒ unit llM" 
  where [llvm_code,llvm_inline]: "arl_free al ≡ doM {
    let (_,_,a) = al;
    narray_free a
  }"
  

  definition arl_nth :: "('a::llvm_rep,'l::len2) array_list ⇒ 'll::len2 word ⇒ 'a llM"
    where [llvm_code,llvm_inline]: "arl_nth al i ≡ doM {
      let (l,c,a) = al;
      array_nth a i
    }"
    
  definition arl_upd :: "('a::llvm_rep,'l::len2) array_list ⇒ 'll::len2 word ⇒ 'a ⇒ ('a,'l) array_list llM"
    where [llvm_code,llvm_inline]: "arl_upd al i x ≡ doM {
      let (l,c,a) = al;
      array_upd a i x;
      Mreturn (l,c,a)
    }"
  
  definition arl_len :: "('a::llvm_rep,'l::len2) array_list ⇒ 'l word llM" 
    where [llvm_code,llvm_inline]: "arl_len al ≡ let (l,c,a) = al in Mreturn l"
    
    
  definition [llvm_code,llvm_inline]: "arl_push_back al x ≡ doM {
    l ← arl_len al;
    l ← ll_add l (signed_nat 1);
    al ← arl_ensure_capacity l al;
    arl_push_back' al x
  }"

  definition [llvm_code,llvm_inline]: "arl_pop_back al ≡ doM {
    let (l,c,a) = al;
    l ← ll_sub l (signed_nat 1);
    r ← array_nth a l;
    Mreturn (r,(l,c,a))
  }"
  
  definition [llvm_code,llvm_inline]: "arl_take l' al ≡ doM {
    let (l,c,a) = al;
    Mreturn (l',c,a)
  }"

  definition [llvm_code,llvm_inline]: "arl_last al ≡ doM {
    let (l,c,a) = al;
    l ← ll_sub l (signed_nat 1);
    r ← array_nth a l;
    Mreturn r
  }"
  
  definition [llvm_code,llvm_inline]: "arl_butlast al ≡ doM {
    let (l,c,a) = al;
    l ← ll_sub l (signed_nat 1);
    Mreturn (l,c,a)
  }"
  
    
  text ‹Direct access to array underlying array-list ›
  definition array_of_arl :: "('a::llvm_rep,'l::len2) array_list ⇒ 'a ptr" where 
    [llvm_inline]: "array_of_arl ≡ λ(l,c,a). a"
  
  
  export_llvm (debug) (no_header)
    "arl_new_raw :: (64 word,64) array_list llM" is "arl_new"
    "arl_new_sz_raw :: 64 word ⇒ (64 word,64) array_list llM"
    "arl_clear :: (64 word,64) array_list ⇒ (64 word,64) array_list llM"
    "arl_free :: (64 word,64) array_list ⇒ unit llM" is "arl_free"
    "arl_nth :: (64 word,64) array_list ⇒ 64 word ⇒ 64 word llM" is "arl_nth"
    "arl_upd :: (64 word,64) array_list ⇒ 64 word ⇒ 64 word ⇒ (64 word,64) array_list llM" is "arl_upd"
    "arl_len :: (64 word,64) array_list ⇒ 64 word llM" is "arl_len"
    "arl_push_back :: (64 word,64) array_list ⇒ 64 word ⇒ (64 word,64) array_list llM" is "arl_push_back"
    "arl_pop_back :: (64 word,64) array_list ⇒ (64 word × (64 word,64) array_list) llM" is "arl_pop_back"
    "arl_take :: 64 word ⇒ (64 word,64) array_list ⇒ (64 word,64) array_list llM" is "arl_take"
    "arl_last :: (64 word,64) array_list ⇒ 64 word llM" is "arl_last"
    "arl_butlast :: (64 word,64) array_list ⇒ ((64 word,64) array_list) llM" is "arl_butlast"
    
    
  subsection ‹Reasoning Setup›  
  
  definition arl_assn' :: "('a::llvm_rep list × nat, 'l::len2 word × 'l word × 'a ptr) dr_assn"
    where "arl_assn' ≡ mk_assn (λ(xs,c) (li,ci,ai). 
      EXS l a. ↿snat.assn l li ** ↿snat.assn c ci ** ↿narray_assn a ai 
        ** ↑(LENGTH('l)>4 ∧ l≤c ∧ c=length a ∧ xs = take l a))"
      
  definition arl_assn :: "('a::llvm_rep list, 'l::len2 word × 'l word × 'a ptr) dr_assn"
    where "arl_assn ≡ mk_assn (λxs ali. EXS c. ↿arl_assn' (xs,c) ali)"
    
  subsubsection ‹Auxiliary Rules›
  
  lemma arl_aux_compute_size_rule[vcg_rules]: 
    "llvm_htriple 
      (↑⇩d(LENGTH('a)>2) ** ↿snat.assn c ci ** ↿snat.assn c' ci' ** ↑⇩d(c≤c')) 
      (arl_aux_compute_size ci (ci'::'a::len2 word)) 
      (λri. EXS r. ↿snat.assn r ri ** ↑(max c c' ≤ r))"  
    unfolding arl_aux_compute_size_def
    apply (vcg_monadify)
    by vcg
    
    
  lemma arl_resize_rule[vcg_rules]: 
    "llvm_htriple 
      (↿snat.assn l li ** ↿snat.assn c (ci::'l::len2 word) ** ↿narray_assn a ai ** ↿snat.assn c⇩n ci⇩n
        ** ↑⇩d(LENGTH('l)>2 ∧ c⇩n>c ∧ l≤c ∧ c=length a)
      ) 
      (arl_resize ci⇩n (li,ci,ai))
      (λ(li,ci,ai). EXS c' a'. ↿snat.assn l li ** ↿snat.assn c' ci ** ↿narray_assn a' ai
        ** ↑(c'≥c⇩n ∧ c'=length a' ∧ take l a' = take l a)
      )"  
    unfolding arl_resize_def
    by vcg'
  
    
  lemma arl_ensure_capacity_rule[vcg_rules]: 
    "llvm_htriple
      (↿arl_assn' (al,oc) ali ** ↿snat.assn c ci) (arl_ensure_capacity ci ali) 
      (λali. EXS c'. ↿arl_assn' (al,c') ali ** ↑(c'≥c))
    "  
    unfolding arl_assn'_def arl_ensure_capacity_def
    by vcg
    
  lemma arl_push_back'_rule[vcg_rules]:
    "llvm_htriple 
      (↿arl_assn' (al,c) ali ** ↑⇩d(length al < c)) 
      (arl_push_back' ali x) 
      (λali. EXS c. ↿arl_assn' (al@[x],c) ali)"
    unfolding arl_assn'_def arl_push_back'_def
    apply (vcg_monadify)
    apply vcg'
    apply (auto simp: take_update_last)
    done
        
  lemma arl_len_rule_internal:
    "llvm_htriple (↿arl_assn' (al,c) ali) (arl_len ali) (λli. ↿arl_assn' (al,c) ali ** ↿snat.assn (length al) li)"  
    unfolding arl_assn'_def arl_len_def
    by vcg
  
  subsubsection ‹Interface Rules›

  lemma arl_new_raw_rule[vcg_rules]: 
    "llvm_htriple (↑(LENGTH('l)>4)) (arl_new_raw) (λali. ↿arl_assn [] (ali::(_,'l::len2)array_list))"
    unfolding arl_new_def arl_new_raw_def arl_initial_size_def arl_assn_def arl_assn'_def
    apply (vcg_monadify)
    by vcg'
  
      
  lemma arl_new_rule[vcg_rules]: 
    "llvm_htriple (↑(LENGTH('c)>4)) (arl_new TYPE('a::llvm_rep) TYPE('c::len2)) (λali. ↿arl_assn [] ali)"
    unfolding arl_new_def arl_new_raw_def arl_initial_size_def arl_assn_def arl_assn'_def
    apply (vcg_monadify)
    by vcg'

  lemma arl_new_sz_rule[vcg_rules]: 
    "llvm_htriple 
      (↿snat.assn n ni ** ↑(LENGTH('c::len2)>4)) 
      (arl_new_sz TYPE('a::llvm_rep) (ni::'c word)) 
      (λali. ↿arl_assn (replicate n init) ali)"
    unfolding arl_new_sz_def arl_new_sz_raw_def arl_initial_size_def arl_assn_def arl_assn'_def
    apply (vcg_monadify)
    by vcg'

  lemma arl_new_repl_rule[vcg_rules]: 
    "llvm_htriple 
      (↿snat.assn n ni ** ↑(LENGTH('c::len2)>4)) 
      (arl_new_repl (ni::'c word) x) 
      (λali. ↿arl_assn (replicate n x) ali)"
    unfolding arl_new_repl_def arl_initial_size_def arl_assn_def arl_assn'_def
    apply (vcg_monadify)
    by vcg'
    
        
  lemma arl_assn_init_pure: 
    "PRECOND (SOLVE_AUTO (4 < LENGTH('l))) ⟹ □ ⊢ ↿arl_assn [] (init::(_,'l::len2)array_list)"  
    unfolding arl_assn_def arl_assn'_def vcg_tag_defs
    unfolding snat.assn_def snat_invar_def
    supply [fri_rules] = narray_assn_init_pure
    apply simp
    apply (rule ENTAILSD)
    by vcg
    
  lemma arl_clear_rule[vcg_rules]: 
    "llvm_htriple 
      (↿arl_assn al ali) 
      (arl_clear ali) 
      (λali. ↿arl_assn [] ali)"
    unfolding arl_clear_def arl_assn_def arl_assn'_def
    by (vcg_monadify) vcg'
    
  lemma arl_free_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al ali) (arl_free ali) (λ_. □)"  
    unfolding arl_assn_def arl_assn'_def arl_free_def
    by vcg
    
  lemma arl_nth_rule[vcg_rules]:
    "llvm_htriple 
      (↿arl_assn al ali ** ↿snat.assn i ii ** ↑⇩d(i<length al)) 
      (arl_nth ali ii)
      (λx. ↿arl_assn al ali ** ↑(x = al!i))"
    unfolding arl_assn_def arl_assn'_def arl_nth_def
    by vcg
  
  lemma array_of_arl_nth_rule[vcg_rules]: "llvm_htriple 
    (↿arl_assn xs a ** ↿snat.assn i ii ** ↑(i < length xs))
    (array_nth (array_of_arl a) ii)
    (λx. ↿arl_assn xs a ** ↑(x = xs!i))"
    unfolding arl_assn_def arl_assn'_def array_of_arl_def by vcg
    
  lemma arl_upd_rule[vcg_rules]:
    "llvm_htriple 
      (↿arl_assn al ali ** ↿snat.assn i ii ** ↑⇩d(i<length al)) 
      (arl_upd ali ii x)
      (λali'. ↿arl_assn (al[i:=x]) ali' ** ↑(ali' = ali))"
    unfolding arl_assn_def arl_assn'_def arl_upd_def
    by vcg
    
  lemma arl_len_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al ali) (arl_len ali) (λli. ↿arl_assn al ali ** ↿snat.assn (length al) li)"  
    unfolding arl_assn_def
    supply arl_len_rule_internal[vcg_rules]
    by vcg
    
  lemma arl_push_back_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al (ali::(_,'l::len2)array_list) ** ↑⇩d(length al + 1 < max_snat LENGTH('l))) (arl_push_back ali x) (λali. ↿arl_assn (al@[x]) ali)"  
    unfolding arl_assn_def arl_push_back_def
    supply arl_len_rule_internal[vcg_rules]
    apply (vcg_monadify)
    by vcg'

  lemma arl_pop_back_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al (ali::(_,'l::len2)array_list) ** ↑⇩d(al≠[])) (arl_pop_back ali) (λ(x,ali). ↿arl_assn (butlast al) ali ** ↑(x=last al))"  
    unfolding arl_assn_def arl_assn'_def arl_pop_back_def
    supply arl_len_rule_internal[vcg_rules]
    apply (vcg_monadify)
    apply vcg'
    by (auto simp: take_minus_one_conv_butlast last_take_nth_conv)
    
  lemma arl_take_rule[vcg_rules]:
    "llvm_htriple 
      (↿arl_assn al (ali::(_,'l::len2)array_list) ** ↿snat.assn l li ** ↑⇩d(l ≤ length al)) 
      (arl_take li ali) 
      (λali. ↿arl_assn (take l al) ali)"  
    unfolding arl_assn_def arl_assn'_def arl_take_def
    by vcg
    

  lemma arl_last_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al (ali::(_,'l::len2)array_list) ** ↑⇩d(al≠[])) (arl_last ali) (λx. ↿arl_assn al ali ** ↑(x=last al))"  
    unfolding arl_assn_def arl_assn'_def arl_last_def
    supply arl_len_rule_internal[vcg_rules]
    apply (vcg_monadify)
    apply vcg'
    by (auto simp: last_take_nth_conv)
    
    
  lemma arl_butlast_rule[vcg_rules]:
    "llvm_htriple (↿arl_assn al (ali::(_,'l::len2)array_list) ** ↑⇩d(al≠[])) (arl_butlast ali) (λali. ↿arl_assn (butlast al) ali)"  
    unfolding arl_assn_def arl_assn'_def arl_butlast_def
    supply arl_len_rule_internal[vcg_rules]
    apply (vcg_monadify)
    apply vcg'
    by (auto simp: take_minus_one_conv_butlast)
    
    
    
    
        
end