Start updating simplify_aggregates

1 files changed, 69 insertions, 20 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2a3ad87c..804f466a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -49,8 +49,13 @@ Definition hashmap_hash_map_new_with_capacity_fwd
   slots <- hashmap_hash_map_allocate_slots_fwd T n v capacity;
   i <- usize_mul capacity max_load_dividend;
   i0 <- usize_div i max_load_divisor;
-  Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend, max_load_divisor)
-    i0 slots)
+  Return
+    {|
+      Hashmap_hash_map_num_entries := (0%usize);
+      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] *)
@@ -85,8 +90,14 @@ Definition hashmap_hash_map_clear_fwd_back
   v <-
     hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots)
       (0%usize);
-  Return (mkHashmap_hash_map_t (0%usize)
-    self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
+  Return
+    {|
+      Hashmap_hash_map_num_entries := (0%usize);
+      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] *)
@@ -169,16 +180,27 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
     v <-
       vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
         hash_mod l0;
-    Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
-      self.(Hashmap_hash_map_max_load) v))
+    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
+      |})
   else (
     l0 <- hashmap_hash_map_insert_in_list_back T n key value l;
     v <-
       vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
         hash_mod l0;
-    Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
-      self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load)
-      v))
+    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
+      |})
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -263,11 +285,21 @@ Definition hashmap_hash_map_try_resize_fwd_back
       hashmap_hash_map_move_elements_fwd_back T n ntable
         self.(Hashmap_hash_map_slots) (0%usize);
     let (ntable0, _) := p in
-    Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0)
-      ntable0.(Hashmap_hash_map_max_load) ntable0.(Hashmap_hash_map_slots)))
+    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 (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0)
-      self.(Hashmap_hash_map_max_load) self.(Hashmap_hash_map_slots))
+    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)
+      |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
@@ -428,8 +460,14 @@ Definition hashmap_hash_map_get_mut_back
   v <-
     vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
       hash_mod l0;
-  Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
-    self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
+  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
+    |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
@@ -536,17 +574,28 @@ Definition hashmap_hash_map_remove_back
     v <-
       vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
         hash_mod l0;
-    Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
-      self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load)
-      v)
+    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
+      |}
   | Some x0 =>
     i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
     l0 <- hashmap_hash_map_remove_from_list_back T n key l;
     v <-
       vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
         hash_mod l0;
-    Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
-      self.(Hashmap_hash_map_max_load) v)
+    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
+      |}
   end
 .