summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Loops.v380
1 files changed, 374 insertions, 6 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 67ee0880..4fc68e1c 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -22,8 +22,8 @@ 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
+(** [loops::sum_with_mut_borrows] *)
+Fixpoint sum_with_mut_borrows_loop_fwd
(n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
match n with
| O => Fail_ OutOfFuel
@@ -32,14 +32,34 @@ Fixpoint sum_with_borrows_loop_fwd
then (
ms0 <- u32_add ms mi;
mi0 <- u32_add mi 1%u32;
- sum_with_borrows_loop_fwd n0 max mi0 ms0)
+ sum_with_mut_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::sum_with_mut_borrows] *)
+Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 :=
+ sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32)
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Fixpoint sum_with_shared_borrows_loop_fwd
+ (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if i s< max
+ then (
+ i0 <- u32_add i 1%u32;
+ s0 <- u32_add s i0;
+ sum_with_shared_borrows_loop_fwd n0 max i0 s0)
+ else u32_mul s 2%u32
+ end
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
+ sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32)
.
(** [loops::List] *)
@@ -102,6 +122,28 @@ Definition list_nth_mut_loop_back
list_nth_mut_loop_loop_back T n ls i ret
.
+(** [loops::list_nth_shared_loop] *)
+Fixpoint list_nth_shared_loop_loop_fwd
+ (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 =>
+ 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
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop] *)
+Definition list_nth_shared_loop_fwd
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+ list_nth_shared_loop_loop_fwd T n ls i
+.
+
(** [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) :
@@ -200,6 +242,38 @@ Definition list_nth_mut_loop_pair_back'b
list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
.
+(** [loops::list_nth_shared_loop_pair] *)
+Fixpoint list_nth_shared_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_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop_pair] *)
+Definition list_nth_shared_loop_pair_fwd
+ (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
+.
+
(** [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) :
@@ -268,4 +342,298 @@ Definition list_nth_mut_loop_pair_merge_back
list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
.
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Fixpoint list_nth_shared_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_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Definition list_nth_shared_loop_pair_merge_fwd
+ (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
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_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_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_fwd
+ (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
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_loop_pair_loop_back
+ (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_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_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_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_fwd
+ (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
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
+ (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_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_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_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_fwd
+ (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
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_mut_loop_pair_loop_back
+ (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_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_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_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_fwd
+ (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
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
+ (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_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
End Loops .
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:11:31 +0000