Driver/Modules.lean's errors/warnings — every way driving the pipeline up to and including the checker can fail. Wraps each lower-level pass's own error type (lex/parse/annotation/ desugar/typeCheck) plus the resolution-specific conditions (moduleNotFound/ ambiguousModule/cyclicExtends), so Fugue.lean only has to handle one error type for the driver's portion of the pipeline. Passes past the checker (WellFormedness, Typed2Computable, everything after) run outside the driver, on its returned TypedModule, and report through their own error types directly — not wrapped here.

inductive DriverError : Type

moduleId is the offending module's own key into the source registry (Driver/Modules.lean's MonadSourceRegistry) — not necessarily the main module's: an error inside an EXTENDS-ed dependency must render against that dependency's own lines, not whichever module the compile started from.

• lex (moduleId : String) (e : Unexpected Char) : DriverError

  A lexing failure.

• parse (moduleId : String) (e : Unexpected (SurfaceTLAPlus.Token (Located' SurfacePlusCal.Token))) : DriverError

  A parsing failure.

• annotation (moduleId : String) (e : ResolverError) : DriverError

  A @type/@mailbox/@parameter annotation-resolution failure.

• desugar (moduleId : String) (e : DesugarError) : DriverError

  A Surface→Core desugaring failure (TLA⁺ expressions or the embedded PlusCal algorithm).

• moduleNotFound (name : String) : DriverError

  EXTENDS name didn't resolve to any file (searched: the extending module's own directory, -I's search path, and the builtin table).

• ambiguousModule (name : String) (foundAt : List String) : DriverError

  EXTENDS name resolved to more than one candidate — no silent shadowing.

• cyclicExtends (chain : List String) : DriverError

  EXTENDS forms a cycle; chain is the resolution stack at the point the cycle was found, outermost first, with the repeated name appended at the end for a readable A -> B -> A.

• moduleNameMismatch (moduleId declared expected : String) : DriverError

  The file declares MODULE declared but is named after expected. TLA⁺ requires the two to agree — EXTENDS Foo looks for Foo.tla and nothing else — so a mismatch means the module is unreachable by any other module, however well it compiles on its own.

• typeCheck (moduleId : String) (e : TCError) : DriverError

  A real type-checking failure.

@[implicit_reducible]

instance instCompilerDiagnosticDriverErrorString : CompilerDiagnostic DriverError String

Equations

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

inductive DriverWarning : Type

DriverError's non-fatal counterpart — carries a warning from any pass, plus its owning moduleId, through Driver/Modules.lean's accumulate-then-flush machinery.

• parser (moduleId : String) (w : ParserWarning) : DriverWarning
• desugar (moduleId : String) (w : DesugarWarning) : DriverWarning
• typeCheck (moduleId : String) (w : TCWarning) : DriverWarning
• extendsAlgorithm (moduleId dep : String) (span : SourceSpan) : DriverWarning

  EXTENDS dep, where dep has a PlusCal algorithm of its own. EXTENDS imports declarations, never an algorithm, so that algorithm is silently absent from the extending module — and the extending module is the one that has to change, which is why moduleId is its key and span is the dep identifier in its EXTENDS clause rather than anything in the file the algorithm is in.

  Carries the span outright instead of leaving the caller to posOf the name at render time: positions are keyed on a value's address (Common/Position.lean), and by then the parsed EXTENDS list may be gone.

def DriverWarning.name : DriverWarning → String

The -W<name>/-Wno-<name> name a given warning is filtered under — forwards to whichever wrapped warning's own .name, except for the driver's own warnings, which name their registry entry directly.

Equations

• (DriverWarning.parser moduleId w).name = w.name
• (DriverWarning.desugar moduleId w).name = w.name
• (DriverWarning.typeCheck moduleId w).name = w.name
• (DriverWarning.extendsAlgorithm moduleId dep span).name = Diagnostics.extendsAlgorithm.warningName

def DriverWarning.moduleId : DriverWarning → String

The moduleId a given warning is tagged with — every variant carries one, unlike DriverError (whose moduleNotFound/ambiguousModule/cyclicExtends carry none).

Equations

• (DriverWarning.parser moduleId w).moduleId = moduleId
• (DriverWarning.desugar moduleId w).moduleId = moduleId
• (DriverWarning.typeCheck moduleId w).moduleId = moduleId
• (DriverWarning.extendsAlgorithm moduleId dep span).moduleId = moduleId

@[implicit_reducible]

instance instCompilerDiagnosticDriverWarningString : CompilerDiagnostic DriverWarning String

Equations

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