summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/PureMicroPasses.ml45
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v52
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v81
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v89
-rw-r--r--tests/coq/misc/Constants.v6
-rw-r--r--tests/coq/misc/NoNestedBorrows.v8
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst98
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst98
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst80
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst85
-rw-r--r--tests/fstar/misc/Constants.fst6
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst8
-rw-r--r--tests/lean/betree/BetreeMain/Funs.lean227
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean22
-rw-r--r--tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean21
15 files changed, 632 insertions, 294 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 7e6ca822..7d01a622 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1078,6 +1078,8 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
method! visit_texpression env e =
match e.e with
| App _ -> (
+ (* TODO: we should remove this case, which dates from before the
+ introduction of [StructUpdate] *)
let app, args = destruct_apps e in
match app.e with
| Qualif
@@ -1141,6 +1143,43 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
else super#visit_texpression env e
else super#visit_texpression env e
| _ -> super#visit_texpression env e)
+ | StructUpdate { struct_id; init = None; updates } ->
+ let adt_ty = e.ty in
+ (* Attempt to convert all the field updates to projections
+ of fields from an ADT with the same type *)
+ let to_var_proj ((fid, arg) : FieldId.id * texpression) :
+ var_id option =
+ match arg.e with
+ | App (proj, x) -> (
+ match (proj.e, x.e) with
+ | ( Qualif
+ {
+ id = Proj { adt_id = AdtId proj_adt_id; field_id };
+ type_args = _;
+ },
+ Var v ) ->
+ (* We check that this is the proper ADT, and the proper field *)
+ if
+ proj_adt_id = struct_id && field_id = fid
+ && x.ty = adt_ty
+ then Some v
+ else None
+ | _ -> None)
+ | _ -> None
+ in
+ let var_projs = List.map to_var_proj updates in
+ let filt_var_projs = List.filter_map (fun x -> x) var_projs in
+ if filt_var_projs = [] then super#visit_texpression env e
+ else
+ (* If all the projections are from the same variable [x], we
+ simply replace the whole expression with [x] *)
+ let x = List.hd filt_var_projs in
+ if
+ List.length filt_var_projs = List.length updates
+ && List.for_all (fun y -> y = x) filt_var_projs
+ then { e with e = Var x }
+ else (* TODO *)
+ super#visit_texpression env e
| _ -> super#visit_texpression env e
end
in
@@ -1750,9 +1789,11 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
Ex.:
{[
- (* type struct = { f0 : nat; f1 : nat } *)
+ (* type struct = { f0 : nat; f1 : nat; f2 : nat } *)
- Mkstruct x.f0 x.f1 ~~> x
+ Mkstruct x.f0 x.f1 x.f2 ~~> x
+ { f0 := x.f0; f1 := x.f1; f2 := x.f2 } ~~> x
+ { f0 := x.f0; f1 := x.f1; f2 := v } ~~> { x with f2 = v }
]}
*)
let def = simplify_aggregates ctx def in
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] *)
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 =
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean
index e40ca4ca..5d355677 100644
--- a/tests/lean/betree/BetreeMain/Funs.lean
+++ b/tests/lean/betree/BetreeMain/Funs.lean
@@ -223,13 +223,7 @@ def betree_leaf_split_fwd
betree_leaf_id := id1,
betree_leaf_size := params.betree_params_split_size
}
- Result.ret (st1,
- {
- betree_internal_id := self.betree_leaf_id,
- betree_internal_pivot := pivot,
- betree_internal_left := n,
- betree_internal_right := n0
- })
+ Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0)
/- [betree_main::betree::Leaf::{3}::split] -/
def betree_leaf_split_back
@@ -380,8 +374,8 @@ mutual def betree_node_lookup_fwd
match h: self with
| betree_node_t.BetreeNodeInternal node =>
do
- let (st0, msgs) ←
- betree_load_internal_node_fwd node.betree_internal_id st
+ let (mkbetree_internal_t i i0 n n0) := node
+ let (st0, msgs) ← betree_load_internal_node_fwd i st
let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
match h: pending with
| betree_list_t.BetreeListCons p l =>
@@ -390,7 +384,8 @@ mutual def betree_node_lookup_fwd
then
do
let (st1, opt) ←
- betree_internal_lookup_in_children_fwd node key st0
+ betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0
+ n n0) key st0
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.BetreeListCons (k, msg) l)
@@ -414,25 +409,27 @@ mutual def betree_node_lookup_fwd
| betree_message_t.BetreeMessageUpsert ufs =>
do
let (st1, v) ←
- betree_internal_lookup_in_children_fwd node key st0
+ betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+ i0 n n0) key st0
let (st2, v0) ←
betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
betree_message_t.BetreeMessageUpsert ufs) l) v key st1
let node0 ←
- betree_internal_lookup_in_children_back node key st0
+ betree_internal_lookup_in_children_back (mkbetree_internal_t i
+ i0 n n0) key st0
+ let (mkbetree_internal_t i1 _ _ _) := node0
let pending0 ←
betree_node_apply_upserts_back (betree_list_t.BetreeListCons
(k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
let msgs0 ←
betree_node_lookup_first_message_for_key_back key msgs pending0
- let (st3, _) ←
- betree_store_internal_node_fwd node0.betree_internal_id msgs0
- st2
+ let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2
Result.ret (st3, Option.some v0)
| betree_list_t.BetreeListNil =>
do
let (st1, opt) ←
- betree_internal_lookup_in_children_fwd node key st0
+ betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
+ n0) key st0
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
betree_list_t.BetreeListNil
@@ -454,8 +451,8 @@ def betree_node_lookup_back
match h: self with
| betree_node_t.BetreeNodeInternal node =>
do
- let (st0, msgs) ←
- betree_load_internal_node_fwd node.betree_internal_id st
+ let (mkbetree_internal_t i i0 n n0) := node
+ let (st0, msgs) ← betree_load_internal_node_fwd i st
let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
match h: pending with
| betree_list_t.BetreeListCons p l =>
@@ -466,7 +463,9 @@ def betree_node_lookup_back
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.BetreeListCons (k, msg) l)
- let node0 ← betree_internal_lookup_in_children_back node key st0
+ let node0 ←
+ betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
+ n n0) key st0
Result.ret (betree_node_t.BetreeNodeInternal node0)
else
match h: msg with
@@ -476,38 +475,44 @@ def betree_node_lookup_back
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.BetreeListCons (k,
betree_message_t.BetreeMessageInsert v) l)
- Result.ret (betree_node_t.BetreeNodeInternal node)
+ Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+ i i0 n n0))
| betree_message_t.BetreeMessageDelete =>
do
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.BetreeListCons (k,
betree_message_t.BetreeMessageDelete) l)
- Result.ret (betree_node_t.BetreeNodeInternal node)
+ Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+ i i0 n n0))
| betree_message_t.BetreeMessageUpsert ufs =>
do
let (st1, v) ←
- betree_internal_lookup_in_children_fwd node key st0
+ betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+ i0 n n0) key st0
let (st2, _) ←
betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
betree_message_t.BetreeMessageUpsert ufs) l) v key st1
let node0 ←
- betree_internal_lookup_in_children_back node key st0
+ betree_internal_lookup_in_children_back (mkbetree_internal_t i
+ i0 n n0) key st0
+ let (mkbetree_internal_t i1 i2 n1 n2) := node0
let pending0 ←
betree_node_apply_upserts_back (betree_list_t.BetreeListCons
(k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
let msgs0 ←
betree_node_lookup_first_message_for_key_back key msgs pending0
- let _ ←
- betree_store_internal_node_fwd node0.betree_internal_id msgs0
- st2
- Result.ret (betree_node_t.BetreeNodeInternal node0)
+ let _ ← betree_store_internal_node_fwd i1 msgs0 st2
+ Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+ i1 i2 n1 n2))
| betree_list_t.BetreeListNil =>
do
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
betree_list_t.BetreeListNil
- let node0 ← betree_internal_lookup_in_children_back node key st0
+ let node0 ←
+ betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
+ n0) key st0
Result.ret (betree_node_t.BetreeNodeInternal node0)
| betree_node_t.BetreeNodeLeaf node =>
do
@@ -523,9 +528,10 @@ def betree_internal_lookup_in_children_fwd
(self : betree_internal_t) (key : UInt64) (st : State) :
(Result (State × (Option UInt64)))
:=
- if h: key < self.betree_internal_pivot
- then betree_node_lookup_fwd self.betree_internal_left key st
- else betree_node_lookup_fwd self.betree_internal_right key st
+ let (mkbetree_internal_t _ i n n0) := self
+ if h: key < i
+ then betree_node_lookup_fwd n key st
+ else betree_node_lookup_fwd n0 key st
termination_by betree_internal_lookup_in_children_fwd self key st =>
betree_internal_lookup_in_children_terminates self key st
decreasing_by betree_internal_lookup_in_children_decreases self key st
@@ -535,27 +541,16 @@ def betree_internal_lookup_in_children_back
(self : betree_internal_t) (key : UInt64) (st : State) :
(Result betree_internal_t)
:=
- if h: key < self.betree_internal_pivot
+ let (mkbetree_internal_t i i0 n n0) := self
+ if h: key < i0
then
do
- let n ← betree_node_lookup_back self.betree_internal_left key st
- Result.ret
- {
- 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
- }
+ let n1 ← betree_node_lookup_back n key st
+ Result.ret (mkbetree_internal_t i i0 n1 n0)
else
do
- let n ← betree_node_lookup_back self.betree_internal_right key st
- Result.ret
- {
- 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
- }
+ let n1 ← betree_node_lookup_back n0 key st
+ Result.ret (mkbetree_internal_t i i0 n n1)
termination_by betree_internal_lookup_in_children_back self key st =>
betree_internal_lookup_in_children_terminates self key st
decreasing_by betree_internal_lookup_in_children_decreases self key st
@@ -819,8 +814,8 @@ mutual def betree_node_apply_messages_fwd
match h: self with
| betree_node_t.BetreeNodeInternal node =>
do
- let (st0, content) ←
- betree_load_internal_node_fwd node.betree_internal_id st
+ let (mkbetree_internal_t i i0 n n0) := node
+ let (st0, content) ← betree_load_internal_node_fwd i st
let content0 ←
betree_node_apply_messages_to_internal_fwd_back content msgs
let num_msgs ←
@@ -829,17 +824,17 @@ mutual def betree_node_apply_messages_fwd
then
do
let (st1, content1) ←
- betree_internal_flush_fwd node params node_id_cnt content0 st0
+ betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+ node_id_cnt content0 st0
let (node0, _) ←
- betree_internal_flush_back node params node_id_cnt content0 st0
- let (st2, _) ←
- betree_store_internal_node_fwd node0.betree_internal_id content1
- st1
+ betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+ node_id_cnt content0 st0
+ let (mkbetree_internal_t i1 _ _ _) := node0
+ let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1
Result.ret (st2, ())
else
do
- let (st1, _) ←
- betree_store_internal_node_fwd node.betree_internal_id content0 st0
+ let (st1, _) ← betree_store_internal_node_fwd i content0 st0
Result.ret (st1, ())
| betree_node_t.BetreeNodeLeaf node =>
do
@@ -878,8 +873,8 @@ def betree_node_apply_messages_back
match h: self with
| betree_node_t.BetreeNodeInternal node =>
do
- let (st0, content) ←
- betree_load_internal_node_fwd node.betree_internal_id st
+ let (mkbetree_internal_t i i0 n n0) := node
+ let (st0, content) ← betree_load_internal_node_fwd i st
let content0 ←
betree_node_apply_messages_to_internal_fwd_back content msgs
let num_msgs ←
@@ -888,18 +883,20 @@ def betree_node_apply_messages_back
then
do
let (st1, content1) ←
- betree_internal_flush_fwd node params node_id_cnt content0 st0
+ betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+ node_id_cnt content0 st0
let (node0, node_id_cnt0) ←
- betree_internal_flush_back node params node_id_cnt content0 st0
- let _ ←
- betree_store_internal_node_fwd node0.betree_internal_id content1
- st1
- Result.ret (betree_node_t.BetreeNodeInternal node0, node_id_cnt0)
+ betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+ node_id_cnt content0 st0
+ let (mkbetree_internal_t i1 i2 n1 n2) := node0
+ let _ ← betree_store_internal_node_fwd i1 content1 st1
+ Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i1
+ i2 n1 n2), node_id_cnt0)
else
do
- let _ ←
- betree_store_internal_node_fwd node.betree_internal_id content0 st0
- Result.ret (betree_node_t.BetreeNodeInternal node, node_id_cnt)
+ let _ ← betree_store_internal_node_fwd i content0 st0
+ Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i
+ i0 n n0), node_id_cnt)
| betree_node_t.BetreeNodeLeaf node =>
do
let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
@@ -938,41 +935,36 @@ def betree_internal_flush_fwd
(Result (State × (betree_list_t (UInt64 × betree_message_t))))
:=
do
- let p ←
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot
+ let (mkbetree_internal_t _ i n n0) := self
+ let p ← betree_list_partition_at_pivot_fwd betree_message_t content i
let (msgs_left, msgs_right) := p
let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
if h: len_left >= params.betree_params_min_flush_size
then
do
let (st0, _) ←
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st
+ betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
let (_, node_id_cnt0) ←
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st
+ betree_node_apply_messages_back n params node_id_cnt msgs_left st
let len_right ←
betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
if h: len_right >= params.betree_params_min_flush_size
then
do
let (st1, _) ←
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt0 msgs_right st0
+ betree_node_apply_messages_fwd n0 params node_id_cnt0 msgs_right
+ st0
let _ ←
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0
+ betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
Result.ret (st1, betree_list_t.BetreeListNil)
else Result.ret (st0, msgs_right)
else
do
let (st0, _) ←
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt msgs_right st
+ betree_node_apply_messages_fwd n0 params node_id_cnt msgs_right st
let _ ←
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st
+ betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
Result.ret (st0, msgs_left)
termination_by betree_internal_flush_fwd self params node_id_cnt content st =>
betree_internal_flush_terminates self params node_id_cnt content st
@@ -987,55 +979,32 @@ def betree_internal_flush_back
(Result (betree_internal_t × betree_node_id_counter_t))
:=
do
- let p ←
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot
+ let (mkbetree_internal_t i i0 n n0) := self
+ let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0
let (msgs_left, msgs_right) := p
let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
if h: len_left >= params.betree_params_min_flush_size
then
do
let (st0, _) ←
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st
- let (n, node_id_cnt0) ←
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st
+ betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
+ let (n1, node_id_cnt0) ←
+ betree_node_apply_messages_back n params node_id_cnt msgs_left st
let len_right ←
betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
if h: len_right >= params.betree_params_min_flush_size
then
do
- let (n0, node_id_cnt1) ←
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0
- Result.ret
- ({
- 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
- Result.ret
- ({
- 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)
+ let (n2, node_id_cnt1) ←
+ betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
+ Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1)
+ else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0)
else
do
- let (n, node_id_cnt0) ←
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st
- Result.ret
- ({
- 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)
+ let (n1, node_id_cnt0) ←
+ betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
+ Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0)
termination_by betree_internal_flush_back self params node_id_cnt content st =>
betree_internal_flush_terminates self params node_id_cnt content st
decreasing_by
@@ -1082,16 +1051,18 @@ def betree_be_tree_new_fwd
let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
Result.ret (st0,
{
- betree_be_tree_params := {
- betree_params_min_flush_size := min_flush_size,
- betree_params_split_size := split_size
- },
+ 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 := (betree_node_t.BetreeNodeLeaf
- {
- betree_leaf_id := id,
- betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
- })
+ betree_be_tree_root :=
+ (betree_node_t.BetreeNodeLeaf
+ {
+ betree_leaf_id := id,
+ betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
+ })
})
/- [betree_main::betree::BeTree::{6}::apply] -/
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 392c8816..2d3904bb 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -49,8 +49,8 @@ def hashmap_hash_map_new_with_capacity_fwd
Result.ret
{
hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
- hashmap_hash_map_max_load_factor := (max_load_dividend,
- max_load_divisor),
+ hashmap_hash_map_max_load_factor :=
+ (max_load_dividend, max_load_divisor),
hashmap_hash_map_max_load := i0,
hashmap_hash_map_slots := slots
}
@@ -96,7 +96,8 @@ def hashmap_hash_map_clear_fwd_back
Result.ret
{
hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
- hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+ 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
}
@@ -177,7 +178,8 @@ def hashmap_hash_map_insert_no_resize_fwd_back
Result.ret
{
hashmap_hash_map_num_entries := i0,
- hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+ 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
}
@@ -190,7 +192,8 @@ def hashmap_hash_map_insert_no_resize_fwd_back
Result.ret
{
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_factor :=
+ self.hashmap_hash_map_max_load_factor,
hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
hashmap_hash_map_slots := v
}
@@ -431,7 +434,8 @@ def hashmap_hash_map_get_mut_back
Result.ret
{
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_factor :=
+ self.hashmap_hash_map_max_load_factor,
hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
hashmap_hash_map_slots := v
}
@@ -532,7 +536,8 @@ def hashmap_hash_map_remove_back
Result.ret
{
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_factor :=
+ self.hashmap_hash_map_max_load_factor,
hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
hashmap_hash_map_slots := v
}
@@ -547,7 +552,8 @@ def hashmap_hash_map_remove_back
Result.ret
{
hashmap_hash_map_num_entries := i0,
- hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+ 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
}
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
index cf7783b2..12d4190c 100644
--- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
@@ -458,24 +458,24 @@ structure OpaqueDefs where
def new_tuple1_fwd : Result (struct_with_tuple_t UInt32 UInt32) :=
Result.ret
{
- struct_with_tuple_p := ((UInt32.ofNatCore 1 (by intlit)),
- (UInt32.ofNatCore 2 (by intlit)))
+ struct_with_tuple_p :=
+ ((UInt32.ofNatCore 1 (by intlit)), (UInt32.ofNatCore 2 (by intlit)))
}
/- [no_nested_borrows::new_tuple2] -/
def new_tuple2_fwd : Result (struct_with_tuple_t Int16 Int16) :=
Result.ret
{
- struct_with_tuple_p := ((Int16.ofNatCore 1 (by intlit)),
- (Int16.ofNatCore 2 (by intlit)))
+ struct_with_tuple_p :=
+ ((Int16.ofNatCore 1 (by intlit)), (Int16.ofNatCore 2 (by intlit)))
}
/- [no_nested_borrows::new_tuple3] -/
def new_tuple3_fwd : Result (struct_with_tuple_t UInt64 Int64) :=
Result.ret
{
- struct_with_tuple_p := ((UInt64.ofNatCore 1 (by intlit)),
- (Int64.ofNatCore 2 (by intlit)))
+ struct_with_tuple_p :=
+ ((UInt64.ofNatCore 1 (by intlit)), (Int64.ofNatCore 2 (by intlit)))
}
/- [no_nested_borrows::StructWithPair] -/
@@ -486,10 +486,11 @@ structure OpaqueDefs where
def new_pair1_fwd : Result (struct_with_pair_t UInt32 UInt32) :=
Result.ret
{
- struct_with_pair_p := {
- pair_x := (UInt32.ofNatCore 1 (by intlit)),
- pair_y := (UInt32.ofNatCore 2 (by intlit))
- }
+ struct_with_pair_p :=
+ {
+ pair_x := (UInt32.ofNatCore 1 (by intlit)),
+ pair_y := (UInt32.ofNatCore 2 (by intlit))
+ }
}
/- [no_nested_borrows::test_constants] -/
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:46:01 +0000