summaryrefslogtreecommitdiff
path: root/tests/lean/Traits
diff options
context:
space:
mode:
authorSon Ho2023-11-06 18:49:27 +0100
committerSon Ho2023-11-06 18:49:27 +0100
commitc8fce0c24f2f5331f2f1135cc17d45192f2b30e3 (patch)
tree40ce27098cba71a3f24fea32561f8713ca3dcfc1 /tests/lean/Traits
parent16c094457d0b23f5a9e1ea60e3195cc452ed7c43 (diff)
Regenerate part of the trait tests for Lean
Diffstat (limited to 'tests/lean/Traits')
-rw-r--r--tests/lean/Traits/Funs.lean35
-rw-r--r--tests/lean/Traits/Types.lean46
2 files changed, 65 insertions, 16 deletions
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
index 52ff0c0a..156ef1e0 100644
--- a/tests/lean/Traits/Funs.lean
+++ b/tests/lean/Traits/Funs.lean
@@ -31,8 +31,8 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
/- [traits::Option::{1}::get_bool]: forward function -/
def Option.get_bool (T : Type) (self : Option T) : Result Bool :=
match self with
- | Option.none => Result.ret false
- | Option.some t => Result.ret true
+ | none => Result.ret false
+ | some t => Result.ret true
/- Trait implementation: [traits::Option::{1}] -/
def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := {
@@ -105,7 +105,7 @@ def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 :=
/- [traits::u64::{5}::to_type]: forward function -/
def u64.to_type (self : U64) : Result Bool :=
- Result.ret (self > (U64.ofInt 0))
+ Result.ret (self > 0#u64)
/- Trait implementation: [traits::u64::{5}] -/
def u64.ToTypeInst : ToType U64 Bool := {
@@ -129,7 +129,7 @@ def h4
/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/
def TestType.test.TestType1.test
(self : TestType.test.TestType1) : Result Bool :=
- Result.ret (self._0 > (U64.ofInt 1))
+ Result.ret (self._0 > 1#u64)
/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/
def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait
@@ -142,8 +142,8 @@ def TestType.test
(T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
do
let x0 ← inst.to_u64 x
- if x0 > (U64.ofInt 0)
- then TestType.test.TestType1.test { _0 := (U64.ofInt 0) }
+ if x0 > 0#u64
+ then TestType.test.TestType1.test { _0 := 0#u64 }
else Result.ret false
/- [traits::BoolWrapper::{7}::to_type]: forward function -/
@@ -158,21 +158,21 @@ def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType
}
/- [traits::WithConstTy::LEN2] -/
-def with_const_ty_len2_body : Result Usize := Result.ret (Usize.ofInt 32)
+def with_const_ty_len2_body : Result Usize := Result.ret 32#usize
def with_const_ty_len2_c : Usize :=
eval_global with_const_ty_len2_body (by simp)
/- [traits::Bool::{8}::LEN1] -/
-def bool_len1_body : Result Usize := Result.ret (Usize.ofInt 12)
+def bool_len1_body : Result Usize := Result.ret 12#usize
def bool_len1_c : Usize := eval_global bool_len1_body (by simp)
/- [traits::Bool::{8}::f]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
-def Bool.f (i : U64) (a : Array U8 (Usize.ofInt 32)) : Result U64 :=
+def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
Result.ret i
/- Trait implementation: [traits::Bool::{8}] -/
-def Bool.WithConstTyInst : WithConstTy Bool (Usize.ofInt 32) := {
+def Bool.WithConstTyInst : WithConstTy Bool 32#usize := {
LEN1 := bool_len1_c
LEN2 := with_const_ty_len2_c
V := U8
@@ -207,9 +207,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit :=
/- [traits::test_where2]: forward function -/
def test_where2
- (T : Type) (inst : WithConstTy T (Usize.ofInt 32)) (_x : U32) :
- Result Unit
- :=
+ (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit :=
Result.ret ()
/- [traits::test_child_trait1]: forward function -/
@@ -229,4 +227,15 @@ def order1
:=
Result.ret ()
+/- [traits::map_option]: forward function -/
+def map_option
+ (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
+ Result (Option T)
+ :=
+ match x with
+ | none => Result.ret none
+ | some x0 => do
+ let t ← inst.call f0 x0
+ Result.ret (some t)
+
end traits
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
index a8c12fe5..e325da6f 100644
--- a/tests/lean/Traits/Types.lean
+++ b/tests/lean/Traits/Types.lean
@@ -27,7 +27,7 @@ structure OfType (Self : Type) where
/- Trait declaration: [traits::OfTypeBis] -/
structure OfTypeBis (Self T : Type) where
- parent_clause_0 :ToType T Self
+ parent_clause_0 : ToType T Self
of_type : T → Result Self
/- [traits::TestType] -/
@@ -69,8 +69,8 @@ structure ParentTrait1 (Self : Type) where
/- Trait declaration: [traits::ChildTrait] -/
structure ChildTrait (Self : Type) where
- parent_clause_0 :ParentTrait0 Self
- parent_clause_1 :ParentTrait1 Self
+ parent_clause_0 : ParentTrait0 Self
+ parent_clause_1 : ParentTrait1 Self
/- Trait declaration: [traits::Iterator] -/
structure Iterator (Self : Type) where
@@ -83,4 +83,44 @@ structure IntoIterator (Self : Type) where
IntoIter_clause_0 : Iterator IntoIter
into_iter : Self → Result IntoIter
+/- Trait declaration: [traits::FromResidual] -/
+structure FromResidual (Self T : Type) where
+
+/- Trait declaration: [traits::Try] -/
+structure Try (Self : Type) where
+ parent_clause_0 : FromResidual Self Residual
+ Residual : Type
+
+/- Trait declaration: [traits::CFnOnce] -/
+structure CFnOnce (Self Args : Type) where
+ Output : Type
+ call_once : Self → Args → Result Output
+
+/- Trait declaration: [traits::CFnMut] -/
+structure CFnMut (Self Args : Type) where
+ parent_clause_0 : CFnOnce Self Args
+ call_mut : Self → Args → Result parent_clause_0.Output
+ call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [traits::CFn] -/
+structure CFn (Self Args : Type) where
+ parent_clause_0 : CFnMut Self Args
+ call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
+/- Trait declaration: [core::ops::function::FnOnce] -/
+structure core.ops.function.FnOnce (Self Args : Type) where
+ Output : Type
+ call_once : Self → Args → Result Output
+
+/- Trait declaration: [core::ops::function::FnMut] -/
+structure core.ops.function.FnMut (Self Args : Type) where
+ parent_clause_0 : core.ops.function.FnOnce Self Args
+ call_mut : Self → Args → Result parent_clause_0.Output
+ call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [core::ops::function::Fn] -/
+structure core.ops.function.Fn (Self Args : Type) where
+ parent_clause_0 : core.ops.function.FnMut Self Args
+ call : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
end traits