summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-05-06 15:50:00 +0200
committerSon Ho2022-05-06 15:50:00 +0200
commit38276f00f6aaebb70392775b97577c73a657005a (patch)
tree5986ea371e229540c47d46bb6b425645b2ff4ed2
parent44903dc2da42aa1977be4bbaae36b9d5cb7c70c1 (diff)
Make the betree work
-rw-r--r--tests/betree/BetreeMain.Clauses.Template.fst47
-rw-r--r--tests/betree/BetreeMain.Clauses.fst114
-rw-r--r--tests/betree/BetreeMain.Funs.fst612
3 files changed, 405 insertions, 368 deletions
diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
index 19b5574f..e0279259 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/betree/BetreeMain.Clauses.Template.fst
@@ -8,88 +8,95 @@ open BetreeMain.Types
(** [betree_main::betree::List::{1}::len]: decreases clause *)
unfold
-let betree_list_1_len_decreases (t : Type0) (self : betree_list_t t) : nat =
+let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat =
admit ()
(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
unfold
-let betree_list_1_split_at_decreases (t : Type0) (self : betree_list_t t)
+let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
(n : u64) : nat =
admit ()
(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
unfold
-let betree_list_2_partition_at_pivot_decreases (t : Type0)
+let betree_list_partition_at_pivot_decreases (t : Type0)
(self : betree_list_t (u64 & t)) (pivot : u64) : nat =
admit ()
(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
-let betree_node_5_lookup_in_bindings_decreases (key : u64)
+let betree_node_lookup_in_bindings_decreases (key : u64)
(bindings : betree_list_t (u64 & u64)) : nat =
admit ()
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
unfold
-let betree_node_5_lookup_first_message_for_key_decreases (key : u64)
+let betree_node_lookup_first_message_for_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
unfold
-let betree_node_5_apply_upserts_decreases
+let betree_node_apply_upserts_decreases
(msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
(key : u64) (st : state) : nat =
admit ()
(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
unfold
-let betree_internal_4_lookup_in_children_decreases (self : betree_internal_t)
+let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
(key : u64) (st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
unfold
-let betree_node_5_lookup_decreases (self : betree_node_t) (key : u64)
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
(st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
unfold
-let betree_node_5_lookup_mut_in_bindings_decreases (key : u64)
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
(bindings : betree_list_t (u64 & u64)) : nat =
admit ()
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+unfold
+let betree_node_apply_messages_to_leaf_decreases
+ (bindings : betree_list_t (u64 & u64))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
+ admit ()
+
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
unfold
-let betree_node_5_filter_messages_for_key_decreases (key : u64)
+let betree_node_filter_messages_for_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
unfold
-let betree_node_5_lookup_first_message_after_key_decreases (key : u64)
+let betree_node_lookup_first_message_after_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
+(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *)
+unfold
+let betree_node_apply_messages_to_internal_decreases
+ (msgs : betree_list_t (u64 & betree_message_t))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
+ admit ()
+
(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
unfold
-let betree_internal_4_flush_decreases (self : betree_internal_t)
+let betree_internal_flush_decreases (self : betree_internal_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
unfold
-let betree_node_5_apply_messages_decreases (self : betree_node_t)
+let betree_node_apply_messages_decreases (self : betree_node_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::apply]: decreases clause *)
-unfold
-let betree_node_5_apply_decreases (self : betree_node_t)
- (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
- (key : u64) (new_msg : betree_message_t) (st : state) : nat =
- admit ()
-
diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/betree/BetreeMain.Clauses.fst
index b241e756..8fb43e07 100644
--- a/tests/betree/BetreeMain.Clauses.fst
+++ b/tests/betree/BetreeMain.Clauses.fst
@@ -7,88 +7,118 @@ open BetreeMain.Types
(** [betree_main::betree::List::{1}::len]: decreases clause *)
unfold
-let betree_list_1_len_decreases (t : Type0) (self : betree_list_t t) : nat =
- admit ()
+let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : betree_list_t t =
+ self
(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
unfold
-let betree_list_1_split_at_decreases (t : Type0) (self : betree_list_t t)
+let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
(n : u64) : nat =
- admit ()
+ n
(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
unfold
-let betree_list_2_partition_at_pivot_decreases (t : Type0)
- (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
- admit ()
+let betree_list_partition_at_pivot_decreases (t : Type0)
+ (self : betree_list_t (u64 & t)) (pivot : u64) : betree_list_t (u64 & t) =
+ self
(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
-let betree_node_5_lookup_in_bindings_decreases (key : u64)
- (bindings : betree_list_t (u64 & u64)) : nat =
- admit ()
+let betree_node_lookup_in_bindings_decreases (key : u64)
+ (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
+ bindings
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
unfold
-let betree_node_5_lookup_first_message_for_key_decreases (key : u64)
- (msgs : betree_list_t (u64 & betree_message_t)) : nat =
- admit ()
+let betree_node_lookup_first_message_for_key_decreases (key : u64)
+ (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+ msgs
(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
unfold
-let betree_node_5_apply_upserts_decreases
+let betree_node_apply_upserts_decreases
(msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
- (key : u64) (st : state) : nat =
- admit ()
+ (key : u64) (st : state) : betree_list_t (u64 & betree_message_t) =
+ msgs
(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
unfold
-let betree_internal_4_lookup_in_children_decreases (self : betree_internal_t)
- (key : u64) (st : state) : nat =
- admit ()
+let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
+ (key : u64) (st : state) : betree_internal_t =
+ self
(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
unfold
-let betree_node_5_lookup_decreases (self : betree_node_t) (key : u64)
- (st : state) : nat =
- admit ()
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+ (st : state) : betree_node_t =
+ self
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
unfold
-let betree_node_5_lookup_mut_in_bindings_decreases (key : u64)
- (bindings : betree_list_t (u64 & u64)) : nat =
- admit ()
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
+ (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
+ bindings
+
+unfold
+let betree_node_apply_messages_to_leaf_decreases
+ (bindings : betree_list_t (u64 & u64))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+ new_msgs
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
unfold
-let betree_node_5_filter_messages_for_key_decreases (key : u64)
- (msgs : betree_list_t (u64 & betree_message_t)) : nat =
- admit ()
+let betree_node_filter_messages_for_key_decreases (key : u64)
+ (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+ msgs
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
unfold
-let betree_node_5_lookup_first_message_after_key_decreases (key : u64)
- (msgs : betree_list_t (u64 & betree_message_t)) : nat =
- admit ()
-
+let betree_node_lookup_first_message_after_key_decreases (key : u64)
+ (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+ msgs
+
+let betree_node_apply_messages_to_internal_decreases
+ (msgs : betree_list_t (u64 & betree_message_t))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+ new_msgs
+
+(* This is annoying, we can't use the following trick when defining decrease
+ * clauses as separate functions:
+ * [https://github.com/FStarLang/FStar/issues/138]
+ *
+ * Note that the quantity which effectively decreases is:
+ *
+ * [betree_size; messages_length]
+ * where messages_length is 0 when there are no messages
+ * (and where we use the lexicographic ordering, of course)
+ *
+ * For now, we "patch" the code directly (we need to find a better way...)
+ *)
+let rec betree_size (bt : betree_node_t) : nat =
+ match bt with
+ | BetreeNodeInternal node -> 1 + betree_internal_size node
+ | BetreeNodeLeaf _ -> 1
+
+and betree_internal_size (node : betree_internal_t) : nat =
+ 1 + betree_size node.betree_internal_left + betree_size node.betree_internal_right
+
+let rec betree_list_len (#a : Type0) (ls : betree_list_t a) : nat =
+ match ls with
+ | BetreeListCons _ tl -> 1 + betree_list_len tl
+ | BetreeListNil -> 0
+
+(*
(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
unfold
-let betree_internal_4_flush_decreases (self : betree_internal_t)
+let betree_internal_flush_decreases (self : betree_internal_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
unfold
-let betree_node_5_apply_messages_decreases (self : betree_node_t)
+let betree_node_apply_messages_decreases (self : betree_node_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
-
-(** [betree_main::betree::Node::{5}::apply]: decreases clause *)
-unfold
-let betree_node_5_apply_decreases (self : betree_node_t)
- (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
- (key : u64) (new_msg : betree_message_t) (st : state) : nat =
- admit ()
-
+*)
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index e0d5bb32..d2f63634 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -6,7 +6,7 @@ include BetreeMain.Types
include BetreeMain.Opaque
include BetreeMain.Clauses
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [betree_main::betree::load_internal_node] *)
let betree_load_internal_node_fwd
@@ -115,13 +115,13 @@ let betree_upsert_update_fwd
end
(** [betree_main::betree::List::{1}::len] *)
-let rec betree_list_1_len_fwd
+let rec betree_list_len_fwd
(t : Type0) (self : betree_list_t t) :
- Tot (result u64) (decreases (betree_list_1_len_decreases t self))
+ Tot (result u64) (decreases (betree_list_len_decreases t self))
=
begin match self with
| BetreeListCons x tl ->
- begin match betree_list_1_len_fwd t tl with
+ begin match betree_list_len_fwd t tl with
| Fail -> Fail
| Return i ->
begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
@@ -130,10 +130,10 @@ let rec betree_list_1_len_fwd
end
(** [betree_main::betree::List::{1}::split_at] *)
-let rec betree_list_1_split_at_fwd
+let rec betree_list_split_at_fwd
(t : Type0) (self : betree_list_t t) (n : u64) :
Tot (result ((betree_list_t t) & (betree_list_t t)))
- (decreases (betree_list_1_split_at_decreases t self n))
+ (decreases (betree_list_split_at_decreases t self n))
=
begin match n with
| 0 -> Return (BetreeListNil, self)
@@ -143,7 +143,7 @@ let rec betree_list_1_split_at_fwd
begin match u64_sub n 1 with
| Fail -> Fail
| Return i ->
- begin match betree_list_1_split_at_fwd t tl i with
+ begin match betree_list_split_at_fwd t tl i with
| Fail -> Fail
| Return p ->
let (ls0, ls1) = p in
@@ -155,14 +155,13 @@ let rec betree_list_1_split_at_fwd
end
(** [betree_main::betree::List::{1}::push_front] *)
-let betree_list_1_push_front_fwd_back
+let betree_list_push_front_fwd_back
(t : Type0) (self : betree_list_t t) (x : t) : result (betree_list_t t) =
let tl = mem_replace_fwd (betree_list_t t) self BetreeListNil in
let l = tl in Return (BetreeListCons x l)
(** [betree_main::betree::List::{1}::pop_front] *)
-let betree_list_1_pop_front_fwd
- (t : Type0) (self : betree_list_t t) : result t =
+let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t =
let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
begin match ls with
| BetreeListCons x tl -> Return x
@@ -170,7 +169,7 @@ let betree_list_1_pop_front_fwd
end
(** [betree_main::betree::List::{1}::pop_front] *)
-let betree_list_1_pop_front_back
+let betree_list_pop_front_back
(t : Type0) (self : betree_list_t t) : result (betree_list_t t) =
let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
begin match ls with
@@ -179,14 +178,14 @@ let betree_list_1_pop_front_back
end
(** [betree_main::betree::List::{1}::hd] *)
-let betree_list_1_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
+let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
begin match self with
| BetreeListCons hd l -> Return hd
| BetreeListNil -> Fail
end
(** [betree_main::betree::List::{2}::head_has_key] *)
-let betree_list_2_head_has_key_fwd
+let betree_list_head_has_key_fwd
(t : Type0) (self : betree_list_t (u64 & t)) (key : u64) : result bool =
begin match self with
| BetreeListCons hd l -> let (i, _) = hd in Return (i = key)
@@ -194,10 +193,10 @@ let betree_list_2_head_has_key_fwd
end
(** [betree_main::betree::List::{2}::partition_at_pivot] *)
-let rec betree_list_2_partition_at_pivot_fwd
+let rec betree_list_partition_at_pivot_fwd
(t : Type0) (self : betree_list_t (u64 & t)) (pivot : u64) :
Tot (result ((betree_list_t (u64 & t)) & (betree_list_t (u64 & t))))
- (decreases (betree_list_2_partition_at_pivot_decreases t self pivot))
+ (decreases (betree_list_partition_at_pivot_decreases t self pivot))
=
begin match self with
| BetreeListCons hd tl ->
@@ -205,7 +204,7 @@ let rec betree_list_2_partition_at_pivot_fwd
if i >= pivot
then Return (BetreeListNil, BetreeListCons (i, x) tl)
else
- begin match betree_list_2_partition_at_pivot_fwd t tl pivot with
+ begin match betree_list_partition_at_pivot_fwd t tl pivot with
| Fail -> Fail
| Return p ->
let (ls0, ls1) = p in
@@ -215,19 +214,19 @@ let rec betree_list_2_partition_at_pivot_fwd
end
(** [betree_main::betree::Leaf::{3}::split] *)
-let betree_leaf_3_split_fwd
+let betree_leaf_split_fwd
(self : betree_leaf_t) (content : betree_list_t (u64 & u64))
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(st : state) :
result (state & betree_internal_t)
=
begin match
- betree_list_1_split_at_fwd (u64 & u64) content
+ betree_list_split_at_fwd (u64 & u64) content
params.betree_params_split_size with
| Fail -> Fail
| Return p ->
let (content0, content1) = p in
- begin match betree_list_1_hd_fwd (u64 & u64) content1 with
+ begin match betree_list_hd_fwd (u64 & u64) content1 with
| Fail -> Fail
| Return p0 ->
let (pivot, _) = p0 in
@@ -266,19 +265,19 @@ let betree_leaf_3_split_fwd
end
(** [betree_main::betree::Leaf::{3}::split] *)
-let betree_leaf_3_split_back
+let betree_leaf_split_back
(self : betree_leaf_t) (content : betree_list_t (u64 & u64))
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(st : state) :
result betree_node_id_counter_t
=
begin match
- betree_list_1_split_at_fwd (u64 & u64) content
+ betree_list_split_at_fwd (u64 & u64) content
params.betree_params_split_size with
| Fail -> Fail
| Return p ->
let (content0, content1) = p in
- begin match betree_list_1_hd_fwd (u64 & u64) content1 with
+ begin match betree_list_hd_fwd (u64 & u64) content1 with
| Fail -> Fail
| Return _ ->
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
@@ -310,10 +309,10 @@ let betree_leaf_3_split_back
end
(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
-let rec betree_node_5_lookup_in_bindings_fwd
+let rec betree_node_lookup_in_bindings_fwd
(key : u64) (bindings : betree_list_t (u64 & u64)) :
Tot (result (option u64))
- (decreases (betree_node_5_lookup_in_bindings_decreases key bindings))
+ (decreases (betree_node_lookup_in_bindings_decreases key bindings))
=
begin match bindings with
| BetreeListCons hd tl ->
@@ -324,7 +323,7 @@ let rec betree_node_5_lookup_in_bindings_fwd
if i > key
then Return None
else
- begin match betree_node_5_lookup_in_bindings_fwd key tl with
+ begin match betree_node_lookup_in_bindings_fwd key tl with
| Fail -> Fail
| Return opt -> Return opt
end
@@ -332,10 +331,10 @@ let rec betree_node_5_lookup_in_bindings_fwd
end
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
-let rec betree_node_5_lookup_first_message_for_key_fwd
+let rec betree_node_lookup_first_message_for_key_fwd
(key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_lookup_first_message_for_key_decreases key msgs))
+ (decreases (betree_node_lookup_first_message_for_key_decreases key msgs))
=
begin match msgs with
| BetreeListCons x next_msgs ->
@@ -343,7 +342,7 @@ let rec betree_node_5_lookup_first_message_for_key_fwd
if i >= key
then Return (BetreeListCons (i, m) next_msgs)
else
- begin match betree_node_5_lookup_first_message_for_key_fwd key next_msgs
+ begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
with
| Fail -> Fail
| Return l -> Return l
@@ -352,11 +351,11 @@ let rec betree_node_5_lookup_first_message_for_key_fwd
end
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
-let rec betree_node_5_lookup_first_message_for_key_back
+let rec betree_node_lookup_first_message_for_key_back
(key : u64) (msgs : betree_list_t (u64 & betree_message_t))
(ret : betree_list_t (u64 & betree_message_t)) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_lookup_first_message_for_key_decreases key msgs))
+ (decreases (betree_node_lookup_first_message_for_key_decreases key msgs))
=
begin match msgs with
| BetreeListCons x next_msgs ->
@@ -365,7 +364,7 @@ let rec betree_node_5_lookup_first_message_for_key_back
then Return ret
else
begin match
- betree_node_5_lookup_first_message_for_key_back key next_msgs ret with
+ betree_node_lookup_first_message_for_key_back key next_msgs ret with
| Fail -> Fail
| Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
end
@@ -373,19 +372,18 @@ let rec betree_node_5_lookup_first_message_for_key_back
end
(** [betree_main::betree::Node::{5}::apply_upserts] *)
-let rec betree_node_5_apply_upserts_fwd
+let rec betree_node_apply_upserts_fwd
(msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
(key : u64) (st : state) :
Tot (result (state & u64))
- (decreases (betree_node_5_apply_upserts_decreases msgs prev key st))
+ (decreases (betree_node_apply_upserts_decreases msgs prev key st))
=
- begin match betree_list_2_head_has_key_fwd betree_message_t msgs key with
+ begin match betree_list_head_has_key_fwd betree_message_t msgs key with
| Fail -> Fail
| Return b ->
if b
then
- begin match betree_list_1_pop_front_fwd (u64 & betree_message_t) msgs
- with
+ begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
| Fail -> Fail
| Return msg ->
let (_, m) = msg in
@@ -397,10 +395,10 @@ let rec betree_node_5_apply_upserts_fwd
| Fail -> Fail
| Return v ->
begin match
- betree_list_1_pop_front_back (u64 & betree_message_t) msgs with
+ betree_list_pop_front_back (u64 & betree_message_t) msgs with
| Fail -> Fail
| Return msgs0 ->
- begin match betree_node_5_apply_upserts_fwd msgs0 (Some v) key st
+ begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
with
| Fail -> Fail
| Return (st0, i) -> Return (st0, i)
@@ -414,7 +412,7 @@ let rec betree_node_5_apply_upserts_fwd
| Fail -> Fail
| Return (st0, v) ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t) msgs (key,
+ betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
BetreeMessageInsert v) with
| Fail -> Fail
| Return _ -> Return (st0, v)
@@ -423,19 +421,18 @@ let rec betree_node_5_apply_upserts_fwd
end
(** [betree_main::betree::Node::{5}::apply_upserts] *)
-let rec betree_node_5_apply_upserts_back
+let rec betree_node_apply_upserts_back
(msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
(key : u64) (st : state) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_apply_upserts_decreases msgs prev key st))
+ (decreases (betree_node_apply_upserts_decreases msgs prev key st))
=
- begin match betree_list_2_head_has_key_fwd betree_message_t msgs key with
+ begin match betree_list_head_has_key_fwd betree_message_t msgs key with
| Fail -> Fail
| Return b ->
if b
then
- begin match betree_list_1_pop_front_fwd (u64 & betree_message_t) msgs
- with
+ begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
| Fail -> Fail
| Return msg ->
let (_, m) = msg in
@@ -447,11 +444,11 @@ let rec betree_node_5_apply_upserts_back
| Fail -> Fail
| Return v ->
begin match
- betree_list_1_pop_front_back (u64 & betree_message_t) msgs with
+ betree_list_pop_front_back (u64 & betree_message_t) msgs with
| Fail -> Fail
| Return msgs0 ->
- begin match
- betree_node_5_apply_upserts_back msgs0 (Some v) key st with
+ begin match betree_node_apply_upserts_back msgs0 (Some v) key st
+ with
| Fail -> Fail
| Return msgs1 -> Return msgs1
end
@@ -464,7 +461,7 @@ let rec betree_node_5_apply_upserts_back
| Fail -> Fail
| Return (_, v) ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t) msgs (key,
+ betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
BetreeMessageInsert v) with
| Fail -> Fail
| Return msgs0 -> Return msgs0
@@ -473,40 +470,39 @@ let rec betree_node_5_apply_upserts_back
end
(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-let rec betree_internal_4_lookup_in_children_fwd
+let rec betree_internal_lookup_in_children_fwd
(self : betree_internal_t) (key : u64) (st : state) :
Tot (result (state & (option u64)))
- (decreases (betree_internal_4_lookup_in_children_decreases self key st))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
=
if key < self.betree_internal_pivot
then
- begin match betree_node_5_lookup_fwd self.betree_internal_left key st with
+ begin match betree_node_lookup_fwd self.betree_internal_left key st with
| Fail -> Fail
| Return (st0, opt) -> Return (st0, opt)
end
else
- begin match betree_node_5_lookup_fwd self.betree_internal_right key st with
+ begin match betree_node_lookup_fwd self.betree_internal_right key st with
| Fail -> Fail
| Return (st0, opt) -> Return (st0, opt)
end
(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-and betree_internal_4_lookup_in_children_back
+and betree_internal_lookup_in_children_back
(self : betree_internal_t) (key : u64) (st : state) :
Tot (result betree_internal_t)
- (decreases (betree_internal_4_lookup_in_children_decreases self key st))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
=
if key < self.betree_internal_pivot
then
- begin match betree_node_5_lookup_back self.betree_internal_left key st with
+ begin match betree_node_lookup_back self.betree_internal_left key st with
| Fail -> Fail
| Return n ->
Return (Mkbetree_internal_t self.betree_internal_id
self.betree_internal_pivot n self.betree_internal_right)
end
else
- begin match betree_node_5_lookup_back self.betree_internal_right key st
- with
+ begin match betree_node_lookup_back self.betree_internal_right key st with
| Fail -> Fail
| Return n ->
Return (Mkbetree_internal_t self.betree_internal_id
@@ -514,17 +510,17 @@ and betree_internal_4_lookup_in_children_back
end
(** [betree_main::betree::Node::{5}::lookup] *)
-and betree_node_5_lookup_fwd
+and betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
Tot (result (state & (option u64)))
- (decreases (betree_node_5_lookup_decreases self key st))
+ (decreases (betree_node_lookup_decreases self key st))
=
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
| Fail -> Fail
| Return (st0, msgs) ->
- begin match betree_node_5_lookup_first_message_for_key_fwd key msgs with
+ begin match betree_node_lookup_first_message_for_key_fwd key msgs with
| Fail -> Fail
| Return pending ->
begin match pending with
@@ -533,14 +529,14 @@ and betree_node_5_lookup_fwd
if k <> key
then
begin match
- betree_internal_4_lookup_in_children_fwd (Mkbetree_internal_t
+ betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
| Fail -> Fail
| Return (st1, opt) ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, msg) l) with
| Fail -> Fail
| Return _ -> Return (st1, opt)
@@ -550,46 +546,46 @@ and betree_node_5_lookup_fwd
begin match msg with
| BetreeMessageInsert v ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
| Fail -> Fail
| Return _ -> Return (st0, Some v)
end
| BetreeMessageDelete ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageDelete) l) with
| Fail -> Fail
| Return _ -> Return (st0, None)
end
| BetreeMessageUpsert ufs ->
begin match
- betree_internal_4_lookup_in_children_fwd (Mkbetree_internal_t
+ betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
| Fail -> Fail
| Return (st1, v) ->
begin match
- betree_node_5_apply_upserts_fwd (BetreeListCons (k,
+ betree_node_apply_upserts_fwd (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
| Fail -> Fail
| Return (st2, v0) ->
begin match
- betree_internal_4_lookup_in_children_back
+ betree_internal_lookup_in_children_back
(Mkbetree_internal_t node.betree_internal_id
node.betree_internal_pivot node.betree_internal_left
node.betree_internal_right) key st0 with
| Fail -> Fail
| Return node0 ->
begin match
- betree_node_5_apply_upserts_back (BetreeListCons (k,
+ betree_node_apply_upserts_back (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
| Fail -> Fail
| Return pending0 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key
- msgs pending0 with
+ betree_node_lookup_first_message_for_key_back key msgs
+ pending0 with
| Fail -> Fail
| Return msgs0 ->
begin match
@@ -606,14 +602,14 @@ and betree_node_5_lookup_fwd
end
| BetreeListNil ->
begin match
- betree_internal_4_lookup_in_children_fwd (Mkbetree_internal_t
+ betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
| Fail -> Fail
| Return (st1, opt) ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
BetreeListNil with
| Fail -> Fail
| Return _ -> Return (st1, opt)
@@ -626,7 +622,7 @@ and betree_node_5_lookup_fwd
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
| Fail -> Fail
| Return (st0, bindings) ->
- begin match betree_node_5_lookup_in_bindings_fwd key bindings with
+ begin match betree_node_lookup_in_bindings_fwd key bindings with
| Fail -> Fail
| Return opt -> Return (st0, opt)
end
@@ -634,17 +630,17 @@ and betree_node_5_lookup_fwd
end
(** [betree_main::betree::Node::{5}::lookup] *)
-and betree_node_5_lookup_back
+and betree_node_lookup_back
(self : betree_node_t) (key : u64) (st : state) :
Tot (result betree_node_t)
- (decreases (betree_node_5_lookup_decreases self key st))
+ (decreases (betree_node_lookup_decreases self key st))
=
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
| Fail -> Fail
| Return (st0, msgs) ->
- begin match betree_node_5_lookup_first_message_for_key_fwd key msgs with
+ begin match betree_node_lookup_first_message_for_key_fwd key msgs with
| Fail -> Fail
| Return pending ->
begin match pending with
@@ -653,12 +649,12 @@ and betree_node_5_lookup_back
if k <> key
then
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, msg) l) with
| Fail -> Fail
| Return _ ->
begin match
- betree_internal_4_lookup_in_children_back (Mkbetree_internal_t
+ betree_internal_lookup_in_children_back (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
@@ -670,7 +666,7 @@ and betree_node_5_lookup_back
begin match msg with
| BetreeMessageInsert v ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
| Fail -> Fail
| Return _ ->
@@ -680,7 +676,7 @@ and betree_node_5_lookup_back
end
| BetreeMessageDelete ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageDelete) l) with
| Fail -> Fail
| Return _ ->
@@ -690,32 +686,32 @@ and betree_node_5_lookup_back
end
| BetreeMessageUpsert ufs ->
begin match
- betree_internal_4_lookup_in_children_fwd (Mkbetree_internal_t
+ betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
| Fail -> Fail
| Return (st1, v) ->
begin match
- betree_node_5_apply_upserts_fwd (BetreeListCons (k,
+ betree_node_apply_upserts_fwd (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
| Fail -> Fail
| Return (st2, _) ->
begin match
- betree_internal_4_lookup_in_children_back
+ betree_internal_lookup_in_children_back
(Mkbetree_internal_t node.betree_internal_id
node.betree_internal_pivot node.betree_internal_left
node.betree_internal_right) key st0 with
| Fail -> Fail
| Return node0 ->
begin match
- betree_node_5_apply_upserts_back (BetreeListCons (k,
+ betree_node_apply_upserts_back (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
| Fail -> Fail
| Return pending0 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key
- msgs pending0 with
+ betree_node_lookup_first_message_for_key_back key msgs
+ pending0 with
| Fail -> Fail
| Return msgs0 ->
begin match
@@ -737,12 +733,12 @@ and betree_node_5_lookup_back
end
| BetreeListNil ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
BetreeListNil with
| Fail -> Fail
| Return _ ->
begin match
- betree_internal_4_lookup_in_children_back (Mkbetree_internal_t
+ betree_internal_lookup_in_children_back (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) key st0
with
@@ -757,7 +753,7 @@ and betree_node_5_lookup_back
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
| Fail -> Fail
| Return (_, bindings) ->
- begin match betree_node_5_lookup_in_bindings_fwd key bindings with
+ begin match betree_node_lookup_in_bindings_fwd key bindings with
| Fail -> Fail
| Return _ ->
Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
@@ -767,10 +763,10 @@ and betree_node_5_lookup_back
end
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
-let rec betree_node_5_lookup_mut_in_bindings_fwd
+let rec betree_node_lookup_mut_in_bindings_fwd
(key : u64) (bindings : betree_list_t (u64 & u64)) :
Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_5_lookup_mut_in_bindings_decreases key bindings))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
=
begin match bindings with
| BetreeListCons hd tl ->
@@ -778,7 +774,7 @@ let rec betree_node_5_lookup_mut_in_bindings_fwd
if i >= key
then Return (BetreeListCons (i, i0) tl)
else
- begin match betree_node_5_lookup_mut_in_bindings_fwd key tl with
+ begin match betree_node_lookup_mut_in_bindings_fwd key tl with
| Fail -> Fail
| Return l -> Return l
end
@@ -786,11 +782,11 @@ let rec betree_node_5_lookup_mut_in_bindings_fwd
end
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
-let rec betree_node_5_lookup_mut_in_bindings_back
+let rec betree_node_lookup_mut_in_bindings_back
(key : u64) (bindings : betree_list_t (u64 & u64))
(ret : betree_list_t (u64 & u64)) :
Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_5_lookup_mut_in_bindings_decreases key bindings))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
=
begin match bindings with
| BetreeListCons hd tl ->
@@ -798,7 +794,7 @@ let rec betree_node_5_lookup_mut_in_bindings_back
if i >= key
then Return ret
else
- begin match betree_node_5_lookup_mut_in_bindings_back key tl ret with
+ begin match betree_node_lookup_mut_in_bindings_back key tl ret with
| Fail -> Fail
| Return tl0 -> Return (BetreeListCons (i, i0) tl0)
end
@@ -806,34 +802,34 @@ let rec betree_node_5_lookup_mut_in_bindings_back
end
(** [betree_main::betree::Node::{5}::apply_to_leaf] *)
-let betree_node_5_apply_to_leaf_fwd_back
+let betree_node_apply_to_leaf_fwd_back
(bindings : betree_list_t (u64 & u64)) (key : u64)
(new_msg : betree_message_t) :
result (betree_list_t (u64 & u64))
=
- begin match betree_node_5_lookup_mut_in_bindings_fwd key bindings with
+ begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
| Fail -> Fail
| Return bindings0 ->
- begin match betree_list_2_head_has_key_fwd u64 bindings0 key with
+ begin match betree_list_head_has_key_fwd u64 bindings0 key with
| Fail -> Fail
| Return b ->
if b
then
- begin match betree_list_1_pop_front_fwd (u64 & u64) bindings0 with
+ begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
| Fail -> Fail
| Return hd ->
begin match new_msg with
| BetreeMessageInsert v ->
- begin match betree_list_1_pop_front_back (u64 & u64) bindings0 with
+ begin match betree_list_pop_front_back (u64 & u64) bindings0 with
| Fail -> Fail
| Return bindings1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & u64) bindings1 (key,
- v) with
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
+ with
| Fail -> Fail
| Return bindings2 ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings
+ betree_node_lookup_mut_in_bindings_back key bindings
bindings2 with
| Fail -> Fail
| Return bindings3 -> Return bindings3
@@ -841,12 +837,12 @@ let betree_node_5_apply_to_leaf_fwd_back
end
end
| BetreeMessageDelete ->
- begin match betree_list_1_pop_front_back (u64 & u64) bindings0 with
+ begin match betree_list_pop_front_back (u64 & u64) bindings0 with
| Fail -> Fail
| Return bindings1 ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings
- bindings1 with
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ with
| Fail -> Fail
| Return bindings2 -> Return bindings2
end
@@ -856,17 +852,16 @@ let betree_node_5_apply_to_leaf_fwd_back
begin match betree_upsert_update_fwd (Some i) s with
| Fail -> Fail
| Return v ->
- begin match betree_list_1_pop_front_back (u64 & u64) bindings0
- with
+ begin match betree_list_pop_front_back (u64 & u64) bindings0 with
| Fail -> Fail
| Return bindings1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & u64) bindings1 (key,
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
v) with
| Fail -> Fail
| Return bindings2 ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings
+ betree_node_lookup_mut_in_bindings_back key bindings
bindings2 with
| Fail -> Fail
| Return bindings3 -> Return bindings3
@@ -880,12 +875,11 @@ let betree_node_5_apply_to_leaf_fwd_back
begin match new_msg with
| BetreeMessageInsert v ->
begin match
- betree_list_1_push_front_fwd_back (u64 & u64) bindings0 (key, v)
- with
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
| Fail -> Fail
| Return bindings1 ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings bindings1
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
with
| Fail -> Fail
| Return bindings2 -> Return bindings2
@@ -893,8 +887,7 @@ let betree_node_5_apply_to_leaf_fwd_back
end
| BetreeMessageDelete ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings bindings0
- with
+ betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
| Fail -> Fail
| Return bindings1 -> Return bindings1
end
@@ -903,13 +896,13 @@ let betree_node_5_apply_to_leaf_fwd_back
| Fail -> Fail
| Return v ->
begin match
- betree_list_1_push_front_fwd_back (u64 & u64) bindings0 (key, v)
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
with
| Fail -> Fail
| Return bindings1 ->
begin match
- betree_node_5_lookup_mut_in_bindings_back key bindings
- bindings1 with
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ with
| Fail -> Fail
| Return bindings2 -> Return bindings2
end
@@ -919,11 +912,33 @@ let betree_node_5_apply_to_leaf_fwd_back
end
end
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+ (bindings : betree_list_t (u64 & u64))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+ =
+ begin match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl ->
+ let (i, m) = new_msg in
+ begin match betree_node_apply_to_leaf_fwd_back bindings i m with
+ | Fail -> Fail
+ | Return bindings0 ->
+ begin match
+ betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
+ | Fail -> Fail
+ | Return bindings1 -> Return bindings1
+ end
+ end
+ | BetreeListNil -> Return bindings
+ end
+
(** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
-let rec betree_node_5_filter_messages_for_key_fwd_back
+let rec betree_node_filter_messages_for_key_fwd_back
(key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_filter_messages_for_key_decreases key msgs))
+ (decreases (betree_node_filter_messages_for_key_decreases key msgs))
=
begin match msgs with
| BetreeListCons p l ->
@@ -931,12 +946,11 @@ let rec betree_node_5_filter_messages_for_key_fwd_back
if k = key
then
begin match
- betree_list_1_pop_front_back (u64 & betree_message_t) (BetreeListCons
- (k, m) l) with
+ betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
+ m) l) with
| Fail -> Fail
| Return msgs0 ->
- begin match betree_node_5_filter_messages_for_key_fwd_back key msgs0
- with
+ begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
| Fail -> Fail
| Return msgs1 -> Return msgs1
end
@@ -946,18 +960,18 @@ let rec betree_node_5_filter_messages_for_key_fwd_back
end
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
-let rec betree_node_5_lookup_first_message_after_key_fwd
+let rec betree_node_lookup_first_message_after_key_fwd
(key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_lookup_first_message_after_key_decreases key msgs))
+ (decreases (betree_node_lookup_first_message_after_key_decreases key msgs))
=
begin match msgs with
| BetreeListCons p next_msgs ->
let (k, m) = p in
if k = key
then
- begin match
- betree_node_5_lookup_first_message_after_key_fwd key next_msgs with
+ begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
+ with
| Fail -> Fail
| Return l -> Return l
end
@@ -966,11 +980,11 @@ let rec betree_node_5_lookup_first_message_after_key_fwd
end
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
-let rec betree_node_5_lookup_first_message_after_key_back
+let rec betree_node_lookup_first_message_after_key_back
(key : u64) (msgs : betree_list_t (u64 & betree_message_t))
(ret : betree_list_t (u64 & betree_message_t)) :
Tot (result (betree_list_t (u64 & betree_message_t)))
- (decreases (betree_node_5_lookup_first_message_after_key_decreases key msgs))
+ (decreases (betree_node_lookup_first_message_after_key_decreases key msgs))
=
begin match msgs with
| BetreeListCons p next_msgs ->
@@ -978,8 +992,7 @@ let rec betree_node_5_lookup_first_message_after_key_back
if k = key
then
begin match
- betree_node_5_lookup_first_message_after_key_back key next_msgs ret
- with
+ betree_node_lookup_first_message_after_key_back key next_msgs ret with
| Fail -> Fail
| Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
end
@@ -988,32 +1001,32 @@ let rec betree_node_5_lookup_first_message_after_key_back
end
(** [betree_main::betree::Node::{5}::apply_to_internal] *)
-let betree_node_5_apply_to_internal_fwd_back
+let betree_node_apply_to_internal_fwd_back
(msgs : betree_list_t (u64 & betree_message_t)) (key : u64)
(new_msg : betree_message_t) :
result (betree_list_t (u64 & betree_message_t))
=
- begin match betree_node_5_lookup_first_message_for_key_fwd key msgs with
+ begin match betree_node_lookup_first_message_for_key_fwd key msgs with
| Fail -> Fail
| Return msgs0 ->
- begin match betree_list_2_head_has_key_fwd betree_message_t msgs0 key with
+ begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
| Fail -> Fail
| Return b ->
if b
then
begin match new_msg with
| BetreeMessageInsert i ->
- begin match betree_node_5_filter_messages_for_key_fwd_back key msgs0
+ begin match betree_node_filter_messages_for_key_fwd_back key msgs0
with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t) msgs1
+ betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
(key, BetreeMessageInsert i) with
| Fail -> Fail
| Return msgs2 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs msgs2
+ betree_node_lookup_first_message_for_key_back key msgs msgs2
with
| Fail -> Fail
| Return msgs3 -> Return msgs3
@@ -1021,17 +1034,17 @@ let betree_node_5_apply_to_internal_fwd_back
end
end
| BetreeMessageDelete ->
- begin match betree_node_5_filter_messages_for_key_fwd_back key msgs0
+ begin match betree_node_filter_messages_for_key_fwd_back key msgs0
with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t) msgs1
+ betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
(key, BetreeMessageDelete) with
| Fail -> Fail
| Return msgs2 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs msgs2
+ betree_node_lookup_first_message_for_key_back key msgs msgs2
with
| Fail -> Fail
| Return msgs3 -> Return msgs3
@@ -1039,7 +1052,7 @@ let betree_node_5_apply_to_internal_fwd_back
end
end
| BetreeMessageUpsert s ->
- begin match betree_list_1_hd_fwd (u64 & betree_message_t) msgs0 with
+ begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
| Fail -> Fail
| Return p ->
let (_, m) = p in
@@ -1049,17 +1062,17 @@ let betree_node_5_apply_to_internal_fwd_back
| Fail -> Fail
| Return v ->
begin match
- betree_list_1_pop_front_back (u64 & betree_message_t) msgs0
+ betree_list_pop_front_back (u64 & betree_message_t) msgs0
with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t)
+ betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageInsert v) with
| Fail -> Fail
| Return msgs2 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
msgs2 with
| Fail -> Fail
| Return msgs3 -> Return msgs3
@@ -1072,17 +1085,17 @@ let betree_node_5_apply_to_internal_fwd_back
| Fail -> Fail
| Return v ->
begin match
- betree_list_1_pop_front_back (u64 & betree_message_t) msgs0
+ betree_list_pop_front_back (u64 & betree_message_t) msgs0
with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t)
+ betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageInsert v) with
| Fail -> Fail
| Return msgs2 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
msgs2 with
| Fail -> Fail
| Return msgs3 -> Return msgs3
@@ -1092,21 +1105,21 @@ let betree_node_5_apply_to_internal_fwd_back
end
| BetreeMessageUpsert ufs ->
begin match
- betree_node_5_lookup_first_message_after_key_fwd key msgs0 with
+ betree_node_lookup_first_message_after_key_fwd key msgs0 with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t)
+ betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageUpsert s) with
| Fail -> Fail
| Return msgs2 ->
begin match
- betree_node_5_lookup_first_message_after_key_back key msgs0
+ betree_node_lookup_first_message_after_key_back key msgs0
msgs2 with
| Fail -> Fail
| Return msgs3 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs
+ betree_node_lookup_first_message_for_key_back key msgs
msgs3 with
| Fail -> Fail
| Return msgs4 -> Return msgs4
@@ -1119,12 +1132,12 @@ let betree_node_5_apply_to_internal_fwd_back
end
else
begin match
- betree_list_1_push_front_fwd_back (u64 & betree_message_t) msgs0
- (key, new_msg) with
+ betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
+ new_msg) with
| Fail -> Fail
| Return msgs1 ->
begin match
- betree_node_5_lookup_first_message_for_key_back key msgs msgs1 with
+ betree_node_lookup_first_message_for_key_back key msgs msgs1 with
| Fail -> Fail
| Return msgs2 -> Return msgs2
end
@@ -1132,51 +1145,72 @@ let betree_node_5_apply_to_internal_fwd_back
end
end
+(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
+let rec betree_node_apply_messages_to_internal_fwd_back
+ (msgs : betree_list_t (u64 & betree_message_t))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) :
+ Tot (result (betree_list_t (u64 & betree_message_t)))
+ (decreases (betree_node_apply_messages_to_internal_decreases msgs new_msgs))
+ =
+ begin match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl ->
+ let (i, m) = new_msg in
+ begin match betree_node_apply_to_internal_fwd_back msgs i m with
+ | Fail -> Fail
+ | Return msgs0 ->
+ begin match
+ betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
+ | Fail -> Fail
+ | Return msgs1 -> Return msgs1
+ end
+ end
+ | BetreeListNil -> Return msgs
+ end
+
(** [betree_main::betree::Internal::{4}::flush] *)
-let rec betree_internal_4_flush_fwd
+let rec betree_internal_flush_fwd
(self : betree_internal_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (state & (betree_list_t (u64 & betree_message_t))))
- (decreases (betree_internal_4_flush_decreases self params node_id_cnt content
- st))
+ (decreases %[betree_internal_size self; 0])
+ //(decreases (betree_internal_flush_decreases self params node_id_cnt content st))
=
begin match
- betree_list_2_partition_at_pivot_fwd betree_message_t content
+ betree_list_partition_at_pivot_fwd betree_message_t content
self.betree_internal_pivot with
| Fail -> Fail
| Return p ->
let (msgs_left, msgs_right) = p in
- begin match betree_list_1_len_fwd (u64 & betree_message_t) msgs_left with
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
| Fail -> Fail
| Return len_left ->
if len_left >= params.betree_params_min_flush_size
then
begin match
- betree_node_5_apply_messages_fwd self.betree_internal_left params
+ betree_node_apply_messages_fwd self.betree_internal_left params
node_id_cnt msgs_left st with
| Fail -> Fail
| Return (st0, _) ->
begin match
- betree_node_5_apply_messages_back self.betree_internal_left params
+ betree_node_apply_messages_back self.betree_internal_left params
node_id_cnt msgs_left st with
| Fail -> Fail
| Return (_, node_id_cnt0) ->
- begin match
- betree_list_1_len_fwd (u64 & betree_message_t) msgs_right with
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+ with
| Fail -> Fail
| Return len_right ->
if len_right >= params.betree_params_min_flush_size
then
begin match
- betree_node_5_apply_messages_fwd self.betree_internal_right
+ betree_node_apply_messages_fwd self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
| Fail -> Fail
| Return (st1, _) ->
begin match
- betree_node_5_apply_messages_back
- self.betree_internal_right params node_id_cnt0 msgs_right
- st0 with
+ betree_node_apply_messages_back self.betree_internal_right
+ params node_id_cnt0 msgs_right st0 with
| Fail -> Fail
| Return (_, _) -> Return (st1, BetreeListNil)
end
@@ -1187,12 +1221,12 @@ let rec betree_internal_4_flush_fwd
end
else
begin match
- betree_node_5_apply_messages_fwd self.betree_internal_right params
+ betree_node_apply_messages_fwd self.betree_internal_right params
node_id_cnt msgs_right st with
| Fail -> Fail
| Return (st0, _) ->
begin match
- betree_node_5_apply_messages_back self.betree_internal_right params
+ betree_node_apply_messages_back self.betree_internal_right params
node_id_cnt msgs_right st with
| Fail -> Fail
| Return (_, _) -> Return (st0, msgs_left)
@@ -1202,43 +1236,43 @@ let rec betree_internal_4_flush_fwd
end
(** [betree_main::betree::Internal::{4}::flush] *)
-and betree_internal_4_flush_back
+and betree_internal_flush_back
(self : betree_internal_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (betree_internal_t & betree_node_id_counter_t))
- (decreases (betree_internal_4_flush_decreases self params node_id_cnt content
- st))
+ (decreases %[betree_internal_size self; 0])
+ //(decreases (betree_internal_flush_decreases self params node_id_cnt content st))
=
begin match
- betree_list_2_partition_at_pivot_fwd betree_message_t content
+ betree_list_partition_at_pivot_fwd betree_message_t content
self.betree_internal_pivot with
| Fail -> Fail
| Return p ->
let (msgs_left, msgs_right) = p in
- begin match betree_list_1_len_fwd (u64 & betree_message_t) msgs_left with
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
| Fail -> Fail
| Return len_left ->
if len_left >= params.betree_params_min_flush_size
then
begin match
- betree_node_5_apply_messages_fwd self.betree_internal_left params
+ betree_node_apply_messages_fwd self.betree_internal_left params
node_id_cnt msgs_left st with
| Fail -> Fail
| Return (st0, _) ->
begin match
- betree_node_5_apply_messages_back self.betree_internal_left params
+ betree_node_apply_messages_back self.betree_internal_left params
node_id_cnt msgs_left st with
| Fail -> Fail
| Return (n, node_id_cnt0) ->
- begin match
- betree_list_1_len_fwd (u64 & betree_message_t) msgs_right with
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+ with
| Fail -> Fail
| Return len_right ->
if len_right >= params.betree_params_min_flush_size
then
begin match
- betree_node_5_apply_messages_back self.betree_internal_right
+ betree_node_apply_messages_back self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
| Fail -> Fail
| Return (n0, node_id_cnt1) ->
@@ -1254,7 +1288,7 @@ and betree_internal_4_flush_back
end
else
begin match
- betree_node_5_apply_messages_back self.betree_internal_right params
+ betree_node_apply_messages_back self.betree_internal_right params
node_id_cnt msgs_right st with
| Fail -> Fail
| Return (n, node_id_cnt0) ->
@@ -1266,104 +1300,37 @@ and betree_internal_4_flush_back
end
(** [betree_main::betree::Node::{5}::apply_messages] *)
-and betree_node_5_apply_messages_fwd
- (self : betree_node_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
- Tot (result (state & unit))
- (decreases (betree_node_5_apply_messages_decreases self params node_id_cnt
- msgs st))
- =
- begin match msgs with
- | BetreeListCons p msgs0 ->
- let (key, msg) = p in
- begin match betree_node_5_apply_fwd self params node_id_cnt key msg st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match betree_node_5_apply_back self params node_id_cnt key msg st
- with
- | Fail -> Fail
- | Return (self0, node_id_cnt0) ->
- begin match
- betree_node_5_apply_messages_fwd self0 params node_id_cnt0 msgs0 st0
- with
- | Fail -> Fail
- | Return (st1, _) ->
- begin match
- betree_node_5_apply_messages_back self0 params node_id_cnt0 msgs0
- st0 with
- | Fail -> Fail
- | Return (_, _) -> Return (st1, ())
- end
- end
- end
- end
- | BetreeListNil -> Return (st, ())
- end
-
-(** [betree_main::betree::Node::{5}::apply_messages] *)
-and betree_node_5_apply_messages_back
+and betree_node_apply_messages_fwd
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
- Tot (result (betree_node_t & betree_node_id_counter_t))
- (decreases (betree_node_5_apply_messages_decreases self params node_id_cnt
- msgs st))
- =
- begin match msgs with
- | BetreeListCons p msgs0 ->
- let (key, msg) = p in
- begin match betree_node_5_apply_fwd self params node_id_cnt key msg st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match betree_node_5_apply_back self params node_id_cnt key msg st
- with
- | Fail -> Fail
- | Return (self0, node_id_cnt0) ->
- begin match
- betree_node_5_apply_messages_back self0 params node_id_cnt0 msgs0 st0
- with
- | Fail -> Fail
- | Return (self1, node_id_cnt1) -> Return (self1, node_id_cnt1)
- end
- end
- end
- | BetreeListNil -> Return (self, node_id_cnt)
- end
-
-(** [betree_main::betree::Node::{5}::apply] *)
-and betree_node_5_apply_fwd
- (self : betree_node_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t) (key : u64)
- (new_msg : betree_message_t) (st : state) :
Tot (result (state & unit))
- (decreases (betree_node_5_apply_decreases self params node_id_cnt key new_msg
- st))
+ (decreases %[betree_size self; betree_list_len msgs])
+// (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs st))
=
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
| Fail -> Fail
| Return (st0, content) ->
- begin match betree_node_5_apply_to_internal_fwd_back content key new_msg
+ begin match betree_node_apply_messages_to_internal_fwd_back content msgs
with
| Fail -> Fail
| Return content0 ->
- begin match betree_list_1_len_fwd (u64 & betree_message_t) content0
- with
+ begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
| Fail -> Fail
| Return num_msgs ->
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- betree_internal_4_flush_fwd (Mkbetree_internal_t
+ betree_internal_flush_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) params
node_id_cnt content0 st0 with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- betree_internal_4_flush_back (Mkbetree_internal_t
+ betree_internal_flush_back (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) params
node_id_cnt content0 st0 with
@@ -1391,10 +1358,10 @@ and betree_node_5_apply_fwd
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
| Fail -> Fail
| Return (st0, content) ->
- begin match betree_node_5_apply_to_leaf_fwd_back content key new_msg with
+ begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
| Fail -> Fail
| Return content0 ->
- begin match betree_list_1_len_fwd (u64 & u64) content0 with
+ begin match betree_list_len_fwd (u64 & u64) content0 with
| Fail -> Fail
| Return len ->
begin match u64_mul 2 params.betree_params_split_size with
@@ -1403,7 +1370,7 @@ and betree_node_5_apply_fwd
if len >= i
then
begin match
- betree_leaf_3_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
+ betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
node.betree_leaf_size) content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, _) ->
@@ -1427,39 +1394,38 @@ and betree_node_5_apply_fwd
end
end
-(** [betree_main::betree::Node::{5}::apply] *)
-and betree_node_5_apply_back
+(** [betree_main::betree::Node::{5}::apply_messages] *)
+and betree_node_apply_messages_back
(self : betree_node_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t) (key : u64)
- (new_msg : betree_message_t) (st : state) :
+ (node_id_cnt : betree_node_id_counter_t)
+ (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (betree_node_t & betree_node_id_counter_t))
- (decreases (betree_node_5_apply_decreases self params node_id_cnt key new_msg
- st))
+ (decreases %[betree_size self; betree_list_len msgs])
+// (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs st))
=
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
| Fail -> Fail
| Return (st0, content) ->
- begin match betree_node_5_apply_to_internal_fwd_back content key new_msg
+ begin match betree_node_apply_messages_to_internal_fwd_back content msgs
with
| Fail -> Fail
| Return content0 ->
- begin match betree_list_1_len_fwd (u64 & betree_message_t) content0
- with
+ begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
| Fail -> Fail
| Return num_msgs ->
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- betree_internal_4_flush_fwd (Mkbetree_internal_t
+ betree_internal_flush_fwd (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) params
node_id_cnt content0 st0 with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- betree_internal_4_flush_back (Mkbetree_internal_t
+ betree_internal_flush_back (Mkbetree_internal_t
node.betree_internal_id node.betree_internal_pivot
node.betree_internal_left node.betree_internal_right) params
node_id_cnt content0 st0 with
@@ -1495,10 +1461,10 @@ and betree_node_5_apply_back
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
| Fail -> Fail
| Return (st0, content) ->
- begin match betree_node_5_apply_to_leaf_fwd_back content key new_msg with
+ begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
| Fail -> Fail
| Return content0 ->
- begin match betree_list_1_len_fwd (u64 & u64) content0 with
+ begin match betree_list_len_fwd (u64 & u64) content0 with
| Fail -> Fail
| Return len ->
begin match u64_mul 2 params.betree_params_split_size with
@@ -1507,7 +1473,7 @@ and betree_node_5_apply_back
if len >= i
then
begin match
- betree_leaf_3_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
+ betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
node.betree_leaf_size) content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, new_node) ->
@@ -1517,9 +1483,9 @@ and betree_node_5_apply_back
| Fail -> Fail
| Return (_, _) ->
begin match
- betree_leaf_3_split_back (Mkbetree_leaf_t
- node.betree_leaf_id node.betree_leaf_size) content0
- params node_id_cnt st0 with
+ betree_leaf_split_back (Mkbetree_leaf_t node.betree_leaf_id
+ node.betree_leaf_size) content0 params node_id_cnt st0
+ with
| Fail -> Fail
| Return node_id_cnt0 ->
Return (BetreeNodeInternal new_node, node_id_cnt0)
@@ -1541,8 +1507,44 @@ and betree_node_5_apply_back
end
end
+(** [betree_main::betree::Node::{5}::apply] *)
+let betree_node_apply_fwd
+ (self : betree_node_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t) (key : u64)
+ (new_msg : betree_message_t) (st : state) :
+ result (state & unit)
+ =
+ let l = BetreeListNil in
+ begin match
+ betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
+ (key, new_msg) l) st with
+ | Fail -> Fail
+ | Return (st0, _) ->
+ begin match
+ betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
+ (key, new_msg) l) st with
+ | Fail -> Fail
+ | Return (_, _) -> Return (st0, ())
+ end
+ end
+
+(** [betree_main::betree::Node::{5}::apply] *)
+let betree_node_apply_back
+ (self : betree_node_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t) (key : u64)
+ (new_msg : betree_message_t) (st : state) :
+ result (betree_node_t & betree_node_id_counter_t)
+ =
+ let l = BetreeListNil in
+ begin match
+ betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
+ (key, new_msg) l) st with
+ | Fail -> Fail
+ | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0)
+ end
+
(** [betree_main::betree::BeTree::{6}::new] *)
-let betree_be_tree_6_new_fwd
+let betree_be_tree_new_fwd
(min_flush_size : u64) (split_size : u64) (st : state) :
result (state & betree_be_tree_t)
=
@@ -1566,17 +1568,17 @@ let betree_be_tree_6_new_fwd
end
(** [betree_main::betree::BeTree::{6}::apply] *)
-let betree_be_tree_6_apply_fwd
+let betree_be_tree_apply_fwd
(self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) :
result (state & unit)
=
begin match
- betree_node_5_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
+ betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
self.betree_be_tree_node_id_cnt key msg st with
| Fail -> Fail
| Return (st0, _) ->
begin match
- betree_node_5_apply_back self.betree_be_tree_root
+ betree_node_apply_back self.betree_be_tree_root
self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
with
| Fail -> Fail
@@ -1585,114 +1587,112 @@ let betree_be_tree_6_apply_fwd
end
(** [betree_main::betree::BeTree::{6}::apply] *)
-let betree_be_tree_6_apply_back
+let betree_be_tree_apply_back
(self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) :
result betree_be_tree_t
=
begin match
- betree_node_5_apply_back self.betree_be_tree_root
- self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
- with
+ betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params
+ self.betree_be_tree_node_id_cnt key msg st with
| Fail -> Fail
| Return (n, nic) ->
Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
end
(** [betree_main::betree::BeTree::{6}::insert] *)
-let betree_be_tree_6_insert_fwd
+let betree_be_tree_insert_fwd
(self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
result (state & unit)
=
- begin match
- betree_be_tree_6_apply_fwd self key (BetreeMessageInsert value) st with
+ begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
+ with
| Fail -> Fail
| Return (st0, _) ->
begin match
- betree_be_tree_6_apply_back self key (BetreeMessageInsert value) st with
+ betree_be_tree_apply_back self key (BetreeMessageInsert value) st with
| Fail -> Fail
| Return _ -> Return (st0, ())
end
end
(** [betree_main::betree::BeTree::{6}::insert] *)
-let betree_be_tree_6_insert_back
+let betree_be_tree_insert_back
(self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
result betree_be_tree_t
=
- begin match
- betree_be_tree_6_apply_back self key (BetreeMessageInsert value) st with
+ begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st
+ with
| Fail -> Fail
| Return self0 -> Return self0
end
(** [betree_main::betree::BeTree::{6}::delete] *)
-let betree_be_tree_6_delete_fwd
+let betree_be_tree_delete_fwd
(self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
- begin match betree_be_tree_6_apply_fwd self key BetreeMessageDelete st with
+ begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
| Fail -> Fail
| Return (st0, _) ->
- begin match betree_be_tree_6_apply_back self key BetreeMessageDelete st
- with
+ begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
| Fail -> Fail
| Return _ -> Return (st0, ())
end
end
(** [betree_main::betree::BeTree::{6}::delete] *)
-let betree_be_tree_6_delete_back
+let betree_be_tree_delete_back
(self : betree_be_tree_t) (key : u64) (st : state) :
result betree_be_tree_t
=
- begin match betree_be_tree_6_apply_back self key BetreeMessageDelete st with
+ begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
| Fail -> Fail
| Return self0 -> Return self0
end
(** [betree_main::betree::BeTree::{6}::upsert] *)
-let betree_be_tree_6_upsert_fwd
+let betree_be_tree_upsert_fwd
(self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
(st : state) :
result (state & unit)
=
- begin match betree_be_tree_6_apply_fwd self key (BetreeMessageUpsert upd) st
+ begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
with
| Fail -> Fail
| Return (st0, _) ->
- begin match
- betree_be_tree_6_apply_back self key (BetreeMessageUpsert upd) st with
+ begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
+ with
| Fail -> Fail
| Return _ -> Return (st0, ())
end
end
(** [betree_main::betree::BeTree::{6}::upsert] *)
-let betree_be_tree_6_upsert_back
+let betree_be_tree_upsert_back
(self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
(st : state) :
result betree_be_tree_t
=
- begin match betree_be_tree_6_apply_back self key (BetreeMessageUpsert upd) st
+ begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
with
| Fail -> Fail
| Return self0 -> Return self0
end
(** [betree_main::betree::BeTree::{6}::lookup] *)
-let betree_be_tree_6_lookup_fwd
+let betree_be_tree_lookup_fwd
(self : betree_be_tree_t) (key : u64) (st : state) :
result (state & (option u64))
=
- begin match betree_node_5_lookup_fwd self.betree_be_tree_root key st with
+ begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
| Fail -> Fail
| Return (st0, opt) -> Return (st0, opt)
end
(** [betree_main::betree::BeTree::{6}::lookup] *)
-let betree_be_tree_6_lookup_back
+let betree_be_tree_lookup_back
(self : betree_be_tree_t) (key : u64) (st : state) :
result betree_be_tree_t
=
- begin match betree_node_5_lookup_back self.betree_be_tree_root key st with
+ begin match betree_node_lookup_back self.betree_be_tree_root key st with
| Fail -> Fail
| Return n ->
Return (Mkbetree_be_tree_t self.betree_be_tree_params