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 VarInfo

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.VarMap : Type

structure Lean.IR.ExplicitRC.Context : Type

• env : Environment
• decls : Array Decl
• varMap : VarMap
• jpLiveVarMap : JPLiveVarMap
• localCtx : LocalContext

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

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

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

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

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

@[inline]

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

@[inline]

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

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

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

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

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