From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 16:20:20 +0200 Subject: Regenerate the test files --- tests/coq/misc/Loops.v | 120 +++++++++++++++++++++++-------------------------- 1 file changed, 55 insertions(+), 65 deletions(-) (limited to 'tests/coq/misc/Loops.v') diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index ae529cf8..f396f16f 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -83,7 +83,7 @@ Fixpoint sum_array_loop s1 <- u32_add s i1; i2 <- usize_add i 1%usize; sum_array_loop N n1 a i2 s1) - else Return s + else Ok s end . @@ -110,7 +110,7 @@ Fixpoint clear_loop i2 <- usize_add i 1%usize; v1 <- index_mut_back 0%u32; clear_loop n1 v1 i2) - else Return v + else Ok v end . @@ -138,8 +138,8 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool := | O => Fail_ OutOfFuel | S n1 => match ls with - | List_Cons y tl => if y s= x then Return true else list_mem_loop n1 x tl - | List_Nil => Return false + | List_Cons y tl => if y s= x then Ok true else list_mem_loop n1 x tl + | List_Nil => Ok false end end . @@ -162,16 +162,13 @@ Fixpoint list_nth_mut_loop_loop match ls with | List_Cons x tl => if i s= 0%u32 - then - let back := fun (ret : T) => Return (List_Cons ret tl) in - Return (x, back) + then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_loop_loop T n1 tl i1; let (t, back) := p in - let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1) - in - Return (t, back1)) + let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in + Ok (t, back1)) | List_Nil => Fail_ Failure end end @@ -196,7 +193,7 @@ Fixpoint list_nth_shared_loop_loop match ls with | List_Cons x tl => if i s= 0%u32 - then Return x + then Ok x else (i1 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n1 tl i1) | List_Nil => Fail_ Failure end @@ -223,14 +220,13 @@ Fixpoint get_elem_mut_loop | List_Cons y tl => if y s= x then - let back := fun (ret : usize) => Return (List_Cons ret tl) in - Return (y, back) + let back := fun (ret : usize) => Ok (List_Cons ret tl) in Ok (y, back) else ( p <- get_elem_mut_loop n1 x tl; let (i, back) := p in - let back1 := - fun (ret : usize) => tl1 <- back ret; Return (List_Cons y tl1) in - Return (i, back1)) + let back1 := fun (ret : usize) => tl1 <- back ret; Ok (List_Cons y tl1) + in + Ok (i, back1)) | List_Nil => Fail_ Failure end end @@ -249,7 +245,7 @@ Definition get_elem_mut p1 <- get_elem_mut_loop n x ls; let (i, back) := p1 in let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in - Return (i, back1) + Ok (i, back1) . (** [loops::get_elem_shared]: loop 0: @@ -260,8 +256,7 @@ Fixpoint get_elem_shared_loop | O => Fail_ OutOfFuel | S n1 => match ls with - | List_Cons y tl => - if y s= x then Return y else get_elem_shared_loop n1 x tl + | List_Cons y tl => if y s= x then Ok y else get_elem_shared_loop n1 x tl | List_Nil => Fail_ Failure end end @@ -285,14 +280,13 @@ Definition id_mut (T : Type) (ls : List_t T) : result ((List_t T) * (List_t T -> result (List_t T))) := - Return (ls, Return) + Ok (ls, Ok) . (** [loops::id_shared]: Source: 'src/loops.rs', lines 149:0-149:45 *) Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) := - Return ls -. + Ok ls. (** [loops::list_nth_mut_loop_with_id]: loop 0: Source: 'src/loops.rs', lines 154:0-165:1 *) @@ -306,16 +300,13 @@ Fixpoint list_nth_mut_loop_with_id_loop match ls with | List_Cons x tl => if i s= 0%u32 - then - let back := fun (ret : T) => Return (List_Cons ret tl) in - Return (x, back) + then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_loop_with_id_loop T n1 i1 tl; let (t, back) := p in - let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1) - in - Return (t, back1)) + let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in + Ok (t, back1)) | List_Nil => Fail_ Failure end end @@ -332,7 +323,7 @@ Definition list_nth_mut_loop_with_id p1 <- list_nth_mut_loop_with_id_loop T n i ls1; let (t, back) := p1 in let back1 := fun (ret : T) => l <- back ret; id_mut_back l in - Return (t, back1) + Ok (t, back1) . (** [loops::list_nth_shared_loop_with_id]: loop 0: @@ -345,7 +336,7 @@ Fixpoint list_nth_shared_loop_with_id_loop match ls with | List_Cons x tl => if i s= 0%u32 - then Return x + then Ok x else ( i1 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n1 i1 tl) | List_Nil => Fail_ Failure @@ -375,18 +366,18 @@ Fixpoint list_nth_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back'a := fun (ret : T) => Return (List_Cons ret tl0) in - let back'b := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back'a, back'b) + let back'a := fun (ret : T) => Ok (List_Cons ret tl0) in + let back'b := fun (ret : T) => Ok (List_Cons ret tl1) in + Ok ((x0, x1), back'a, back'b) else ( i1 <- u32_sub i 1%u32; t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1; let '(p, back'a, back'b) := t in let back'a1 := - fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in + fun (ret : T) => tl01 <- back'a ret; Ok (List_Cons x0 tl01) in let back'b1 := - fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in - Return (p, back'a1, back'b1)) + fun (ret : T) => tl11 <- back'b ret; Ok (List_Cons x1 tl11) in + Ok (p, back'a1, back'b1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -417,7 +408,7 @@ Fixpoint list_nth_shared_loop_pair_loop match ls1 with | List_Cons x1 tl1 => if i s= 0%u32 - then Return (x0, x1) + then Ok (x0, x1) else ( i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n1 tl0 tl1 i1) | List_Nil => Fail_ Failure @@ -453,9 +444,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop then let back := fun (ret : (T * T)) => - let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1) - in - Return ((x0, x1), back) + let (t, t1) := ret in Ok (List_Cons t tl0, List_Cons t1 tl1) in + Ok ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; @@ -464,8 +454,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop fun (ret : (T * T)) => p2 <- back ret; let (tl01, tl11) := p2 in - Return (List_Cons x0 tl01, List_Cons x1 tl11) in - Return (p1, back1)) + Ok (List_Cons x0 tl01, List_Cons x1 tl11) in + Ok (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -496,7 +486,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop match ls1 with | List_Cons x1 tl1 => if i s= 0%u32 - then Return (x0, x1) + then Ok (x0, x1) else ( i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_merge_loop T n1 tl0 tl1 i1) @@ -531,15 +521,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back) + let back := fun (ret : T) => Ok (List_Cons ret tl0) in + Ok ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1; let (p1, back) := p in let back1 := - fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in - Return (p1, back1)) + fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in + Ok (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -571,15 +561,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back) + let back := fun (ret : T) => Ok (List_Cons ret tl0) in + Ok ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1; let (p1, back) := p in let back1 := - fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in - Return (p1, back1)) + fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in + Ok (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -611,15 +601,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back) + let back := fun (ret : T) => Ok (List_Cons ret tl1) in + Ok ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1; let (p1, back) := p in let back1 := - fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in - Return (p1, back1)) + fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in + Ok (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -651,15 +641,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back) + let back := fun (ret : T) => Ok (List_Cons ret tl1) in + Ok ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; let (p1, back) := p in let back1 := - fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in - Return (p1, back1)) + fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in + Ok (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -684,7 +674,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | S n1 => if i s> 0%u32 then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1) - else Return tt + else Ok tt end . @@ -692,7 +682,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := 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 + _ <- ignore_input_mut_borrow_loop n i; Ok _a . (** [loops::incr_ignore_input_mut_borrow]: loop 0: @@ -703,7 +693,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | S n1 => if i s> 0%u32 then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1) - else Return tt + else Ok tt end . @@ -711,7 +701,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := 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 + a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1 . (** [loops::ignore_input_shared_borrow]: loop 0: @@ -722,7 +712,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := | S n1 => if i s> 0%u32 then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1) - else Return tt + else Ok tt end . @@ -730,7 +720,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := 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 + _ <- ignore_input_shared_borrow_loop n i; Ok _a . End Loops. -- cgit v1.2.3