Improve simplify_aggregates to introduce structure updates

1 files changed, 9 insertions, 48 deletions

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 =