Elaborator framework for (mutual) inductives

This module defines the framework for elaborating (mutually recursive) inductive types. Commands such as inductive and structure plug into this framework, and the framework orchestrates their mutual elaboration.

The main entry point for new inductive commands are the @[builtin_inductive_elab]/@[inductive_elab] attributes, which register a handler for a given decl syntax.

The main entry point to elaboration are the functions

• Lean.Elab.Command.isInductiveCommand to determine whether syntax has a registered inductive elaborator.
• Lean.Elab.Command.elabInductives to elaborate a list of syntaxes as mutually inductive types.
• Lean.Elab.Command.elabInductive to elaborate a single inductive command.

For mutual ... end in particular:

• Lean.Elab.Command.isMutualInductive to check whether each syntax element of a mutual ... end block has a registered inductive elaborator.
• Lean.Elab.Command.elabMutualInductive to elaborate a list of syntaxes satisfying isMutualInductive as a mutually inductive block.

See the docstring on Lean.Elab.Command.InductiveElabDescr for an overview of the framework.

opaque Lean.Elab.Command.inductive.autoPromoteIndices : Lean.Option Bool

opaque Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse : Lean.Option Bool

structure Lean.Elab.Command.CtorView : Type

View of a constructor. Only ref, modifiers, declName, and declId are required by the mutual inductive elaborator itself.

• ref : Syntax

  Syntax for the whole constructor.

• modifiers : Modifiers
• declName : Name

  Fully qualified name of the constructor.

• declId : Syntax

  Syntax for the name of the constructor, used to apply terminfo. If the source is synthetic, terminfo is not applied.

• binders : Syntax

  For handler use. The inductive uses it for the binders to the constructor.

• type? : Option Syntax

  For handler use. The inductive command uses it for the resulting type for the constructor.

instance Lean.Elab.Command.instInhabitedCtorView : Inhabited CtorView

Equations

• Lean.Elab.Command.instInhabitedCtorView = { default := { ref := default, modifiers := default, declName := default, declId := default, binders := default, type? := default } }

structure Lean.Elab.Command.ComputedFieldView : Type

• ref : Syntax
• modifiers : Syntax
• fieldId : Name
• type : Term
• matchAlts : TSyntax `Lean.Parser.Term.matchAlts

structure Lean.Elab.Command.InductiveView : Type

A view for generic inductive types.

• ref : Syntax
• declId : Syntax
• modifiers : Modifiers
• isClass : Bool
• allowIndices : Bool

  Whether the command should allow indices (like inductive) or not (like structure).

• allowSortPolymorphism : Bool

  Whether the command supports creating inductive types that can be polymorphic across both Prop and Type _. If false, then either the universe must be Prop or it must be of the form Type _.

• shortDeclName : Name
• declName : Name
• levelNames : List Name
• binders : Syntax
• type? : Option Syntax
• ctors : Array CtorView
• computedFields : Array ComputedFieldView
• derivingClasses : Array DerivingClassView

instance Lean.Elab.Command.instInhabitedInductiveView : Inhabited InductiveView

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Command.PreElabHeaderResult : Type

Elaborated header for an inductive type before fvars for each inductive are added to the local context.

• view : InductiveView
• levelNames : List Name
• numParams : Nat
• type : Expr
• origParams : Array Expr

  The parameters in the header's initial local context. Used for adding fvar alias terminfo.

instance Lean.Elab.Command.instInhabitedPreElabHeaderResult : Inhabited PreElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedPreElabHeaderResult = { default := { view := default, levelNames := default, numParams := default, type := default, origParams := default } }

structure Lean.Elab.Command.ElabHeaderResultextends Lean.Elab.Command.PreElabHeaderResult : Type

The elaborated header with the indFVar registered for this inductive type.

• view : InductiveView
• levelNames : List Name
• numParams : Nat
• type : Expr
• origParams : Array Expr
• indFVar : Expr

instance Lean.Elab.Command.instInhabitedElabHeaderResult : Inhabited ElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedElabHeaderResult = { default := { toPreElabHeaderResult := default, indFVar := default } }

structure Lean.Elab.Command.InductiveElabStep3 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr

• finalize : TermElabM Unit

  Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered. The levelParams, params, and replaceIndFVars arguments of prefinalize are still valid here.

structure Lean.Elab.Command.InductiveElabStep2 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• ctors : List Constructor

  The constructors produced by InductiveElabStep1.

• collectUsedFVars : StateRefT' IO.RealWorld CollectFVars.State MetaM Unit

  Function to collect additional fvars that might be missed by the constructors. It is permissible to include fvars that do not exist in the local context (structure for example includes its field fvars).

• checkUniverses (numParams : Nat) (u : Level) : TermElabM Unit

  Function to check universes and provide a custom error. (structure uses this to do checks per field to give nicer messages.)

• finalizeTermElab : TermElabM Unit

  Step to finalize term elaboration, done immediately after universe level processing is complete.

• prefinalize (levelParams : List Name) (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : TermElabM InductiveElabStep3

  Like finalize, but occurs before afterTypeChecking attributes.

instance Lean.Elab.Command.instInhabitedInductiveElabStep2 : Inhabited InductiveElabStep2

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Command.InductiveElabStep1 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• view : InductiveView
• elabCtors (rs : Array ElabHeaderResult) (r : ElabHeaderResult) (params : Array Expr) : TermElabM InductiveElabStep2

instance Lean.Elab.Command.instInhabitedInductiveElabStep1 : Inhabited InductiveElabStep1

Equations

• Lean.Elab.Command.instInhabitedInductiveElabStep1 = { default := { view := default, elabCtors := default } }

structure Lean.Elab.Command.InductiveElabDescr : Type

Descriptor for a command processor that elaborates an inductive type.

Elaboration occurs in the following steps:

• Every command has its mkInductiveView evaluated, producing InductiveViews and callbacks for the next steps (all recorded in InductiveElabStep1).
• Each InductiveView gets elaborated, creating ElabHeaderResults, and the local contexts are unified into a single one with a consistent set of parameters between each inductive.
• Each callback is called to elaborate each inductives' constructors and some additional callbacks (all recorded in InductiveElabStep2).
• Fvars are collected from the constructors and from the InductiveStep2.collectUsedFVars callbacks. This is used to compute the final set of scoped variables that should be used as additional parameters.
• Universe levels are checked. Commands can give custom errors using InductiveStep2.collectUniverses.
• Elaboration of constructors is finalized, with additional tasks done by each InductiveStep2.collectUniverses.
• The inductive family is added to the environment and is checked by the kernel.
• Attributes and other finalization activities are performed, including those defined by InductiveStep2.prefinalize and InductiveStep3.finalize.

• mkInductiveView : Modifiers → Syntax → TermElabM InductiveElabStep1

instance Lean.Elab.Command.instInhabitedInductiveElabDescr : Inhabited InductiveElabDescr

Equations

• Lean.Elab.Command.instInhabitedInductiveElabDescr = { default := { mkInductiveView := default } }

opaque Lean.Elab.Command.inductiveElabAttr : KeyedDeclsAttribute InductiveElabDescr

Environment extension to register inductive type elaborator commands.

def Lean.Elab.Command.isInductiveCommand {m : Type → Type} [Monad m] [MonadEnv m] (stx : Syntax) : m Bool

Returns true if the syntax partipates in the mutual inductive elaborator. These do not need to be commands. In fact inductive and structure are registered on the Lean.Parser.Command.inductive and Lean.Parser.Command.structure syntaxes.

Equations

• Lean.Elab.Command.isInductiveCommand stx = do let env ← Lean.getEnv pure !(Lean.Elab.Command.inductiveElabAttr.getEntries env stx.getKind).isEmpty

def Lean.Elab.Command.mkInductiveView (modifiers : Modifiers) (stx : Syntax) : TermElabM InductiveElabStep1

Initializes the elaborator associated to the given syntax.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.checkValidInductiveModifier {m : Type → Type} [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.checkValidCtorModifier {m : Type → Type} [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.withExplicitToImplicit {α : Type} (xs : Array Expr) (k : TermElabM α) : TermElabM α

Execute k with updated binder information for xs. Any x that is explicit becomes implicit.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId)

Returns some ?m if u is of the form ?m + k. Returns none if u does not contain universe metavariables. Throw exception otherwise.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.accLevel (u r : Level) (rOffset : Nat) : ExceptT MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit

Auxiliary function for updateResultingUniverse. Consider the constraint u ≤ ?r + rOffset where u has no metavariables except for perhaps ?r. This function attempts to find a unique minimal solution of the form ?r := max l₁ ... lₙ where each lᵢ is normalized and not a max/imax.

It also records information about how "too big" rOffset is. Consider u ≤ ?r + 1, from for example

inductive I (α : Sort u) : Type _ where
  | mk (x : α)

This is likely a mistake. The correct solution would be Type (max u 1) rather than Type (u + 1), but by this point it is impossible to rectify. So, for u ≤ ?r + 1 we record the pair of u and 1 so that we can inform the user what they should have probably used instead.

Equations

• Lean.Elab.Command.accLevel u r rOffset = Lean.Elab.Command.accLevel.go r u rOffset

def Lean.Elab.Command.accLevel.go (r u : Level) (rOffset : Nat) : ExceptT MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Command.accLevel.go r (u_2.max v) rOffset = do Lean.Elab.Command.accLevel.go r u_2 rOffset Lean.Elab.Command.accLevel.go r v rOffset
• Lean.Elab.Command.accLevel.go r (u_2.imax v) rOffset = do Lean.Elab.Command.accLevel.go r u_2 rOffset Lean.Elab.Command.accLevel.go r v rOffset
• Lean.Elab.Command.accLevel.go r Lean.Level.zero rOffset = pure ()
• Lean.Elab.Command.accLevel.go r u_2.succ rOffset_2.succ = Lean.Elab.Command.accLevel.go r u_2 rOffset_2

def Lean.Elab.Command.accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT Lean.Elab.Command.AccLevelState✝ TermElabM Unit

Auxiliary function for updateResultingUniverse. Applies accLevel to the given constructor parameter.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.withCtorRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (views : Array InductiveView) (ctorName : Name) (k : m α) : m α

Executes k using the Syntax reference associated with constructor ctorName.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.InductiveView.withTypeRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (view : InductiveView) (k : m α) : m α

Runs k with the resulting type as the ref or, if that's not available, with the view's ref.

Equations

• view.withTypeRef k = Lean.withRef view.ref (match view.type? with | some type => Lean.withRef type k | none => k)

def Lean.Elab.Command.withViewTypeRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (views : Array InductiveView) (k : m α) : m α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit

Equations

• Lean.Elab.Command.elabInductive modifiers stx = Lean.Elab.Command.elabInductives #[(modifiers, stx)]

def Lean.Elab.Command.isMutualInductive {m : Type → Type} [Monad m] [MonadEnv m] (stx : Syntax) : m Bool

Returns true if all elements of the mutual block (Lean.Parser.Command.mutual) are inductive declarations.

Equations

• Lean.Elab.Command.isMutualInductive stx = Array.allM (fun (elem : Lean.Syntax) => Lean.Elab.Command.isInductiveCommand elem[1]) stx[1].getArgs

def Lean.Elab.Command.elabMutualInductive (elems : Array Syntax) : CommandElabM Unit

Elaborates a mutual block, assuming the commands satisfy Lean.Elab.Command.isMutualInductive.

Equations

• One or more equations did not get rendered due to their size.