Documentation

Lean.Compiler.IR.RC

structure Lean.IR.ExplicitRC.VarInfo:

Type

ref : Bool
persistent : Bool
consume : Bool

instance Lean.IR.ExplicitRC.instInhabitedVarInfo:

Inhabited Lean.IR.ExplicitRC.VarInfo

Equations

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

@[inline]

abbrev Lean.IR.ExplicitRC.VarMap:

Type

Equations

Lean.IR.ExplicitRC.VarMap = Std.RBMap Lean.IR.VarId Lean.IR.ExplicitRC.VarInfo fun x y => compare x.idx y.idx

structure Lean.IR.ExplicitRC.Context:

Type

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

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 Std.RBMap.find? ctx.jpLiveVarMap j with | some s => s | none => ∅

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

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) :

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) :

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) :

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)