opaque Lean.IR.ToIR.taggedReturnAttr : TagAttribute

Marks an extern definition to be guaranteed to always return tagged values. This information is used to optimize reference counting in the compiler.

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

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

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

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

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

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

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

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

def Lean.IR.ToIR.newVar : M VarId

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

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

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

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

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

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

inductive Lean.IR.ToIR.TranslatedProj : Type

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

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

instance Lean.IR.ToIR.instInhabitedTranslatedProj : Inhabited TranslatedProj

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

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

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

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

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