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 and Alt.default is used. Reason: if there is no Alt.default branch, then we can decide whether x at FnBody.case x alts is an enumeration type by simply inspecting the CtorInfo values at alts.
• This transformation is applied before lower level optimizations are applied which use Expr.isShared, Expr.isTaggedPtr, and FnBody.set.
• This transformation is applied after reset and reuse instructions have been added. Reason: resetreuse.lean ignores box and unbox instructions.

def Lean.IR.ExplicitBoxing.mkBoxedName (n : Lean.Name) : Lean.Name

def Lean.IR.ExplicitBoxing.isBoxedName (name : Lean.Name) : Bool

@[reducible, inline]

abbrev Lean.IR.ExplicitBoxing.N (α : Type) : Type

Equations

• Lean.IR.ExplicitBoxing.N = StateM Nat

def Lean.IR.ExplicitBoxing.requiresBoxedVersion (env : Lean.Environment) (decl : Lean.IR.Decl) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.ExplicitBoxing.mkBoxedVersionAux (decl : Lean.IR.Decl) : Lean.IR.ExplicitBoxing.N Lean.IR.Decl

def Lean.IR.ExplicitBoxing.mkBoxedVersion (decl : Lean.IR.Decl) : Lean.IR.Decl

Equations

• Lean.IR.ExplicitBoxing.mkBoxedVersion decl = StateT.run' (Lean.IR.ExplicitBoxing.mkBoxedVersionAux decl) 1

def Lean.IR.ExplicitBoxing.addBoxedVersions (env : Lean.Environment) (decls : Array Lean.IR.Decl) : Array Lean.IR.Decl

def Lean.IR.ExplicitBoxing.getScrutineeType (alts : Array Lean.IR.Alt) : Lean.IR.IRType

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.

def Lean.IR.ExplicitBoxing.eqvTypes (t₁ t₂ : Lean.IR.IRType) : Bool

Equations

• Lean.IR.ExplicitBoxing.eqvTypes t₁ t₂ = (t₁.isScalar == t₂.isScalar && (!t₁.isScalar || t₁ == t₂))

structure Lean.IR.ExplicitBoxing.BoxingContext : Type

• f : Lean.IR.FunId
• localCtx : Lean.IR.LocalContext
• resultType : Lean.IR.IRType
• decls : Array Lean.IR.Decl
• env : Lean.Environment

structure Lean.IR.ExplicitBoxing.BoxingState : Type

• nextIdx : Lean.IR.Index
• auxDecls : Array Lean.IR.Decl

  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.

• auxDeclCache : Lean.AssocList Lean.IR.FnBody Lean.IR.Expr
• nextAuxId : Nat

@[reducible, inline]

abbrev Lean.IR.ExplicitBoxing.M (α : Type) : Type

Equations

• Lean.IR.ExplicitBoxing.M = ReaderT Lean.IR.ExplicitBoxing.BoxingContext (StateT Lean.IR.ExplicitBoxing.BoxingState Id)

def Lean.IR.ExplicitBoxing.getEnv : Lean.IR.ExplicitBoxing.M Lean.Environment

def Lean.IR.ExplicitBoxing.getLocalContext : Lean.IR.ExplicitBoxing.M Lean.IR.LocalContext

def Lean.IR.ExplicitBoxing.getResultType : Lean.IR.ExplicitBoxing.M Lean.IR.IRType

def Lean.IR.ExplicitBoxing.getVarType (x : Lean.IR.VarId) : Lean.IR.ExplicitBoxing.M Lean.IR.IRType

Equations

• Lean.IR.ExplicitBoxing.getVarType x = do let localCtx ← Lean.IR.ExplicitBoxing.getLocalContext match localCtx.getType x with | some t => pure t | none => pure Lean.IR.IRType.object

def Lean.IR.ExplicitBoxing.getJPParams (j : Lean.IR.JoinPointId) : Lean.IR.ExplicitBoxing.M (Array Lean.IR.Param)

Equations

• Lean.IR.ExplicitBoxing.getJPParams j = do let localCtx ← Lean.IR.ExplicitBoxing.getLocalContext match localCtx.getJPParams j with | some ys => pure ys | none => pure #[]

def Lean.IR.ExplicitBoxing.getDecl (fid : Lean.IR.FunId) : Lean.IR.ExplicitBoxing.M Lean.IR.Decl

@[inline]

def Lean.IR.ExplicitBoxing.withParams {α : Type} (xs : Array Lean.IR.Param) (k : Lean.IR.ExplicitBoxing.M α) : Lean.IR.ExplicitBoxing.M α

@[inline]

def Lean.IR.ExplicitBoxing.withVDecl {α : Type} (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (v : Lean.IR.Expr) (k : Lean.IR.ExplicitBoxing.M α) : Lean.IR.ExplicitBoxing.M α

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.IR.ExplicitBoxing.withJDecl {α : Type} (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (v : Lean.IR.FnBody) (k : Lean.IR.ExplicitBoxing.M α) : Lean.IR.ExplicitBoxing.M α

def Lean.IR.ExplicitBoxing.mkCast (x : Lean.IR.VarId) (xType expectedType : Lean.IR.IRType) : Lean.IR.ExplicitBoxing.M Lean.IR.Expr

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.

@[inline]

def Lean.IR.ExplicitBoxing.castVarIfNeeded (x : Lean.IR.VarId) (expected : Lean.IR.IRType) (k : Lean.IR.VarId → Lean.IR.ExplicitBoxing.M Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.IR.ExplicitBoxing.castArgIfNeeded (x : Lean.IR.Arg) (expected : Lean.IR.IRType) (k : Lean.IR.Arg → Lean.IR.ExplicitBoxing.M Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

Equations

• Lean.IR.ExplicitBoxing.castArgIfNeeded (Lean.IR.Arg.var x_2) expected k = Lean.IR.ExplicitBoxing.castVarIfNeeded x_2 expected fun (x : Lean.IR.VarId) => k (Lean.IR.Arg.var x)
• Lean.IR.ExplicitBoxing.castArgIfNeeded x expected k = k x

def Lean.IR.ExplicitBoxing.castArgsIfNeededAux (xs : Array Lean.IR.Arg) (typeFromIdx : Nat → Lean.IR.IRType) : Lean.IR.ExplicitBoxing.M (Array Lean.IR.Arg × Array Lean.IR.FnBody)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.IR.ExplicitBoxing.castArgsIfNeeded (xs : Array Lean.IR.Arg) (ps : Array Lean.IR.Param) (k : Array Lean.IR.Arg → Lean.IR.ExplicitBoxing.M Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

@[inline]

def Lean.IR.ExplicitBoxing.boxArgsIfNeeded (xs : Array Lean.IR.Arg) (k : Array Lean.IR.Arg → Lean.IR.ExplicitBoxing.M Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.ExplicitBoxing.unboxResultIfNeeded (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

def Lean.IR.ExplicitBoxing.castResultIfNeeded (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (eType : Lean.IR.IRType) (b : Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.ExplicitBoxing.visitVDeclExpr (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody) : Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ExplicitBoxing.visitVDeclExpr x ty e b = pure (Lean.IR.FnBody.vdecl x ty e b)

partial def Lean.IR.ExplicitBoxing.visitFnBody : Lean.IR.FnBody → Lean.IR.ExplicitBoxing.M Lean.IR.FnBody

def Lean.IR.ExplicitBoxing.run (env : Lean.Environment) (decls : Array Lean.IR.Decl) : Array Lean.IR.Decl

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.explicitBoxing (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM (Array Lean.IR.Decl)