structure Lean.Compiler.LCNF.Pass : Type

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

  occurrence : Nat

• Which phase this Pass is supposed to run in

  phase : Lean.Compiler.LCNF.Phase

• The name of the Pass

  name : Lean.Name

• The actual pass function, operating on the Decls.

  run : Array Lean.Compiler.LCNF.Decl → Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)

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

instance Lean.Compiler.LCNF.instInhabitedPass : Inhabited Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.instInhabitedPass = { default := { occurrence := default, phase := default, name := default, run := default } }

structure Lean.Compiler.LCNF.PassInstaller : Type

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

  install : Array Lean.Compiler.LCNF.Pass → Lean.CoreM (Array Lean.Compiler.LCNF.Pass)

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

instance Lean.Compiler.LCNF.instInhabitedPassInstaller : Inhabited Lean.Compiler.LCNF.PassInstaller

Equations

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

structure Lean.Compiler.LCNF.PassManager : Type

• passes : Array Lean.Compiler.LCNF.Pass

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

instance Lean.Compiler.LCNF.instInhabitedPassManager : Inhabited Lean.Compiler.LCNF.PassManager

Equations

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

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

Equations

• Lean.Compiler.LCNF.Phase.toNat _fun_discr = match _fun_discr with | Lean.Compiler.LCNF.Phase.base => 0 | Lean.Compiler.LCNF.Phase.mono => 1 | Lean.Compiler.LCNF.Phase.impure => 2

instance Lean.Compiler.LCNF.Phase.instLTPhase : LT Lean.Compiler.LCNF.Phase

Equations

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

instance Lean.Compiler.LCNF.Phase.instLEPhase : LE Lean.Compiler.LCNF.Phase

Equations

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

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

Equations

• Lean.Compiler.LCNF.Phase.instDecidableLtPhaseInstLTPhase = Nat.decLt (Lean.Compiler.LCNF.Phase.toNat p1) (Lean.Compiler.LCNF.Phase.toNat p2)

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

Equations

• Lean.Compiler.LCNF.Phase.instDecidableLePhaseInstLEPhase = Nat.decLe (Lean.Compiler.LCNF.Phase.toNat p1) (Lean.Compiler.LCNF.Phase.toNat p2)

instance Lean.Compiler.LCNF.Phase.instToStringPhase : ToString Lean.Compiler.LCNF.Phase

Equations

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

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

Equations

• Lean.Compiler.LCNF.Pass.mkPerDeclaration name run phase occurrence = { occurrence := occurrence, phase := phase, name := name, run := fun xs => Array.mapM run xs }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.PassInstaller.run manager installer = do let a ← Lean.Compiler.LCNF.PassInstaller.install installer manager.passes pure { passes := a }

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

Equations

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