Context for the LiftM
monad.
- liftInstParamOnly : Bool
If
liftInstParamOnly
istrue
, then only local functions that take local instances as parameters are lambda lifted. - suffix : Name
Suffix for the new auxiliary declarations being created.
- mainDecl : Decl
Declaration where lambda lifting is being applied. We use it to provide the "base name" for auxiliary declarations and the flag
safe
. - inheritInlineAttrs : Bool
If true, the lambda-lifted functions inherit the inline attribute from
mainDecl
. We use this feature to implement@[inline] instance ...
and@[always_inline] instance ...
- minSize : Nat
Only local functions with
size > minSize
are lambda lifted. We use this feature to implement@[inline] instance ...
and@[always_inline] instance ...
Instances For
Monad for applying lambda lifting.
Equations
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.
Equations
Instances For
Return true
if the given declaration should be lambda lifted.
Equations
Instances For
Equations
Instances For
Eliminate all local function declarations.
Equations
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)