Theory ROBDD.Pointer_Map_Impl

section‹Imparative implementation for Pointermap›
theory Pointer_Map_Impl
imports Array_List 
  Separation_Logic_Imperative_HOL.Sep_Main
  Separation_Logic_Imperative_HOL.Hash_Map_Impl
  Pointer_Map
begin

  record 'a pointermap_impl =
    entriesi :: "'a array_list"
    getentryi :: "('a,nat) hashtable"
  lemma pointermapieq_exhaust: "entries a = entries b ⟹ getentry a = getentry b ⟹ a = (b :: 'a pointermap)" by simp

  definition is_pointermap_impl :: "('a::{hashable,heap}) pointermap ⇒ 'a pointermap_impl ⇒ assn" where
    "is_pointermap_impl b bi ≡ 
      is_array_list (entries b) (entriesi bi) 
    * is_hashmap (getentry b) (getentryi bi)"

  lemma is_pointermap_impl_prec: "precise is_pointermap_impl"
    unfolding is_pointermap_impl_def[abs_def]
  apply(rule preciseI)
  apply(clarsimp)
  apply(rename_tac a a' x y p F F')
  apply(rule pointermapieq_exhaust)
   apply(rule_tac p = "entriesi p" and h = "(x,y)" in preciseD[OF is_array_list_prec])
   apply(unfold star_aci(1))
   apply blast
  apply(rule_tac p = "getentryi p" and h = "(x,y)" in preciseD[OF is_hashmap_prec])
  apply(simp only: star_aci(2)[symmetric])
  apply(simp only: star_aci(1)[symmetric]) (* black unfold magic *)
  apply(simp only: star_aci(2)[symmetric])
  done

  definition pointermap_empty where
    "pointermap_empty ≡ do {
      hm ← hm_new;
      arl ← arl_empty;
      return ⦇entriesi = arl, getentryi = hm ⦈
    }"

  lemma [sep_heap_rules]: "< emp > pointermap_empty <is_pointermap_impl empty_pointermap>⇩t"
    unfolding is_pointermap_impl_def
    by (sep_auto simp: pointermap_empty_def empty_pointermap_def)

  definition pm_pthi where
    "pm_pthi m p ≡ arl_nth (entriesi m) p"

  lemma [sep_heap_rules]: "pointermap_sane m ⟹ pointermap_p_valid p m ⟹
    < is_pointermap_impl m mi > pm_pthi mi p <λai. is_pointermap_impl m mi * ↑(ai = pm_pth m p)>"
    by (sep_auto simp: pm_pthi_def pm_pth_def is_pointermap_impl_def pointermap_p_valid_def)

  definition pointermap_getmki where
    "pointermap_getmki a m ≡ do {
        lo ← ht_lookup a (getentryi m);
        (case lo of 
          Some l ⇒ return (l,m) | 
          None ⇒ do {
            p ← return (snd (entriesi m));
        ent ← arl_append (entriesi m) a;
        lut ← hm_update a p (getentryi m);
        u ← return ⦇entriesi = ent, getentryi = lut⦈;
        return (p,u)
          }
        )
    }"

  lemmas pointermap_getmki_defs = pointermap_getmki_def pointermap_getmk_def pointermap_insert_def is_pointermap_impl_def
  lemma [sep_heap_rules]: "pointermap_sane m ⟹ pointermap_getmk a m = (p,u) ⟹
    < is_pointermap_impl m mi >
      pointermap_getmki a mi
    <λ(pi,ui). is_pointermap_impl u ui * ↑(pi = p)>⇩t"
  apply(cases "getentry m a")
   apply(unfold pointermap_getmki_def)
   apply(unfold return_bind)
   apply(rule bind_rule[where R = "λr. is_pointermap_impl m mi * ↑(r = None ∧ (snd (entriesi mi) = p)) * true"])
    apply(sep_auto simp: pointermap_getmki_defs is_array_list_def split: prod.splits;fail)
   apply(sep_auto simp: pointermap_getmki_defs)+
  done

end