diff options
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 93 |
1 files changed, 71 insertions, 22 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 260c4254..6be1f757 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -39,8 +39,14 @@ def hashmap_hash_map_new_with_capacity_fwd let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity let i <- USize.checked_mul capacity max_load_dividend let i0 <- USize.checked_div i max_load_divisor - result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) - (max_load_dividend, max_load_divisor) i0 slots) + result.ret + { + hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), + hashmap_hash_map_max_load_factor := (max_load_dividend, + max_load_divisor), + hashmap_hash_map_max_load := i0, + hashmap_hash_map_slots := slots + } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := @@ -77,8 +83,13 @@ def hashmap_hash_map_clear_fwd_back do let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots - result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + 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 + } /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd @@ -147,18 +158,28 @@ 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 (mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load - v) + 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 + } else do let l0 <- hashmap_hash_map_insert_in_list_back T key value l let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load - v) + 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 + } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : result UInt32 := @@ -232,11 +253,23 @@ def hashmap_hash_map_try_resize_fwd_back let (ntable0, _) <- hashmap_hash_map_move_elements_fwd_back T ntable self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, - i0) ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) + 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 + } else - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, - i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + 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 + } /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ def hashmap_hash_map_insert_fwd_back @@ -369,8 +402,14 @@ 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 (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + 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 + } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd @@ -464,9 +503,14 @@ 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 (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load - v) + 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 + } | Option.some x0 => do let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries @@ -475,9 +519,14 @@ 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 (mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load - v) + 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 + } /- [hashmap_main::hashmap::test1] -/ |