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.
140 lines
3.7 KiB
Text
140 lines
3.7 KiB
Text
|
||
universe w₁ w₂ w₃
|
||
|
||
namespace Struct
|
||
structure S1.{r, s} (α : Type s) : Type (max s r) :=
|
||
up :: (down : α)
|
||
|
||
def ex1.{u, v} (α : Type u) (σ : Type (max v u)) (h : σ = S1.{v, u} α) : True :=
|
||
trivial
|
||
|
||
structure S2.{u, v} (α : Sort u) (β : Sort v) :=
|
||
(a : α)
|
||
(b : β)
|
||
|
||
def ex2.{u, v} (α : Sort u) (β : Sort v) (σ : Sort (max u v 1)) (h : σ = S2 α β) : True :=
|
||
trivial
|
||
|
||
structure S3.{u, v} (α : Type u) (β : Type v) :=
|
||
(a : α)
|
||
(b : β)
|
||
|
||
def ex3.{u, v} (α : Type u) (β : Type v) (σ : Type (max u v)) (h : σ = S3 α β) : True :=
|
||
trivial
|
||
|
||
structure S4.{u, v} (α : Sort u) (β : Sort v) : Type _ := -- Warning: possibly too high
|
||
(a : α)
|
||
(b : β)
|
||
|
||
structure S5.{u, v} (α : Type (u+1)) (β : Type v) :=
|
||
(a : α)
|
||
(b : β)
|
||
|
||
def ex5.{u, v} (α : Type (u+1)) (β : Type v) (σ : Type (max (u+1) v)) (h : σ = S5 α β) : True :=
|
||
trivial
|
||
|
||
structure S6.{u, v} (α : Sort (max u v)) (β : Type v) :=
|
||
(a : α)
|
||
(b : β)
|
||
|
||
#check S6.{w₁, w₂}
|
||
|
||
def ex6.{u, v} (α : Sort (max u v)) (β : Type v) (σ : Sort max u (v+1)) (h : σ = S6.{u, v} α β) : True :=
|
||
trivial
|
||
|
||
structure S7.{u, v} (α : Sort u) (β : Sort v) : Sort (max u v) := -- Error: invalid universe polymorphic type
|
||
(a : α) (b : β)
|
||
|
||
end Struct
|
||
|
||
namespace Induct
|
||
|
||
inductive S2.{u, v} (α : Sort u) (β : Sort v)
|
||
| mk (a : α) (b : β)
|
||
|
||
def ex2.{u, v} (α : Sort u) (β : Sort v) (σ : Sort (max u v 1)) (h : σ = S2 α β) : True :=
|
||
trivial
|
||
|
||
inductive S3.{u, v} (α : Type u) (β : Type v)
|
||
| mk (a : α) (b : β)
|
||
|
||
def ex3.{u, v} (α : Type u) (β : Type v) (σ : Type (max u v)) (h : σ = S3 α β) : True :=
|
||
trivial
|
||
|
||
inductive S4.{u, v} (α : Sort u) (β : Sort v) : Type _ -- Error: inference procedure failed
|
||
| mk (a : α) (b : β)
|
||
|
||
inductive S5.{u, v} (α : Type (u+1)) (β : Type v)
|
||
| mk (a : α) (b : β)
|
||
|
||
def ex5.{u, v} (α : Type (u+1)) (β : Type v) (σ : Type (max (u+1) v)) (h : σ = S5 α β) : True :=
|
||
trivial
|
||
|
||
inductive S6.{u, v} (α : Sort u) (β : Sort v) : Sort (max u v) -- Warning: possibly too high
|
||
| mk (a : α) (b : β)
|
||
|
||
inductive Term
|
||
| Var : Nat → Term
|
||
| App : Term → Term → Term
|
||
| All : (Nat → Term) → Term
|
||
|
||
open Lean
|
||
|
||
inductive Stx
|
||
| node (args : Array Stx) : Stx
|
||
|
||
def ex7 (h : Stx = Nat) : True :=
|
||
trivial
|
||
|
||
|
||
/-!
|
||
Universe level inference failure is localized to syntax of field type.
|
||
-/
|
||
structure S8 : Type 5 where
|
||
t1 : Sort _
|
||
|
||
/-!
|
||
Used to have an 'accidental higher universe' error.
|
||
The issue was that we would get the constraints `u ≤ ?r + 1` and `u ≤ ?r`
|
||
and it would complain about the first, despite the fact that it's implied by the second.
|
||
-/
|
||
inductive NotBadLevelConstraint (α : Sort u) (β : Type u) : Type _ where
|
||
| mk (x : α) (y : β)
|
||
|
||
/-!
|
||
Used to have 'accidental higher universe' error.
|
||
The issue was that we would get the constraints `u ≤ ?r` and `u ≤ ?r + 1`
|
||
like in `NotBadLevelConstraint`.
|
||
-/
|
||
inductive NotBadLevelConstraint'
|
||
| foobar {Foo : Sort u} : Foo → NotBadLevelConstraint'
|
||
| somelist : List NotBadLevelConstraint' → NotBadLevelConstraint'
|
||
|
||
namespace Sorry
|
||
set_option warn.sorry false
|
||
|
||
/-!
|
||
Used to have an 'accidental higher universe' error.
|
||
Now there's no error. Since the resulting type is `Type`, it infers `sorry : Type`.
|
||
-/
|
||
inductive Sorry1 where
|
||
| y (b : sorry)
|
||
|
||
/-!
|
||
Used to have an 'invalid universe level in constructor' error.
|
||
Now there's no error. Since the resulting type is `Type`, it infers `sorry : Type`.
|
||
-/
|
||
inductive Sorry1' : Type where
|
||
| y (b : sorry)
|
||
|
||
/-!
|
||
Used to have an 'accidental higher universe' error.
|
||
Now has a "failed to infer universe levels in type of binder" error instead,
|
||
since the universe of `sorry` is underconstrained.
|
||
-/
|
||
inductive Sorry2 : Type 2 where
|
||
| y (b : sorry)
|
||
|
||
end Sorry
|
||
|
||
end Induct
|