Desugarer.Errors

source

inductive DesugarError :

Type

Errors produced while desugaring SurfaceTLAPlus/SurfacePlusCal into CoreTLAPlus/CorePlusCal.

misplacedAt (pos : SourceSpan) : DesugarError
@ used outside of an EXCEPT update.
gotoNotInTailPosition (pos : SourceSpan) : DesugarError
A goto is followed by more unlabelled statements — unreachable dead code (a goto followed by a label is fine).
unlabelledStatement (pos : SourceSpan) : DesugarError
A statement appears before the first label of its enclosing thread — there is no label to attach it (or the block it starts) to.
nestedLabel (pos : SourceSpan) : DesugarError
A label appears inside a with body — never allowed, since a with binding only makes sense within one atomic step.
whileInWith (pos : SourceSpan) : DesugarError
A while statement appears inside a with body, at any nesting depth.
whileNotLabelled (pos : SourceSpan) : DesugarError
A while statement is not immediately preceded by a real, user-written label; none is auto-inserted.
notFollowedByLabel (pos : SourceSpan) : DesugarError
A statement following an if/either that contains a labelled statement or a goto anywhere within it is not itself labelled.
withBoundVarWritten (pos : SourceSpan) (name : String) : DesugarError
A statement writes into a variable currently bound by an enclosing with — an assign target or a receive's target Ref. A with-bound name is a fixed local binding, not a process variable, so writing to it is meaningless.
wrongAnnotationKindAtSite (pos : SourceSpan) (found expected : String) : DesugarError
An annotation-carrying slot only accepts specific kinds of annotation, but a different kind was found there.
duplicateAnnotation (pos : SourceSpan) (kind : String) : DesugarError
Two or more annotations of the same kind found at one slot, for a kind whose content can actually differ between instances (@type, @mailbox). Content-free markers (@parameter) get a warning instead (DesugarWarning.duplicateParameterAnnotation).
conflictingAssignment (pos : SourceSpan) (name : String) : DesugarError
The same bare variable (no index — x, not x[…]) is written more than once within one atomic step (assign/receive, any combination), on the same control path. Indexed writes (x[0] := …) aren't tracked by this check.
invalidRecordFieldAccess (pos : SourceSpan) : DesugarError
The right-hand side of a record-access . is not a bare field-name identifier (e.g. r.1, r.(f)).

Instances For

source

@[implicit_reducible]

instance instCompilerDiagnosticDesugarErrorString :

CompilerDiagnostic DesugarError String

Equations

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

source

inductive DesugarWarning :

Type

Non-fatal issues found while desugaring — collected out-of-band and filtered/printed once desugaring returns (Driver/Modules.lean's compileModule).

duplicateParameterAnnotation (pos : SourceSpan) : DesugarWarning
A @parameter marker repeated on the same variable — content-free, so a warning rather than DesugarError.duplicateAnnotation.
partialMulticastAnnotation (pos : SourceSpan) : DesugarWarning
A multicast filter whose components carry @type annotations on some binds but not all. The desugarer collapses the components into one binder over their Cartesian product, whose declared type is the tuple of theirs — which it can only build when every component supplies one. The annotations that were written are dropped, and the recipient's type comes from the channel's own declared domain instead.