summaryrefslogtreecommitdiff
path: root/tests/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/betree')
-rw-r--r--tests/betree/BetreeMain.Funs.fst113
-rw-r--r--tests/betree/Primitives.fst2
2 files changed, 29 insertions, 86 deletions
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index b11ca399..9b960ce5 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -135,9 +135,9 @@ let rec betree_list_split_at_fwd
Tot (result ((betree_list_t t) & (betree_list_t t)))
(decreases (betree_list_split_at_decreases t self n))
=
- begin match n with
- | 0 -> Return (BetreeListNil, self)
- | _ ->
+ if n = 0
+ then Return (BetreeListNil, self)
+ else
begin match self with
| BetreeListCons hd tl ->
begin match u64_sub n 1 with
@@ -152,7 +152,6 @@ let rec betree_list_split_at_fwd
end
| BetreeListNil -> Fail
end
- end
(** [betree_main::betree::List::{1}::push_front] *)
let betree_list_push_front_fwd_back
@@ -528,10 +527,7 @@ and betree_node_lookup_fwd
let (k, msg) = p in
if k <> key
then
- begin match
- 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
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, opt) ->
@@ -559,10 +555,7 @@ and betree_node_lookup_fwd
| Return _ -> Return (st0, None)
end
| BetreeMessageUpsert ufs ->
- begin match
- 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
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, v) ->
@@ -572,10 +565,7 @@ and betree_node_lookup_fwd
| Fail -> Fail
| Return (st2, v0) ->
begin match
- 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
+ betree_internal_lookup_in_children_back node key st0 with
| Fail -> Fail
| Return node0 ->
begin match
@@ -601,11 +591,7 @@ and betree_node_lookup_fwd
end
end
| BetreeListNil ->
- begin match
- 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
+ begin match betree_internal_lookup_in_children_fwd node key st0 with
| Fail -> Fail
| Return (st1, opt) ->
begin match
@@ -653,10 +639,7 @@ and betree_node_lookup_back
(BetreeListCons (k, msg) l) with
| Fail -> Fail
| Return _ ->
- begin match
- 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
+ begin match betree_internal_lookup_in_children_back node key st0
with
| Fail -> Fail
| Return node0 -> Return (BetreeNodeInternal node0)
@@ -669,26 +652,17 @@ and betree_node_lookup_back
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right))
+ | Return _ -> Return (BetreeNodeInternal node)
end
| BetreeMessageDelete ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageDelete) l) with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right))
+ | Return _ -> Return (BetreeNodeInternal node)
end
| BetreeMessageUpsert ufs ->
- begin match
- 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
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, v) ->
@@ -698,10 +672,7 @@ and betree_node_lookup_back
| Fail -> Fail
| Return (st2, _) ->
begin match
- 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
+ betree_internal_lookup_in_children_back node key st0 with
| Fail -> Fail
| Return node0 ->
begin match
@@ -718,12 +689,7 @@ and betree_node_lookup_back
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st2 with
| Fail -> Fail
- | Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node0.betree_internal_id
- node0.betree_internal_pivot
- node0.betree_internal_left
- node0.betree_internal_right))
+ | Return (_, _) -> Return (BetreeNodeInternal node0)
end
end
end
@@ -737,10 +703,7 @@ and betree_node_lookup_back
BetreeListNil with
| Fail -> Fail
| Return _ ->
- begin match
- 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
+ begin match betree_internal_lookup_in_children_back node key st0
with
| Fail -> Fail
| Return node0 -> Return (BetreeNodeInternal node0)
@@ -755,9 +718,7 @@ and betree_node_lookup_back
| Return (_, bindings) ->
begin match betree_node_lookup_in_bindings_fwd key bindings with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size))
+ | Return _ -> Return (BetreeNodeLeaf node)
end
end
end
@@ -1323,17 +1284,13 @@ and betree_node_apply_messages_fwd
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- 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
+ betree_internal_flush_fwd node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- 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
+ betree_internal_flush_back node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (node0, _) ->
begin match
@@ -1370,8 +1327,7 @@ and betree_node_apply_messages_fwd
if len >= i
then
begin match
- betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0 with
+ betree_leaf_split_fwd node content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, _) ->
begin match
@@ -1418,17 +1374,13 @@ and betree_node_apply_messages_back
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- 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
+ betree_internal_flush_fwd node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- 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
+ betree_internal_flush_back node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (node0, node_id_cnt0) ->
begin match
@@ -1436,10 +1388,7 @@ and betree_node_apply_messages_back
content1 st1 with
| Fail -> Fail
| Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node0.betree_internal_id node0.betree_internal_pivot
- node0.betree_internal_left node0.betree_internal_right),
- node_id_cnt0)
+ Return (BetreeNodeInternal node0, node_id_cnt0)
end
end
end
@@ -1448,11 +1397,7 @@ and betree_node_apply_messages_back
betree_store_internal_node_fwd node.betree_internal_id content0
st0 with
| Fail -> Fail
- | Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right),
- node_id_cnt)
+ | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
end
end
end
@@ -1473,8 +1418,7 @@ and betree_node_apply_messages_back
if len >= i
then
begin match
- betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0 with
+ betree_leaf_split_fwd node content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, new_node) ->
begin match
@@ -1483,8 +1427,7 @@ and betree_node_apply_messages_back
| Fail -> Fail
| Return (_, _) ->
begin match
- betree_leaf_split_back (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0
+ betree_leaf_split_back node content0 params node_id_cnt st0
with
| Fail -> Fail
| Return node_id_cnt0 ->
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 03:14:15 +0000