Start updating simplify_aggregates

1 files changed, 67 insertions, 18 deletions

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] *)