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
- Lean.IR.ExplicitBoxing.mkBoxedName n = Lean.Name.mkStr n "_boxed"
Equations
- Lean.IR.ExplicitBoxing.isBoxedName name = match name with | Lean.Name.str pre "_boxed" => true | x => false
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- One or more equations did not get rendered due to their size.
Infer scrutinee type using case
alternatives.
This can be done whenever alts
does not contain an Alt.default _
value.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.IR.ExplicitBoxing.eqvTypes t₁ t₂ = (Lean.IR.IRType.isScalar t₁ == Lean.IR.IRType.isScalar t₂ && (!Lean.IR.IRType.isScalar t₁ || t₁ == t₂))
- f : Lean.IR.FunId
- localCtx : Lean.IR.LocalContext
- resultType : Lean.IR.IRType
- decls : Array Lean.IR.Decl
- env : Lean.Environment
Instances For
- nextIdx : Lean.IR.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.
auxDecls : Array Lean.IR.Decl- auxDeclCache : Lean.AssocList Lean.IR.FnBody Lean.IR.Expr
- nextAuxId : Nat
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.IR.ExplicitBoxing.getDecl fid = do let ctx ← read match Lean.IR.findEnvDecl' ctx.env fid ctx.decls with | some decl => pure decl | none => pure default
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Auxiliary function used by castVarIfNeeded.
It is used when the expected type does not match xType
.
If xType
is scalar, then we need to "box" it. Otherwise, we need to "unbox" it.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.IR.ExplicitBoxing.castArgIfNeeded x expected k = match x with | Lean.IR.Arg.var x => Lean.IR.ExplicitBoxing.castVarIfNeeded x expected fun x => k (Lean.IR.Arg.var x) | x => k x
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.IR.explicitBoxing decls = do let env ← Lean.IR.getEnv pure (Lean.IR.ExplicitBoxing.run env decls)