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.

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.

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.

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

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

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.

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

Simplify the given local function declaration.

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

Try to simplify cases of constructor

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

Simplify code