Theory Refine_Imperative_HOL.IICF_MS_Array_List

theory IICF_MS_Array_List
imports 
  "../Intf/IICF_List" 
  Separation_Logic_Imperative_HOL.Array_Blit
  Separation_Logic_Imperative_HOL.Default_Insts
begin

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

  definition "is_ms_array_list ms l ≡ λ(a,n). ∃⇩Al'. a ↦⇩a l' * ↑(n ≤ length l' ∧ l = take n l' ∧ ms=length l')"

  lemma is_ms_array_list_prec[safe_constraint_rules]: "precise (is_ms_array_list ms)"
    unfolding is_ms_array_list_def[abs_def]
    apply(rule preciseI)
    apply(simp split: prod.splits) 
  	using preciseD snga_prec by fastforce

  definition "marl_empty_sz maxsize ≡ do {
    a ← Array.new maxsize default;
    return (a,0)
  }"

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

  definition marl_length :: "'a::heap ms_array_list ⇒ nat Heap" where
    "marl_length ≡ λ(a,n). return (n)"

  definition marl_is_empty :: "'a::heap ms_array_list ⇒ bool Heap" where
    "marl_is_empty ≡ λ(a,n). return (n=0)"

  definition marl_last :: "'a::heap ms_array_list ⇒ 'a Heap" where
    "marl_last ≡ λ(a,n). do {
      Array.nth a (n - 1)
    }"

  definition marl_butlast :: "'a::heap ms_array_list ⇒ 'a ms_array_list Heap" where
    "marl_butlast ≡ λ(a,n). do {
      return (a,n - 1)
    }"

  definition marl_get :: "'a::heap ms_array_list ⇒ nat ⇒ 'a Heap" where
    "marl_get ≡ λ(a,n) i. Array.nth a i"

  definition marl_set :: "'a::heap ms_array_list ⇒ nat ⇒ 'a ⇒ 'a ms_array_list Heap" where
    "marl_set ≡ λ(a,n) i x. do { a ← Array.upd i x a; return (a,n)}"

  lemma marl_empty_sz_rule[sep_heap_rules]: "< emp > marl_empty_sz N <is_ms_array_list N []>"
    by (sep_auto simp: marl_empty_sz_def is_ms_array_list_def)

  lemma marl_append_rule[sep_heap_rules]: "length l < N ⟹
    < is_ms_array_list N l a > 
      marl_append a x 
    <λa. is_ms_array_list N (l@[x]) a >⇩t"  
    by (sep_auto 
      simp: marl_append_def is_ms_array_list_def take_update_last 
      split: prod.splits)
    
  lemma marl_length_rule[sep_heap_rules]: "
    <is_ms_array_list N l a> 
      marl_length a
    <λr. is_ms_array_list N l a * ↑(r=length l)>"
    by (sep_auto simp: marl_length_def is_ms_array_list_def)
    
  lemma marl_is_empty_rule[sep_heap_rules]: "
    <is_ms_array_list N l a> 
      marl_is_empty a
    <λr. is_ms_array_list N l a * ↑(r⟷(l=[]))>"
    by (sep_auto simp: marl_is_empty_def is_ms_array_list_def)

  lemma marl_last_rule[sep_heap_rules]: "
    l≠[] ⟹
    <is_ms_array_list N l a> 
      marl_last a
    <λr. is_ms_array_list N l a * ↑(r=last l)>"
    by (sep_auto simp: marl_last_def is_ms_array_list_def last_take_nth_conv)
    
  lemma marl_butlast_rule[sep_heap_rules]: "
    l≠[] ⟹
    <is_ms_array_list N l a> 
      marl_butlast a
    <is_ms_array_list N (butlast l)>⇩t"
    by (sep_auto 
      split: prod.splits
      simp: marl_butlast_def is_ms_array_list_def butlast_take)

  lemma marl_get_rule[sep_heap_rules]: "
    i<length l ⟹
    <is_ms_array_list N l a> 
      marl_get a i
    <λr. is_ms_array_list N l a * ↑(r=l!i)>"
    by (sep_auto simp: marl_get_def is_ms_array_list_def split: prod.split)

  lemma marl_set_rule[sep_heap_rules]: "
    i<length l ⟹
    <is_ms_array_list N l a> 
      marl_set a i x
    <is_ms_array_list N (l[i:=x])>"
    by (sep_auto simp: marl_set_def is_ms_array_list_def split: prod.split)

  definition "marl_assn N A ≡ hr_comp (is_ms_array_list N) (⟨the_pure A⟩list_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "marl_assn N A" for N A]

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

  definition [simp]: "op_marl_empty_sz (N::nat) ≡ op_list_empty"
  context fixes N :: nat begin
    sepref_register "PR_CONST (op_marl_empty_sz N)"
  end

  lemma [def_pat_rules]: "op_marl_empty_sz$N ≡ UNPROTECT (op_marl_empty_sz N)" by simp

  lemma marl_fold_custom_empty_sz: 
    "op_list_empty = op_marl_empty_sz N"
    "mop_list_empty = RETURN (op_marl_empty_sz N)"
    "[] = op_marl_empty_sz N"
    by auto

  lemma marl_empty_hnr_aux: "(uncurry0 (marl_empty_sz N), uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_ms_array_list N"
    by sep_auto
  lemmas marl_empty_hnr = marl_empty_hnr_aux[FCOMP op_list_empty.fref[of "the_pure A" for A]]
  lemmas marl_empty_hnr_mop = marl_empty_hnr[FCOMP mk_mop_rl0_np[OF mop_list_empty_alt]]

  lemma marl_empty_sz_hnr[sepref_fr_rules]:
    "(uncurry0 (marl_empty_sz N), uncurry0 (RETURN (PR_CONST (op_marl_empty_sz N)))) ∈ unit_assn⇧k →⇩a marl_assn N A"
    using marl_empty_hnr
    by simp

  lemma marl_append_hnr_aux: "(uncurry marl_append,uncurry (RETURN oo op_list_append)) ∈ [λ(l,_). length l<N]⇩a ((is_ms_array_list N)⇧d *⇩a id_assn⇧k) → is_ms_array_list N"
    by sep_auto
  lemmas marl_append_hnr[sepref_fr_rules] = marl_append_hnr_aux[FCOMP op_list_append.fref]
  lemmas marl_append_hnr_mop[sepref_fr_rules] = marl_append_hnr[FCOMP mk_mop_rl2_np[OF mop_list_append_alt]]

  lemma marl_length_hnr_aux: "(marl_length,RETURN o op_list_length) ∈ (is_ms_array_list N)⇧k →⇩a nat_assn"
    by sep_auto
  lemmas marl_length_hnr[sepref_fr_rules] = marl_length_hnr_aux[FCOMP op_list_length.fref[of "the_pure A" for A]]
  lemmas marl_length_hnr_mop[sepref_fr_rules] = marl_length_hnr[FCOMP mk_mop_rl1_np[OF mop_list_length_alt]]

  lemma marl_is_empty_hnr_aux: "(marl_is_empty,RETURN o op_list_is_empty) ∈ (is_ms_array_list N)⇧k →⇩a bool_assn"
    by sep_auto
  lemmas marl_is_empty_hnr[sepref_fr_rules] = marl_is_empty_hnr_aux[FCOMP op_list_is_empty.fref[of "the_pure A" for A]]
  lemmas marl_is_empty_hnr_mop[sepref_fr_rules] = marl_is_empty_hnr[FCOMP mk_mop_rl1_np[OF mop_list_is_empty_alt]]

  lemma marl_last_hnr_aux: "(marl_last,RETURN o op_list_last) ∈ [λx. x≠[]]⇩a (is_ms_array_list N)⇧k → id_assn"
    by sep_auto
  lemmas marl_last_hnr[sepref_fr_rules] = marl_last_hnr_aux[FCOMP op_list_last.fref]
  lemmas marl_last_hnr_mop[sepref_fr_rules] = marl_last_hnr[FCOMP mk_mop_rl1[OF mop_list_last_alt]]

  lemma marl_butlast_hnr_aux: "(marl_butlast,RETURN o op_list_butlast) ∈ [λx. x≠[]]⇩a (is_ms_array_list N)⇧d → (is_ms_array_list N)"
    by sep_auto
  lemmas marl_butlast_hnr[sepref_fr_rules] = marl_butlast_hnr_aux[FCOMP op_list_butlast.fref[of "the_pure A" for A]]
  lemmas marl_butlast_hnr_mop[sepref_fr_rules] = marl_butlast_hnr[FCOMP mk_mop_rl1[OF mop_list_butlast_alt]]

  lemma marl_get_hnr_aux: "(uncurry marl_get,uncurry (RETURN oo op_list_get)) ∈ [λ(l,i). i<length l]⇩a ((is_ms_array_list N)⇧k *⇩a nat_assn⇧k) → id_assn"
    by sep_auto
  lemmas marl_get_hnr[sepref_fr_rules] = marl_get_hnr_aux[FCOMP op_list_get.fref]
  lemmas marl_get_hnr_mop[sepref_fr_rules] = marl_get_hnr[FCOMP mk_mop_rl2[OF mop_list_get_alt]]

  lemma marl_set_hnr_aux: "(uncurry2 marl_set,uncurry2 (RETURN ooo op_list_set)) ∈ [λ((l,i),_). i<length l]⇩a ((is_ms_array_list N)⇧d *⇩a nat_assn⇧k *⇩a id_assn⇧k) → (is_ms_array_list N)"
    by sep_auto
  lemmas marl_set_hnr[sepref_fr_rules] = marl_set_hnr_aux[FCOMP op_list_set.fref]
  lemmas marl_set_hnr_mop[sepref_fr_rules] = marl_set_hnr[FCOMP mk_mop_rl3[OF mop_list_set_alt]]

end

context
  fixes N :: nat
  assumes N_sz: "N>10"
begin

schematic_goal "hn_refine (emp) (?c::?'c Heap) ?Γ' ?R (do {
  let x = op_marl_empty_sz N;
  RETURN (x@[1::nat])
})"  
  using N_sz
  by sepref

end

schematic_goal "hn_refine (emp) (?c::?'c Heap) ?Γ' ?R (do {
  let x = op_list_empty;
  RETURN (x@[1::nat])
})"  
  apply (subst marl_fold_custom_empty_sz[where N=10])
  apply sepref
  done

end