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 usetandssetinstructions for unboxed data.
- Duses the auxiliary function- Dmain.
- Dmainreturns 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]
We use Context to track join points in scope.