summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/External_Funs.v4
-rw-r--r--tests/coq/misc/External_FunsExternal_Template.v9
-rw-r--r--tests/coq/misc/External_TypesExternal_Template.v3
-rw-r--r--tests/coq/misc/Loops.v78
-rw-r--r--tests/coq/misc/NoNestedBorrows.v12
-rw-r--r--tests/coq/misc/Paper.v12
-rw-r--r--tests/coq/misc/PoloniusList.v4
7 files changed, 63 insertions, 59 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index faf91fef..a6832854 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,8 +46,8 @@ Definition custom_swap
p <- core_mem_swap T x y st;
let (st1, p1) := p in
let (x1, y1) := p1 in
- let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
- Return (st1, (x1, back_'a))
+ let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+ Return (st1, (x1, back))
.
(** [external::test_custom_swap]:
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 6773ac18..24dd2d47 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,19 +12,22 @@ Include External_Types.
Module External_FunsExternal_Template.
(** [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 *)
Axiom core_mem_swap :
forall(T : Type), 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 *)
Axiom 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 *)
Axiom core_option_Option_unwrap :
forall(T : Type), option T -> state -> result (state * T)
.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7ba79d8e..7d6af202 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -10,7 +10,8 @@ Local Open Scope Primitives_scope.
Module External_TypesExternal_Template.
(** [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 *)
Axiom core_num_nonzero_NonZeroU32_t : Type.
(** The state type used in the state-error monad *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 7c83a014..ae529cf8 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a, back_'b)
+ let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
+ let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back'a, back'b)
else (
i1 <- u32_sub i 1%u32;
t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
- let '(p, back_'a, back_'b) := t in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- let back_'b1 :=
- fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
- Return (p, back_'a1, back_'b1))
+ let '(p, back'a, back'b) := t in
+ let back'a1 :=
+ fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+ let back'b1 :=
+ fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
+ Return (p, back'a1, back'b1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a :=
+ let back :=
fun (ret : (T * T)) =>
let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
in
- Return ((x0, x1), back_'a)
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
+ let (p1, back) := p in
+ let back1 :=
fun (ret : (T * T)) =>
- p2 <- back_'a ret;
+ p2 <- back ret;
let (tl01, tl11) := p2 in
Return (List_Cons x0 tl01, List_Cons x1 tl11) in
- Return (p1, back_'a1))
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'b)
+ let back := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
- let (p1, back_'b) := p in
- let back_'b1 :=
- fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
- Return (p1, back_'b1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 76dc4cf6..d4035104 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -321,8 +321,8 @@ Check (test_split_list )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
- else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+ then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+ else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
.
(** [no_nested_borrows::choose_test]:
@@ -399,16 +399,16 @@ Fixpoint list_nth_mut
| List_Cons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
- let back_'a :=
+ let back :=
fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
in
- Return (t, back_'a))
+ Return (t, back))
| List_Nil => Fail_ Failure
end
.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index ad77fa2a..77276223 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -27,8 +27,8 @@ Check (test_incr )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
- else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+ then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+ else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
.
(** [paper::test_choose]:
@@ -70,16 +70,16 @@ Fixpoint list_nth_mut
| List_Cons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
- let back_'a :=
+ let back :=
fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
in
- Return (t, back_'a))
+ Return (t, back))
| List_Nil => Fail_ Failure
end
.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index 8f403a8e..dfa09328 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -31,10 +31,10 @@ Fixpoint get_list_at_x
else (
p <- get_list_at_x tl x;
let (l, get_list_at_x_back) := p in
- let back_'a :=
+ let back :=
fun (ret : List_t u32) =>
tl1 <- get_list_at_x_back ret; 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-23 07:24:42 +0000