Documentation

Lean.Compiler.IR.ExpandResetReuse

@[reducible, inline]

Mapping from variable to projections

Equations
    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[inline]
          Equations
            Instances For

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

              Equations
                Instances For
                  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 ....

                    @[reducible, inline]
                    Equations
                      Instances For

                        Auxiliary function for eraseProjIncFor

                        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 remove 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
                              Instances For
                                @[reducible, inline]
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For

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

                                            Equations
                                              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
                                                            def Lean.IR.ExpandResetReuse.expand (mainFn : FnBodyArray FnBodyM FnBody) (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) :
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For

                                                                    (Try to) expand reset and reuse instructions.

                                                                    Equations
                                                                      Instances For