summaryrefslogtreecommitdiff
path: root/tests/coq/betree
diff options
context:
space:
mode:
authorSon Ho2022-12-17 12:55:40 +0100
committerSon HO2023-02-03 11:21:46 +0100
commitacdfede396a36723258e0a6d7b264cec9ca99672 (patch)
tree9ac729846efb96491bb35e03aca7d8796f50285d /tests/coq/betree
parent01a95c7da8cc0c937d94e6a9bc753d2ceb163c17 (diff)
Regenerate the files
Diffstat (limited to 'tests/coq/betree')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v133
1 files changed, 38 insertions, 95 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index ddcff646..004db30e 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -15,9 +15,7 @@ Definition betree_load_internal_node_fwd
(id : u64) (st : state) :
result (state * (Betree_list_t (u64 * Betree_message_t)))
:=
- p <- betree_utils_load_internal_node_fwd id st;
- let (st0, l) := p in
- Return (st0, l)
+ betree_utils_load_internal_node_fwd id st
.
(** [betree_main::betree::store_internal_node] *)
@@ -33,9 +31,7 @@ Definition betree_store_internal_node_fwd
(** [betree_main::betree::load_leaf_node] *)
Definition betree_load_leaf_node_fwd
(id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) :=
- p <- betree_utils_load_leaf_node_fwd id st;
- let (st0, l) := p in
- Return (st0, l)
+ betree_utils_load_leaf_node_fwd id st
.
(** [betree_main::betree::store_leaf_node] *)
@@ -55,7 +51,7 @@ Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
(** [betree_main::betree::fresh_node_id] *)
Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
- counter0 <- u64_add counter 1%u64; Return counter0
+ u64_add counter 1%u64
.
(** [betree_main::betree::NodeIdCounter::{0}::new] *)
@@ -97,11 +93,9 @@ Definition betree_upsert_update_fwd
match st with
| BetreeUpsertFunStateAdd v =>
margin <- u64_sub core_num_u64_max_c prev0;
- if margin s>= v
- then (i <- u64_add prev0 v; Return i)
- else Return core_num_u64_max_c
+ if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
| BetreeUpsertFunStateSub v =>
- if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64)
+ if prev0 s>= v then u64_sub prev0 v else Return (0%u64)
end
end
.
@@ -113,8 +107,7 @@ Fixpoint betree_list_len_fwd
| O => Fail_ OutOfFuel
| S n0 =>
match self with
- | BetreeListCons t tl =>
- i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0
+ | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i
| BetreeListNil => Return (0%u64)
end
end
@@ -258,8 +251,7 @@ Definition betree_leaf_split_back
let (st0, _) := p1 in
p2 <- betree_store_leaf_node_fwd id1 content1 st0;
let (_, _) := p2 in
- node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
- Return node_id_cnt1
+ betree_node_id_counter_fresh_id_back node_id_cnt0
.
(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
@@ -278,7 +270,7 @@ Fixpoint betree_node_lookup_in_bindings_fwd
else
if i s> key
then Return None
- else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt)
+ else betree_node_lookup_in_bindings_fwd n0 key tl
| BetreeListNil => Return None
end
end
@@ -297,9 +289,7 @@ Fixpoint betree_node_lookup_first_message_for_key_fwd
let (i, m) := x in
if i s>= key
then Return (BetreeListCons (i, m) next_msgs)
- else (
- l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs;
- Return l)
+ else betree_node_lookup_first_message_for_key_fwd n0 key next_msgs
| BetreeListNil => Return BetreeListNil
end
end
@@ -348,9 +338,7 @@ Fixpoint betree_node_apply_upserts_fwd
| BetreeMessageUpsert s =>
v <- betree_upsert_update_fwd prev s;
msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
- p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st;
- let (st0, i) := p in
- Return (st0, i)
+ betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st
end)
else (
p <- core_option_option_unwrap_fwd u64 prev st;
@@ -383,16 +371,13 @@ Fixpoint betree_node_apply_upserts_back
| BetreeMessageUpsert s =>
v <- betree_upsert_update_fwd prev s;
msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
- msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st;
- Return msgs1
+ betree_node_apply_upserts_back n0 msgs0 (Some v) key st
end)
else (
p <- core_option_option_unwrap_fwd u64 prev st;
let (_, v) := p in
- msgs0 <-
- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
- BetreeMessageInsert v);
- Return msgs0)
+ betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
+ BetreeMessageInsert v))
end
.
@@ -556,14 +541,8 @@ with betree_internal_lookup_in_children_fwd
| O => Fail_ OutOfFuel
| S n0 =>
if key s< self.(Betree_internal_pivot)
- then (
- p <- betree_node_lookup_fwd n0 self.(Betree_internal_left) key st;
- let (st0, opt) := p in
- Return (st0, opt))
- else (
- p <- betree_node_lookup_fwd n0 self.(Betree_internal_right) key st;
- let (st0, opt) := p in
- Return (st0, opt))
+ then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
+ else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
end
(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
@@ -599,7 +578,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_fwd
let (i, i0) := hd in
if i s>= key
then Return (BetreeListCons (i, i0) tl)
- else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l)
+ else betree_node_lookup_mut_in_bindings_fwd n0 key tl
| BetreeListNil => Return BetreeListNil
end
end
@@ -643,43 +622,31 @@ Definition betree_node_apply_to_leaf_fwd_back
bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
bindings2 <-
betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- bindings3 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
- Return bindings3
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
| BetreeMessageDelete =>
bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- bindings2 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
- Return bindings2
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
| BetreeMessageUpsert s =>
let (_, i) := hd in
v <- betree_upsert_update_fwd (Some i) s;
bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
bindings2 <-
betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- bindings3 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
- Return bindings3
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
end)
else
match new_msg with
| BetreeMessageInsert v =>
bindings1 <-
betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- bindings2 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
- Return bindings2
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
| BetreeMessageDelete =>
- bindings1 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings0;
- Return bindings1
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings0
| BetreeMessageUpsert s =>
v <- betree_upsert_update_fwd None s;
bindings1 <-
betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- bindings2 <-
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
- Return bindings2
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
end
.
@@ -696,9 +663,7 @@ Fixpoint betree_node_apply_messages_to_leaf_fwd_back
| BetreeListCons new_msg new_msgs_tl =>
let (i, m) := new_msg in
bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
- bindings1 <-
- betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl;
- Return bindings1
+ betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
| BetreeListNil => Return bindings
end
end
@@ -720,8 +685,7 @@ Fixpoint betree_node_filter_messages_for_key_fwd_back
msgs0 <-
betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons
(k, m) l);
- msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
- Return msgs1)
+ betree_node_filter_messages_for_key_fwd_back n0 key msgs0)
else Return (BetreeListCons (k, m) l)
| BetreeListNil => Return BetreeListNil
end
@@ -740,9 +704,7 @@ Fixpoint betree_node_lookup_first_message_after_key_fwd
| BetreeListCons p next_msgs =>
let (k, m) := p in
if k s= key
- then (
- l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs;
- Return l)
+ then betree_node_lookup_first_message_after_key_fwd n0 key next_msgs
else Return (BetreeListCons (k, m) next_msgs)
| BetreeListNil => Return BetreeListNil
end
@@ -788,15 +750,13 @@ Definition betree_node_apply_to_internal_fwd_back
msgs2 <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
BetreeMessageInsert i);
- msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
- Return msgs3
+ betree_node_lookup_first_message_for_key_back n key msgs msgs2
| BetreeMessageDelete =>
msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
msgs2 <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
BetreeMessageDelete);
- msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
- Return msgs3
+ betree_node_lookup_first_message_for_key_back n key msgs msgs2
| BetreeMessageUpsert s =>
p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0;
let (_, m) := p in
@@ -807,18 +767,14 @@ Definition betree_node_apply_to_internal_fwd_back
msgs2 <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
BetreeMessageInsert v);
- msgs3 <-
- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
- Return msgs3
+ betree_node_lookup_first_message_for_key_back n key msgs msgs2
| BetreeMessageDelete =>
v <- betree_upsert_update_fwd None s;
msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
msgs2 <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
BetreeMessageInsert v);
- msgs3 <-
- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
- Return msgs3
+ betree_node_lookup_first_message_for_key_back n key msgs msgs2
| BetreeMessageUpsert ufs =>
msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0;
msgs2 <-
@@ -826,17 +782,14 @@ Definition betree_node_apply_to_internal_fwd_back
BetreeMessageUpsert s);
msgs3 <-
betree_node_lookup_first_message_after_key_back n key msgs0 msgs2;
- msgs4 <-
- betree_node_lookup_first_message_for_key_back n key msgs msgs3;
- Return msgs4
+ betree_node_lookup_first_message_for_key_back n key msgs msgs3
end
end
else (
msgs1 <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
new_msg);
- msgs2 <- betree_node_lookup_first_message_for_key_back n key msgs msgs1;
- Return msgs2)
+ betree_node_lookup_first_message_for_key_back n key msgs msgs1)
.
(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
@@ -852,9 +805,7 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
| BetreeListCons new_msg new_msgs_tl =>
let (i, m) := new_msg in
msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m;
- msgs1 <-
- betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl;
- Return msgs1
+ betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl
| BetreeListNil => Return msgs
end
end
@@ -1101,11 +1052,8 @@ Definition betree_node_apply_back
result (Betree_node_t * Betree_node_id_counter_t)
:=
let l := BetreeListNil in
- p <-
- betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
- (key, new_msg) l) st;
- let (self0, node_id_cnt0) := p in
- Return (self0, node_id_cnt0)
+ betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
+ (key, new_msg) l) st
.
(** [betree_main::betree::BeTree::{6}::new] *)
@@ -1169,8 +1117,7 @@ Definition betree_be_tree_insert_back
(n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
result Betree_be_tree_t
:=
- self0 <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
- Return self0
+ betree_be_tree_apply_back n self key (BetreeMessageInsert value) st
.
(** [betree_main::betree::BeTree::{6}::delete] *)
@@ -1190,8 +1137,7 @@ Definition betree_be_tree_delete_back
(n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
result Betree_be_tree_t
:=
- self0 <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
- Return self0
+ betree_be_tree_apply_back n self key BetreeMessageDelete st
.
(** [betree_main::betree::BeTree::{6}::upsert] *)
@@ -1213,8 +1159,7 @@ Definition betree_be_tree_upsert_back
(upd : Betree_upsert_fun_state_t) (st : state) :
result Betree_be_tree_t
:=
- self0 <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
- Return self0
+ betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st
.
(** [betree_main::betree::BeTree::{6}::lookup] *)
@@ -1222,9 +1167,7 @@ Definition betree_be_tree_lookup_fwd
(n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
result (state * (option u64))
:=
- p <- betree_node_lookup_fwd n self.(Betree_be_tree_root) key st;
- let (st0, opt) := p in
- Return (st0, opt)
+ betree_node_lookup_fwd n self.(Betree_be_tree_root) key st
.
(** [betree_main::betree::BeTree::{6}::lookup] *)