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

Instances For

• Lean.IR.ExplicitRC.instInhabitedVarInfo

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

Equations

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

@[inline, reducible]

abbrev Lean.IR.ExplicitRC.VarMap : Type

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.IR.ExplicitRC.getJPLiveVars ctx j = match Lean.RBMap.find? ctx.jpLiveVarMap j with | some s => s | none => ∅

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

Equations

• Lean.IR.ExplicitRC.mustConsume ctx x = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; info.ref && info.consume

@[inline]

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

Equations

• Lean.IR.ExplicitRC.addInc ctx x b n = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; if (n == 0) = true then b else Lean.IR.FnBody.inc x n true info.persistent b

@[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 = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; Lean.IR.FnBody.dec x 1 true info.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.

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

Equations

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