def Lean.Compiler.LCNF.Phase.toNat : Phase → Nat

Equations

• Lean.Compiler.LCNF.Phase.base.toNat = 0
• Lean.Compiler.LCNF.Phase.mono.toNat = 1
• Lean.Compiler.LCNF.Phase.impure.toNat = 2

@[instance_reducible]

instance Lean.Compiler.LCNF.instToStringPhase : ToString Phase

Equations

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

def Lean.Compiler.LCNF.Phase.withPurityCheck {α : Sort u_1} [Inhabited α] (pp : Phase) (ip : Purity) (x : pp.toPurity = ip → α) : α

Equations

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

@[instance_reducible]

instance Lean.Compiler.LCNF.instLTPhase : LT Phase

Equations

• Lean.Compiler.LCNF.instLTPhase = { lt := fun (l r : Lean.Compiler.LCNF.Phase) => l.toNat < r.toNat }

@[instance_reducible]

instance Lean.Compiler.LCNF.instLEPhase : LE Phase

Equations

• Lean.Compiler.LCNF.instLEPhase = { le := fun (l r : Lean.Compiler.LCNF.Phase) => l.toNat ≤ r.toNat }

@[instance_reducible]

instance Lean.Compiler.LCNF.instDecidableLtPhase {p1 p2 : Phase} : Decidable (p1 < p2)

Equations

• Lean.Compiler.LCNF.instDecidableLtPhase = p1.toNat.decLt p2.toNat

@[instance_reducible]

instance Lean.Compiler.LCNF.instDecidableLePhase {p1 p2 : Phase} : Decidable (p1 ≤ p2)

Equations

• Lean.Compiler.LCNF.instDecidableLePhase = p1.toNat.decLe p2.toNat

@[simp]

theorem Lean.Compiler.LCNF.Phase.le_refl (p : Phase) : p ≤ p

structure Lean.Compiler.LCNF.Pass : Type

A single compiler Pass, consisting of the actual pass function operating on the Decls as well as meta information.

• occurrence : Nat

  Which occurrence of the pass in the pipeline this is. Some passes, like simp, can occur multiple times in the pipeline. For most passes this value does not matter.

• phase : Phase

  Which phase this Pass is supposed to run in

• phaseOut : Phase

  Resulting phase.

• phaseInv : self.phaseOut ≥ self.phase
• shouldAlwaysRunCheck : Bool

  Whether IR validation checks should always run after this pass, regardless of configuration options.

• name : Name

  The name of the Pass

• run : Array (Decl self.phase.toPurity) → CompilerM (Array (Decl self.phaseOut.toPurity))

  The actual pass function, operating on the Decls.

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedPass : Inhabited Pass

Equations

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

structure Lean.Compiler.LCNF.PassInstaller : Type

Can be used to install, remove, replace etc. passes by tagging a declaration of type PassInstaller with the cpass attribute.

• phase : Phase

  Affected phase.

• install : Array Pass → CoreM (Array Pass)

  When the installer is run this function will receive a list of all current Passes and return a new one, this can modify the list (and the Passes contained within) in any way it wants.

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedPassInstaller : Inhabited PassInstaller

Equations

• Lean.Compiler.LCNF.instInhabitedPassInstaller = { default := Lean.Compiler.LCNF.instInhabitedPassInstaller.default }

def Lean.Compiler.LCNF.instInhabitedPassInstaller.default : PassInstaller

Equations

• Lean.Compiler.LCNF.instInhabitedPassInstaller.default = { phase := default, install := default }

structure Lean.Compiler.LCNF.PassManager : Type

The PassManager used to store all Passes that will be run within pipeline.

• basePasses : Array Pass

  Passes that happen during the LCNF base phase

• monoPasses : Array Pass

  Passes that happen during the LCNF mono phase before lambda lifting

• monoPassesNoLambda : Array Pass

  Passes that happen during the LCNF mono phase after lambda lifting. Note that lifted lambdas will have been lifted out of the SCC they originated from if possible.

• impurePasses : Array Pass

  Passes that happen during the LCNF impure phase.

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedPassManager : Inhabited PassManager

Equations

• Lean.Compiler.LCNF.instInhabitedPassManager = { default := Lean.Compiler.LCNF.instInhabitedPassManager.default }

def Lean.Compiler.LCNF.instInhabitedPassManager.default : PassManager

Equations

• Lean.Compiler.LCNF.instInhabitedPassManager.default = { basePasses := default, monoPasses := default, monoPassesNoLambda := default, impurePasses := default }

def Lean.Compiler.LCNF.Pass.mkPerDeclaration (name : Name) (phase : Phase) (run : Decl phase.toPurity → CompilerM (Decl phase.toPurity)) (occurrence : Nat := 0) : Pass

Equations

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

def Lean.Compiler.LCNF.PassManager.validate (manager : PassManager) : CoreM Unit

Equations

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

def Lean.Compiler.LCNF.PassManager.findOccurrenceBounds (targetName : Name) (passes : Array Pass) : CoreM (Nat × Nat)

Equations

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

def Lean.Compiler.LCNF.PassInstaller.installAtEnd (phase : Phase) (p : Pass) : PassInstaller

Equations

• Lean.Compiler.LCNF.PassInstaller.installAtEnd phase p = { phase := phase, install := fun (passes : Array Lean.Compiler.LCNF.Pass) => pure (passes.push p) }

def Lean.Compiler.LCNF.PassInstaller.append (phase : Phase) (passesNew : Array Pass) : PassInstaller

Equations

• Lean.Compiler.LCNF.PassInstaller.append phase passesNew = { phase := phase, install := fun (passes : Array Lean.Compiler.LCNF.Pass) => pure (passes ++ passesNew) }

def Lean.Compiler.LCNF.PassInstaller.withEachOccurrence (phase : Phase) (targetName : Name) (f : Nat → PassInstaller) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.installAfter (phase : Phase) (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.installAfterEach (phase : Phase) (targetName : Name) (p : Pass → Pass) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.installBefore (phase : Phase) (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.installBeforeEachOccurrence (phase : Phase) (targetName : Name) (p : Pass → Pass) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.replacePass (phase : Phase) (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.replaceEachOccurrence (phase : Phase) (targetName : Name) (p : Pass → Pass) : PassInstaller

Equations

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

def Lean.Compiler.LCNF.PassInstaller.run (manager : PassManager) (installer : PassInstaller) : CoreM PassManager

Equations

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

def Lean.Compiler.LCNF.PassInstaller.runFromDecl (manager : PassManager) (declName : Name) : CoreM PassManager

Equations

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