summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v81
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst22
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst38
3 files changed, 56 insertions, 85 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 004db30e..10cdedd1 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -46,7 +46,7 @@ Definition betree_store_leaf_node_fwd
(** [betree_main::betree::fresh_node_id] *)
Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
- i <- u64_add counter 1%u64; let _ := i in Return counter
+ _ <- u64_add counter 1%u64; Return counter
.
(** [betree_main::betree::fresh_node_id] *)
@@ -62,8 +62,7 @@ Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
Definition betree_node_id_counter_fresh_id_fwd
(self : Betree_node_id_counter_t) : result u64 :=
- i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
- let _ := i in
+ _ <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
Return self.(Betree_node_id_counter_next_node_id)
.
@@ -242,15 +241,13 @@ Definition betree_leaf_split_back
betree_list_split_at_fwd (u64 * u64) n content
params.(Betree_params_split_size);
let (content0, content1) := p in
- p0 <- betree_list_hd_fwd (u64 * u64) content1;
- let _ := p0 in
+ _ <- betree_list_hd_fwd (u64 * u64) content1;
id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
- p1 <- betree_store_leaf_node_fwd id0 content0 st;
- let (st0, _) := p1 in
- p2 <- betree_store_leaf_node_fwd id1 content1 st0;
- let (_, _) := p2 in
+ p0 <- betree_store_leaf_node_fwd id0 content0 st;
+ let (st0, _) := p0 in
+ _ <- betree_store_leaf_node_fwd id1 content1 st0;
betree_node_id_counter_fresh_id_back node_id_cnt0
.
@@ -343,10 +340,9 @@ Fixpoint betree_node_apply_upserts_fwd
else (
p <- core_option_option_unwrap_fwd u64 prev st;
let (st0, v) := p in
- l <-
+ _ <-
betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
BetreeMessageInsert v);
- let _ := l in
Return (st0, v))
end
.
@@ -401,24 +397,21 @@ Fixpoint betree_node_lookup_fwd
then (
p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
let (st1, opt) := p1 in
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, msg) l);
- let _ := l0 in
Return (st1, opt))
else
match msg with
| BetreeMessageInsert v =>
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, BetreeMessageInsert v) l);
- let _ := l0 in
Return (st0, Some v)
| BetreeMessageDelete =>
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, BetreeMessageDelete) l);
- let _ := l0 in
Return (st0, None)
| BetreeMessageUpsert ufs =>
p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
@@ -443,10 +436,9 @@ Fixpoint betree_node_lookup_fwd
| BetreeListNil =>
p0 <- betree_internal_lookup_in_children_fwd n0 node key st0;
let (st1, opt) := p0 in
- l <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
BetreeListNil;
- let _ := l in
Return (st1, opt)
end
| BetreeNodeLeaf node =>
@@ -475,25 +467,22 @@ with betree_node_lookup_back
let (k, msg) := p0 in
if k s<> key
then (
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, msg) l);
- let _ := l0 in
node0 <- betree_internal_lookup_in_children_back n0 node key st0;
Return (BetreeNodeInternal node0))
else
match msg with
| BetreeMessageInsert v =>
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, BetreeMessageInsert v) l);
- let _ := l0 in
Return (BetreeNodeInternal node)
| BetreeMessageDelete =>
- l0 <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
(BetreeListCons (k, BetreeMessageDelete) l);
- let _ := l0 in
Return (BetreeNodeInternal node)
| BetreeMessageUpsert ufs =>
p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
@@ -509,25 +498,22 @@ with betree_node_lookup_back
msgs0 <-
betree_node_lookup_first_message_for_key_back n0 key msgs
pending0;
- p3 <-
+ _ <-
betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
st2;
- let (_, _) := p3 in
Return (BetreeNodeInternal node0)
end
| BetreeListNil =>
- l <-
+ _ <-
betree_node_lookup_first_message_for_key_back n0 key msgs
BetreeListNil;
- let _ := l in
node0 <- betree_internal_lookup_in_children_back n0 node key st0;
Return (BetreeNodeInternal node0)
end
| BetreeNodeLeaf node =>
p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
let (_, bindings) := p in
- opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
- let _ := opt in
+ _ <- betree_node_lookup_in_bindings_fwd n0 key bindings;
Return (BetreeNodeLeaf node)
end
end
@@ -892,15 +878,13 @@ with betree_node_apply_messages_back
p1 <-
betree_internal_flush_back n0 node params node_id_cnt content0 st0;
let (node0, node_id_cnt0) := p1 in
- p2 <-
+ _ <-
betree_store_internal_node_fwd node0.(Betree_internal_id) content1
st1;
- let (_, _) := p2 in
Return (BetreeNodeInternal node0, node_id_cnt0))
else (
- p0 <-
+ _ <-
betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
- let (_, _) := p0 in
Return (BetreeNodeInternal node, node_id_cnt))
| BetreeNodeLeaf node =>
p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
@@ -912,15 +896,13 @@ with betree_node_apply_messages_back
then (
p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0;
let (st1, new_node) := p0 in
- p1 <-
+ _ <-
betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
- let (_, _) := p1 in
node_id_cnt0 <-
betree_leaf_split_back n0 node content0 params node_id_cnt st0;
Return (BetreeNodeInternal new_node, node_id_cnt0))
else (
- p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
- let (_, _) := p0 in
+ _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len),
node_id_cnt))
end
@@ -958,10 +940,9 @@ with betree_internal_flush_fwd
betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
node_id_cnt0 msgs_right st0;
let (st1, _) := p2 in
- p3 <-
+ _ <-
betree_node_apply_messages_back n0 self.(Betree_internal_right)
params node_id_cnt0 msgs_right st0;
- let (_, _) := p3 in
Return (st1, BetreeListNil))
else Return (st0, msgs_right))
else (
@@ -969,10 +950,9 @@ with betree_internal_flush_fwd
betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
node_id_cnt msgs_right st;
let (st0, _) := p0 in
- p1 <-
+ _ <-
betree_node_apply_messages_back n0 self.(Betree_internal_right) params
node_id_cnt msgs_right st;
- let (_, _) := p1 in
Return (st0, msgs_left))
end
@@ -1037,10 +1017,9 @@ Definition betree_node_apply_fwd
betree_node_apply_messages_fwd n self params node_id_cnt (BetreeListCons
(key, new_msg) l) st;
let (st0, _) := p in
- p0 <-
+ _ <-
betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
(key, new_msg) l) st;
- let (_, _) := p0 in
Return (st0, tt)
.
@@ -1080,10 +1059,9 @@ Definition betree_be_tree_apply_fwd
betree_node_apply_fwd n self.(Betree_be_tree_root)
self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
let (st0, _) := p in
- p0 <-
+ _ <-
betree_node_apply_back n self.(Betree_be_tree_root)
self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
- let (_, _) := p0 in
Return (st0, tt)
.
@@ -1107,8 +1085,7 @@ Definition betree_be_tree_insert_fwd
:=
p <- betree_be_tree_apply_fwd n self key (BetreeMessageInsert value) st;
let (st0, _) := p in
- bt <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
- let _ := bt in
+ _ <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
Return (st0, tt)
.
@@ -1127,8 +1104,7 @@ Definition betree_be_tree_delete_fwd
:=
p <- betree_be_tree_apply_fwd n self key BetreeMessageDelete st;
let (st0, _) := p in
- bt <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
- let _ := bt in
+ _ <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
Return (st0, tt)
.
@@ -1148,8 +1124,7 @@ Definition betree_be_tree_upsert_fwd
:=
p <- betree_be_tree_apply_fwd n self key (BetreeMessageUpsert upd) st;
let (st0, _) := p in
- bt <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
- let _ := bt in
+ _ <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
Return (st0, tt)
.
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 628eb2c3..854862b2 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -272,8 +272,7 @@ let betree_leaf_split_back
| Return (st0, _) ->
begin match betree_store_leaf_node_fwd id1 content1 st0 with
| Fail e -> Fail e
- | Return (_, _) ->
- betree_node_id_counter_fresh_id_back node_id_cnt0
+ | Return _ -> betree_node_id_counter_fresh_id_back node_id_cnt0
end
end
end
@@ -603,7 +602,7 @@ and betree_node_lookup_back
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st2 with
| Fail e -> Fail e
- | Return (_, _) -> Return (BetreeNodeInternal node0)
+ | Return _ -> Return (BetreeNodeInternal node0)
end
end
end
@@ -1126,8 +1125,7 @@ and betree_node_apply_messages_back
betree_store_internal_node_fwd node0.betree_internal_id
content1 st1 with
| Fail e -> Fail e
- | Return (_, _) ->
- Return (BetreeNodeInternal node0, node_id_cnt0)
+ | Return _ -> Return (BetreeNodeInternal node0, node_id_cnt0)
end
end
end
@@ -1136,7 +1134,7 @@ and betree_node_apply_messages_back
betree_store_internal_node_fwd node.betree_internal_id content0
st0 with
| Fail e -> Fail e
- | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
+ | Return _ -> Return (BetreeNodeInternal node, node_id_cnt)
end
end
end
@@ -1164,7 +1162,7 @@ and betree_node_apply_messages_back
betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
st1 with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
begin match
betree_leaf_split_back node content0 params node_id_cnt st0
with
@@ -1179,7 +1177,7 @@ and betree_node_apply_messages_back
betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
len), node_id_cnt)
end
@@ -1234,7 +1232,7 @@ and betree_internal_flush_fwd
betree_node_apply_messages_back self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
| Fail e -> Fail e
- | Return (_, _) -> Return (st1, BetreeListNil)
+ | Return _ -> Return (st1, BetreeListNil)
end
end
else Return (st0, msgs_right)
@@ -1251,7 +1249,7 @@ and betree_internal_flush_fwd
betree_node_apply_messages_back self.betree_internal_right params
node_id_cnt msgs_right st with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, msgs_left)
+ | Return _ -> Return (st0, msgs_left)
end
end
end
@@ -1338,7 +1336,7 @@ let betree_node_apply_fwd
betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
(key, new_msg) l) st with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
@@ -1392,7 +1390,7 @@ let betree_be_tree_apply_fwd
self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 01fc457e..2a336271 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -311,7 +311,7 @@ let betree_leaf_split_back1
| Return (st1, _) ->
begin match betree_store_leaf_node_fwd id1 content1 st1 with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -350,7 +350,7 @@ let betree_leaf_split_back2
| Return (st1, _) ->
begin match betree_store_leaf_node_fwd id1 content1 st1 with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
begin match betree_node_id_counter_fresh_id_back node_id_cnt0
with
| Fail e -> Fail e
@@ -691,8 +691,7 @@ and betree_node_lookup_back
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st5 with
| Fail e -> Fail e
- | Return (_, _) ->
- Return (st0, BetreeNodeInternal node0)
+ | Return _ -> Return (st0, BetreeNodeInternal node0)
end
end
end
@@ -1219,7 +1218,7 @@ and betree_node_apply_messages_back'a
betree_store_internal_node_fwd node0.betree_internal_id
content1 st3 with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
end
end
@@ -1229,8 +1228,7 @@ and betree_node_apply_messages_back'a
betree_store_internal_node_fwd node.betree_internal_id content0
st1 with
| Fail e -> Fail e
- | Return (_, _) ->
- Return (st0, (BetreeNodeInternal node, node_id_cnt))
+ | Return _ -> Return (st0, (BetreeNodeInternal node, node_id_cnt))
end
end
end
@@ -1263,7 +1261,7 @@ and betree_node_apply_messages_back'a
betree_leaf_split_back0 node content0 params node_id_cnt
st1 st3 with
| Fail e -> Fail e
- | Return (_, ()) ->
+ | Return _ ->
begin match
betree_leaf_split_back2 node content0 params node_id_cnt
st1 st0 with
@@ -1279,7 +1277,7 @@ and betree_node_apply_messages_back'a
betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t
node.betree_leaf_id len), node_id_cnt))
end
@@ -1326,7 +1324,7 @@ and betree_node_apply_messages_back1
betree_store_internal_node_fwd node0.betree_internal_id
content1 st3 with
| Fail e -> Fail e
- | Return (_, _) ->
+ | Return _ ->
betree_internal_flush_back1 node params node_id_cnt content0
st1 st0
end
@@ -1337,7 +1335,7 @@ and betree_node_apply_messages_back1
betree_store_internal_node_fwd node.betree_internal_id content0
st1 with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -1370,7 +1368,7 @@ and betree_node_apply_messages_back1
betree_leaf_split_back0 node content0 params node_id_cnt
st1 st3 with
| Fail e -> Fail e
- | Return (_, ()) ->
+ | Return _ ->
betree_leaf_split_back1 node content0 params node_id_cnt
st1 st0
end
@@ -1381,7 +1379,7 @@ and betree_node_apply_messages_back1
betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
with
| Fail e -> Fail e
- | Return (_, _) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -1535,7 +1533,7 @@ and betree_internal_flush_back'a
self.betree_internal_right params node_id_cnt0
msgs_right st3 st5 with
| Fail e -> Fail e
- | Return (_, ()) ->
+ | Return _ ->
Return (st0, (Mkbetree_internal_t
self.betree_internal_id self.betree_internal_pivot n
n0, node_id_cnt1))
@@ -1565,7 +1563,7 @@ and betree_internal_flush_back'a
betree_node_apply_messages_back1 self.betree_internal_right
params node_id_cnt msgs_right st st2 with
| Fail e -> Fail e
- | Return (_, ()) ->
+ | Return _ ->
Return (st0, (Mkbetree_internal_t self.betree_internal_id
self.betree_internal_pivot self.betree_internal_left n,
node_id_cnt0))
@@ -1633,7 +1631,7 @@ and betree_internal_flush_back1
self.betree_internal_right params node_id_cnt0
msgs_right st3 st5 with
| Fail e -> Fail e
- | Return (_, ()) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -1657,7 +1655,7 @@ and betree_internal_flush_back1
betree_node_apply_messages_back1 self.betree_internal_right
params node_id_cnt msgs_right st st2 with
| Fail e -> Fail e
- | Return (_, ()) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -1709,7 +1707,7 @@ let betree_node_apply_back'a
betree_node_apply_messages_back1 self params node_id_cnt
(BetreeListCons (key, new_msg) l) st st2 with
| Fail e -> Fail e
- | Return (_, ()) -> Return (st0, (self0, node_id_cnt0))
+ | Return _ -> Return (st0, (self0, node_id_cnt0))
end
end
end
@@ -1736,7 +1734,7 @@ let betree_node_apply_back1
betree_node_apply_messages_back1 self params node_id_cnt
(BetreeListCons (key, new_msg) l) st st2 with
| Fail e -> Fail e
- | Return (_, ()) -> Return (st0, ())
+ | Return _ -> Return (st0, ())
end
end
end
@@ -1809,7 +1807,7 @@ let betree_be_tree_apply_back
self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
st2 with
| Fail e -> Fail e
- | Return (_, ()) ->
+ | Return _ ->
Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
end
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:32:22 +0000