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 VarInfo

Equations

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

@[reducible, inline]

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 : Environment
• decls : Array Decl
• varMap : VarMap
• jpLiveVarMap : JPLiveVarMap
• localCtx : LocalContext

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.IR.ExplicitRC.getJPLiveVars (ctx : Context) (j : JoinPointId) : 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 : Context) (x : 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 : Context) (x : VarId) (b : FnBody) (n : Nat := 1) : FnBody

Equations

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

@[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 true (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 : FnBody → Context → FnBody × LiveVarSet

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.IR.getEnv pure (Array.map (Lean.IR.ExplicitRC.visitDecl env decls) decls)