This pass is responsible for inserting box and unbox instructions and generally attempts to make the IR actually type correct. After this pass is the first time where we can generally assume type information to actually be correct in the entirety of LCNF. Furthermore, it also generates boxed versions of functions if required. They take all arguments as [t]object/tagged and return a [t]object/tagged. These functions are used by the interpreter and when allocating closures.

This pass does not support: isShared, inc, dec, set, setTag and del.

def Lean.Compiler.LCNF.addBoxedVersions (decls : Array (Decl Purity.impure)) : CompilerM (Array (Decl Purity.impure))

For all declarations in decls add their _boxed version if required.

Equations

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

def Lean.Compiler.LCNF.explicitBoxing : Pass

Equations

• Lean.Compiler.LCNF.explicitBoxing = { phase := Lean.Compiler.LCNF.Phase.impure, phaseInv := Lean.Compiler.LCNF.explicitBoxing._proof_1✝, name := `boxing, run := Lean.Compiler.LCNF.run✝ }