Documentation

Lean.Compiler.LCNF.FixedParams

Fixed Parameter Static Analyzer #

Instances For
    • 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
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, inline]

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

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

                  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