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
Try to inline a join point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
Equations
- Lean.Compiler.LCNF.Simp.elimVar? value = match value with | Lean.Compiler.LCNF.LetValue.fvar fvarId #[] => pure (some fvarId) | x => pure none
Instances For
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.
Simplify the given local function declaration.
Try to simplify cases of constructor
Simplify code