Documentation

Lean.Compiler.LCNF.FixedParams

Fixed Parameter Static Analyzer #

source
inductive Lean.Compiler.LCNF.FixedParams.AbsValue :
Type

Abstract value for the "fixed parameter" analysis.

Instances For
    source
    instance Lean.Compiler.LCNF.FixedParams.instInhabitedAbsValue :
    Inhabited Lean.Compiler.LCNF.FixedParams.AbsValue
    Equations
    source
    instance Lean.Compiler.LCNF.FixedParams.instBEqAbsValue :
    BEq Lean.Compiler.LCNF.FixedParams.AbsValue
    Equations
    source
    instance Lean.Compiler.LCNF.FixedParams.instHashableAbsValue :
    Hashable Lean.Compiler.LCNF.FixedParams.AbsValue
    Equations
    source
    structure Lean.Compiler.LCNF.FixedParams.Context :
    Type
    Instances For
      source
      structure Lean.Compiler.LCNF.FixedParams.State :
      Type
      • visited : Lean.HashSet (Lake.Name × Array Lean.Compiler.LCNF.FixedParams.AbsValue)

        Set of calls that have been already analyzed. Recall that we assume that only functions in decls may have recursive calls to the function being analyzed (i.e., main). Whenever there is function application f a₁ ... aₙ, where f is in decls, f is not main, and we visit with the abstract values assigned to aᵢ, but first we record the visit here.

      • fixed : Array Bool

        Bitmask containing the result, i.e., which parameters of main are fixed. We initialize it with true everywhere.

      Instances For
        source
        @[inline, reducible]
        abbrev Lean.Compiler.LCNF.FixedParams.FixParamM (α : Type) :
        Type

        Monad for the fixed parameter static analyzer. We use the unit-exception to interrupt the analysis.

        Equations
        Instances For
          source
          @[inline, reducible]
          abbrev Lean.Compiler.LCNF.FixedParams.abort {α : Type} :
          Lean.Compiler.LCNF.FixedParams.FixParamM α

          Stop the analysis and mark all parameters as non-fixed.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Compiler.LCNF.FixedParams.evalFVar (fvarId : Lean.FVarId) :
            Lean.Compiler.LCNF.FixedParams.FixParamM Lean.Compiler.LCNF.FixedParams.AbsValue
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Compiler.LCNF.FixedParams.evalArg (arg : Lean.Compiler.LCNF.Arg) :
              Lean.Compiler.LCNF.FixedParams.FixParamM Lean.Compiler.LCNF.FixedParams.AbsValue
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Compiler.LCNF.FixedParams.inMutualBlock (declName : Lake.Name) :
                Lean.Compiler.LCNF.FixedParams.FixParamM Bool
                Equations
                Instances For
                  source
                  def Lean.Compiler.LCNF.FixedParams.mkAssignment (decl : Lean.Compiler.LCNF.Decl) (values : Array Lean.Compiler.LCNF.FixedParams.AbsValue) :
                  Lean.FVarIdMap Lean.Compiler.LCNF.FixedParams.AbsValue
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def Lean.Compiler.LCNF.FixedParams.evalLetValue (e : Lean.Compiler.LCNF.LetValue) :
                    Lean.Compiler.LCNF.FixedParams.FixParamM Unit
                    source
                    partial def Lean.Compiler.LCNF.FixedParams.evalCode (code : Lean.Compiler.LCNF.Code) :
                    Lean.Compiler.LCNF.FixedParams.FixParamM Unit
                    source
                    partial def Lean.Compiler.LCNF.FixedParams.evalApp (declName : Lake.Name) (args : Array Lean.Compiler.LCNF.Arg) :
                    Lean.Compiler.LCNF.FixedParams.FixParamM Unit
                    source
                    def Lean.Compiler.LCNF.FixedParams.mkInitialValues (numParams : Nat) :
                    Array Lean.Compiler.LCNF.FixedParams.AbsValue
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Lean.Compiler.LCNF.mkFixedParamsMap (decls : Array Lean.Compiler.LCNF.Decl) :
                      Lake.NameMap (Array Bool)

                      Given the (potentially mutually) recursive declarations decls, return a map from declaration name decl.name to a bit-mask m where m[i] is true iff the decl.params[i] is a fixed argument. That is, it does not change in recursive applications. The function 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