Make a minor fix

5 files changed, 33 insertions, 46 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 476359f0..f3061273 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2061,13 +2061,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
     let var_name = ctx_get_var (Option.get supd.init) ctx in
     F.pp_print_string fmt var_name;
     F.pp_print_space fmt ();
-    let where_keyword =
-      match !backend with
-      | FStar -> "where"
-      | Lean -> "with"
-      | Coq -> raise (Failure "Unreachable")
-    in
-    F.pp_print_string fmt where_keyword;
+    F.pp_print_string fmt "with";
     F.pp_print_space fmt ());
   F.pp_open_hvbox fmt 0;
   let delimiter = match !backend with Lean -> "," | Coq | FStar -> ";" in
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index b098d8ca..0c868f47 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -469,10 +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 { self where betree_internal_left = n }
+    Return { self with betree_internal_left = n }
   else
     let* n = betree_node_lookup_back self.betree_internal_right key st in
-    Return { self where betree_internal_right = n }
+    Return { self with betree_internal_right = n }
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -785,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 { node where betree_leaf_size = len },
-        node_id_cnt)
+      Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt)
   end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
@@ -860,14 +859,14 @@ and betree_internal_flush_back
         betree_node_apply_messages_back self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
       Return
-        ({ self where betree_internal_left = n; betree_internal_right = n0 },
+        ({ self with betree_internal_left = n; betree_internal_right = n0 },
         node_id_cnt1)
-    else Return ({ self where betree_internal_left = n }, node_id_cnt0)
+    else Return ({ self with 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 ({ self where betree_internal_right = n }, node_id_cnt0)
+    Return ({ self with betree_internal_right = n }, node_id_cnt0)
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -939,7 +938,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
-    { self where betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n }
+    { self with betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n }
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -1004,7 +1003,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 { self where betree_be_tree_root = n }
+  Return { self with 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 eb1802fd..c70bef08 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -515,11 +515,11 @@ 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, { self where betree_internal_left = n })
+    Return (st1, { self with betree_internal_left = n })
   else
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_right key st st0 in
-    Return (st1, { self where betree_internal_right = n })
+    Return (st1, { self with betree_internal_right = n })
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -836,7 +836,7 @@ 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 { node where betree_leaf_size = len },
+      Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
         node_id_cnt))
   end
 
@@ -979,9 +979,9 @@ and betree_internal_flush_back'a
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st3 st5 in
       Return (st0,
-        ({ self where betree_internal_left = n; betree_internal_right = n0 },
+        ({ self with betree_internal_left = n; betree_internal_right = n0 },
         node_id_cnt1))
-    else Return (st0, ({ self where betree_internal_left = n }, node_id_cnt0))
+    else Return (st0, ({ self with betree_internal_left = n }, node_id_cnt0))
   else
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
@@ -992,7 +992,7 @@ 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, ({ self where betree_internal_right = n }, node_id_cnt0))
+    Return (st0, ({ self with betree_internal_right = n }, node_id_cnt0))
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back1
@@ -1154,7 +1154,7 @@ let betree_be_tree_apply_back
     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,
-    { self where betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n })
+    { self with betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n })
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -1235,7 +1235,7 @@ let betree_be_tree_lookup_back
   =
   let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0
     in
-  Return (st1, { self where betree_be_tree_root = n })
+  Return (st1, { self with 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 42ec35ee..44ad7463 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -69,7 +69,7 @@ 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 { self where hash_map_num_entries = 0; hash_map_slots = v }
+  Return { self with hash_map_num_entries = 0; hash_map_slots = v }
 
 (** [hashmap::HashMap::{0}::len] *)
 let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
@@ -130,11 +130,11 @@ 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 { self where hash_map_num_entries = i0; hash_map_slots = v }
+    Return { self with hash_map_num_entries = i0; 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 { self where hash_map_slots = v }
+    Return { self with hash_map_slots = v }
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -200,11 +200,11 @@ let hash_map_try_resize_fwd_back
     Return
       {
         ntable0
-          where
+          with
           hash_map_num_entries = self.hash_map_num_entries;
           hash_map_max_load_factor = (i, i0)
       }
-  else Return { self where hash_map_max_load_factor = (i, i0) }
+  else Return { self with hash_map_max_load_factor = (i, i0) }
 
 (** [hashmap::HashMap::{0}::insert] *)
 let hash_map_insert_fwd_back
@@ -331,7 +331,7 @@ 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 { self where hash_map_slots = v }
+  Return { self with hash_map_slots = v }
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_fwd
@@ -409,12 +409,12 @@ 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 { self where hash_map_slots = v }
+    Return { self with 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 { self where hash_map_num_entries = i0; hash_map_slots = v }
+    Return { self with hash_map_num_entries = i0; 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 cb8460c7..e8cd54c1 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -75,7 +75,7 @@ let hashmap_hash_map_clear_fwd_back
   let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
     in
   Return
-    { self where hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v }
+    { self with hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v }
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
 let hashmap_hash_map_len_fwd
@@ -145,17 +145,14 @@ let hashmap_hash_map_insert_no_resize_fwd_back
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
     Return
-      {
-        self
-          where
-          hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v
+      { self with hashmap_hash_map_num_entries = i0; 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 { self where hashmap_hash_map_slots = v }
+    Return { self with hashmap_hash_map_slots = v }
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -228,11 +225,11 @@ let hashmap_hash_map_try_resize_fwd_back
     Return
       {
         ntable0
-          where
+          with
           hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
           hashmap_hash_map_max_load_factor = (i, i0)
       }
-  else Return { self where hashmap_hash_map_max_load_factor = (i, i0) }
+  else Return { self with hashmap_hash_map_max_load_factor = (i, i0) }
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
 let hashmap_hash_map_insert_fwd_back
@@ -371,7 +368,7 @@ 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 { self where hashmap_hash_map_slots = v }
+  Return { self with hashmap_hash_map_slots = v }
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
@@ -463,7 +460,7 @@ 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 { self where hashmap_hash_map_slots = v }
+    Return { self with 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
@@ -471,10 +468,7 @@ let hashmap_hash_map_remove_back
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
     Return
-      {
-        self
-          where
-          hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v
+      { self with hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v
       }
   end