diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/Loops.v | 186 |
1 files changed, 186 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 8d552b5b..67ee0880 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -22,6 +22,26 @@ Definition sum_fwd (n : nat) (max : u32) : result u32 := sum_loop_fwd n max (0%u32) (0%u32) . +(** [loops::sum_with_borrows] *) +Fixpoint sum_with_borrows_loop_fwd + (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + if mi s< max + then ( + ms0 <- u32_add ms mi; + mi0 <- u32_add mi 1%u32; + sum_with_borrows_loop_fwd n0 max mi0 ms0) + else u32_mul ms 2%u32 + end +. + +(** [loops::sum_with_borrows] *) +Definition sum_with_borrows_fwd (n : nat) (max : u32) : result u32 := + sum_with_borrows_loop_fwd n max (0%u32) (0%u32) +. + (** [loops::List] *) Inductive List_t (T : Type) := | ListCons : T -> List_t T -> List_t T @@ -82,4 +102,170 @@ Definition list_nth_mut_loop_back list_nth_mut_loop_loop_back T n ls i ret . +(** [loops::list_nth_mut_loop_pair] *) +Fixpoint list_nth_mut_loop_pair_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons 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 + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_loop_pair] *) +Definition list_nth_mut_loop_pair_fwd + (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 +. + +(** [loops::list_nth_mut_loop_pair] *) +Fixpoint list_nth_mut_loop_pair_loop_back'a + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl0) + else ( + i0 <- u32_sub i 1%u32; + l1 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; + Return (ListCons x0 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_loop_pair] *) +Definition list_nth_mut_loop_pair_back'a + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_mut_loop_pair_loop_back'a T n ls0 ls1 i ret +. + +(** [loops::list_nth_mut_loop_pair] *) +Fixpoint list_nth_mut_loop_pair_loop_back'b + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl1) + else ( + i0 <- u32_sub i 1%u32; + l1 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; + Return (ListCons x1 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_loop_pair] *) +Definition list_nth_mut_loop_pair_back'b + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret +. + +(** [loops::list_nth_mut_loop_pair_merge] *) +Fixpoint list_nth_mut_loop_pair_merge_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons 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 + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_loop_pair_merge] *) +Definition list_nth_mut_loop_pair_merge_fwd + (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 +. + +(** [loops::list_nth_mut_loop_pair_merge] *) +Fixpoint list_nth_mut_loop_pair_merge_loop_back + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : (T * T)) + : + result ((List_t T) * (List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then let (t, t0) := ret in Return (ListCons t tl0, ListCons 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 (l1, l2) := p in + Return (ListCons x0 l1, ListCons x1 l2)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_loop_pair_merge] *) +Definition list_nth_mut_loop_pair_merge_back + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) + (ret : (T * T)) : + result ((List_t T) * (List_t T)) + := + list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret +. + End Loops . |