From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Mar 2024 05:29:29 +0100 Subject: Regenerate the tests --- tests/coq/misc/Loops.v | 39 ++++++++++----------------------------- 1 file changed, 10 insertions(+), 29 deletions(-) (limited to 'tests/coq/misc/Loops.v') diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index e235b60d..85b54510 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -183,7 +183,7 @@ Definition list_nth_mut_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result (T * (T -> result (List_t T))) := - p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back) + list_nth_mut_loop_loop T n ls i . (** [loops::list_nth_shared_loop]: loop 0: @@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T))) := - t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i; - let '(p, back_'a, back_'b) := t in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair]: loop 0: @@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T)))) := - p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair_merge]: loop 0: @@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: @@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: @@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'b) := p in - Return (p1, back_'b) + list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: @@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::ignore_input_mut_borrow]: loop 0: @@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | 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) + then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | 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) + then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := | 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) + then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1) else Return tt end . -- cgit v1.2.3 From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 20 Mar 2024 06:17:41 +0100 Subject: Regenerate the code --- tests/coq/misc/Loops.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'tests/coq/misc/Loops.v') diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 85b54510..7c83a014 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 := (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) Fixpoint sum_with_mut_borrows_loop - (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := + (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n1 => - if mi s< max + if i s< max then ( - ms1 <- u32_add ms mi; - mi1 <- u32_add mi 1%u32; - sum_with_mut_borrows_loop n1 max mi1 ms1) - else u32_mul ms 2%u32 + ms <- u32_add s i; + mi <- u32_add i 1%u32; + sum_with_mut_borrows_loop n1 max mi ms) + else u32_mul s 2%u32 end . @@ -245,10 +245,10 @@ Definition get_elem_mut p <- alloc_vec_Vec_index_mut (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - let (l, index_mut_back) := p in - p1 <- get_elem_mut_loop n x l; + let (ls, index_mut_back) := p in + p1 <- get_elem_mut_loop n x ls; let (i, back) := p1 in - let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in + let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in Return (i, back1) . @@ -273,10 +273,10 @@ Definition get_elem_shared (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : result usize := - l <- + ls <- alloc_vec_Vec_index (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - get_elem_shared_loop n x l + get_elem_shared_loop n x ls . (** [loops::id_mut]: -- cgit v1.2.3