summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Demo.lean1
-rw-r--r--tests/lean/Demo/Demo.lean148
-rw-r--r--tests/lean/Demo/Properties.lean68
-rw-r--r--tests/lean/lakefile.lean1
4 files changed, 218 insertions, 0 deletions
diff --git a/tests/lean/Demo.lean b/tests/lean/Demo.lean
new file mode 100644
index 00000000..79cd1323
--- /dev/null
+++ b/tests/lean/Demo.lean
@@ -0,0 +1 @@
+import Demo.Properties
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
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
new file mode 100644
index 00000000..cdec7332
--- /dev/null
+++ b/tests/lean/Demo/Properties.lean
@@ -0,0 +1,68 @@
+import Base
+import Demo.Demo
+open Primitives
+open Result
+
+namespace demo
+
+#check U32.add_spec
+
+-- @[pspec]
+theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
+ : ∃ y, mul2_add1 x = ret y ∧
+ ↑y = 2 * ↑x + (1 : Int)
+ := by
+ rw [mul2_add1]
+ progress with U32.add_spec as ⟨ i ⟩
+ progress as ⟨ i' ⟩
+ simp; scalar_tac
+
+theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
+ ∃ z, use_mul2_add1 x y = ret z ∧
+ ↑z = 2 * ↑x + (1 : Int) + ↑y := by
+ rw [use_mul2_add1]
+ progress with mul2_add1_spec as ⟨ i ⟩
+ progress as ⟨ i' ⟩
+ simp; scalar_tac
+
+open CList
+
+@[simp] def CList.to_list {α : Type} (x : CList α) : List α :=
+ match x with
+ | CNil => []
+ | CCons hd tl => hd :: tl.to_list
+
+theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
+ (h : ↑i < l.to_list.len) :
+ ∃ x, list_nth T l i = ret x ∧
+ x = l.to_list.index ↑i
+ := by
+ rw [list_nth]
+ match l with
+ | CNil =>
+ simp_all; scalar_tac
+ | CCons hd tl =>
+ simp_all
+ if hi: i = 0#u32 then
+ simp_all
+ else
+ simp_all
+ progress as ⟨ i1 ⟩
+ progress as ⟨ x ⟩
+ simp_all
+
+theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
+ ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+ rw [i32_id]
+ if hx : x = 0#i32 then
+ simp_all
+ else
+ simp_all
+ progress as ⟨ x1 ⟩
+ progress as ⟨ x2 ⟩
+ progress
+ simp_all
+termination_by x.val.toNat
+decreasing_by scalar_decr_tac
+
+end demo
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index 781fc8b8..3a777824 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -20,3 +20,4 @@ package «tests» {}
@[default_target] lean_lib PoloniusList
@[default_target] lean_lib Arrays
@[default_target] lean_lib Traits
+@[default_target] lean_lib Demo