inductive Lean.Compiler.LCNF.SpecParamInfo : Type

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

• fixedInst : 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 : 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 : SpecParamInfo

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

• user : 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 : SpecParamInfo

  Parameter is not going to be specialized.

instance Lean.Compiler.LCNF.instInhabitedSpecParamInfo : Inhabited SpecParamInfo

Equations

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

def Lean.Compiler.LCNF.instInhabitedSpecParamInfo.default : SpecParamInfo

Equations

• Lean.Compiler.LCNF.instInhabitedSpecParamInfo.default = Lean.Compiler.LCNF.SpecParamInfo.fixedInst

def Lean.Compiler.LCNF.instReprSpecParamInfo.repr : SpecParamInfo → Nat → Format

Equations

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

instance Lean.Compiler.LCNF.instReprSpecParamInfo : Repr SpecParamInfo

Equations

• Lean.Compiler.LCNF.instReprSpecParamInfo = { reprPrec := Lean.Compiler.LCNF.instReprSpecParamInfo.repr }

@[inline]

def Lean.Compiler.LCNF.SpecParamInfo.causesSpecialization : SpecParamInfo → Bool

Equations

• Lean.Compiler.LCNF.SpecParamInfo.fixedInst.causesSpecialization = true
• Lean.Compiler.LCNF.SpecParamInfo.fixedHO.causesSpecialization = true
• Lean.Compiler.LCNF.SpecParamInfo.user.causesSpecialization = true
• Lean.Compiler.LCNF.SpecParamInfo.fixedNeutral.causesSpecialization = false
• Lean.Compiler.LCNF.SpecParamInfo.other.causesSpecialization = false

instance Lean.Compiler.LCNF.instToMessageDataSpecParamInfo : ToMessageData SpecParamInfo

Equations

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

structure Lean.Compiler.LCNF.SpecEntry : Type

• declName : Name

  The name of the declaration.

• paramsInfo : Array SpecParamInfo

  Information about which parameters of the declaration qualify for specialization.

• alreadySpecialized : Bool

  True if declName was already specialized before. This is relevant because we specialize declarations that have already been specialized less aggressively than declarations that have not.

def Lean.Compiler.LCNF.instInhabitedSpecEntry.default : SpecEntry

Equations

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

instance Lean.Compiler.LCNF.instInhabitedSpecEntry : Inhabited SpecEntry

Equations

• Lean.Compiler.LCNF.instInhabitedSpecEntry = { default := Lean.Compiler.LCNF.instInhabitedSpecEntry.default }

instance Lean.Compiler.LCNF.instToMessageDataSpecEntry : ToMessageData SpecEntry

Equations

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

structure Lean.Compiler.LCNF.SpecState : Type

• specInfo : PHashMap Name SpecEntry

instance Lean.Compiler.LCNF.instInhabitedSpecState : Inhabited SpecState

Equations

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

def Lean.Compiler.LCNF.instInhabitedSpecState.default : SpecState

Equations

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

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

Equations

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

opaque Lean.Compiler.LCNF.specExtension : SimplePersistentEnvExtension SpecEntry 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.computeSpecEntries (decls : Array Decl) (autoSpecialize : Name → Option (Array Nat) → Bool) (alreadySpecialized : Array Bool) : CompilerM (Array SpecEntry)

Compute specialization information for decls. We assume that decls contains a full SCC of computationally relevant declarations. Furthermore this function takes:

• autoSpecialize which determines whether we apply "automated" specialization to a decl, that is whether we automatically specialize for all fixedHO parameters. It receives both the name and the array of arguments mentioned in @[specialize] if any.
• alreadySpecialized which is a mask that says whether a decl is already a specialized declaration itself.

Equations

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

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

Compute and save specialization information for decls. Assumes that decls is an SCC of user defined declarations.

Equations

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

def Lean.Compiler.LCNF.getSpecEntryCore? (env : Environment) (declName : Name) : Option SpecEntry

Equations

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

def Lean.Compiler.LCNF.getSpecEntry? {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m (Option SpecEntry)

Equations

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

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

Equations

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