inductive Lean.Compiler.LCNF.SpecParamInfo : Type

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

  fixedInst: 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.

  fixedHO: Lean.Compiler.LCNF.SpecParamInfo

• Computationally irrelevant parameters that are fixed in recursive declarations.

  fixedNeutral: 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.

  user: Lean.Compiler.LCNF.SpecParamInfo

• Parameter is not going to be specialized.

  other: Lean.Compiler.LCNF.SpecParamInfo

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

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.SMap Lean.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 : Lean.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

• Lean.Compiler.LCNF.SpecState.addEntry s e = match s with | { specInfo := specInfo } => { specInfo := Lean.SMap.insert specInfo e.declName e.paramsInfo }

def Lean.Compiler.LCNF.SpecState.switch : Lean.Compiler.LCNF.SpecState → Lean.Compiler.LCNF.SpecState

Equations

• Lean.Compiler.LCNF.SpecState.switch _fun_discr = match _fun_discr with | { specInfo := specInfo } => { specInfo := Lean.SMap.switch specInfo }

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.

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 : Lean.Name) : Option (Array Lean.Compiler.LCNF.SpecParamInfo)

Equations

• Lean.Compiler.LCNF.getSpecParamInfoCore? env declName = Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.Compiler.LCNF.specExtension env).specInfo declName

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

Equations

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

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

Equations

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