Theory LLVM_DS_List_Seg

section ‹Singly Linked List Segments›
theory LLVM_DS_List_Seg
imports LLVM_DS_Block_Alloc
begin

subsection ‹Nodes›
text ‹
  We define a node of a list to contain a data value and a next pointer.
›

datatype 'a node = Node (val: 'a) ("next": "'a node ptr")
hide_const (open) node.val node.next

subsubsection ‹Encoding to heap-representable›

instantiation node :: (llvm_rep)llvm_rep
begin
  definition "to_val_node ≡ λNode a b ⇒ LL_STRUCT [to_val a, to_val b]"
  definition "from_val_node p ≡ case llvm_val.the_fields p of [a,b] ⇒ Node (from_val a) (from_val b)"
  definition [simp]: "struct_of_node (_::(('a) node) itself) ≡ VS_STRUCT [struct_of TYPE('a), struct_of TYPE('a node ptr)]"
  definition [simp]: "init_node ::('a) node ≡ Node init init"
  
  instance
    apply standard
    unfolding from_val_node_def to_val_node_def struct_of_node_def init_node_def
    (* TODO: Clean proof here, not breaking abstraction barriers! *)
    apply (auto simp: to_val_word_def init_zero fun_eq_iff split: node.splits)
    subgoal for v v1 v2
      apply (cases v)
      apply (auto split: list.splits)
      done
    subgoal
      by (simp add: LLVM_Shallow.null_def to_val_ptr_def)
    done

end

subsubsection ‹Setup for LLVM code export›
text ‹Declare structure to code generator.›

lemma struct_of_node[ll_struct_of]: "struct_of TYPE('a::llvm_rep node) = VS_STRUCT [struct_of TYPE('a), struct_of TYPE('a::llvm_rep node ptr)]"
  by auto

(*
lemma to_val_node[ll_to_val]: "to_val x = LL_STRUCT [to_val (node.val x), to_val (node.next x)]"
  apply (cases x)
  apply (auto simp: to_val_node_def)
  done
*)  

text ‹Declare as named structure. Required b/c of circular reference.›
lemma [ll_identified_structures]: "ll_is_identified_structure ''node'' TYPE(_ node)"  
  unfolding ll_is_identified_structure_def
  by simp

subsubsection ‹Code Generator Preprocessor Setup›  
text ‹The next two are auxiliary lemmas›
lemma node_insert_value:
  "ll_insert_value (Node x n) x' 0 = Mreturn (Node x' n)"
  "ll_insert_value (Node x n) n' (Suc 0) = Mreturn (Node x n')"

  apply (simp_all add: ll_insert_value_def llvm_insert_value_def Let_def checked_from_val_def 
                to_val_node_def from_val_node_def)
  done

lemma node_extract_value:
  "ll_extract_value (Node x n) 0 = Mreturn x"  
  "ll_extract_value (Node x n) (Suc 0) = Mreturn n"  
  apply (simp_all add: ll_extract_value_def llvm_extract_value_def Let_def checked_from_val_def 
                to_val_node_def from_val_node_def)
  done
  
text ‹Lemmas to translate node construction and destruction›
lemma inline_return_node[llvm_pre_simp]: "Mreturn (Node a x) = doM {
    r ← ll_insert_value init a 0;
    r ← ll_insert_value r x 1;
    Mreturn r
  }"
  apply (auto simp: node_insert_value)
  done

lemma inline_node_case[llvm_pre_simp]: "(case x of (Node a n) ⇒ f a n) = doM {
  a ← ll_extract_value x 0;
  n ← ll_extract_value x 1;
  f a n
}"  
  apply (cases x)
  apply (auto simp: node_extract_value)
  done
  
lemma inline_return_node_case[llvm_pre_simp]: "doM {Mreturn (case x of (Node a n) ⇒ f a n)} = doM {
  a ← ll_extract_value x 0;
  n ← ll_extract_value x 1;
  Mreturn (f a n)
}"  
  apply (cases x)
  apply (auto simp: node_extract_value)
  done
  
lemmas [llvm_inline] = node.val_def node.next_def

(* TODO: Move *)  

subsection ‹List Segment Assertion›
text ‹
  Intuitively, ‹lseg l p s› describes a list starting at ‹p› and
  ending with a pointer ‹s›. The content of the list are ‹l›.
  Note that the pointer ‹s› may also occur earlier in the list, in which
  case it is handled as a usual next-pointer.
›


fun lseg 
  :: "'a::llvm_rep list ⇒ 'a node ptr ⇒ 'a node ptr ⇒ ll_assn"
  where
  "lseg [] p s = ↑(p=s)"
| "lseg (x#l) p s = (
    if p=null then sep_false 
    else (EXS q. ↿ll_bpto (Node x q) p ** lseg l q s))"

lemma lseg_if_splitf1[simp]: 
  "lseg l null null = ↑(l=[])"
  apply (cases l, simp_all)
  done

lemma lseg_if_splitf2[simp]: 
  "lseg (x#xs) p q 
    = (EXS n. ↿ll_bpto (Node x n) p ** lseg xs n q ** ↑(p≠null))"
  apply (cases p, simp_all add: sep_algebra_simps)
  done

subsection ‹Lemmas›

lemma lseg_Cons[simp]: "lseg (x#l) p s = (EXS q. ↿ll_bpto (Node x q) p ** lseg l q s)"
  by simp
  
lemmas [simp del] = lseg.simps(2)  

lemma lseg_append: "lseg (xs@ys) p s = (EXS q. lseg xs p q ** lseg ys q s)"  
  apply (induction xs arbitrary: p)
  apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
  done
  
corollary lseg_split: "lseg (xs@ys) p s ⊢ (EXS q. lseg xs p q ** lseg ys q s)"
  by (simp add: lseg_append)

corollary lseg_fuse: "lseg xs p q ** lseg ys q s ⊢ lseg (xs@ys) p s"
  by (metis entails_def lseg_append)

  
  
end