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)"
  
  term array_new
  
  definition [llvm_inline]: 
    "narray_new TYPE('a::llvm_rep) n  if n=signed_nat 0 then Mreturn null else array_new TYPE('a) n"

  thm array_new_rule_snat[no_vars]
  
  lemma narray_new_rule_snat[vcg_rules]: 
    "llvm_htriple (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 
    (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 
    (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  if p=null then Mreturn () else array_free p"
  
  thm array_free_rule[no_vars]
  
  lemma narray_free_rule[vcg_rules]: 
    "llvm_htriple (narray_assn xs p) (narray_free p) (λ_. )"
    unfolding narray_assn_def narray_free_def
    apply (cases xs; clarsimp)
    apply vcg
    done


  lemma narrayset_rule_snat[vcg_rules]: "llvm_htriple 
    (narray_assn dst dsti ** snat.assn n ni ** d(nlength 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;
    Mreturn 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(nlength src  nlength 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;
    Mreturn 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;
    narray_free a
  }"  
    
  export_llvm (debug) example1 (* is "example1" file "exampel1.ll"*)
    
  
  
  
subsection Array Slices    

context begin

  interpretation llvm_prim_mem_setup .
    
  definition "array_base_assn  mk_assn (λn p. if n=0 then (p=null) else ll_malloc_tag (int n) p)"

  definition "array_slice_assn  mk_assn (λxs p. 
    if xs=[] then  
    else (ll_range {0..<int (length xs)}) ((!) xs o nat) p
  )"

  lemma array_slice_empty[sep_algebra_simps]: 
    "array_slice_assn [] p = "
    "array_slice_assn xs null = (xs=[])"
    unfolding array_slice_assn_def
    by (auto simp add: sep_algebra_simps ll_range_def)
  
  lemma array_assn_split: "narray_assn xs p = (array_slice_assn xs p ** array_base_assn (length xs) p)"
    unfolding array_assn_def narray_assn_def array_slice_assn_def array_base_assn_def
    by (auto simp: sep_algebra_simps split: list.split)
  
  lemma array_slice_split_aux: "{0..<i + j} = {0..<i}  {i..<i+j}" if "i0" "j0" for i j :: int
    using that by auto
    
    
  lemma ll_range_shift:
    "(ll_range {l+ofs..<h+ofs}) f p = (ll_range {l..<h}) (λi. f (i+ofs)) (p+aofs)"
  proof -
    have "(⋃*i{l + ofs..<h + ofs}. ll_pto (f i) (p +a i)) = (⋃*i((+)ofs)`{l..<h}. ll_pto (f i) (p +a i))" 
      by simp
    also have " = (⋃*x{l..<h}. ll_pto (f (x + ofs)) (p +a (ofs + x)))"  
      apply (subst sep_set_img_map)
      apply (simp_all add: algebra_simps)
      done
    finally show ?thesis
      apply (simp add: ll_range_def)
      apply (cases "abase p"; simp add: sep_algebra_simps)
      done
  qed    
    
  (* TODO: Move *)
  lemma ll_range_empty[sep_algebra_simps]: "(ll_range {}) f p = (abase p)" unfolding ll_range_def by (auto)
  
  (* TODO: Move *)
  lemma ll_range_no_base[sep_algebra_simps]: "¬abase p  (ll_range I) f p = sep_false"
    unfolding ll_range_def by (auto)
  
    
  lemma array_slice_assn_split: "array_slice_assn (xs1@xs2) p = (array_slice_assn xs1 p ** array_slice_assn xs2 (p +a int (length xs1)))"  
  proof -

    have 1: "(ll_range {0..<int (length xs1)}) (λi. (xs1 @ xs2) ! nat i) p 
      = (ll_range {0..<int (length xs1)}) (λi. xs1 ! nat i) p"
      apply (rule ll_range_cong)
      apply auto
      done
      
    have "(ll_range {int (length xs1)..<int (length xs1) + int (length xs2)}) (λx. (xs1 @ xs2) ! nat x) p
      = (ll_range {0+int (length xs1)..<int (length xs2) + int (length xs1)}) (λx. (xs1 @ xs2) ! nat x) p"  
      by (simp add: algebra_simps)
    also have " = (ll_range {0..<int (length xs2)}) (λi. (xs1 @ xs2) ! nat (i + int (length xs1))) (p +a int (length xs1))"
      apply (subst ll_range_shift)
      ..
    also have " = (ll_range {0..<int (length xs2)}) (λi. xs2 ! nat i) (p +a int (length xs1))"
      apply (rule ll_range_cong)
      apply (auto simp: nth_append nat_add_distrib)
      done
    finally show ?thesis
      unfolding array_slice_assn_def
      apply (simp add: comp_def array_slice_split_aux ll_range_merge[symmetric] 1)
      apply (cases "abase p")
      apply (auto simp: sep_algebra_simps)
      done
    
  qed    

  lemma array_slice_assn_cnv_range_upd:  
    "i<length xs  array_slice_assn (xs[i:=x]) p = ((ll_range {0..<int (length xs)}) (((!) xs  nat)(int i := x)) p)"
    unfolding array_slice_assn_def
    apply (simp add: sep_algebra_simps)
    apply (rule ll_range_cong)
    by auto
      

  lemma array_slice_nth_rule_snat[vcg_rules]: "llvm_htriple 
    (array_slice_assn xs p ** snat.assn i ii ** d(i<length xs))
    (array_nth p ii)
    (λr. (r = xs!i) ** array_slice_assn xs p)"
    unfolding array_nth_def array_slice_assn_def snat.assn_def
    supply [simp] = cnv_snat_to_uint and [simp del] = nat_uint_eq
    by vcg
    
    
  lemma array_slice_rule_snat[vcg_rules]: "llvm_htriple
    (array_slice_assn xs p ** snat.assn i ii ** d(i<length xs))
    (array_upd p ii x)
    (λr. (r=p) ** array_slice_assn (xs[i:=x]) p)"
    apply (cases "i<length xs") 
    subgoal
      apply (subst array_slice_assn_cnv_range_upd; simp)
      unfolding array_upd_def array_slice_assn_def snat.assn_def
      supply [simp] = cnv_snat_to_uint and [simp del] = nat_uint_eq
      supply [fri_rules] = fri_abs_cong_rl
      apply vcg
      done
    subgoal by vcg  
    done
    
    
end  
  
  
end