summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst65
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst66
2 files changed, 26 insertions, 105 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-22 11:45:30 +0000