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

Instances For

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

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

Instances For

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

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

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

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

Instances For

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

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

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

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

source
structure Lean.Compiler.LCNF.SpecState :
Type

- specInfo : PHashMap Name (Array SpecParamInfo)

Instances For

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

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

Instances For

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

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

source
structure Lean.Compiler.LCNF.SpecEntry :
Type

- declName : Name
- paramsInfo : Array SpecParamInfo

Instances For

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

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

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

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

Instances For

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

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

Instances For

source
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`).

source
def Lean.Compiler.LCNF.saveSpecParamInfo (decls : Array Decl) :
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.

Instances For

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

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

Instances For

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

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

Instances For

source
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.getSpecParamInfoCore? __do_lift declName).isSome

Instances For