structure Lean.IR.ToIR.BuilderState : Type

• vars : Std.HashMap FVarId Arg
• joinPoints : Std.HashMap FVarId JoinPointId
• nextId : Nat
• subst : Compiler.LCNF.FVarSubst

  We keep around a substitution here because we run a second trivial structure elimination when converting to IR. This elimination is aware of the fact that Void is irrelevant while the first one in LCNF isn't because LCNF is still pure. However, IR does not allow us to have bindings of the form let x := y which might occur when for example projecting out of a trivial structure where previously a binding would've been let x := proj y i and now becomes let x := y. For this reason we carry around these kinds of bindings in this substitution and apply it whenever we access an fvar in the conversion.

@[reducible, inline]

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

Equations

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

instance Lean.IR.ToIR.instMonadFVarSubstMFalse : Compiler.LCNF.MonadFVarSubst M false

Equations

• Lean.IR.ToIR.instMonadFVarSubstMFalse = { getSubst := do let __do_lift ← get pure __do_lift.subst }

instance Lean.IR.ToIR.instMonadFVarSubstStateM : Compiler.LCNF.MonadFVarSubstState M

Equations

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

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

Equations

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

def Lean.IR.ToIR.getFVarValue (fvarId : FVarId) : M Arg

Equations

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

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

Equations

• Lean.IR.ToIR.getJoinPointValue fvarId = do let __do_lift ← get pure (__do_lift.joinPoints.get! fvarId)

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

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

def Lean.IR.ToIR.newVar : M VarId

Equations

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

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

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

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

• Lean.IR.ToIR.lowerArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.IR.ToIR.getFVarValue fvarId
• 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

def Lean.IR.ToIR.instInhabitedTranslatedProj.default : TranslatedProj

Equations

• Lean.IR.ToIR.instInhabitedTranslatedProj.default = Lean.IR.ToIR.TranslatedProj.expr default

instance Lean.IR.ToIR.instInhabitedTranslatedProj : Inhabited TranslatedProj

Equations

• Lean.IR.ToIR.instInhabitedTranslatedProj = { default := Lean.IR.ToIR.instInhabitedTranslatedProj.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)
• Lean.IR.ToIR.lowerProj base ctorInfo Lean.IR.CtorFieldInfo.void = (Lean.IR.ToIR.TranslatedProj.erased, Lean.IR.IRType.void)

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

Equations

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

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.