Documentation

Lean.Compiler.LCNF.FloatLetIn

The decision of the float mechanism.

Instances For

    The context for BaseFloatM.

    • All the declarations that were collected in the current LCNF basic block up to the current statement (in reverse order for efficiency).

    Instances For

      The state for FloatM

      Instances For
        @[reducible, inline]

        Use to collect relevant declarations for the floating mechanism.

        Equations
        Instances For

          Add decl to the list of declarations and run x with that updated context.

          Equations
          Instances For

            Whether to ignore decl for the floating mechanism. We want to do this if:

            • decl' is storing a typeclass instance
            • decl is a projection from a variable that is storing a typeclass instance
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Compute the initial decision for all declarations that BaseFloatM collected up to this point, with respect to cs. The initial decisions are:

              • dont if the declaration is detected by ignore?
              • dont if the declaration is the discriminant of cs since we obviously need the discriminant to be computed before the match.
              • dont if we see the declaration being used in more than one cases arm
              • arm or default if we see the declaration only being used in exactly one cases arm
              • unknown otherwise
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Compute the initial new arms. This will just set up a map from all arms of cs to empty Arrays, plus one additional entry for dont.

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

                  Will:

                  • put decl into the dont arm
                  • decide that any free variable that occurs in decl and is a declaration of interest as not getting moved either.
                  let x := ...
                  let y := ...
                  let z := x + y
                  cases z with
                  | n => z * x
                  | m => z * y
                  

                  Here x and y are originally marked as getting floated into n and m respectively but since z can't be moved we don't want that to move x and y.

                  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

                      Will:

                      • put decl into the arm it is marked to be moved into
                      • for any variables that might occur in decl and are of interest:
                        • if they are already meant to be floated into the same arm or not at all leave them untouched:
                          let x := ...
                          let y := x + z
                          cases z with
                          | n => x * y
                          | m => z
                          
                          If we are at y x is already marked to be floated into n as well.
                        • if there hasn't be a decision yet, that is they are marked with .unknown we float them into the same arm as the current value:
                          let x := ..
                          let y := x + 2
                          cases z with
                          | n => y
                          | m => z
                          
                          Here x is initially marked as .unknown since it occurs in no branch, however since we want to move y into the n branch we can also decide to move x into the n branch. Note that this decision might be revoked later on in the case of:
                          let x := ..
                          let a := x + 1
                          let y := x + 2
                          cases z with
                          | n => y
                          | m => a
                          
                          When we visit a x is now marked as getting moved into n but since it also occurs in a which wants to be moved somewhere else we will instead decide to not move x at all.
                        • if they are meant to be floated somewhere else decide that they won't get floated:
                          let x := ...
                          let y := x + z
                          cases z with
                          | n => y
                          | m => x
                          
                          If we are at y x is still marked to be moved but we don't want that.
                      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

                          Iterate through decl, pushing local declarations that are only used in one control flow arm into said arm in order to avoid useless computations.

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

                            Iterate through the collected declarations, determining from the bottom up whether they (and the declarations they refer to) should get moved down into the arms of the cases statement or not.

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