Theory BPlusTree_ImpSplitCE

theory BPlusTree_ImpSplitCE
  imports
    BPlusTree_ImpRange
    BPlusTree_ImpSet
    BPlusTree_SplitCE
begin


subsection "Obtaining executable code"

text "In order to obtain fully defined functions,
we need to plug our split function implementations
into the locales we introduced previously."

text "Obtaining actual code turns out to be slightly more difficult
  due to the use of locales. However, we successfully obtain
the B-tree insertion and membership query with binary search splitting."



global_interpretation bplustree_imp_binary_split_list: split⇩i_list_smeq bin'_split
  defines bplustree_isin_list = bplustree_imp_binary_split_list.isin_list⇩i
    and bplustree_ins_list = bplustree_imp_binary_split_list.ins_list⇩i
    and bplustree_del_list = bplustree_imp_binary_split_list.del_list⇩i
    and bplustree_lrange_list = bplustree_imp_binary_split_list.lrange_list⇩i
  apply unfold_locales
  apply(sep_auto heap: bin'_split_rule)
  done

print_theorems

global_interpretation bplustree_imp_binary_split: 
  split⇩i_full_smeq bin_split bin'_split 
  defines bplustree_isin = bplustree_imp_binary_split.isin⇩i
    and bplustree_ins = bplustree_imp_binary_split.ins⇩i
    and bplustree_insert = bplustree_imp_binary_split.insert⇩i
    (*and bplustree_del = bplustree_imp_binary_split.del
    and bplustree_delete = bplustree_imp_binary_split.delete*)
    and bplustree_empty = bplustree_imp_binary_split.empty⇩i
    and bplustree_leaf_nodes_lrange = bplustree_imp_binary_split.leaf_nodes_lrange⇩i
    and bplustree_lrange = bplustree_imp_binary_split.concat_leaf_nodes_lrange⇩i
  apply unfold_locales
  apply(sep_auto heap: bin_split_rule)
  done

lemma [code]:
"bplustree_isin p x =
!p ⤜
(λnode.
    case node of
    Btnode ts t ⇒
      bin_split ts x ⤜
      (λi. pfa_length ts ⤜
            (λtsl. if i < tsl
                    then pfa_get ts i ⤜
                         (λs. let (sub, sep) = s in bplustree_isin (the sub) x)
                    else bplustree_isin t x))
    | Btleaf xs xa ⇒ bplustree_isin_list x xs)"
  unfolding bplustree_isin_list_def
  by (simp add: bplustree_imp_binary_split.isin⇩i.simps)
lemma [code]:
"bplustree_ins k x p =
!p ⤜
(λnode.
    case node of
    Btnode tsi ti ⇒
      bin_split tsi x ⤜
      (λi. pfa_length tsi ⤜
            (λtsl. if i < tsl
                    then pfa_get tsi i ⤜
                         (λs. let (sub, sep) = s
                               in bplustree_ins k x (the sub) ⤜
                                  (λr. case r of
                                        bplustree_imp_binary_split.T⇩i lp ⇒
                                          pfa_set tsi i (Some lp, sep) ⤜
                                          (λ_. return (bplustree_imp_binary_split.T⇩i p))
                                        | bplustree_imp_binary_split.Up⇩i lp x' rp ⇒
                                            pfa_set tsi i (Some rp, sep) ⤜
                                            (λ_.
  pfa_insert_grow tsi i (Some lp, x') ⤜
  (λtsi'. p := Btnode tsi' ti ⤜ (λ_. bplustree_imp_binary_split.node⇩i k p)))))
                    else bplustree_ins k x ti ⤜
                         (λr. case r of
                               bplustree_imp_binary_split.T⇩i lp ⇒
                                 p := Btnode tsi lp ⤜
                                 (λ_. return (bplustree_imp_binary_split.T⇩i p))
                               | bplustree_imp_binary_split.Up⇩i lp x' rp ⇒
                                   pfa_append_grow' tsi (Some lp, x') ⤜
                                   (λtsi'.
                                       p := Btnode tsi' rp ⤜
                                       (λ_. bplustree_imp_binary_split.node⇩i k p)))))
    | Btleaf ksi nxt ⇒
         bplustree_ins_list x ksi ⤜
        (λksi'. p := Btleaf ksi' nxt ⤜ (λ_. bplustree_imp_binary_split.Lnode⇩i k p)))"
  unfolding bplustree_ins_list_def
  by (simp add: bplustree_imp_binary_split.ins⇩i.simps)

declare bplustree_imp_binary_split.leaf_nodes_lrange⇩i.simps[code]
lemma [code]:
"bplustree_lrange ti x =
    bplustree_leaf_nodes_lrange ti x ⤜
    (λlp. !the lp ⤜
           (λli. case li of
                  Btleaf xs nxt ⇒
                    bplustree_lrange_list x xs ⤜
                    (λarr_it. leaf_values_adjust (nxt, None) arr_it ⤜ return)))"
  unfolding bplustree_lrange_list_def
  by (simp add: bplustree_imp_binary_split.concat_leaf_nodes_lrange⇩i_def)

export_code bplustree_empty bplustree_isin bplustree_insert bplustree_lrange leaf_values_init leaf_values_next leaf_values_has_next checking OCaml SML Scala
export_code bplustree_empty bplustree_isin bplustree_insert bplustree_lrange leaf_values_init leaf_values_next leaf_values_has_next in OCaml module_name BPlusTree
export_code bplustree_empty bplustree_isin bplustree_insert bplustree_lrange leaf_values_init leaf_values_next leaf_values_has_next in SML module_name BPlusTree
export_code bplustree_empty bplustree_isin bplustree_insert bplustree_lrange leaf_values_init leaf_values_next leaf_values_has_next in Scala module_name BPlusTree



end