diff options
author | Son Ho | 2024-03-09 00:49:10 +0100 |
---|---|---|
committer | Son Ho | 2024-03-09 00:49:10 +0100 |
commit | 181749b50ef5f71e8639a5c2e97be99a6710e698 (patch) | |
tree | 53c93e14776510b59f44104e70621bb9d4c6a98b /tests/coq | |
parent | 814f94b9e60818aac8060715e82edeffa6d5233f (diff) |
Regenerate the test files
Diffstat (limited to '')
-rw-r--r-- | tests/coq/arrays/Arrays.v | 69 | ||||
-rw-r--r-- | tests/coq/misc/Loops.v | 64 |
2 files changed, 133 insertions, 0 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 3a6fb02f..79be3678 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -516,4 +516,73 @@ Definition ite : result unit := Return tt . +(** [arrays::zero_slice]: loop 0: + Source: 'src/arrays.rs', lines 303:0-310:1 *) +Fixpoint zero_slice_loop + (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) := + match n with + | O => Fail_ OutOfFuel + | S n1 => + if i s< len + then ( + p <- slice_index_mut_usize u8 a i; + let (_, index_mut_back) := p in + i1 <- usize_add i 1%usize; + a1 <- index_mut_back 0%u8; + zero_slice_loop n1 a1 i1 len) + else Return a + end +. + +(** [arrays::zero_slice]: + Source: 'src/arrays.rs', lines 303:0-303:31 *) +Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) := + let len := slice_len u8 a in zero_slice_loop n a 0%usize len +. + +(** [arrays::iter_mut_slice]: loop 0: + Source: 'src/arrays.rs', lines 312:0-318:1 *) +Fixpoint iter_mut_slice_loop + (n : nat) (len : usize) (i : usize) : result unit := + match n with + | 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) + else Return tt + end +. + +(** [arrays::iter_mut_slice]: + Source: 'src/arrays.rs', lines 312:0-312:35 *) +Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) := + let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a +. + +(** [arrays::sum_mut_slice]: loop 0: + Source: 'src/arrays.rs', lines 320:0-328:1 *) +Fixpoint sum_mut_slice_loop + (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 := + match n with + | O => Fail_ OutOfFuel + | S n1 => + let i1 := slice_len u32 a in + if i s< i1 + then ( + i2 <- slice_index_usize u32 a i; + s1 <- u32_add s i2; + i3 <- usize_add i 1%usize; + sum_mut_slice_loop n1 a i3 s1) + else Return s + end +. + +(** [arrays::sum_mut_slice]: + Source: 'src/arrays.rs', lines 320:0-320:42 *) +Definition sum_mut_slice + (n : nat) (a : slice u32) : result (u32 * (slice u32)) := + i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a) +. + End Arrays. diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 8260db02..e235b60d 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge Return (p1, back_'a) . +(** [loops::ignore_input_mut_borrow]: loop 0: + Source: 'src/loops.rs', lines 345:0-349:1 *) +Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := + match n with + | 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) + else Return tt + end +. + +(** [loops::ignore_input_mut_borrow]: + Source: 'src/loops.rs', lines 345:0-345:56 *) +Definition ignore_input_mut_borrow + (n : nat) (_a : u32) (i : u32) : result u32 := + _ <- ignore_input_mut_borrow_loop n i; Return _a +. + +(** [loops::incr_ignore_input_mut_borrow]: loop 0: + Source: 'src/loops.rs', lines 353:0-358:1 *) +Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := + match n with + | 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) + else Return tt + end +. + +(** [loops::incr_ignore_input_mut_borrow]: + Source: 'src/loops.rs', lines 353:0-353:60 *) +Definition incr_ignore_input_mut_borrow + (n : nat) (a : u32) (i : u32) : result u32 := + a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1 +. + +(** [loops::ignore_input_shared_borrow]: loop 0: + Source: 'src/loops.rs', lines 362:0-366:1 *) +Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := + match n with + | 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) + else Return tt + end +. + +(** [loops::ignore_input_shared_borrow]: + Source: 'src/loops.rs', lines 362:0-362:59 *) +Definition ignore_input_shared_borrow + (n : nat) (_a : u32) (i : u32) : result u32 := + _ <- ignore_input_shared_borrow_loop n i; Return _a +. + End Loops. |