inductive Lean.Compiler.LCNF.FloatLetIn.Decision : Type

• arm: Lake.Name → Lean.Compiler.LCNF.FloatLetIn.Decision

  Push into the arm with name name.

• default: Lean.Compiler.LCNF.FloatLetIn.Decision

  Push into the default arm.

• dont: Lean.Compiler.LCNF.FloatLetIn.Decision

  Dont move this declaration it is needed where it is right now.

• unknown: Lean.Compiler.LCNF.FloatLetIn.Decision

  No decision has been made yet.

The decision of the float mechanism.

instance Lean.Compiler.LCNF.FloatLetIn.instHashableDecision : Hashable Lean.Compiler.LCNF.FloatLetIn.Decision

instance Lean.Compiler.LCNF.FloatLetIn.instBEqDecision : BEq Lean.Compiler.LCNF.FloatLetIn.Decision

instance Lean.Compiler.LCNF.FloatLetIn.instInhabitedDecision : Inhabited Lean.Compiler.LCNF.FloatLetIn.Decision

instance Lean.Compiler.LCNF.FloatLetIn.instReprDecision : Repr Lean.Compiler.LCNF.FloatLetIn.Decision

def Lean.Compiler.LCNF.FloatLetIn.Decision.ofAlt : Lean.Compiler.LCNF.Alt → Lean.Compiler.LCNF.FloatLetIn.Decision

structure Lean.Compiler.LCNF.FloatLetIn.BaseFloatContext : Type

• decls : List Lean.Compiler.LCNF.CodeDecl

  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.

structure Lean.Compiler.LCNF.FloatLetIn.FloatState : Type

• decision : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FloatLetIn.Decision

  A map from identifiers of declarations to their current decision.

• newArms : Lean.HashMap Lean.Compiler.LCNF.FloatLetIn.Decision (List Lean.Compiler.LCNF.CodeDecl)

  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

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FloatLetIn.BaseFloatM (α : Type) : Type

Use to collect relevant declarations for the floating mechanism.

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FloatLetIn.FloatM (α : Type) : Type

Use to compute the actual floating.

def Lean.Compiler.LCNF.FloatLetIn.withNewCandidate {α : Type} (decl : Lean.Compiler.LCNF.CodeDecl) (x : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM α) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM α

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

def Lean.Compiler.LCNF.FloatLetIn.withNewScope {α : Type} (x : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM α) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM α

Run x with an empty list of declarations.

def Lean.Compiler.LCNF.FloatLetIn.ignore? (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM Bool

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

def Lean.Compiler.LCNF.FloatLetIn.initialDecisions (cs : Lean.Compiler.LCNF.Cases) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM (Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FloatLetIn.Decision)

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

def Lean.Compiler.LCNF.FloatLetIn.initialDecisions.goFVar (plannedDecision : Lean.Compiler.LCNF.FloatLetIn.Decision) (var : Lean.FVarId) : StateRefT' IO.RealWorld (Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FloatLetIn.Decision) Lean.Compiler.LCNF.FloatLetIn.BaseFloatM Unit

def Lean.Compiler.LCNF.FloatLetIn.initialDecisions.goAlt (alt : Lean.Compiler.LCNF.Alt) : StateRefT' IO.RealWorld (Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FloatLetIn.Decision) Lean.Compiler.LCNF.FloatLetIn.BaseFloatM Unit

def Lean.Compiler.LCNF.FloatLetIn.initialDecisions.goCases (cs : Lean.Compiler.LCNF.Cases) : StateRefT' IO.RealWorld (Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FloatLetIn.Decision) Lean.Compiler.LCNF.FloatLetIn.BaseFloatM Unit

def Lean.Compiler.LCNF.FloatLetIn.initialNewArms (cs : Lean.Compiler.LCNF.Cases) : Lean.HashMap Lean.Compiler.LCNF.FloatLetIn.Decision (List Lean.Compiler.LCNF.CodeDecl)

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.

def Lean.Compiler.LCNF.FloatLetIn.dontFloat (decl : Lean.Compiler.LCNF.CodeDecl) : Lean.Compiler.LCNF.FloatLetIn.FloatM Unit

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.

def Lean.Compiler.LCNF.FloatLetIn.dontFloat.goFVar (fvar : Lean.FVarId) : Lean.Compiler.LCNF.FloatLetIn.FloatM Unit

def Lean.Compiler.LCNF.FloatLetIn.float (decl : Lean.Compiler.LCNF.CodeDecl) : Lean.Compiler.LCNF.FloatLetIn.FloatM Unit

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.

def Lean.Compiler.LCNF.FloatLetIn.float.goFVar (fvar : Lean.FVarId) (arm : Lean.Compiler.LCNF.FloatLetIn.Decision) : Lean.Compiler.LCNF.FloatLetIn.FloatM Unit

def Lean.Compiler.LCNF.FloatLetIn.floatLetIn (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

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

def Lean.Compiler.LCNF.FloatLetIn.floatLetIn.goCases : Lean.Compiler.LCNF.FloatLetIn.FloatM Unit

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.

partial def Lean.Compiler.LCNF.FloatLetIn.floatLetIn.go (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.Decl.floatLetIn (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

def Lean.Compiler.LCNF.floatLetIn (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Pass