diff options
Diffstat (limited to 'tests/fstar/betree_back_stateful/BetreeMain.Funs.fst')
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 676 |
1 files changed, 0 insertions, 676 deletions
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst deleted file mode 100644 index 9942ef68..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ /dev/null @@ -1,676 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -module BetreeMain.Funs -open Primitives -include BetreeMain.Types -include BetreeMain.FunsExternal -include BetreeMain.Clauses - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree::load_internal_node]: - Source: 'src/betree.rs', lines 36:0-36:52 *) -let betree_load_internal_node - (id : u64) (st : state) : - result (state & (betree_List_t (u64 & betree_Message_t))) - = - betree_utils_load_internal_node id st - -(** [betree_main::betree::store_internal_node]: - Source: 'src/betree.rs', lines 41:0-41:60 *) -let betree_store_internal_node - (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - result (state & unit) - = - betree_utils_store_internal_node id content st - -(** [betree_main::betree::load_leaf_node]: - Source: 'src/betree.rs', lines 46:0-46:44 *) -let betree_load_leaf_node - (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) = - betree_utils_load_leaf_node id st - -(** [betree_main::betree::store_leaf_node]: - Source: 'src/betree.rs', lines 51:0-51:52 *) -let betree_store_leaf_node - (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : - result (state & unit) - = - betree_utils_store_leaf_node id content st - -(** [betree_main::betree::fresh_node_id]: - Source: 'src/betree.rs', lines 55:0-55:48 *) -let betree_fresh_node_id (counter : u64) : result (u64 & u64) = - let* counter1 = u64_add counter 1 in Ok (counter, counter1) - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: - Source: 'src/betree.rs', lines 206:4-206:20 *) -let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = - Ok { next_node_id = 0 } - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: - Source: 'src/betree.rs', lines 210:4-210:36 *) -let betree_NodeIdCounter_fresh_id - (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) = - let* i = u64_add self.next_node_id 1 in - Ok (self.next_node_id, { next_node_id = i }) - -(** [betree_main::betree::upsert_update]: - Source: 'src/betree.rs', lines 234:0-234:70 *) -let betree_upsert_update - (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = - begin match prev with - | None -> - begin match st with - | Betree_UpsertFunState_Add v -> Ok v - | Betree_UpsertFunState_Sub _ -> Ok 0 - end - | Some prev1 -> - begin match st with - | Betree_UpsertFunState_Add v -> - let* margin = u64_sub core_u64_max prev1 in - if margin >= v then u64_add prev1 v else Ok core_u64_max - | Betree_UpsertFunState_Sub v -> - if prev1 >= v then u64_sub prev1 v else Ok 0 - end - end - -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: - Source: 'src/betree.rs', lines 276:4-276:24 *) -let rec betree_List_len - (t : Type0) (self : betree_List_t t) : - Tot (result u64) (decreases (betree_List_len_decreases t self)) - = - begin match self with - | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i - | Betree_List_Nil -> Ok 0 - end - -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -let rec betree_List_split_at - (t : Type0) (self : betree_List_t t) (n : u64) : - Tot (result ((betree_List_t t) & (betree_List_t t))) - (decreases (betree_List_split_at_decreases t self n)) - = - if n = 0 - then Ok (Betree_List_Nil, self) - else - begin match self with - | Betree_List_Cons hd tl -> - let* i = u64_sub n 1 in - let* p = betree_List_split_at t tl i in - let (ls0, ls1) = p in - Ok (Betree_List_Cons hd ls0, ls1) - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 *) -let betree_List_push_front - (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = - let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in - Ok (Betree_List_Cons x tl) - -(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 *) -let betree_List_pop_front - (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) = - let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in - begin match ls with - | Betree_List_Cons x tl -> Ok (x, tl) - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 *) -let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = - begin match self with - | Betree_List_Cons hd _ -> Ok hd - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 *) -let betree_ListPairU64T_head_has_key - (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = - begin match self with - | Betree_List_Cons hd _ -> let (i, _) = hd in Ok (i = key) - | Betree_List_Nil -> Ok false - end - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -let rec betree_ListPairU64T_partition_at_pivot - (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : - Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot)) - = - begin match self with - | Betree_List_Cons hd tl -> - let (i, x) = hd in - if i >= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl) - else - let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in - let (ls0, ls1) = p in - Ok (Betree_List_Cons (i, x) ls0, ls1) - | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) - end - -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 *) -let betree_Leaf_split - (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (st : state) : - result (state & (betree_Internal_t & betree_NodeIdCounter_t)) - = - let* p = betree_List_split_at (u64 & u64) content params.split_size in - let (content0, content1) = p in - let* p1 = betree_List_hd (u64 & u64) content1 in - let (pivot, _) = p1 in - let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in - let* (st1, _) = betree_store_leaf_node id0 content0 st in - let* (st2, _) = betree_store_leaf_node id1 content1 st1 in - let n = Betree_Node_Leaf { id = id0; size = params.split_size } in - let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, - node_id_cnt2)) - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -let rec betree_Node_lookup_first_message_for_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & - betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons x next_msgs -> - let (i, m) = x in - if i >= key - then Ok (Betree_List_Cons (i, m) next_msgs, Ok) - else - let* (l, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key next_msgs in - let back = - fun ret -> - let* next_msgs1 = lookup_first_message_for_key_back ret in - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -let rec betree_Node_lookup_in_bindings - (key : u64) (bindings : betree_List_t (u64 & u64)) : - Tot (result (option u64)) - (decreases (betree_Node_lookup_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i = key - then Ok (Some i1) - else if i > key then Ok None else betree_Node_lookup_in_bindings key tl - | Betree_List_Nil -> Ok None - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -let rec betree_Node_apply_upserts - (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) : - Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key)) - = - let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in - if b - then - let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in - let (_, m) = msg in - begin match m with - | Betree_Message_Insert _ -> Fail Failure - | Betree_Message_Delete -> Fail Failure - | Betree_Message_Upsert s -> - let* v = betree_upsert_update prev s in - betree_Node_apply_upserts msgs1 (Some v) key - end - else - let* v = core_option_Option_unwrap u64 prev in - let* msgs1 = - betree_List_push_front (u64 & betree_Message_t) msgs (key, - Betree_Message_Insert v) in - Ok (v, msgs1) - -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 *) -let rec betree_Internal_lookup_in_children - (self : betree_Internal_t) (key : u64) (st : state) : - Tot (result (state & ((option u64) & betree_Internal_t))) - (decreases (betree_Internal_lookup_in_children_decreases self key st)) - = - if key < self.pivot - then - let* (st1, (o, n)) = betree_Node_lookup self.left key st in - Ok (st1, (o, { self with left = n })) - else - let* (st1, (o, n)) = betree_Node_lookup self.right key st in - Ok (st1, (o, { self with right = n })) - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 *) -and betree_Node_lookup - (self : betree_Node_t) (key : u64) (st : state) : - Tot (result (state & ((option u64) & betree_Node_t))) - (decreases (betree_Node_lookup_decreases self key st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, msgs) = betree_load_internal_node node.id st in - let* (pending, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key msgs in - begin match pending with - | Betree_List_Cons p l -> - let (k, msg) = p in - if k <> key - then - let* (st2, (o, node1)) = - betree_Internal_lookup_in_children node key st1 in - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Ok (st2, (o, Betree_Node_Internal node1)) - else - begin match msg with - | Betree_Message_Insert v -> - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Insert v) l) in - Ok (st1, (Some v, Betree_Node_Internal node)) - | Betree_Message_Delete -> - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Delete) l) in - Ok (st1, (None, Betree_Node_Internal node)) - | Betree_Message_Upsert ufs -> - let* (st2, (v, node1)) = - betree_Internal_lookup_in_children node key st1 in - let* (v1, pending1) = - betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key in - let* msgs1 = lookup_first_message_for_key_back pending1 in - let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in - Ok (st3, (Some v1, Betree_Node_Internal node1)) - end - | Betree_List_Nil -> - let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 - in - let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Ok (st2, (o, Betree_Node_Internal node1)) - end - | Betree_Node_Leaf node -> - let* (st1, bindings) = betree_load_leaf_node node.id st in - let* o = betree_Node_lookup_in_bindings key bindings in - Ok (st1, (o, Betree_Node_Leaf node)) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -let rec betree_Node_filter_messages_for_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_filter_messages_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p l -> - let (k, m) = p in - if k = key - then - let* (_, msgs1) = - betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) - l) in - betree_Node_filter_messages_for_key key msgs1 - else Ok (Betree_List_Cons (k, m) l) - | Betree_List_Nil -> Ok Betree_List_Nil - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -let rec betree_Node_lookup_first_message_after_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & - betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p next_msgs -> - let (k, m) = p in - if k = key - then - let* (l, lookup_first_message_after_key_back) = - betree_Node_lookup_first_message_after_key key next_msgs in - let back = - fun ret -> - let* next_msgs1 = lookup_first_message_after_key_back ret in - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back) - else Ok (Betree_List_Cons (k, m) next_msgs, Ok) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 *) -let betree_Node_apply_to_internal - (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 & betree_Message_t)) - = - let* (msgs1, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs1 key in - if b - then - begin match new_msg with - | Betree_Message_Insert i -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert i) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Delete) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert s -> - let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in - let (_, m) = p in - begin match m with - | Betree_Message_Insert prev -> - let* v = betree_upsert_update (Some prev) s in - let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 - in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete -> - let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 - in - let* v = betree_upsert_update None s in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert _ -> - let* (msgs2, lookup_first_message_after_key_back) = - betree_Node_lookup_first_message_after_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Upsert s) in - let* msgs4 = lookup_first_message_after_key_back msgs3 in - lookup_first_message_for_key_back msgs4 - end - end - else - let* msgs2 = - betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back msgs2 - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 *) -let rec betree_Node_apply_messages_to_internal - (msgs : betree_List_t (u64 & betree_Message_t)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* msgs1 = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal msgs1 new_msgs_tl - | Betree_List_Nil -> Ok msgs - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -let rec betree_Node_lookup_mut_in_bindings - (key : u64) (bindings : betree_List_t (u64 & u64)) : - Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> - result (betree_List_t (u64 & u64))))) - (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i >= key - then Ok (Betree_List_Cons (i, i1) tl, Ok) - else - let* (l, lookup_mut_in_bindings_back) = - betree_Node_lookup_mut_in_bindings key tl in - let back = - fun ret -> - let* tl1 = lookup_mut_in_bindings_back ret in - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 *) -let betree_Node_apply_to_leaf - (bindings : betree_List_t (u64 & u64)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 & u64)) - = - let* (bindings1, lookup_mut_in_bindings_back) = - betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in - if b - then - let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - lookup_mut_in_bindings_back bindings3 - | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 - | Betree_Message_Upsert s -> - let (_, i) = hd in - let* v = betree_upsert_update (Some i) s in - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - lookup_mut_in_bindings_back bindings3 - end - else - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back bindings2 - | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 - | Betree_Message_Upsert s -> - let* v = betree_upsert_update None s in - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back bindings2 - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -let rec betree_Node_apply_messages_to_leaf - (bindings : betree_List_t (u64 & u64)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & u64))) - (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* bindings1 = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl - | Betree_List_Nil -> Ok bindings - end - -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 *) -let rec betree_Internal_flush - (self : betree_Internal_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & ((betree_List_t (u64 & betree_Message_t)) & - (betree_Internal_t & betree_NodeIdCounter_t)))) - (decreases ( - betree_Internal_flush_decreases self params node_id_cnt content st)) - = - let* p = - betree_ListPairU64T_partition_at_pivot betree_Message_t content self.pivot - in - let (msgs_left, msgs_right) = p in - let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in - if len_left >= params.min_flush_size - then - let* (st1, p1) = - betree_Node_apply_messages self.left params node_id_cnt msgs_left st in - let (n, node_id_cnt1) = p1 in - let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in - if len_right >= params.min_flush_size - then - let* (st2, p2) = - betree_Node_apply_messages self.right params node_id_cnt1 msgs_right - st1 in - let (n1, node_id_cnt2) = p2 in - Ok (st2, (Betree_List_Nil, ({ self with left = n; right = n1 }, - node_id_cnt2))) - else Ok (st1, (msgs_right, ({ self with left = n }, node_id_cnt1))) - else - let* (st1, p1) = - betree_Node_apply_messages self.right params node_id_cnt msgs_right st in - let (n, node_id_cnt1) = p1 in - Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 *) -and betree_Node_apply_messages - (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & (betree_Node_t & betree_NodeIdCounter_t))) - (decreases ( - betree_Node_apply_messages_decreases self params node_id_cnt msgs st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, content) = betree_load_internal_node node.id st in - let* content1 = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in - if num_msgs >= params.min_flush_size - then - let* (st2, (content2, p)) = - betree_Internal_flush node params node_id_cnt content1 st1 in - let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content2 st2 in - Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)) - else - let* (st2, _) = betree_store_internal_node node.id content1 st1 in - Ok (st2, (Betree_Node_Internal node, node_id_cnt)) - | Betree_Node_Leaf node -> - let* (st1, content) = betree_load_leaf_node node.id st in - let* content1 = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) content1 in - let* i = u64_mul 2 params.split_size in - if len >= i - then - let* (st2, (new_node, node_id_cnt1)) = - betree_Leaf_split node content1 params node_id_cnt st1 in - let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)) - else - let* (st2, _) = betree_store_leaf_node node.id content1 st1 in - Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 *) -let betree_Node_apply - (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) (key : u64) - (new_msg : betree_Message_t) (st : state) : - result (state & (betree_Node_t & betree_NodeIdCounter_t)) - = - let* (st1, p) = - betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key, - new_msg) Betree_List_Nil) st in - let (self1, node_id_cnt1) = p in - Ok (st1, (self1, node_id_cnt1)) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 *) -let betree_BeTree_new - (min_flush_size : u64) (split_size : u64) (st : state) : - result (state & betree_BeTree_t) - = - let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in - Ok (st1, - { - params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = node_id_cnt1; - root = (Betree_Node_Leaf { id = id; size = 0 }) - }) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 *) -let betree_BeTree_apply - (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : - result (state & betree_BeTree_t) - = - let* (st1, p) = - betree_Node_apply self.root self.params self.node_id_cnt key msg st in - let (n, nic) = p in - Ok (st1, { self with node_id_cnt = nic; root = n }) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 *) -let betree_BeTree_insert - (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key (Betree_Message_Insert value) st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 *) -let betree_BeTree_delete - (self : betree_BeTree_t) (key : u64) (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key Betree_Message_Delete st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 *) -let betree_BeTree_upsert - (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) - (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key (Betree_Message_Upsert upd) st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 *) -let betree_BeTree_lookup - (self : betree_BeTree_t) (key : u64) (st : state) : - result (state & ((option u64) & betree_BeTree_t)) - = - let* (st1, (o, n)) = betree_Node_lookup self.root key st in - Ok (st1, (o, { self with root = n })) - -(** [betree_main::main]: - Source: 'src/main.rs', lines 4:0-4:9 *) -let main : result unit = - Ok () - -(** Unit test for [betree_main::main] *) -let _ = assert_norm (main = Ok ()) - |