Merge pull request #73 from AeneasVerif/son/demo

Add some demo files

1 files changed, 148 insertions, 0 deletions

diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
new file mode 100644
index 00000000..01818585
--- /dev/null
+++ b/tests/lean/Demo/Demo.lean
@@ -0,0 +1,148 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [demo]
+import Base
+open Primitives
+
+namespace demo
+
+/- [demo::choose]:
+   Source: 'src/demo.rs', lines 5:0-5:70 -/
+def choose
+  (T : Type) (b : Bool) (x : T) (y : T) :
+  Result (T × (T → Result (T × T)))
+  :=
+  if b
+  then let back_'a := fun ret => Result.ret (ret, y)
+       Result.ret (x, back_'a)
+  else let back_'a := fun ret => Result.ret (x, ret)
+       Result.ret (y, back_'a)
+
+/- [demo::mul2_add1]:
+   Source: 'src/demo.rs', lines 13:0-13:31 -/
+def mul2_add1 (x : U32) : Result U32 :=
+  do
+  let i ← x + x
+  i + 1#u32
+
+/- [demo::use_mul2_add1]:
+   Source: 'src/demo.rs', lines 17:0-17:43 -/
+def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
+  do
+  let i ← mul2_add1 x
+  i + y
+
+/- [demo::incr]:
+   Source: 'src/demo.rs', lines 21:0-21:31 -/
+def incr (x : U32) : Result U32 :=
+  x + 1#u32
+
+/- [demo::CList]
+   Source: 'src/demo.rs', lines 27:0-27:17 -/
+inductive CList (T : Type) :=
+| CCons : T → CList T → CList T
+| CNil : CList T
+
+/- [demo::list_nth]:
+   Source: 'src/demo.rs', lines 32:0-32:56 -/
+divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
+  match l with
+  | CList.CCons x tl =>
+    if i = 0#u32
+    then Result.ret x
+    else do
+         let i1 ← i - 1#u32
+         list_nth T tl i1
+  | CList.CNil => Result.fail .panic
+
+/- [demo::list_nth_mut]:
+   Source: 'src/demo.rs', lines 47:0-47:68 -/
+divergent def list_nth_mut
+  (T : Type) (l : CList T) (i : U32) :
+  Result (T × (T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons x tl =>
+    if i = 0#u32
+    then
+      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
+      Result.ret (x, back_'a)
+    else
+      do
+      let i1 ← i - 1#u32
+      let (t, list_nth_mut_back) ← list_nth_mut T tl i1
+      let back_'a :=
+        fun ret =>
+          do
+          let tl1 ← list_nth_mut_back ret
+          Result.ret (CList.CCons x tl1)
+      Result.ret (t, back_'a)
+  | CList.CNil => Result.fail .panic
+
+/- [demo::list_nth_mut1]: loop 0:
+   Source: 'src/demo.rs', lines 62:0-71:1 -/
+divergent def list_nth_mut1_loop
+  (T : Type) (l : CList T) (i : U32) :
+  Result (T × (T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons x tl =>
+    if i = 0#u32
+    then
+      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
+      Result.ret (x, back_'a)
+    else
+      do
+      let i1 ← i - 1#u32
+      let (t, back_'a) ← list_nth_mut1_loop T tl i1
+      let back_'a1 :=
+        fun ret => do
+                   let tl1 ← back_'a ret
+                   Result.ret (CList.CCons x tl1)
+      Result.ret (t, back_'a1)
+  | CList.CNil => Result.fail .panic
+
+/- [demo::list_nth_mut1]:
+   Source: 'src/demo.rs', lines 62:0-62:77 -/
+def list_nth_mut1
+  (T : Type) (l : CList T) (i : U32) :
+  Result (T × (T → Result (CList T)))
+  :=
+  do
+  let (t, back_'a) ← list_nth_mut1_loop T l i
+  Result.ret (t, back_'a)
+
+/- [demo::i32_id]:
+   Source: 'src/demo.rs', lines 73:0-73:28 -/
+divergent def i32_id (i : I32) : Result I32 :=
+  if i = 0#i32
+  then Result.ret 0#i32
+  else do
+       let i1 ← i - 1#i32
+       let i2 ← i32_id i1
+       i2 + 1#i32
+
+/- Trait declaration: [demo::Counter]
+   Source: 'src/demo.rs', lines 83:0-83:17 -/
+structure Counter (Self : Type) where
+  incr : Self → Result (Usize × Self)
+
+/- [demo::{usize}::incr]:
+   Source: 'src/demo.rs', lines 88:4-88:31 -/
+def Usize.incr (self : Usize) : Result (Usize × Usize) :=
+  do
+  let self1 ← self + 1#usize
+  Result.ret (self, self1)
+
+/- Trait implementation: [demo::{usize}]
+   Source: 'src/demo.rs', lines 87:0-87:22 -/
+def demo.CounterUsizeInst : Counter Usize := {
+  incr := Usize.incr
+}
+
+/- [demo::use_counter]:
+   Source: 'src/demo.rs', lines 95:0-95:59 -/
+def use_counter
+  (T : Type) (CounterTInst : Counter T) (cnt : T) : Result (Usize × T) :=
+  CounterTInst.incr cnt
+
+end demo