Insert explicit RC instructions. So, it assumes the input code does not contain inc nor dec instructions. This transformation is applied before lower level optimizations that introduce the instructions release and set

structure Lean.IR.ExplicitRC.VarInfo : Type

• ref : Bool
• persistent : Bool
• consume : Bool

instance Lean.IR.ExplicitRC.instInhabitedVarInfo : Inhabited Lean.IR.ExplicitRC.VarInfo

Equations

• Lean.IR.ExplicitRC.instInhabitedVarInfo = { default := { ref := default, persistent := default, consume := default } }

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.VarMap : Type

structure Lean.IR.ExplicitRC.Context : Type

• env : Lean.Environment
• decls : Array Lean.IR.Decl
• varMap : Lean.IR.ExplicitRC.VarMap
• jpLiveVarMap : Lean.IR.JPLiveVarMap
• localCtx : Lean.IR.LocalContext

def Lean.IR.ExplicitRC.getDecl (ctx : Lean.IR.ExplicitRC.Context) (fid : Lean.IR.FunId) : Lean.IR.Decl

def Lean.IR.ExplicitRC.getVarInfo (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) : Lean.IR.ExplicitRC.VarInfo

Equations

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

def Lean.IR.ExplicitRC.getJPParams (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) : Array Lean.IR.Param

def Lean.IR.ExplicitRC.getJPLiveVars (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) : Lean.IR.LiveVarSet

def Lean.IR.ExplicitRC.mustConsume (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) : Bool

Equations

• Lean.IR.ExplicitRC.mustConsume ctx x = ((Lean.IR.ExplicitRC.getVarInfo ctx x).ref && (Lean.IR.ExplicitRC.getVarInfo ctx x).consume)

@[inline]

def Lean.IR.ExplicitRC.addInc (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) (n : Nat := 1) : Lean.IR.FnBody

@[inline]

def Lean.IR.ExplicitRC.addDec (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.ExplicitRC.addDec ctx x b = Lean.IR.FnBody.dec x 1 true (Lean.IR.ExplicitRC.getVarInfo ctx x).persistent b

def Lean.IR.ExplicitRC.updateVarInfoWithParams (ctx : Lean.IR.ExplicitRC.Context) (ps : Array Lean.IR.Param) : Lean.IR.ExplicitRC.Context

Equations

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

partial def Lean.IR.ExplicitRC.visitFnBody : Lean.IR.FnBody → Lean.IR.ExplicitRC.Context → Lean.IR.FnBody × Lean.IR.LiveVarSet

def Lean.IR.ExplicitRC.visitDecl (env : Lean.Environment) (decls : Array Lean.IR.Decl) (d : Lean.IR.Decl) : Lean.IR.Decl

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ExplicitRC.visitDecl env decls d = d

def Lean.IR.explicitRC (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM (Array Lean.IR.Decl)