Diagnostic codes: the stable identity of a diagnostic, independent of its wording.

rustc-shaped — E0042, W0003 — because that shape is already what a user expects to be able to look up (fugue explain E0042), grep a build log for, or write into a regression fixture's expectations. Wording changes freely; a code never does.

inductive Severity : Type

Whether a diagnostic stops the compile. The letter a code starts with.

• error : Severity

  Fatal: E….

• warning : Severity

  Non-fatal: W…, and suppressible via -Wno-<name>.

@[implicit_reducible]

instance instDecidableEqSeverity : DecidableEq Severity

Equations

• instDecidableEqSeverity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprSeverity.repr : Severity → ℕ → Std.Format

Equations

• instReprSeverity.repr Severity.error prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Severity.error")).group prec✝
• instReprSeverity.repr Severity.warning prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Severity.warning")).group prec✝

@[implicit_reducible]

instance instReprSeverity : Repr Severity

Equations

• instReprSeverity = { reprPrec := instReprSeverity.repr }

@[implicit_reducible]

instance instInhabitedSeverity : Inhabited Severity

Equations

• instInhabitedSeverity = { default := instInhabitedSeverity.default }

def instBEqSeverity.beq : Severity → Severity → Bool

Equations

• instBEqSeverity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance instBEqSeverity : BEq Severity

Equations

• instBEqSeverity = { beq := instBEqSeverity.beq }

def instHashableSeverity.hash : Severity → UInt64

Equations

• instHashableSeverity.hash Severity.error = 0
• instHashableSeverity.hash Severity.warning = 1

@[implicit_reducible]

instance instHashableSeverity : Hashable Severity

Equations

• instHashableSeverity = { hash := instHashableSeverity.hash }

def instOrdSeverity.ord : Severity → Severity → Ordering

Equations

• instOrdSeverity.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance instOrdSeverity : Ord Severity

Equations

• instOrdSeverity = { compare := instOrdSeverity.ord }

def Severity.letter : Severity → Char

The letter this severity's codes start with.

Equations

• Severity.error.letter = 'E'
• Severity.warning.letter = 'W'

structure DiagnosticCode : Type

A diagnostic's code: a severity and a four-digit number, e.g. E0042.

A structure over Fin 10000 rather than a String, so a malformed code cannot be constructed in the first place — every code that exists renders in the one canonical form, and explain's argument either parses into this type or was never a code at all.

• severity : Severity

  Error or warning.

• number : Fin 10000

  The number, unique within the whole compiler (not per severity, not per stage).

def instDecidableEqDiagnosticCode.decEq (x✝ x✝¹ : DiagnosticCode) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDiagnosticCode.decEq { severity := a, number := a_1 } { severity := b, number := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqDiagnosticCode : DecidableEq DiagnosticCode

Equations

• instDecidableEqDiagnosticCode = instDecidableEqDiagnosticCode.decEq

@[implicit_reducible]

instance instReprDiagnosticCode : Repr DiagnosticCode

Equations

• instReprDiagnosticCode = { reprPrec := instReprDiagnosticCode.repr }

def instReprDiagnosticCode.repr : DiagnosticCode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instInhabitedDiagnosticCode : Inhabited DiagnosticCode

Equations

• instInhabitedDiagnosticCode = { default := instInhabitedDiagnosticCode.default }

def instBEqDiagnosticCode.beq : DiagnosticCode → DiagnosticCode → Bool

Equations

• instBEqDiagnosticCode.beq { severity := a, number := a_1 } { severity := b, number := b_1 } = (a == b && a_1 == b_1)
• instBEqDiagnosticCode.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqDiagnosticCode : BEq DiagnosticCode

Equations

• instBEqDiagnosticCode = { beq := instBEqDiagnosticCode.beq }

@[implicit_reducible]

instance instHashableDiagnosticCode : Hashable DiagnosticCode

Equations

• instHashableDiagnosticCode = { hash := instHashableDiagnosticCode.hash }

def instHashableDiagnosticCode.hash : DiagnosticCode → UInt64

Equations

• instHashableDiagnosticCode.hash { severity := a, number := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance instOrdDiagnosticCode : Ord DiagnosticCode

Equations

• instOrdDiagnosticCode = { compare := instOrdDiagnosticCode.ord }

def instOrdDiagnosticCode.ord : DiagnosticCode → DiagnosticCode → Ordering

Equations

• instOrdDiagnosticCode.ord { severity := a, number := a_1 } { severity := b, number := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

def DiagnosticCode.toString (c : DiagnosticCode) : String

E0042: the letter, then the number padded to four digits.

Equations

• c.toString = toString c.severity.letter ++ toString (String.replicate (4 - (toString ↑c.number).length) '0') ++ toString (toString ↑c.number)

@[implicit_reducible]

instance DiagnosticCode.instToString : ToString DiagnosticCode

Equations

• DiagnosticCode.instToString = { toString := DiagnosticCode.toString }

def DiagnosticCode.ofString? (s : String) : Option DiagnosticCode

Parse a code back from its printed form; none if s is not one. Strict: the letter must be E/W, and exactly four digits must follow — E42 and banana are both simply not codes.

Equations

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