From ce8614be6bd96c51756bf5922b5dfd4c59650dd4 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 30 May 2024 12:33:05 +0200 Subject: Implement two phases of loops join + collapse --- tests/coq/arrays/Arrays.v | 68 +++-------------------------------------------- 1 file changed, 3 insertions(+), 65 deletions(-) (limited to 'tests/coq/arrays') diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 35dea58c..b7bef7c7 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -375,58 +375,15 @@ Definition non_copyable_array : result unit := take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]) . -(** [arrays::sum]: loop 0: - Source: 'tests/src/arrays.rs', lines 242:0-250:1 *) -Fixpoint sum_loop - (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := slice_len u32 s in - if i s< i1 - then ( - i2 <- slice_index_usize u32 s i; - sum3 <- u32_add sum1 i2; - i3 <- usize_add i 1%usize; - sum_loop n1 s sum3 i3) - else Ok sum1 - end -. - (** [arrays::sum]: Source: 'tests/src/arrays.rs', lines 242:0-242:28 *) Definition sum (n : nat) (s : slice u32) : result u32 := - sum_loop n s 0%u32 0%usize -. - -(** [arrays::sum2]: loop 0: - Source: 'tests/src/arrays.rs', lines 252:0-261:1 *) -Fixpoint sum2_loop - (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) : - result u32 - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := slice_len u32 s in - if i s< i1 - then ( - i2 <- slice_index_usize u32 s i; - i3 <- slice_index_usize u32 s2 i; - i4 <- u32_add i2 i3; - sum3 <- u32_add sum1 i4; - i5 <- usize_add i 1%usize; - sum2_loop n1 s s2 sum3 i5) - else Ok sum1 - end -. + admit. (** [arrays::sum2]: Source: 'tests/src/arrays.rs', lines 252:0-252:41 *) Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 := - let i := slice_len u32 s in - let i1 := slice_len u32 s2 in - if negb (i s= i1) then Fail_ Failure else sum2_loop n s s2 0%u32 0%usize + admit . (** [arrays::f0]: @@ -507,29 +464,10 @@ Definition ite : result unit := Ok tt . -(** [arrays::zero_slice]: loop 0: - Source: 'tests/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 Ok a - end -. - (** [arrays::zero_slice]: Source: 'tests/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 -. + admit. (** [arrays::iter_mut_slice]: loop 0: Source: 'tests/src/arrays.rs', lines 312:0-318:1 *) -- cgit v1.2.3 From 092dae81f5f90281b634e229102d2dff7f5c3fd7 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 13:09:37 +0200 Subject: Regenerate test output --- tests/coq/arrays/Arrays.v | 68 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 65 insertions(+), 3 deletions(-) (limited to 'tests/coq/arrays') diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index b7bef7c7..35dea58c 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -375,15 +375,58 @@ Definition non_copyable_array : result unit := take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]) . +(** [arrays::sum]: loop 0: + Source: 'tests/src/arrays.rs', lines 242:0-250:1 *) +Fixpoint sum_loop + (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 := + match n with + | O => Fail_ OutOfFuel + | S n1 => + let i1 := slice_len u32 s in + if i s< i1 + then ( + i2 <- slice_index_usize u32 s i; + sum3 <- u32_add sum1 i2; + i3 <- usize_add i 1%usize; + sum_loop n1 s sum3 i3) + else Ok sum1 + end +. + (** [arrays::sum]: Source: 'tests/src/arrays.rs', lines 242:0-242:28 *) Definition sum (n : nat) (s : slice u32) : result u32 := - admit. + sum_loop n s 0%u32 0%usize +. + +(** [arrays::sum2]: loop 0: + Source: 'tests/src/arrays.rs', lines 252:0-261:1 *) +Fixpoint sum2_loop + (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) : + result u32 + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + let i1 := slice_len u32 s in + if i s< i1 + then ( + i2 <- slice_index_usize u32 s i; + i3 <- slice_index_usize u32 s2 i; + i4 <- u32_add i2 i3; + sum3 <- u32_add sum1 i4; + i5 <- usize_add i 1%usize; + sum2_loop n1 s s2 sum3 i5) + else Ok sum1 + end +. (** [arrays::sum2]: Source: 'tests/src/arrays.rs', lines 252:0-252:41 *) Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 := - admit + let i := slice_len u32 s in + let i1 := slice_len u32 s2 in + if negb (i s= i1) then Fail_ Failure else sum2_loop n s s2 0%u32 0%usize . (** [arrays::f0]: @@ -464,10 +507,29 @@ Definition ite : result unit := Ok tt . +(** [arrays::zero_slice]: loop 0: + Source: 'tests/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 Ok a + end +. + (** [arrays::zero_slice]: Source: 'tests/src/arrays.rs', lines 303:0-303:31 *) Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) := - admit. + let len := slice_len u8 a in zero_slice_loop n a 0%usize len +. (** [arrays::iter_mut_slice]: loop 0: Source: 'tests/src/arrays.rs', lines 312:0-318:1 *) -- cgit v1.2.3 From 2e3d1cdfde3e19af97e0d0fa47f92cfd66c688d9 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 14:25:23 +0200 Subject: Regenerate tests --- tests/coq/arrays/_CoqProject | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/coq/arrays') diff --git a/tests/coq/arrays/_CoqProject b/tests/coq/arrays/_CoqProject index a4e82408..4ccc7663 100644 --- a/tests/coq/arrays/_CoqProject +++ b/tests/coq/arrays/_CoqProject @@ -3,5 +3,5 @@ -arg -w -arg all -Arrays.v +Arrays.v Primitives.v -- cgit v1.2.3