summaryrefslogtreecommitdiff
path: root/tests/coq/arrays
diff options
context:
space:
mode:
authorSon HO2024-03-20 06:48:08 +0100
committerGitHub2024-03-20 06:48:08 +0100
commit0d52c3fe35d0b24de729bdfb917ad6c7104d0c6e (patch)
tree7748d3c19a0993edc710690491a2dc6ea3a2b58f /tests/coq/arrays
parent8111c970fcae9d609961eba2ad6716e8c9fc1046 (diff)
parent34850eed3c66f7f2c432294e4c589be53ad5d37b (diff)
Merge pull request #93 from AeneasVerif/son/examples
Add some examples and improve the shape of the generated code
Diffstat (limited to 'tests/coq/arrays')
-rw-r--r--tests/coq/arrays/Arrays.v31
1 files changed, 11 insertions, 20 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 34d163b7..049d63cb 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -30,27 +30,25 @@ Definition array_to_mut_slice_
(T : Type) (s : array T 32%usize) :
result ((slice T) * (slice T -> result (array T 32%usize)))
:=
- p <- array_to_slice_mut T 32%usize s;
- let (s1, to_slice_mut_back) := p in
- Return (s1, to_slice_mut_back)
+ array_to_slice_mut T 32%usize s
.
(** [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 *)
Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+ s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
.
(** [arrays::shared_array_len]:
Source: 'src/arrays.rs', lines 29:0-29:48 *)
Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+ s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
.
(** [arrays::shared_slice_len]:
Source: 'src/arrays.rs', lines 33:0-33:44 *)
Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
- let i := slice_len T s in Return i
+ Return (slice_len T s)
.
(** [arrays::index_array_shared]:
@@ -78,9 +76,7 @@ Definition index_mut_array
(T : Type) (s : array T 32%usize) (i : usize) :
result (T * (T -> result (array T 32%usize)))
:=
- p <- array_index_mut_usize T 32%usize s i;
- let (t, index_mut_back) := p in
- Return (t, index_mut_back)
+ array_index_mut_usize T 32%usize s i
.
(** [arrays::index_slice]:
@@ -95,9 +91,7 @@ Definition index_mut_slice
(T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T)))
:=
- p <- slice_index_mut_usize T s i;
- let (t, index_mut_back) := p in
- Return (t, index_mut_back)
+ slice_index_mut_usize T s i
.
(** [arrays::slice_subslice_shared_]:
@@ -136,9 +130,7 @@ Definition array_to_slice_mut_
(x : array u32 32%usize) :
result ((slice u32) * (slice u32 -> result (array u32 32%usize)))
:=
- p <- array_to_slice_mut u32 32%usize x;
- let (s, to_slice_mut_back) := p in
- Return (s, to_slice_mut_back)
+ array_to_slice_mut u32 32%usize x
.
(** [arrays::array_subslice_shared_]:
@@ -334,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) :=
Definition update_all : result unit :=
_ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
_ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
- a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
- p <- array_to_slice_mut u32 2%usize a;
+ x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
+ p <- array_to_slice_mut u32 2%usize x;
let (s, to_slice_mut_back) := p in
s1 <- update_mut_slice s;
_ <- to_slice_mut_back s1;
@@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit :=
(** [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 *)
Definition non_copyable_array : result unit :=
- _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt
+ take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ])
.
(** [arrays::sum]: loop 0:
@@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop
| O => Fail_ OutOfFuel
| S n1 =>
if i s< len
- then (
- i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+ then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
else Return tt
end
.