inductive Lean.Compiler.LCNF.SpecParamInfo : Type

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

• 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.

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

Equations

• Lean.Compiler.LCNF.instInhabitedSpecParamInfo = { default := Lean.Compiler.LCNF.SpecParamInfo.fixedInst }

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

Equations

• Lean.Compiler.LCNF.instReprSpecParamInfo = { reprPrec := Lean.Compiler.LCNF.reprSpecParamInfo✝ }

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedSpecState = { default := { specInfo := default } }

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

Equations

• Lean.Compiler.LCNF.instInhabitedSpecEntry = { default := { declName := default, paramsInfo := default } }

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

Equations

• { specInfo := specInfo }.addEntry e = { specInfo := Lean.PersistentHashMap.insert specInfo e.declName e.paramsInfo }

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 dependencies 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.

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.getSpecParamInfo? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getSpecParamInfoCore? __do_lift declName)

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

Equations

• Lean.Compiler.LCNF.isSpecCandidate declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getSpecParamInfoCore? __do_lift declName).isSome