Lean.Compiler.IR.ResetReuse

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.

source

structure Lean.IR.ResetReuse.Context :

Type

lctx : Lean.IR.LocalContext
alreadyFound : Lean.PHashSet Lean.IR.VarId
Contains all variables in cases statements in the current path and variables that are already in reset statements when we invoke R.
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 →
  ...
```
A variable can already be in a reset statement when we invoke R because we execute it with and without relaxedReuse.
relaxedReuse : Bool
If relaxedReuse := true, then allow memory cells from different constructors to be reused. For example, we can reuse a PSigma.mk to allocate a Prod.mk. To avoid counterintuitive behavior, we first try relaxedReuse := false, and then relaxedReuse := true.