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
- env : Lean.Environment
- decls : Array Lean.IR.Decl
- varMap : Lean.IR.ExplicitRC.VarMap
- jpLiveVarMap : Lean.IR.JPLiveVarMap
- localCtx : Lean.IR.LocalContext
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
@[inline]
def
Lean.IR.ExplicitRC.addInc
(ctx : Lean.IR.ExplicitRC.Context)
(x : Lean.IR.VarId)
(b : Lean.IR.FnBody)
(n : optParam Nat 1)
 :
Instances For
@[inline]
def
Lean.IR.ExplicitRC.addDec
(ctx : Lean.IR.ExplicitRC.Context)
(x : Lean.IR.VarId)
(b : Lean.IR.FnBody)
 :
Instances For
def
Lean.IR.ExplicitRC.updateVarInfoWithParams
(ctx : Lean.IR.ExplicitRC.Context)
(ps : Array Lean.IR.Param)
 :
Instances For
def
Lean.IR.ExplicitRC.visitDecl
(env : Lean.Environment)
(decls : Array Lean.IR.Decl)
(d : Lean.IR.Decl)
 :