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

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

Instances For

source

structure Lean.Compiler.LCNF.FindUsed.State :

Type

used : Lean.FVarIdSet

Instances For

source

@[reducible, inline]

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)

Instances For

source

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.

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

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.FindUsed.visitLetValue Lean.Compiler.LCNF.LetValue.erased = pure ()
Lean.Compiler.LCNF.FindUsed.visitLetValue (Lean.Compiler.LCNF.LetValue.value value) = pure ()
Lean.Compiler.LCNF.FindUsed.visitLetValue (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId) = Lean.Compiler.LCNF.FindUsed.visitFVar fvarId
Lean.Compiler.LCNF.FindUsed.visitLetValue (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = do Lean.Compiler.LCNF.FindUsed.visitFVar fvarId Array.forM Lean.Compiler.LCNF.FindUsed.visitArg args

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

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

Instances For

source

@[reducible, inline]

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

Type

Equations

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

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