summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/Constants.v32
-rw-r--r--tests/coq/misc/External_Funs.v9
-rw-r--r--tests/coq/misc/Loops.v9
-rw-r--r--tests/coq/misc/NoNestedBorrows.v38
-rw-r--r--tests/coq/misc/Paper.v8
-rw-r--r--tests/coq/misc/PoloniusList.v4
6 files changed, 32 insertions, 68 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 7d3e5a34..acc15a13 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -23,10 +23,10 @@ Definition x2_body : result u32 := Return (3%u32).
Definition x2_c : u32 := x2_body%global.
(** [constants::incr] *)
-Definition incr_fwd (n : u32) : result u32 := i <- u32_add n 1%u32; Return i.
+Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32.
(** [constants::X3] *)
-Definition x3_body : result u32 := i <- incr_fwd (32%u32); Return i.
+Definition x3_body : result u32 := incr_fwd (32%u32).
Definition x3_c : u32 := x3_body%global.
(** [constants::mk_pair0] *)
@@ -47,15 +47,11 @@ Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
.
(** [constants::P0] *)
-Definition p0_body : result (u32 * u32) :=
- p <- mk_pair0_fwd (0%u32) (1%u32); Return p
-.
+Definition p0_body : result (u32 * u32) := mk_pair0_fwd (0%u32) (1%u32).
Definition p0_c : (u32 * u32) := p0_body%global.
(** [constants::P1] *)
-Definition p1_body : result (Pair_t u32 u32) :=
- p <- mk_pair1_fwd (0%u32) (1%u32); Return p
-.
+Definition p1_body : result (Pair_t u32 u32) := mk_pair1_fwd (0%u32) (1%u32).
Definition p1_c : Pair_t u32 u32 := p1_body%global.
(** [constants::P2] *)
@@ -80,16 +76,14 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
.
(** [constants::Y] *)
-Definition y_body : result (Wrap_t i32) :=
- w <- wrap_new_fwd i32 (2%i32); Return w
-.
+Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32).
Definition y_c : Wrap_t i32 := y_body%global.
(** [constants::unwrap_y] *)
Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val).
(** [constants::YVAL] *)
-Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i.
+Definition yval_body : result i32 := unwrap_y_fwd.
Definition yval_c : i32 := yval_body%global.
(** [constants::get_z1::Z1] *)
@@ -100,9 +94,7 @@ Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
Definition get_z1_fwd : result i32 := Return get_z1_z1_c.
(** [constants::add] *)
-Definition add_fwd (a : i32) (b : i32) : result i32 :=
- i <- i32_add a b; Return i
-.
+Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b.
(** [constants::Q1] *)
Definition q1_body : result i32 := Return (5%i32).
@@ -113,12 +105,12 @@ Definition q2_body : result i32 := Return q1_c.
Definition q2_c : i32 := q2_body%global.
(** [constants::Q3] *)
-Definition q3_body : result i32 := i <- add_fwd q2_c (3%i32); Return i.
+Definition q3_body : result i32 := add_fwd q2_c (3%i32).
Definition q3_c : i32 := q3_body%global.
(** [constants::get_z2] *)
Definition get_z2_fwd : result i32 :=
- i <- get_z1_fwd; i0 <- add_fwd i q3_c; i1 <- add_fwd q1_c i0; Return i1
+ i <- get_z1_fwd; i0 <- add_fwd i q3_c; add_fwd q1_c i0
.
(** [constants::S1] *)
@@ -126,7 +118,7 @@ Definition s1_body : result u32 := Return (6%u32).
Definition s1_c : u32 := s1_body%global.
(** [constants::S2] *)
-Definition s2_body : result u32 := i <- incr_fwd s1_c; Return i.
+Definition s2_body : result u32 := incr_fwd s1_c.
Definition s2_c : u32 := s2_body%global.
(** [constants::S3] *)
@@ -134,9 +126,7 @@ Definition s3_body : result (Pair_t u32 u32) := Return p3_c.
Definition s3_c : Pair_t u32 u32 := s3_body%global.
(** [constants::S4] *)
-Definition s4_body : result (Pair_t u32 u32) :=
- p <- mk_pair1_fwd (7%u32) (8%u32); Return p
-.
+Definition s4_body : result (Pair_t u32 u32) := mk_pair1_fwd (7%u32) (8%u32).
Definition s4_c : Pair_t u32 u32 := s4_body%global.
End Constants .
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 3ddc1cf3..90390c1b 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -41,9 +41,7 @@ Definition test_new_non_zero_u32_fwd
(x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) :=
p <- core_num_nonzero_non_zero_u32_new_fwd x st;
let (st0, opt) := p in
- p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0;
- let (st1, nzu) := p0 in
- Return (st1, nzu)
+ core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0
.
(** [external::test_vec] *)
@@ -94,10 +92,7 @@ Definition test_custom_swap_back
(x : u32) (y : u32) (st : state) (st0 : state) :
result (state * (u32 * u32))
:=
- p <- custom_swap_back u32 x y st (1%u32) st0;
- let (st1, p0) := p in
- let (x0, y0) := p0 in
- Return (st1, (x0, y0))
+ custom_swap_back u32 x y st (1%u32) st0
.
(** [external::test_swap_non_zero] *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 48de76c2..b3f27546 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -25,10 +25,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd
| ListCons x tl =>
if i s= 0%u32
then Return x
- else (
- i0 <- u32_sub i 1%u32;
- t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
- Return t)
+ else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop0_fwd T n0 tl i0)
| ListNil => Fail_ Failure
end
end
@@ -37,7 +34,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd
(** [loops::list_nth_mut_loop] *)
Definition list_nth_mut_loop_fwd
(T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
- t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
+ list_nth_mut_loop_loop0_fwd T n ls i
.
(** [loops::list_nth_mut_loop] *)
@@ -66,7 +63,7 @@ Definition list_nth_mut_loop_back
(T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
result (List_t T)
:=
- l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
+ list_nth_mut_loop_loop0_back T n ls i ret
.
End Loops .
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index a5f6126b..e91cf81a 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -46,37 +46,25 @@ Arguments SumLeft {T1} {T2} _.
Arguments SumRight {T1} {T2} _.
(** [no_nested_borrows::neg_test] *)
-Definition neg_test_fwd (x : i32) : result i32 := i <- i32_neg x; Return i.
+Definition neg_test_fwd (x : i32) : result i32 := i32_neg x.
(** [no_nested_borrows::add_test] *)
-Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
- i <- u32_add x y; Return i
-.
+Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y.
(** [no_nested_borrows::subs_test] *)
-Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
- i <- u32_sub x y; Return i
-.
+Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y.
(** [no_nested_borrows::div_test] *)
-Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
- i <- u32_div x y; Return i
-.
+Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y.
(** [no_nested_borrows::div_test1] *)
-Definition div_test1_fwd (x : u32) : result u32 :=
- i <- u32_div x 2%u32; Return i
-.
+Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32.
(** [no_nested_borrows::rem_test] *)
-Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
- i <- u32_rem x y; Return i
-.
+Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
(** [no_nested_borrows::cast_test] *)
-Definition cast_test_fwd (x : u32) : result i32 :=
- i <- scalar_cast U32 I32 x; Return i
-.
+Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
(** [no_nested_borrows::test2] *)
Definition test2_fwd : result unit :=
@@ -261,8 +249,7 @@ Arguments TreeNode {T} _ _ _.
(** [no_nested_borrows::list_length] *)
Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
match l with
- | ListCons t l1 =>
- i <- list_length_fwd T l1; i0 <- u32_add 1%u32 i; Return i0
+ | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i
| ListNil => Return (0%u32)
end
.
@@ -273,7 +260,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
| ListCons x tl =>
if i s= 0%u32
then Return x
- else (i0 <- u32_sub i 1%u32; t <- list_nth_shared_fwd T tl i0; Return t)
+ else (i0 <- u32_sub i 1%u32; list_nth_shared_fwd T tl i0)
| ListNil => Fail_ Failure
end
.
@@ -284,7 +271,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
| ListCons x tl =>
if i s= 0%u32
then Return x
- else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t)
+ else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0)
| ListNil => Fail_ Failure
end
.
@@ -308,7 +295,7 @@ Fixpoint list_nth_mut_back
Fixpoint list_rev_aux_fwd
(T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
match li with
- | ListCons hd tl => l <- list_rev_aux_fwd T tl (ListCons hd lo); Return l
+ | ListCons hd tl => list_rev_aux_fwd T tl (ListCons hd lo)
| ListNil => Return lo
end
.
@@ -316,8 +303,7 @@ Fixpoint list_rev_aux_fwd
(** [no_nested_borrows::list_rev] *)
Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) :=
let li := mem_replace_fwd (List_t T) l ListNil in
- l0 <- list_rev_aux_fwd T li ListNil;
- Return l0
+ list_rev_aux_fwd T li ListNil
.
(** [no_nested_borrows::test_list_functions] *)
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 616eed37..cb4486c6 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -7,9 +7,7 @@ Local Open Scope Primitives_scope.
Module Paper.
(** [paper::ref_incr] *)
-Definition ref_incr_fwd_back (x : i32) : result i32 :=
- x0 <- i32_add x 1%i32; Return x0
-.
+Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32.
(** [paper::test_incr] *)
Definition test_incr_fwd : result unit :=
@@ -63,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
| ListCons x tl =>
if i s= 0%u32
then Return x
- else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t)
+ else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0)
| ListNil => Fail_ Failure
end
.
@@ -86,7 +84,7 @@ Fixpoint list_nth_mut_back
(** [paper::sum] *)
Fixpoint sum_fwd (l : List_t i32) : result i32 :=
match l with
- | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0
+ | ListCons x tl => i <- sum_fwd tl; i32_add x i
| ListNil => Return (0%i32)
end
.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index a45c77c5..bd6df02e 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -19,9 +19,7 @@ Arguments ListNil {T}.
Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) :=
match ls with
| ListCons hd tl =>
- if hd s= x
- then Return (ListCons hd tl)
- else (l <- get_list_at_x_fwd tl x; Return l)
+ if hd s= x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
| ListNil => Return ListNil
end
.