inductive Lean.Compiler.LCNF.SpecParamInfo : Type

• fixedInst: Lean.Compiler.LCNF.SpecParamInfo

  A parameter that is an type class instance (or an arrow that produces a type class instance), and is fixed in recursive declarations. By default, Lean always specializes this kind of argument.

• fixedHO: Lean.Compiler.LCNF.SpecParamInfo

  A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration with @[specialize] without specifying which arguments should be specialized, Lean will specialize .fixedHO arguments in addition to .fixedInst.

• fixedNeutral: Lean.Compiler.LCNF.SpecParamInfo

  Computationally irrelevant parameters that are fixed in recursive declarations, and there is a fixedInst, fixedHO, or user param that depends on it.

• user: Lean.Compiler.LCNF.SpecParamInfo

  An argument that has been specified in the @[specialize] attribute. Lean specializes it even if it is not fixed in recursive declarations. Non-termination can happen, and Lean interrupts it with an error message based on the stack depth.

• other: Lean.Compiler.LCNF.SpecParamInfo

  Parameter is not going to be specialized.

Each parameter is associated with a SpecParamInfo. This information is used by LCNF/Specialize.lean.

instance Lean.Compiler.LCNF.instInhabitedSpecParamInfo : Inhabited Lean.Compiler.LCNF.SpecParamInfo

instance Lean.Compiler.LCNF.instReprSpecParamInfo : Repr Lean.Compiler.LCNF.SpecParamInfo

instance Lean.Compiler.LCNF.instToMessageDataSpecParamInfo : Lean.ToMessageData Lean.Compiler.LCNF.SpecParamInfo

structure Lean.Compiler.LCNF.SpecState : Type

• specInfo : Lean.PHashMap Lake.Name (Array Lean.Compiler.LCNF.SpecParamInfo)

instance Lean.Compiler.LCNF.instInhabitedSpecState : Inhabited Lean.Compiler.LCNF.SpecState

structure Lean.Compiler.LCNF.SpecEntry : Type

• declName : Lake.Name
• paramsInfo : Array Lean.Compiler.LCNF.SpecParamInfo

instance Lean.Compiler.LCNF.instInhabitedSpecEntry : Inhabited Lean.Compiler.LCNF.SpecEntry

def Lean.Compiler.LCNF.SpecState.addEntry (s : Lean.Compiler.LCNF.SpecState) (e : Lean.Compiler.LCNF.SpecEntry) : Lean.Compiler.LCNF.SpecState

opaque Lean.Compiler.LCNF.specExtension : Lean.SimplePersistentEnvExtension Lean.Compiler.LCNF.SpecEntry Lean.Compiler.LCNF.SpecState

Extension for storing SpecParamInfo for declarations being compiled. Remark: we only store information for declarations that will be specialized.

Note: fixedNeutral must have forward dependencies.

The code specializer consider a fixedNeutral parameter during code specialization only if it contains forward dependecies that are tagged as .user, .fixedHO, or .fixedInst. The motivation is to minimize the number of code specializations that have little or no impact on performance. For example, let's consider the function.

def liftMacroM
    {α : Type} {m : Type → Type}
    [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m]
    [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do

The parameter α does not occur in any local instance, and x is marked as .other since the function is not tagged as [specialize]. There is little value in considering α during code specialization, but if we do many copies of this function will be generated. Recall users may still force the code specializer to take α into account by using [specialize α] (α has .user info), or [specialize x] (α has .fixedNeutral since x is a forward dependency tagged as .user), or [specialize] (α has .fixedNeutral since x is a forward dependency tagged as .fixedHO).

def Lean.Compiler.LCNF.saveSpecParamInfo (decls : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

Save parameter information for decls.

Remark: this function, similarly to mkFixedArgMap, assumes that if a function f was declared in a mutual block, then decls contains all (computationally relevant) functions in the mutual block.

def Lean.Compiler.LCNF.getSpecParamInfoCore? (env : Lean.Environment) (declName : Lake.Name) : Option (Array Lean.Compiler.LCNF.SpecParamInfo)

def Lean.Compiler.LCNF.getSpecParamInfo? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m (Option (Array Lean.Compiler.LCNF.SpecParamInfo))

def Lean.Compiler.LCNF.isSpecCandidate {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m Bool