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

The decision of the float mechanism.

• arm: Lean.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.

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.instHashableDecision = { hash := Lean.Compiler.LCNF.FloatLetIn.hashDecision✝ }

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.instBEqDecision = { beq := Lean.Compiler.LCNF.FloatLetIn.beqDecision✝ }

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.instInhabitedDecision = { default := Lean.Compiler.LCNF.FloatLetIn.Decision.arm default }

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.instReprDecision = { reprPrec := Lean.Compiler.LCNF.FloatLetIn.reprDecision✝ }

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.Decision.ofAlt (Lean.Compiler.LCNF.AltCore.alt name params code) = Lean.Compiler.LCNF.FloatLetIn.Decision.arm name
• Lean.Compiler.LCNF.FloatLetIn.Decision.ofAlt (Lean.Compiler.LCNF.AltCore.default code) = Lean.Compiler.LCNF.FloatLetIn.Decision.default

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

The context for BaseFloatM.

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

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

The state for FloatM

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

  A map from identifiers of declarations to their current decision.

• newArms : Std.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

@[reducible, inline]

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

Use to collect relevant declarations for the floating mechanism.

Equations

• Lean.Compiler.LCNF.FloatLetIn.BaseFloatM = ReaderT Lean.Compiler.LCNF.FloatLetIn.BaseFloatContext Lean.Compiler.LCNF.CompilerM

@[reducible, inline]

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

Use to compute the actual floating.

Equations

• Lean.Compiler.LCNF.FloatLetIn.FloatM = StateRefT' IO.RealWorld Lean.Compiler.LCNF.FloatLetIn.FloatState Lean.Compiler.LCNF.FloatLetIn.BaseFloatM

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.

Equations

• Lean.Compiler.LCNF.FloatLetIn.withNewCandidate decl x = withReader (fun (r : Lean.Compiler.LCNF.FloatLetIn.BaseFloatContext) => { decls := decl :: r.decls }) x

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.

Equations

• Lean.Compiler.LCNF.FloatLetIn.withNewScope x = withReader (fun (x : Lean.Compiler.LCNF.FloatLetIn.BaseFloatContext) => { decls := [] }) x

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

Equations

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

def Lean.Compiler.LCNF.FloatLetIn.initialDecisions (cs : Lean.Compiler.LCNF.Cases) : Lean.Compiler.LCNF.FloatLetIn.BaseFloatM (Std.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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.FloatLetIn.initialDecisions.goCases cs = Array.forM Lean.Compiler.LCNF.FloatLetIn.initialDecisions.goAlt cs.alts

def Lean.Compiler.LCNF.FloatLetIn.initialNewArms (cs : Lean.Compiler.LCNF.Cases) : Std.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.

Equations

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

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.

Equations

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

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

Equations

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

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

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

Equations

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

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

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.

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.

Equations

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

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

Equations

• decl.floatLetIn = Lean.Compiler.LCNF.FloatLetIn.floatLetIn decl

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

Equations

• Lean.Compiler.LCNF.floatLetIn phase occurrence = Lean.Compiler.LCNF.Pass.mkPerDeclaration `floatLetIn Lean.Compiler.LCNF.Decl.floatLetIn phase occurrence