- liftInstParamOnly : BoolIf liftInstParamOnlyistrue, then only local functions that take local instances as parameters are lambda lifted.
- suffix : Lake.NameSuffix for the new auxiliary declarations being created. 
- mainDecl : Lean.Compiler.LCNF.DeclDeclaration where lambda lifting is being applied. We use it to provide the "base name" for auxiliary declarations and the flag safe.
- inheritInlineAttrs : BoolIf true, the lambda-lifted functions inherit the inline attribute from mainDecl. We use this feature to implement@[inline] instance ...and@[always_inline] instance ...
- minSize : NatOnly local functions with size > minSizeare lambda lifted. We use this feature to implement@[inline] instance ...and@[always_inline] instance ...
Context for the LiftM monad.
Instances For
- decls : Array Lean.Compiler.LCNF.DeclNew auxiliary declarations 
- nextIdx : NatNext index for generating auxiliary declaration name. 
State for the LiftM monad.
Instances For
Monad for applying lambda lifting.
Instances For
Return true if the given declaration takes a local instance as a parameter.
We lambda lift this kind of local function declaration before specialization.
Instances For
Return true if the given declaration should be lambda lifted.
Instances For
Create a new auxiliary declaration. The array closure contains all free variables
occurring in decl.
Instances For
Instances For
Instances For
Eliminate all local function declarations.
Instances For
During eager lambda lifting, we lift
- All local function declarations from instances (motivation: make sure it is cheap to inline them later)
- Local function declarations that take local instances as parameters (motivation: ensure they are specialized)