Documentation

Lean.Compiler.LCNF.ReduceArity

Function arity reduction #

This module finds "used" parameters in a declaration, and then create an auxiliary 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.

source
structure Lean.Compiler.LCNF.FindUsed.Context :
Type
Instances For
    source
    structure Lean.Compiler.LCNF.FindUsed.State :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Compiler.LCNF.FindUsed.FindUsedM (α : Type) :
      Type
      Equations
      Instances For
        source
        def Lean.Compiler.LCNF.FindUsed.visitFVar (fvarId : Lean.FVarId) :
        Lean.Compiler.LCNF.FindUsed.FindUsedM Unit
        Instances For
          source
          def Lean.Compiler.LCNF.FindUsed.visitArg (arg : Lean.Compiler.LCNF.Arg) :
          Lean.Compiler.LCNF.FindUsed.FindUsedM Unit
          Equations
          Instances For
            source
            def Lean.Compiler.LCNF.FindUsed.visitLetValue (e : Lean.Compiler.LCNF.LetValue) :
            Lean.Compiler.LCNF.FindUsed.FindUsedM Unit
            Instances For
              source
              partial def Lean.Compiler.LCNF.FindUsed.visit (code : Lean.Compiler.LCNF.Code) :
              Lean.Compiler.LCNF.FindUsed.FindUsedM Unit
              source
              def Lean.Compiler.LCNF.FindUsed.collectUsedParams (decl : Lean.Compiler.LCNF.Decl) :
              Lean.Compiler.LCNF.CompilerM Lean.FVarIdSet
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                structure Lean.Compiler.LCNF.ReduceArity.Context :
                Type
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Lean.Compiler.LCNF.ReduceArity.ReduceM (α : Type) :
                  Type
                  Instances For
                    source
                    partial def Lean.Compiler.LCNF.ReduceArity.reduce (code : Lean.Compiler.LCNF.Code) :
                    Lean.Compiler.LCNF.ReduceArity.ReduceM Lean.Compiler.LCNF.Code
                    source
                    def Lean.Compiler.LCNF.Decl.reduceArity (decl : Lean.Compiler.LCNF.Decl) :
                    Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Lean.Compiler.LCNF.reduceArity :
                      Lean.Compiler.LCNF.Pass
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For