Remark: the insertResetReuse transformation is applied before we have inserted inc/dec instructions, and perfomed lower level optimizations that introduce the instructions release and set.

Remark: the functions S, D and R defined here implement the corresponding functions in the paper "Counting Immutable Beans"

Here are the main differences:

• We use the State monad to manage the generation of fresh variable names.
• Support for join points, and uset and sset instructions for unboxed data.
• D uses the auxiliary function Dmain.
• Dmain returns a pair (b, found) to avoid quadratic behavior when checking the last occurrence of the variable x.
• Because we have join points in the actual implementation, a variable may be live even if it does not occur in a function body. See example at livevars.lean.

@[inline, reducible]

abbrev Lean.IR.ResetReuse.M (α : Type) : Type

We use Context to track join points in scope.

Equations

• Lean.IR.ResetReuse.M = ReaderT Lean.IR.LocalContext (StateT Lean.IR.Index Id)

partial def Lean.IR.ResetReuse.R : Lean.IR.FnBody → Lean.IR.ResetReuse.M Lean.IR.FnBody

def Lean.IR.Decl.insertResetReuse (d : Lean.IR.Decl) : Lean.IR.Decl

Equations

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