diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 57 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 57 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 65 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 66 | ||||
| -rw-r--r-- | tests/lean/betree/BetreeMain/Funs.lean | 16 | ||||
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 63 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 69 |
7 files changed, 79 insertions, 314 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 = diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 1ca469ea..eb1802fd 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -515,23 +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, - { - 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 (st1, { self where betree_internal_left = n }) else let* (st1, n) = betree_node_lookup_back self.betree_internal_right key st st0 in - Return (st1, - { - 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 (st1, { self where betree_internal_right = n }) (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -848,8 +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 - { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len }, + Return (st0, (BetreeNodeLeaf { node where betree_leaf_size = len }, node_id_cnt)) end @@ -992,20 +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, - ({ - 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 (st0, - ({ - 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 (st0, ({ self where betree_internal_left = n }, node_id_cnt0)) else let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_right params @@ -1016,13 +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, - ({ - 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 (st0, ({ self where betree_internal_right = n }, node_id_cnt0)) (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back1 @@ -1184,11 +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, - { - 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 @@ -1269,12 +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, - { - 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 (st1, { self where 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 120f8323..42ec35ee 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -69,13 +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 - { - hash_map_num_entries = 0; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where 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 = @@ -136,23 +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 - { - hash_map_num_entries = i0; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where 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 - { - hash_map_num_entries = self.hash_map_num_entries; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where hash_map_slots = v } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -217,19 +199,12 @@ let hash_map_try_resize_fwd_back hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in Return { - hash_map_num_entries = self.hash_map_num_entries; - hash_map_max_load_factor = (i, i0); - hash_map_max_load = ntable0.hash_map_max_load; - hash_map_slots = ntable0.hash_map_slots - } - else - Return - { - hash_map_num_entries = self.hash_map_num_entries; - hash_map_max_load_factor = (i, i0); - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = self.hash_map_slots + ntable0 + where + 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) } (** [hashmap::HashMap::{0}::insert] *) let hash_map_insert_fwd_back @@ -356,13 +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 - { - hash_map_num_entries = self.hash_map_num_entries; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where hash_map_slots = v } (** [hashmap::HashMap::{0}::remove_from_list] *) let rec hash_map_remove_from_list_loop_fwd @@ -440,24 +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 - { - hash_map_num_entries = self.hash_map_num_entries; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where 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 - { - hash_map_num_entries = i0; - hash_map_max_load_factor = self.hash_map_max_load_factor; - hash_map_max_load = self.hash_map_max_load; - hash_map_slots = v - } + Return { self where 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 ae98386a..cb8460c7 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -75,12 +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 - { - hashmap_hash_map_num_entries = 0; - hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v - } + { self where hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -151,25 +146,16 @@ let hashmap_hash_map_insert_no_resize_fwd_back hash_mod l0 in Return { - hashmap_hash_map_num_entries = i0; - hashmap_hash_map_max_load_factor = - self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v + self + where + 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 - { - hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; - hashmap_hash_map_max_load_factor = - self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v - } + Return { self where hashmap_hash_map_slots = v } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -241,19 +227,12 @@ let hashmap_hash_map_try_resize_fwd_back self.hashmap_hash_map_slots 0 in Return { - hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; - hashmap_hash_map_max_load_factor = (i, i0); - hashmap_hash_map_max_load = ntable0.hashmap_hash_map_max_load; - hashmap_hash_map_slots = ntable0.hashmap_hash_map_slots - } - else - Return - { - hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; - hashmap_hash_map_max_load_factor = (i, i0); - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = self.hashmap_hash_map_slots + ntable0 + where + 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) } (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back @@ -392,13 +371,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 - { - hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; - hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v - } + Return { self where hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -490,14 +463,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 - { - hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; - hashmap_hash_map_max_load_factor = - self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v - } + Return { self where 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 @@ -506,11 +472,9 @@ let hashmap_hash_map_remove_back hash_mod l0 in Return { - hashmap_hash_map_num_entries = i0; - hashmap_hash_map_max_load_factor = - self.hashmap_hash_map_max_load_factor; - hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; - hashmap_hash_map_slots = v + self + where + hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v } end diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean index 5d355677..e161e066 100644 --- a/tests/lean/betree/BetreeMain/Funs.lean +++ b/tests/lean/betree/BetreeMain/Funs.lean @@ -919,8 +919,7 @@ def betree_node_apply_messages_back do let _ ← betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 Result.ret (betree_node_t.BetreeNodeLeaf - { betree_leaf_id := node.betree_leaf_id, betree_leaf_size := len }, - node_id_cnt) + { node with betree_leaf_size := len }, node_id_cnt) termination_by betree_node_apply_messages_back self params node_id_cnt msgs st => betree_node_apply_messages_terminates self params node_id_cnt msgs st @@ -1091,11 +1090,7 @@ def 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 Result.ret - { - betree_be_tree_params := self.betree_be_tree_params, - 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] -/ def betree_be_tree_insert_fwd @@ -1177,12 +1172,7 @@ def betree_be_tree_lookup_back := do let n ← betree_node_lookup_back self.betree_be_tree_root key st - Result.ret - { - 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 - } + Result.ret { self with betree_be_tree_root := n } /- [betree_main::main] -/ def main_fwd : Result Unit := diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 0b3708fa..0d83b04d 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -79,10 +79,10 @@ def hash_map_clear_fwd_back (USize.ofNatCore 0 (by intlit)) Result.ret { - hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v + self + with + hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), + hash_map_slots := v } /- [hashmap::HashMap::{0}::len] -/ @@ -149,23 +149,12 @@ def hash_map_insert_no_resize_fwd_back let l0 ← hash_map_insert_in_list_back T key value l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret - { - hash_map_num_entries := i0, - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v - } + { self with hash_map_num_entries := i0, hash_map_slots := v } else do let l0 ← hash_map_insert_in_list_back T key value l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 - Result.ret - { - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v - } + Result.ret { self with hash_map_slots := v } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : Result UInt32 := @@ -239,19 +228,12 @@ def hash_map_try_resize_fwd_back (USize.ofNatCore 0 (by intlit)) Result.ret { - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := (i, i0), - hash_map_max_load := ntable0.hash_map_max_load, - hash_map_slots := ntable0.hash_map_slots + ntable0 + with + hash_map_num_entries := self.hash_map_num_entries, + hash_map_max_load_factor := (i, i0) } - else - Result.ret - { - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := (i, i0), - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := self.hash_map_slots - } + else Result.ret { self with hash_map_max_load_factor := (i, i0) } /- [hashmap::HashMap::{0}::insert] -/ def hash_map_insert_fwd_back @@ -382,13 +364,7 @@ def hash_map_get_mut_back let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod let l0 ← hash_map_get_mut_in_list_back T l key ret0 let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 - Result.ret - { - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v - } + Result.ret { self with hash_map_slots := v } /- [hashmap::HashMap::{0}::remove_from_list] -/ def hash_map_remove_from_list_loop_fwd @@ -470,13 +446,7 @@ def hash_map_remove_back do let l0 ← hash_map_remove_from_list_back T key l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 - Result.ret - { - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v - } + Result.ret { self with hash_map_slots := v } | Option.some x0 => do let i0 ← USize.checked_sub self.hash_map_num_entries @@ -484,12 +454,7 @@ def hash_map_remove_back let l0 ← hash_map_remove_from_list_back T key l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret - { - hash_map_num_entries := i0, - hash_map_max_load_factor := self.hash_map_max_load_factor, - hash_map_max_load := self.hash_map_max_load, - hash_map_slots := v - } + { self with hash_map_num_entries := i0, hash_map_slots := v } /- [hashmap::test1] -/ def test1_fwd : Result Unit := diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 2d3904bb..bf3a30e9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -95,11 +95,10 @@ def hashmap_hash_map_clear_fwd_back hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots Result.ret { - hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v + self + with + hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), + hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::HashMap::{0}::len] -/ @@ -177,11 +176,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back hash_mod l0 Result.ret { - hashmap_hash_map_num_entries := i0, - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v + self + with + hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v } else do @@ -189,14 +186,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 - Result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } + Result.ret { self with hashmap_hash_map_slots := v } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : Result UInt32 := @@ -278,19 +268,12 @@ def hashmap_hash_map_try_resize_fwd_back self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) Result.ret { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0), - hashmap_hash_map_max_load := ntable0.hashmap_hash_map_max_load, - hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots + ntable0 + with + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0) } - else - Result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0), - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := self.hashmap_hash_map_slots - } + else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ def hashmap_hash_map_insert_fwd_back @@ -431,14 +414,7 @@ def hashmap_hash_map_get_mut_back let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 - Result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } + Result.ret { self with hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd @@ -533,14 +509,7 @@ def hashmap_hash_map_remove_back let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 - Result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } + Result.ret { self with hashmap_hash_map_slots := v } | Option.some x0 => do let i0 ← USize.checked_sub self.hashmap_hash_map_num_entries @@ -551,11 +520,9 @@ def hashmap_hash_map_remove_back hash_mod l0 Result.ret { - hashmap_hash_map_num_entries := i0, - hashmap_hash_map_max_load_factor := - self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v + self + with + hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::test1] -/ |