Documentation

Lean.Compiler.IR.ExpandResetReuse

@[inline, reducible]

Mapping from variable to projections

Equations
Instances For
    @[inline]
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Create a mapping from variables to projections. This function assumes variable ids have been normalized

      Equations
      Instances For

        Return true iff x is consumed in all branches of the current block. Here consumption means the block contains a dec x or reuse x ....

        Try to erase inc instructions on projections of y occurring in the tail of bs. Return the updated bs and a bit mask specifying which incs have been removed.

        Equations
        Instances For

          Replace reuse x ctor ... with ctor ..., and remoce dec x

          replace

          x := reset y; b
          

          with

          inc z_1; ...; inc z_i; dec y; b'
          

          where z_i's are the variables in mask, and b' is b where we removed dec x and replaced reuse x ctor_i ... with ctor_i ....

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Given set x[i] := y, return true iff y := proj[i] x

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Given uset x[i] := y, return true iff y := uproj[i] x

                Equations
                Instances For

                  Given sset x[n, i] := y, return true iff y := sproj[n, i] x

                  Equations
                  Instances For

                    Remove unnecessary set/uset/sset operations

                    replace

                    x := reset y; b
                    

                    with

                    let f_i_1 := proj[i_1] y;
                    ...
                    let f_i_k := proj[i_k] y;
                    b'
                    

                    where i_js are the field indexes that the code did not touch immediately before the reset. That is mask[j] == none. b' is b where y dec x is replaced with del y, and z := reuse x ctor_i ws; F is replaced with set x i ws[i] operations, and we replace z with x in F

                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For