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.
101 lines
2.5 KiB
Text
101 lines
2.5 KiB
Text
inductive Enum where | a1 | a2 | a3 | a4 | a5
|
||
deriving DecidableEq
|
||
|
||
/--
|
||
info: protected def Enum.ctorIdx : Enum → Nat :=
|
||
fun x => Enum.casesOn x 0 1 2 3 4
|
||
-/
|
||
#guard_msgs in
|
||
#print Enum.ctorIdx
|
||
|
||
inductive NonRec where | a1 (u : Unit) | a2 (i : Int) | a3 (n : Nat) (f : Fin n) | a4 (s : String) (b : Bool) | a5
|
||
|
||
/--
|
||
info: protected def NonRec.ctorIdx : NonRec → Nat :=
|
||
fun x => NonRec.casesOn x (fun u => 0) (fun i => 1) (fun n f => 2) (fun s b => 3) 4
|
||
-/
|
||
#guard_msgs in
|
||
#print NonRec.ctorIdx
|
||
|
||
|
||
inductive Nested (α : Type) where
|
||
| a1 (x : α)
|
||
| a2 (y : Nested α)
|
||
| a3 (z : List (Nested α))
|
||
|
||
/--
|
||
info: protected def Nested.ctorIdx : {α : Type} → Nested α → Nat :=
|
||
fun {α} x => x.casesOn (fun x => 0) (fun y => 1) fun z => 2
|
||
-/
|
||
#guard_msgs in
|
||
#print Nested.ctorIdx
|
||
|
||
mutual
|
||
inductive A (m : Nat) : Nat → Type
|
||
| self : A m n → A m (n+m)
|
||
| other : B m n → A m (n+m)
|
||
| empty : A m 0
|
||
inductive B (m : Nat) : Nat → Type
|
||
| self : B m n → B m (n+m)
|
||
| other : A m n → B m (n+m)
|
||
| empty : B m 0
|
||
end
|
||
|
||
/--
|
||
info: protected def A.ctorIdx : {m a : Nat} → A m a → Nat :=
|
||
fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
|
||
-/
|
||
#guard_msgs in
|
||
#print A.ctorIdx
|
||
/--
|
||
info: protected def B.ctorIdx : {m a : Nat} → B m a → Nat :=
|
||
fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
|
||
-/
|
||
#guard_msgs in
|
||
#print B.ctorIdx
|
||
|
||
-- Single constructor inductives do not use casesOn
|
||
|
||
inductive Single where | only (n : Nat)
|
||
/--
|
||
info: protected def Single.ctorIdx : Single → Nat :=
|
||
fun x => 0
|
||
-/
|
||
#guard_msgs in #print Single.ctorIdx
|
||
|
||
structure Struct where
|
||
field1 : Nat
|
||
field2 : Bool
|
||
/--
|
||
info: protected def Struct.ctorIdx : Struct → Nat :=
|
||
fun x => 0
|
||
-/
|
||
#guard_msgs in #print Struct.ctorIdx
|
||
|
||
-- Unsafe inductives do get a definition
|
||
|
||
unsafe inductive U : Type | mk : (U → U) → U
|
||
/--
|
||
info: unsafe protected def U.ctorIdx : U → Nat :=
|
||
fun x => 0
|
||
-/
|
||
#guard_msgs in
|
||
#print U.ctorIdx
|
||
|
||
-- This should not get a ctorIdx, only types should
|
||
|
||
inductive Eq' : α → α → Prop where | refl (a : α) : Eq' a a
|
||
/-- error: Unknown constant `Eq'.ctorIdx` -/
|
||
#guard_msgs in
|
||
#print Eq'.ctorIdx
|
||
|
||
|
||
set_option linter.deprecated true
|
||
|
||
-- Enumeration types get a deprecated alias, other types dont
|
||
/-- info: Enum.toCtorIdx : Enum → Nat -/
|
||
#guard_msgs in #check Enum.toCtorIdx
|
||
/-- warning: `Enum.toCtorIdx` has been deprecated: Use `Enum.ctorIdx` instead -/
|
||
#guard_msgs in example := Enum.toCtorIdx
|
||
/-- error: Unknown identifier `Nonrec.toCtorIdx` -/
|
||
#guard_msgs in #check Nonrec.toCtorIdx
|