From 9cda6b33d667b861f371e89e7cccaf43135cfc7a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 21 Apr 2022 12:29:24 +0200 Subject: Regenerate the test files --- tests/hashmap/Hashmap.Funs.fst | 56 ++++++++++--------- tests/hashmap_on_disk/HashmapMain.Funs.fst | 89 ++++++++++++++++-------------- tests/misc/BetreeNll.fst | 2 +- tests/misc/External.Funs.fst | 2 +- tests/misc/NoNestedBorrows.fst | 18 +++--- tests/misc/Paper.fst | 12 ++-- 6 files changed, 93 insertions(+), 86 deletions(-) diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index 80783781..f75a0c01 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -21,13 +21,13 @@ let rec hash_map_allocate_slots_fwd | _ -> begin match vec_push_back (list_t t) slots ListNil with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_sub n 1 with | Fail -> Fail | Return i -> - begin match hash_map_allocate_slots_fwd t v i with + begin match hash_map_allocate_slots_fwd t slots0 i with | Fail -> Fail - | Return v0 -> Return v0 + | Return v -> Return v end end end @@ -72,13 +72,13 @@ let rec hash_map_clear_slots_fwd_back then begin match vec_index_mut_back (list_t t) slots i ListNil with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hash_map_clear_slots_fwd_back t v i1 with + begin match hash_map_clear_slots_fwd_back t slots0 i1 with | Fail -> Fail - | Return v0 -> Return v0 + | Return slots1 -> Return slots1 end end end @@ -129,7 +129,7 @@ let rec hash_map_insert_in_list_back else begin match hash_map_insert_in_list_back t key value ls0 with | Fail -> Fail - | Return l -> Return (ListCons ckey cvalue l) + | Return ls1 -> Return (ListCons ckey cvalue ls1) end | ListNil -> let l = ListNil in Return (ListCons key value l) end @@ -200,10 +200,10 @@ let rec hash_map_move_elements_from_list_fwd_back | ListCons k v tl -> begin match hash_map_insert_no_resize_fwd_back t ntable k v with | Fail -> Fail - | Return hm -> - begin match hash_map_move_elements_from_list_fwd_back t hm tl with + | Return ntable0 -> + begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with | Fail -> Fail - | Return hm0 -> Return hm0 + | Return ntable1 -> Return ntable1 end end | ListNil -> Return ntable @@ -224,17 +224,18 @@ let rec hash_map_move_elements_fwd_back let ls = mem_replace_fwd (list_t t) l ListNil in begin match hash_map_move_elements_from_list_fwd_back t ntable ls with | Fail -> Fail - | Return hm -> + | Return ntable0 -> let l0 = mem_replace_back (list_t t) l ListNil in begin match vec_index_mut_back (list_t t) slots i l0 with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hash_map_move_elements_fwd_back t hm v i1 with + begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1 + with | Fail -> Fail - | Return (hm0, v0) -> Return (hm0, v0) + | Return (ntable1, slots1) -> Return (ntable1, slots1) end end end @@ -265,9 +266,9 @@ let hash_map_try_resize_fwd_back hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 with | Fail -> Fail - | Return (hm, _) -> + | Return (ntable0, _) -> Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - hm.hash_map_max_load hm.hash_map_slots) + ntable0.hash_map_max_load ntable0.hash_map_slots) end end end @@ -284,22 +285,23 @@ let hash_map_insert_fwd_back = begin match hash_map_insert_no_resize_fwd_back t self key value with | Fail -> Fail - | Return hm -> - begin match hash_map_len_fwd t hm with + | Return self0 -> + begin match hash_map_len_fwd t self0 with | Fail -> Fail | Return i -> - if i > hm.hash_map_max_load + if i > self0.hash_map_max_load then begin match - hash_map_try_resize_fwd_back t (Mkhash_map_t hm.hash_map_num_entries - hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots) - with + hash_map_try_resize_fwd_back t (Mkhash_map_t + self0.hash_map_num_entries self0.hash_map_max_load_factor + self0.hash_map_max_load self0.hash_map_slots) with | Fail -> Fail - | Return hm0 -> Return hm0 + | Return self1 -> Return self1 end else - Return (Mkhash_map_t hm.hash_map_num_entries - hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots) + Return (Mkhash_map_t self0.hash_map_num_entries + self0.hash_map_max_load_factor self0.hash_map_max_load + self0.hash_map_slots) end end @@ -410,7 +412,7 @@ let rec hash_map_get_mut_in_list_back else begin match hash_map_get_mut_in_list_back t key ls0 ret with | Fail -> Fail - | Return l -> Return (ListCons ckey cvalue l) + | Return ls1 -> Return (ListCons ckey cvalue ls1) end | ListNil -> Fail end @@ -509,7 +511,7 @@ let rec hash_map_remove_from_list_back else begin match hash_map_remove_from_list_back t key tl with | Fail -> Fail - | Return l -> Return (ListCons ckey x l) + | Return tl0 -> Return (ListCons ckey x tl0) end | ListNil -> Return ListNil end diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index cf0df7a7..a4167186 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -23,13 +23,13 @@ let rec hashmap_hash_map_allocate_slots_fwd | _ -> begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_sub n 1 with | Fail -> Fail | Return i -> - begin match hashmap_hash_map_allocate_slots_fwd t v i st with + begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with | Fail -> Fail - | Return (st0, v0) -> Return (st0, v0) + | Return (st0, v) -> Return (st0, v) end end end @@ -77,11 +77,11 @@ let rec hashmap_hash_map_clear_slots_fwd begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hashmap_hash_map_clear_slots_fwd t v i1 st with + begin match hashmap_hash_map_clear_slots_fwd t slots0 i1 st with | Fail -> Fail | Return (st0, _) -> Return (st0, ()) end @@ -101,13 +101,13 @@ let rec hashmap_hash_map_clear_slots_back begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hashmap_hash_map_clear_slots_back t v i1 st with + begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with | Fail -> Fail - | Return (st0, v0) -> Return (st0, v0) + | Return (st0, slots1) -> Return (st0, slots1) end end end @@ -175,7 +175,7 @@ let rec hashmap_hash_map_insert_in_list_back else begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with | Fail -> Fail - | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l) + | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1) end | HashmapListNil -> let l = HashmapListNil in Return (st, HashmapListCons key value l) @@ -288,8 +288,9 @@ let rec hashmap_hash_map_move_elements_from_list_fwd | HashmapListCons k v tl -> begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with + | Return (st0, ntable0) -> + begin match hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0 + with | Fail -> Fail | Return (st1, _) -> Return (st1, ()) end @@ -309,11 +310,11 @@ let rec hashmap_hash_map_move_elements_from_list_back | HashmapListCons k v tl -> begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0 - with + | Return (st0, ntable0) -> + begin match + hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with | Fail -> Fail - | Return (st1, hm0) -> Return (st1, hm0) + | Return (st1, ntable1) -> Return (st1, ntable1) end end | HashmapListNil -> Return (st, ntable) @@ -336,15 +337,16 @@ let rec hashmap_hash_map_move_elements_fwd begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st with | Fail -> Fail - | Return (st0, hm) -> + | Return (st0, ntable0) -> let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with + begin match + hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with | Fail -> Fail | Return (st1, _) -> Return (st1, ()) end @@ -371,17 +373,19 @@ let rec hashmap_hash_map_move_elements_back begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st with | Fail -> Fail - | Return (st0, hm) -> + | Return (st0, ntable0) -> let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with | Fail -> Fail - | Return v -> + | Return slots0 -> begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with + begin match + hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 with | Fail -> Fail - | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0)) + | Return (st1, (ntable1, slots1)) -> + Return (st1, (ntable1, slots1)) end end end @@ -447,10 +451,11 @@ let hashmap_hash_map_try_resize_back hashmap_hash_map_move_elements_back t ntable self.hashmap_hash_map_slots 0 st0 with | Fail -> Fail - | Return (st1, (hm, _)) -> + | Return (st1, (ntable0, _)) -> Return (st1, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) + ntable0.hashmap_hash_map_max_load + ntable0.hashmap_hash_map_slots) end end end @@ -468,16 +473,18 @@ let hashmap_hash_map_insert_fwd = begin match hashmap_hash_map_insert_no_resize_back t self key value st with | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_len_fwd t hm st0 with + | Return (st0, self0) -> + begin match hashmap_hash_map_len_fwd t self0 st0 with | Fail -> Fail | Return (st1, i) -> - if i > hm.hashmap_hash_map_max_load + if i > self0.hashmap_hash_map_max_load then begin match hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t - hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor - hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with + self0.hashmap_hash_map_num_entries + self0.hashmap_hash_map_max_load_factor + self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) + st1 with | Fail -> Fail | Return (st2, _) -> Return (st2, ()) end @@ -493,23 +500,25 @@ let hashmap_hash_map_insert_back = begin match hashmap_hash_map_insert_no_resize_back t self key value st with | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_len_fwd t hm st0 with + | Return (st0, self0) -> + begin match hashmap_hash_map_len_fwd t self0 st0 with | Fail -> Fail | Return (st1, i) -> - if i > hm.hashmap_hash_map_max_load + if i > self0.hashmap_hash_map_max_load then begin match hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t - hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor - hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with + self0.hashmap_hash_map_num_entries + self0.hashmap_hash_map_max_load_factor + self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) + st1 with | Fail -> Fail - | Return (st2, hm0) -> Return (st2, hm0) + | Return (st2, self1) -> Return (st2, self1) end else - Return (st1, Mkhashmap_hash_map_t hm.hashmap_hash_map_num_entries - hm.hashmap_hash_map_max_load_factor hm.hashmap_hash_map_max_load - hm.hashmap_hash_map_slots) + Return (st1, Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries + self0.hashmap_hash_map_max_load_factor + self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) end end @@ -630,7 +639,7 @@ let rec hashmap_hash_map_get_mut_in_list_back else begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with | Fail -> Fail - | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l) + | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1) end | HashmapListNil -> Fail end @@ -740,7 +749,7 @@ let rec hashmap_hash_map_remove_from_list_back else begin match hashmap_hash_map_remove_from_list_back t key tl st with | Fail -> Fail - | Return (st0, l) -> Return (st0, HashmapListCons ckey x l) + | Return (st0, tl0) -> Return (st0, HashmapListCons ckey x tl0) end | HashmapListNil -> Return (st, HashmapListNil) end diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst index ae35827c..14c1d2ba 100644 --- a/tests/misc/BetreeNll.fst +++ b/tests/misc/BetreeNll.fst @@ -34,7 +34,7 @@ let rec get_list_at_x_back else begin match get_list_at_x_back tl x ret with | Fail -> Fail - | Return l -> Return (ListCons hd l) + | Return tl0 -> Return (ListCons hd tl0) end | ListNil -> Return ret end diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst index 927dad9c..57e9deee 100644 --- a/tests/misc/External.Funs.fst +++ b/tests/misc/External.Funs.fst @@ -22,7 +22,7 @@ let swap_back | Return (st0, x0) -> begin match core_mem_swap_back1 t x y st0 with | Fail -> Fail - | Return (st1, x1) -> Return (st1, (x0, x1)) + | Return (st1, y0) -> Return (st1, (x0, y0)) end end diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index e2457a72..8620f7e9 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -112,7 +112,7 @@ let _ = assert_norm (test_list1_fwd = Return ()) (** [no_nested_borrows::test_box1] *) let test_box1_fwd : result unit = - let i = 1 in let x = i in if not (x = 1) then Fail else Return () + let b = 1 in let x = b in if not (x = 1) then Fail else Return () (** Unit test for [no_nested_borrows::test_box1] *) let _ = assert_norm (test_box1_fwd = Return ()) @@ -192,10 +192,8 @@ let get_elem_test_fwd : result unit = else begin match get_elem_back i32 true 0 0 z0 with | Fail -> Fail - | Return (i, i0) -> - if not (i = 1) - then Fail - else if not (i0 = 0) then Fail else Return () + | Return (x, y) -> + if not (x = 1) then Fail else if not (y = 0) then Fail else Return () end end end @@ -334,7 +332,7 @@ let rec list_nth_mut_back | Return i0 -> begin match list_nth_mut_back t tl i0 ret with | Fail -> Fail - | Return l0 -> Return (ListCons x l0) + | Return tl0 -> Return (ListCons x tl0) end end end @@ -392,20 +390,20 @@ let test_list_functions_fwd : result unit = else begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with | Fail -> Fail - | Return l2 -> - begin match list_nth_shared_fwd i32 l2 0 with + | Return ls -> + begin match list_nth_shared_fwd i32 ls 0 with | Fail -> Fail | Return i3 -> if not (i3 = 0) then Fail else - begin match list_nth_shared_fwd i32 l2 1 with + begin match list_nth_shared_fwd i32 ls 1 with | Fail -> Fail | Return i4 -> if not (i4 = 3) then Fail else - begin match list_nth_shared_fwd i32 l2 2 with + begin match list_nth_shared_fwd i32 ls 2 with | Fail -> Fail | Return i5 -> if not (i5 = 2) then Fail else Return () diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst index a6ec184c..205227be 100644 --- a/tests/misc/Paper.fst +++ b/tests/misc/Paper.fst @@ -13,7 +13,7 @@ let ref_incr_fwd_back (x : i32) : result i32 = let test_incr_fwd : result unit = begin match ref_incr_fwd_back 0 with | Fail -> Fail - | Return i -> if not (i = 1) then Fail else Return () + | Return x -> if not (x = 1) then Fail else Return () end (** Unit test for [paper::test_incr] *) @@ -41,10 +41,8 @@ let test_choose_fwd : result unit = else begin match choose_back i32 true 0 0 z0 with | Fail -> Fail - | Return (i, i0) -> - if not (i = 1) - then Fail - else if not (i0 = 0) then Fail else Return () + | Return (x, y) -> + if not (x = 1) then Fail else if not (y = 0) then Fail else Return () end end end @@ -89,7 +87,7 @@ let rec list_nth_mut_back | Return i0 -> begin match list_nth_mut_back t tl i0 ret with | Fail -> Fail - | Return l0 -> Return (ListCons x l0) + | Return tl0 -> Return (ListCons x tl0) end end end @@ -144,7 +142,7 @@ let call_choose_fwd (p : (u32 & u32)) : result u32 = | Return pz0 -> begin match choose_back u32 true px py pz0 with | Fail -> Fail - | Return (i, _) -> Return i + | Return (px0, _) -> Return px0 end end end -- cgit v1.2.3