summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
authorSon Ho2022-11-14 09:55:13 +0100
committerSon HO2022-11-14 14:21:04 +0100
commit019a9e34e6375a5e015e4978aad89aa8febc237c (patch)
treed49947453752ef5ecf17687e02c33c031d91995f /tests/coq
parent6eab7f1d8eeb7826d44c6bbacf24935965c8f7da (diff)
Improve the formatting of [if then else] expressions
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v132
-rw-r--r--tests/coq/misc/Paper.v24
2 files changed, 70 insertions, 86 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 9075d01d..774b8a1e 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -210,13 +210,12 @@ Definition choose_test_fwd : result unit :=
z0 <- i32_add z 1 %i32;
if negb (z0 s= 1 %i32)
then Fail_
- else
- (
- p <- choose_back i32 true (0 %i32) (0 %i32) z0;
- let (x, y) := p in
- if negb (x s= 1 %i32)
- then Fail_
- else if negb (y s= 0 %i32) then Fail_ else Return tt )
+ else (
+ p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+ let (x, y) := p in
+ if negb (x s= 1 %i32)
+ then Fail_
+ else if negb (y s= 0 %i32) then Fail_ else Return tt)
.
(** Unit test for [no_nested_borrows::choose_test] *)
@@ -258,7 +257,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; t <- list_nth_shared_fwd T tl i0; Return t)
| ListNil => Fail_
end
.
@@ -269,7 +268,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; t <- list_nth_mut_fwd T tl i0; Return t)
| ListNil => Fail_
end
.
@@ -281,11 +280,10 @@ Fixpoint list_nth_mut_back
| ListCons x tl =>
if i s= 0 %u32
then Return (ListCons ret tl)
- else
- (
- i0 <- u32_sub i 1 %u32;
- tl0 <- list_nth_mut_back T tl i0 ret;
- Return (ListCons x tl0) )
+ else (
+ i0 <- u32_sub i 1 %u32;
+ tl0 <- list_nth_mut_back T tl i0 ret;
+ Return (ListCons x tl0))
| ListNil => Fail_
end
.
@@ -314,39 +312,30 @@ Definition test_list_functions_fwd : result unit :=
i <- list_length_fwd i32 (ListCons (0 %i32) l1);
if negb (i s= 3 %u32)
then Fail_
- else
- (
- i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
- if negb (i0 s= 0 %i32)
+ else (
+ i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
+ if negb (i0 s= 0 %i32)
+ then Fail_
+ else (
+ i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
+ if negb (i1 s= 1 %i32)
then Fail_
- else
- (
- i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
- if negb (i1 s= 1 %i32)
+ else (
+ i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
+ if negb (i2 s= 2 %i32)
+ then Fail_
+ else (
+ ls <- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 %i32);
+ i3 <- list_nth_shared_fwd i32 ls (0 %u32);
+ if negb (i3 s= 0 %i32)
then Fail_
- else
- (
- i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
- if negb (i2 s= 2 %i32)
- then Fail_
- else
- (
- ls <-
- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3
- %i32);
- i3 <- list_nth_shared_fwd i32 ls (0 %u32);
- if negb (i3 s= 0 %i32)
- then Fail_
- else
- (
- i4 <- list_nth_shared_fwd i32 ls (1 %u32);
- if negb (i4 s= 3 %i32)
- then Fail_
- else
- (
- i5 <- list_nth_shared_fwd i32 ls (2 %u32);
- if negb (i5 s= 2 %i32) then Fail_ else Return tt ) )
- ) ) ) )
+ else (
+ i4 <- list_nth_shared_fwd i32 ls (1 %u32);
+ if negb (i4 s= 3 %i32)
+ then Fail_
+ else (
+ i5 <- list_nth_shared_fwd i32 ls (2 %u32);
+ if negb (i5 s= 2 %i32) then Fail_ else Return tt))))))
.
(** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -448,34 +437,31 @@ Definition test_constants_fwd : result unit :=
let (i, _) := p in
if negb (i s= 1 %u32)
then Fail_
- else
- (
- swt0 <- new_tuple2_fwd;
- match swt0 with
- | mkStruct_with_tuple_t p0 =>
- let (i0, _) := p0 in
- if negb (i0 s= 1 %i16)
- then Fail_
- else
- (
- swt1 <- new_tuple3_fwd;
- match swt1 with
- | mkStruct_with_tuple_t p1 =>
- let (i1, _) := p1 in
- if negb (i1 s= 1 %u64)
- then Fail_
- else
- (
- swp <- new_pair1_fwd;
- match swp with
- | mkStruct_with_pair_t p2 =>
- match p2 with
- | mkPair_t i2 i3 =>
- if negb (i2 s= 1 %u32) then Fail_ else Return tt
- end
- end )
- end )
- end )
+ else (
+ swt0 <- new_tuple2_fwd;
+ match swt0 with
+ | mkStruct_with_tuple_t p0 =>
+ let (i0, _) := p0 in
+ if negb (i0 s= 1 %i16)
+ then Fail_
+ else (
+ swt1 <- new_tuple3_fwd;
+ match swt1 with
+ | mkStruct_with_tuple_t p1 =>
+ let (i1, _) := p1 in
+ if negb (i1 s= 1 %u64)
+ then Fail_
+ else (
+ swp <- new_pair1_fwd;
+ match swp with
+ | mkStruct_with_pair_t p2 =>
+ match p2 with
+ | mkPair_t i2 i3 =>
+ if negb (i2 s= 1 %u32) then Fail_ else Return tt
+ end
+ end)
+ end)
+ end)
end
.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index e15e0dc1..25c01d7b 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -34,13 +34,12 @@ Definition test_choose_fwd : result unit :=
z0 <- i32_add z 1 %i32;
if negb (z0 s= 1 %i32)
then Fail_
- else
- (
- p <- choose_back i32 true (0 %i32) (0 %i32) z0;
- let (x, y) := p in
- if negb (x s= 1 %i32)
- then Fail_
- else if negb (y s= 0 %i32) then Fail_ else Return tt )
+ else (
+ p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+ let (x, y) := p in
+ if negb (x s= 1 %i32)
+ then Fail_
+ else if negb (y s= 0 %i32) then Fail_ else Return tt)
.
(** Unit test for [paper::test_choose] *)
@@ -61,7 +60,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; t <- list_nth_mut_fwd T tl i0; Return t)
| ListNil => Fail_
end
.
@@ -73,11 +72,10 @@ Fixpoint list_nth_mut_back
| ListCons x tl =>
if i s= 0 %u32
then Return (ListCons ret tl)
- else
- (
- i0 <- u32_sub i 1 %u32;
- tl0 <- list_nth_mut_back T tl i0 ret;
- Return (ListCons x tl0) )
+ else (
+ i0 <- u32_sub i 1 %u32;
+ tl0 <- list_nth_mut_back T tl i0 ret;
+ Return (ListCons x tl0))
| ListNil => Fail_
end
.