Start updating simplify_aggregates

5 files changed, 178 insertions, 58 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index fe22b029..dc97a9e9 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -56,7 +56,7 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
-  Return (mkBetree_node_id_counter_t (0%u64))
+  Return {| Betree_node_id_counter_next_node_id := (0%u64) |}
 .
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
@@ -70,7 +70,7 @@ Definition betree_node_id_counter_fresh_id_fwd
 Definition betree_node_id_counter_fresh_id_back
   (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
   i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
-  Return (mkBetree_node_id_counter_t i)
+  Return {| Betree_node_id_counter_next_node_id := i |}
 .
 
 (** [core::num::u64::{10}::MAX] *)
@@ -223,10 +223,16 @@ Definition betree_leaf_split_fwd
   let (st0, _) := p1 in
   p2 <- betree_store_leaf_node_fwd id1 content1 st0;
   let (st1, _) := p2 in
-  let n0 := BetreeNodeLeaf (mkBetree_leaf_t id0
-    params.(Betree_params_split_size)) in
-  let n1 := BetreeNodeLeaf (mkBetree_leaf_t id1
-    params.(Betree_params_split_size)) in
+  let n0 := BetreeNodeLeaf
+    {|
+      Betree_leaf_id := id0;
+      Betree_leaf_size := params.(Betree_params_split_size)
+    |} in
+  let n1 := BetreeNodeLeaf
+    {|
+      Betree_leaf_id := id1;
+      Betree_leaf_size := params.(Betree_params_split_size)
+    |} in
   Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
 .
 
@@ -903,8 +909,9 @@ with betree_node_apply_messages_back
         Return (BetreeNodeInternal new_node, node_id_cnt0))
       else (
         _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
-        Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len),
-          node_id_cnt))
+        Return (BetreeNodeLeaf
+          {| Betree_leaf_id := node.(Betree_leaf_id); Betree_leaf_size := len
+          |}, node_id_cnt))
     end
   end
 
@@ -1045,8 +1052,18 @@ Definition betree_be_tree_new_fwd
   p <- betree_store_leaf_node_fwd id BetreeListNil st;
   let (st0, _) := p in
   node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
-  Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0%u64))))
+  Return (st0,
+    {|
+      Betree_be_tree_params :=
+        {|
+          Betree_params_min_flush_size := min_flush_size;
+          Betree_params_split_size := split_size
+        |};
+      Betree_be_tree_node_id_cnt := node_id_cnt0;
+      Betree_be_tree_root :=
+        (BetreeNodeLeaf
+          {| Betree_leaf_id := id; Betree_leaf_size := (0%u64) |})
+    |})
 .
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
@@ -1075,7 +1092,12 @@ Definition betree_be_tree_apply_back
     betree_node_apply_back n self.(Betree_be_tree_root)
       self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
   let (n0, nic) := p in
-  Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n0)
+  Return
+    {|
+      Betree_be_tree_params := self.(Betree_be_tree_params);
+      Betree_be_tree_node_id_cnt := nic;
+      Betree_be_tree_root := n0
+    |}
 .
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
@@ -1151,8 +1173,12 @@ Definition betree_be_tree_lookup_back
   result Betree_be_tree_t
   :=
   n0 <- betree_node_lookup_back n self.(Betree_be_tree_root) key st;
-  Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
-    self.(Betree_be_tree_node_id_cnt) n0)
+  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 := n0
+    |}
 .
 
 (** [betree_main::main] *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index b952e60c..1245c654 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -47,8 +47,13 @@ Definition hash_map_new_with_capacity_fwd
   slots <- hash_map_allocate_slots_fwd T n v capacity;
   i <- usize_mul capacity max_load_dividend;
   i0 <- usize_div i max_load_divisor;
-  Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0
-    slots)
+  Return
+    {|
+      Hash_map_num_entries := (0%usize);
+      Hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
+      Hash_map_max_load := i0;
+      Hash_map_slots := slots
+    |}
 .
 
 (** [hashmap::HashMap::{0}::new] *)
@@ -78,8 +83,13 @@ Fixpoint hash_map_clear_loop_fwd_back
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
   v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize);
-  Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
-    self.(Hash_map_max_load) v)
+  Return
+    {|
+      Hash_map_num_entries := (0%usize);
+      Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+      Hash_map_max_load := self.(Hash_map_max_load);
+      Hash_map_slots := v
+    |}
 .
 
 (** [hashmap::HashMap::{0}::len] *)
@@ -156,13 +166,23 @@ Definition hash_map_insert_no_resize_fwd_back
     i0 <- usize_add self.(Hash_map_num_entries) 1%usize;
     l0 <- hash_map_insert_in_list_back T n key value l;
     v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-    Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
-      self.(Hash_map_max_load) v))
+    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
+      |})
   else (
     l0 <- hash_map_insert_in_list_back T n key value l;
     v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-    Return (mkHash_map_t self.(Hash_map_num_entries)
-      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v))
+    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
+      |})
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -242,11 +262,21 @@ Definition hash_map_try_resize_fwd_back
       hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots)
         (0%usize);
     let (ntable0, _) := p in
-    Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
-      ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots)))
+    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 (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
-      self.(Hash_map_max_load) self.(Hash_map_slots))
+    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)
+      |}
 .
 
 (** [hashmap::HashMap::{0}::insert] *)
@@ -396,8 +426,13 @@ Definition hash_map_get_mut_back
   l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
   l0 <- hash_map_get_mut_in_list_back T n l key ret;
   v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-  Return (mkHash_map_t self.(Hash_map_num_entries)
-    self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
+  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
+    |}
 .
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
@@ -487,14 +522,24 @@ Definition hash_map_remove_back
   | None =>
     l0 <- hash_map_remove_from_list_back T n key l;
     v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-    Return (mkHash_map_t self.(Hash_map_num_entries)
-      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
+    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
+      |}
   | Some x0 =>
     i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
     l0 <- hash_map_remove_from_list_back T n key l;
     v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-    Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
-      self.(Hash_map_max_load) v)
+    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
+      |}
   end
 .
 
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
 .
 
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 0a72558d..cd3880c2 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -44,7 +44,7 @@ Arguments Pair_y {T1} {T2}.
 
 (** [constants::mk_pair1] *)
 Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
-  Return (mkPair_t x y)
+  Return {| Pair_x := x; Pair_y := y |}
 .
 
 (** [constants::P0] *)
@@ -61,7 +61,7 @@ Definition p2_c : (u32 * u32) := p2_body%global.
 
 (** [constants::P3] *)
 Definition p3_body : result (Pair_t u32 u32) :=
-  Return (mkPair_t (0%u32) (1%u32))
+  Return {| Pair_x := (0%u32); Pair_y := (1%u32) |}
 .
 Definition p3_c : Pair_t u32 u32 := p3_body%global.
 
@@ -73,7 +73,7 @@ Arguments Wrap_val {T}.
 
 (** [constants::Wrap::{0}::new] *)
 Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
-  Return (mkWrap_t val)
+  Return {| Wrap_val := val |}
 .
 
 (** [constants::Y] *)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 98ed1cf6..826b52b6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -423,17 +423,17 @@ Arguments Struct_with_tuple_p {T1} {T2}.
 
 (** [no_nested_borrows::new_tuple1] *)
 Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
-  Return (mkStruct_with_tuple_t (1%u32, 2%u32))
+  Return {| Struct_with_tuple_p := (1%u32, 2%u32) |}
 .
 
 (** [no_nested_borrows::new_tuple2] *)
 Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
-  Return (mkStruct_with_tuple_t (1%i16, 2%i16))
+  Return {| Struct_with_tuple_p := (1%i16, 2%i16) |}
 .
 
 (** [no_nested_borrows::new_tuple3] *)
 Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
-  Return (mkStruct_with_tuple_t (1%u64, 2%i64))
+  Return {| Struct_with_tuple_p := (1%u64, 2%i64) |}
 .
 
 (** [no_nested_borrows::StructWithPair] *)
@@ -448,7 +448,7 @@ Arguments Struct_with_pair_p {T1} {T2}.
 
 (** [no_nested_borrows::new_pair1] *)
 Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
-  Return (mkStruct_with_pair_t (mkPair_t (1%u32) (2%u32)))
+  Return {| Struct_with_pair_p := {| Pair_x := (1%u32); Pair_y := (2%u32) |} |}
 .
 
 (** [no_nested_borrows::test_constants] *)