summaryrefslogtreecommitdiff
path: root/tests/fstar/betree
diff options
context:
space:
mode:
authorSon Ho2022-11-14 11:58:31 +0100
committerSon HO2022-11-14 14:21:04 +0100
commit5a96e28b8706ed945ccbb569881ca1888cd73ace (patch)
tree9e48a9c0b50f96a413f874c90919c90ffbefc0cb /tests/fstar/betree
parent868fa924a37a3af6e701bbc0a2d51fefc2dc7c33 (diff)
Regenerate the files and fix the proofs
Diffstat (limited to 'tests/fstar/betree')
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst421
-rw-r--r--tests/fstar/betree/Primitives.fst32
2 files changed, 230 insertions, 223 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 8cb5eb41..f6045dfd 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -14,7 +14,7 @@ let betree_load_internal_node_fwd
result (state & (betree_list_t (u64 & betree_message_t)))
=
begin match betree_utils_load_internal_node_fwd id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, l) -> Return (st0, l)
end
@@ -24,7 +24,7 @@ let betree_store_internal_node_fwd
result (state & unit)
=
begin match betree_utils_store_internal_node_fwd id content st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) -> Return (st0, ())
end
@@ -32,7 +32,7 @@ let betree_store_internal_node_fwd
let betree_load_leaf_node_fwd
(id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
begin match betree_utils_load_leaf_node_fwd id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, l) -> Return (st0, l)
end
@@ -42,21 +42,21 @@ let betree_store_leaf_node_fwd
result (state & unit)
=
begin match betree_utils_store_leaf_node_fwd id content st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) -> Return (st0, ())
end
(** [betree_main::betree::fresh_node_id] *)
let betree_fresh_node_id_fwd (counter : u64) : result u64 =
begin match u64_add counter 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return counter
end
(** [betree_main::betree::fresh_node_id] *)
let betree_fresh_node_id_back (counter : u64) : result u64 =
begin match u64_add counter 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return counter0 -> Return counter0
end
@@ -68,7 +68,7 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
let betree_node_id_counter_fresh_id_fwd
(self : betree_node_id_counter_t) : result u64 =
begin match u64_add self.betree_node_id_counter_next_node_id 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return self.betree_node_id_counter_next_node_id
end
@@ -76,7 +76,7 @@ let betree_node_id_counter_fresh_id_fwd
let betree_node_id_counter_fresh_id_back
(self : betree_node_id_counter_t) : result betree_node_id_counter_t =
begin match u64_add self.betree_node_id_counter_next_node_id 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i -> Return (Mkbetree_node_id_counter_t i)
end
@@ -97,12 +97,12 @@ let betree_upsert_update_fwd
begin match st with
| BetreeUpsertFunStateAdd v ->
begin match u64_sub core_num_u64_max_c prev0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return margin ->
if margin >= v
then
begin match u64_add prev0 v with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i -> Return i
end
else Return core_num_u64_max_c
@@ -111,7 +111,7 @@ let betree_upsert_update_fwd
if prev0 >= v
then
begin match u64_sub prev0 v with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i -> Return i
end
else Return 0
@@ -126,9 +126,12 @@ let rec betree_list_len_fwd
begin match self with
| BetreeListCons x tl ->
begin match betree_list_len_fwd t tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
- begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+ begin match u64_add 1 i with
+ | Fail e -> Fail e
+ | Return i0 -> Return i0
+ end
end
| BetreeListNil -> Return 0
end
@@ -145,17 +148,17 @@ let rec betree_list_split_at_fwd
begin match self with
| BetreeListCons hd tl ->
begin match u64_sub n 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match betree_list_split_at_fwd t tl i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (ls0, ls1) = p in
let l = ls0 in
Return (BetreeListCons hd l, ls1)
end
end
- | BetreeListNil -> Fail
+ | BetreeListNil -> Fail Failure
end
(** [betree_main::betree::List::{1}::push_front] *)
@@ -170,7 +173,7 @@ 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
- | BetreeListNil -> Fail
+ | BetreeListNil -> Fail Failure
end
(** [betree_main::betree::List::{1}::pop_front] *)
@@ -179,14 +182,14 @@ let betree_list_pop_front_back
let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
begin match ls with
| BetreeListCons x tl -> Return tl
- | BetreeListNil -> Fail
+ | BetreeListNil -> Fail Failure
end
(** [betree_main::betree::List::{1}::hd] *)
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
+ | BetreeListNil -> Fail Failure
end
(** [betree_main::betree::List::{2}::head_has_key] *)
@@ -210,7 +213,7 @@ let rec betree_list_partition_at_pivot_fwd
then Return (BetreeListNil, BetreeListCons (i, x) tl)
else
begin match betree_list_partition_at_pivot_fwd t tl pivot with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (ls0, ls1) = p in
let l = ls0 in
@@ -229,27 +232,27 @@ let betree_leaf_split_fwd
begin match
betree_list_split_at_fwd (u64 & u64) content
params.betree_params_split_size with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (content0, content1) = p in
begin match betree_list_hd_fwd (u64 & u64) content1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p0 ->
let (pivot, _) = p0 in
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return id0 ->
begin match betree_node_id_counter_fresh_id_back node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt0 ->
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return id1 ->
begin match betree_store_leaf_node_fwd id0 content0 st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match betree_store_leaf_node_fwd id1 content1 st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
let n = BetreeNodeLeaf (Mkbetree_leaf_t id0
params.betree_params_split_size) in
@@ -275,30 +278,30 @@ let betree_leaf_split_back
begin match
betree_list_split_at_fwd (u64 & u64) content
params.betree_params_split_size with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (content0, content1) = p in
begin match betree_list_hd_fwd (u64 & u64) content1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ ->
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return id0 ->
begin match betree_node_id_counter_fresh_id_back node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt0 ->
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return id1 ->
begin match betree_store_leaf_node_fwd id0 content0 st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match betree_store_leaf_node_fwd id1 content1 st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) ->
begin match betree_node_id_counter_fresh_id_back node_id_cnt0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt1 -> Return node_id_cnt1
end
end
@@ -325,7 +328,7 @@ let rec betree_node_lookup_in_bindings_fwd
then Return None
else
begin match betree_node_lookup_in_bindings_fwd key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return opt -> Return opt
end
| BetreeListNil -> Return None
@@ -345,7 +348,7 @@ let rec betree_node_lookup_first_message_for_key_fwd
else
begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l -> Return l
end
| BetreeListNil -> Return BetreeListNil
@@ -366,7 +369,7 @@ let rec betree_node_lookup_first_message_for_key_back
else
begin match
betree_node_lookup_first_message_for_key_back key next_msgs ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
end
| BetreeListNil -> Return ret
@@ -380,28 +383,28 @@ let rec betree_node_apply_upserts_fwd
(decreases (betree_node_apply_upserts_decreases msgs prev key st))
=
begin match betree_list_head_has_key_fwd betree_message_t msgs key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b ->
if b
then
begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msg ->
let (_, m) = msg in
begin match m with
- | BetreeMessageInsert i -> Fail
- | BetreeMessageDelete -> Fail
+ | BetreeMessageInsert i -> Fail Failure
+ | BetreeMessageDelete -> Fail Failure
| BetreeMessageUpsert s ->
begin match betree_upsert_update_fwd prev s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match
betree_list_pop_front_back (u64 & betree_message_t) msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, i) -> Return (st0, i)
end
end
@@ -410,12 +413,12 @@ let rec betree_node_apply_upserts_fwd
end
else
begin match core_option_option_unwrap_fwd u64 prev st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, v) ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
BetreeMessageInsert v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, v)
end
end
@@ -429,28 +432,28 @@ let rec betree_node_apply_upserts_back
(decreases (betree_node_apply_upserts_decreases msgs prev key st))
=
begin match betree_list_head_has_key_fwd betree_message_t msgs key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b ->
if b
then
begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msg ->
let (_, m) = msg in
begin match m with
- | BetreeMessageInsert i -> Fail
- | BetreeMessageDelete -> Fail
+ | BetreeMessageInsert i -> Fail Failure
+ | BetreeMessageDelete -> Fail Failure
| BetreeMessageUpsert s ->
begin match betree_upsert_update_fwd prev s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match
betree_list_pop_front_back (u64 & betree_message_t) msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match betree_node_apply_upserts_back msgs0 (Some v) key st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 -> Return msgs1
end
end
@@ -459,12 +462,12 @@ let rec betree_node_apply_upserts_back
end
else
begin match core_option_option_unwrap_fwd u64 prev st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, v) ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
BetreeMessageInsert v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 -> Return msgs0
end
end
@@ -479,10 +482,10 @@ let rec betree_node_lookup_fwd
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, msgs) ->
begin match betree_node_lookup_first_message_for_key_fwd key msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pending ->
begin match pending with
| BetreeListCons p l ->
@@ -491,12 +494,12 @@ let rec betree_node_lookup_fwd
then
begin match betree_internal_lookup_in_children_fwd node key st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, opt) ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, msg) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st1, opt)
end
end
@@ -506,44 +509,44 @@ let rec betree_node_lookup_fwd
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, Some v)
end
| BetreeMessageDelete ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageDelete) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, None)
end
| BetreeMessageUpsert ufs ->
begin match betree_internal_lookup_in_children_fwd node key st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, v) ->
begin match
betree_node_apply_upserts_fwd (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, v0) ->
begin match
betree_internal_lookup_in_children_back node key st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node0 ->
begin match
betree_node_apply_upserts_back (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pending0 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
pending0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st3, _) -> Return (st3, Some v0)
end
end
@@ -554,12 +557,12 @@ let rec betree_node_lookup_fwd
end
| BetreeListNil ->
begin match betree_internal_lookup_in_children_fwd node key st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, opt) ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
BetreeListNil with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st1, opt)
end
end
@@ -568,10 +571,10 @@ let rec betree_node_lookup_fwd
end
| BetreeNodeLeaf node ->
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, bindings) ->
begin match betree_node_lookup_in_bindings_fwd key bindings with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return opt -> Return (st0, opt)
end
end
@@ -586,10 +589,10 @@ and betree_node_lookup_back
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, msgs) ->
begin match betree_node_lookup_first_message_for_key_fwd key msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pending ->
begin match pending with
| BetreeListCons p l ->
@@ -599,11 +602,11 @@ and betree_node_lookup_back
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, msg) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ ->
begin match betree_internal_lookup_in_children_back node key st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node0 -> Return (BetreeNodeInternal node0)
end
end
@@ -613,44 +616,44 @@ and betree_node_lookup_back
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| 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
+ | Fail e -> Fail e
| Return _ -> Return (BetreeNodeInternal node)
end
| BetreeMessageUpsert ufs ->
begin match betree_internal_lookup_in_children_fwd node key st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, v) ->
begin match
betree_node_apply_upserts_fwd (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) ->
begin match
betree_internal_lookup_in_children_back node key st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node0 ->
begin match
betree_node_apply_upserts_back (BetreeListCons (k,
BetreeMessageUpsert ufs) l) v key st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pending0 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
pending0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) -> Return (BetreeNodeInternal node0)
end
end
@@ -663,11 +666,11 @@ and betree_node_lookup_back
begin match
betree_node_lookup_first_message_for_key_back key msgs
BetreeListNil with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ ->
begin match betree_internal_lookup_in_children_back node key st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node0 -> Return (BetreeNodeInternal node0)
end
end
@@ -676,10 +679,10 @@ and betree_node_lookup_back
end
| BetreeNodeLeaf node ->
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, bindings) ->
begin match betree_node_lookup_in_bindings_fwd key bindings with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (BetreeNodeLeaf node)
end
end
@@ -694,12 +697,12 @@ and betree_internal_lookup_in_children_fwd
if key < self.betree_internal_pivot
then
begin match betree_node_lookup_fwd self.betree_internal_left key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, opt) -> Return (st0, opt)
end
else
begin match betree_node_lookup_fwd self.betree_internal_right key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, opt) -> Return (st0, opt)
end
@@ -712,14 +715,14 @@ and betree_internal_lookup_in_children_back
if key < self.betree_internal_pivot
then
begin match betree_node_lookup_back self.betree_internal_left key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| 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_lookup_back self.betree_internal_right key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return n ->
Return (Mkbetree_internal_t self.betree_internal_id
self.betree_internal_pivot self.betree_internal_left n)
@@ -738,7 +741,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd
then Return (BetreeListCons (i, i0) tl)
else
begin match betree_node_lookup_mut_in_bindings_fwd key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l -> Return l
end
| BetreeListNil -> Return BetreeListNil
@@ -758,7 +761,7 @@ let rec betree_node_lookup_mut_in_bindings_back
then Return ret
else
begin match betree_node_lookup_mut_in_bindings_back key tl ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (BetreeListCons (i, i0) tl0)
end
| BetreeListNil -> Return ret
@@ -771,62 +774,62 @@ let betree_node_apply_to_leaf_fwd_back
result (betree_list_t (u64 & u64))
=
begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings0 ->
begin match betree_list_head_has_key_fwd u64 bindings0 key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b ->
if b
then
begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hd ->
begin match new_msg with
| BetreeMessageInsert v ->
begin match betree_list_pop_front_back (u64 & u64) bindings0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 ->
begin match
betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings2 ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings
bindings2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings3 -> Return bindings3
end
end
end
| BetreeMessageDelete ->
begin match betree_list_pop_front_back (u64 & u64) bindings0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings bindings1
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings2 -> Return bindings2
end
end
| BetreeMessageUpsert s ->
let (_, i) = hd in
begin match betree_upsert_update_fwd (Some i) s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match betree_list_pop_front_back (u64 & u64) bindings0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 ->
begin match
betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings2 ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings
bindings2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings3 -> Return bindings3
end
end
@@ -839,34 +842,34 @@ let betree_node_apply_to_leaf_fwd_back
| BetreeMessageInsert v ->
begin match
betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings bindings1
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings2 -> Return bindings2
end
end
| BetreeMessageDelete ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 -> Return bindings1
end
| BetreeMessageUpsert s ->
begin match betree_upsert_update_fwd None s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match
betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 ->
begin match
betree_node_lookup_mut_in_bindings_back key bindings bindings1
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings2 -> Return bindings2
end
end
@@ -886,11 +889,11 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
| 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
+ | Fail e -> Fail e
| Return bindings0 ->
begin match
betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return bindings1 -> Return bindings1
end
end
@@ -911,10 +914,10 @@ let rec betree_node_filter_messages_for_key_fwd_back
begin match
betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
m) l) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 -> Return msgs1
end
end
@@ -935,7 +938,7 @@ let rec betree_node_lookup_first_message_after_key_fwd
then
begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l -> Return l
end
else Return (BetreeListCons (k, m) next_msgs)
@@ -956,7 +959,7 @@ let rec betree_node_lookup_first_message_after_key_back
then
begin match
betree_node_lookup_first_message_after_key_back key next_msgs ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
end
else Return ret
@@ -970,10 +973,10 @@ let betree_node_apply_to_internal_fwd_back
result (betree_list_t (u64 & betree_message_t))
=
begin match betree_node_lookup_first_message_for_key_fwd key msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs0 ->
begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b ->
if b
then
@@ -981,17 +984,17 @@ let betree_node_apply_to_internal_fwd_back
| BetreeMessageInsert i ->
begin match betree_node_filter_messages_for_key_fwd_back key msgs0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
(key, BetreeMessageInsert i) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs msgs2
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs3 -> Return msgs3
end
end
@@ -999,45 +1002,45 @@ let betree_node_apply_to_internal_fwd_back
| BetreeMessageDelete ->
begin match betree_node_filter_messages_for_key_fwd_back key msgs0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
(key, BetreeMessageDelete) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs msgs2
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs3 -> Return msgs3
end
end
end
| BetreeMessageUpsert s ->
begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (_, m) = p in
begin match m with
| BetreeMessageInsert prev ->
begin match betree_upsert_update_fwd (Some prev) s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match
betree_list_pop_front_back (u64 & betree_message_t) msgs0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageInsert v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
msgs2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs3 -> Return msgs3
end
end
@@ -1045,22 +1048,22 @@ let betree_node_apply_to_internal_fwd_back
end
| BetreeMessageDelete ->
begin match betree_upsert_update_fwd None s with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
begin match
betree_list_pop_front_back (u64 & betree_message_t) msgs0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageInsert v) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
msgs2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs3 -> Return msgs3
end
end
@@ -1069,22 +1072,22 @@ let betree_node_apply_to_internal_fwd_back
| BetreeMessageUpsert ufs ->
begin match
betree_node_lookup_first_message_after_key_fwd key msgs0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t)
msgs1 (key, BetreeMessageUpsert s) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 ->
begin match
betree_node_lookup_first_message_after_key_back key msgs0
msgs2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs3 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
msgs3 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs4 -> Return msgs4
end
end
@@ -1097,11 +1100,11 @@ let betree_node_apply_to_internal_fwd_back
begin match
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
new_msg) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 ->
begin match
betree_node_lookup_first_message_for_key_back key msgs msgs1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs2 -> Return msgs2
end
end
@@ -1119,11 +1122,11 @@ let rec betree_node_apply_messages_to_internal_fwd_back
| 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
+ | Fail e -> Fail e
| Return msgs0 ->
begin match
betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return msgs1 -> Return msgs1
end
end
@@ -1142,31 +1145,31 @@ let rec betree_node_apply_messages_fwd
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, content) ->
begin match betree_node_apply_messages_to_internal_fwd_back content msgs
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return content0 ->
begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return num_msgs ->
if num_msgs >= params.betree_params_min_flush_size
then
begin match
betree_internal_flush_fwd node params node_id_cnt content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, content1) ->
begin match
betree_internal_flush_back node params node_id_cnt content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (node0, _) ->
begin match
betree_store_internal_node_fwd node0.betree_internal_id
content1 st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) -> Return (st2, ())
end
end
@@ -1175,7 +1178,7 @@ let rec betree_node_apply_messages_fwd
begin match
betree_store_internal_node_fwd node.betree_internal_id content0
st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) -> Return (st1, ())
end
end
@@ -1183,27 +1186,27 @@ let rec betree_node_apply_messages_fwd
end
| BetreeNodeLeaf node ->
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, content) ->
begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return content0 ->
begin match betree_list_len_fwd (u64 & u64) content0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len ->
begin match u64_mul 2 params.betree_params_split_size with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if len >= i
then
begin match
betree_leaf_split_fwd node content0 params node_id_cnt st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
begin match
betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) -> Return (st2, ())
end
end
@@ -1211,7 +1214,7 @@ let rec betree_node_apply_messages_fwd
begin match
betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) -> Return (st1, ())
end
end
@@ -1232,31 +1235,31 @@ and betree_node_apply_messages_back
begin match self with
| BetreeNodeInternal node ->
begin match betree_load_internal_node_fwd node.betree_internal_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, content) ->
begin match betree_node_apply_messages_to_internal_fwd_back content msgs
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return content0 ->
begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return num_msgs ->
if num_msgs >= params.betree_params_min_flush_size
then
begin match
betree_internal_flush_fwd node params node_id_cnt content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, content1) ->
begin match
betree_internal_flush_back node params node_id_cnt content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (node0, node_id_cnt0) ->
begin match
betree_store_internal_node_fwd node0.betree_internal_id
content1 st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) ->
Return (BetreeNodeInternal node0, node_id_cnt0)
end
@@ -1266,7 +1269,7 @@ and betree_node_apply_messages_back
begin match
betree_store_internal_node_fwd node.betree_internal_id content0
st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
end
end
@@ -1274,32 +1277,32 @@ and betree_node_apply_messages_back
end
| BetreeNodeLeaf node ->
begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, content) ->
begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return content0 ->
begin match betree_list_len_fwd (u64 & u64) content0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len ->
begin match u64_mul 2 params.betree_params_split_size with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if len >= i
then
begin match
betree_leaf_split_fwd node content0 params node_id_cnt st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, new_node) ->
begin match
betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) ->
begin match
betree_leaf_split_back node content0 params node_id_cnt st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt0 ->
Return (BetreeNodeInternal new_node, node_id_cnt0)
end
@@ -1309,7 +1312,7 @@ and betree_node_apply_messages_back
begin match
betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) ->
Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
len), node_id_cnt)
@@ -1332,39 +1335,39 @@ and betree_internal_flush_fwd
begin match
betree_list_partition_at_pivot_fwd betree_message_t content
self.betree_internal_pivot with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (msgs_left, msgs_right) = p in
begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len_left ->
if len_left >= params.betree_params_min_flush_size
then
begin match
betree_node_apply_messages_fwd self.betree_internal_left params
node_id_cnt msgs_left st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
betree_node_apply_messages_back self.betree_internal_left params
node_id_cnt msgs_left st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, node_id_cnt0) ->
begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len_right ->
if len_right >= params.betree_params_min_flush_size
then
begin match
betree_node_apply_messages_fwd self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
begin match
betree_node_apply_messages_back self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) -> Return (st1, BetreeListNil)
end
end
@@ -1376,12 +1379,12 @@ and betree_internal_flush_fwd
begin match
betree_node_apply_messages_fwd self.betree_internal_right params
node_id_cnt msgs_right st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
betree_node_apply_messages_back self.betree_internal_right params
node_id_cnt msgs_right st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) -> Return (st0, msgs_left)
end
end
@@ -1400,34 +1403,34 @@ and betree_internal_flush_back
begin match
betree_list_partition_at_pivot_fwd betree_message_t content
self.betree_internal_pivot with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return p ->
let (msgs_left, msgs_right) = p in
begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len_left ->
if len_left >= params.betree_params_min_flush_size
then
begin match
betree_node_apply_messages_fwd self.betree_internal_left params
node_id_cnt msgs_left st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
betree_node_apply_messages_back self.betree_internal_left params
node_id_cnt msgs_left st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (n, node_id_cnt0) ->
begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return len_right ->
if len_right >= params.betree_params_min_flush_size
then
begin match
betree_node_apply_messages_back self.betree_internal_right
params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (n0, node_id_cnt1) ->
Return (Mkbetree_internal_t self.betree_internal_id
self.betree_internal_pivot n n0, node_id_cnt1)
@@ -1443,7 +1446,7 @@ and betree_internal_flush_back
begin match
betree_node_apply_messages_back self.betree_internal_right params
node_id_cnt msgs_right st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (n, node_id_cnt0) ->
Return (Mkbetree_internal_t self.betree_internal_id
self.betree_internal_pivot self.betree_internal_left n,
@@ -1463,12 +1466,12 @@ let betree_node_apply_fwd
begin match
betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
(key, new_msg) l) st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
(key, new_msg) l) st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, _) -> Return (st0, ())
end
end
@@ -1484,7 +1487,7 @@ let betree_node_apply_back
begin match
betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
(key, new_msg) l) st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0)
end
@@ -1494,16 +1497,16 @@ let betree_be_tree_new_fwd
result (state & betree_be_tree_t)
=
begin match betree_node_id_counter_new_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt ->
begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return id ->
begin match betree_store_leaf_node_fwd id BetreeListNil st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match betree_node_id_counter_fresh_id_back node_id_cnt with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return node_id_cnt0 ->
Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size
split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
@@ -1520,13 +1523,13 @@ let betree_be_tree_apply_fwd
begin match
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
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
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
+ | Fail e -> Fail e
| Return (_, _) -> Return (st0, ())
end
end
@@ -1539,7 +1542,7 @@ let betree_be_tree_apply_back
begin match
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
+ | Fail e -> Fail e
| Return (n, nic) ->
Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
end
@@ -1551,11 +1554,11 @@ let betree_be_tree_insert_fwd
=
begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match
betree_be_tree_apply_back self key (BetreeMessageInsert value) st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, ())
end
end
@@ -1567,7 +1570,7 @@ let betree_be_tree_insert_back
=
begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self0 -> Return self0
end
@@ -1575,10 +1578,10 @@ let betree_be_tree_insert_back
let betree_be_tree_delete_fwd
(self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, ())
end
end
@@ -1589,7 +1592,7 @@ let betree_be_tree_delete_back
result betree_be_tree_t
=
begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self0 -> Return self0
end
@@ -1601,11 +1604,11 @@ let betree_be_tree_upsert_fwd
=
begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (st0, ())
end
end
@@ -1618,7 +1621,7 @@ let betree_be_tree_upsert_back
=
begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self0 -> Return self0
end
@@ -1628,7 +1631,7 @@ let betree_be_tree_lookup_fwd
result (state & (option u64))
=
begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, opt) -> Return (st0, opt)
end
@@ -1638,7 +1641,7 @@ let betree_be_tree_lookup_back
result betree_be_tree_t
=
begin match betree_node_lookup_back self.betree_be_tree_root key st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return n ->
Return (Mkbetree_be_tree_t self.betree_be_tree_params
self.betree_be_tree_node_id_cnt n)
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
#pop-options
(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
type result (a : Type0) : Type0 =
| Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
// Monadic bind and return.
// Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
match m with
| Return x -> f x
- | Fail -> Fail
+ | Fail e -> Fail e
// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
// Normalize and unwrap a successful result (used for globals).
let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
- if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (x / y) else Fail
+ if y <> 0 then mk_scalar ty (x / y) else Fail Failure
/// The remainder operation
let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)
let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(requires True)
(ensures (fun res ->
match res with
- | Fail -> True
+ | Fail e -> e == Failure
| Return v' -> length v' = length v + 1)) =
if length v < usize_max then begin
(**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(**) assert(length (append v [x]) = length v + 1);
Return (append v [x])
end
- else Fail
+ else Fail Failure
// The **forward** function shouldn't be used
let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
- if i < length v then Return (list_update v i x) else Fail
+ if i < length v then Return (list_update v i x) else Fail Failure
// The **backward** function shouldn't be used
let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
- if i < length v then Return (list_update v i nx) else Fail
+ if i < length v then Return (list_update v i nx) else Fail Failure