From 49117ba254679f98938223711810191c3f7d788f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 27 Oct 2023 13:34:03 +0200 Subject: Regenerate the Coq test files --- tests/coq/misc/Loops.v | 412 +++++++++++++++++++++++++------------------------ 1 file changed, 212 insertions(+), 200 deletions(-) (limited to 'tests/coq/misc/Loops.v') diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 82e57576..180a1d68 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -9,23 +9,23 @@ Local Open Scope Primitives_scope. Module Loops. (** [loops::sum]: loop 0: forward function *) -Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := +Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n0 => if i s< max - then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop_fwd n0 max i0 s0) + then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop n0 max i0 s0) else u32_mul s 2%u32 end . (** [loops::sum]: forward function *) -Definition sum_fwd (n : nat) (max : u32) : result u32 := - sum_loop_fwd n max 0%u32 0%u32 +Definition sum (n : nat) (max : u32) : result u32 := + sum_loop n max 0%u32 0%u32 . (** [loops::sum_with_mut_borrows]: loop 0: forward function *) -Fixpoint sum_with_mut_borrows_loop_fwd +Fixpoint sum_with_mut_borrows_loop (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := match n with | O => Fail_ OutOfFuel @@ -34,18 +34,18 @@ Fixpoint sum_with_mut_borrows_loop_fwd then ( ms0 <- u32_add ms mi; mi0 <- u32_add mi 1%u32; - sum_with_mut_borrows_loop_fwd n0 max mi0 ms0) + sum_with_mut_borrows_loop n0 max mi0 ms0) else u32_mul ms 2%u32 end . (** [loops::sum_with_mut_borrows]: forward function *) -Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_mut_borrows_loop_fwd n max 0%u32 0%u32 +Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 := + sum_with_mut_borrows_loop n max 0%u32 0%u32 . (** [loops::sum_with_shared_borrows]: loop 0: forward function *) -Fixpoint sum_with_shared_borrows_loop_fwd +Fixpoint sum_with_shared_borrows_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel @@ -54,87 +54,88 @@ Fixpoint sum_with_shared_borrows_loop_fwd then ( i0 <- u32_add i 1%u32; s0 <- u32_add s i0; - sum_with_shared_borrows_loop_fwd n0 max i0 s0) + sum_with_shared_borrows_loop n0 max i0 s0) else u32_mul s 2%u32 end . (** [loops::sum_with_shared_borrows]: forward function *) -Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_shared_borrows_loop_fwd n max 0%u32 0%u32 +Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 := + sum_with_shared_borrows_loop n max 0%u32 0%u32 . (** [loops::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -Fixpoint clear_loop_fwd_back - (n : nat) (v : vec u32) (i : usize) : result (vec u32) := +Fixpoint clear_loop + (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len u32 v in + let i0 := alloc_vec_Vec_len u32 v in if i s< i0 then ( i1 <- usize_add i 1%usize; - v0 <- vec_index_mut_back u32 v i 0%u32; - clear_loop_fwd_back n0 v0 i1) + v0 <- + alloc_vec_Vec_index_mut_back u32 usize + (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0%u32; + clear_loop n0 v0 i1) else Return v end . (** [loops::clear]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) := - clear_loop_fwd_back n v 0%usize +Definition clear + (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) := + clear_loop n v 0%usize . (** [loops::List] *) Inductive List_t (T : Type) := -| ListCons : T -> List_t T -> List_t T -| ListNil : List_t T +| List_Cons : T -> List_t T -> List_t T +| List_Nil : List_t T . -Arguments ListCons {T} _ _. -Arguments ListNil {T}. +Arguments List_Cons {T} _ _. +Arguments List_Nil {T}. (** [loops::list_mem]: loop 0: forward function *) -Fixpoint list_mem_loop_fwd - (n : nat) (x : u32) (ls : List_t u32) : result bool := +Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons y tl => - if y s= x then Return true else list_mem_loop_fwd n0 x tl - | ListNil => Return false + | List_Cons y tl => if y s= x then Return true else list_mem_loop n0 x tl + | List_Nil => Return false end end . (** [loops::list_mem]: forward function *) -Definition list_mem_fwd (n : nat) (x : u32) (ls : List_t u32) : result bool := - list_mem_loop_fwd n x ls +Definition list_mem (n : nat) (x : u32) (ls : List_t u32) : result bool := + list_mem_loop n x ls . (** [loops::list_nth_mut_loop]: loop 0: forward function *) -Fixpoint list_nth_mut_loop_loop_fwd +Fixpoint list_nth_mut_loop_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop_fwd T n0 tl i0) - | ListNil => Fail_ Failure + else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop T n0 tl i0) + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_loop]: forward function *) -Definition list_nth_mut_loop_fwd +Definition list_nth_mut_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - list_nth_mut_loop_loop_fwd T n ls i + list_nth_mut_loop_loop T n ls i . (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) @@ -146,14 +147,14 @@ Fixpoint list_nth_mut_loop_loop_back | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 - then Return (ListCons ret tl) + then Return (List_Cons ret tl) else ( i0 <- u32_sub i 1%u32; tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret; - Return (ListCons x tl0)) - | ListNil => Fail_ Failure + Return (List_Cons x tl0)) + | List_Nil => Fail_ Failure end end . @@ -167,46 +168,50 @@ Definition list_nth_mut_loop_back . (** [loops::list_nth_shared_loop]: loop 0: forward function *) -Fixpoint list_nth_shared_loop_loop_fwd +Fixpoint list_nth_shared_loop_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop_fwd T n0 tl i0) - | ListNil => Fail_ Failure + else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n0 tl i0) + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_loop]: forward function *) -Definition list_nth_shared_loop_fwd +Definition list_nth_shared_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - list_nth_shared_loop_loop_fwd T n ls i + list_nth_shared_loop_loop T n ls i . (** [loops::get_elem_mut]: loop 0: forward function *) -Fixpoint get_elem_mut_loop_fwd +Fixpoint get_elem_mut_loop (n : nat) (x : usize) (ls : List_t usize) : result usize := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons y tl => - if y s= x then Return y else get_elem_mut_loop_fwd n0 x tl - | ListNil => Fail_ Failure + | List_Cons y tl => if y s= x then Return y else get_elem_mut_loop n0 x tl + | List_Nil => Fail_ Failure end end . (** [loops::get_elem_mut]: forward function *) -Definition get_elem_mut_fwd - (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_mut_fwd (List_t usize) slots 0%usize; - get_elem_mut_loop_fwd n x l +Definition get_elem_mut + (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : + result usize + := + l <- + alloc_vec_Vec_index_mut (List_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) + slots 0%usize; + get_elem_mut_loop n x l . (** [loops::get_elem_mut]: loop 0: backward function 0 *) @@ -218,50 +223,60 @@ Fixpoint get_elem_mut_loop_back | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons y tl => + | List_Cons y tl => if y s= x - then Return (ListCons ret tl) - else (tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y tl0)) - | ListNil => Fail_ Failure + then Return (List_Cons ret tl) + else ( + tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (List_Cons y tl0)) + | List_Nil => Fail_ Failure end end . (** [loops::get_elem_mut]: backward function 0 *) Definition get_elem_mut_back - (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) : - result (vec (List_t usize)) + (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) (ret : usize) : + result (alloc_vec_Vec (List_t usize)) := - l <- vec_index_mut_fwd (List_t usize) slots 0%usize; + l <- + alloc_vec_Vec_index_mut (List_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) + slots 0%usize; l0 <- get_elem_mut_loop_back n x l ret; - vec_index_mut_back (List_t usize) slots 0%usize l0 + alloc_vec_Vec_index_mut_back (List_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) slots + 0%usize l0 . (** [loops::get_elem_shared]: loop 0: forward function *) -Fixpoint get_elem_shared_loop_fwd +Fixpoint get_elem_shared_loop (n : nat) (x : usize) (ls : List_t usize) : result usize := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons y tl => - if y s= x then Return y else get_elem_shared_loop_fwd n0 x tl - | ListNil => Fail_ Failure + | List_Cons y tl => + if y s= x then Return y else get_elem_shared_loop n0 x tl + | List_Nil => Fail_ Failure end end . (** [loops::get_elem_shared]: forward function *) -Definition get_elem_shared_fwd - (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_fwd (List_t usize) slots 0%usize; - get_elem_shared_loop_fwd n x l +Definition get_elem_shared + (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : + result usize + := + l <- + alloc_vec_Vec_index (List_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (List_t usize)) + slots 0%usize; + get_elem_shared_loop n x l . (** [loops::id_mut]: forward function *) -Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) := - Return ls -. +Definition id_mut (T : Type) (ls : List_t T) : result (List_t T) := + Return ls. (** [loops::id_mut]: backward function 0 *) Definition id_mut_back @@ -270,31 +285,30 @@ Definition id_mut_back . (** [loops::id_shared]: forward function *) -Definition id_shared_fwd (T : Type) (ls : List_t T) : result (List_t T) := +Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) := Return ls . (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) -Fixpoint list_nth_mut_loop_with_id_loop_fwd +Fixpoint list_nth_mut_loop_with_id_loop (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 then Return x - else ( - i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop_fwd T n0 i0 tl) - | ListNil => Fail_ Failure + else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop T n0 i0 tl) + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_loop_with_id]: forward function *) -Definition list_nth_mut_loop_with_id_fwd +Definition list_nth_mut_loop_with_id (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - ls0 <- id_mut_fwd T ls; list_nth_mut_loop_with_id_loop_fwd T n i ls0 + ls0 <- id_mut T ls; list_nth_mut_loop_with_id_loop T n i ls0 . (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) @@ -306,14 +320,14 @@ Fixpoint list_nth_mut_loop_with_id_loop_back | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 - then Return (ListCons ret tl) + then Return (List_Cons ret tl) else ( i0 <- u32_sub i 1%u32; tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret; - Return (ListCons x tl0)) - | ListNil => Fail_ Failure + Return (List_Cons x tl0)) + | List_Nil => Fail_ Failure end end . @@ -323,36 +337,36 @@ Definition list_nth_mut_loop_with_id_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) := - ls0 <- id_mut_fwd T ls; + ls0 <- id_mut T ls; l <- list_nth_mut_loop_with_id_loop_back T n i ls0 ret; id_mut_back T ls l . (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) -Fixpoint list_nth_shared_loop_with_id_loop_fwd +Fixpoint list_nth_shared_loop_with_id_loop (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons x tl => + | List_Cons x tl => if i s= 0%u32 then Return x else ( - i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop_fwd T n0 i0 tl) - | ListNil => Fail_ Failure + i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n0 i0 tl) + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_loop_with_id]: forward function *) -Definition list_nth_shared_loop_with_id_fwd +Definition list_nth_shared_loop_with_id (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n i ls0 + ls0 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls0 . (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) -Fixpoint list_nth_mut_loop_pair_loop_fwd +Fixpoint list_nth_mut_loop_pair_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -360,27 +374,26 @@ Fixpoint list_nth_mut_loop_pair_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( - i0 <- u32_sub i 1%u32; - list_nth_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + i0 <- u32_sub i 1%u32; list_nth_mut_loop_pair_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_loop_pair]: forward function *) -Definition list_nth_mut_loop_pair_fwd +Definition list_nth_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_mut_loop_pair_loop_fwd T n ls0 ls1 i + list_nth_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) @@ -392,18 +405,18 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else ( i0 <- u32_sub i 1%u32; tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; - Return (ListCons x0 tl00)) - | ListNil => Fail_ Failure + Return (List_Cons x0 tl00)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -425,18 +438,18 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else ( i0 <- u32_sub i 1%u32; tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; - Return (ListCons x1 tl10)) - | ListNil => Fail_ Failure + Return (List_Cons x1 tl10)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -450,7 +463,7 @@ Definition list_nth_mut_loop_pair_back'b . (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) -Fixpoint list_nth_shared_loop_pair_loop_fwd +Fixpoint list_nth_shared_loop_pair_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -458,31 +471,30 @@ Fixpoint list_nth_shared_loop_pair_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( - i0 <- u32_sub i 1%u32; - list_nth_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + i0 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_loop_pair]: forward function *) -Definition list_nth_shared_loop_pair_fwd +Definition list_nth_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i + list_nth_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) -Fixpoint list_nth_mut_loop_pair_merge_loop_fwd +Fixpoint list_nth_mut_loop_pair_merge_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -490,27 +502,27 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_mut_loop_pair_merge_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_loop_pair_merge]: forward function *) -Definition list_nth_mut_loop_pair_merge_fwd +Definition list_nth_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i + list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) @@ -523,19 +535,19 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1) + then let (t, t0) := ret in Return (List_Cons t tl0, List_Cons t0 tl1) else ( i0 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; let (tl00, tl10) := p in - Return (ListCons x0 tl00, ListCons x1 tl10)) - | ListNil => Fail_ Failure + Return (List_Cons x0 tl00, List_Cons x1 tl10)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -550,7 +562,7 @@ Definition list_nth_mut_loop_pair_merge_back . (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) -Fixpoint list_nth_shared_loop_pair_merge_loop_fwd +Fixpoint list_nth_shared_loop_pair_merge_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -558,31 +570,31 @@ Fixpoint list_nth_shared_loop_pair_merge_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_shared_loop_pair_merge_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_loop_pair_merge]: forward function *) -Definition list_nth_shared_loop_pair_merge_fwd +Definition list_nth_shared_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i + list_nth_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) -Fixpoint list_nth_mut_shared_loop_pair_loop_fwd +Fixpoint list_nth_mut_shared_loop_pair_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -590,27 +602,27 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_mut_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_mut_shared_loop_pair_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_shared_loop_pair]: forward function *) -Definition list_nth_mut_shared_loop_pair_fwd +Definition list_nth_mut_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i + list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) @@ -622,18 +634,18 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else ( i0 <- u32_sub i 1%u32; tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 tl00)) - | ListNil => Fail_ Failure + Return (List_Cons x0 tl00)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -647,7 +659,7 @@ Definition list_nth_mut_shared_loop_pair_back . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) -Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd +Fixpoint list_nth_mut_shared_loop_pair_merge_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -655,27 +667,27 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_mut_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_mut_shared_loop_pair_merge_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) -Definition list_nth_mut_shared_loop_pair_merge_fwd +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) := - list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i + list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) @@ -687,19 +699,19 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else ( i0 <- u32_sub i 1%u32; tl00 <- list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 tl00)) - | ListNil => Fail_ Failure + Return (List_Cons x0 tl00)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -713,7 +725,7 @@ Definition list_nth_mut_shared_loop_pair_merge_back . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) -Fixpoint list_nth_shared_mut_loop_pair_loop_fwd +Fixpoint list_nth_shared_mut_loop_pair_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -721,27 +733,27 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_shared_mut_loop_pair_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_mut_loop_pair]: forward function *) -Definition list_nth_shared_mut_loop_pair_fwd +Definition list_nth_shared_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := - list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i + list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) @@ -753,18 +765,18 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else ( i0 <- u32_sub i 1%u32; tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 tl10)) - | ListNil => Fail_ Failure + Return (List_Cons x1 tl10)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . @@ -778,7 +790,7 @@ Definition list_nth_shared_mut_loop_pair_back . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) -Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd +Fixpoint list_nth_shared_mut_loop_pair_merge_loop (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := @@ -786,27 +798,27 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 then Return (x0, x1) else ( i0 <- u32_sub i 1%u32; - list_nth_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) - | ListNil => Fail_ Failure + list_nth_shared_mut_loop_pair_merge_loop T n0 tl0 tl1 i0) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) -Definition list_nth_shared_mut_loop_pair_merge_fwd +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) := - list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i + list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) @@ -818,19 +830,19 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back | O => Fail_ OutOfFuel | S n0 => match ls0 with - | ListCons x0 tl0 => + | List_Cons x0 tl0 => match ls1 with - | ListCons x1 tl1 => + | List_Cons x1 tl1 => if i s= 0%u32 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else ( i0 <- u32_sub i 1%u32; tl10 <- list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 tl10)) - | ListNil => Fail_ Failure + Return (List_Cons x1 tl10)) + | List_Nil => Fail_ Failure end - | ListNil => Fail_ Failure + | List_Nil => Fail_ Failure end end . -- cgit v1.2.3