Improve simplify_aggregates to introduce structure updates

9 files changed, 127 insertions, 317 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8dd5910f..f2b5f00f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2054,7 +2054,13 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
     let var_name = ctx_get_var (Option.get supd.init) ctx in
     F.pp_print_string fmt var_name;
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "where";
+    let where_keyword =
+      match !backend with
+      | FStar -> "where"
+      | Lean -> "with"
+      | Coq -> raise (Failure "Unreachable")
+    in
+    F.pp_print_string fmt where_keyword;
     F.pp_print_space fmt ());
   F.pp_open_hvbox fmt 0;
   let delimiter = match !backend with Lean -> "," | Coq | FStar -> ";" in
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 7d01a622..74f3c576 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1178,8 +1178,47 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 List.length filt_var_projs = List.length updates
                 && List.for_all (fun y -> y = x) filt_var_projs
               then { e with e = Var x }
-              else (* TODO *)
-                super#visit_texpression env e
+              else if
+                (* Attempt to create an "update" expression (i.e., of
+                   the shape [{ x with f := v }]).
+
+                   This is not supported by Coq *)
+                !Config.backend <> Coq
+              then (
+                (* Compute the number of occurrences of each variable *)
+                let occurs = ref VarId.Map.empty in
+                List.iter
+                  (fun x ->
+                    let num =
+                      match VarId.Map.find_opt x !occurs with
+                      | None -> 1
+                      | Some n -> n + 1
+                    in
+                    occurs := VarId.Map.add x num !occurs)
+                  filt_var_projs;
+                (* Find the max - note that we can initialize the max at 0,
+                   because there is at least one variable *)
+                let max = ref 0 in
+                let x = ref x in
+                List.iter
+                  (fun (y, n) ->
+                    if n > !max then (
+                      max := n;
+                      x := y))
+                  (VarId.Map.bindings !occurs);
+                (* Create the update expression *)
+                let updates =
+                  List.filter_map
+                    (fun ((fid, fe), y_opt) ->
+                      if y_opt = Some !x then None else Some (fid, fe))
+                    (List.combine updates var_projs)
+                in
+                let supd =
+                  StructUpdate { struct_id; init = Some !x; updates }
+                in
+                let e = { e with e = supd } in
+                super#visit_texpression env e)
+              else super#visit_texpression env e
         | _ -> super#visit_texpression env e
     end
   in
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] -/