Documentation

Lean.Compiler.LCNF.SpecInfo

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

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

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

      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 dependecies 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).

      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
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Instances For
            Equations
            Instances For