Theory Separation_Logic_Imperative_HOL.Circ_List

section ‹Circular Singly Linked Lists›
theory Circ_List
imports List_Seg Imp_List_Spec
begin

text ‹
  Example of circular lists, with efficient append, prepend, pop, and rotate
  operations.
›

subsection ‹Datatype Definition›

type_synonym 'a cs_list = "'a node ref option"

text ‹A circular list is described by a list segment, with special
  cases for the empty list:›
fun cs_list :: "'a::heap list ⇒ 'a node ref option ⇒ assn" where
  "cs_list [] None = emp"
| "cs_list (x#l) (Some p) = lseg (x#l) (Some p) (Some p)"
| "cs_list _ _ = false"

lemma [simp]: "cs_list l None = ↑(l=[])"
  by (cases l) auto

lemma [simp]: 
  "cs_list l (Some p) 
  = (∃⇩Ax ls. ↑(l=x#ls) * lseg (x#ls) (Some p) (Some p))"
  apply (rule ent_iffI)
  apply (cases l) 
  apply simp
  apply sep_auto
  apply (cases l) 
  apply simp
  apply sep_auto
  done

subsection ‹Precision›
lemma cs_prec: 
  "precise cs_list"
  apply rule
  apply (case_tac p)
  apply clarsimp

  apply clarsimp
  apply (subgoal_tac "x=xa ∧ n=na", simp)

  apply (erule prec_frame_expl[OF lseg_prec1])
  apply frame_inference
  apply frame_inference

  apply (drule prec_frame[OF sngr_prec])
  apply frame_inference
  apply frame_inference
  apply simp
  done

lemma cs_imp_list_impl: "imp_list cs_list"
  apply unfold_locales
  apply (rule cs_prec)
  done
interpretation cs: imp_list cs_list by (rule cs_imp_list_impl)

subsection ‹Operations›
subsubsection ‹Allocate Empty List›
definition cs_empty :: "'a::heap cs_list Heap" where
  "cs_empty ≡ return None"

lemma cs_empty_rule: "<emp> cs_empty <cs_list []>"
  unfolding cs_empty_def
  by sep_auto

lemma cs_empty_impl: "imp_list_empty cs_list cs_empty" 
  by unfold_locales (sep_auto heap: cs_empty_rule)
interpretation cs: imp_list_empty cs_list cs_empty by (rule cs_empty_impl)

subsubsection ‹Prepend Element›
fun cs_prepend :: "'a ⇒ 'a::heap cs_list ⇒ 'a cs_list Heap" where
  "cs_prepend x None = do {
    p ← ref (Node x None); 
    p:=Node x (Some p); 
    return (Some p)
  }"
| "cs_prepend x (Some p) = do {
    n ← !p;
    q ← ref (Node (val n) (next n));
    p := Node x (Some q);
    return (Some p)
  }"

declare cs_prepend.simps [simp del]

lemma cs_prepend_rule: 
  "<cs_list l p> cs_prepend x p <cs_list (x#l)>"
  apply (cases p)
  apply simp_all
  apply (sep_auto simp: cs_prepend.simps)

  apply (sep_auto simp: cs_prepend.simps)
  done

lemma cs_prepend_impl: "imp_list_prepend cs_list cs_prepend"
  by unfold_locales (sep_auto heap: cs_prepend_rule)
interpretation cs: imp_list_prepend cs_list cs_prepend 
  by (rule cs_prepend_impl)

subsubsection ‹Append Element›
fun cs_append :: "'a ⇒ 'a::heap cs_list ⇒ 'a cs_list Heap" where
  "cs_append x None = do { 
    p ← ref (Node x None); 
    p:=Node x (Some p); 
    return (Some p) }"
| "cs_append x (Some p) = do {
    n ← !p;
    q ← ref (Node (val n) (next n));
    p := Node x (Some q);
    return (Some q)
  }"

declare cs_append.simps [simp del]

lemma cs_append_rule: 
  "<cs_list l p> cs_append x p <cs_list (l@[x])>"
  apply (cases p)
  apply simp_all
  apply (sep_auto simp: cs_append.simps)

  apply (sep_auto simp: cs_append.simps)
  apply (rule ent_frame_fwd)
  apply (rule_tac s=a in lseg_append) (* frame_inference does no backtracking
    on instantiating schematics, hence we have to give it some help here. *)
  apply frame_inference
  apply (sep_auto)
  done

lemma cs_append_impl: "imp_list_append cs_list cs_append"
  by unfold_locales (sep_auto heap: cs_append_rule)
interpretation cs: imp_list_append cs_list cs_append
  by (rule cs_append_impl)

subsubsection ‹Pop First Element›
fun cs_pop :: "'a::heap cs_list ⇒ ('a×'a cs_list) Heap" where
  "cs_pop None = raise STR ''Pop from empty list''"
| "cs_pop (Some p) = do {
    n1 ← !p;
    if next n1 = Some p then
      return (val n1,None) ― ‹Singleton list becomes empty list›
    else do {
      let p2 = the (next n1);
      n2 ← !p2;
      p := Node (val n2) (next n2);
      return (val n1,Some p)
    }
  }"

declare cs_pop.simps[simp del]

lemma cs_pop_rule: 
  "<cs_list (x#l) p> cs_pop p <λ(y,p'). cs_list l p' * true * ↑(y=x)>"
  apply (cases p)
  apply (sep_auto simp: cs_pop.simps)

  apply (cases l)
  apply (sep_auto simp: cs_pop.simps dflt_simps: option.sel)

  apply (sep_auto 
    simp: cs_pop.simps 
    dflt_simps: option.sel 
    eintros del: exI)
  (* Some unfortunate quantifier fiddling :( *)
  apply (rule_tac x=aa in exI)
  apply (rule_tac x=list in exI)
  apply (rule_tac x=a in exI)
  apply clarsimp
  apply (rule exI)
  apply sep_auto
  done

lemma cs_pop_impl: "imp_list_pop cs_list cs_pop"
  apply unfold_locales 
  apply (sep_auto heap: cs_pop_rule elim!: neq_NilE)
  done
interpretation cs: imp_list_pop cs_list cs_pop by (rule cs_pop_impl)

subsubsection ‹Rotate›
fun cs_rotate :: "'a::heap cs_list ⇒ 'a cs_list Heap" where
  "cs_rotate None = return None"
| "cs_rotate (Some p) = do {
    n ← !p;
    return (next n)
  }"

declare cs_rotate.simps [simp del]

lemma cs_rotate_rule: 
  "<cs_list l p> cs_rotate p <cs_list (rotate1 l)>"
  apply (cases p)
  apply (sep_auto simp: cs_rotate.simps)

  apply (cases l)
  apply simp

  apply (case_tac list)
  apply simp
  apply (sep_auto simp: cs_rotate.simps)

  apply (sep_auto simp: cs_rotate.simps)
  apply (rule ent_frame_fwd)
  apply (rule_tac s="a" in lseg_append)
  apply frame_inference
  apply sep_auto
  done

lemma cs_rotate_impl: "imp_list_rotate cs_list cs_rotate"
  apply unfold_locales 
  apply (sep_auto heap: cs_rotate_rule)
  done
interpretation cs: imp_list_rotate cs_list cs_rotate by (rule cs_rotate_impl)

subsection ‹Test›
definition "test ≡ do {
  l ← cs_empty;
  l ← cs_append ''a'' l;
  l ← cs_append ''b'' l;
  l ← cs_append ''c'' l;
  l ← cs_prepend ''0'' l;
  l ← cs_rotate l;
  (v1,l)←cs_pop l;
  (v2,l)←cs_pop l;
  (v3,l)←cs_pop l;
  (v4,l)←cs_pop l;
  return [v1,v2,v3,v4]
}"

definition "test_result ≡ [''a'', ''b'', ''c'', ''0'']"

lemma "<emp> test <λr. ↑(r=test_result) * true>"
  unfolding test_def test_result_def
  apply (sep_auto)
  done
  
export_code test checking SML_imp

ML_val ‹
  val res = @{code test} ();
  if res = @{code test_result} then () else raise Match;
›

hide_const (open) test test_result

end