1 files changed, 138 insertions, 0 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
new file mode 100644
index 00000000..f9082979
--- /dev/null
+++ b/tests/fstar/demo/Demo.fst
@@ -0,0 +1,138 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [demo] *)
+module Demo
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [demo::choose]:
+    Source: 'src/demo.rs', lines 5:0-5:70 *)
+let choose
+  (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
+  if b
+  then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
+  else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+
+(** [demo::mul2_add1]:
+    Source: 'src/demo.rs', lines 13:0-13:31 *)
+let mul2_add1 (x : u32) : result u32 =
+  let* i = u32_add x x in u32_add i 1
+
+(** [demo::use_mul2_add1]:
+    Source: 'src/demo.rs', lines 17:0-17:43 *)
+let use_mul2_add1 (x : u32) (y : u32) : result u32 =
+  let* i = mul2_add1 x in u32_add i y
+
+(** [demo::incr]:
+    Source: 'src/demo.rs', lines 21:0-21:31 *)
+let incr (x : u32) : result u32 =
+  u32_add x 1
+
+(** [demo::CList]
+    Source: 'src/demo.rs', lines 27:0-27:17 *)
+type cList_t (t : Type0) =
+| CList_CCons : t -> cList_t t -> cList_t t
+| CList_CNil : cList_t t
+
+(** [demo::list_nth]:
+    Source: 'src/demo.rs', lines 32:0-32:56 *)
+let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      if i = 0 then Return x else let* i1 = u32_sub i 1 in list_nth t n1 tl i1
+    | CList_CNil -> Fail Failure
+    end
+
+(** [demo::list_nth_mut]:
+    Source: 'src/demo.rs', lines 47:0-47:68 *)
+let rec list_nth_mut
+  (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
+  result (t & (t -> result (cList_t t)))
+  =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      if i = 0
+      then
+        let back_'a = fun ret -> Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else
+        let* i1 = u32_sub i 1 in
+        let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in
+        let back_'a =
+          fun ret ->
+            let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in
+        Return (x1, back_'a)
+    | CList_CNil -> Fail Failure
+    end
+
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'src/demo.rs', lines 62:0-71:1 *)
+let rec list_nth_mut1_loop
+  (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
+  result (t & (t -> result (cList_t t)))
+  =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      if i = 0
+      then
+        let back_'a = fun ret -> Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else
+        let* i1 = u32_sub i 1 in
+        let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in
+        let back_'a1 =
+          fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in
+        Return (x1, back_'a1)
+    | CList_CNil -> Fail Failure
+    end
+
+(** [demo::list_nth_mut1]:
+    Source: 'src/demo.rs', lines 62:0-62:77 *)
+let list_nth_mut1
+  (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
+  result (t & (t -> result (cList_t t)))
+  =
+  let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
+
+(** [demo::i32_id]:
+    Source: 'src/demo.rs', lines 73:0-73:28 *)
+let rec i32_id (n : nat) (i : i32) : result i32 =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    if i = 0
+    then Return 0
+    else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
+
+(** Trait declaration: [demo::Counter]
+    Source: 'src/demo.rs', lines 83:0-83:17 *)
+noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
+
+(** [demo::{usize}::incr]:
+    Source: 'src/demo.rs', lines 88:4-88:31 *)
+let usize_incr (self : usize) : result (usize & usize) =
+  let* self1 = usize_add self 1 in Return (self, self1)
+
+(** Trait implementation: [demo::{usize}]
+    Source: 'src/demo.rs', lines 87:0-87:22 *)
+let demo_CounterUsizeInst : counter_t usize = { incr = usize_incr; }
+
+(** [demo::use_counter]:
+    Source: 'src/demo.rs', lines 95:0-95:59 *)
+let use_counter
+  (t : Type0) (counterTInst : counter_t t) (cnt : t) : result (usize & t) =
+  counterTInst.incr cnt
+