Documentation

Lean.Compiler.IR.Boxing

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

Equations

Lean.IR.ExplicitBoxing.mkBoxedName n = Lean.Name.mkStr n "_boxed"

def Lean.IR.ExplicitBoxing.isBoxedName:

Lean.Name → Bool

Equations

Lean.IR.ExplicitBoxing.isBoxedName _fun_discr = match _fun_discr with | Lean.Name.str a "_boxed" a_1 => true | x => false

@[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) :

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

Equations

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

def Lean.IR.ExplicitBoxing.mkBoxedVersion (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

Equations

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

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

Equations

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

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

Equations

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

structure Lean.IR.ExplicitBoxing.BoxingContext:

Type

structure Lean.IR.ExplicitBoxing.BoxingState:

Type

nextIdx : Lean.IR.Index
auxDecls : Array Lean.IR.Decl
auxDeclCache : Std.AssocList Lean.IR.FnBody Lean.IR.Expr
nextAuxId : Nat

@[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

Equations

Lean.IR.ExplicitBoxing.getEnv = Lean.IR.ExplicitBoxing.BoxingContext.env <$> read

def Lean.IR.ExplicitBoxing.getLocalContext:

Lean.IR.ExplicitBoxing.M Lean.IR.LocalContext

Equations

Lean.IR.ExplicitBoxing.getLocalContext = Lean.IR.ExplicitBoxing.BoxingContext.localCtx <$> read

def Lean.IR.ExplicitBoxing.getResultType:

Lean.IR.ExplicitBoxing.M Lean.IR.IRType

Equations

Lean.IR.ExplicitBoxing.getResultType = Lean.IR.ExplicitBoxing.BoxingContext.resultType <$> read

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

Lean.IR.ExplicitBoxing.M Lean.IR.IRType

Equations

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

def Lean.IR.ExplicitBoxing.getJPParams (j : Lean.IR.JoinPointId) :

Lean.IR.ExplicitBoxing.M (Array Lean.IR.Param)

Equations

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

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

Lean.IR.ExplicitBoxing.M Lean.IR.Decl

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

@[inline]

def Lean.IR.ExplicitBoxing.withParams {α : Type} (xs : Array Lean.IR.Param) (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.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 α

Equations

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

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

Lean.IR.ExplicitBoxing.M Lean.IR.Expr

Equations

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

@[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 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

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

Equations

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

@[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

Equations

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

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.

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)

Equations

Lean.IR.explicitBoxing decls = do let env ← Lean.IR.getEnv pure (Lean.IR.ExplicitBoxing.run env decls)