Documentation

Lean.Compiler.LCNF.PushProj

This pass pushes projections into directly neighboring nested case statements.

Suppose we have an LCNF pure input that looks as follows:

cases a with
| alt1 p1 p2 =>
  cases b with
  | alt2 p3 p4 =>
    ...
  | alt3 p5 p6 =>
    ...
| ...

ToImpure will convert this into:

cases a with
| alt1 p1 p2 =>
  let p1 := proj[0] a;
  let p2 := proj[1] a;
  cases b with
  | alt2 p3 p4 =>
    let p3 := proj[0] b;
    let p4 := proj[1] b;
    ...
  | alt3 p5 p6 =>
    let p5 := proj[0] b;
    let p6 := proj[1] b;
    ...
| ...

Let's assume p1 is used in both alt2 and alt3 and p2 is used only in alt3 then this pass will convert the code into:

cases a with
| alt1 p1 p2 =>
  cases b with
  | alt2 p3 p4 =>
    let p1 := proj[0] a;
    let p3 := proj[0] b;
    let p4 := proj[1] b;
    ...
  | alt3 p5 p6 =>
    let p1 := proj[0] a;
    let p2 := proj[1] a;
    let p5 := proj[0] b;
    let p6 := proj[1] b;
    ...
| ...

This helps to avoid loading memory that is not actually required in all branches.

Note that unlike floatLetIn, this pass is willing to duplicate projections that are being pushed around.

TODO: we suspect it might also help with reuse analysis, check this. This pass was ported from IR to LCNF.

source
def Lean.Compiler.LCNF.pushProj (occurrence : Nat) :
Pass
Equations
Instances For