Theory LLVM_DS_NArray

section ‹Array with Potential Zero Size›
theory LLVM_DS_NArray
imports "LLVM_DS_Array"
begin

  term array_assn

  type_synonym 'a narray = "'a ptr"
  
  definition "narray_assn ≡ mk_assn (λxs p. (case xs of [] ⇒ ↑(p=null) | _ ⇒ ↿array_assn xs p) ** $$''if'' 1 ** $$''ptrcmp_eq'' 1)"
  
  
  
  definition [llvm_inline]: 
    "narray_new TYPE('a::llvm_rep) n ≡ doM { b←ll_icmp_eq n (signed_nat 0); llc_if b (return null) (array_new TYPE('a) n) }"

  thm array_new_rule_snat[no_vars]
  
  abbreviation "cost_narray_new n ≡ $$''malloc'' n ** $$''free'' 1 ** $$''if'' 1 ** $$''if'' 1 ** $$''icmp_eq'' 1 ** $$''ptrcmp_eq'' 1"
  
  lemma narray_new_rule_snat[vcg_rules]: 
    "llvm_htriple (cost_narray_new n ** ↿snat.assn n ni) (narray_new TYPE(_) ni) (↿narray_assn (replicate n init))"
    unfolding narray_assn_def narray_new_def
    supply [split] = list.split
    apply vcg_monadify
    apply vcg
    done
    

  (* TODO: From an abstract point of view, 
    it's a bad idea to split init by the simplifier! 
    Remove that from default setup!
  *)(*      
  lemma narray_assn_init_pure: "□ ⊢ ↿narray_assn [] null"  
    unfolding narray_assn_def
    by (auto simp: sep_algebra_simps)
  *)  
    
  thm array_nth_rule_snat[no_vars]  
    
  lemma narray_nth_rule[vcg_rules]: "llvm_htriple 
    ($$''ofs_ptr'' 1 ** $$''load'' 1 ** ↿narray_assn xs p ∧* ↿snat.assn i ii ∧* ↑⇩d(i < length xs)) 
    (array_nth p ii)
    (λr. ↑(r = xs ! i) ∧* ↿narray_assn xs p)"  
    unfolding narray_assn_def 
    apply (clarsimp split: list.split)
    apply vcg
    done
    
  thm array_upd_rule_snat[no_vars]  

  lemma narray_upd_rule_snat[vcg_rules]: "llvm_htriple 
    ($$''ofs_ptr'' 1 ** $$''store'' 1 ** ↿narray_assn xs p ∧* ↿snat.assn i ii ∧* ↑⇩d(i < length xs)) 
    (array_upd p ii x)
    (λr. ↑(r = p) ∧* ↿narray_assn (xs[i := x]) p)"
    unfolding narray_assn_def 
    apply (clarsimp split: list.splits nat.splits; intro allI impI conjI)
    apply vcg
    done
    
  definition [llvm_code]: "narray_free p ≡ doM { b ← ll_ptrcmp_eq p null; llc_if b (return ()) (array_free p) }"
  
  lemma narray_free_rule[vcg_rules]: 
    "llvm_htriple (↿narray_assn xs p) (narray_free p) (λ_. □)"
    unfolding narray_assn_def narray_free_def
    supply [split] = list.split
    apply vcg_monadify
    apply vcg
    done


  (*  
  lemma narrayset_rule_snat[vcg_rules]: "llvm_htriple 
    (↿narray_assn dst dsti ** ↿snat.assn n ni ** ↑⇩d(n≤length dst))
    (arrayset dsti c ni)
    (λ_. ↿narray_assn (replicate n c @ drop n dst) dsti)"  
    unfolding narray_assn_def
    apply (cases dst; clarsimp split: list.splits)
    supply [vcg_rules] = arrayset_zerosize_rule
    by vcg
        
  definition [llvm_code]: "narray_new_init n (c::'a::llvm_rep) ≡ doM { 
    r ← narray_new TYPE('a) n; 
    arrayset r c n;
    return r
  }"
  
  lemma narray_new_init_rule[vcg_rules]: "llvm_htriple   
    (↿snat.assn n ni) 
    (narray_new_init ni c) 
    (λr. ↿narray_assn (replicate n c) r)"
    unfolding narray_new_init_def
    by vcg 
    
  lemma arraycpy_0_rl:
    "llvm_htriple (↿snat.assn 0 ni) (arraycpy dsti srci ni) (λ_. □)"  
    unfolding arraycpy_def
    apply (subst llc_while_unfold)
    apply vcg_monadify
    apply vcg'
    done
    
  lemma narraycpy_rule_snat[vcg_rules]: 
    "llvm_htriple 
      (↿narray_assn dst dsti ** ↿narray_assn src srci ** ↿snat.assn n ni ** ↑⇩d(n≤length src ∧ n≤length dst))
      (arraycpy dsti srci ni)
      (λ_. ↿narray_assn (take n src @ drop n dst) dsti ** ↿narray_assn src srci)"
    unfolding narray_assn_def
    apply (cases dst; cases src; simp)
    supply [vcg_rules] = arraycpy_0_rl
    apply vcg
    apply (clarsimp split: list.splits)
    apply vcg
    done

  
  definition [llvm_code]: "array_grow newsz oldsz src ≡ doM {
    dst ← narray_new TYPE(_) newsz;
    arraycpy dst src oldsz;
    narray_free src;
    return dst
  }"  
  
  lemma narray_grow_rule_snat[vcg_rules]: "llvm_htriple 
    (↿narray_assn src srci ** ↿snat.assn newsz newszi ** ↿snat.assn oldsz oldszi ** ↑(oldsz ≤ length src ∧ oldsz ≤ newsz))
    (array_grow newszi oldszi srci)
    (λdsti. ↿narray_assn (take oldsz src@replicate (newsz - oldsz) init) dsti)"
    unfolding array_grow_def
    by vcg
  *)    
      
  definition [llvm_code]: "example1 (n::64 word) ≡ doM {
    a ← narray_new TYPE(8 word) n;
    array_upd a (1::64 word) 42;
    ll_call (narray_free a)
  }"  
    
  export_llvm (debug) example1 (* is "example1" file "exampel1.ll"*)
    
end