diff options
Diffstat (limited to '')
| -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 |
5 files changed, 178 insertions, 58 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] *) |