The output of PlusCal statement checking. ElaboratedPlusCal.Statement/Block/Branches/ Declarations/Process/Algorithm mirror CorePlusCal's shape node-for-node, but parameterized over (τ ε : Type) rather than CorePlusCal's (α β : Type): Ref carries an extra resolved type : τ, and Statement.receive an extra coe : TypedTLAPlus.Coercion, so a later pass (WellFormedness/Restrictions.lean check 1) can tell whether a bare Ref position (assign's LHS, receive's destination) is Channel-shaped without Γ, which is gone by then. Coercion isn't a third parameter — its shape is TLA⁺-expression-specific regardless of instantiation.

TypedPlusCal pins this layer at τ := TypedTLAPlus.Typ, ε := TypedTLAPlus.Expression TypedTLAPlus.Typ. Core/ComputablePlusCal/Syntax.lean pins the same layer at ComputableTLAPlus's types, reusing these definitions rather than re-copying them: neither Ref.type nor receive's Coercion field change shape across the two, so no second monomorphic copy is needed. Multicast is reused generically from CorePlusCal (its target is a bare String, not a Ref, so no type to carry either way).

structure ElaboratedPlusCal.Ref (τ ε : Type) : Type

Carries its own resolved baseType (unlike CorePlusCal.Ref). args follows CorePlusCal.Ref's shape: one entry per path segment, .inl for a .field segment, .inr for a (unary) bracket-index segment.

baseType is the base variable's type (name's Γ-lookup result), before any .args segment is applied — kept this way rather than the result type because the result type is always cheap to recompute from baseType (Ref.stepType/.resultType below), but recovering baseType from the result type isn't possible in general (a record access or tuple projection isn't invertible).

• name : String
• args : List (String ⊕ ε)
• baseType : τ

def ElaboratedPlusCal.instReprRef.repr {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Ref τ✝ ε✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElaboratedPlusCal.instReprRef {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Repr (Ref τ✝ ε✝)

Equations

• ElaboratedPlusCal.instReprRef = { reprPrec := ElaboratedPlusCal.instReprRef.repr }

@[reducible, inline]

abbrev ElaboratedPlusCal.Multicast (τ ε : Type) : Type

CorePlusCal.Multicast, reused generically.

Equations

• ElaboratedPlusCal.Multicast τ ε = CorePlusCal.Multicast τ ε

inductive ElaboratedPlusCal.Statement (τ ε : Type) : Bool → Type

A fresh copy of CorePlusCal.Statement's shape, not an abbrev over it: parameterized over (τ ε : Type) instead of (α β : Type), since receive needs an extra field CorePlusCal.Statement.receive has no room for.

• goto {τ ε : Type} (label : String) : Statement τ ε true
• skip {τ ε : Type} : Statement τ ε false
• print {τ ε : Type} (e : ε) : Statement τ ε false
• assign {τ ε : Type} : List (Ref τ ε × ε) → Statement τ ε false
• if {τ ε : Type} {b : Bool} (cond : ε) (B₁ B₂ : Block τ ε b) : Statement τ ε b
• await {τ ε : Type} (e : ε) : Statement τ ε false
• with {τ ε : Type} (var : String) (ann : τ) («=|∈» : Bool) (val : ε) (B : Block τ ε false) : Statement τ ε false
• assert {τ ε : Type} (e : ε) : Statement τ ε false
• either {τ ε : Type} {b : Bool} (branches : Branches τ ε b) : Statement τ ε b
• while {τ ε : Type} {b : Bool} (cond : ε) (B : Block τ ε b) : Statement τ ε false
• receive {τ ε : Type} (c r : Ref τ ε) (coe : TypedTLAPlus.Coercion) : Statement τ ε false

  Differs from CorePlusCal.Statement.receive by coe: the checked element→reference-type upcast for the value read off the channel at runtime.

• send {τ ε : Type} (c : Ref τ ε) (e : ε) : Statement τ ε false
• multicast {τ ε : Type} (c : String) (filter : Multicast τ ε) : Statement τ ε false

@[implicit_reducible]

instance ElaboratedPlusCal.instReprBranches {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Repr (Branches τ✝ ε✝ a✝)

Equations

• ElaboratedPlusCal.instReprBranches = { reprPrec := ElaboratedPlusCal.instReprBranches.repr_3 }

partial def ElaboratedPlusCal.instReprBranches.repr_2 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Block τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprBlock.repr_1 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Statement τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprStatement.repr_1 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Statement τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprBranches.repr_1 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Statement τ✝ ε✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance ElaboratedPlusCal.instReprStatement {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Repr (Statement τ✝ ε✝ a✝)

Equations

• ElaboratedPlusCal.instReprStatement = { reprPrec := ElaboratedPlusCal.instReprStatement.repr_1 }

partial def ElaboratedPlusCal.instReprStatement.repr_2 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Block τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprBlock.repr_3 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Branches τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprBranches.repr_3 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Branches τ✝ ε✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance ElaboratedPlusCal.instReprBlock {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Repr (Block τ✝ ε✝ a✝)

Equations

• ElaboratedPlusCal.instReprBlock = { reprPrec := ElaboratedPlusCal.instReprBlock.repr_2 }

partial def ElaboratedPlusCal.instReprBlock.repr_2 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Block τ✝ ε✝ a✝ → ℕ → Std.Format

partial def ElaboratedPlusCal.instReprStatement.repr_3 {τ✝ ε✝ : Type} {a✝ : Bool} [Repr τ✝] [Repr ε✝] : Branches τ✝ ε✝ a✝ → ℕ → Std.Format

inductive ElaboratedPlusCal.Block (τ ε : Type) : Bool → Type

A fresh copy of CorePlusCal.Block's shape.

• mk {τ ε : Type} {b : Bool} (begin : List (Statement τ ε false)) («end» : Statement τ ε b) : Block τ ε b

inductive ElaboratedPlusCal.Branches (τ ε : Type) : Bool → Type

A fresh copy of CorePlusCal.Branches's shape.

• either {τ ε : Type} {b : Bool} : Block τ ε b → Branches τ ε b
• or {τ ε : Type} {b : Bool} : Block τ ε b → Branches τ ε b → Branches τ ε b

@[reducible, inline]

abbrev ElaboratedPlusCal.Block.begin {τ ε : Type} {b : Bool} : Block τ ε b → List (Statement τ ε false)

Equations

• (ElaboratedPlusCal.Block.mk begin «end»).begin = begin

@[reducible, inline]

abbrev ElaboratedPlusCal.Block.end {τ ε : Type} {b : Bool} : Block τ ε b → Statement τ ε b

Equations

• (ElaboratedPlusCal.Block.mk begin «end»).end = «end»

def ElaboratedPlusCal.Block.forStatements {τ ε : Type} {b : Bool} {m : Type → Type} [Monad m] (act : {b' : Bool} → Statement τ ε b' → m Unit) (B : Block τ ε b) : m Unit

Runs act over every non-terminal statement in B (B.begin, in order), then its terminal one (B.end). Shared shape for WellFormedness's per-check walkers (Restrictions.checkRestrictions, WellScoped.checkWellScoped, Labelling.checkGotoTargets), each supplying its own act.

Equations

• ElaboratedPlusCal.Block.forStatements act B = do B.begin.forM act act B.end

def ElaboratedPlusCal.Branches.forStatements {τ ε : Type} {b : Bool} {m : Type → Type} [Monad m] (act : {b' : Bool} → Statement τ ε b' → m Unit) : Branches τ ε b → m Unit

Block.forStatements, distributed over either/or branches.

Equations

• One or more equations did not get rendered due to their size.
• ElaboratedPlusCal.Branches.forStatements act (ElaboratedPlusCal.Branches.either B) = ElaboratedPlusCal.Block.forStatements (fun {b' : Bool} => act) B

partial def ElaboratedPlusCal.Statement.forEachNode {τ ε : Type} {b : Bool} {m : Type → Type} [Monad m] (act : {b' : Bool} → Statement τ ε b' → m Unit) (s : Statement τ ε b) : m Unit

Pre-order recursion over s and every statement nested inside it: act s first, then the same over whatever if/either/while/with nest below — the four constructors that embed a Block/Branches; every other statement is a leaf. The structural half of what a per-node check needs, so a check that has no context to thread supplies only the check itself (WellFormedness/Labelling.lean) rather than restating this recursion.

A check whose per-node work depends on where it is in the tree can't use this — WellFormedness/ WellScoped/TypedPlusCal.lean extends its in-scope set at every with binder, which needs the recursion and the check interleaved, so it keeps its own copy.

partial: the recursion isn't visibly decreasing to Lean through the Block/Branches nesting, same as every other walker over this type.

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedStatement {τ ε : Type} {b : Bool} : Inhabited (Statement τ ε b)

Equations

• ElaboratedPlusCal.instInhabitedStatement = { default := ElaboratedPlusCal.Statement.goto Inhabited.default }
• ElaboratedPlusCal.instInhabitedStatement = { default := ElaboratedPlusCal.Statement.skip }

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedBlock {τ ε : Type} {b : Bool} : Inhabited (Block τ ε b)

Equations

• ElaboratedPlusCal.instInhabitedBlock = { default := ElaboratedPlusCal.Block.mk Inhabited.default Inhabited.default }

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedBranches {τ ε : Type} {b : Bool} : Inhabited (Branches τ ε b)

Equations

• ElaboratedPlusCal.instInhabitedBranches = { default := ElaboratedPlusCal.Branches.either Inhabited.default }

structure ElaboratedPlusCal.Declarations (τ ε : Type) : Type

A fresh copy of CorePlusCal.Declarations's shape.

• variables : List (String × τ × Bool × Option (Bool × ε))
• channels : List (String × τ × List ε)
• fifos : List (String × τ × List ε)

def ElaboratedPlusCal.instReprDeclarations.repr {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Declarations τ✝ ε✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElaboratedPlusCal.instReprDeclarations {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Repr (Declarations τ✝ ε✝)

Equations

• ElaboratedPlusCal.instReprDeclarations = { reprPrec := ElaboratedPlusCal.instReprDeclarations.repr }

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedDeclarations {a✝ a✝¹ : Type} : Inhabited (Declarations a✝ a✝¹)

Equations

• ElaboratedPlusCal.instInhabitedDeclarations = { default := ElaboratedPlusCal.instInhabitedDeclarations.default }

structure ElaboratedPlusCal.Process (τ ε : Type) : Type

A fresh copy of CorePlusCal.Process's shape.

• mailbox : Option (String × List ε)
• isFair : Bool
• name : String
• =|∈ : Bool
• id : ε
• localState : Declarations τ ε
• threads : List (List (String × Block τ ε true))

@[implicit_reducible]

instance ElaboratedPlusCal.instReprProcess {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Repr (Process τ✝ ε✝)

Equations

• ElaboratedPlusCal.instReprProcess = { reprPrec := ElaboratedPlusCal.instReprProcess.repr }

def ElaboratedPlusCal.instReprProcess.repr {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Process τ✝ ε✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedProcess {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (Process a✝ a✝¹)

Equations

• ElaboratedPlusCal.instInhabitedProcess = { default := ElaboratedPlusCal.instInhabitedProcess.default }

structure ElaboratedPlusCal.Algorithm (τ ε : Type) : Type

A fresh copy of CorePlusCal.Algorithm's shape.

• isFair : Bool
• name : String
• globalState : Declarations τ ε
• processes : List (Process τ ε)

@[implicit_reducible]

instance ElaboratedPlusCal.instReprAlgorithm {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Repr (Algorithm τ✝ ε✝)

Equations

• ElaboratedPlusCal.instReprAlgorithm = { reprPrec := ElaboratedPlusCal.instReprAlgorithm.repr }

def ElaboratedPlusCal.instReprAlgorithm.repr {τ✝ ε✝ : Type} [Repr τ✝] [Repr ε✝] : Algorithm τ✝ ε✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElaboratedPlusCal.instInhabitedAlgorithm {a✝ a✝¹ : Type} : Inhabited (Algorithm a✝ a✝¹)

Equations

• ElaboratedPlusCal.instInhabitedAlgorithm = { default := ElaboratedPlusCal.instInhabitedAlgorithm.default }

def ElaboratedPlusCal.Process.forStatements {τ ε : Type} {m : Type → Type} [Monad m] (act : {b' : Bool} → Statement τ ε b' → m Unit) (p : Process τ ε) : m Unit

Runs act over the top-level statements of every labelled block of every thread of p — the threads/(label, Block) nesting flattened away. Only the top-level statements: act is whatever the caller wants per block, Statement.forEachNode if it wants the whole subtree.

Per process, not per algorithm, because all three callers need it that way: labels (WellFormedness/Labelling.lean) and in-scope names (WellFormedness/WellScoped/TypedPlusCal. lean) are both process-scoped, and WellFormedness/Reachability.lean visits a process's own id/mailbox/localState expressions in the same loop.

Equations

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

@[reducible, inline]

abbrev TypedPlusCal.Expression : Type

Checked PlusCal expressions — always TypedTLAPlus.Expression at the checker's own Typ.

Equations

• TypedPlusCal.Expression = TypedTLAPlus.Expression TypedTLAPlus.Typ

@[reducible, inline]

abbrev TypedPlusCal.Ref : Type

Equations

• TypedPlusCal.Ref = ElaboratedPlusCal.Ref TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Multicast : Type

Equations

• TypedPlusCal.Multicast = ElaboratedPlusCal.Multicast TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Statement : Bool → Type

Equations

• TypedPlusCal.Statement = ElaboratedPlusCal.Statement TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Block : Bool → Type

Equations

• TypedPlusCal.Block = ElaboratedPlusCal.Block TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Branches : Bool → Type

Equations

• TypedPlusCal.Branches = ElaboratedPlusCal.Branches TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Declarations : Type

Equations

• TypedPlusCal.Declarations = ElaboratedPlusCal.Declarations TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Process : Type

Equations

• TypedPlusCal.Process = ElaboratedPlusCal.Process TypedTLAPlus.Typ TypedPlusCal.Expression

@[reducible, inline]

abbrev TypedPlusCal.Algorithm : Type

Equations

• TypedPlusCal.Algorithm = ElaboratedPlusCal.Algorithm TypedTLAPlus.Typ TypedPlusCal.Expression

def TypedPlusCal.Ref.stepType (τ : TypedTLAPlus.Typ) : String ⊕ Expression → TypedTLAPlus.Typ

The type after one Ref path segment, given the type before it. A pure structural pattern match — every segment is already elaborated, so this replays the same step-rule Elaborator/Expressions.lean's stepInto/indexInto use at check time, without re-checking. Total: the fallback (τ unchanged) only triggers on a Ref no well-typed input can produce.

Equations

• TypedPlusCal.Ref.stepType (SurfaceTLAPlus.Typ.record fs) (Sum.inl field) = (List.lookup field fs).getD (SurfaceTLAPlus.Typ.record fs)
• TypedPlusCal.Ref.stepType τ (Sum.inl field) = τ
• TypedPlusCal.Ref.stepType (x_1.function rng) (Sum.inr idx) = rng
• TypedPlusCal.Ref.stepType elem.seq (Sum.inr idx) = elem
• TypedPlusCal.Ref.stepType (SurfaceTLAPlus.Typ.tuple τs) (Sum.inr (TypedTLAPlus.Expression.nat n)) = (n.toNat?.bind fun (x : ℕ) => τs[x - 1]?).getD (SurfaceTLAPlus.Typ.tuple τs)
• TypedPlusCal.Ref.stepType (SurfaceTLAPlus.Typ.tuple τs) (Sum.inr idx) = SurfaceTLAPlus.Typ.tuple τs
• TypedPlusCal.Ref.stepType τ (Sum.inr idx) = τ

def TypedPlusCal.Ref.resultType (r : Ref) : TypedTLAPlus.Typ

A Ref's final/result type — what assign r e/receive c r check e's type against — recomputed from baseType by walking args left to right via stepType.

Equations

• r.resultType = List.foldl TypedPlusCal.Ref.stepType r.baseType r.args