Documentation

Lean.Compiler.LCNF.ResetReuse

This module implements the insertion of reset-reuse instructions into lambda pure as described in "Counting Immutable Beans" (https://arxiv.org/pdf/1908.05647). The insertion happens before we add low-level reference counting and other memory management related operations. In addition to the IR specified in the paper this implementation supports join points and several operations for unboxed data.

The algorithm attempts to identify situations where we potentially free a piece of memory and shortly after re-allocate memory of the same shape as the memory that was just freed. It then inserts addition instructions to attempt to reuse the memory right away instead of going through the allocator.

For this the paper defines three functions: