Theory LLVM_DS_Open_List

section ‹Open Singly Linked Lists›
theory LLVM_DS_Open_List
imports LLVM_DS_List_Seg (*Imp_List_Spec*)
begin

subsection ‹Definitions›
type_synonym 'a os_list = "'a node ptr"

definition os_list_assn :: "('a list, ('a::llvm_rep) os_list) dr_assn" where
  "os_list_assn ≡ mk_assn (λl p. lseg l p null)"

lemma os_list_assn_simps:
  "↿os_list_assn [] p = ↑(p=null)"
  "↿os_list_assn xs null = ↑(xs=[])"
  "↿os_list_assn (x#xs) p = (EXS q. ↿ll_bpto (Node x q) p ** ↿os_list_assn xs q)"
  unfolding os_list_assn_def
  subgoal by auto
  subgoal by auto
  subgoal by (cases "p=null") (auto simp: sep_algebra_simps)
  done
  
  
  
subsection ‹Operations›
subsubsection ‹Allocate Empty List›

definition os_empty :: "_ os_list llM" where [llvm_code, llvm_inline]:
  "os_empty ≡ Mreturn null"

lemma os_empty_rule[vcg_rules]: "llvm_htriple □ os_empty (λr. ↿os_list_assn [] r)"
  unfolding os_empty_def os_list_assn_def
  apply vcg
  done

subsubsection ‹Delete›  

thm partial_function_mono

partial_function (M) os_delete :: "_ os_list ⇒ unit llM" where
  "os_delete p = doM { 
    if p=null then Mreturn () 
    else doM {
      n ← ll_load p;
      ll_free p;
      os_delete (node.next n)
    }
  }"

lemma os_delete_rule[vcg_rules]: 
  "llvm_htriple (↿os_list_assn xs p) (os_delete p) (λ_. □)"  
proof (induction xs arbitrary: p)
  case Nil
  note [simp] = os_list_assn_simps
  show ?case 
    apply (subst os_delete.simps)
    by vcg
next
  case (Cons a xs)
  
  note [vcg_rules] = Cons.IH
  note [simp] = os_list_assn_simps
  
  interpret llvm_prim_ctrl_setup .
  
  show ?case 
    apply (subst os_delete.simps)
    apply vcg
    done
    
  
qed
  
  
  
  
subsubsection ‹Emptiness check›
text ‹A linked list is empty, iff it is the null pointer.›

find_consts bool "1 word"

definition os_is_empty :: "_ os_list ⇒ 1 word llM" where [llvm_code, llvm_inline]:
  "os_is_empty b ≡ Mreturn (from_bool (b = null))"

lemma os_is_empty_rule[vcg_rules]: 
  "llvm_htriple (↿os_list_assn xs b) (os_is_empty b) (λr. ↿os_list_assn xs b ** ↑(r = from_bool (xs = [])))"
  unfolding os_is_empty_def os_list_assn_def
  apply (cases "b=null"; cases xs; simp)
  apply vcg
  done
  
definition os_is_empty' :: "'a os_list ⇒ 8 word llM"
where [llvm_code, llvm_inline]: "os_is_empty' xsi ≡ doM {
  b ← os_is_empty xsi;
  if to_bool b then Mreturn 1 else Mreturn 0
}"

lemma os_is_empty'_rule[vcg_rules]: 
  "llvm_htriple (↿os_list_assn xs b) (os_is_empty' b) (λr. ↿os_list_assn xs b ** ↑(r = (if xs = [] then 1 else 0)))"
proof -
  interpret llvm_prim_ctrl_setup .
  show ?thesis  
    unfolding os_is_empty'_def
    by vcg
    
qed    
  
subsubsection ‹Prepend›

text ‹To push an element to the front of a list we allocate a new node which
  stores the element and the old list as successor. The new list is the new 
  allocated reference.›

  
definition os_prepend :: "'a ⇒ 'a::llvm_rep os_list ⇒ 'a os_list llM" where [llvm_code, llvm_inline]:
  "os_prepend a n = doM { ll_ref (Node a n) }"

lemma os_prepend_rule[vcg_rules]:
  "llvm_htriple (↿os_list_assn xs n) (os_prepend x n) (λr. ↿os_list_assn (x # xs) r)"
  unfolding os_prepend_def os_list_assn_def
  apply vcg
  done

subsubsection‹Pop›
text ‹To pop the first element out of the list we look up the value and the
  reference of the node and Mreturn the pair of those.›

definition os_pop :: "'a::llvm_rep os_list ⇒ ('a × 'a os_list) llM" where
  [llvm_code]: "os_pop p = doM { n ← ll_load p; ll_free p; Mreturn (node.val n, node.next n) }"

lemma os_pop_rule[vcg_rules]:
  "xs ≠ [] ⟹ llvm_htriple 
    (↿os_list_assn xs r) 
    (os_pop r) 
    (λ(x,r'). ↑(x=hd xs) ** ↿os_list_assn (tl xs) r')
  "
  apply (cases xs; simp)
  unfolding os_pop_def os_list_assn_def
  by vcg

definition os_pop' :: "'a::llvm_rep os_list ⇒ ('a × 'a os_list) ptr ⇒ unit llM" 
where [llvm_code, llvm_inline]:
"os_pop' xsi resultp ≡ doM {
  r ← os_pop xsi;
  ll_store r resultp
}"  
  
lemma os_pop'_rule[vcg_rules]:
  "xs ≠ [] ⟹ llvm_htriple 
    (↿os_list_assn xs r ** ↿ll_pto XX resultp) 
    (os_pop' r resultp) 
    (λ_. EXS x r'. ↿ll_pto (x,r') resultp ** ↑(x=hd xs) ** ↿os_list_assn (tl xs) r')
  "
proof -
  interpret llvm_prim_setup .
  assume "xs≠[]"
  then show ?thesis
    unfolding os_pop'_def
    by vcg
qed    
  
subsubsection ‹Reverse›

text ‹The following reversal function is equivalent to the one from 
  Imperative HOL. And gives a more difficult example.›

partial_function (M) os_reverse_aux 
  :: "'a::llvm_rep os_list ⇒ 'a os_list ⇒ 'a os_list llM" 
  where
  "os_reverse_aux q p = doM {
    if p=null then Mreturn q
    else doM {
      v ← ll_load p;
      ll_store (Node (node.val v) q) p;
      os_reverse_aux p (node.next v)
    }
  }"

lemmas [llvm_code] = os_reverse_aux.simps
  
lemma os_reverse_aux_simps[simp]:
  "os_reverse_aux q null = Mreturn q"
  "p≠null ⟹ os_reverse_aux q p = doM {
      v ← ll_load p;
      ll_store (Node (node.val v) q) p;
      os_reverse_aux p (node.next v)
    }"
  apply (subst os_reverse_aux.simps)
  apply simp
  apply (subst os_reverse_aux.simps)
  apply simp
  done

  
definition [llvm_code, llvm_inline]: "os_reverse p = os_reverse_aux null p"

lemma os_reverse_aux_rule: 
  "llvm_htriple 
    (↿os_list_assn xs p ** ↿os_list_assn ys q) 
    (os_reverse_aux q p)
    (λr. ↿os_list_assn ((rev xs) @ ys) r)"
proof (induct xs arbitrary: p q ys)
  case Nil 
  thus ?case
    supply [simp] = os_list_assn_simps
    apply vcg
    done
next
  case (Cons x xs)
  
  note [vcg_rules] = Cons.hyps[where ys = "x#ys"]
  note [simp, named_ss fri_prepare_simps] = os_list_assn_simps
  
  show ?case
    apply (cases "p≠null"; simp)
    by vcg

qed

lemma os_reverse_rule[vcg_rules]: "llvm_htriple 
  (↿os_list_assn xs p) 
  (os_reverse p) 
  (λr. ↿os_list_assn (rev xs) r)"
  unfolding os_reverse_def
  supply [simp] = os_list_assn_simps
  supply R = os_reverse_aux_rule[where ys="[]", simplified]
  supply [vcg_rules] = R
  by vcg
  

subsubsection ‹Remove›
 
text ‹Remove all appearances of an element from a linked list.›

partial_function (M) os_rem 
  :: "'a::llvm_rep ⇒ 'a node ptr ⇒ 'a node ptr llM" 
  where 
  "os_rem x p = doM {
    if p=null then Mreturn null
    else doM {
      n ← ll_load p;
      q ← os_rem x (node.next n);
      if node.val n = x then doM {
        ll_free p;
        Mreturn q
      } else doM {
        ll_store (Node (node.val n) q) p;
        Mreturn p
      }
    } 
  }"

lemmas [llvm_code] = os_rem.simps  
  
lemma [simp]: 
  "os_rem x null = Mreturn null"
  "p≠null ⟹ os_rem x p = doM {
      n ← ll_load p;
      q ← os_rem x (node.next n);
      if node.val n = x then doM {
        ll_free p;
        Mreturn q
      } else doM {
        ll_store (Node (node.val n) q) p;
        Mreturn p
      }
    }"
  apply (subst os_rem.simps, simp)+
  done

lemma os_rem_rule[vcg_rules]: 
  "llvm_htriple (↿os_list_assn xs p) (os_rem x p) (λr. ↿os_list_assn (removeAll x xs) r)"
proof (induct xs arbitrary: p x) (* Have to generalize over x, as 
    preprocessor introduces a new variable. *)
  case Nil 
  
  note [simp] = os_list_assn_simps
  show ?case
    apply vcg
    done
next
  case (Cons y xs) 
  
  note [vcg_rules] = Cons.hyps
  
  note [simp] = os_list_assn_simps
  show ?case 
    apply (cases "p=null"; simp)
    by vcg
  
qed

export_llvm 
  "os_empty :: 64 word os_list llM" is "os_list os_empty ()"
  "os_is_empty' :: 64 word os_list ⇒ _" is "char os_is_empty (os_list)"
  "os_prepend :: 64 word ⇒ _" is "os_list os_prepend(_, os_list)"
  "os_pop' :: 64 word os_list ⇒ _" is "void os_pop(os_list,pop_result*)"
  "os_reverse:: 64 word os_list ⇒ _" is os_reverse
  "os_rem :: 64 word ⇒ _" is os_rem
  defines ‹
    typedef list_elem * os_list;
    typedef struct {uint64_t data; list_elem *next;} list_elem;
    typedef struct {uint64_t data; list_elem *list;} pop_result;
  ›
  rewrites ‹64 word node› = list_elem
  file "../../regression/gencode/open_list.ll"
  
  
end