@[implicit_reducible, instance 100]

instance instColorized_common {α : Type} : Colorized.Colorized α

Anything can be colorized if we ignore the annotations.

Equations

• instColorized_common = { colorize := fun (x : Colorized.Section) (x_1 : Colorized.Color) => id, style := fun (x : Colorized.Style) => id }

class CompilerDiagnostic (ε : Type u_1) (α : outParam Type) [Colorized.Colorized α] : Type u_1

• isError : Bool
• posOf : ε → SourceSpan
• msgOf : ε → α
• hintsOf : ε → List α
• name : ε → String

  The -W<name>/-Wno-<name> name this diagnostic is filtered under. Only meaningful for warnings — an error is never suppressed by -W, so its instance leaves this at the default.

• code : ε → DiagnosticCode

  This diagnostic's stable code (Common/Diagnostics/Registry.lean), printed as error[E0042]: and taken as the identity a regression fixture or fugue explain names. Deliberately without a default: an instance must map every constructor to an entry, so adding a diagnostic without registering it fails to compile.

@[implicit_reducible]

instance instCompilerDiagnosticEmptyString : CompilerDiagnostic Empty String

A pass with no warnings uses MonadDiagnostic Empty ε m. Lets List Empty still satisfy a generic [CompilerDiagnostic α String] requirement; every field is Empty.elim since no Empty value ever exists to apply it to.

Equations

• instCompilerDiagnosticEmptyString = { isError := true, posOf := Empty.elim, msgOf := Empty.elim, code := Empty.elim }

def colorizeIf {α : Type} [Colorized.Colorized α] (enabled : Bool) (c : Colorized.Color) (x : α) : α

Colorized.color, but a no-op when enabled is false (-fno-color). Not private: Fugue.lean reuses it for its Built/Replayed progress lines too.

Equations

• colorizeIf enabled c x = if enabled = true then Colorized.Colorized.color c x else x

def styleIf {α : Type} [Colorized.Colorized α] (enabled : Bool) (s : Colorized.Style) (x : α) : α

Colorized.style, but a no-op when enabled is false (-fno-color). Not private: Fugue.lean reuses it too, for its Built/Replayed/Failed progress lines.

Equations

• styleIf enabled s x = if enabled = true then Colorized.Colorized.style s x else x

def CompilerDiagnostic.pretty {ε : Type u_1} {α : Type} [Colorized.Colorized α] [ToString α] [CompilerDiagnostic ε α] (err : ε) (source : List String.Slice) (colored : Bool := true) : String

Renders one diagnostic: an error[E0042]:-style header, the message and its hints, and the offending source line with the span underlined. colored := false (driven by -fno-color) disables ANSI styling.

Equations

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

class MonadDiagnostic (α : outParam (Type u_1)) (β : outParam (Type u_2)) (m : Type u_1 → Type u_3) extends MonadWriter (List α) m, MonadExceptOf β m : Type (max (max (u_1 + 1) u_2) u_3)

The effects a diagnostics-producing pass needs: an always-growing List α of non-fatal warnings (MonadWriter), plus MonadExceptOf's throw/catch for a fatal β. The point isn't the two constraints alone but their interaction, only actually guaranteed by DiagT below: the accumulated List α survives a throw, unlike the ordinary WriterT (List α) (ExceptT β ·) order, where a throw short-circuits before the writer's log is ever paired with anything.

• tell (w : List α) : m PUnit
• listen {α : Type u_1} (f : m α) : m (α × List α)
• pass {α : Type u_1} (f : m (α × (List α → List α))) : m α
• throw {α : Type u_1} : β → m α
• tryCatch {α : Type u_1} (body : m α) (handler : β → m α) : m α

def warn {α : Type u_1} {β : Type u_2} {m : Type u_1 → Type u_3} [MonadDiagnostic α β m] (w : α) : m PUnit

Emit a single warning. MonadWriter.tell wants a full List α (its monoid unit is []), but every call site only ever has one warning in hand at a time.

Equations

• warn w = tell [w]

def DiagT (α : Type u_1) (β : Type u_2) (m : Type (max (max u_3 u_2) u_1) → Type u_4) (γ : Type u_3) : Type u_4

The one concrete MonadDiagnostic α β instance that keeps the promise above: Except β γ lives inside the pair as ordinary data, rather than as a monadic short-circuit wrapping the pair from outside — so a throw is just pure ([], .error e), and every warning already tell'd is already in that [], nothing lost. Also why listen/pass stay lossless, unlike the generic ExceptT ε N composition, where listen's N (α × ω) shape has nowhere to put ω once α disappears on a throw.

Equations

• DiagT α β m γ = m (List α × Except β γ)

def DiagT.run {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : Type (max (max u_1 u_2) u_3) → Type u_4} (x : DiagT α β m γ) : m (List α × Except β γ)

Unwrap a DiagT action down to the underlying m, always pairing every warning tell'd against it with the final Except-wrapped result — regardless of which branch that result took. The one place the main driver needs to reach into, to flush a pass's warnings whether or not that pass ultimately threw.

Equations

• x.run = x

def DiagT.mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : Type (max (max u_3 u_2) u_1) → Type u_4} (x : m (List α × Except β γ)) : DiagT α β m γ

Wrap an m action already in the right shape back up as a DiagT.

Equations

• DiagT.mk x = x

@[implicit_reducible]

instance DiagT.instMonad {α : Type u_1} {β : Type u_2} {m : Type (max (max u_1 u_2) u_3) → Type u_4} [Monad m] : Monad (DiagT α β m)

Equations

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

@[implicit_reducible]

instance DiagT.instMonadWriterList {α : Type} {β : Type u_1} {m : Type u_1 → Type u_2} [Monad m] : MonadWriter (List α) (DiagT α β m)

Equations

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

@[implicit_reducible]

instance DiagT.instMonadExceptOf {α : Type u_1} {β : Type u_2} {m : Type (max (max u_1 u_2) u_3) → Type u_4} [Monad m] : MonadExceptOf β (DiagT α β m)

Equations

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

@[implicit_reducible]

instance DiagT.instMonadLift {α : Type u_1} {β : Type u_2} {m : Type (max (max u_3 u_1) u_2) → Type u_4} [Monad m] : MonadLift m (DiagT α β m)

Lift any ambient m action in, unconditionally producing no warnings.

Equations

• DiagT.instMonadLift = { monadLift := fun {α_1 : Type (max (max ?u.4 ?u.3) ?u.2)} (x : m α_1) => DiagT.mk do let a ← x pure ([], Except.ok a) }

@[implicit_reducible]

instance DiagT.instMonadReaderOf {α : Type u_1} {β : Type u_2} {m : Type (max (max u_3 u_1) u_2) → Type u_4} [Monad m] {ρ : Type (max (max u_3 u_1) u_2)} [MonadReaderOf ρ m] : MonadReaderOf ρ (DiagT α β m)

Lets FlagsEnv/ResolutionStack reach through whatever DiagT layer compileModule runs at — lifts straight from the base m, same shape as the MonadLift instance above.

Equations

• DiagT.instMonadReaderOf = { read := DiagT.mk do let r ← read pure ([], Except.ok r) }

@[implicit_reducible]

instance DiagT.instMonadWithReaderOf {α : Type u_1} {β : Type u_2} {m : Type (max (max u_3 u_1) u_2) → Type u_4} {ρ : Type (max (max u_3 u_1) u_2)} [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ (DiagT α β m)

Companion to the MonadReaderOf lift above — ResolutionStack's push-on-recurse, pop-on-return pattern (withReader (mod.name :: ·)) needs to reach through DiagT too.

Equations

• DiagT.instMonadWithReaderOf = { withReader := fun {α_1 : Type (max (max ?u.4 ?u.3) ?u.2)} (f : ρ → ρ) (x : DiagT α β m α_1) => DiagT.mk (withReader f x.run) }

@[implicit_reducible]

instance DiagT.instMonadStateOf {α β : Type} {m : Type → Type u_1} [Monad m] {σ : Type} [MonadStateOf σ m] : MonadStateOf σ (DiagT α β m)

Lifts m's own state through DiagT, so any [MonadStateOf _ m]-generic instance picks it up automatically without a dedicated DiagT instance.

Equations

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

def DiagT.lift {α : Type u_1} {α' : Type (max (max u_1 u_2) (max u_3 u_1) u_2)} {β : Type u_2} {β' : Type u_4} {γ : Type (max (max u_3 u_1) u_2)} {n : Type (max (max u_1 u_2) (max u_3 u_1) u_2) → Type u_5} {m : Type (max (max u_1 u_2) (max u_3 u_1) u_2) → Type u_6} [Monad m] [MonadLiftT n m] [MonadDiagnostic α' β' m] (f : α → α') (g : β → β') (x : DiagT α β n γ) : m γ

Absorbs a self-contained sub-computation's diagnostics into the caller's ambient MonadDiagnostic α' β' m: tells f-mapped warnings, then throws g e on .error, or returns the value on .ok. n is x's own base monad (Id for a pure runner, IO-flavored for a nested recursive call), lifted into m via MonadLiftT so nothing about x's concrete stack leaks into the caller. Lets a caller let-bind straight through a sub-pass's result without unwrapping its DiagT/Except by hand.

Equations

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