Statement desugaring: SurfacePlusCal's implicit-fallthrough statement lists become
CorePlusCal's explicit-goto, type-indexed-terminal Blocks.
A label may appear inside an if/while/either body, not just at a thread's top level: it
marks the start of a new addressable atomic block, so it is extracted into its own top-level
(label, Block) entry, with explicit gotos stitching control flow back together. with is
the one exception — its body never allows a nested label, goto, or while, and one found
there is a hard error.
A goto may only appear as the last statement of its enclosing list. A while must be
immediately preceded by a real label; none is auto-inserted. An if/either containing a
label or goto must itself be followed by a real label; none is synthesized.
If a thread's last label runs out of statements without an explicit terminal, goto Done is
inserted — "Done" is a reserved sentinel needing no matching label definition.
ownLabel/fallthrough and WithContext's bound-variable list are Reader effects
(SegmentContext/WithContext below); acc — the segment's own accumulated statements —
stays an explicit fold parameter.
Names currently bound by an enclosing with (innermost first; order doesn't matter),
threaded as a Reader through Statement.desugarLabelFree and friends. Nested withs
accumulate rather than replace. Used to reject a while, or a write (assign/receive)
targeting a with-bound name — a fixed local binding, not a process variable.
Instances For
The Reader context desugarSegment threads through its recursion: which label (if any)
owns the segment being built (none for an if/either branch, which has no address of its
own), and where to goto if the segment runs out of statements without an explicit redirect.
- fallthrough : String
Instances For
Equations
The concrete expression type used once β is fixed to CoreTLAPlus.Expression.
Equations
Instances For
The annotation slot every PlusCal node carries through desugaring: the raw comment
annotations parsed at each site, which stripEmbeddedTypeAnnotations later turns into an
Option Typ. Pinned rather than left generic, matching Declarations.desugarCheck below —
collapsing a multicast filter has to read @type off each component and build one for the
binder it synthesizes, which no generic annotation type allows.
Equations
Instances For
x[e₁, …, eₙ]'s indices, per bracket group, collapsed to CorePlusCal.Ref's own unary
shape via SurfaceTLAPlus.wrapIndices; .field segments pass through unchanged. pos is the
enclosing statement's own position.
No @@ here: Ref is not a position-carrying node in this codebase (neither
CorePlusCal.Ref's Functor/Traversable instances nor any downstream pass registers one),
and every diagnostic about a Ref is reported against its enclosing statement's span.
Equations
- SurfacePlusCal.Ref.desugarRef pos r = { name := r.name, args := List.map (Sum.map id (SurfaceTLAPlus.wrapIndices pos)) r.args }
Instances For
Collapse a multicast's surface filter to CorePlusCal.Multicast's single binder.
multicast(c, [x₁ ⋈₁ e₁, …, xₙ ⋈ₙ eₙ ↦ v]) reaches every c[y] for y in the Cartesian
product of the components, an ∈-bind contributing its own set and an =-bind the singleton
{e} — so the components name the parts of a recipient tuple and do not scope over one
another. One component is already that binder. Several collapse to a fresh one over
D₁ \X … \X Dₙ, with each original name rewritten in v to its projection off it, exactly as
SurfaceTLAPlus.collapseToSingleBinder does for a multi-binder function literal.
The synthesized binder's declared type is the tuple of the components' own, which is available
only when every one of them carries a @type; a filter annotating some but not all warns
(partialMulticastAnnotation) and keeps none, the recipient's type being fixed by the
channel's declared domain regardless. Annotations of other kinds on a collapsed component are
dropped with it — stripEmbeddedTypeAnnotations is what would otherwise reject them, and
there is no longer a site for them to sit at.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Does this statement need the extraction-capable desugaring path (desugarSegment) rather
than the cheap always-non-terminal one (desugarLabelFreeBlock)? True if a label appears
anywhere within it, an if/either branch or while body ends in a bare goto, or a
while appears anywhere. A with body never needs extraction.
Declared at the root List namespace so dot-notation on a List (String ⊕ Statement CoreAnn β) resolves to it. true as soon as a label is found anywhere, the last element is a bare
goto, any statement (Statement.needsExtraction) does, or a while appears in the list.
Reject any statement-list entry that is a label — used for with bodies, the one
construct real PlusCal never allows a label inside.
Equations
- SurfacePlusCal.rejectLabels [] = pure []
- SurfacePlusCal.rejectLabels (Sum.inl l :: tail) = throw (DesugarError.nestedLabel (posOf l))
- SurfacePlusCal.rejectLabels (Sum.inr s :: rest) = (fun (x : List (SurfacePlusCal.Statement SurfacePlusCal.CoreAnn β)) => s :: x) <$> SurfacePlusCal.rejectLabels rest
Instances For
Flatten a multi-binder with (x = e, y ∈ S, …) { … } into a nested chain of single-binder
CorePlusCal.Statement.withs (with (x = e) { with (y ∈ S) { … } }) — CorePlusCal.Statement. with only ever binds one variable at a time (Core/CorePlusCal/Syntax.lean's module doc).
Every binder past the first is wrapped in its own label-free Block (⟨[], ·⟩) around the
next binder, with B — the already-desugared body — innermost.
Every link of the chain is registered at pos, the whole surface with's own span: the chain
is one source construct, and no binder past the first has a narrower span of its own to
report.
Equations
- SurfacePlusCal.buildWithChain pos [] B = panicWithPosWithDecl "Desugarer.PlusCal" "SurfacePlusCal.buildWithChain" 171 12 "unreachable code has been reached"
- SurfacePlusCal.buildWithChain pos [(x, ann, eq, e)] B = CorePlusCal.Statement.with x ann eq e B @@ pos
- SurfacePlusCal.buildWithChain pos ((x, ann, eq, e) :: rest) B = CorePlusCal.Statement.with x ann eq e (CorePlusCal.Block.mk [] (SurfacePlusCal.buildWithChain pos rest B)) @@ pos
Instances For
Desugar a statement known not to be last in its enclosing sequence and known to need no
extraction anywhere inside it: always yields a non-terminal (false) CorePlusCal.Statement,
with if/while/either's sub-blocks recursing via desugarLabelFreeBlock.
Reads WithContext for which names are currently with-bound. A while is rejected outright
if any are bound (whileInWith); an assign or receive targeting a bound name is likewise
rejected (withBoundVarWritten).
Desugar a statement-list known to be entirely label-free into a non-terminal block:
every entry desugars via Statement.desugarLabelFree, except the last, whose own natural
terminality (a bare goto, or an if/either that recursively is) is preserved.
Turn a list of desugared branch-blocks into CorePlusCal.Branches.
Equations
- SurfacePlusCal.buildBranches [] = panicWithPosWithDecl "Desugarer.PlusCal" "SurfacePlusCal.buildBranches" 237 12 "unreachable code has been reached"
- SurfacePlusCal.buildBranches [b] = CorePlusCal.Branches.either b
- SurfacePlusCal.buildBranches (b :: bs) = CorePlusCal.Branches.or b (SurfacePlusCal.buildBranches bs)
Instances For
Desugar stmts — content directly following a label, per the ambient SegmentContext's
ownLabel (if this call is processing exactly that; none for an if/either branch, which
has no address of its own) — into the terminal CorePlusCal.Block for this segment, plus every
(label, Block) pair extracted from labels nested within it (if/while/either bodies).
SegmentContext.fallthrough is where to implicitly goto once the segment (or its last
extracted continuation) runs out of statements without an explicit redirect.
acc accumulates the segment's own non-terminal statements so far, in order — an explicit
parameter rather than folded into the Reader context (module doc above).
Desugar one parallel thread ({...} block) into its sequence of labelled, terminal
CorePlusCal.Blocks — the thread's own top-level labels plus everything extracted from
nested labels within if/while/either bodies.
Equations
- One or more equations did not get rendered due to their size.
- SurfacePlusCal.Thread.desugar [] = pure []
- SurfacePlusCal.Thread.desugar (Sum.inr s :: tail) = throw (DesugarError.unlabelledStatement (posOf s))
Instances For
Validate and extract a Process.ann slot: at most one @mailbox, nothing else, with its
filter arguments fully desugared (desugarMailboxArg).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Validate @parameter's placement (only on a ∈-initialized entry) and extract its
presence into the dedicated isParameter field — a repeated @parameter is a warning, not
an error. Every other annotation is left untouched in α for stripEmbeddedTypeAnnotations
to validate later.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Desugar one process: goto-explicitize its threads (Thread.desugar) and validate/extract
its @mailbox annotation (extractMailbox) and its local declarations' @parameter
annotations (Declarations.desugarCheck).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Desugar a whole algorithm: its global declarations (Declarations.desugarCheck) and
every process (Process.desugar).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checks that no two assignments write the same base variable within one atomic step, on the
same control path, regardless of indexing (checkWrite above) — from both of assign's and
receive's Refs (the channel counts as a write too, not just the target). if/either
branches are separate control paths, checked independently from the same starting set, with
their writes unioned into what continues past them.
while is not handled the same way: its body never contributes to what follows it, full
stop, not "unless it diverges" the way a naive if-shaped treatment might suggest. Every
PlusCal while iteration is its own atomic step — why a label is required immediately before
one (RejectWhileNonfreshExtraction.tla/AcceptWhileFreshReuse.tla) — so "the loop's body
ran" and "control reached the code after the loop" are never part of the same atomic step, no
matter what the body contains or how it ends. (This used to propagate the body's writes
forward unconditionally, which is what made E0018 fire on, e.g.,
while (c) { x := 0; l: … }; x := 1; — flagging two writes that can never coexist on one
execution as if they were sequential; AcceptConflictingAssignAcrossWhileExit.tla pins the
fix.) The body is still checked for conflicts within itself, same as any other block.
if/either do not get the same "body can leave through a goto, so don't propagate its
writes" treatment, even though a branch certainly can end in one. The desugarer
(Thread.desugar's desugarContinuation, above) requires a real label immediately after any
if/either whose branch needs extraction (contains a goto or an internal label) — so
whenever a branch's own writes could wrongly merge with sibling code in the same block, that
sibling code cannot exist: it would already have been rejected as notFollowedByLabel, or
pulled out to its own labelled block. Equivalently, in the type (Core/CorePlusCal/Syntax.lean):
a Block's begin entries are always Statement _ _ false, so an if/either with more
code after it in the same block is thereby b = false — and since if/either share one b
across all their branches, every branch is b = false there too, never diverging. A branch
that is allowed to diverge only occurs where the if/either is itself a block's own tail,
where there is no "what follows in this block" to propagate into to begin with. Unlike
while's body, which is a genuinely separate Block with its own independent b — nothing
ties it to whatever follows the while — an if/either branch's divergence and "is there
more in this block" are the same fact, so no extra check is needed here.
Run checkAssignConflicts over every atomic step (one top-level (label, Block) pair per
thread) of a whole algorithm — each starts with a fresh, empty seen set, since crossing a
label is exactly crossing an atomic-step boundary.
DiagT … Id rather than a bare Except, for the same reason as
CoreTLAPlus.Module.stripTLAPlusAnnotations (Desugarer/TLAPlus.lean): one MonadDiagnostic
shape for every entry point, absorbed by the caller with DiagT.lift. Emits no warnings today.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Validate and strip every remaining @type-only annotation slot in an already
Process.desugar/Declarations.desugarCheck-processed algorithm, using the same extractType
(Desugarer/TLAPlus.lean) as the TLA⁺ side — and, like it, reports through DiagT … Id rather
than a bare Except.
Equations
Instances For
Run statement desugaring (fused with @mailbox/@parameter checking/extraction) against the
concrete monad it needs: WithContext's and SegmentContext's Readers, plus MonadDiagnostic
for error reporting and the List DesugarWarning accumulator — instantiated at DiagT, so a
warning emitted before a later fatal error still survives. Also runs
CorePlusCal.Algorithm.checkAssignConflicts before stripEmbeddedTypeAnnotations, so the
returned CorePlusCal.Algorithm is fully checked with every annotation slot resolved — both run
after warnings are already extracted, since neither touches them. The base monad n stays
abstract for the same reason as Desugarer/TLAPlus.lean's runDesugarer: the fresh-name counter
it needs belongs to one compile, not to the process.
Equations
- a.runDesugarer = do let algo ← (a.desugar.run { }).run Inhabited.default DiagT.lift id id algo.checkAssignConflicts DiagT.lift id id algo.stripEmbeddedTypeAnnotations