summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst57
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst57
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst65
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst66
-rw-r--r--tests/lean/betree/BetreeMain/Funs.lean16
-rw-r--r--tests/lean/hashmap/Hashmap/Funs.lean63
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean69
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] -/