inductive Lean.IR.ToIR.FVarClassification : Type

• var (id : VarId) : FVarClassification
• joinPoint (id : JoinPointId) : FVarClassification
• erased : FVarClassification

structure Lean.IR.ToIR.BuilderState : Type

• fvars : Std.HashMap FVarId FVarClassification
• nextId : Nat

@[reducible, inline]

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

Equations

• Lean.IR.ToIR.M = StateRefT' IO.RealWorld Lean.IR.ToIR.BuilderState Lean.CoreM

def Lean.IR.ToIR.M.run {α : Type} (x : M α) : CoreM α

Equations

• x.run = StateRefT'.run' x { }

def Lean.IR.ToIR.bindVar (fvarId : FVarId) : M VarId

Equations

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

def Lean.IR.ToIR.bindVarToVarId (fvarId : FVarId) (varId : VarId) : M Unit

Equations

• Lean.IR.ToIR.bindVarToVarId fvarId varId = modify fun (s : Lean.IR.ToIR.BuilderState) => { fvars := s.fvars.insertIfNew fvarId (Lean.IR.ToIR.FVarClassification.var varId), nextId := s.nextId }

def Lean.IR.ToIR.newVar : M VarId

Equations

• Lean.IR.ToIR.newVar = modifyGet fun (s : Lean.IR.ToIR.BuilderState) => let varId := { idx := s.nextId }; (varId, { fvars := s.fvars, nextId := s.nextId + 1 })

def Lean.IR.ToIR.bindJoinPoint (fvarId : FVarId) : M JoinPointId

Equations

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

def Lean.IR.ToIR.bindErased (fvarId : FVarId) : M Unit

Equations

• Lean.IR.ToIR.bindErased fvarId = modify fun (s : Lean.IR.ToIR.BuilderState) => { fvars := s.fvars.insertIfNew fvarId Lean.IR.ToIR.FVarClassification.erased, nextId := s.nextId }

def Lean.IR.ToIR.findDecl (n : Name) : M (Option Decl)

Equations

• Lean.IR.ToIR.findDecl n = do let __do_lift ← Lean.getEnv pure (Lean.IR.findEnvDecl __do_lift n)

def Lean.IR.ToIR.addDecl (d : Decl) : M Unit

Equations

• Lean.IR.ToIR.addDecl d = Lean.modifyEnv fun (env : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Lean.IR.declMapExt (env.addExtraName d.name) d

def Lean.IR.ToIR.lowerLitValue (v : Compiler.LCNF.LitValue) : LitVal

Equations

• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.nat n) = Lean.IR.LitVal.num n
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.str s) = Lean.IR.LitVal.str s
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint8 v_2) = Lean.IR.LitVal.num v_2.toNat
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint16 v_2) = Lean.IR.LitVal.num v_2.toNat
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint32 v_2) = Lean.IR.LitVal.num v_2.toNat
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint64 v_2) = Lean.IR.LitVal.num v_2.toNat
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.usize v_2) = Lean.IR.LitVal.num v_2.toNat

def Lean.IR.ToIR.lowerEnumToScalarType (name : Name) : M (Option IRType)

Equations

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

def Lean.IR.ToIR.lowerType (e : Lean.Expr) : M IRType

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ToIR.lowerType (Lean.Expr.const `UInt8 us) = pure Lean.IR.IRType.uint8
• Lean.IR.ToIR.lowerType (Lean.Expr.const `Bool us) = pure Lean.IR.IRType.uint8
• Lean.IR.ToIR.lowerType (Lean.Expr.const `UInt16 us) = pure Lean.IR.IRType.uint16
• Lean.IR.ToIR.lowerType (Lean.Expr.const `UInt32 us) = pure Lean.IR.IRType.uint32
• Lean.IR.ToIR.lowerType (Lean.Expr.const `UInt64 us) = pure Lean.IR.IRType.uint64
• Lean.IR.ToIR.lowerType (Lean.Expr.const `USize us) = pure Lean.IR.IRType.usize
• Lean.IR.ToIR.lowerType (Lean.Expr.const `Float us) = pure Lean.IR.IRType.float
• Lean.IR.ToIR.lowerType (Lean.Expr.const `Float32 us) = pure Lean.IR.IRType.float32
• Lean.IR.ToIR.lowerType (Lean.Expr.const `lcErased us) = pure Lean.IR.IRType.irrelevant
• Lean.IR.ToIR.lowerType (Lean.Expr.forallE binderName binderType body binderInfo) = pure Lean.IR.IRType.object
• Lean.IR.ToIR.lowerType e = panicWithPosWithDecl "Lean.Compiler.IR.ToIR" "Lean.IR.ToIR.lowerType" 121 9 "invalid type"

def Lean.IR.ToIR.getCtorInfo (name : Name) : M (CtorInfo × Array CtorFieldInfo)

Equations

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

def Lean.IR.ToIR.lowerArg (a : Compiler.LCNF.Arg) : M Arg

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ToIR.lowerArg Lean.Compiler.LCNF.Arg.erased = pure Lean.IR.Arg.irrelevant
• Lean.IR.ToIR.lowerArg (Lean.Compiler.LCNF.Arg.type expr) = pure Lean.IR.Arg.irrelevant

inductive Lean.IR.ToIR.TranslatedProj : Type

• expr (e : Expr) : TranslatedProj
• erased : TranslatedProj

instance Lean.IR.ToIR.instInhabitedTranslatedProj : Inhabited TranslatedProj

Equations

• Lean.IR.ToIR.instInhabitedTranslatedProj = { default := Lean.IR.ToIR.TranslatedProj.expr default }

def Lean.IR.ToIR.lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo) : TranslatedProj × IRType

Equations

• Lean.IR.ToIR.lowerProj base ctorInfo (Lean.IR.CtorFieldInfo.object i) = (Lean.IR.ToIR.TranslatedProj.expr (Lean.IR.Expr.proj i base), Lean.IR.IRType.object)
• Lean.IR.ToIR.lowerProj base ctorInfo (Lean.IR.CtorFieldInfo.usize i) = (Lean.IR.ToIR.TranslatedProj.expr (Lean.IR.Expr.uproj i base), Lean.IR.IRType.usize)
• Lean.IR.ToIR.lowerProj base ctorInfo (Lean.IR.CtorFieldInfo.scalar sz offset irType) = (Lean.IR.ToIR.TranslatedProj.expr (Lean.IR.Expr.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType)
• Lean.IR.ToIR.lowerProj base ctorInfo Lean.IR.CtorFieldInfo.irrelevant = (Lean.IR.ToIR.TranslatedProj.erased, Lean.IR.IRType.irrelevant)

def Lean.IR.ToIR.lowerParam (p : Compiler.LCNF.Param) : M Param

Equations

• Lean.IR.ToIR.lowerParam p = do let x ← Lean.IR.ToIR.bindVar p.fvarId let ty ← Lean.IR.ToIR.lowerType p.type pure { x := x, borrow := p.borrow, ty := ty }

partial def Lean.IR.ToIR.lowerCode (c : Compiler.LCNF.Code) : M FnBody

partial def Lean.IR.ToIR.lowerLet (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) : M FnBody

partial def Lean.IR.ToIR.lowerLet.mkVar (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (v : VarId) : M FnBody

partial def Lean.IR.ToIR.lowerLet.mkExpr (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (e : Expr) : M FnBody

partial def Lean.IR.ToIR.lowerLet.mkErased (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) : Unit → M FnBody

partial def Lean.IR.ToIR.lowerLet.mkPartialApp (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (e : Expr) (restArgs : Array Arg) : M FnBody

partial def Lean.IR.ToIR.lowerLet.tryIrDecl? (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (name : Name) (args : Array Arg) : M (Option FnBody)

partial def Lean.IR.ToIR.lowerLet.lowerNonObjectFields (k : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (fields : Array CtorFieldInfo) (args : Array Compiler.LCNF.Arg) (objVar : VarId) : Unit → M FnBody

partial def Lean.IR.ToIR.lowerLet.lowerNonObjectFields.loop (k : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (fields : Array CtorFieldInfo) (args : Array Compiler.LCNF.Arg) (objVar : VarId) (usizeCount i : Nat) : M FnBody

partial def Lean.IR.ToIR.lowerAlt (discr : VarId) (a : Compiler.LCNF.Alt) : M Alt

partial def Lean.IR.ToIR.lowerAlt.loop (discr : VarId) (code : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (params : Array Compiler.LCNF.Param) (fields : Array CtorFieldInfo) (i : Nat) : M FnBody

def Lean.IR.ToIR.lowerResultType (type : Lean.Expr) (arity : Nat) : M IRType

Equations

• Lean.IR.ToIR.lowerResultType type arity = Lean.IR.ToIR.lowerType (Lean.IR.ToIR.lowerResultType.resultTypeForArity type arity)

def Lean.IR.ToIR.lowerResultType.resultTypeForArity (type : Lean.Expr) (arity : Nat) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ToIR.lowerResultType.resultTypeForArity (Lean.Expr.const `lcErased us) arity = if (arity == 0) = true then Lean.Expr.const `lcErased us else Lean.mkConst `lcErased

def Lean.IR.ToIR.lowerDecl (d : Compiler.LCNF.Decl) : M (Option Decl)

Equations

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

def Lean.IR.toIR (decls : Array Compiler.LCNF.Decl) : CoreM (Array Decl)

Equations

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