From 42fe6fb304b322b2bfabab243964375520f46973 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 9 Feb 2024 15:24:57 +0100
Subject: Add some demo files

---
 tests/coq/demo/Demo.v | 167 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 167 insertions(+)
 create mode 100644 tests/coq/demo/Demo.v

(limited to 'tests/coq/demo/Demo.v')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
new file mode 100644
index 00000000..1abe7c5c
--- /dev/null
+++ b/tests/coq/demo/Demo.v
@@ -0,0 +1,167 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [demo] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Demo.
+
+(** [demo::choose]:
+    Source: 'src/demo.rs', lines 5:0-5:70 *)
+Definition choose
+  (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
+  if b
+  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
+  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+.
+
+(** [demo::mul2_add1]:
+    Source: 'src/demo.rs', lines 13:0-13:31 *)
+Definition mul2_add1 (x : u32) : result u32 :=
+  i <- u32_add x x; u32_add i 1%u32
+.
+
+(** [demo::use_mul2_add1]:
+    Source: 'src/demo.rs', lines 17:0-17:43 *)
+Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
+  i <- mul2_add1 x; u32_add i y
+.
+
+(** [demo::incr]:
+    Source: 'src/demo.rs', lines 21:0-21:31 *)
+Definition incr (x : u32) : result u32 :=
+  u32_add x 1%u32.
+
+(** [demo::CList]
+    Source: 'src/demo.rs', lines 27:0-27:17 *)
+Inductive CList_t (T : Type) :=
+| CList_CCons : T -> CList_t T -> CList_t T
+| CList_CNil : CList_t T
+.
+
+Arguments CList_CCons { _ }.
+Arguments CList_CNil { _ }.
+
+(** [demo::list_nth]:
+    Source: 'src/demo.rs', lines 32:0-32:56 *)
+Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut]:
+    Source: 'src/demo.rs', lines 47:0-47:68 *)
+Fixpoint list_nth_mut
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then
+        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut T n1 tl i1;
+        let (t, list_nth_mut_back) := p in
+        let back_'a :=
+          fun (ret : T) =>
+            tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
+        Return (t, back_'a))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'src/demo.rs', lines 62:0-71:1 *)
+Fixpoint list_nth_mut1_loop
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then
+        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut1_loop T n1 tl i1;
+        let (t, back_'a) := p in
+        let back_'a1 :=
+          fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in
+        Return (t, back_'a1))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut1]:
+    Source: 'src/demo.rs', lines 62:0-62:77 *)
+Definition list_nth_mut1
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+.
+
+(** [demo::i32_id]:
+    Source: 'src/demo.rs', lines 73:0-73:28 *)
+Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s= 0%i32
+    then Return 0%i32
+    else (i1 <- i32_sub i 1%i32; i2 <- i32_id n1 i1; i32_add i2 1%i32)
+  end
+.
+
+(** Trait declaration: [demo::Counter]
+    Source: 'src/demo.rs', lines 83:0-83:17 *)
+Record Counter_t (Self : Type) := mkCounter_t {
+  Counter_t_incr : Self -> result (usize * Self);
+}.
+
+Arguments mkCounter_t { _ }.
+Arguments Counter_t_incr { _ }.
+
+(** [demo::{usize}::incr]:
+    Source: 'src/demo.rs', lines 88:4-88:31 *)
+Definition usize_incr (self : usize) : result (usize * usize) :=
+  self1 <- usize_add self 1%usize; Return (self, self1)
+.
+
+(** Trait implementation: [demo::{usize}]
+    Source: 'src/demo.rs', lines 87:0-87:22 *)
+Definition demo_CounterUsizeInst : Counter_t usize := {|
+  Counter_t_incr := usize_incr;
+|}.
+
+(** [demo::use_counter]:
+    Source: 'src/demo.rs', lines 95:0-95:59 *)
+Definition use_counter
+  (T : Type) (counterTInst : Counter_t T) (cnt : T) : result (usize * T) :=
+  counterTInst.(Counter_t_incr) cnt
+.
+
+End Demo.
-- 
cgit v1.2.3