Documentation

Lean.Compiler.LCNF.Simp.FunDeclInfo

Local function usage information used to decide whether it should be inlined or not. The information is an approximation, but it is on the "safe" side. That is, if we tagged a function with .once, then it is applied only once. A local function may be marked as .many, but after simplifications the number of applications may reduce to 1. This is not a big problem in practice because we run the simplifier multiple times, and this information is recomputed from scratch at the beginning of each simplification step.

Instances For

    Local function declaration statistics.

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

        Add new occurrence for the local function with binder name key.

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

          Add new occurrence for the local function occurring as an argument for another function.

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

            Add new occurrence for the local function with binder name key.

            Equations
            Instances For
              Equations
              • { map := map }.restore fvarId none = { map := map.erase fvarId }
              • { map := map }.restore fvarId (some saved) = { map := map.insert fvarId saved }
              Instances For

                Traverse code and update function occurrence map. This map is used to decide whether we inline local functions or not. If mustInline := true, then all local function declarations occurring in code are tagged as .mustInline. Recall that we use .mustInline for local function declarations occurring in type class instances.

                Equations
                Instances For