From 304490110509324a20c7c2c3be9bf61931fa3a1c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 17 Dec 2022 10:50:43 +0100
Subject: Make minor modifications and generate code for loops

---
 tests/coq/misc/Loops.v     | 72 ++++++++++++++++++++++++++++++++++++++++++++++
 tests/coq/misc/_CoqProject |  1 +
 2 files changed, 73 insertions(+)
 create mode 100644 tests/coq/misc/Loops.v

(limited to 'tests/coq')

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
new file mode 100644
index 00000000..48de76c2
--- /dev/null
+++ b/tests/coq/misc/Loops.v
@@ -0,0 +1,72 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Loops.
+
+(** [loops::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _.
+Arguments ListNil {T}.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_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;
+        t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
+        Return t)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
+.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_back
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return (ListCons ret tl)
+      else (
+        i0 <- u32_sub i 1%u32;
+        l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret;
+        Return (ListCons x l))
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_back
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
+.
+
+End Loops .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index c9ee0ff6..db6c2742 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
 -arg -w
 -arg all
 
+Loops.v
 Primitives.v
 External_Funs.v
 Constants.v
-- 
cgit v1.2.3