summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tests/hashmap/Hashmap.Funs.fst95
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst132
-rw-r--r--tests/misc/NoNestedBorrows.fst34
-rw-r--r--tests/misc/Paper.fst36
4 files changed, 149 insertions, 148 deletions
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 5a987799..80783781 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -42,14 +42,14 @@ let hash_map_new_with_capacity_fwd
let v = vec_new (list_t t) in
begin match hash_map_allocate_slots_fwd t v capacity with
| Fail -> Fail
- | Return v0 ->
+ | Return slots ->
begin match usize_mul capacity max_load_dividend with
| Fail -> Fail
| Return i ->
begin match usize_div i max_load_divisor with
| Fail -> Fail
| Return i0 ->
- Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0)
+ Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots)
end
end
end
@@ -141,9 +141,9 @@ let hash_map_insert_no_resize_fwd_back
=
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -152,12 +152,12 @@ let hash_map_insert_no_resize_fwd_back
| Return l ->
begin match hash_map_insert_in_list_fwd t key value l with
| Fail -> Fail
- | Return b ->
- if b
+ | Return inserted ->
+ if inserted
then
begin match usize_add self.hash_map_num_entries 1 with
| Fail -> Fail
- | Return i1 ->
+ | Return i0 ->
begin match hash_map_insert_in_list_back t key value l with
| Fail -> Fail
| Return l0 ->
@@ -166,7 +166,7 @@ let hash_map_insert_no_resize_fwd_back
with
| Fail -> Fail
| Return v ->
- Return (Mkhash_map_t i1 self.hash_map_max_load_factor
+ Return (Mkhash_map_t i0 self.hash_map_max_load_factor
self.hash_map_max_load v)
end
end
@@ -221,12 +221,12 @@ let rec hash_map_move_elements_fwd_back
begin match vec_index_mut_fwd (list_t t) slots i with
| Fail -> Fail
| Return l ->
- let l0 = mem_replace_fwd (list_t t) l ListNil in
- begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
+ 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 ->
- let l1 = mem_replace_back (list_t t) l ListNil in
- begin match vec_index_mut_back (list_t t) slots i l1 with
+ 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 ->
begin match usize_add i 1 with
@@ -245,33 +245,34 @@ let rec hash_map_move_elements_fwd_back
(** [hashmap::HashMap::{0}::try_resize] *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- let i = vec_len (list_t t) self.hash_map_slots in
+ let capacity = vec_len (list_t t) self.hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
| Return n1 ->
- let (i0, i1) = self.hash_map_max_load_factor in
- begin match usize_div n1 i0 with
+ let (i, i0) = self.hash_map_max_load_factor in
+ begin match usize_div n1 i with
| Fail -> Fail
- | Return i2 ->
- if i <= i2
+ | Return i1 ->
+ if capacity <= i1
then
- begin match usize_mul i 2 with
+ begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i3 ->
- begin match hash_map_new_with_capacity_fwd t i3 i0 i1 with
+ | Return i2 ->
+ begin match hash_map_new_with_capacity_fwd t i2 i i0 with
| Fail -> Fail
- | Return hm ->
+ | Return ntable ->
begin match
- hash_map_move_elements_fwd_back t hm self.hash_map_slots 0 with
+ hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
+ with
| Fail -> Fail
- | Return (hm0, _) ->
- Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
- hm0.hash_map_max_load hm0.hash_map_slots)
+ | Return (hm, _) ->
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+ hm.hash_map_max_load hm.hash_map_slots)
end
end
end
else
- Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
self.hash_map_max_load self.hash_map_slots)
end
end
@@ -325,9 +326,9 @@ let hash_map_contains_key_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result bool =
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
@@ -363,9 +364,9 @@ let hash_map_get_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
@@ -419,9 +420,9 @@ let hash_map_get_mut_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -443,9 +444,9 @@ let hash_map_get_mut_back
=
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -518,9 +519,9 @@ let hash_map_remove_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -548,9 +549,9 @@ let hash_map_remove_back
(t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
begin match hash_key_fwd key with
| Fail -> Fail
- | Return i ->
- let i0 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i0 with
+ | Return hash ->
+ let i = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -578,7 +579,7 @@ let hash_map_remove_back
| Some x0 ->
begin match usize_sub self.hash_map_num_entries 1 with
| Fail -> Fail
- | Return i1 ->
+ | Return i0 ->
begin match hash_map_remove_from_list_back t key l with
| Fail -> Fail
| Return l0 ->
@@ -587,7 +588,7 @@ let hash_map_remove_back
with
| Fail -> Fail
| Return v ->
- Return (Mkhash_map_t i1 self.hash_map_max_load_factor
+ Return (Mkhash_map_t i0 self.hash_map_max_load_factor
self.hash_map_max_load v)
end
end
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 89b9ef5b..cf0df7a7 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -44,7 +44,7 @@ let hashmap_hash_map_new_with_capacity_fwd
let v = vec_new (hashmap_list_t t) in
begin match hashmap_hash_map_allocate_slots_fwd t v capacity st with
| Fail -> Fail
- | Return (st0, v0) ->
+ | Return (st0, slots) ->
begin match usize_mul capacity max_load_dividend with
| Fail -> Fail
| Return i ->
@@ -52,7 +52,7 @@ let hashmap_hash_map_new_with_capacity_fwd
| Fail -> Fail
| Return i0 ->
Return (st0, Mkhashmap_hash_map_t 0 (max_load_dividend,
- max_load_divisor) i0 v0)
+ max_load_divisor) i0 slots)
end
end
end
@@ -189,9 +189,9 @@ let hashmap_hash_map_insert_no_resize_fwd
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -201,8 +201,8 @@ let hashmap_hash_map_insert_no_resize_fwd
| Return l ->
begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
| Fail -> Fail
- | Return (st1, b) ->
- if b
+ | Return (st1, inserted) ->
+ if inserted
then
begin match usize_add self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
@@ -222,9 +222,9 @@ let hashmap_hash_map_insert_no_resize_back
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -234,12 +234,12 @@ let hashmap_hash_map_insert_no_resize_back
| Return l ->
begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
| Fail -> Fail
- | Return (st1, b) ->
- if b
+ | Return (st1, inserted) ->
+ if inserted
then
begin match usize_add self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
- | Return i1 ->
+ | Return i0 ->
begin match
hashmap_hash_map_insert_in_list_back t key value l st1 with
| Fail -> Fail
@@ -249,7 +249,7 @@ let hashmap_hash_map_insert_no_resize_back
self.hashmap_hash_map_slots hash_mod l0 with
| Fail -> Fail
| Return v ->
- Return (st2, Mkhashmap_hash_map_t i1
+ Return (st2, Mkhashmap_hash_map_t i0
self.hashmap_hash_map_max_load_factor
self.hashmap_hash_map_max_load v)
end
@@ -332,13 +332,13 @@ let rec hashmap_hash_map_move_elements_fwd
begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
| Fail -> Fail
| Return l ->
- let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
- begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+ let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+ begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
with
| Fail -> Fail
| Return (st0, hm) ->
- let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
- begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
+ 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 ->
begin match usize_add i 1 with
@@ -367,13 +367,13 @@ let rec hashmap_hash_map_move_elements_back
begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
| Fail -> Fail
| Return l ->
- let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
- begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+ let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+ begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
with
| Fail -> Fail
| Return (st0, hm) ->
- let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
- begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
+ 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 ->
begin match usize_add i 1 with
@@ -394,24 +394,24 @@ let hashmap_hash_map_try_resize_fwd
(t : Type0) (self : hashmap_hash_map_t t) (st : state) :
result (state & unit)
=
- let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
| Return n1 ->
- let (i0, i1) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i0 with
+ let (i, i0) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i with
| Fail -> Fail
- | Return i2 ->
- if i <= i2
+ | Return i1 ->
+ if capacity <= i1
then
- begin match usize_mul i 2 with
+ begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i3 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+ | Return i2 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
| Fail -> Fail
- | Return (st0, hm) ->
+ | Return (st0, ntable) ->
begin match
- hashmap_hash_map_move_elements_back t hm
+ hashmap_hash_map_move_elements_back t ntable
self.hashmap_hash_map_slots 0 st0 with
| Fail -> Fail
| Return (st1, (_, _)) -> Return (st1, ())
@@ -427,36 +427,36 @@ let hashmap_hash_map_try_resize_back
(t : Type0) (self : hashmap_hash_map_t t) (st : state) :
result (state & (hashmap_hash_map_t t))
=
- let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
| Return n1 ->
- let (i0, i1) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i0 with
+ let (i, i0) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i with
| Fail -> Fail
- | Return i2 ->
- if i <= i2
+ | Return i1 ->
+ if capacity <= i1
then
- begin match usize_mul i 2 with
+ begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i3 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+ | Return i2 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
| Fail -> Fail
- | Return (st0, hm) ->
+ | Return (st0, ntable) ->
begin match
- hashmap_hash_map_move_elements_back t hm
+ hashmap_hash_map_move_elements_back t ntable
self.hashmap_hash_map_slots 0 st0 with
| Fail -> Fail
- | Return (st1, (hm0, _)) ->
+ | Return (st1, (hm, _)) ->
Return (st1, Mkhashmap_hash_map_t
- self.hashmap_hash_map_num_entries (i0, i1)
- hm0.hashmap_hash_map_max_load hm0.hashmap_hash_map_slots)
+ self.hashmap_hash_map_num_entries (i, i0)
+ hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots)
end
end
end
else
Return (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (
- i0, i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
end
end
@@ -538,9 +538,9 @@ let hashmap_hash_map_contains_key_fwd
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -581,9 +581,9 @@ let hashmap_hash_map_get_fwd
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -642,9 +642,9 @@ let hashmap_hash_map_get_mut_fwd
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -668,9 +668,9 @@ let hashmap_hash_map_get_mut_back
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -752,9 +752,9 @@ let hashmap_hash_map_remove_fwd
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -785,9 +785,9 @@ let hashmap_hash_map_remove_back
=
begin match hashmap_hash_key_fwd key st with
| Fail -> Fail
- | Return (st0, i) ->
- let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_rem i i0 with
+ | Return (st0, hash) ->
+ let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_rem hash i with
| Fail -> Fail
| Return hash_mod ->
begin match
@@ -817,7 +817,7 @@ let hashmap_hash_map_remove_back
| Some x0 ->
begin match usize_sub self.hashmap_hash_map_num_entries 1 with
| Fail -> Fail
- | Return i1 ->
+ | Return i0 ->
begin match hashmap_hash_map_remove_from_list_back t key l st1
with
| Fail -> Fail
@@ -827,7 +827,7 @@ let hashmap_hash_map_remove_back
self.hashmap_hash_map_slots hash_mod l0 with
| Fail -> Fail
| Return v ->
- Return (st2, Mkhashmap_hash_map_t i1
+ Return (st2, Mkhashmap_hash_map_t i0
self.hashmap_hash_map_max_load_factor
self.hashmap_hash_map_max_load v)
end
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index d272bb86..e2457a72 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -60,11 +60,11 @@ let get_max_fwd (x : u32) (y : u32) : result u32 =
let test3_fwd : result unit =
begin match get_max_fwd 4 3 with
| Fail -> Fail
- | Return i ->
+ | Return x ->
begin match get_max_fwd 10 11 with
| Fail -> Fail
- | Return i0 ->
- begin match u32_add i i0 with
+ | Return y ->
+ begin match u32_add x y with
| Fail -> Fail
| Return z -> if not (z = 15) then Fail else Return ()
end
@@ -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 i0 = i in if not (i0 = 1) then Fail else Return ()
+ let i = 1 in let x = i in if not (x = 1) then Fail else Return ()
(** Unit test for [no_nested_borrows::test_box1] *)
let _ = assert_norm (test_box1_fwd = Return ())
@@ -131,7 +131,7 @@ let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
let test_copy_int_fwd : result unit =
begin match copy_int_fwd 0 with
| Fail -> Fail
- | Return i -> if not (0 = i) then Fail else Return ()
+ | Return y -> if not (0 = y) then Fail else Return ()
end
(** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -183,19 +183,19 @@ let get_elem_back
let get_elem_test_fwd : result unit =
begin match get_elem_fwd i32 true 0 0 with
| Fail -> Fail
- | Return i ->
- begin match i32_add i 1 with
+ | Return z ->
+ begin match i32_add z 1 with
| Fail -> Fail
- | Return z ->
- if not (z = 1)
+ | Return z0 ->
+ if not (z0 = 1)
then Fail
else
- begin match get_elem_back i32 true 0 0 z with
+ begin match get_elem_back i32 true 0 0 z0 with
| Fail -> Fail
- | Return (i0, i1) ->
- if not (i0 = 1)
+ | Return (i, i0) ->
+ if not (i = 1)
then Fail
- else if not (i1 = 0) then Fail else Return ()
+ else if not (i0 = 0) then Fail else Return ()
end
end
end
@@ -355,10 +355,10 @@ let rec list_rev_aux_fwd
(** [no_nested_borrows::list_rev] *)
let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
- let l0 = mem_replace_fwd (list_t t) l ListNil in
- begin match list_rev_aux_fwd t ListNil l0 with
+ let li = mem_replace_fwd (list_t t) l ListNil in
+ begin match list_rev_aux_fwd t ListNil li with
| Fail -> Fail
- | Return l1 -> Return l1
+ | Return l0 -> Return l0
end
(** [no_nested_borrows::test_list_functions] *)
@@ -536,7 +536,7 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
(** [no_nested_borrows::test_mem_replace] *)
let test_mem_replace_fwd_back (px : u32) : result u32 =
- let i = mem_replace_fwd u32 px 1 in if not (i = 0) then Fail else Return 2
+ let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
(** [no_nested_borrows::test_shared_borrow_bool1] *)
let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index 1278733b..a6ec184c 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -32,19 +32,19 @@ let choose_back
let test_choose_fwd : result unit =
begin match choose_fwd i32 true 0 0 with
| Fail -> Fail
- | Return i ->
- begin match i32_add i 1 with
+ | Return z ->
+ begin match i32_add z 1 with
| Fail -> Fail
- | Return z ->
- if not (z = 1)
+ | Return z0 ->
+ if not (z0 = 1)
then Fail
else
- begin match choose_back i32 true 0 0 z with
+ begin match choose_back i32 true 0 0 z0 with
| Fail -> Fail
- | Return (i0, i1) ->
- if not (i0 = 1)
+ | Return (i, i0) ->
+ if not (i = 1)
then Fail
- else if not (i1 = 0) then Fail else Return ()
+ else if not (i0 = 0) then Fail else Return ()
end
end
end
@@ -115,16 +115,16 @@ let test_nth_fwd : result unit =
let l1 = ListCons 2 l0 in
begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
| Fail -> Fail
- | Return i ->
- begin match i32_add i 1 with
+ | Return x ->
+ begin match i32_add x 1 with
| Fail -> Fail
- | Return x ->
- begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x with
+ | Return x0 ->
+ begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
| Fail -> Fail
| Return l2 ->
begin match sum_fwd l2 with
| Fail -> Fail
- | Return i0 -> if not (i0 = 7) then Fail else Return ()
+ | Return i -> if not (i = 7) then Fail else Return ()
end
end
end
@@ -138,13 +138,13 @@ let call_choose_fwd (p : (u32 & u32)) : result u32 =
let (px, py) = p in
begin match choose_fwd u32 true px py with
| Fail -> Fail
- | Return i ->
- begin match u32_add i 1 with
+ | Return pz ->
+ begin match u32_add pz 1 with
| Fail -> Fail
- | Return pz ->
- begin match choose_back u32 true px py pz with
+ | Return pz0 ->
+ begin match choose_back u32 true px py pz0 with
| Fail -> Fail
- | Return (i0, _) -> Return i0
+ | Return (i, _) -> Return i
end
end
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 13:07:36 +0000