diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 1416 | ||||
| -rw-r--r-- | tests/fstar/betree/Primitives.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 1978 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 540 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 607 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 9 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Funs.fst | 94 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 313 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 220 | ||||
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 95 | ||||
| -rw-r--r-- | tests/fstar/misc/PoloniusList.fst | 7 | ||||
| -rw-r--r-- | tests/fstar/misc/Primitives.fst | 4 |
15 files changed, 1667 insertions, 3632 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 854862b2..8c0c1cc1 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -20,10 +20,8 @@ let betree_store_internal_node_fwd (id : u64) (content : betree_list_t (u64 & betree_message_t)) (st : state) : result (state & unit) = - begin match betree_utils_store_internal_node_fwd id content st with - | Fail e -> Fail e - | Return (st0, _) -> Return (st0, ()) - end + let* (st0, _) = betree_utils_store_internal_node_fwd id content st in + Return (st0, ()) (** [betree_main::betree::load_leaf_node] *) let betree_load_leaf_node_fwd @@ -35,17 +33,12 @@ let betree_store_leaf_node_fwd (id : u64) (content : betree_list_t (u64 & u64)) (st : state) : result (state & unit) = - begin match betree_utils_store_leaf_node_fwd id content st with - | Fail e -> Fail e - | Return (st0, _) -> Return (st0, ()) - end + let* (st0, _) = betree_utils_store_leaf_node_fwd id content st in + Return (st0, ()) (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_fwd (counter : u64) : result u64 = - begin match u64_add counter 1 with - | Fail e -> Fail e - | Return _ -> Return counter - end + let* _ = u64_add counter 1 in Return counter (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 @@ -57,18 +50,14 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) 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 e -> Fail e - | Return _ -> Return self.betree_node_id_counter_next_node_id - end + let* _ = u64_add self.betree_node_id_counter_next_node_id 1 in + Return self.betree_node_id_counter_next_node_id (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) 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 e -> Fail e - | Return i -> Return (Mkbetree_node_id_counter_t i) - end + let* i = u64_add self.betree_node_id_counter_next_node_id 1 in + Return (Mkbetree_node_id_counter_t i) (** [core::num::u64::{10}::MAX] *) let core_num_u64_max_body : result u64 = Return 18446744073709551615 @@ -86,11 +75,8 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - begin match u64_sub core_num_u64_max_c prev0 with - | Fail e -> Fail e - | Return margin -> - if margin >= v then u64_add prev0 v else Return core_num_u64_max_c - end + let* margin = u64_sub core_num_u64_max_c prev0 in + if margin >= v then u64_add prev0 v else Return core_num_u64_max_c | BetreeUpsertFunStateSub v -> if prev0 >= v then u64_sub prev0 v else Return 0 end @@ -102,11 +88,7 @@ let rec betree_list_len_fwd Tot (result u64) (decreases (betree_list_len_decreases t self)) = begin match self with - | BetreeListCons x tl -> - begin match betree_list_len_fwd t tl with - | Fail e -> Fail e - | Return i -> u64_add 1 i - end + | BetreeListCons x tl -> let* i = betree_list_len_fwd t tl in u64_add 1 i | BetreeListNil -> Return 0 end @@ -121,17 +103,11 @@ let rec betree_list_split_at_fwd else begin match self with | BetreeListCons hd tl -> - begin match u64_sub n 1 with - | Fail e -> Fail e - | Return i -> - begin match betree_list_split_at_fwd t tl i with - | Fail e -> Fail e - | Return p -> - let (ls0, ls1) = p in - let l = ls0 in - Return (BetreeListCons hd l, ls1) - end - end + let* i = u64_sub n 1 in + let* p = betree_list_split_at_fwd t tl i in + let (ls0, ls1) = p in + let l = ls0 in + Return (BetreeListCons hd l, ls1) | BetreeListNil -> Fail Failure end @@ -185,14 +161,11 @@ let rec betree_list_partition_at_pivot_fwd let (i, x) = hd in if i >= pivot then Return (BetreeListNil, BetreeListCons (i, x) tl) - else - begin match betree_list_partition_at_pivot_fwd t tl pivot with - | Fail e -> Fail e - | Return p -> - let (ls0, ls1) = p in - let l = ls0 in - Return (BetreeListCons (i, x) l, ls1) - end + else begin + let* p = betree_list_partition_at_pivot_fwd t tl pivot in + let (ls0, ls1) = p in + let l = ls0 in + Return (BetreeListCons (i, x) l, ls1) end | BetreeListNil -> Return (BetreeListNil, BetreeListNil) end @@ -203,44 +176,22 @@ let betree_leaf_split_fwd (st : state) : result (state & betree_internal_t) = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return p0 -> - let (pivot, _) = p0 in - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match betree_store_leaf_node_fwd id1 content1 st0 with - | Fail e -> Fail e - | Return (st1, _) -> - let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 - params.betree_params_split_size) in - let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 - params.betree_params_split_size) in - Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n - n0) - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* p0 = betree_list_hd_fwd (u64 & u64) content1 in + let (pivot, _) = p0 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in + let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in + let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size) + in + let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size) + in + Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0) (** [betree_main::betree::Leaf::{3}::split] *) let betree_leaf_split_back @@ -249,37 +200,17 @@ let betree_leaf_split_back (st : state) : result betree_node_id_counter_t = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return _ -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | 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 - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* _ = betree_list_hd_fwd (u64 & u64) content1 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in + let* _ = betree_store_leaf_node_fwd id1 content1 st0 in + betree_node_id_counter_fresh_id_back node_id_cnt0 (** [betree_main::betree::Node::{5}::lookup_in_bindings] *) let rec betree_node_lookup_in_bindings_fwd @@ -326,12 +257,10 @@ let rec betree_node_lookup_first_message_for_key_back let (i, m) = x in if i >= key then Return ret - else - begin match - betree_node_lookup_first_message_for_key_back key next_msgs ret with - | Fail e -> Fail e - | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0) - end + else begin + let* next_msgs0 = + betree_node_lookup_first_message_for_key_back key next_msgs ret in + Return (BetreeListCons (i, m) next_msgs0) end | BetreeListNil -> Return ret end @@ -342,43 +271,25 @@ let rec betree_node_apply_upserts_fwd Tot (result (state & u64)) (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 e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msg -> - let (_, m) = msg in - begin match m with - | BetreeMessageInsert i -> Fail Failure - | BetreeMessageDelete -> Fail Failure - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd prev s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msgs0 -> - betree_node_apply_upserts_fwd msgs0 (Some v) key st - end - end - end - end - else - begin match core_option_option_unwrap_fwd u64 prev st with - | 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 e -> Fail e - | Return _ -> Return (st0, v) - end - end - end + let* b = betree_list_head_has_key_fwd betree_message_t msgs key in + if b + then begin + let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in + let (_, m) = msg in + begin match m with + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd prev s in + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in + betree_node_apply_upserts_fwd msgs0 (Some v) key st + end end + else begin + let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in + let* _ = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, + BetreeMessageInsert v) in + Return (st0, v) end (** [betree_main::betree::Node::{5}::apply_upserts] *) let rec betree_node_apply_upserts_back @@ -387,39 +298,23 @@ let rec betree_node_apply_upserts_back Tot (result (betree_list_t (u64 & betree_message_t))) (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 e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msg -> - let (_, m) = msg in - begin match m with - | BetreeMessageInsert i -> Fail Failure - | BetreeMessageDelete -> Fail Failure - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd prev s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msgs0 -> - betree_node_apply_upserts_back msgs0 (Some v) key st - end - end - end - end - else - begin match core_option_option_unwrap_fwd u64 prev st with - | Fail e -> Fail e - | Return (_, v) -> - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, - BetreeMessageInsert v) - end - end + let* b = betree_list_head_has_key_fwd betree_message_t msgs key in + if b + then begin + let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in + let (_, m) = msg in + begin match m with + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd prev s in + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in + betree_node_apply_upserts_back msgs0 (Some v) key st + end end + else begin + let* (_, v) = core_option_option_unwrap_fwd u64 prev st in + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, + BetreeMessageInsert v) end (** [betree_main::betree::Node::{5}::lookup] *) let rec betree_node_lookup_fwd @@ -429,103 +324,59 @@ 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 e -> Fail e - | Return (st0, msgs) -> - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return pending -> - begin match pending with - | BetreeListCons p l -> - let (k, msg) = p in - if k <> key - then - begin match betree_internal_lookup_in_children_fwd node key st0 - with - | 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 e -> Fail e - | Return _ -> Return (st1, opt) - end - end - else - begin match msg with - | BetreeMessageInsert v -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, BetreeMessageInsert v) l) with - | 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 e -> Fail e - | Return _ -> Return (st0, None) - end - | BetreeMessageUpsert ufs -> - begin match betree_internal_lookup_in_children_fwd node key st0 - with - | Fail e -> Fail e - | Return (st1, v) -> - begin match - betree_node_apply_upserts_fwd (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 with - | Fail e -> Fail e - | Return (st2, v0) -> - begin match - betree_internal_lookup_in_children_back node key st0 with - | Fail e -> Fail e - | Return node0 -> - begin match - betree_node_apply_upserts_back (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 with - | Fail e -> Fail e - | Return pending0 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - pending0 with - | Fail e -> Fail e - | Return msgs0 -> - begin match - betree_store_internal_node_fwd - node0.betree_internal_id msgs0 st2 with - | Fail e -> Fail e - | Return (st3, _) -> Return (st3, Some v0) - end - end - end - end - end - end - end - | BetreeListNil -> - begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail e -> Fail e - | Return (st1, opt) -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - BetreeListNil with - | Fail e -> Fail e - | Return _ -> Return (st1, opt) - end - end + let* (st0, msgs) = betree_load_internal_node_fwd node.betree_internal_id st + in + let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in + begin match pending with + | BetreeListCons p l -> + let (k, msg) = p in + if k <> key + then begin + let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 + in + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l) in + Return (st1, opt) end + else + begin match msg with + | BetreeMessageInsert v -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l) in + Return (st0, Some v) + | BetreeMessageDelete -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageDelete) l) in + Return (st0, None) + | BetreeMessageUpsert ufs -> + let* (st1, v) = betree_internal_lookup_in_children_fwd node key st0 + in + let* (st2, v0) = + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 in + let* node0 = betree_internal_lookup_in_children_back node key st0 in + let* pending0 = + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 in + let* msgs0 = + betree_node_lookup_first_message_for_key_back key msgs pending0 in + let* (st3, _) = + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 + in + Return (st3, Some v0) end - end + | BetreeListNil -> + let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 in + let* _ = + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in + Return (st1, opt) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st0, bindings) -> - begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return opt -> Return (st0, opt) - end - end + let* (st0, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* opt = betree_node_lookup_in_bindings_fwd key bindings in + Return (st0, opt) end (** [betree_main::betree::Node::{5}::lookup] *) @@ -536,104 +387,58 @@ 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 e -> Fail e - | Return (st0, msgs) -> - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return pending -> - begin match pending with - | BetreeListCons p l -> - let (k, msg) = p in - if k <> key - then - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, msg) l) with - | Fail e -> Fail e - | Return _ -> - begin match betree_internal_lookup_in_children_back node key st0 - with - | Fail e -> Fail e - | Return node0 -> Return (BetreeNodeInternal node0) - end - end - else - begin match msg with - | BetreeMessageInsert v -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, BetreeMessageInsert v) l) with - | 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 e -> Fail e - | Return _ -> Return (BetreeNodeInternal node) - end - | BetreeMessageUpsert ufs -> - begin match betree_internal_lookup_in_children_fwd node key st0 - with - | Fail e -> Fail e - | Return (st1, v) -> - begin match - betree_node_apply_upserts_fwd (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 with - | Fail e -> Fail e - | Return (st2, _) -> - begin match - betree_internal_lookup_in_children_back node key st0 with - | Fail e -> Fail e - | Return node0 -> - begin match - betree_node_apply_upserts_back (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 with - | Fail e -> Fail e - | Return pending0 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - pending0 with - | Fail e -> Fail e - | Return msgs0 -> - begin match - betree_store_internal_node_fwd - node0.betree_internal_id msgs0 st2 with - | Fail e -> Fail e - | Return _ -> Return (BetreeNodeInternal node0) - end - end - end - end - end - end - end - | BetreeListNil -> - begin match + let* (st0, msgs) = betree_load_internal_node_fwd node.betree_internal_id st + in + let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in + begin match pending with + | BetreeListCons p l -> + let (k, msg) = p in + if k <> key + then begin + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l) in + let* node0 = betree_internal_lookup_in_children_back node key st0 in + Return (BetreeNodeInternal node0) end + else + begin match msg with + | BetreeMessageInsert v -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l) in + Return (BetreeNodeInternal node) + | BetreeMessageDelete -> + let* _ = betree_node_lookup_first_message_for_key_back key msgs - BetreeListNil with - | Fail e -> Fail e - | Return _ -> - begin match betree_internal_lookup_in_children_back node key st0 - with - | Fail e -> Fail e - | Return node0 -> Return (BetreeNodeInternal node0) - end - end + (BetreeListCons (k, BetreeMessageDelete) l) in + Return (BetreeNodeInternal node) + | BetreeMessageUpsert ufs -> + let* (st1, v) = betree_internal_lookup_in_children_fwd node key st0 + in + let* (st2, _) = + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 in + let* node0 = betree_internal_lookup_in_children_back node key st0 in + let* pending0 = + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 in + let* msgs0 = + betree_node_lookup_first_message_for_key_back key msgs pending0 in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 + in + Return (BetreeNodeInternal node0) end - end + | BetreeListNil -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in + let* node0 = betree_internal_lookup_in_children_back node key st0 in + Return (BetreeNodeInternal node0) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (_, bindings) -> - begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return _ -> Return (BetreeNodeLeaf node) - end - end + let* (_, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* _ = betree_node_lookup_in_bindings_fwd key bindings in + Return (BetreeNodeLeaf node) end (** [betree_main::betree::Internal::{4}::lookup_in_children] *) @@ -653,20 +458,14 @@ and betree_internal_lookup_in_children_back (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then - begin match betree_node_lookup_back self.betree_internal_left key st with - | 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 e -> Fail e - | Return n -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) - end + then begin + let* n = betree_node_lookup_back self.betree_internal_left key st in + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right) end + else begin + let* n = betree_node_lookup_back self.betree_internal_right key st in + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n) end (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -695,11 +494,9 @@ let rec betree_node_lookup_mut_in_bindings_back let (i, i0) = hd in if i >= key then Return ret - else - begin match betree_node_lookup_mut_in_bindings_back key tl ret with - | Fail e -> Fail e - | Return tl0 -> Return (BetreeListCons (i, i0) tl0) - end + else begin + let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in + Return (BetreeListCons (i, i0) tl0) end | BetreeListNil -> Return ret end @@ -709,82 +506,42 @@ let betree_node_apply_to_leaf_fwd_back (new_msg : betree_message_t) : result (betree_list_t (u64 & u64)) = - begin match betree_node_lookup_mut_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return bindings0 -> - begin match betree_list_head_has_key_fwd u64 bindings0 key with - | Fail e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with - | 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 e -> Fail e - | Return bindings1 -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) - with - | Fail e -> Fail e - | Return bindings2 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - end - end - | BetreeMessageDelete -> - begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - | BetreeMessageUpsert s -> - let (_, i) = hd in - begin match betree_upsert_update_fwd (Some i) s with - | Fail e -> Fail e - | Return v -> - begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail e -> Fail e - | Return bindings1 -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, - v) with - | Fail e -> Fail e - | Return bindings2 -> - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 - end - end - end - end - end - else - begin match new_msg with - | BetreeMessageInsert v -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - | BetreeMessageDelete -> - betree_node_lookup_mut_in_bindings_back key bindings bindings0 - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd None s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) - with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - end - end + let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in + let* b = betree_list_head_has_key_fwd u64 bindings0 key in + if b + then begin + let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + | BetreeMessageDelete -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageUpsert s -> + let (_, i) = hd in + let* v = betree_upsert_update_fwd (Some i) s in + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + end end + else + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageDelete -> + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd None s in + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end - end (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) let rec betree_node_apply_messages_to_leaf_fwd_back @@ -796,11 +553,8 @@ let rec betree_node_apply_messages_to_leaf_fwd_back 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 e -> Fail e - | Return bindings0 -> - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl - end + let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl | BetreeListNil -> Return bindings end @@ -814,13 +568,11 @@ let rec betree_node_filter_messages_for_key_fwd_back | BetreeListCons p l -> let (k, m) = p in if k = key - then - begin match + then begin + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, - m) l) with - | Fail e -> Fail e - | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0 - end + m) l) in + betree_node_filter_messages_for_key_fwd_back key msgs0 end else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil end @@ -851,12 +603,10 @@ let rec betree_node_lookup_first_message_after_key_back | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then - begin match - betree_node_lookup_first_message_after_key_back key next_msgs ret with - | Fail e -> Fail e - | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0) - end + then begin + let* next_msgs0 = + betree_node_lookup_first_message_after_key_back key next_msgs ret in + Return (BetreeListCons (k, m) next_msgs0) end else Return ret | BetreeListNil -> Return ret end @@ -867,118 +617,59 @@ let betree_node_apply_to_internal_fwd_back (new_msg : betree_message_t) : result (betree_list_t (u64 & betree_message_t)) = - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return msgs0 -> - begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with - | Fail e -> Fail e - | Return b -> - if b - then - begin match new_msg with - | BetreeMessageInsert i -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 - (key, BetreeMessageInsert i) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs msgs2 - end - end - | BetreeMessageDelete -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 - (key, BetreeMessageDelete) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs msgs2 - end - end - | BetreeMessageUpsert s -> - begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with - | 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 e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs2 - end - end - end - | BetreeMessageDelete -> - begin match betree_upsert_update_fwd None s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs2 - end - end - end - | BetreeMessageUpsert ufs -> - begin match - betree_node_lookup_first_message_after_key_fwd key msgs0 with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageUpsert s) with - | Fail e -> Fail e - | Return msgs2 -> - begin match - betree_node_lookup_first_message_after_key_back key msgs0 - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs3 - end - end - end - end - end - end - else - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, - new_msg) with - | Fail e -> Fail e - | Return msgs1 -> - betree_node_lookup_first_message_for_key_back key msgs msgs1 - end + let* msgs0 = betree_node_lookup_first_message_for_key_fwd key msgs in + let* b = betree_list_head_has_key_fwd betree_message_t msgs0 key in + if b + then + begin match new_msg with + | BetreeMessageInsert i -> + let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert i) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageDelete -> + let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageDelete) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageUpsert s -> + let* p = betree_list_hd_fwd (u64 & betree_message_t) msgs0 in + let (_, m) = p in + begin match m with + | BetreeMessageInsert prev -> + let* v = betree_upsert_update_fwd (Some prev) s in + let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert v) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageDelete -> + let* v = betree_upsert_update_fwd None s in + let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert v) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageUpsert ufs -> + let* msgs1 = betree_node_lookup_first_message_after_key_fwd key msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageUpsert s) in + let* msgs3 = + betree_node_lookup_first_message_after_key_back key msgs0 msgs2 in + betree_node_lookup_first_message_for_key_back key msgs msgs3 + end end - end + else begin + let* msgs1 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, + new_msg) in + betree_node_lookup_first_message_for_key_back key msgs msgs1 end (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) let rec betree_node_apply_messages_to_internal_fwd_back @@ -990,11 +681,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back 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 e -> Fail e - | Return msgs0 -> - betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl - end + let* msgs0 = betree_node_apply_to_internal_fwd_back msgs i m in + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl | BetreeListNil -> Return msgs end @@ -1009,83 +697,40 @@ 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 e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_internal_fwd_back content msgs - with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | 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 e -> Fail e - | Return (st1, content1) -> - begin match - betree_internal_flush_back node params node_id_cnt content0 st0 - with - | Fail e -> Fail e - | Return (node0, _) -> - begin match - betree_store_internal_node_fwd node0.betree_internal_id - content1 st1 with - | Fail e -> Fail e - | Return (st2, _) -> Return (st2, ()) - end - end - end - else - begin match - betree_store_internal_node_fwd node.betree_internal_id content0 - st0 with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end - end + let* (st0, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then begin + let* (st1, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st0 in + let* (node0, _) = + betree_internal_flush_back node params node_id_cnt content0 st0 in + let* (st2, _) = + betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in + Return (st2, ()) end + else begin + let* (st1, _) = + betree_store_internal_node_fwd node.betree_internal_id content0 st0 in + Return (st1, ()) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail e -> Fail e - | Return len -> - begin match u64_mul 2 params.betree_params_split_size with - | 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 e -> Fail e - | Return (st1, _) -> - begin match - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil - st1 with - | Fail e -> Fail e - | Return (st2, _) -> Return (st2, ()) - end - end - else - begin match - betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 - with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end - end - end + let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then begin + let* (st1, _) = + betree_leaf_split_fwd node content0 params node_id_cnt st0 in + let* (st2, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in + Return (st2, ()) end + else begin + let* (st1, _) = + betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in + Return (st1, ()) end end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -1099,92 +744,42 @@ 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 e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_internal_fwd_back content msgs - with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | 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 e -> Fail e - | Return (st1, content1) -> - begin match - betree_internal_flush_back node params node_id_cnt content0 st0 - with - | Fail e -> Fail e - | Return (node0, node_id_cnt0) -> - begin match - betree_store_internal_node_fwd node0.betree_internal_id - content1 st1 with - | Fail e -> Fail e - | Return _ -> Return (BetreeNodeInternal node0, node_id_cnt0) - end - end - end - else - begin match - betree_store_internal_node_fwd node.betree_internal_id content0 - st0 with - | Fail e -> Fail e - | Return _ -> Return (BetreeNodeInternal node, node_id_cnt) - end - end - end - end + let* (st0, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then begin + let* (st1, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st0 in + let* (node0, node_id_cnt0) = + betree_internal_flush_back node params node_id_cnt content0 st0 in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in + Return (BetreeNodeInternal node0, node_id_cnt0) end + else begin + let* _ = + betree_store_internal_node_fwd node.betree_internal_id content0 st0 in + Return (BetreeNodeInternal node, node_id_cnt) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail e -> Fail e - | Return len -> - begin match u64_mul 2 params.betree_params_split_size with - | 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 e -> Fail e - | Return (st1, new_node) -> - begin match - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil - st1 with - | Fail e -> Fail e - | Return _ -> - begin match - betree_leaf_split_back node content0 params node_id_cnt st0 - with - | Fail e -> Fail e - | Return node_id_cnt0 -> - Return (BetreeNodeInternal new_node, node_id_cnt0) - end - end - end - else - begin match - betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 - with - | Fail e -> Fail e - | Return _ -> - Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id - len), node_id_cnt) - end - end - end - end - end + let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then begin + let* (st1, new_node) = + betree_leaf_split_fwd node content0 params node_id_cnt st0 in + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 + in + let* node_id_cnt0 = + betree_leaf_split_back node content0 params node_id_cnt st0 in + Return (BetreeNodeInternal new_node, node_id_cnt0) end + else begin + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in + Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), + node_id_cnt) end end (** [betree_main::betree::Internal::{4}::flush] *) @@ -1196,64 +791,38 @@ and betree_internal_flush_fwd (decreases ( betree_internal_flush_decreases self params node_id_cnt content st)) = - begin match + let* p = betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | 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 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 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 e -> Fail e - | Return (_, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | 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 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 e -> Fail e - | Return _ -> Return (st1, BetreeListNil) - end - end - else Return (st0, msgs_right) - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | 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 e -> Fail e - | Return _ -> Return (st0, msgs_left) - end - end - end - end + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then begin + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (_, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then begin + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + let* _ = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + Return (st1, BetreeListNil) end + else Return (st0, msgs_right) end + else begin + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st in + let* _ = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st in + Return (st0, msgs_left) end (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back @@ -1264,60 +833,37 @@ and betree_internal_flush_back (decreases ( betree_internal_flush_decreases self params node_id_cnt content st)) = - begin match + let* p = betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | 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 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 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 e -> Fail e - | Return (n, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | 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 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) - end - else - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right, - node_id_cnt0) - end - end - end - else - begin match - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st with - | 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, - node_id_cnt0) - end + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then begin + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (n, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then begin + let* (n0, node_id_cnt1) = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n n0, node_id_cnt1) end + else + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0) end - end + else begin + let* (n, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st in + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0) end (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -1327,18 +873,13 @@ let betree_node_apply_fwd result (state & unit) = let l = BetreeListNil in - begin match + let* (st0, _) = betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons - (key, new_msg) l) st with - | 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 e -> Fail e - | Return _ -> Return (st0, ()) - end - end + (key, new_msg) l) st in + let* _ = + betree_node_apply_messages_back self params node_id_cnt (BetreeListCons + (key, new_msg) l) st in + Return (st0, ()) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_back @@ -1356,72 +897,45 @@ let betree_be_tree_new_fwd (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_be_tree_t) = - begin match betree_node_id_counter_new_fwd with - | Fail e -> Fail e - | Return node_id_cnt -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id -> - begin match betree_store_leaf_node_fwd id BetreeListNil st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | 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))) - end - end - end - end + let* node_id_cnt = betree_node_id_counter_new_fwd in + let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size) + node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0))) (** [betree_main::betree::BeTree::{6}::apply] *) let betree_be_tree_apply_fwd (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) : result (state & unit) = - begin match + let* (st0, _) = 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 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 e -> Fail e - | Return _ -> Return (st0, ()) - end - end + self.betree_be_tree_node_id_cnt key msg st in + let* _ = + betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params + self.betree_be_tree_node_id_cnt key msg st in + Return (st0, ()) (** [betree_main::betree::BeTree::{6}::apply] *) 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 + let* (n, nic) = 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 e -> Fail e - | Return (n, nic) -> - Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n) - end + self.betree_be_tree_node_id_cnt key msg st in + Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n) (** [betree_main::betree::BeTree::{6}::insert] *) 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_apply_fwd self key (BetreeMessageInsert value) st - with - | Fail e -> Fail e - | Return (st0, _) -> - begin match - betree_be_tree_apply_back self key (BetreeMessageInsert value) st with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end + let* (st0, _) = + betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st in + let* _ = betree_be_tree_apply_back self key (BetreeMessageInsert value) st in + Return (st0, ()) (** [betree_main::betree::BeTree::{6}::insert] *) let betree_be_tree_insert_back @@ -1433,14 +947,9 @@ let betree_be_tree_insert_back (** [betree_main::betree::BeTree::{6}::delete] *) 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 e -> Fail e - | Return (st0, _) -> - begin match betree_be_tree_apply_back self key BetreeMessageDelete st with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end + let* (st0, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in + let* _ = betree_be_tree_apply_back self key BetreeMessageDelete st in + Return (st0, ()) (** [betree_main::betree::BeTree::{6}::delete] *) let betree_be_tree_delete_back @@ -1455,16 +964,10 @@ let betree_be_tree_upsert_fwd (st : state) : result (state & unit) = - begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st - with - | Fail e -> Fail e - | Return (st0, _) -> - begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st - with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end + let* (st0, _) = + betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st in + let* _ = betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st in + Return (st0, ()) (** [betree_main::betree::BeTree::{6}::upsert] *) let betree_be_tree_upsert_back @@ -1486,12 +989,9 @@ let betree_be_tree_lookup_back (self : betree_be_tree_t) (key : u64) (st : state) : result betree_be_tree_t = - begin match betree_node_lookup_back self.betree_be_tree_root key st with - | Fail e -> Fail e - | Return n -> - Return (Mkbetree_be_tree_t self.betree_be_tree_params - self.betree_be_tree_node_id_cnt n) - end + let* n = betree_node_lookup_back self.betree_be_tree_root key st in + Return (Mkbetree_be_tree_t self.betree_be_tree_params + self.betree_be_tree_node_id_cnt n) (** [betree_main::main] *) let main_fwd : result unit = Return () diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 2a336271..201778df 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -20,10 +20,8 @@ let betree_store_internal_node_fwd (id : u64) (content : betree_list_t (u64 & betree_message_t)) (st : state) : result (state & unit) = - begin match betree_utils_store_internal_node_fwd id content st with - | Fail e -> Fail e - | Return (st0, _) -> Return (st0, ()) - end + let* (st0, _) = betree_utils_store_internal_node_fwd id content st in + Return (st0, ()) (** [betree_main::betree::load_leaf_node] *) let betree_load_leaf_node_fwd @@ -35,17 +33,12 @@ let betree_store_leaf_node_fwd (id : u64) (content : betree_list_t (u64 & u64)) (st : state) : result (state & unit) = - begin match betree_utils_store_leaf_node_fwd id content st with - | Fail e -> Fail e - | Return (st0, _) -> Return (st0, ()) - end + let* (st0, _) = betree_utils_store_leaf_node_fwd id content st in + Return (st0, ()) (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_fwd (counter : u64) : result u64 = - begin match u64_add counter 1 with - | Fail e -> Fail e - | Return _ -> Return counter - end + let* _ = u64_add counter 1 in Return counter (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 @@ -57,18 +50,14 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) 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 e -> Fail e - | Return _ -> Return self.betree_node_id_counter_next_node_id - end + let* _ = u64_add self.betree_node_id_counter_next_node_id 1 in + Return self.betree_node_id_counter_next_node_id (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) 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 e -> Fail e - | Return i -> Return (Mkbetree_node_id_counter_t i) - end + let* i = u64_add self.betree_node_id_counter_next_node_id 1 in + Return (Mkbetree_node_id_counter_t i) (** [core::num::u64::{10}::MAX] *) let core_num_u64_max_body : result u64 = Return 18446744073709551615 @@ -86,11 +75,8 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - begin match u64_sub core_num_u64_max_c prev0 with - | Fail e -> Fail e - | Return margin -> - if margin >= v then u64_add prev0 v else Return core_num_u64_max_c - end + let* margin = u64_sub core_num_u64_max_c prev0 in + if margin >= v then u64_add prev0 v else Return core_num_u64_max_c | BetreeUpsertFunStateSub v -> if prev0 >= v then u64_sub prev0 v else Return 0 end @@ -102,11 +88,7 @@ let rec betree_list_len_fwd Tot (result u64) (decreases (betree_list_len_decreases t self)) = begin match self with - | BetreeListCons x tl -> - begin match betree_list_len_fwd t tl with - | Fail e -> Fail e - | Return i -> u64_add 1 i - end + | BetreeListCons x tl -> let* i = betree_list_len_fwd t tl in u64_add 1 i | BetreeListNil -> Return 0 end @@ -121,17 +103,11 @@ let rec betree_list_split_at_fwd else begin match self with | BetreeListCons hd tl -> - begin match u64_sub n 1 with - | Fail e -> Fail e - | Return i -> - begin match betree_list_split_at_fwd t tl i with - | Fail e -> Fail e - | Return p -> - let (ls0, ls1) = p in - let l = ls0 in - Return (BetreeListCons hd l, ls1) - end - end + let* i = u64_sub n 1 in + let* p = betree_list_split_at_fwd t tl i in + let (ls0, ls1) = p in + let l = ls0 in + Return (BetreeListCons hd l, ls1) | BetreeListNil -> Fail Failure end @@ -185,14 +161,11 @@ let rec betree_list_partition_at_pivot_fwd let (i, x) = hd in if i >= pivot then Return (BetreeListNil, BetreeListCons (i, x) tl) - else - begin match betree_list_partition_at_pivot_fwd t tl pivot with - | Fail e -> Fail e - | Return p -> - let (ls0, ls1) = p in - let l = ls0 in - Return (BetreeListCons (i, x) l, ls1) - end + else begin + let* p = betree_list_partition_at_pivot_fwd t tl pivot in + let (ls0, ls1) = p in + let l = ls0 in + Return (BetreeListCons (i, x) l, ls1) end | BetreeListNil -> Return (BetreeListNil, BetreeListNil) end @@ -203,44 +176,22 @@ let betree_leaf_split_fwd (st : state) : result (state & betree_internal_t) = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return p0 -> - let (pivot, _) = p0 in - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match betree_store_leaf_node_fwd id1 content1 st0 with - | Fail e -> Fail e - | Return (st1, _) -> - let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 - params.betree_params_split_size) in - let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 - params.betree_params_split_size) in - Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n - n0) - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* p0 = betree_list_hd_fwd (u64 & u64) content1 in + let (pivot, _) = p0 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in + let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in + let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size) + in + let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size) + in + Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0) (** [betree_main::betree::Leaf::{3}::split] *) let betree_leaf_split_back0 @@ -249,37 +200,17 @@ let betree_leaf_split_back0 (st : state) (st0 : state) : result (state & unit) = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return _ -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* _ = betree_list_hd_fwd (u64 & u64) content1 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in + let* _ = betree_store_leaf_node_fwd id1 content1 st1 in + Return (st0, ()) (** [betree_main::betree::Leaf::{3}::split] *) let betree_leaf_split_back1 @@ -288,37 +219,17 @@ let betree_leaf_split_back1 (st : state) (st0 : state) : result (state & unit) = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return _ -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* _ = betree_list_hd_fwd (u64 & u64) content1 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in + let* _ = betree_store_leaf_node_fwd id1 content1 st1 in + Return (st0, ()) (** [betree_main::betree::Leaf::{3}::split] *) let betree_leaf_split_back2 @@ -327,42 +238,18 @@ let betree_leaf_split_back2 (st : state) (st0 : state) : result (state & betree_node_id_counter_t) = - begin match + let* p = betree_list_split_at_fwd (u64 & u64) content - params.betree_params_split_size with - | Fail e -> Fail e - | Return p -> - let (content0, content1) = p in - begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail e -> Fail e - | Return _ -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id0 -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail e -> Fail e - | Return node_id_cnt0 -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail e -> Fail e - | Return id1 -> - begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail e -> Fail e - | Return _ -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt0 - with - | Fail e -> Fail e - | Return node_id_cnt1 -> Return (st0, node_id_cnt1) - end - end - end - end - end - end - end - end + params.betree_params_split_size in + let (content0, content1) = p in + let* _ = betree_list_hd_fwd (u64 & u64) content1 in + let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in + let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in + let* _ = betree_store_leaf_node_fwd id1 content1 st1 in + let* node_id_cnt1 = betree_node_id_counter_fresh_id_back node_id_cnt0 in + Return (st0, node_id_cnt1) (** [betree_main::betree::Node::{5}::lookup_in_bindings] *) let rec betree_node_lookup_in_bindings_fwd @@ -409,12 +296,10 @@ let rec betree_node_lookup_first_message_for_key_back let (i, m) = x in if i >= key then Return ret - else - begin match - betree_node_lookup_first_message_for_key_back key next_msgs ret with - | Fail e -> Fail e - | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0) - end + else begin + let* next_msgs0 = + betree_node_lookup_first_message_for_key_back key next_msgs ret in + Return (BetreeListCons (i, m) next_msgs0) end | BetreeListNil -> Return ret end @@ -425,43 +310,25 @@ let rec betree_node_apply_upserts_fwd Tot (result (state & u64)) (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 e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msg -> - let (_, m) = msg in - begin match m with - | BetreeMessageInsert i -> Fail Failure - | BetreeMessageDelete -> Fail Failure - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd prev s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msgs0 -> - betree_node_apply_upserts_fwd msgs0 (Some v) key st - end - end - end - end - else - begin match core_option_option_unwrap_fwd u64 prev st with - | 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 e -> Fail e - | Return _ -> Return (st0, v) - end - end - end + let* b = betree_list_head_has_key_fwd betree_message_t msgs key in + if b + then begin + let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in + let (_, m) = msg in + begin match m with + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd prev s in + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in + betree_node_apply_upserts_fwd msgs0 (Some v) key st + end end + else begin + let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in + let* _ = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, + BetreeMessageInsert v) in + Return (st0, v) end (** [betree_main::betree::Node::{5}::apply_upserts] *) let rec betree_node_apply_upserts_back @@ -470,43 +337,25 @@ let rec betree_node_apply_upserts_back Tot (result (state & (betree_list_t (u64 & betree_message_t)))) (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 e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msg -> - let (_, m) = msg in - begin match m with - | BetreeMessageInsert i -> Fail Failure - | BetreeMessageDelete -> Fail Failure - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd prev s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail e -> Fail e - | Return msgs0 -> - betree_node_apply_upserts_back msgs0 (Some v) key st st0 - end - end - end - end - else - begin match core_option_option_unwrap_fwd u64 prev st with - | Fail e -> Fail e - | Return (_, v) -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, - BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs0 -> Return (st0, msgs0) - end - end - end + let* b = betree_list_head_has_key_fwd betree_message_t msgs key in + if b + then begin + let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in + let (_, m) = msg in + begin match m with + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd prev s in + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in + betree_node_apply_upserts_back msgs0 (Some v) key st st0 + end end + else begin + let* (_, v) = core_option_option_unwrap_fwd u64 prev st in + let* msgs0 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, + BetreeMessageInsert v) in + Return (st0, msgs0) end (** [betree_main::betree::Node::{5}::lookup] *) let rec betree_node_lookup_fwd @@ -516,104 +365,60 @@ 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 e -> Fail e - | Return (st0, msgs) -> - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return pending -> - begin match pending with - | BetreeListCons p l -> - let (k, msg) = p in - if k <> key - then - begin match betree_internal_lookup_in_children_fwd node key st0 - with - | 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 e -> Fail e - | Return _ -> Return (st1, opt) - end - end - else - begin match msg with - | BetreeMessageInsert v -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, BetreeMessageInsert v) l) with - | 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 e -> Fail e - | Return _ -> Return (st0, None) - end - | BetreeMessageUpsert ufs -> - begin match betree_internal_lookup_in_children_fwd node key st0 - with - | Fail e -> Fail e - | Return (st1, v) -> - begin match - betree_node_apply_upserts_fwd (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 with - | Fail e -> Fail e - | Return (st2, v0) -> - begin match - betree_internal_lookup_in_children_back node key st0 st2 - with - | Fail e -> Fail e - | Return (st3, node0) -> - begin match - betree_node_apply_upserts_back (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1 st3 with - | Fail e -> Fail e - | Return (st4, pending0) -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - pending0 with - | Fail e -> Fail e - | Return msgs0 -> - begin match - betree_store_internal_node_fwd - node0.betree_internal_id msgs0 st4 with - | Fail e -> Fail e - | Return (st5, _) -> Return (st5, Some v0) - end - end - end - end - end - end - end - | BetreeListNil -> - begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail e -> Fail e - | Return (st1, opt) -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - BetreeListNil with - | Fail e -> Fail e - | Return _ -> Return (st1, opt) - end - end + let* (st0, msgs) = betree_load_internal_node_fwd node.betree_internal_id st + in + let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in + begin match pending with + | BetreeListCons p l -> + let (k, msg) = p in + if k <> key + then begin + let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 + in + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l) in + Return (st1, opt) end + else + begin match msg with + | BetreeMessageInsert v -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l) in + Return (st0, Some v) + | BetreeMessageDelete -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageDelete) l) in + Return (st0, None) + | BetreeMessageUpsert ufs -> + let* (st1, v) = betree_internal_lookup_in_children_fwd node key st0 + in + let* (st2, v0) = + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 in + let* (st3, node0) = + betree_internal_lookup_in_children_back node key st0 st2 in + let* (st4, pending0) = + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1 st3 in + let* msgs0 = + betree_node_lookup_first_message_for_key_back key msgs pending0 in + let* (st5, _) = + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st4 + in + Return (st5, Some v0) end - end + | BetreeListNil -> + let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 in + let* _ = + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in + Return (st1, opt) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st0, bindings) -> - begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return opt -> Return (st0, opt) - end - end + let* (st0, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* opt = betree_node_lookup_in_bindings_fwd key bindings in + Return (st0, opt) end (** [betree_main::betree::Node::{5}::lookup] *) @@ -624,105 +429,61 @@ 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 e -> Fail e - | Return (st1, msgs) -> - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return pending -> - begin match pending with - | BetreeListCons p l -> - let (k, msg) = p in - if k <> key - then - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, msg) l) with - | Fail e -> Fail e - | Return _ -> - begin match - betree_internal_lookup_in_children_back node key st1 st0 with - | Fail e -> Fail e - | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0) - end - end - else - begin match msg with - | BetreeMessageInsert v -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, BetreeMessageInsert v) l) with - | Fail e -> Fail e - | Return _ -> Return (st0, BetreeNodeInternal node) - end - | BetreeMessageDelete -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - (BetreeListCons (k, BetreeMessageDelete) l) with - | Fail e -> Fail e - | Return _ -> Return (st0, BetreeNodeInternal node) - end - | BetreeMessageUpsert ufs -> - begin match betree_internal_lookup_in_children_fwd node key st1 - with - | Fail e -> Fail e - | Return (st2, v) -> - begin match - betree_node_apply_upserts_fwd (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st2 with - | Fail e -> Fail e - | Return (st3, _) -> - begin match - betree_internal_lookup_in_children_back node key st1 st3 - with - | Fail e -> Fail e - | Return (st4, node0) -> - begin match - betree_node_apply_upserts_back (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st2 st4 with - | Fail e -> Fail e - | Return (st5, pending0) -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - pending0 with - | Fail e -> Fail e - | Return msgs0 -> - begin match - betree_store_internal_node_fwd - node0.betree_internal_id msgs0 st5 with - | Fail e -> Fail e - | Return _ -> Return (st0, BetreeNodeInternal node0) - end - end - end - end - end - end - end - | BetreeListNil -> - begin match + let* (st1, msgs) = betree_load_internal_node_fwd node.betree_internal_id st + in + let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in + begin match pending with + | BetreeListCons p l -> + let (k, msg) = p in + if k <> key + then begin + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l) in + let* (st2, node0) = + betree_internal_lookup_in_children_back node key st1 st0 in + Return (st2, BetreeNodeInternal node0) end + else + begin match msg with + | BetreeMessageInsert v -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l) in + Return (st0, BetreeNodeInternal node) + | BetreeMessageDelete -> + let* _ = betree_node_lookup_first_message_for_key_back key msgs - BetreeListNil with - | Fail e -> Fail e - | Return _ -> - begin match - betree_internal_lookup_in_children_back node key st1 st0 with - | Fail e -> Fail e - | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0) - end - end + (BetreeListCons (k, BetreeMessageDelete) l) in + Return (st0, BetreeNodeInternal node) + | BetreeMessageUpsert ufs -> + let* (st2, v) = betree_internal_lookup_in_children_fwd node key st1 + in + let* (st3, _) = + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st2 in + let* (st4, node0) = + betree_internal_lookup_in_children_back node key st1 st3 in + let* (st5, pending0) = + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st2 st4 in + let* msgs0 = + betree_node_lookup_first_message_for_key_back key msgs pending0 in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st5 + in + Return (st0, BetreeNodeInternal node0) end - end + | BetreeListNil -> + let* _ = + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in + let* (st2, node0) = + betree_internal_lookup_in_children_back node key st1 st0 in + Return (st2, BetreeNodeInternal node0) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (_, bindings) -> - begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return _ -> Return (st0, BetreeNodeLeaf node) - end - end + let* (_, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* _ = betree_node_lookup_in_bindings_fwd key bindings in + Return (st0, BetreeNodeLeaf node) end (** [betree_main::betree::Internal::{4}::lookup_in_children] *) @@ -742,22 +503,16 @@ and betree_internal_lookup_in_children_back (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then - begin match betree_node_lookup_back self.betree_internal_left key st st0 - with - | Fail e -> Fail e - | Return (st1, n) -> - Return (st1, 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 st0 - with - | Fail e -> Fail e - | Return (st1, n) -> - Return (st1, Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) - end + then begin + let* (st1, n) = + betree_node_lookup_back self.betree_internal_left key st st0 in + Return (st1, Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right) end + else begin + let* (st1, n) = + betree_node_lookup_back self.betree_internal_right key st st0 in + Return (st1, Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n) end (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -786,11 +541,9 @@ let rec betree_node_lookup_mut_in_bindings_back let (i, i0) = hd in if i >= key then Return ret - else - begin match betree_node_lookup_mut_in_bindings_back key tl ret with - | Fail e -> Fail e - | Return tl0 -> Return (BetreeListCons (i, i0) tl0) - end + else begin + let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in + Return (BetreeListCons (i, i0) tl0) end | BetreeListNil -> Return ret end @@ -800,82 +553,42 @@ let betree_node_apply_to_leaf_fwd_back (new_msg : betree_message_t) : result (betree_list_t (u64 & u64)) = - begin match betree_node_lookup_mut_in_bindings_fwd key bindings with - | Fail e -> Fail e - | Return bindings0 -> - begin match betree_list_head_has_key_fwd u64 bindings0 key with - | Fail e -> Fail e - | Return b -> - if b - then - begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with - | 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 e -> Fail e - | Return bindings1 -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) - with - | Fail e -> Fail e - | Return bindings2 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - end - end - | BetreeMessageDelete -> - begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - | BetreeMessageUpsert s -> - let (_, i) = hd in - begin match betree_upsert_update_fwd (Some i) s with - | Fail e -> Fail e - | Return v -> - begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail e -> Fail e - | Return bindings1 -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, - v) with - | Fail e -> Fail e - | Return bindings2 -> - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 - end - end - end - end - end - else - begin match new_msg with - | BetreeMessageInsert v -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - | BetreeMessageDelete -> - betree_node_lookup_mut_in_bindings_back key bindings bindings0 - | BetreeMessageUpsert s -> - begin match betree_upsert_update_fwd None s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) - with - | Fail e -> Fail e - | Return bindings1 -> - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - end - end + let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in + let* b = betree_list_head_has_key_fwd u64 bindings0 key in + if b + then begin + let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + | BetreeMessageDelete -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageUpsert s -> + let (_, i) = hd in + let* v = betree_upsert_update_fwd (Some i) s in + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + end end + else + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageDelete -> + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd None s in + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end - end (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) let rec betree_node_apply_messages_to_leaf_fwd_back @@ -887,11 +600,8 @@ let rec betree_node_apply_messages_to_leaf_fwd_back 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 e -> Fail e - | Return bindings0 -> - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl - end + let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl | BetreeListNil -> Return bindings end @@ -905,13 +615,11 @@ let rec betree_node_filter_messages_for_key_fwd_back | BetreeListCons p l -> let (k, m) = p in if k = key - then - begin match + then begin + let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, - m) l) with - | Fail e -> Fail e - | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0 - end + m) l) in + betree_node_filter_messages_for_key_fwd_back key msgs0 end else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil end @@ -942,12 +650,10 @@ let rec betree_node_lookup_first_message_after_key_back | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then - begin match - betree_node_lookup_first_message_after_key_back key next_msgs ret with - | Fail e -> Fail e - | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0) - end + then begin + let* next_msgs0 = + betree_node_lookup_first_message_after_key_back key next_msgs ret in + Return (BetreeListCons (k, m) next_msgs0) end else Return ret | BetreeListNil -> Return ret end @@ -958,118 +664,59 @@ let betree_node_apply_to_internal_fwd_back (new_msg : betree_message_t) : result (betree_list_t (u64 & betree_message_t)) = - begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail e -> Fail e - | Return msgs0 -> - begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with - | Fail e -> Fail e - | Return b -> - if b - then - begin match new_msg with - | BetreeMessageInsert i -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 - (key, BetreeMessageInsert i) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs msgs2 - end - end - | BetreeMessageDelete -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 - (key, BetreeMessageDelete) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs msgs2 - end - end - | BetreeMessageUpsert s -> - begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with - | 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 e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs2 - end - end - end - | BetreeMessageDelete -> - begin match betree_upsert_update_fwd None s with - | Fail e -> Fail e - | Return v -> - begin match - betree_list_pop_front_back (u64 & betree_message_t) msgs0 - with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs2 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs2 - end - end - end - | BetreeMessageUpsert ufs -> - begin match - betree_node_lookup_first_message_after_key_fwd key msgs0 with - | Fail e -> Fail e - | Return msgs1 -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) - msgs1 (key, BetreeMessageUpsert s) with - | Fail e -> Fail e - | Return msgs2 -> - begin match - betree_node_lookup_first_message_after_key_back key msgs0 - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> - betree_node_lookup_first_message_for_key_back key msgs - msgs3 - end - end - end - end - end - end - else - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, - new_msg) with - | Fail e -> Fail e - | Return msgs1 -> - betree_node_lookup_first_message_for_key_back key msgs msgs1 - end + let* msgs0 = betree_node_lookup_first_message_for_key_fwd key msgs in + let* b = betree_list_head_has_key_fwd betree_message_t msgs0 key in + if b + then + begin match new_msg with + | BetreeMessageInsert i -> + let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert i) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageDelete -> + let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageDelete) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageUpsert s -> + let* p = betree_list_hd_fwd (u64 & betree_message_t) msgs0 in + let (_, m) = p in + begin match m with + | BetreeMessageInsert prev -> + let* v = betree_upsert_update_fwd (Some prev) s in + let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert v) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageDelete -> + let* v = betree_upsert_update_fwd None s in + let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageInsert v) in + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | BetreeMessageUpsert ufs -> + let* msgs1 = betree_node_lookup_first_message_after_key_fwd key msgs0 + in + let* msgs2 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, + BetreeMessageUpsert s) in + let* msgs3 = + betree_node_lookup_first_message_after_key_back key msgs0 msgs2 in + betree_node_lookup_first_message_for_key_back key msgs msgs3 + end end - end + else begin + let* msgs1 = + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, + new_msg) in + betree_node_lookup_first_message_for_key_back key msgs msgs1 end (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) let rec betree_node_apply_messages_to_internal_fwd_back @@ -1081,11 +728,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back 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 e -> Fail e - | Return msgs0 -> - betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl - end + let* msgs0 = betree_node_apply_to_internal_fwd_back msgs i m in + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl | BetreeListNil -> Return msgs end @@ -1100,85 +744,41 @@ 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 e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_internal_fwd_back content msgs - with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | 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 e -> Fail e - | Return (st1, content1) -> - begin match - betree_internal_flush_back'a node params node_id_cnt content0 - st0 st1 with - | Fail e -> Fail e - | Return (st2, (node0, _)) -> - begin match - betree_store_internal_node_fwd node0.betree_internal_id - content1 st2 with - | Fail e -> Fail e - | Return (st3, _) -> Return (st3, ()) - end - end - end - else - begin match - betree_store_internal_node_fwd node.betree_internal_id content0 - st0 with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end - end + let* (st0, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then begin + let* (st1, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st0 in + let* (st2, (node0, _)) = + betree_internal_flush_back'a node params node_id_cnt content0 st0 st1 + in + let* (st3, _) = + betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in + Return (st3, ()) end + else begin + let* (st1, _) = + betree_store_internal_node_fwd node.betree_internal_id content0 st0 in + Return (st1, ()) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st0, content) -> - begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail e -> Fail e - | Return len -> - begin match u64_mul 2 params.betree_params_split_size with - | 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 e -> Fail e - | Return (st1, _) -> - begin match - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil - st1 with - | Fail e -> Fail e - | Return (st2, _) -> - betree_leaf_split_back0 node content0 params node_id_cnt st0 - st2 - end - end - else - begin match - betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 - with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end - end - end + let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then begin + let* (st1, _) = + betree_leaf_split_fwd node content0 params node_id_cnt st0 in + let* (st2, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in + betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 end + else begin + let* (st1, _) = + betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in + Return (st1, ()) end end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -1192,99 +792,45 @@ and betree_node_apply_messages_back'a = begin match self with | BetreeNodeInternal node -> - begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail e -> Fail e - | Return (st1, content) -> - begin match betree_node_apply_messages_to_internal_fwd_back content msgs - with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | 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 st1 - with - | Fail e -> Fail e - | Return (st2, content1) -> - begin match - betree_internal_flush_back'a node params node_id_cnt content0 - st1 st2 with - | Fail e -> Fail e - | Return (st3, (node0, node_id_cnt0)) -> - begin match - betree_store_internal_node_fwd node0.betree_internal_id - content1 st3 with - | Fail e -> Fail e - | Return _ -> - Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) - end - end - end - else - begin match - betree_store_internal_node_fwd node.betree_internal_id content0 - st1 with - | Fail e -> Fail e - | Return _ -> Return (st0, (BetreeNodeInternal node, node_id_cnt)) - end - end - end - end + let* (st1, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then begin + let* (st2, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st1 in + let* (st3, (node0, node_id_cnt0)) = + betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 + in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in + Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) end + else begin + let* _ = + betree_store_internal_node_fwd node.betree_internal_id content0 st1 in + Return (st0, (BetreeNodeInternal node, node_id_cnt)) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st1, content) -> - begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail e -> Fail e - | Return len -> - begin match u64_mul 2 params.betree_params_split_size with - | Fail e -> Fail e - | Return i -> - if len >= i - then - begin match - betree_leaf_split_fwd node content0 params node_id_cnt st1 with - | Fail e -> Fail e - | Return (st2, new_node) -> - begin match - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil - st2 with - | Fail e -> Fail e - | Return (st3, _) -> - begin match - betree_leaf_split_back0 node content0 params node_id_cnt - st1 st3 with - | Fail e -> Fail e - | Return _ -> - begin match - betree_leaf_split_back2 node content0 params node_id_cnt - st1 st0 with - | Fail e -> Fail e - | Return (st4, node_id_cnt0) -> - Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) - end - end - end - end - else - begin match - betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 - with - | Fail e -> Fail e - | Return _ -> - Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t - node.betree_leaf_id len), node_id_cnt)) - end - end - end - end - end + let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then begin + let* (st2, new_node) = + betree_leaf_split_fwd node content0 params node_id_cnt st1 in + let* (st3, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in + let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 + in + let* (st4, node_id_cnt0) = + betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in + Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) end + else begin + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in + Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), + node_id_cnt)) end end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -1298,93 +844,42 @@ and betree_node_apply_messages_back1 = begin match self with | BetreeNodeInternal node -> - begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail e -> Fail e - | Return (st1, content) -> - begin match betree_node_apply_messages_to_internal_fwd_back content msgs - with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | 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 st1 - with - | Fail e -> Fail e - | Return (st2, content1) -> - begin match - betree_internal_flush_back'a node params node_id_cnt content0 - st1 st2 with - | Fail e -> Fail e - | Return (st3, (node0, _)) -> - begin match - betree_store_internal_node_fwd node0.betree_internal_id - content1 st3 with - | Fail e -> Fail e - | Return _ -> - betree_internal_flush_back1 node params node_id_cnt content0 - st1 st0 - end - end - end - else - begin match - betree_store_internal_node_fwd node.betree_internal_id content0 - st1 with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end - end - end + let* (st1, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then begin + let* (st2, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st1 in + let* (st3, (node0, _)) = + betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 + in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in + betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 end + else begin + let* _ = + betree_store_internal_node_fwd node.betree_internal_id content0 st1 in + Return (st0, ()) end | BetreeNodeLeaf node -> - begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail e -> Fail e - | Return (st1, content) -> - begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail e -> Fail e - | Return content0 -> - begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail e -> Fail e - | Return len -> - begin match u64_mul 2 params.betree_params_split_size with - | Fail e -> Fail e - | Return i -> - if len >= i - then - begin match - betree_leaf_split_fwd node content0 params node_id_cnt st1 with - | Fail e -> Fail e - | Return (st2, _) -> - begin match - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil - st2 with - | Fail e -> Fail e - | Return (st3, _) -> - begin match - betree_leaf_split_back0 node content0 params node_id_cnt - st1 st3 with - | Fail e -> Fail e - | Return _ -> - betree_leaf_split_back1 node content0 params node_id_cnt - st1 st0 - end - end - end - else - begin match - betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 - with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end - end - end - end + let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then begin + let* (st2, _) = + betree_leaf_split_fwd node content0 params node_id_cnt st1 in + let* (st3, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in + let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 + in + betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 end + else begin + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in + Return (st0, ()) end end (** [betree_main::betree::Internal::{4}::flush] *) @@ -1396,84 +891,47 @@ and betree_internal_flush_fwd (decreases ( betree_internal_flush_decreases self params node_id_cnt content st)) = - begin match + let* p = betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | 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 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 e -> Fail e - | Return (st0, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_left params - node_id_cnt msgs_left st st0 with - | Fail e -> Fail e - | Return (st1, (_, node_id_cnt0)) -> - begin match - betree_node_apply_messages_back1 self.betree_internal_left params - node_id_cnt msgs_left st st1 with - | Fail e -> Fail e - | Return (st2, ()) -> - begin match - betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | 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 st2 with - | Fail e -> Fail e - | Return (st3, _) -> - begin match - betree_node_apply_messages_back'a - self.betree_internal_right params node_id_cnt0 - msgs_right st2 st3 with - | Fail e -> Fail e - | Return (st4, (_, _)) -> - begin match - betree_node_apply_messages_back1 - self.betree_internal_right params node_id_cnt0 - msgs_right st2 st4 with - | Fail e -> Fail e - | Return (st5, ()) -> Return (st5, BetreeListNil) - end - end - end - else Return (st2, msgs_right) - end - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_right params - node_id_cnt msgs_right st st0 with - | Fail e -> Fail e - | Return (st1, (_, _)) -> - begin match - betree_node_apply_messages_back1 self.betree_internal_right - params node_id_cnt msgs_right st st1 with - | Fail e -> Fail e - | Return (st2, ()) -> Return (st2, msgs_left) - end - end - end - end - end + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then begin + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (st1, (_, node_id_cnt0)) = + betree_node_apply_messages_back'a self.betree_internal_left params + node_id_cnt msgs_left st st0 in + let* (st2, ()) = + betree_node_apply_messages_back1 self.betree_internal_left params + node_id_cnt msgs_left st st1 in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then begin + let* (st3, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st2 in + let* (st4, (_, _)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt0 msgs_right st2 st3 in + let* (st5, ()) = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt0 msgs_right st2 st4 in + Return (st5, BetreeListNil) end + else Return (st2, msgs_right) end + else begin + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st in + let* (st1, (_, _)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt msgs_right st st0 in + let* (st2, ()) = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt msgs_right st st1 in + Return (st2, msgs_left) end (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back'a @@ -1485,93 +943,53 @@ and betree_internal_flush_back'a (decreases ( betree_internal_flush_decreases self params node_id_cnt content st)) = - begin match + let* p = betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | 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 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 e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_left params - node_id_cnt msgs_left st st1 with - | Fail e -> Fail e - | Return (st2, (n, node_id_cnt0)) -> - begin match - betree_node_apply_messages_back1 self.betree_internal_left params - node_id_cnt msgs_left st st2 with - | Fail e -> Fail e - | Return (st3, ()) -> - begin match - betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | 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 st3 with - | Fail e -> Fail e - | Return (st4, _) -> - begin match - betree_node_apply_messages_back'a - self.betree_internal_right params node_id_cnt0 - msgs_right st3 st4 with - | Fail e -> Fail e - | Return (st5, (n0, node_id_cnt1)) -> - begin match - betree_node_apply_messages_back1 - self.betree_internal_right params node_id_cnt0 - msgs_right st3 st5 with - | Fail e -> Fail e - | Return _ -> - Return (st0, (Mkbetree_internal_t - self.betree_internal_id self.betree_internal_pivot n - n0, node_id_cnt1)) - end - end - end - else - Return (st0, (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right, - node_id_cnt0)) - end - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_right params - node_id_cnt msgs_right st st1 with - | Fail e -> Fail e - | Return (st2, (n, node_id_cnt0)) -> - begin match - 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, (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n, - node_id_cnt0)) - end - end - end + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then begin + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (st2, (n, node_id_cnt0)) = + betree_node_apply_messages_back'a self.betree_internal_left params + node_id_cnt msgs_left st st1 in + let* (st3, ()) = + betree_node_apply_messages_back1 self.betree_internal_left params + node_id_cnt msgs_left st st2 in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then begin + let* (st4, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st3 in + let* (st5, (n0, node_id_cnt1)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt0 msgs_right st3 st4 in + let* _ = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt0 msgs_right st3 st5 in + Return (st0, (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n n0, node_id_cnt1)) end + else + Return (st0, (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0)) + end + else begin + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st in + let* (st2, (n, node_id_cnt0)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt msgs_right st st1 in + let* _ = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt msgs_right st st2 in + Return (st0, (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)) end - end (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back1 @@ -1583,84 +1001,47 @@ and betree_internal_flush_back1 (decreases ( betree_internal_flush_decreases self params node_id_cnt content st)) = - begin match + let* p = betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | 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 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 e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_left params - node_id_cnt msgs_left st st1 with - | Fail e -> Fail e - | Return (st2, (_, node_id_cnt0)) -> - begin match - betree_node_apply_messages_back1 self.betree_internal_left params - node_id_cnt msgs_left st st2 with - | Fail e -> Fail e - | Return (st3, ()) -> - begin match - betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | 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 st3 with - | Fail e -> Fail e - | Return (st4, _) -> - begin match - betree_node_apply_messages_back'a - self.betree_internal_right params node_id_cnt0 - msgs_right st3 st4 with - | Fail e -> Fail e - | Return (st5, (_, _)) -> - begin match - betree_node_apply_messages_back1 - self.betree_internal_right params node_id_cnt0 - msgs_right st3 st5 with - | Fail e -> Fail e - | Return _ -> Return (st0, ()) - end - end - end - else Return (st0, ()) - end - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self.betree_internal_right params - node_id_cnt msgs_right st st1 with - | Fail e -> Fail e - | Return (st2, (_, _)) -> - begin match - 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, ()) - end - end - end - end - end + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then begin + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (st2, (_, node_id_cnt0)) = + betree_node_apply_messages_back'a self.betree_internal_left params + node_id_cnt msgs_left st st1 in + let* (st3, ()) = + betree_node_apply_messages_back1 self.betree_internal_left params + node_id_cnt msgs_left st st2 in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then begin + let* (st4, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st3 in + let* (st5, (_, _)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt0 msgs_right st3 st4 in + let* _ = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt0 msgs_right st3 st5 in + Return (st0, ()) end + else Return (st0, ()) end + else begin + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st in + let* (st2, (_, _)) = + betree_node_apply_messages_back'a self.betree_internal_right params + node_id_cnt msgs_right st st1 in + let* _ = + betree_node_apply_messages_back1 self.betree_internal_right params + node_id_cnt msgs_right st st2 in + Return (st0, ()) end (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -1670,20 +1051,14 @@ let betree_node_apply_fwd result (state & unit) = let l = BetreeListNil in - begin match + let* (st0, _) = betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons - (key, new_msg) l) st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match - betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons - (key, new_msg) l) st st0 with - | Fail e -> Fail e - | Return (st1, (_, _)) -> - betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons - (key, new_msg) l) st st1 - end - end + (key, new_msg) l) st in + let* (st1, (_, _)) = + betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st0 in + betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st1 (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_back'a @@ -1693,24 +1068,16 @@ let betree_node_apply_back'a result (state & (betree_node_t & betree_node_id_counter_t)) = let l = BetreeListNil in - begin match + let* (st1, _) = betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons - (key, new_msg) l) st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons - (key, new_msg) l) st st1 with - | Fail e -> Fail e - | Return (st2, (self0, node_id_cnt0)) -> - begin match - 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)) - end - end - end + (key, new_msg) l) st in + let* (st2, (self0, node_id_cnt0)) = + betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st1 in + let* _ = + betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st2 in + Return (st0, (self0, node_id_cnt0)) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_back1 @@ -1720,70 +1087,43 @@ let betree_node_apply_back1 result (state & unit) = let l = BetreeListNil in - begin match + let* (st1, _) = betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons - (key, new_msg) l) st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons - (key, new_msg) l) st st1 with - | Fail e -> Fail e - | Return (st2, (_, _)) -> - begin match - 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, ()) - end - end - end + (key, new_msg) l) st in + let* (st2, (_, _)) = + betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st1 in + let* _ = + betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st2 in + Return (st0, ()) (** [betree_main::betree::BeTree::{6}::new] *) let betree_be_tree_new_fwd (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_be_tree_t) = - begin match betree_node_id_counter_new_fwd with - | Fail e -> Fail e - | Return node_id_cnt -> - begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail e -> Fail e - | Return id -> - begin match betree_store_leaf_node_fwd id BetreeListNil st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | 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))) - end - end - end - end + let* node_id_cnt = betree_node_id_counter_new_fwd in + let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in + let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in + let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in + Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size) + node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0))) (** [betree_main::betree::BeTree::{6}::apply] *) let betree_be_tree_apply_fwd (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) : result (state & unit) = - begin match + let* (st0, _) = 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 e -> Fail e - | Return (st0, _) -> - begin match - betree_node_apply_back'a self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - st0 with - | Fail e -> Fail e - | Return (st1, (_, _)) -> - betree_node_apply_back1 self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - st1 - end - end + self.betree_be_tree_node_id_cnt key msg st in + let* (st1, (_, _)) = + betree_node_apply_back'a self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st0 + in + betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params + self.betree_be_tree_node_id_cnt key msg st st1 (** [betree_main::betree::BeTree::{6}::apply] *) let betree_be_tree_apply_back @@ -1791,44 +1131,28 @@ let betree_be_tree_apply_back (st0 : state) : result (state & betree_be_tree_t) = - begin match + let* (st1, _) = 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 e -> Fail e - | Return (st1, _) -> - begin match - betree_node_apply_back'a self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - st1 with - | Fail e -> Fail e - | Return (st2, (n, nic)) -> - begin match - betree_node_apply_back1 self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - st2 with - | Fail e -> Fail e - | Return _ -> - Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n) - end - end - end + self.betree_be_tree_node_id_cnt key msg st in + let* (st2, (n, nic)) = + betree_node_apply_back'a self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st1 + in + let* _ = + betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params + self.betree_be_tree_node_id_cnt key msg st st2 in + Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n) (** [betree_main::betree::BeTree::{6}::insert] *) 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_apply_fwd self key (BetreeMessageInsert value) st - with - | Fail e -> Fail e - | Return (st0, _) -> - begin match - betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0 - with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end + let* (st0, _) = + betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st in + let* (st1, _) = + betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0 in + Return (st1, ()) (** [betree_main::betree::BeTree::{6}::insert] *) let betree_be_tree_insert_back @@ -1836,45 +1160,29 @@ let betree_be_tree_insert_back (st0 : state) : result (state & betree_be_tree_t) = - begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st - with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1 - with - | Fail e -> Fail e - | Return (_, self0) -> Return (st0, self0) - end - end + let* (st1, _) = + betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st in + let* (_, self0) = + betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1 in + Return (st0, self0) (** [betree_main::betree::BeTree::{6}::delete] *) 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 e -> Fail e - | Return (st0, _) -> - begin match betree_be_tree_apply_back self key BetreeMessageDelete st st0 - with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end + let* (st0, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in + let* (st1, _) = betree_be_tree_apply_back self key BetreeMessageDelete st st0 + in + Return (st1, ()) (** [betree_main::betree::BeTree::{6}::delete] *) let betree_be_tree_delete_back (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_be_tree_t) = - begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match betree_be_tree_apply_back self key BetreeMessageDelete st st1 - with - | Fail e -> Fail e - | Return (_, self0) -> Return (st0, self0) - end - end + let* (st1, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in + let* (_, self0) = + betree_be_tree_apply_back self key BetreeMessageDelete st st1 in + Return (st0, self0) (** [betree_main::betree::BeTree::{6}::upsert] *) let betree_be_tree_upsert_fwd @@ -1882,16 +1190,11 @@ let betree_be_tree_upsert_fwd (st : state) : result (state & unit) = - begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st - with - | Fail e -> Fail e - | Return (st0, _) -> - begin match - betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end + let* (st0, _) = + betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st in + let* (st1, _) = + betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 in + Return (st1, ()) (** [betree_main::betree::BeTree::{6}::upsert] *) let betree_be_tree_upsert_back @@ -1899,16 +1202,11 @@ let betree_be_tree_upsert_back (st : state) (st0 : state) : result (state & betree_be_tree_t) = - begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st - with - | Fail e -> Fail e - | Return (st1, _) -> - begin match - betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 with - | Fail e -> Fail e - | Return (_, self0) -> Return (st0, self0) - end - end + let* (st1, _) = + betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st in + let* (_, self0) = + betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 in + Return (st0, self0) (** [betree_main::betree::BeTree::{6}::lookup] *) let betree_be_tree_lookup_fwd @@ -1922,12 +1220,10 @@ let betree_be_tree_lookup_back (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_be_tree_t) = - begin match betree_node_lookup_back self.betree_be_tree_root key st st0 with - | Fail e -> Fail e - | Return (st1, n) -> - Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params - self.betree_be_tree_node_id_cnt n) - end + let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0 + in + Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params + self.betree_be_tree_node_id_cnt n) (** [betree_main::main] *) let main_fwd : result unit = Return () diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 68bda221..0140aadc 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -17,15 +17,10 @@ let rec hash_map_allocate_slots_loop_fwd (decreases (hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then - begin match vec_push_back (list_t t) slots ListNil with - | Fail e -> Fail e - | Return slots0 -> - begin match usize_sub n 1 with - | Fail e -> Fail e - | Return n0 -> hash_map_allocate_slots_loop_fwd t slots0 n0 - end - end + then begin + let* slots0 = vec_push_back (list_t t) slots ListNil in + let* n0 = usize_sub n 1 in + hash_map_allocate_slots_loop_fwd t slots0 n0 end else Return slots (** [hashmap::HashMap::{0}::allocate_slots] *) @@ -40,19 +35,10 @@ let hash_map_new_with_capacity_fwd result (hash_map_t t) = let v = vec_new (list_t t) in - begin match hash_map_allocate_slots_fwd t v capacity with - | Fail e -> Fail e - | Return slots -> - begin match usize_mul capacity max_load_dividend with - | Fail e -> Fail e - | Return i -> - begin match usize_div i max_load_divisor with - | Fail e -> Fail e - | Return i0 -> - Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots) - end - end - end + let* slots = hash_map_allocate_slots_fwd t v capacity in + let* i = usize_mul capacity max_load_dividend in + let* i0 = usize_div i max_load_divisor in + Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots) (** [hashmap::HashMap::{0}::new] *) let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = @@ -66,26 +52,18 @@ let rec hash_map_clear_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - begin match vec_index_mut_back (list_t t) slots i ListNil with - | Fail e -> Fail e - | Return slots0 -> hash_map_clear_loop_fwd_back t slots0 i1 - end - end + then begin + let* i1 = usize_add i 1 in + let* slots0 = vec_index_mut_back (list_t t) slots i ListNil in + hash_map_clear_loop_fwd_back t slots0 i1 end else Return slots (** [hashmap::HashMap::{0}::clear] *) let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = - begin match hash_map_clear_loop_fwd_back t self.hash_map_slots 0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load - v) - end + let* v = hash_map_clear_loop_fwd_back t self.hash_map_slots 0 in + Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load + v) (** [hashmap::HashMap::{0}::len] *) let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize = @@ -120,11 +98,9 @@ let rec hash_map_insert_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey value tl) - else - begin match hash_map_insert_in_list_loop_back t key value tl with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons ckey cvalue tl0) - end + else begin + let* tl0 = hash_map_insert_in_list_loop_back t key value tl in + Return (ListCons ckey cvalue tl0) end | ListNil -> let l = ListNil in Return (ListCons key value l) end @@ -138,55 +114,23 @@ let hash_map_insert_no_resize_fwd_back (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : result (hash_map_t t) = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> - begin match hash_map_insert_in_list_fwd t key value l with - | Fail e -> Fail e - | Return inserted -> - if inserted - then - begin match usize_add self.hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hash_map_insert_in_list_back t key value l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 - with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t i0 self.hash_map_max_load_factor - self.hash_map_max_load v) - end - end - end - else - begin match hash_map_insert_in_list_back t key value l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 - with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load v) - end - end - end - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in + let* inserted = hash_map_insert_in_list_fwd t key value l in + if inserted + then begin + let* i0 = usize_add self.hash_map_num_entries 1 in + let* l0 = hash_map_insert_in_list_back t key value l in + let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in + Return (Mkhash_map_t i0 self.hash_map_max_load_factor + self.hash_map_max_load v) end + else begin + let* l0 = hash_map_insert_in_list_back t key value l in + let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in + Return (Mkhash_map_t self.hash_map_num_entries + self.hash_map_max_load_factor self.hash_map_max_load v) end (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -200,11 +144,8 @@ let rec hash_map_move_elements_from_list_loop_fwd_back = begin match ls with | ListCons k v tl -> - begin match hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail e -> Fail e - | Return ntable0 -> - hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl - end + let* ntable0 = hash_map_insert_no_resize_fwd_back t ntable k v in + hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl | ListNil -> Return ntable end @@ -221,26 +162,14 @@ let rec hash_map_move_elements_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then - begin match vec_index_mut_fwd (list_t t) slots i with - | Fail e -> Fail e - | Return l -> - let ls = mem_replace_fwd (list_t t) l ListNil in - begin match hash_map_move_elements_from_list_fwd_back t ntable ls with - | Fail e -> Fail e - | Return ntable0 -> - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - let l0 = mem_replace_back (list_t t) l ListNil in - begin match vec_index_mut_back (list_t t) slots i l0 with - | Fail e -> Fail e - | Return slots0 -> - hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 - end - end - end - end + then begin + let* l = vec_index_mut_fwd (list_t t) slots i in + let ls = mem_replace_fwd (list_t t) l ListNil in + let* ntable0 = hash_map_move_elements_from_list_fwd_back t ntable ls in + let* i1 = usize_add i 1 in + let l0 = mem_replace_back (list_t t) l ListNil in + let* slots0 = vec_index_mut_back (list_t t) slots i l0 in + hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end else Return (ntable, slots) (** [hashmap::HashMap::{0}::move_elements] *) @@ -253,58 +182,33 @@ let hash_map_move_elements_fwd_back (** [hashmap::HashMap::{0}::try_resize] *) let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = - begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail e -> Fail e - | Return max_usize -> - let capacity = vec_len (list_t t) self.hash_map_slots in - begin match usize_div max_usize 2 with - | Fail e -> Fail e - | Return n1 -> - let (i, i0) = self.hash_map_max_load_factor in - begin match usize_div n1 i with - | Fail e -> Fail e - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail e -> Fail e - | Return i2 -> - begin match hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail e -> Fail e - | Return ntable -> - begin match - hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 - with - | Fail e -> Fail e - | Return (ntable0, _) -> - Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - ntable0.hash_map_max_load ntable0.hash_map_slots) - end - end - end - else - Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - self.hash_map_max_load self.hash_map_slots) - end - end - end + let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in + let capacity = vec_len (list_t t) self.hash_map_slots in + let* n1 = usize_div max_usize 2 in + let (i, i0) = self.hash_map_max_load_factor in + let* i1 = usize_div n1 i in + if capacity <= i1 + then begin + let* i2 = usize_mul capacity 2 in + let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in + let* (ntable0, _) = + hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) + ntable0.hash_map_max_load ntable0.hash_map_slots) end + else + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) + self.hash_map_max_load self.hash_map_slots) (** [hashmap::HashMap::{0}::insert] *) let hash_map_insert_fwd_back (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : result (hash_map_t t) = - begin match hash_map_insert_no_resize_fwd_back t self key value with - | Fail e -> Fail e - | Return self0 -> - begin match hash_map_len_fwd t self0 with - | Fail e -> Fail e - | Return i -> - if i > self0.hash_map_max_load - then hash_map_try_resize_fwd_back t self0 - else Return self0 - end - end + let* self0 = hash_map_insert_no_resize_fwd_back t self key value in + let* i = hash_map_len_fwd t self0 in + if i > self0.hash_map_max_load + then hash_map_try_resize_fwd_back t self0 + else Return self0 (** [hashmap::HashMap::{0}::contains_key_in_list] *) let rec hash_map_contains_key_in_list_loop_fwd @@ -328,19 +232,11 @@ let hash_map_contains_key_in_list_fwd (** [hashmap::HashMap::{0}::contains_key] *) let hash_map_contains_key_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result bool = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail e -> Fail e - | Return l -> hash_map_contains_key_in_list_fwd t key l - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in + hash_map_contains_key_in_list_fwd t key l (** [hashmap::HashMap::{0}::get_in_list] *) let rec hash_map_get_in_list_loop_fwd @@ -363,19 +259,11 @@ let hash_map_get_in_list_fwd (** [hashmap::HashMap::{0}::get] *) let hash_map_get_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail e -> Fail e - | Return l -> hash_map_get_in_list_fwd t key l - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in + hash_map_get_in_list_fwd t key l (** [hashmap::HashMap::{0}::get_mut_in_list] *) let rec hash_map_get_mut_in_list_loop_fwd @@ -405,11 +293,9 @@ let rec hash_map_get_mut_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey ret tl) - else - begin match hash_map_get_mut_in_list_loop_back t tl key ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons ckey cvalue tl0) - end + else begin + let* tl0 = hash_map_get_mut_in_list_loop_back t tl key ret in + Return (ListCons ckey cvalue tl0) end | ListNil -> Fail Failure end @@ -421,51 +307,25 @@ let hash_map_get_mut_in_list_back (** [hashmap::HashMap::{0}::get_mut] *) let hash_map_get_mut_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> hash_map_get_mut_in_list_fwd t l key - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in + hash_map_get_mut_in_list_fwd t l key (** [hashmap::HashMap::{0}::get_mut] *) let hash_map_get_mut_back (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) : result (hash_map_t t) = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> - begin match hash_map_get_mut_in_list_back t l key ret with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load v) - end - end - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in + let* l0 = hash_map_get_mut_in_list_back t l key ret in + let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in + Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor + self.hash_map_max_load v) (** [hashmap::HashMap::{0}::remove_from_list] *) let rec hash_map_remove_from_list_loop_fwd @@ -506,11 +366,9 @@ let rec hash_map_remove_from_list_loop_back | ListCons i cvalue tl0 -> Return tl0 | ListNil -> Fail Failure end - else - begin match hash_map_remove_from_list_loop_back t key tl with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons ckey x tl0) - end + else begin + let* tl0 = hash_map_remove_from_list_loop_back t key tl in + Return (ListCons ckey x tl0) end | ListNil -> Return ListNil end @@ -522,164 +380,74 @@ let hash_map_remove_from_list_back (** [hashmap::HashMap::{0}::remove] *) let hash_map_remove_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> - begin match hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Return None - | Some x0 -> - begin match usize_sub self.hash_map_num_entries 1 with - | Fail e -> Fail e - | Return _ -> Return (Some x0) - end - end - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in + let* x = hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> Return None + | Some x0 -> + let* _ = usize_sub self.hash_map_num_entries 1 in Return (Some x0) end (** [hashmap::HashMap::{0}::remove] *) let hash_map_remove_back (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) = - begin match hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (list_t t) self.hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> - begin match hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> - begin match hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 - with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load v) - end - end - | Some x0 -> - begin match usize_sub self.hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 - with - | Fail e -> Fail e - | Return v -> - Return (Mkhash_map_t i0 self.hash_map_max_load_factor - self.hash_map_max_load v) - end - end - end - end - end - end - end + let* hash = hash_key_fwd key in + let i = vec_len (list_t t) self.hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in + let* x = hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> + let* l0 = hash_map_remove_from_list_back t key l in + let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in + Return (Mkhash_map_t self.hash_map_num_entries + self.hash_map_max_load_factor self.hash_map_max_load v) + | Some x0 -> + let* i0 = usize_sub self.hash_map_num_entries 1 in + let* l0 = hash_map_remove_from_list_back t key l in + let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in + Return (Mkhash_map_t i0 self.hash_map_max_load_factor + self.hash_map_max_load v) end (** [hashmap::test1] *) let test1_fwd : result unit = - begin match hash_map_new_fwd u64 with - | Fail e -> Fail e - | Return hm -> - begin match hash_map_insert_fwd_back u64 hm 0 42 with - | Fail e -> Fail e - | Return hm0 -> - begin match hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail e -> Fail e - | Return hm1 -> - begin match hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail e -> Fail e - | Return hm2 -> - begin match hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail e -> Fail e - | Return hm3 -> - begin match hash_map_get_fwd u64 hm3 128 with - | Fail e -> Fail e - | Return i -> - if not (i = 18) - then Fail Failure - else - begin match hash_map_get_mut_back u64 hm3 1024 56 with - | Fail e -> Fail e - | Return hm4 -> - begin match hash_map_get_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return i0 -> - if not (i0 = 56) - then Fail Failure - else - begin match hash_map_remove_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Fail Failure - | Some x0 -> - if not (x0 = 56) - then Fail Failure - else - begin match hash_map_remove_back u64 hm4 1024 with - | Fail e -> Fail e - | Return hm5 -> - begin match hash_map_get_fwd u64 hm5 0 with - | Fail e -> Fail e - | Return i1 -> - if not (i1 = 42) - then Fail Failure - else - begin match hash_map_get_fwd u64 hm5 128 with - | Fail e -> Fail e - | Return i2 -> - if not (i2 = 18) - then Fail Failure - else - begin match hash_map_get_fwd u64 hm5 1056 - with - | Fail e -> Fail e - | Return i3 -> - if not (i3 = 256) - then Fail Failure - else Return () - end - end - end - end - end - end - end - end - end - end - end - end - end - end + let* hm = hash_map_new_fwd u64 in + let* hm0 = hash_map_insert_fwd_back u64 hm 0 42 in + let* hm1 = hash_map_insert_fwd_back u64 hm0 128 18 in + let* hm2 = hash_map_insert_fwd_back u64 hm1 1024 138 in + let* hm3 = hash_map_insert_fwd_back u64 hm2 1056 256 in + let* i = hash_map_get_fwd u64 hm3 128 in + if not (i = 18) + then Fail Failure + else begin + let* hm4 = hash_map_get_mut_back u64 hm3 1024 56 in + let* i0 = hash_map_get_fwd u64 hm4 1024 in + if not (i0 = 56) + then Fail Failure + else begin + let* x = hash_map_remove_fwd u64 hm4 1024 in + begin match x with + | None -> Fail Failure + | Some x0 -> + if not (x0 = 56) + then Fail Failure + else begin + let* hm5 = hash_map_remove_back u64 hm4 1024 in + let* i1 = hash_map_get_fwd u64 hm5 0 in + if not (i1 = 42) + then Fail Failure + else begin + let* i2 = hash_map_get_fwd u64 hm5 128 in + if not (i2 = 18) + then Fail Failure + else begin + let* i3 = hash_map_get_fwd u64 hm5 1056 in + if not (i3 = 256) then Fail Failure else Return () end end end + end end end (** Unit test for [hashmap::test1] *) let _ = assert_norm (test1_fwd = Return ()) diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 56cff453..51021daf 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -18,15 +18,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then - begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with - | Fail e -> Fail e - | Return slots0 -> - begin match usize_sub n 1 with - | Fail e -> Fail e - | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 - end - end + then begin + let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in + let* n0 = usize_sub n 1 in + hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end else Return slots (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) @@ -43,20 +38,11 @@ let hashmap_hash_map_new_with_capacity_fwd result (hashmap_hash_map_t t) = let v = vec_new (hashmap_list_t t) in - begin match hashmap_hash_map_allocate_slots_fwd t v capacity with - | Fail e -> Fail e - | Return slots -> - begin match usize_mul capacity max_load_dividend with - | Fail e -> Fail e - | Return i -> - begin match usize_div i max_load_divisor with - | Fail e -> Fail e - | Return i0 -> - Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 - slots) - end - end - end + let* slots = hashmap_hash_map_allocate_slots_fwd t v capacity in + let* i = usize_mul capacity max_load_dividend in + let* i0 = usize_div i max_load_divisor in + Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 + slots) (** [hashmap_main::hashmap::HashMap::{0}::new] *) let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = @@ -70,28 +56,20 @@ let rec hashmap_hash_map_clear_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil - with - | Fail e -> Fail e - | Return slots0 -> hashmap_hash_map_clear_loop_fwd_back t slots0 i1 - end - end + then begin + let* i1 = usize_add i 1 in + let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil + in + hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end else Return slots (** [hashmap_main::hashmap::HashMap::{0}::clear] *) let hashmap_hash_map_clear_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match - hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end + let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 + in + Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -127,11 +105,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey value tl) - else - begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) - end + else begin + let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in + Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) end @@ -148,59 +124,30 @@ let hashmap_hash_map_insert_no_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_insert_in_list_fwd t key value l with - | Fail e -> Fail e - | Return inserted -> - if inserted - then - begin match usize_add self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hashmap_hash_map_insert_in_list_back t key value l - with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - else - begin match hashmap_hash_map_insert_in_list_back t key value l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in + if inserted + then begin + let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in + let* l0 = hashmap_hash_map_insert_in_list_back t key value l in + let* v = + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod l0 in + Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) end + else begin + let* l0 = hashmap_hash_map_insert_in_list_back t key value l in + let* v = + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod l0 in + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) end - end (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -215,11 +162,8 @@ let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back = begin match ls with | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail e -> Fail e - | Return ntable0 -> - hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl - end + let* ntable0 = hashmap_hash_map_insert_no_resize_fwd_back t ntable k v in + hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl | HashmapListNil -> Return ntable end @@ -239,27 +183,15 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then - begin match vec_index_mut_fwd (hashmap_list_t t) slots i with - | Fail e -> Fail e - | Return l -> - let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls - with - | Fail e -> Fail e - | Return ntable0 -> - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with - | Fail e -> Fail e - | Return slots0 -> - hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 - end - end - end - end + then begin + let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in + let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in + let* ntable0 = + hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls in + let* i1 = usize_add i 1 in + let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in + hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end else Return (ntable, slots) (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) @@ -273,59 +205,34 @@ let hashmap_hash_map_move_elements_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) let hashmap_hash_map_try_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail e -> Fail e - | Return max_usize -> - let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_div max_usize 2 with - | Fail e -> Fail e - | Return n1 -> - let (i, i0) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i with - | Fail e -> Fail e - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail e -> Fail e - | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail e -> Fail e - | Return ntable -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable - self.hashmap_hash_map_slots 0 with - | Fail e -> Fail e - | Return (ntable0, _) -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - (i, i0) ntable0.hashmap_hash_map_max_load - ntable0.hashmap_hash_map_slots) - end - end - end - else - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, - i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) - end - end - end + let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in + let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* n1 = usize_div max_usize 2 in + let (i, i0) = self.hashmap_hash_map_max_load_factor in + let* i1 = usize_div n1 i in + if capacity <= i1 + then begin + let* i2 = usize_mul capacity 2 in + let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in + let* (ntable0, _) = + hashmap_hash_map_move_elements_fwd_back t ntable + self.hashmap_hash_map_slots 0 in + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end + else + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with - | Fail e -> Fail e - | Return self0 -> - begin match hashmap_hash_map_len_fwd t self0 with - | Fail e -> Fail e - | Return i -> - if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back t self0 - else Return self0 - end - end + let* self0 = hashmap_hash_map_insert_no_resize_fwd_back t self key value in + let* i = hashmap_hash_map_len_fwd t self0 in + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back t self0 + else Return self0 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) let rec hashmap_hash_map_contains_key_in_list_loop_fwd @@ -349,21 +256,12 @@ let hashmap_hash_map_contains_key_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) let hashmap_hash_map_contains_key_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_contains_key_in_list_fwd t key l (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) let rec hashmap_hash_map_get_in_list_loop_fwd @@ -387,21 +285,12 @@ let hashmap_hash_map_get_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::get] *) let hashmap_hash_map_get_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_get_in_list_fwd t key l - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_get_in_list_fwd t key l (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) let rec hashmap_hash_map_get_mut_in_list_loop_fwd @@ -432,11 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey ret tl) - else - begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) - end + else begin + let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in + Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> Fail Failure end @@ -450,55 +337,31 @@ let hashmap_hash_map_get_mut_in_list_back (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_get_mut_in_list_fwd t l key - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + hashmap_hash_map_get_mut_in_list_fwd t l key (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_get_mut_in_list_back t l key ret with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* l0 = hashmap_hash_map_get_mut_in_list_back t l key ret in + let* v = + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + l0 in + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -543,11 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back | HashmapListCons i cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end - else - begin match hashmap_hash_map_remove_from_list_loop_back t key tl with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey x tl0) - end + else begin + let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in + Return (HashmapListCons ckey x tl0) end | HashmapListNil -> Return HashmapListNil end @@ -561,32 +422,17 @@ let hashmap_hash_map_remove_from_list_back (** [hashmap_main::hashmap::HashMap::{0}::remove] *) let hashmap_hash_map_remove_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Return None - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return _ -> Return (Some x0) - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* x = hashmap_hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> Return None + | Some x0 -> + let* _ = usize_sub self.hashmap_hash_map_num_entries 1 in Return (Some x0) end (** [hashmap_main::hashmap::HashMap::{0}::remove] *) @@ -594,141 +440,66 @@ let hashmap_hash_map_remove_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* x = hashmap_hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> + let* l0 = hashmap_hash_map_remove_from_list_back t key l in + let* v = + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod l0 in + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + | Some x0 -> + let* i0 = usize_sub self.hashmap_hash_map_num_entries 1 in + let* l0 = hashmap_hash_map_remove_from_list_back t key l in + let* v = + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod l0 in + Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) end (** [hashmap_main::hashmap::test1] *) let hashmap_test1_fwd : result unit = - begin match hashmap_hash_map_new_fwd u64 with - | Fail e -> Fail e - | Return hm -> - begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with - | Fail e -> Fail e - | Return hm0 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail e -> Fail e - | Return hm1 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail e -> Fail e - | Return hm2 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail e -> Fail e - | Return hm3 -> - begin match hashmap_hash_map_get_fwd u64 hm3 128 with - | Fail e -> Fail e - | Return i -> - if not (i = 18) - then Fail Failure - else - begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with - | Fail e -> Fail e - | Return hm4 -> - begin match hashmap_hash_map_get_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return i0 -> - if not (i0 = 56) - then Fail Failure - else - begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Fail Failure - | Some x0 -> - if not (x0 = 56) - then Fail Failure - else - begin match - hashmap_hash_map_remove_back u64 hm4 1024 with - | Fail e -> Fail e - | Return hm5 -> - begin match hashmap_hash_map_get_fwd u64 hm5 0 - with - | Fail e -> Fail e - | Return i1 -> - if not (i1 = 42) - then Fail Failure - else - begin match - hashmap_hash_map_get_fwd u64 hm5 128 with - | Fail e -> Fail e - | Return i2 -> - if not (i2 = 18) - then Fail Failure - else - begin match - hashmap_hash_map_get_fwd u64 hm5 1056 - with - | Fail e -> Fail e - | Return i3 -> - if not (i3 = 256) - then Fail Failure - else Return () - end - end - end - end - end - end - end - end - end - end - end - end - end - end + let* hm = hashmap_hash_map_new_fwd u64 in + let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm 0 42 in + let* hm1 = hashmap_hash_map_insert_fwd_back u64 hm0 128 18 in + let* hm2 = hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 in + let* hm3 = hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 in + let* i = hashmap_hash_map_get_fwd u64 hm3 128 in + if not (i = 18) + then Fail Failure + else begin + let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in + let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in + if not (i0 = 56) + then Fail Failure + else begin + let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in + begin match x with + | None -> Fail Failure + | Some x0 -> + if not (x0 = 56) + then Fail Failure + else begin + let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in + let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in + if not (i1 = 42) + then Fail Failure + else begin + let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in + if not (i2 = 18) + then Fail Failure + else begin + let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in + if not (i3 = 256) then Fail Failure else Return () end end end + end end end (** Unit test for [hashmap_main::hashmap::test1] *) let _ = assert_norm (hashmap_test1_fwd = Return ()) @@ -736,18 +507,10 @@ let _ = assert_norm (hashmap_test1_fwd = Return ()) (** [hashmap_main::insert_on_disk] *) let insert_on_disk_fwd (key : usize) (value : u64) (st : state) : result (state & unit) = - begin match hashmap_utils_deserialize_fwd st with - | Fail e -> Fail e - | Return (st0, hm) -> - begin match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail e -> Fail e - | Return hm0 -> - begin match hashmap_utils_serialize_fwd hm0 st0 with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end + let* (st0, hm) = hashmap_utils_deserialize_fwd st in + let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm key value in + let* (st1, _) = hashmap_utils_serialize_fwd hm0 st0 in + Return (st1, ()) (** [hashmap_main::main] *) let main_fwd : result unit = Return () diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index 9b90e9c7..1a2f4133 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -96,14 +96,7 @@ let q3_c : i32 = eval_global q3_body (** [constants::get_z2] *) let get_z2_fwd : result i32 = - begin match get_z1_fwd with - | Fail e -> Fail e - | Return i -> - begin match add_fwd i q3_c with - | Fail e -> Fail e - | Return i0 -> add_fwd q1_c i0 - end - end + let* i = get_z1_fwd in let* i0 = add_fwd i q3_c in add_fwd q1_c i0 (** [constants::S1] *) let s1_body : result u32 = Return 6 diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 2529ec33..f70a9fc6 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -9,53 +9,30 @@ include External.Opaque (** [external::swap] *) let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = - begin match core_mem_swap_fwd t x y st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match core_mem_swap_back0 t x y st st0 with - | Fail e -> Fail e - | Return (st1, _) -> - begin match core_mem_swap_back1 t x y st st1 with - | Fail e -> Fail e - | Return (st2, _) -> Return (st2, ()) - end - end - end + let* (st0, _) = core_mem_swap_fwd t x y st in + let* (st1, _) = core_mem_swap_back0 t x y st st0 in + let* (st2, _) = core_mem_swap_back1 t x y st st1 in + Return (st2, ()) (** [external::swap] *) let swap_back (t : Type0) (x : t) (y : t) (st : state) (st0 : state) : result (state & (t & t)) = - begin match core_mem_swap_fwd t x y st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match core_mem_swap_back0 t x y st st1 with - | Fail e -> Fail e - | Return (st2, x0) -> - begin match core_mem_swap_back1 t x y st st2 with - | Fail e -> Fail e - | Return (_, y0) -> Return (st0, (x0, y0)) - end - end - end + let* (st1, _) = core_mem_swap_fwd t x y st in + let* (st2, x0) = core_mem_swap_back0 t x y st st1 in + let* (_, y0) = core_mem_swap_back1 t x y st st2 in + Return (st0, (x0, y0)) (** [external::test_new_non_zero_u32] *) let test_new_non_zero_u32_fwd (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) = - begin match core_num_nonzero_non_zero_u32_new_fwd x st with - | Fail e -> Fail e - | Return (st0, opt) -> - core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 - end + let* (st0, opt) = core_num_nonzero_non_zero_u32_new_fwd x st in + core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 (** [external::test_vec] *) let test_vec_fwd : result unit = - let v = vec_new u32 in - begin match vec_push_back u32 v 0 with - | Fail e -> Fail e - | Return _ -> Return () - end + let v = vec_new u32 in let* _ = vec_push_back u32 v 0 in Return () (** Unit test for [external::test_vec] *) let _ = assert_norm (test_vec_fwd = Return ()) @@ -63,44 +40,25 @@ let _ = assert_norm (test_vec_fwd = Return ()) (** [external::custom_swap] *) let custom_swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & t) = - begin match core_mem_swap_fwd t x y st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match core_mem_swap_back0 t x y st st0 with - | Fail e -> Fail e - | Return (st1, x0) -> - begin match core_mem_swap_back1 t x y st st1 with - | Fail e -> Fail e - | Return (st2, _) -> Return (st2, x0) - end - end - end + let* (st0, _) = core_mem_swap_fwd t x y st in + let* (st1, x0) = core_mem_swap_back0 t x y st st0 in + let* (st2, _) = core_mem_swap_back1 t x y st st1 in + Return (st2, x0) (** [external::custom_swap] *) let custom_swap_back (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) : result (state & (t & t)) = - begin match core_mem_swap_fwd t x y st with - | Fail e -> Fail e - | Return (st1, _) -> - begin match core_mem_swap_back0 t x y st st1 with - | Fail e -> Fail e - | Return (st2, _) -> - begin match core_mem_swap_back1 t x y st st2 with - | Fail e -> Fail e - | Return (_, y0) -> Return (st0, (ret, y0)) - end - end - end + let* (st1, _) = core_mem_swap_fwd t x y st in + let* (st2, _) = core_mem_swap_back0 t x y st st1 in + let* (_, y0) = core_mem_swap_back1 t x y st st2 in + Return (st0, (ret, y0)) (** [external::test_custom_swap] *) let test_custom_swap_fwd (x : u32) (y : u32) (st : state) : result (state & unit) = - begin match custom_swap_fwd u32 x y st with - | Fail e -> Fail e - | Return (st0, _) -> Return (st0, ()) - end + let* (st0, _) = custom_swap_fwd u32 x y st in Return (st0, ()) (** [external::test_custom_swap] *) let test_custom_swap_back @@ -111,13 +69,7 @@ let test_custom_swap_back (** [external::test_swap_non_zero] *) let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = - begin match swap_fwd u32 x 0 st with - | Fail e -> Fail e - | Return (st0, _) -> - begin match swap_back u32 x 0 st st0 with - | Fail e -> Fail e - | Return (st1, (x0, _)) -> - if x0 = 0 then Fail Failure else Return (st1, x0) - end - end + let* (st0, _) = swap_fwd u32 x 0 st in + let* (st1, (x0, _)) = swap_back u32 x 0 st st0 in + if x0 = 0 then Fail Failure else Return (st1, x0) diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 3e8425dd..0d3c39f7 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -13,14 +13,8 @@ let rec sum_loop_fwd Tot (result u32) (decreases (sum_loop_decreases max i s)) = if i < max - then - begin match u32_add s i with - | Fail e -> Fail e - | Return s0 -> - begin match u32_add i 1 with - | Fail e -> Fail e - | Return i0 -> sum_loop_fwd max i0 s0 - end + then begin + let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0 end else u32_mul s 2 @@ -33,15 +27,10 @@ let rec sum_with_mut_borrows_loop_fwd Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) = if mi < max - then - begin match u32_add ms mi with - | Fail e -> Fail e - | Return ms0 -> - begin match u32_add mi 1 with - | Fail e -> Fail e - | Return mi0 -> sum_with_mut_borrows_loop_fwd max mi0 ms0 - end - end + then begin + let* ms0 = u32_add ms mi in + let* mi0 = u32_add mi 1 in + sum_with_mut_borrows_loop_fwd max mi0 ms0 end else u32_mul ms 2 (** [loops::sum_with_mut_borrows] *) @@ -54,15 +43,10 @@ let rec sum_with_shared_borrows_loop_fwd Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) = if i < max - then - begin match u32_add i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match u32_add s i0 with - | Fail e -> Fail e - | Return s0 -> sum_with_shared_borrows_loop_fwd max i0 s0 - end - end + then begin + let* i0 = u32_add i 1 in + let* s0 = u32_add s i0 in + sum_with_shared_borrows_loop_fwd max i0 s0 end else u32_mul s 2 (** [loops::sum_with_shared_borrows] *) @@ -76,15 +60,10 @@ let rec clear_loop_fwd_back = let i0 = vec_len u32 v in if i < i0 - then - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - begin match vec_index_mut_back u32 v i 0 with - | Fail e -> Fail e - | Return v0 -> clear_loop_fwd_back v0 i1 - end - end + then begin + let* i1 = usize_add i 1 in + let* v0 = vec_index_mut_back u32 v i 0 in + clear_loop_fwd_back v0 i1 end else Return v (** [loops::clear] *) @@ -113,11 +92,7 @@ let rec list_nth_mut_loop_loop_fwd | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_loop_loop_fwd t tl i0 - end + else begin let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 end | ListNil -> Fail Failure end @@ -134,15 +109,10 @@ let rec list_nth_mut_loop_loop_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_loop_back t tl i0 ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons x tl0) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in + Return (ListCons x tl0) end | ListNil -> Fail Failure end @@ -160,10 +130,7 @@ let rec list_nth_shared_loop_loop_fwd | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_loop_fwd t tl i0 + else begin let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0 end | ListNil -> Fail Failure end @@ -184,10 +151,8 @@ let rec get_elem_mut_loop_fwd (** [loops::get_elem_mut] *) let get_elem_mut_fwd (slots : vec (list_t usize)) (x : usize) : result usize = - begin match vec_index_mut_fwd (list_t usize) slots 0 with - | Fail e -> Fail e - | Return l -> get_elem_mut_loop_fwd x l - end + let* l = vec_index_mut_fwd (list_t usize) slots 0 in + get_elem_mut_loop_fwd x l (** [loops::get_elem_mut] *) let rec get_elem_mut_loop_back @@ -198,11 +163,8 @@ let rec get_elem_mut_loop_back | ListCons y tl -> if y = x then Return (ListCons ret tl) - else - begin match get_elem_mut_loop_back x tl ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons y tl0) - end + else begin + let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) end | ListNil -> Fail Failure end @@ -211,14 +173,9 @@ let get_elem_mut_back (slots : vec (list_t usize)) (x : usize) (ret : usize) : result (vec (list_t usize)) = - begin match vec_index_mut_fwd (list_t usize) slots 0 with - | Fail e -> Fail e - | Return l -> - begin match get_elem_mut_loop_back x l ret with - | Fail e -> Fail e - | Return l0 -> vec_index_mut_back (list_t usize) slots 0 l0 - end - end + let* l = vec_index_mut_fwd (list_t usize) slots 0 in + let* l0 = get_elem_mut_loop_back x l ret in + vec_index_mut_back (list_t usize) slots 0 l0 (** [loops::get_elem_shared] *) let rec get_elem_shared_loop_fwd @@ -233,10 +190,7 @@ let rec get_elem_shared_loop_fwd (** [loops::get_elem_shared] *) let get_elem_shared_fwd (slots : vec (list_t usize)) (x : usize) : result usize = - begin match vec_index_fwd (list_t usize) slots 0 with - | Fail e -> Fail e - | Return l -> get_elem_shared_loop_fwd x l - end + let* l = vec_index_fwd (list_t usize) slots 0 in get_elem_shared_loop_fwd x l (** [loops::id_mut] *) let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls @@ -258,21 +212,15 @@ let rec list_nth_mut_loop_with_id_loop_fwd | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_loop_with_id_loop_fwd t i0 tl - end + else begin + let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl end | ListNil -> Fail Failure end (** [loops::list_nth_mut_loop_with_id] *) let list_nth_mut_loop_with_id_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = - begin match id_mut_fwd t ls with - | Fail e -> Fail e - | Return ls0 -> list_nth_mut_loop_with_id_loop_fwd t i ls0 - end + let* ls0 = id_mut_fwd t ls in list_nth_mut_loop_with_id_loop_fwd t i ls0 (** [loops::list_nth_mut_loop_with_id] *) let rec list_nth_mut_loop_with_id_loop_back @@ -284,29 +232,19 @@ let rec list_nth_mut_loop_with_id_loop_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons x tl0) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in + Return (ListCons x tl0) end | ListNil -> Fail Failure end (** [loops::list_nth_mut_loop_with_id] *) let list_nth_mut_loop_with_id_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = - begin match id_mut_fwd t ls with - | Fail e -> Fail e - | Return ls0 -> - begin match list_nth_mut_loop_with_id_loop_back t i ls0 ret with - | Fail e -> Fail e - | Return l -> id_mut_back t ls l - end - end + let* ls0 = id_mut_fwd t ls in + let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in + id_mut_back t ls l (** [loops::list_nth_shared_loop_with_id] *) let rec list_nth_shared_loop_with_id_loop_fwd @@ -318,10 +256,8 @@ let rec list_nth_shared_loop_with_id_loop_fwd | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t i0 tl + else begin + let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl end | ListNil -> Fail Failure end @@ -329,10 +265,8 @@ let rec list_nth_shared_loop_with_id_loop_fwd (** [loops::list_nth_shared_loop_with_id] *) let list_nth_shared_loop_with_id_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = - begin match id_shared_fwd t ls with - | Fail e -> Fail e - | Return ls0 -> list_nth_shared_loop_with_id_loop_fwd t i ls0 - end + let* ls0 = id_shared_fwd t ls in + list_nth_shared_loop_with_id_loop_fwd t i ls0 (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_fwd @@ -346,10 +280,8 @@ let rec list_nth_mut_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0 + else begin + let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end @@ -373,15 +305,10 @@ let rec list_nth_mut_loop_pair_loop_back'a | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with - | Fail e -> Fail e - | Return tl00 -> Return (ListCons x0 tl00) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in + Return (ListCons x0 tl00) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -406,15 +333,10 @@ let rec list_nth_mut_loop_pair_loop_back'b | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with - | Fail e -> Fail e - | Return tl10 -> Return (ListCons x1 tl10) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in + Return (ListCons x1 tl10) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -439,11 +361,9 @@ let rec list_nth_shared_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -466,11 +386,9 @@ let rec list_nth_mut_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -493,16 +411,11 @@ let rec list_nth_mut_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret - with - | Fail e -> Fail e - | Return (tl00, tl10) -> Return (ListCons x0 tl00, ListCons x1 tl10) - end - end + else begin + let* i0 = u32_sub i 1 in + let* (tl00, tl10) = + list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (ListCons x0 tl00, ListCons x1 tl10) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -527,11 +440,9 @@ let rec list_nth_shared_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -554,11 +465,9 @@ let rec list_nth_mut_shared_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -581,16 +490,10 @@ let rec list_nth_mut_shared_loop_pair_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret - with - | Fail e -> Fail e - | Return tl00 -> Return (ListCons x0 tl00) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (ListCons x0 tl00) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -615,12 +518,9 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -643,16 +543,11 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match - list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with - | Fail e -> Fail e - | Return tl00 -> Return (ListCons x0 tl00) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl00 = + list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (ListCons x0 tl00) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -677,11 +572,9 @@ let rec list_nth_shared_mut_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -704,16 +597,10 @@ let rec list_nth_shared_mut_loop_pair_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret - with - | Fail e -> Fail e - | Return tl10 -> Return (ListCons x1 tl10) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (ListCons x1 tl10) end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -738,12 +625,9 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 - end + else begin + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -766,16 +650,11 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match - list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with - | Fail e -> Fail e - | Return tl10 -> Return (ListCons x1 tl10) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl10 = + list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (ListCons x1 tl10) end | ListNil -> Fail Failure end | ListNil -> Fail Failure diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index f8c63798..ce1f544c 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -52,8 +52,7 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x (** [no_nested_borrows::test2] *) -let test2_fwd : result unit = - begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end +let test2_fwd : result unit = let* _ = u32_add 23 44 in Return () (** Unit test for [no_nested_borrows::test2] *) let _ = assert_norm (test2_fwd = Return ()) @@ -64,28 +63,17 @@ let get_max_fwd (x : u32) (y : u32) : result u32 = (** [no_nested_borrows::test3] *) let test3_fwd : result unit = - begin match get_max_fwd 4 3 with - | Fail e -> Fail e - | Return x -> - begin match get_max_fwd 10 11 with - | Fail e -> Fail e - | Return y -> - begin match u32_add x y with - | Fail e -> Fail e - | Return z -> if not (z = 15) then Fail Failure else Return () - end - end - end + let* x = get_max_fwd 4 3 in + let* y = get_max_fwd 10 11 in + let* z = u32_add x y in + if not (z = 15) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test3] *) let _ = assert_norm (test3_fwd = Return ()) (** [no_nested_borrows::test_neg1] *) let test_neg1_fwd : result unit = - begin match i32_neg 3 with - | Fail e -> Fail e - | Return y -> if not (y = -3) then Fail Failure else Return () - end + let* y = i32_neg 3 in if not (y = -3) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_neg1] *) let _ = assert_norm (test_neg1_fwd = Return ()) @@ -138,10 +126,7 @@ let test_panic_fwd (b : bool) : result unit = (** [no_nested_borrows::test_copy_int] *) let test_copy_int_fwd : result unit = - begin match copy_int_fwd 0 with - | Fail e -> Fail e - | Return y -> if not (0 = y) then Fail Failure else Return () - end + let* y = copy_int_fwd 0 in if not (0 = y) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_copy_int] *) let _ = assert_norm (test_copy_int_fwd = Return ()) @@ -156,10 +141,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool = (** [no_nested_borrows::test_is_cons] *) let test_is_cons_fwd : result unit = let l = ListNil in - begin match is_cons_fwd i32 (ListCons 0 l) with - | Fail e -> Fail e - | Return b -> if not b then Fail Failure else Return () - end + let* b = is_cons_fwd i32 (ListCons 0 l) in + if not b then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_is_cons] *) let _ = assert_norm (test_is_cons_fwd = Return ()) @@ -174,11 +157,9 @@ let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) = (** [no_nested_borrows::test_split_list] *) let test_split_list_fwd : result unit = let l = ListNil in - begin match split_list_fwd i32 (ListCons 0 l) with - | Fail e -> Fail e - | Return p -> - let (hd, _) = p in if not (hd = 0) then Fail Failure else Return () - end + let* p = split_list_fwd i32 (ListCons 0 l) in + let (hd, _) = p in + if not (hd = 0) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_split_list] *) let _ = assert_norm (test_split_list_fwd = Return ()) @@ -194,24 +175,15 @@ let choose_back (** [no_nested_borrows::choose_test] *) let choose_test_fwd : result unit = - begin match choose_fwd i32 true 0 0 with - | Fail e -> Fail e - | Return z -> - begin match i32_add z 1 with - | Fail e -> Fail e - | Return z0 -> - if not (z0 = 1) - then Fail Failure - else - begin match choose_back i32 true 0 0 z0 with - | Fail e -> Fail e - | Return (x, y) -> - if not (x = 1) - then Fail Failure - else if not (y = 0) then Fail Failure else Return () - end - end - end + let* z = choose_fwd i32 true 0 0 in + let* z0 = i32_add z 1 in + if not (z0 = 1) + then Fail Failure + else begin + let* (x, y) = choose_back i32 true 0 0 z0 in + if not (x = 1) + then Fail Failure + else if not (y = 0) then Fail Failure else Return () end (** Unit test for [no_nested_borrows::choose_test] *) let _ = assert_norm (choose_test_fwd = Return ()) @@ -232,11 +204,7 @@ and tree_t (t : Type0) = (** [no_nested_borrows::list_length] *) let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = begin match l with - | ListCons x l1 -> - begin match list_length_fwd t l1 with - | Fail e -> Fail e - | Return i -> u32_add 1 i - end + | ListCons x l1 -> let* i = list_length_fwd t l1 in u32_add 1 i | ListNil -> Return 0 end @@ -246,11 +214,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_shared_fwd t tl i0 - end + else begin let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0 end | ListNil -> Fail Failure end @@ -260,11 +224,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_fwd t tl i0 - end + else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end | ListNil -> Fail Failure end @@ -275,15 +235,10 @@ let rec list_nth_mut_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_back t tl i0 ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons x tl0) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_back t tl i0 ret in + Return (ListCons x tl0) end | ListNil -> Fail Failure end @@ -305,57 +260,34 @@ let test_list_functions_fwd : result unit = let l = ListNil in let l0 = ListCons 2 l in let l1 = ListCons 1 l0 in - begin match list_length_fwd i32 (ListCons 0 l1) with - | Fail e -> Fail e - | Return i -> - if not (i = 3) + let* i = list_length_fwd i32 (ListCons 0 l1) in + if not (i = 3) + then Fail Failure + else begin + let* i0 = list_nth_shared_fwd i32 (ListCons 0 l1) 0 in + if not (i0 = 0) then Fail Failure - else - begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with - | Fail e -> Fail e - | Return i0 -> - if not (i0 = 0) + else begin + let* i1 = list_nth_shared_fwd i32 (ListCons 0 l1) 1 in + if not (i1 = 1) + then Fail Failure + else begin + let* i2 = list_nth_shared_fwd i32 (ListCons 0 l1) 2 in + if not (i2 = 2) then Fail Failure - else - begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with - | Fail e -> Fail e - | Return i1 -> - if not (i1 = 1) + else begin + let* ls = list_nth_mut_back i32 (ListCons 0 l1) 1 3 in + let* i3 = list_nth_shared_fwd i32 ls 0 in + if not (i3 = 0) + then Fail Failure + else begin + let* i4 = list_nth_shared_fwd i32 ls 1 in + if not (i4 = 3) then Fail Failure - else - begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with - | Fail e -> Fail e - | Return i2 -> - if not (i2 = 2) - then Fail Failure - else - begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with - | Fail e -> Fail e - | Return ls -> - begin match list_nth_shared_fwd i32 ls 0 with - | Fail e -> Fail e - | Return i3 -> - if not (i3 = 0) - then Fail Failure - else - begin match list_nth_shared_fwd i32 ls 1 with - | Fail e -> Fail e - | Return i4 -> - if not (i4 = 3) - then Fail Failure - else - begin match list_nth_shared_fwd i32 ls 2 with - | Fail e -> Fail e - | Return i5 -> - if not (i5 = 2) then Fail Failure else Return () - end - end - end - end - end - end - end - end + else begin + let* i5 = list_nth_shared_fwd i32 ls 2 in + if not (i5 = 2) then Fail Failure else Return () end end end end + end end (** Unit test for [no_nested_borrows::test_list_functions] *) let _ = assert_norm (test_list_functions_fwd = Return ()) @@ -433,37 +365,25 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) = (** [no_nested_borrows::test_constants] *) let test_constants_fwd : result unit = - begin match new_tuple1_fwd with - | Fail e -> Fail e - | Return swt -> - let (i, _) = swt.struct_with_tuple_p in - if not (i = 1) + let* swt = new_tuple1_fwd in + let (i, _) = swt.struct_with_tuple_p in + if not (i = 1) + then Fail Failure + else begin + let* swt0 = new_tuple2_fwd in + let (i0, _) = swt0.struct_with_tuple_p in + if not (i0 = 1) then Fail Failure - else - begin match new_tuple2_fwd with - | Fail e -> Fail e - | Return swt0 -> - let (i0, _) = swt0.struct_with_tuple_p in - if not (i0 = 1) + else begin + let* swt1 = new_tuple3_fwd in + let (i1, _) = swt1.struct_with_tuple_p in + if not (i1 = 1) + then Fail Failure + else begin + let* swp = new_pair1_fwd in + if not (swp.struct_with_pair_p.pair_x = 1) then Fail Failure - else - begin match new_tuple3_fwd with - | Fail e -> Fail e - | Return swt1 -> - let (i1, _) = swt1.struct_with_tuple_p in - if not (i1 = 1) - then Fail Failure - else - begin match new_pair1_fwd with - | Fail e -> Fail e - | Return swp -> - if not (swp.struct_with_pair_p.pair_x = 1) - then Fail Failure - else Return () - end - end - end - end + else Return () end end end (** Unit test for [no_nested_borrows::test_constants] *) let _ = assert_norm (test_constants_fwd = Return ()) diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index 199ceb63..95f13f62 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -10,10 +10,8 @@ let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1 (** [paper::test_incr] *) let test_incr_fwd : result unit = - begin match ref_incr_fwd_back 0 with - | Fail e -> Fail e - | Return x -> if not (x = 1) then Fail Failure else Return () - end + let* x = ref_incr_fwd_back 0 in + if not (x = 1) then Fail Failure else Return () (** Unit test for [paper::test_incr] *) let _ = assert_norm (test_incr_fwd = Return ()) @@ -29,24 +27,15 @@ let choose_back (** [paper::test_choose] *) let test_choose_fwd : result unit = - begin match choose_fwd i32 true 0 0 with - | Fail e -> Fail e - | Return z -> - begin match i32_add z 1 with - | Fail e -> Fail e - | Return z0 -> - if not (z0 = 1) - then Fail Failure - else - begin match choose_back i32 true 0 0 z0 with - | Fail e -> Fail e - | Return (x, y) -> - if not (x = 1) - then Fail Failure - else if not (y = 0) then Fail Failure else Return () - end - end - end + let* z = choose_fwd i32 true 0 0 in + let* z0 = i32_add z 1 in + if not (z0 = 1) + then Fail Failure + else begin + let* (x, y) = choose_back i32 true 0 0 z0 in + if not (x = 1) + then Fail Failure + else if not (y = 0) then Fail Failure else Return () end (** Unit test for [paper::test_choose] *) let _ = assert_norm (test_choose_fwd = Return ()) @@ -62,11 +51,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_fwd t tl i0 - end + else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end | ListNil -> Fail Failure end @@ -77,26 +62,17 @@ let rec list_nth_mut_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_back t tl i0 ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons x tl0) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_back t tl i0 ret in + Return (ListCons x tl0) end | ListNil -> Fail Failure end (** [paper::sum] *) let rec sum_fwd (l : list_t i32) : result i32 = begin match l with - | ListCons x tl -> - begin match sum_fwd tl with - | Fail e -> Fail e - | Return i -> i32_add x i - end + | ListCons x tl -> let* i = sum_fwd tl in i32_add x i | ListNil -> Return 0 end @@ -105,22 +81,11 @@ let test_nth_fwd : result unit = let l = ListNil in let l0 = ListCons 3 l in let l1 = ListCons 2 l0 in - begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with - | Fail e -> Fail e - | Return x -> - begin match i32_add x 1 with - | Fail e -> Fail e - | Return x0 -> - begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with - | Fail e -> Fail e - | Return l2 -> - begin match sum_fwd l2 with - | Fail e -> Fail e - | Return i -> if not (i = 7) then Fail Failure else Return () - end - end - end - end + let* x = list_nth_mut_fwd i32 (ListCons 1 l1) 2 in + let* x0 = i32_add x 1 in + let* l2 = list_nth_mut_back i32 (ListCons 1 l1) 2 x0 in + let* i = sum_fwd l2 in + if not (i = 7) then Fail Failure else Return () (** Unit test for [paper::test_nth] *) let _ = assert_norm (test_nth_fwd = Return ()) @@ -128,16 +93,8 @@ let _ = assert_norm (test_nth_fwd = Return ()) (** [paper::call_choose] *) let call_choose_fwd (p : (u32 & u32)) : result u32 = let (px, py) = p in - begin match choose_fwd u32 true px py with - | Fail e -> Fail e - | Return pz -> - begin match u32_add pz 1 with - | Fail e -> Fail e - | Return pz0 -> - begin match choose_back u32 true px py pz0 with - | Fail e -> Fail e - | Return (px0, _) -> Return px0 - end - end - end + let* pz = choose_fwd u32 true px py in + let* pz0 = u32_add pz 1 in + let* (px0, _) = choose_back u32 true px py pz0 in + Return px0 diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index 12618dbb..db0dc0d5 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -25,11 +25,8 @@ let rec get_list_at_x_back | ListCons hd tl -> if hd = x then Return ret - else - begin match get_list_at_x_back tl x ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons hd tl0) - end + else begin + let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) end | ListNil -> Return ret end diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e |