Documentation

Lean.Compiler.LCNF.SpecInfo

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

Instances For
    source
    instance Lean.Compiler.LCNF.instInhabitedSpecParamInfo :
    Inhabited Lean.Compiler.LCNF.SpecParamInfo
    source
    instance Lean.Compiler.LCNF.instReprSpecParamInfo :
    Repr Lean.Compiler.LCNF.SpecParamInfo
    source
    instance Lean.Compiler.LCNF.instToMessageDataSpecParamInfo :
    Lean.ToMessageData Lean.Compiler.LCNF.SpecParamInfo
    Equations
    • One or more equations did not get rendered due to their size.
    source
    structure Lean.Compiler.LCNF.SpecState :
    Type
    Instances For
      source
      instance Lean.Compiler.LCNF.instInhabitedSpecState :
      Inhabited Lean.Compiler.LCNF.SpecState
      source
      structure Lean.Compiler.LCNF.SpecEntry :
      Type
      Instances For
        source
        instance Lean.Compiler.LCNF.instInhabitedSpecEntry :
        Inhabited Lean.Compiler.LCNF.SpecEntry
        source
        def Lean.Compiler.LCNF.SpecState.addEntry (s : Lean.Compiler.LCNF.SpecState) (e : Lean.Compiler.LCNF.SpecEntry) :
        Lean.Compiler.LCNF.SpecState
        Instances For
          source
          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).

          source
          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.
          Instances For
            source
            def Lean.Compiler.LCNF.getSpecParamInfoCore? (env : Lean.Environment) (declName : Lean.Name) :
            Option (Array Lean.Compiler.LCNF.SpecParamInfo)
            Instances For
              source
              def Lean.Compiler.LCNF.getSpecParamInfo? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) :
              m (Option (Array Lean.Compiler.LCNF.SpecParamInfo))
              Instances For
                source
                def Lean.Compiler.LCNF.isSpecCandidate {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) :
                m Bool
                Equations
                Instances For