# Documentation

Lean.Compiler.LCNF.FloatLetIn

The decision of the float mechanism.

Instances For
Equations
• One or more equations did not get rendered due to their size.
• All the declarations that were collected in the current LCNF basic block up to the current statement (in reverse order for efficiency).

decls :

The context for BaseFloatM.

Instances For
• A map from identifiers of declarations to their current decision.

• A map from decisions (excluding unknown) to the declarations with these decisions (in correct order). Basically:

• Which declarations do we not move
• Which declarations do we move into a certain arm
• Which declarations do we move into the default arm

The state for FloatM

Instances For
@[inline]

Use to collect relevant declarations for the floating mechanism.

Equations
@[inline]

Use to compute the actual floating.

Equations

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

Equations

Run x with an empty list of declarations.

Equations

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.

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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.

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.
Equations
• One or more equations did not get rendered due to their size.

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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

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.