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.

structure Lean.Compiler.LCNF.FindUsed.Context : Type

• decl : Lean.Compiler.LCNF.Decl
• params : Lean.FVarIdSet

structure Lean.Compiler.LCNF.FindUsed.State : Type

• used : Lean.FVarIdSet

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FindUsed.FindUsedM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.FindUsed.FindUsedM = ReaderT Lean.Compiler.LCNF.FindUsed.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.FindUsed.State Lean.Compiler.LCNF.CompilerM)

def Lean.Compiler.LCNF.FindUsed.visitFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.FindUsed.FindUsedM Unit

Equations

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

def Lean.Compiler.LCNF.FindUsed.visitArg (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.FindUsed.FindUsedM Unit

Equations

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

def Lean.Compiler.LCNF.FindUsed.visitLetValue (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.FindUsed.FindUsedM Unit

Equations

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

partial def Lean.Compiler.LCNF.FindUsed.visit (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.FindUsed.FindUsedM Unit

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.

structure Lean.Compiler.LCNF.ReduceArity.Context : Type

• declName : Lake.Name
• auxDeclName : Lake.Name
• paramMask : Array Bool

@[inline, reducible]

abbrev Lean.Compiler.LCNF.ReduceArity.ReduceM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ReduceArity.ReduceM = ReaderT Lean.Compiler.LCNF.ReduceArity.Context Lean.Compiler.LCNF.CompilerM

partial def Lean.Compiler.LCNF.ReduceArity.reduce (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.ReduceArity.ReduceM Lean.Compiler.LCNF.Code

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.

def Lean.Compiler.LCNF.reduceArity : Lean.Compiler.LCNF.Pass

Equations

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