# 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 : Decl
- params : FVarIdSet

Instances For

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

- used : FVarIdHashSet

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 : FVarId) :
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 : Arg) :
FindUsedM Unit
Equations

- Lean.Compiler.LCNF.FindUsed.visitArg Lean.Compiler.LCNF.Arg.erased = pure ()
- Lean.Compiler.LCNF.FindUsed.visitArg (Lean.Compiler.LCNF.Arg.type expr) = pure ()
- Lean.Compiler.LCNF.FindUsed.visitArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.FindUsed.visitFVar fvarId

Instances For

source
def Lean.Compiler.LCNF.FindUsed.visitLetValue (e : LetValue) :
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.lit 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 : Code) :
FindUsedM Unit
source
def Lean.Compiler.LCNF.FindUsed.collectUsedParams (decl : Decl) :
CompilerM FVarIdHashSet
Equations

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

Instances For

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

- declName : Name
- auxDeclName : 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 : Code) :
ReduceM Code
source
def Lean.Compiler.LCNF.Decl.reduceArity (decl : Decl) :
CompilerM (Array Decl)
Equations

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

Instances For

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

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

Instances For