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

instance Lean.IR.ExplicitRC.instInhabitedDerivedValInfo : Inhabited DerivedValInfo

Equations

• Lean.IR.ExplicitRC.instInhabitedDerivedValInfo = { default := { parent? := default, children := default } }

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.DerivedValMap : Type

Equations

• Lean.IR.ExplicitRC.DerivedValMap = Std.HashMap Lean.IR.VarId Lean.IR.ExplicitRC.DerivedValInfo

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

• varMap : DerivedValMap
• borrowedParams : VarIdSet

@[reducible, inline]

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

Equations

• Lean.IR.ExplicitRC.CollectDerivedValInfo.M = StateM Lean.IR.ExplicitRC.CollectDerivedValInfo.State

structure Lean.IR.ExplicitRC.VarInfo : Type

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

instance Lean.IR.ExplicitRC.instInhabitedVarInfo : Inhabited VarInfo

Equations

• Lean.IR.ExplicitRC.instInhabitedVarInfo = { default := { isPossibleRef := default, isDefiniteRef := default, persistent := default } }

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.VarMap : Type

Equations

• Lean.IR.ExplicitRC.VarMap = Std.TreeMap Lean.IR.VarId Lean.IR.ExplicitRC.VarInfo fun (x y : Lean.IR.VarId) => compare x.idx y.idx

structure Lean.IR.ExplicitRC.LiveVars : Type

• vars : VarIdSet
• borrows : VarIdSet

instance Lean.IR.ExplicitRC.instInhabitedLiveVars : Inhabited LiveVars

Equations

• Lean.IR.ExplicitRC.instInhabitedLiveVars = { default := { vars := default, borrows := default } }

@[inline]

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

Equations

• liveVars1.merge liveVars2 = { vars := Std.TreeSet.merge liveVars1.vars liveVars2.vars, borrows := Std.TreeSet.merge liveVars1.borrows liveVars2.borrows }

@[reducible, inline]

abbrev Lean.IR.ExplicitRC.JPLiveVarMap : Type

Equations

• Lean.IR.ExplicitRC.JPLiveVarMap = Std.TreeMap Lean.IR.JoinPointId Lean.IR.ExplicitRC.LiveVars fun (x y : Lean.IR.JoinPointId) => compare x.idx y.idx

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

Equations

• Lean.IR.ExplicitRC.getDecl ctx fid = (Lean.IR.findEnvDecl' ctx.env fid ctx.decls).get!

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

Equations

• Lean.IR.ExplicitRC.getVarInfo ctx x = Std.TreeMap.get! ctx.varMap x

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

Equations

• Lean.IR.ExplicitRC.getJPParams ctx j = (ctx.localCtx.getJPParams j).get!

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

Equations

• Lean.IR.ExplicitRC.getJPLiveVars ctx j = Std.TreeMap.get! ctx.jpLiveVarMap j

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

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 Decl) : CompilerM (Array Decl)

Equations

• Lean.IR.explicitRC decls = do let env ← Lean.getEnv pure (Array.map (Lean.IR.ExplicitRC.visitDecl env decls) decls)