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 } }

@[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 : 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 = ((Lean.IR.ExplicitRC.getVarInfo ctx x).ref && (Lean.IR.ExplicitRC.getVarInfo ctx x).consume)

@[inline]

def Lean.IR.ExplicitRC.addInc (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) (n : Nat := 1) : Lean.IR.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 : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) : Lean.IR.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 : 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.
• Lean.IR.ExplicitRC.visitDecl env decls d = d

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)