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.DerivedValInfo : Type

• parent? : Option VarId
• children : VarIdSet

def Lean.IR.ExplicitRC.instInhabitedDerivedValInfo.default : DerivedValInfo

instance Lean.IR.ExplicitRC.instInhabitedDerivedValInfo : Inhabited DerivedValInfo

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.DerivedValMap : Type

structure Lean.IR.ExplicitRC.CollectDerivedValInfo.State : Type

• varMap : DerivedValMap
• borrowedParams : VarIdSet

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.CollectDerivedValInfo.M (α : Type) : Type

structure Lean.IR.ExplicitRC.VarInfo : Type

• isPossibleRef : Bool
• isDefiniteRef : Bool
• persistent : Bool

def Lean.IR.ExplicitRC.instInhabitedVarInfo.default : VarInfo

instance Lean.IR.ExplicitRC.instInhabitedVarInfo : Inhabited VarInfo

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.VarMap : Type

structure Lean.IR.ExplicitRC.LiveVars : Type

• vars : VarIdSet
• borrows : VarIdSet

def Lean.IR.ExplicitRC.instInhabitedLiveVars.default : LiveVars

instance Lean.IR.ExplicitRC.instInhabitedLiveVars : Inhabited LiveVars

@[inline]

def Lean.IR.ExplicitRC.LiveVars.merge (liveVars1 liveVars2 : LiveVars) : LiveVars

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.JPLiveVarMap : Type

structure Lean.IR.ExplicitRC.Context : Type

• env : Environment
• decls : Array Decl
• borrowedParams : VarIdSet
• derivedValMap : DerivedValMap
• 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) : LiveVars

@[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 (b : FnBody) (ctx : Context) : FnBody × LiveVars

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

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