Theory LLVM_DS_Circ_List

section ‹Circular Singly Linked Lists›
theory LLVM_DS_Circ_List
imports LLVM_DS_List_Seg
begin

text ‹
  Example of circular lists, with efficient append, prepend, pop, and rotate
  operations.
  
  TODO: Add delete operation,. e.g. by iterating pop
›

subsection ‹Datatype Definition›

type_synonym 'a cs_list = "'a node ptr"

definition "cs_list_assn ≡ mk_assn (λxs p. lseg xs p p ** ↑(xs=[] ⟷ p=null))"

lemma cs_list_assn_simps:
  "↿cs_list_assn xs null = ↑(xs=[])"
  "↿cs_list_assn [] p = ↑(p=null)"
  unfolding cs_list_assn_def 
  by (auto simp: sep_algebra_simps)


subsection ‹Operations›
subsubsection ‹Allocate Empty List›
definition cs_empty :: "'a::llvm_rep cs_list llM" where [llvm_code, llvm_inline]:
  "cs_empty ≡ Mreturn null"

lemma cs_empty_rule: "llvm_htriple □ cs_empty (λr. ↿cs_list_assn [] r)"
  unfolding cs_empty_def cs_list_assn_def
  by vcg

subsubsection ‹Prepend Element›

definition cs_prepend :: "'a::llvm_rep ⇒ 'a cs_list ⇒ 'a cs_list llM" where [llvm_code]:
  "cs_prepend x p ≡ 
    if p=null then doM {
      p ← ll_balloc;
      ll_store (Node x p) p;
      Mreturn p
    } else doM {
      n ← ll_load p;
      q ← ll_ref (Node (node.val n) (node.next n));
      ll_store (Node x q) p;
      Mreturn p
    }"

lemma cs_prepend_rule: 
  "llvm_htriple (↿cs_list_assn xs p) (cs_prepend x p) (λr. ↿cs_list_assn (x#xs) r)"
  unfolding cs_prepend_def cs_list_assn_def
  apply (cases "xs"; simp)
  apply vcg
  done

subsubsection ‹Append Element›
definition cs_append :: "'a::llvm_rep ⇒ 'a cs_list ⇒ 'a cs_list llM" where [llvm_code]:
  "cs_append x p ≡ doM {
    if p=null then doM {
      p ← ll_balloc;
      ll_store (Node x p) p;
      Mreturn p
    } else doM {
      n ← ll_load p;
      q ← ll_ref (Node (node.val n) (node.next n));
      ll_store (Node x q) p;
      Mreturn q
    }
  }"

lemma cs_append_rule: 
  "llvm_htriple (↿cs_list_assn xs p) (cs_append x p) (λr. ↿cs_list_assn (xs@[x]) r)"
  unfolding cs_append_def cs_list_assn_def
  apply (cases "xs"; simp add: lseg_append)
  apply vcg
  done

subsubsection ‹Pop First Element›

definition cs_pop :: "'a::llvm_rep cs_list ⇒ ('a×'a cs_list) llM" where [llvm_code]:
  "cs_pop p ≡ doM {
    n⇩1 ← ll_load p;
    let p⇩2 = node.next n⇩1;
    tmp ← ll_ptrcmp_eq p⇩2 p;
    if to_bool tmp then doM {
      ll_free p;
      Mreturn (node.val n⇩1,null) ― ‹Singleton list becomes empty list›
    } else doM {
      n⇩2 ← ll_load p⇩2;
      ll_store n⇩2 p;
      ll_free p⇩2;
      Mreturn (node.val n⇩1,p)
    }
  }"

  
lemma ll_bpto_not_same1: 
  "(↿ll_bpto x p ∧* ↿ll_bpto y p) = sep_false"  
  apply (auto simp: ll_bpto_def sep_algebra_simps ll_pto_not_same)
  by (simp add: ll_pto_not_same sep.mult.left_commute sep.mult_commute)

lemma ll_bpto_not_same2: 
  "(↿ll_bpto x p ∧* ↿ll_bpto y p ** F) = sep_false"  
  apply (auto simp: ll_bpto_def sep_algebra_simps ll_pto_not_same)
  by (simp add: ll_pto_not_same sep.mult.left_commute sep.mult_commute)

lemmas ll_bpto_not_same = ll_bpto_not_same1 ll_bpto_not_same2  
    
context  
begin
  interpretation llvm_prim_ctrl_setup .
  interpretation llvm_prim_arith_setup .
  
lemma cs_pop_rule: 
  "llvm_htriple (↿cs_list_assn (x#xs) p) (cs_pop p) (λ(y,p'). ↿cs_list_assn xs p' ** ↑(y=x))"
  unfolding cs_list_assn_def cs_pop_def
  apply (cases xs; simp)
  supply [simp] = ll_bpto_not_same
  apply vcg
  done

end
  
subsubsection ‹Rotate›

definition cs_rotate :: "'a::llvm_rep cs_list ⇒ 'a cs_list llM" where [llvm_code]:
  "cs_rotate p ≡ if p=null then Mreturn null else doM {
    n ← ll_load p;
    Mreturn (node.next n)
  }"

  
lemma list01_cases:
  obtains (Nil) "xs=[]" | (Sng) x where "xs=[x]" | (Long) x y xs' where "xs=x#y#xs'"
  by (rule remdups_adj.cases)
  
  
  
lemma cs_rotate_rule: 
  "llvm_htriple (↿cs_list_assn xs p) (cs_rotate p) (λr. ↿cs_list_assn (rotate1 xs) r)"
  unfolding cs_list_assn_def cs_rotate_def
  apply (cases xs rule: list01_cases; simp add: lseg_append)
  apply vcg
  done

subsection ‹Test›
definition [llvm_code]: "test ≡ doM {
  l ← cs_empty;
  l ← cs_append 1 l;
  l ← cs_append 2 l;
  l ← cs_append 3 l;
  l ← cs_prepend 4 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;
  Mreturn (v1,v2,v3,v4)
}"

(* TODO: Move! *)

export_llvm 
  "cs_empty :: 64 word cs_list llM"
  "cs_prepend :: 64 word ⇒ _"
  "cs_append :: 64 word ⇒ _"
  "cs_pop :: 64 word cs_list ⇒ _"

export_llvm "test :: (64 word × _) llM"

end