Documentation

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:

  • 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.

Instances For
    @[reducible, inline]

    We use Context to track join points in scope.

    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        • d.insertResetReuseCore relaxedReuse = d
        Instances For
          Equations
          • d.insertResetReuse = (d.insertResetReuseCore false).insertResetReuseCore true
          Instances For