diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 17 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 16 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 16 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 22 |
4 files changed, 32 insertions, 39 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index b098d8ca..0c868f47 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -469,10 +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 { self where betree_internal_left = n } + Return { self with betree_internal_left = n } else let* n = betree_node_lookup_back self.betree_internal_right key st in - Return { self where betree_internal_right = n } + Return { self with betree_internal_right = n } (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -785,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 { node where betree_leaf_size = len }, - node_id_cnt) + Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt) end (** [betree_main::betree::Internal::{4}::flush] *) @@ -860,14 +859,14 @@ and betree_internal_flush_back betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 in Return - ({ self where betree_internal_left = n; betree_internal_right = n0 }, + ({ self with betree_internal_left = n; betree_internal_right = n0 }, node_id_cnt1) - else Return ({ self where betree_internal_left = n }, node_id_cnt0) + else Return ({ self with 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 ({ self where betree_internal_right = n }, node_id_cnt0) + Return ({ self with betree_internal_right = n }, node_id_cnt0) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -939,7 +938,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 - { self where betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n } + { self with betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n } (** [betree_main::betree::BeTree::{6}::insert] *) let betree_be_tree_insert_fwd @@ -1004,7 +1003,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 { self where betree_be_tree_root = n } + Return { self with betree_be_tree_root = n } (** [betree_main::main] *) let main_fwd : result unit = diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index eb1802fd..c70bef08 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -515,11 +515,11 @@ and betree_internal_lookup_in_children_back then let* (st1, n) = betree_node_lookup_back self.betree_internal_left key st st0 in - Return (st1, { self where betree_internal_left = n }) + Return (st1, { self with betree_internal_left = n }) else let* (st1, n) = betree_node_lookup_back self.betree_internal_right key st st0 in - Return (st1, { self where betree_internal_right = n }) + Return (st1, { self with betree_internal_right = n }) (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -836,7 +836,7 @@ and betree_node_apply_messages_back'a Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) else let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in - Return (st0, (BetreeNodeLeaf { node where betree_leaf_size = len }, + Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt)) end @@ -979,9 +979,9 @@ and betree_internal_flush_back'a betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 in Return (st0, - ({ self where betree_internal_left = n; betree_internal_right = n0 }, + ({ self with betree_internal_left = n; betree_internal_right = n0 }, node_id_cnt1)) - else Return (st0, ({ self where betree_internal_left = n }, node_id_cnt0)) + else Return (st0, ({ self with betree_internal_left = n }, node_id_cnt0)) else let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_right params @@ -992,7 +992,7 @@ and betree_internal_flush_back'a let* _ = betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 in - Return (st0, ({ self where betree_internal_right = n }, node_id_cnt0)) + Return (st0, ({ self with betree_internal_right = n }, node_id_cnt0)) (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back1 @@ -1154,7 +1154,7 @@ let betree_be_tree_apply_back 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, - { self where betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n }) + { self with betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n }) (** [betree_main::betree::BeTree::{6}::insert] *) let betree_be_tree_insert_fwd @@ -1235,7 +1235,7 @@ let betree_be_tree_lookup_back = let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0 in - Return (st1, { self where betree_be_tree_root = n }) + Return (st1, { self with betree_be_tree_root = n }) (** [betree_main::main] *) let main_fwd : result unit = diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 42ec35ee..44ad7463 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -69,7 +69,7 @@ let rec hash_map_clear_loop_fwd_back let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = let* v = hash_map_clear_loop_fwd_back t self.hash_map_slots 0 in - Return { self where hash_map_num_entries = 0; hash_map_slots = v } + Return { self with hash_map_num_entries = 0; hash_map_slots = v } (** [hashmap::HashMap::{0}::len] *) let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize = @@ -130,11 +130,11 @@ let hash_map_insert_no_resize_fwd_back 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 { self where hash_map_num_entries = i0; hash_map_slots = v } + Return { self with hash_map_num_entries = i0; hash_map_slots = v } else 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 { self where hash_map_slots = v } + Return { self with hash_map_slots = v } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -200,11 +200,11 @@ let hash_map_try_resize_fwd_back Return { ntable0 - where + with hash_map_num_entries = self.hash_map_num_entries; hash_map_max_load_factor = (i, i0) } - else Return { self where hash_map_max_load_factor = (i, i0) } + else Return { self with hash_map_max_load_factor = (i, i0) } (** [hashmap::HashMap::{0}::insert] *) let hash_map_insert_fwd_back @@ -331,7 +331,7 @@ let hash_map_get_mut_back 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 { self where hash_map_slots = v } + Return { self with hash_map_slots = v } (** [hashmap::HashMap::{0}::remove_from_list] *) let rec hash_map_remove_from_list_loop_fwd @@ -409,12 +409,12 @@ let hash_map_remove_back | 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 { self where hash_map_slots = v } + Return { self with hash_map_slots = 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 { self where hash_map_num_entries = i0; hash_map_slots = v } + Return { self with hash_map_num_entries = i0; hash_map_slots = v } end (** [hashmap::test1] *) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index cb8460c7..e8cd54c1 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -75,7 +75,7 @@ let hashmap_hash_map_clear_fwd_back let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 in Return - { self where hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v } + { self with hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -145,17 +145,14 @@ let hashmap_hash_map_insert_no_resize_fwd_back vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return - { - self - where - hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v + { self with hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v } else 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 { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = v } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -228,11 +225,11 @@ let hashmap_hash_map_try_resize_fwd_back Return { ntable0 - where + with hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; hashmap_hash_map_max_load_factor = (i, i0) } - else Return { self where hashmap_hash_map_max_load_factor = (i, i0) } + else Return { self with hashmap_hash_map_max_load_factor = (i, i0) } (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back @@ -371,7 +368,7 @@ let hashmap_hash_map_get_mut_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -463,7 +460,7 @@ let hashmap_hash_map_remove_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = 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 @@ -471,10 +468,7 @@ let hashmap_hash_map_remove_back vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return - { - self - where - hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v + { self with hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v } end |