mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
205 lines
4.2 KiB
Lean4
205 lines
4.2 KiB
Lean4
import Lean.Elab.Deriving.ToExpr
|
||
|
||
/-!
|
||
# Tests for the `ToExpr` deriving handler
|
||
-/
|
||
|
||
open Lean
|
||
|
||
/-!
|
||
Test without universes
|
||
-/
|
||
inductive MonoOption' (α : Type) : Type
|
||
| some (a : α)
|
||
| none
|
||
deriving ToExpr
|
||
|
||
/--
|
||
info: Lean.Expr.app
|
||
(Lean.Expr.app (Lean.Expr.const `MonoOption'.some []) (Lean.Expr.const `Bool []))
|
||
(Lean.Expr.const `Bool.true [])
|
||
-/
|
||
#guard_msgs in
|
||
#eval repr <| toExpr <| MonoOption'.some true
|
||
|
||
/-!
|
||
Test with a universe polymorphic type parameter
|
||
-/
|
||
inductive Option' (α : Type u)
|
||
| some (a : α)
|
||
| none
|
||
deriving ToExpr
|
||
|
||
/--
|
||
info: Lean.Expr.app
|
||
(Lean.Expr.app (Lean.Expr.const `Option'.some [Lean.Level.zero]) (Lean.Expr.const `Bool []))
|
||
(Lean.Expr.const `Bool.true [])
|
||
-/
|
||
#guard_msgs in
|
||
#eval repr <| toExpr <| Option'.some true
|
||
|
||
example : ToExpr (Option' Nat) := inferInstance
|
||
|
||
/-!
|
||
Test with higher universe levels
|
||
-/
|
||
structure MyULift.{r, s} (α : Type s) : Type (max s r) where
|
||
up :: down : α
|
||
deriving ToExpr
|
||
|
||
/--
|
||
info: Lean.Expr.app
|
||
(Lean.Expr.app
|
||
(Lean.Expr.const `Option'.some [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero))])
|
||
(Lean.Expr.app
|
||
(Lean.Expr.const `MyULift [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero)), Lean.Level.zero])
|
||
(Lean.Expr.const `Bool [])))
|
||
(Lean.Expr.app
|
||
(Lean.Expr.app
|
||
(Lean.Expr.const `MyULift.up [Lean.Level.succ (Lean.Level.succ (Lean.Level.zero)), Lean.Level.zero])
|
||
(Lean.Expr.const `Bool []))
|
||
(Lean.Expr.const `Bool.true []))
|
||
-/
|
||
#guard_msgs in
|
||
#eval repr <| toExpr <| Option'.some (MyULift.up.{2} true)
|
||
|
||
example : ToExpr (Option' <| MyULift.{20} Nat) := inferInstance
|
||
example [ToLevel.{u}] : ToExpr (Option' <| MyULift.{u} Nat) := inferInstance
|
||
|
||
/-!
|
||
Test with empty type.
|
||
-/
|
||
inductive Empty'
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with recursive type
|
||
-/
|
||
inductive List' (α : Type u)
|
||
| cons (a : α) (as : List' α)
|
||
| nil
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with nested type
|
||
-/
|
||
inductive Foo
|
||
| l (x : List Foo)
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with mutual inductive type
|
||
-/
|
||
mutual
|
||
inductive A
|
||
| nil
|
||
| cons (a : A) (b : B)
|
||
deriving ToExpr
|
||
inductive B
|
||
| cons₁ (a : A)
|
||
| cons₂ (a : A) (b : B)
|
||
deriving ToExpr
|
||
end
|
||
|
||
/--
|
||
info: Lean.Expr.app
|
||
(Lean.Expr.app (Lean.Expr.const `A.cons []) (Lean.Expr.const `A.nil []))
|
||
(Lean.Expr.app (Lean.Expr.const `B.cons₁ []) (Lean.Expr.const `A.nil []))
|
||
-/
|
||
#guard_msgs in
|
||
#eval repr <| toExpr <| A.cons A.nil (B.cons₁ A.nil)
|
||
/--
|
||
info: Lean.Expr.app
|
||
(Lean.Expr.app (Lean.Expr.const `B.cons₂ []) (Lean.Expr.const `A.nil []))
|
||
(Lean.Expr.app (Lean.Expr.const `B.cons₁ []) (Lean.Expr.const `A.nil []))
|
||
-/
|
||
#guard_msgs in
|
||
#eval repr <| toExpr <| B.cons₂ A.nil (B.cons₁ A.nil)
|
||
|
||
/-!
|
||
Test with explicit universe level
|
||
-/
|
||
|
||
inductive WithUniverse.{u} (α : Type u)
|
||
| foo (a : α)
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with universe level coming from `universe` command
|
||
-/
|
||
universe u in
|
||
inductive WithAmbientUniverse (α : Type u)
|
||
| foo (a : α)
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with an ambient universe `u`, a directly specified universe `v`, and an implicit universe `w`.
|
||
-/
|
||
universe u in
|
||
structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (γ : Type w) where
|
||
a : α
|
||
b : β
|
||
c : γ
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test using the `variable` command, with an autoimplicit universe.
|
||
-/
|
||
variable (α : Type u) in
|
||
inductive VariableParameter : Type u
|
||
| foo (a : α)
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Mutual inductive with universe levels.
|
||
-/
|
||
mutual
|
||
inductive A' (α : Type u) where
|
||
| mk (x : α) (a : A' α) (b : B' α)
|
||
deriving ToExpr
|
||
inductive B' (α : Type u) where
|
||
| mk (x : α) (a : A' α) (b : B' α)
|
||
deriving ToExpr
|
||
end
|
||
|
||
/-!
|
||
Nested with universe level.
|
||
-/
|
||
inductive Foo' (α : Type u)
|
||
| l (x : α) (x : List (Foo' α))
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
### Tests with without universe autoimplicits.
|
||
-/
|
||
section NoAutoImplicit
|
||
set_option autoImplicit false
|
||
|
||
/-!
|
||
Test with universe specified directly on the type
|
||
-/
|
||
inductive ExplicitList'.{u} (α : Type u)
|
||
| cons (a : α) (as : List' α)
|
||
| nil
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with ambient (explicit) universe
|
||
-/
|
||
universe u in
|
||
inductive AmbientList' (α : Type u)
|
||
| cons (a : α) (as : List' α)
|
||
| nil
|
||
deriving ToExpr
|
||
|
||
/-!
|
||
Test with both ambient and directly specified universes.
|
||
-/
|
||
universe u in
|
||
structure ExplicitAmbientPair.{v} (α : Type u) (β : Type v) where
|
||
a : α
|
||
b : β
|
||
deriving ToExpr
|
||
|
||
end NoAutoImplicit
|