SurfacePlusCal, but with every goto explicit and at the end of a block — the output of statement desugaring.

Statement/Block/Branches are indexed by a Bool tracking whether a statement/block is "terminal" (ends in goto) at the type level: "every block ends in exactly one terminal statement" is a structural invariant rather than a side condition to maintain by hand.

Process.threads : List (List (String × Block α β true)) pairs each atomic block with its label (the outer list is SurfacePlusCal's parallel {...} {...} threads, the inner list the sequence of labelled atomic blocks within one thread).

Process/Declarations/Algorithm share the same α/β as Statement/Block/Branches/ Multicast: α is the declared-type annotation at whatever stage of checking it's currently at. Content that can't be expressed via this shared α (@mailbox's channel name/index expressions, @parameter's presence-as-a-Bool) instead gets a concrete field (Process.mailbox, Declarations.variables' isParameter).

structure CorePlusCal.Multicast (α β : Type) : Type

A multicast's recipients and payload, after the desugarer has collapsed SurfacePlusCal.MulticastFilter's bind list to a single binder.

The surface form [x₁ ⋈₁ e₁, …, xₙ ⋈ₙ eₙ ↦ v] names the components of a recipient tuple, not a chain of lets: it reaches every c[y] for y in the Cartesian product of the components, where an ∈-bind contributes its set and an =-bind the singleton containing its value. The desugarer turns that product into one set (set) over one binder (recipient), rewriting each original name in val to a projection of it — the same collapse a multi-binder function literal [x ∈ A, y ∈ B ↦ e] already gets. So nothing downstream reconstructs which bind was which, and n = 1 — the overwhelmingly common case — passes through untouched.

• recipient : String
• ann : α

  The recipient's declared-type annotation slot, at whatever stage of checking this is: the channel's own domain type once checked, since the recipient is what indexes the channel.

• set : β

  The set of recipients, always of the channel's domain type.

• val : β

@[implicit_reducible]

instance CorePlusCal.instReprMulticast {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (Multicast α✝ β✝)

Equations

• CorePlusCal.instReprMulticast = { reprPrec := CorePlusCal.instReprMulticast.repr }

def CorePlusCal.instReprMulticast.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Multicast α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CorePlusCal.instInhabitedMulticast {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} [Inhabited a✝¹] : Inhabited (Multicast a✝ a✝¹)

Equations

• CorePlusCal.instInhabitedMulticast = { default := CorePlusCal.instInhabitedMulticast.default }

@[implicit_reducible]

instance CorePlusCal.instBifunctorMulticast : Bifunctor Multicast

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBitraversableMulticast : Bitraversable Multicast

Equations

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

structure CorePlusCal.Ref (β : Type) : Type

SurfacePlusCal.Ref, but each bracket group's own index is unary: x[e₁, …, eₙ] (n > 1) desugars to x[<<e₁, …, eₙ>>]. x[e₁][e₂] (two separate bracket groups) is unaffected — args' outer list (one entry per path segment) doesn't change shape. .inl for a .field segment, .inr for a (now-unary) bracket-index segment.

• name : String
• args : List (String ⊕ β)

def CorePlusCal.instReprRef.repr {β✝ : Type} [Repr β✝] : Ref β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CorePlusCal.instReprRef {β✝ : Type} [Repr β✝] : Repr (Ref β✝)

Equations

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

@[implicit_reducible]

instance CorePlusCal.instFunctorRef : Functor Ref

Equations

• CorePlusCal.instFunctorRef = { map := fun {α β : Type} (f : α → β) (r : CorePlusCal.Ref α) => { name := r.name, args := Sum.map id f <$> r.args } }

@[implicit_reducible]

instance CorePlusCal.instTraversableRef : Traversable Ref

Equations

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

inductive CorePlusCal.Statement (α β : Type) : Bool → Type

• 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

  Binds exactly one variable — a multi-binder surface with (x = 3, y ∈ S) {…} is flattened into a nested chain of single-binder ones (with (x = 3) { with (y ∈ S) {…} }) before reaching this type.

• assert {α β : Type} (e : β) : Statement α β false
• either {α β : Type} {b : Bool} (branches : Branches α β b) : Statement α β b
• while {α β : Type} {b : Bool} (cond : β) (B : Block α β b) : Statement α β false

  while's body may be either terminal or not (terminal when a labelled step was extracted from the loop body, ending in a goto back to the condition check); the while statement itself is always non-terminal, since falling out of the loop continues normally to whatever follows it.

• receive {α β : Type} (c r : Ref β) : Statement α β false
• send {α β : Type} (c : Ref β) (e : β) : Statement α β false
• multicast {α β : Type} (c : String) (filter : Multicast α β) : Statement α β false

partial def CorePlusCal.instReprStatement.repr_1 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Statement α✝ β✝ a✝ → ℕ → Std.Format

partial def CorePlusCal.instReprBlock.repr_3 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Branches α✝ β✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance CorePlusCal.instReprStatement {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Repr (Statement α✝ β✝ a✝)

Equations

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

partial def CorePlusCal.instReprBlock.repr_2 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Block α✝ β✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance CorePlusCal.instReprBlock {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Repr (Block α✝ β✝ a✝)

Equations

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

partial def CorePlusCal.instReprBlock.repr_1 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Statement α✝ β✝ a✝ → ℕ → Std.Format

partial def CorePlusCal.instReprStatement.repr_3 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Branches α✝ β✝ a✝ → ℕ → Std.Format

partial def CorePlusCal.instReprStatement.repr_2 {α✝ β✝ : Type} {a✝ : Bool} [Repr α✝] [Repr β✝] : Block α✝ β✝ a✝ → ℕ → Std.Format

inductive CorePlusCal.Block (α β : Type) : Bool → Type

A block is a (possibly empty) sequence of non-terminal statements followed by a potentially-terminal one.

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

inductive CorePlusCal.Branches (α β : Type) : Bool → Type

• either {α β : Type} {b : Bool} : Block α β b → Branches α β b
• or {α β : Type} {b : Bool} : Block α β b → Branches α β b → Branches α β b

@[reducible, inline]

abbrev CorePlusCal.Block.begin {α β : Type} {b : Bool} : Block α β b → List (Statement α β false)

Equations

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

@[reducible, inline]

abbrev CorePlusCal.Block.end {α β : Type} {b : Bool} : Block α β b → Statement α β b

Equations

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

@[implicit_reducible]

instance CorePlusCal.instInhabitedStatement {α β : Type} {b : Bool} : Inhabited (Statement α β b)

Equations

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

@[implicit_reducible]

instance CorePlusCal.instInhabitedBlock {α β : Type} {b : Bool} : Inhabited (Block α β b)

Equations

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

@[implicit_reducible]

instance CorePlusCal.instInhabitedBranches {α β : Type} {b : Bool} : Inhabited (Branches α β b)

Equations

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

partial def CorePlusCal.Statement.bimap {b : Bool} {α β γ δ : Type} (f : α → β) (g : γ → δ) (S : Statement α γ b) : Statement β δ b

partial def CorePlusCal.Block.bimap {α β γ δ : Type} {b : Bool} (f : α → β) (g : γ → δ) (B : Block α γ b) : Block β δ b

partial def CorePlusCal.Branches.bimap {α β γ δ : Type} {b : Bool} (f : α → β) (g : γ → δ) : Branches α γ b → Branches β δ b

@[implicit_reducible]

instance CorePlusCal.instBifunctorStatement {b : Bool} : Bifunctor fun (x1 x2 : Type) => Statement x1 x2 b

Equations

• CorePlusCal.instBifunctorStatement = { bimap := fun {α α' β β' : Type} => CorePlusCal.Statement.bimap }

@[implicit_reducible]

instance CorePlusCal.instBifunctorBlock {b : Bool} : Bifunctor fun (x1 x2 : Type) => Block x1 x2 b

Equations

• CorePlusCal.instBifunctorBlock = { bimap := fun {α α' β β' : Type} => CorePlusCal.Block.bimap }

@[implicit_reducible]

instance CorePlusCal.instBifunctorBranches {b : Bool} : Bifunctor fun (x1 x2 : Type) => Branches x1 x2 b

Equations

• CorePlusCal.instBifunctorBranches = { bimap := fun {α α' β β' : Type} => CorePlusCal.Branches.bimap }

@[implicit_reducible]

def CorePlusCal.instInhabitedOfApplicative_core {F : Type u_1 → Type u_2} [Applicative F] {α : Type u_1} [Inhabited α] : Inhabited (F α)

Equations

• CorePlusCal.instInhabitedOfApplicative_core = { default := pure Inhabited.default }

partial def CorePlusCal.Statement.bitraverse {F : Type → Type} [Applicative F] {α β γ δ : Type} {b : Bool} (f : α → F β) (g : γ → F δ) (S : Statement α γ b) : F (Statement β δ b)

partial def CorePlusCal.Block.bitraverse {F : Type → Type} [Applicative F] {α β γ δ : Type} {b : Bool} (f : α → F β) (g : γ → F δ) (B : Block α γ b) : F (Block β δ b)

partial def CorePlusCal.Branches.bitraverse {F : Type → Type} [Applicative F] {α β γ δ : Type} {b : Bool} (f : α → F β) (g : γ → F δ) : Branches α γ b → F (Branches β δ b)

@[implicit_reducible]

instance CorePlusCal.instBitraversableStatement {b : Bool} : Bitraversable fun (x1 x2 : Type) => Statement x1 x2 b

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBitraversableBlock {b : Bool} : Bitraversable fun (x1 x2 : Type) => Block x1 x2 b

Equations

• CorePlusCal.instBitraversableBlock = { toBifunctor := CorePlusCal.instBifunctorBlock, bitraverse := fun {m : Type → Type} [Applicative m] {α α' β β' : Type} => CorePlusCal.Block.bitraverse }

@[implicit_reducible]

instance CorePlusCal.instBitraversableBranches {b : Bool} : Bitraversable fun (x1 x2 : Type) => Branches x1 x2 b

Equations

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

structure CorePlusCal.Declarations (α β : Type) : Type

The declarations at the top of an algorithm or process block — the annotation-carrying counterpart is SurfacePlusCal.Declarations. Shares the same α as Statement/Block/ Branches/Multicast.

• variables : List (String × α × Bool × Option (Bool × β))

  (name, declared-type annotation, isParameter, initializer); isParameter is true only on a @parameter-annotated, ∈-initialized entry. The initializer's Bool is true for =, false for ∈.

• channels : List (String × α × List β)
• fifos : List (String × α × List β)

def CorePlusCal.instReprDeclarations.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Declarations α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CorePlusCal.instReprDeclarations {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (Declarations α✝ β✝)

Equations

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

@[implicit_reducible]

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

Equations

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

def CorePlusCal.Declarations.bimap {α β γ δ : Type} (f : α → β) (g : γ → δ) (decls : Declarations α γ) : Declarations β δ

Equations

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

def CorePlusCal.Declarations.bitraverse {F : Type → Type} [Applicative F] {α β γ δ : Type} (f : α → F β) (g : γ → F δ) (decls : Declarations α γ) : F (Declarations β δ)

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBifunctorDeclarations : Bifunctor Declarations

Equations

• CorePlusCal.instBifunctorDeclarations = { bimap := fun {α α' β β' : Type} => CorePlusCal.Declarations.bimap }

@[implicit_reducible]

instance CorePlusCal.instBitraversableDeclarations : Bitraversable Declarations

Equations

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

structure CorePlusCal.Process (α β : Type) : Type

• mailbox : Option (String × List β)

  (channel name, filter/index args), from at most one @mailbox annotation; none if the process has no mailbox.

• isFair : Bool
• name : String
• =|∈ : Bool

  true for =, false for ∈.

• id : β
• localState : Declarations α β
• threads : List (List (String × Block α β true))

  One entry per parallel {...} thread; each thread is a sequence of labelled atomic blocks, in program order.

@[implicit_reducible]

instance CorePlusCal.instReprProcess {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (Process α✝ β✝)

Equations

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

def CorePlusCal.instReprProcess.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Process α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBifunctorProcess : Bifunctor Process

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBitraversableProcess : Bitraversable Process

Equations

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

structure CorePlusCal.Algorithm (α β : Type) : Type

• isFair : Bool
• name : String
• globalState : Declarations α β
• processes : List (Process α β)

def CorePlusCal.instReprAlgorithm.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Algorithm α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CorePlusCal.instReprAlgorithm {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (Algorithm α✝ β✝)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBifunctorAlgorithm : Bifunctor Algorithm

Equations

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

@[implicit_reducible]

instance CorePlusCal.instBitraversableAlgorithm : Bitraversable Algorithm

Equations

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