Documentation

Lean.Compiler.LCNF.FloatLetIn

The decision of the float mechanism.

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

    The context for BaseFloatM.

    Instances For

      The state for FloatM

      Instances For
        @[inline, reducible]

        Use to collect relevant declarations for the floating mechanism.

        Instances For
          @[inline, reducible]

          Use to compute the actual floating.

          Instances For

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

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

                  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.

                    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 alreayd 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 wont 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.
                      Instances For

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

                        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.

                          Instances For