afcf52e623
This PR generates `.ctorIdx` functions for all inductive types, not just enumeration types. This can be a building block for other constructions (`BEq`, `noConfusion`) that are size-efficient even for large inductives. It also renames it from `.toCtorIdx` to `.ctorIdx`, which is the more idiomatic naming. The old name exists as an alias, with a deprecation attribute to be added after the next stage0 update. These functions can arguably compiled down to a rather efficient tag lookup, rather than a `case` statement. This is future work (but hopefully near future). For a fair number of basic types the compiler is not able to compile a function using `casesOn` until further definitions have been defined. This therefore (ab)uses the `genInjectivity` flag and `gen_injective_theorems%` command to also control the generation of this construct. For (slightly) more efficient kernel reduction one could use `.rec` rather than `.casesOn`. I did not do that yet, also because it complicates compilation.
71 lines
1.8 KiB
Text
71 lines
1.8 KiB
Text
inductive Enum where | a1 | a2 | a3 | a4 | a5
|
||
deriving DecidableEq
|
||
|
||
/--
|
||
info: @[reducible] 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: @[reducible] 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: @[reducible] 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: @[reducible] 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: @[reducible] 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
|
||
|
||
|
||
unsafe inductive U : Type | mk : (U → U) → U
|
||
/--
|
||
info: @[reducible] unsafe protected def U.ctorIdx : U → Nat :=
|
||
fun x => U.casesOn x fun a => 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
|