Add explicit boxing and unboxing instructions. Recall that the Lean to λ_pure compiler produces code without these instructions.
Assumptions:
- This transformation is applied before explicit RC instructions (
inc
,dec
) are inserted. - This transformation is applied before
FnBody.case
has been simplified andAlt.default
is used. Reason: if there is noAlt.default
branch, then we can decide whetherx
atFnBody.case x alts
is an enumeration type by simply inspecting theCtorInfo
values atalts
. - This transformation is applied before lower level optimizations are applied which use
Expr.isShared
,Expr.isTaggedPtr
, andFnBody.set
. - This transformation is applied after
reset
andreuse
instructions have been added. Reason:resetreuse.lean
ignoresbox
andunbox
instructions.
Equations
Instances For
Equations
Instances For
Infer scrutinee type using case
alternatives.
This can be done whenever alts
does not contain an Alt.default _
value.
Equations
Instances For
- f : FunId
- localCtx : LocalContext
- resultType : IRType
- env : Environment
Instances For
- nextIdx : Index
We create auxiliary declarations when boxing constant and literals. The idea is to avoid code such as
let x1 := Uint64.inhabited; let x2 := box x1; ...
We currently do not cache these declarations in an environment extension, but we use auxDeclCache to avoid creating equivalent auxiliary declarations more than once when processing the same IR declaration.
- nextAuxId : Nat
Instances For
Equations
Instances For
@[inline]
def
Lean.IR.ExplicitBoxing.withJDecl
{α : Type}
(j : JoinPointId)
(xs : Array Param)
(v : FnBody)
(k : M α)
:
M α