Documentation

Lean.Compiler.LCNF.ReduceArity

Function arity reduction #

This module finds "used" parameters in a declaration, and then create an auxliary declaration that contains only used parameters. For example:

def f (x y : Nat) : Nat :=
  let _x.1 := Nat.add x x
  let _x.2 := Nat.mul _x.1 _x.1
  _x.2

is converted into

def f._rarg (x : Nat) : Nat :=
  let _x.1 := Nat.add x x
  let _x.2 := Nat.mul _x.1 _x.1
  _x.2
def f (x y : Nat) : Nat :=
  let _x.1 := f._rarg x
  _x.1

Note that any f full application is going to be inlined in the next simp pass.

This module has basic support for detecting "unused" variables in recursive definitions. For example, the y in the following definition in correctly treated as "unused"

def f (x y : Nat) : Nat :=
  cases x
  | zero => x
  | succ _x.1 =>
    let _x.2 := f _x.1 y
    let _x.3 := Nat.mul _x.2 _x.2
    _x.3

This module does not have similar support for mutual recursive applications. We assume this limitation is irrelevant in practice.

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