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) => have 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 d

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

Equations

• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.nat n) = (Lean.IR.LitVal.num n, if n < UInt32.size then Lean.IR.IRType.tagged else Lean.IR.IRType.tobject)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.str s) = (Lean.IR.LitVal.str s, Lean.IR.IRType.object)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint8 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint8)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint16 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint16)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint32 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint32)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint64 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint64)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.usize v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.usize)

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.erased
• Lean.IR.ToIR.lowerArg (Lean.Compiler.LCNF.Arg.type expr) = pure Lean.IR.Arg.erased

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 irType) = (Lean.IR.ToIR.TranslatedProj.expr (Lean.IR.Expr.proj i base), irType)
• 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.erased = (Lean.IR.ToIR.TranslatedProj.erased, Lean.IR.IRType.erased)

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 ← liftM (Lean.IR.toIRType 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.lowerAlt (discr : VarId) (a : Compiler.LCNF.Alt) : M Alt

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

Equations

• Lean.IR.ToIR.lowerResultType type arity = liftM (Lean.IR.toIRType (Lean.IR.ToIR.lowerResultType.resultTypeForArity✝ type arity))

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.