Start updating simplify_aggregates

6 files changed, 287 insertions, 88 deletions

diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f3a01884..4c541aaf 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -46,7 +46,7 @@ let betree_fresh_node_id_back (counter : u64) : result u64 =
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
-  Return (Mkbetree_node_id_counter_t 0)
+  Return { betree_node_id_counter_next_node_id = 0 }
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_fwd
@@ -58,7 +58,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
-  Return (Mkbetree_node_id_counter_t i)
+  Return { betree_node_id_counter_next_node_id = i }
 
 (** [core::num::u64::{10}::MAX] *)
 let core_num_u64_max_body : result u64 = Return 18446744073709551615
@@ -188,11 +188,19 @@ let betree_leaf_split_fwd
   let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
   let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in
   let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in
-  let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size)
-    in
-  let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size)
-    in
-  Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0)
+  let n = BetreeNodeLeaf
+    { betree_leaf_id = id0; betree_leaf_size = params.betree_params_split_size
+    } in
+  let n0 = BetreeNodeLeaf
+    { betree_leaf_id = id1; betree_leaf_size = params.betree_params_split_size
+    } in
+  Return (st1,
+    {
+      betree_internal_id = self.betree_leaf_id;
+      betree_internal_pivot = pivot;
+      betree_internal_left = n;
+      betree_internal_right = n0
+    })
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back
@@ -461,12 +469,22 @@ 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 (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right)
+    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
+      }
   else
     let* n = betree_node_lookup_back self.betree_internal_right key st in
-    Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n)
+    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
+      }
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -779,7 +797,8 @@ 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 (Mkbetree_leaf_t node.betree_leaf_id len),
+      Return (BetreeNodeLeaf
+        { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len },
         node_id_cnt)
   end
 
@@ -853,17 +872,32 @@ and betree_internal_flush_back
       let* (n0, node_id_cnt1) =
         betree_node_apply_messages_back self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1)
+      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 (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0)
+      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)
   else
     let* (n, node_id_cnt0) =
       betree_node_apply_messages_back self.betree_internal_right params
         node_id_cnt msgs_right st in
-    Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)
+    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)
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -901,8 +935,17 @@ let betree_be_tree_new_fwd
   let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in
   let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in
   let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
-  Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
+  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 })
+    })
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_fwd
@@ -925,7 +968,12 @@ let betree_be_tree_apply_back
   let* (n, nic) =
     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 (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
+  Return
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = nic;
+      betree_be_tree_root = n
+    }
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -990,8 +1038,12 @@ 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 (Mkbetree_be_tree_t self.betree_be_tree_params
-    self.betree_be_tree_node_id_cnt n)
+  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
+    }
 
 (** [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 7e44928c..1ca469ea 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -46,7 +46,7 @@ let betree_fresh_node_id_back (counter : u64) : result u64 =
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
-  Return (Mkbetree_node_id_counter_t 0)
+  Return { betree_node_id_counter_next_node_id = 0 }
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_fwd
@@ -58,7 +58,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
-  Return (Mkbetree_node_id_counter_t i)
+  Return { betree_node_id_counter_next_node_id = i }
 
 (** [core::num::u64::{10}::MAX] *)
 let core_num_u64_max_body : result u64 = Return 18446744073709551615
@@ -188,11 +188,19 @@ let betree_leaf_split_fwd
   let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
   let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in
   let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in
-  let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size)
-    in
-  let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size)
-    in
-  Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0)
+  let n = BetreeNodeLeaf
+    { betree_leaf_id = id0; betree_leaf_size = params.betree_params_split_size
+    } in
+  let n0 = BetreeNodeLeaf
+    { betree_leaf_id = id1; betree_leaf_size = params.betree_params_split_size
+    } in
+  Return (st1,
+    {
+      betree_internal_id = self.betree_leaf_id;
+      betree_internal_pivot = pivot;
+      betree_internal_left = n;
+      betree_internal_right = n0
+    })
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back0
@@ -507,13 +515,23 @@ 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, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right)
+    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
+      })
   else
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_right key st st0 in
-    Return (st1, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n)
+    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
+      })
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -830,7 +848,8 @@ 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 (Mkbetree_leaf_t node.betree_leaf_id len),
+      Return (st0, (BetreeNodeLeaf
+        { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len },
         node_id_cnt))
   end
 
@@ -972,11 +991,21 @@ and betree_internal_flush_back'a
       let* _ =
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st3 st5 in
-      Return (st0, (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1))
+      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, (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0))
+      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))
   else
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
@@ -987,8 +1016,13 @@ 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, (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0))
+    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))
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back1
@@ -1106,8 +1140,17 @@ let betree_be_tree_new_fwd
   let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in
   let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in
   let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
-  Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
+  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 })
+    })
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_fwd
@@ -1140,7 +1183,12 @@ let betree_be_tree_apply_back
   let* _ =
     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, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
+  Return (st0,
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = nic;
+      betree_be_tree_root = n
+    })
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -1221,8 +1269,12 @@ let betree_be_tree_lookup_back
   =
   let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0
     in
-  Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params
-    self.betree_be_tree_node_id_cnt n)
+  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
+    })
 
 (** [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 62799976..120f8323 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -39,7 +39,13 @@ let hash_map_new_with_capacity_fwd
   let* slots = hash_map_allocate_slots_fwd t v capacity in
   let* i = usize_mul capacity max_load_dividend in
   let* i0 = usize_div i max_load_divisor in
-  Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots)
+  Return
+    {
+      hash_map_num_entries = 0;
+      hash_map_max_load_factor = (max_load_dividend, max_load_divisor);
+      hash_map_max_load = i0;
+      hash_map_slots = slots
+    }
 
 (** [hashmap::HashMap::{0}::new] *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
@@ -63,8 +69,13 @@ 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 (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
-    v)
+  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
+    }
 
 (** [hashmap::HashMap::{0}::len] *)
 let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
@@ -125,13 +136,23 @@ 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 (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
     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 (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] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -194,11 +215,21 @@ let hash_map_try_resize_fwd_back
     let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in
     let* (ntable0, _) =
       hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 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] *)
 let hash_map_insert_fwd_back
@@ -325,8 +356,13 @@ 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 (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] *)
 let rec hash_map_remove_from_list_loop_fwd
@@ -404,14 +440,24 @@ 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 (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 ->
     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 (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
 
 (** [hashmap::test1] *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 7e1a7636..ae98386a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -42,8 +42,13 @@ let hashmap_hash_map_new_with_capacity_fwd
   let* slots = hashmap_hash_map_allocate_slots_fwd t v capacity in
   let* i = usize_mul capacity max_load_dividend in
   let* i0 = usize_div i max_load_divisor in
-  Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
-    slots)
+  Return
+    {
+      hashmap_hash_map_num_entries = 0;
+      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] *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
@@ -69,8 +74,13 @@ let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
     in
-  Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
-    self.hashmap_hash_map_max_load v)
+  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
+    }
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
 let hashmap_hash_map_len_fwd
@@ -139,15 +149,27 @@ let 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 in
-    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
     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 (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] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -217,11 +239,21 @@ let hashmap_hash_map_try_resize_fwd_back
     let* (ntable0, _) =
       hashmap_hash_map_move_elements_fwd_back t ntable
         self.hashmap_hash_map_slots 0 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] *)
 let hashmap_hash_map_insert_fwd_back
@@ -360,8 +392,13 @@ 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 (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] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
@@ -453,16 +490,28 @@ 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 (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 ->
     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
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
-    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
 
 (** [hashmap_main::hashmap::test1] *)
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index bf13ad43..bf2f0b1b 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -38,7 +38,7 @@ type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
 
 (** [constants::mk_pair1] *)
 let 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] *)
 let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1
@@ -53,7 +53,7 @@ let p2_body : result (u32 & u32) = Return (0, 1)
 let p2_c : (u32 & u32) = eval_global p2_body
 
 (** [constants::P3] *)
-let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_body : result (pair_t u32 u32) = Return { pair_x = 0; pair_y = 1 }
 let p3_c : pair_t u32 u32 = eval_global p3_body
 
 (** [constants::Wrap] *)
@@ -61,7 +61,7 @@ type wrap_t (t : Type0) = { wrap_val : t; }
 
 (** [constants::Wrap::{0}::new] *)
 let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
-  Return (Mkwrap_t val0)
+  Return { wrap_val = val0 }
 
 (** [constants::Y] *)
 let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 1e186c79..3770ab5d 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -353,15 +353,15 @@ type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); }
 
 (** [no_nested_borrows::new_tuple1] *)
 let new_tuple1_fwd : result (struct_with_tuple_t u32 u32) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple2] *)
 let new_tuple2_fwd : result (struct_with_tuple_t i16 i16) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple3] *)
 let new_tuple3_fwd : result (struct_with_tuple_t u64 i64) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::StructWithPair] *)
 type struct_with_pair_t (t1 t2 : Type0) =
@@ -371,7 +371,7 @@ type struct_with_pair_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::new_pair1] *)
 let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
-  Return (Mkstruct_with_pair_t (Mkpair_t 1 2))
+  Return { struct_with_pair_p = { pair_x = 1; pair_y = 2 } }
 
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =