Improve simplify_aggregates to introduce structure updates

3 files changed, 35 insertions, 113 deletions

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] -/