Remark: the insertResetReuse transformation is applied before we have
inc/dec instructions, and perfomed lower level optimizations
that introduce the instructions
Remark: the functions
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
ssetinstructions for unboxed data.
Duses the auxiliary function
Dmainreturns a pair
(b, found)to avoid quadratic behavior when checking the last occurrence of the variable
- 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
abbrev Lean.IR.ResetReuse.M (α : Type) :
Context to track join points in scope.
- One or more equations did not get rendered due to their size.