Documentation

Lean.Compiler.LCNF.Simp.Main

Create a new local function declaration when info.args.size < info.params.size. We use this function to inline/specialize a partial application of a local function.

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

    Try to inline a join point.

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

      When the configuration flag etaPoly = true, we eta-expand partial applications of functions that take local instances as arguments. This kind of function is inlined or specialized, and we create new simplification opportunities by eta-expanding them.

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

        Similar to Code.isReturnOf, but taking the current substitution into account.

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

            If the value of the given let-declaration is an application that can be inlined, inline it and simplify the result.

            k is the "continuation" for the let declaration, if the application is inlined, it will also be simplified.

            Note: inlineApp? did not use to be in this mutually recursive declaration. It used to be invoked by simp, and would return Option Code that would be then simplified by simp. However, this simpler architecture produced an exponential blowup in when processing functions such as Lean.Elab.Deriving.Ord.mkMatch.mkAlts. The key problem is that when inlining a declaration we often can reduce the number of exit points by simplified the inlined code, and then connecting the result to the continuation k. However, this optimization is only possible if we simplify the inlined code before we attach it to the continuation.