diff options
author | Son Ho | 2023-03-08 00:09:25 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | c00d77052e8cb778e5311a4344cf8449dd3726b6 (patch) | |
tree | 2bdf05a740e5607b0996ec6bbeef62a513bc4494 /tests/lean/hashmap_on_disk | |
parent | ca77353c20e425c687ba207023d56828de6495b6 (diff) |
Improve simplify_aggregates to introduce structure updates
Diffstat (limited to 'tests/lean/hashmap_on_disk')
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 69 |
1 files changed, 18 insertions, 51 deletions
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] -/ |