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