summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r--tests/fstar/misc/External.Funs.fst4
-rw-r--r--tests/fstar/misc/External.FunsExternal.fsti9
-rw-r--r--tests/fstar/misc/External.TypesExternal.fsti3
-rw-r--r--tests/fstar/misc/Loops.Funs.fst83
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst11
-rw-r--r--tests/fstar/misc/Paper.fst11
-rw-r--r--tests/fstar/misc/PoloniusList.fst4
7 files changed, 63 insertions, 62 deletions
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 3ba20022..78960404 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -34,8 +34,8 @@ let custom_swap
result (state & (t & (t -> state -> result (state & (t & t)))))
=
let* (st1, (x1, y1)) = core_mem_swap t x y st in
- let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
- Return (st1, (x1, back_'a))
+ let back = fun ret st2 -> Return (st2, (ret, y1)) in
+ Return (st1, (x1, back))
(** [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 *)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index a412aea9..4c1c58b7 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,16 +7,19 @@ include External.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+ Name pattern: core::mem::swap *)
val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+ Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
val core_num_nonzero_NonZeroU32_new
: u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
val core_option_Option_unwrap
(t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 4bfbe0c5..45174c7e 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -6,7 +6,8 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+ Name pattern: core::num::nonzero::NonZeroU32 *)
val core_num_nonzero_NonZeroU32_t : Type0
(** The state type used in the state-error monad *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 7c099da2..93683deb 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- let back_'b = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a, back_'b)
+ let back'a = fun ret -> Return (List_Cons ret tl0) in
+ let back'b = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back'a, back'b)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
- in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- let back_'b1 =
- fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
- Return (p, back_'a1, back_'b1)
+ let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in
+ let back'a1 =
+ fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in
+ let back'b1 =
+ fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in
+ Return (p, back'a1, back'b1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a =
+ let back =
fun ret ->
let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
- Return ((x0, x1), back_'a)
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
+ let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+ let back1 =
fun ret ->
- let* (tl01, tl11) = back_'a ret in
+ let* (tl01, tl11) = back ret in
Return (List_Cons x0 tl01, List_Cons x1 tl11) in
- Return (p, back_'a1)
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+ let back1 =
+ fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) =
- list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1
+ in
+ let back1 =
+ fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'b = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'b)
+ let back = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
- let back_'b1 =
- fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
- Return (p, back_'b1)
+ let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+ let back1 =
+ fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) =
- list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1
+ in
+ let back1 =
+ fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index db63eb0d..1a93beaa 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -291,8 +291,8 @@ let _ = assert_norm (test_split_list = Return ())
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [no_nested_borrows::choose_test]:
Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *)
@@ -355,15 +355,14 @@ let rec list_nth_mut
begin match l with
| List_Cons x tl ->
if i = 0
- then
- let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
in
- Return (x1, back_'a)
+ Return (x1, back)
| List_Nil -> Fail Failure
end
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index ddc5e7a8..c2f47ad1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ())
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -57,15 +57,14 @@ let rec list_nth_mut
begin match l with
| List_Cons x tl ->
if i = 0
- then
- let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
in
- Return (x1, back_'a)
+ Return (x1, back)
| List_Nil -> Fail Failure
end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index b477802b..4203247e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -23,10 +23,10 @@ let rec get_list_at_x
then Return (List_Cons hd tl, Return)
else
let* (l, get_list_at_x_back) = get_list_at_x tl x in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
- Return (l, back_'a)
+ Return (l, back)
| List_Nil -> Return (List_Nil, Return)
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 14:37:23 +0000