diff options
author | Son Ho | 2023-03-07 23:50:36 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | ca77353c20e425c687ba207023d56828de6495b6 (patch) | |
tree | 4a800459fb5ec27dcfb1f20e4d5d0d785bb07959 /tests | |
parent | fa76f1b94e1f68d520b02c0dc1072cb73fa9d8be (diff) |
Start updating simplify_aggregates
Diffstat (limited to 'tests')
-rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 52 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 81 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 89 | ||||
-rw-r--r-- | tests/coq/misc/Constants.v | 6 | ||||
-rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 8 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 98 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 98 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 80 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 85 | ||||
-rw-r--r-- | tests/fstar/misc/Constants.fst | 6 | ||||
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 8 | ||||
-rw-r--r-- | tests/lean/betree/BetreeMain/Funs.lean | 227 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 22 | ||||
-rw-r--r-- | tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean | 21 |
14 files changed, 589 insertions, 292 deletions
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] -/ |