summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/External_Funs.v6
-rw-r--r--tests/coq/misc/Loops.v61
-rw-r--r--tests/coq/misc/NoNestedBorrows.v9
-rw-r--r--tests/coq/misc/Paper.v2
-rw-r--r--tests/coq/misc/_CoqProject4
5 files changed, 29 insertions, 53 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 91ea88c9..faf91fef 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -45,9 +45,9 @@ Definition custom_swap
:=
p <- core_mem_swap T x y st;
let (st1, p1) := p in
- let (t, t1) := p1 in
- let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in
- Return (st1, (t, back_'a))
+ let (x1, y1) := p1 in
+ let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+ Return (st1, (x1, back_'a))
.
(** [external::test_custom_swap]:
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e235b60d..7c83a014 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 :=
(** [loops::sum_with_mut_borrows]: loop 0:
Source: 'src/loops.rs', lines 19:0-31:1 *)
Fixpoint sum_with_mut_borrows_loop
- (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+ (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
match n with
| O => Fail_ OutOfFuel
| S n1 =>
- if mi s< max
+ if i s< max
then (
- ms1 <- u32_add ms mi;
- mi1 <- u32_add mi 1%u32;
- sum_with_mut_borrows_loop n1 max mi1 ms1)
- else u32_mul ms 2%u32
+ ms <- u32_add s i;
+ mi <- u32_add i 1%u32;
+ sum_with_mut_borrows_loop n1 max mi ms)
+ else u32_mul s 2%u32
end
.
@@ -183,7 +183,7 @@ Definition list_nth_mut_loop
(T : Type) (n : nat) (ls : List_t T) (i : u32) :
result (T * (T -> result (List_t T)))
:=
- p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
+ list_nth_mut_loop_loop T n ls i
.
(** [loops::list_nth_shared_loop]: loop 0:
@@ -245,10 +245,10 @@ Definition get_elem_mut
p <-
alloc_vec_Vec_index_mut (List_t usize) usize
(core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
- let (l, index_mut_back) := p in
- p1 <- get_elem_mut_loop n x l;
+ let (ls, index_mut_back) := p in
+ p1 <- get_elem_mut_loop n x ls;
let (i, back) := p1 in
- let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+ let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
Return (i, back1)
.
@@ -273,10 +273,10 @@ Definition get_elem_shared
(n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
result usize
:=
- l <-
+ ls <-
alloc_vec_Vec_index (List_t usize) usize
(core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
- get_elem_shared_loop n x l
+ get_elem_shared_loop n x ls
.
(** [loops::id_mut]:
@@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
:=
- t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
- let '(p, back_'a, back_'b) := t in
- Return (p, back_'a, back_'b)
+ list_nth_mut_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
:=
- p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
- let (p1, back_'b) := p in
- Return (p1, back_'b)
+ list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::ignore_input_mut_borrow]: loop 0:
@@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
else Return tt
end
.
@@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32;
- _ <- incr_ignore_input_mut_borrow_loop n1 i1;
- Return tt)
+ then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
else Return tt
end
.
@@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32;
- _ <- ignore_input_shared_borrow_loop n1 i1;
- Return tt)
+ then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
else Return tt
end
.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 73c4ee58..76dc4cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -475,9 +475,7 @@ Definition id_mut_pair1
(T1 T2 : Type) (x : T1) (y : T2) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1)
- in
- Return ((x, y), back_'a)
+ Return ((x, y), Return)
.
(** [no_nested_borrows::id_mut_pair2]:
@@ -486,10 +484,7 @@ Definition id_mut_pair2
(T1 T2 : Type) (p : (T1 * T2)) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- let (t, t1) := p in
- let back_'a :=
- fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in
- Return ((t, t1), back_'a)
+ let (t, t1) := p in Return ((t, t1), Return)
.
(** [no_nested_borrows::id_mut_pair3]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 769cf34c..ad77fa2a 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
(** [paper::test_incr]:
Source: 'src/paper.rs', lines 8:0-8:18 *)
Definition test_incr : result unit :=
- i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt
+ x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_incr] *)
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 869cdb4d..308de4f4 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
-arg -w
-arg all
+External_FunsExternal_Template.v
Loops.v
External_Types.v
Primitives.v
@@ -10,9 +11,8 @@ External_Funs.v
External_TypesExternal.v
Constants.v
PoloniusList.v
-Paper.v
NoNestedBorrows.v
External_FunsExternal.v
Bitwise.v
External_TypesExternal_Template.v
-External_FunsExternal_Template.v
+Paper.v
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 22:18:30 +0000