Remark: the insertResetReuse transformation is applied before we have inserted inc/dec instructions, and performed 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.

structure Lean.IR.ResetReuse.Context : Type

• lctx : Lean.IR.LocalContext
• casesVars : Lean.PHashSet Lean.IR.VarId

  Contains all variables in cases statements in the current path. We use this information to prevent double-reset in code such as

  case x_i : obj of
  Prod.mk →
    case x_i : obj of
    Prod.mk →
    ...
  

@[reducible, inline]

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

We use Context to track join points in scope.

Equations

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

partial def Lean.IR.ResetReuse.R (e : 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.