diff options
author | Son Ho | 2023-03-08 00:09:25 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | c00d77052e8cb778e5311a4344cf8449dd3726b6 (patch) | |
tree | 2bdf05a740e5607b0996ec6bbeef62a513bc4494 /tests/fstar/betree/BetreeMain.Funs.fst | |
parent | ca77353c20e425c687ba207023d56828de6495b6 (diff) |
Improve simplify_aggregates to introduce structure updates
Diffstat (limited to 'tests/fstar/betree/BetreeMain.Funs.fst')
-rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 57 |
1 files changed, 9 insertions, 48 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 4c541aaf..b098d8ca 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -469,22 +469,10 @@ and betree_internal_lookup_in_children_back if key < self.betree_internal_pivot then let* n = betree_node_lookup_back self.betree_internal_left key st in - Return - { - betree_internal_id = self.betree_internal_id; - betree_internal_pivot = self.betree_internal_pivot; - betree_internal_left = n; - betree_internal_right = self.betree_internal_right - } + Return { self where betree_internal_left = n } else let* n = betree_node_lookup_back self.betree_internal_right key st in - Return - { - betree_internal_id = self.betree_internal_id; - betree_internal_pivot = self.betree_internal_pivot; - betree_internal_left = self.betree_internal_left; - betree_internal_right = n - } + Return { self where betree_internal_right = n } (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -797,8 +785,7 @@ and betree_node_apply_messages_back Return (BetreeNodeInternal new_node, node_id_cnt0) else let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in - Return (BetreeNodeLeaf - { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len }, + Return (BetreeNodeLeaf { node where betree_leaf_size = len }, node_id_cnt) end @@ -873,31 +860,14 @@ and betree_internal_flush_back betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 in Return - ({ - betree_internal_id = self.betree_internal_id; - betree_internal_pivot = self.betree_internal_pivot; - betree_internal_left = n; - betree_internal_right = n0 - }, node_id_cnt1) - else - Return - ({ - betree_internal_id = self.betree_internal_id; - betree_internal_pivot = self.betree_internal_pivot; - betree_internal_left = n; - betree_internal_right = self.betree_internal_right - }, node_id_cnt0) + ({ self where betree_internal_left = n; betree_internal_right = n0 }, + node_id_cnt1) + else Return ({ self where betree_internal_left = n }, node_id_cnt0) else let* (n, node_id_cnt0) = betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st in - Return - ({ - betree_internal_id = self.betree_internal_id; - betree_internal_pivot = self.betree_internal_pivot; - betree_internal_left = self.betree_internal_left; - betree_internal_right = n - }, node_id_cnt0) + Return ({ self where betree_internal_right = n }, node_id_cnt0) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -969,11 +939,7 @@ let betree_be_tree_apply_back 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 - { - betree_be_tree_params = self.betree_be_tree_params; - betree_be_tree_node_id_cnt = nic; - betree_be_tree_root = n - } + { self where betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n } (** [betree_main::betree::BeTree::{6}::insert] *) let betree_be_tree_insert_fwd @@ -1038,12 +1004,7 @@ let betree_be_tree_lookup_back result betree_be_tree_t = let* n = betree_node_lookup_back self.betree_be_tree_root key st in - Return - { - betree_be_tree_params = self.betree_be_tree_params; - betree_be_tree_node_id_cnt = self.betree_be_tree_node_id_cnt; - betree_be_tree_root = n - } + Return { self where betree_be_tree_root = n } (** [betree_main::main] *) let main_fwd : result unit = |