source
def Lean.Compiler.LCNF.Simp.specializePartialApp (info : InlineCandidateInfo) :
SimpM FunDecl

Create a new local function declaration when `info.args.size < info.params.size`. We use this function to inline/specialize a partial application of a local function.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.inlineJp? (fvarId : FVarId) (args : Array Arg) :
SimpM (Option Code)

Try to inline a join point.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.etaPolyApp? (letDecl : LetDecl) :
OptionT SimpM FunDecl

When the configuration flag `etaPoly = true`, we eta-expand partial applications of functions that take local instances as arguments. This kind of function is inlined or specialized, and we create new simplification opportunities by eta-expanding them.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.isReturnOf (c : Code) (fvarId : FVarId) :
SimpM Bool

Similar to `Code.isReturnOf`, but taking the current substitution into account.

Equations

- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.Simp.isReturnOf c fvarId = pure false

Instances For

source
def Lean.Compiler.LCNF.Simp.elimVar? (value : LetValue) :
SimpM (Option FVarId)
Equations

- Lean.Compiler.LCNF.Simp.elimVar? value = match value with | Lean.Compiler.LCNF.LetValue.fvar fvarId #[] => pure (some fvarId) | x => pure none

Instances For

source
partial def Lean.Compiler.LCNF.Simp.inlineApp? (letDecl : LetDecl) (k : Code) :
SimpM (Option Code)

If the value of the given let-declaration is an application that can be inlined, inline it and simplify the result.

`k` is the "continuation" for the let declaration, if the application is inlined, it will also be simplified.

Note: `inlineApp?` did not use to be in this mutually recursive declaration. It used to be invoked by `simp`, and would return `Option Code` that would be then simplified by `simp`. However, this simpler architecture produced an exponential blowup in when processing functions such as `Lean.Elab.Deriving.Ord.mkMatch.mkAlts`. The key problem is that when inlining a declaration we often can reduce the number of exit points by simplified the inlined code, and then connecting the result to the continuation `k`. However, this optimization is only possible if we simplify the inlined code before we attach it to the continuation.

source
partial def Lean.Compiler.LCNF.Simp.simpFunDecl (decl : FunDecl) :
SimpM FunDecl

Simplify the given local function declaration.

source
partial def Lean.Compiler.LCNF.Simp.simpCasesOnCtor? (cases : Cases) :
SimpM (Option Code)

Try to simplify `cases` of `constructor`

source
partial def Lean.Compiler.LCNF.Simp.simp (code : Code) :
SimpM Code

Simplify `code`