The surface syntax of Distributed PlusCal algorithms, as accepted by the parser, prior to desugaring into explicit-goto form.

Positions are attached out-of-band via @@/posOf/match_source (Common/Position.lean), not stored structurally in these types.

structure SurfacePlusCal.Ref (β : Type) : Type

A reference to a (possibly indexed/field-accessed) variable, e.g. x[1][2].y. One entry per path segment, in left-to-right textual order: .inl for a .field segment, .inr for a [e₁, …, eₙ] bracket-index group.

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instFunctorRef : Functor Ref

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instTraversableRef : Traversable Ref

Equations

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

structure SurfacePlusCal.MulticastFilter (α β : Type) : Type

The filter/value expression of a multicast, e.g. [m = self, n \in Actors \ {self} |-> Hello(m, n)].

• binds : List (String × α × Bool × β)

  Each bind is (name, annotation, isEquality, expr); isEquality is true for =, false for \in.

• val : β

@[implicit_reducible]

instance SurfacePlusCal.instReprMulticastFilter {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (MulticastFilter α✝ β✝)

Equations

• SurfacePlusCal.instReprMulticastFilter = { reprPrec := SurfacePlusCal.instReprMulticastFilter.repr }

def SurfacePlusCal.instReprMulticastFilter.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : MulticastFilter α✝ β✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instInhabitedMulticastFilter {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (MulticastFilter a✝ a✝¹)

Equations

• SurfacePlusCal.instInhabitedMulticastFilter = { default := SurfacePlusCal.instInhabitedMulticastFilter.default }

@[implicit_reducible]

instance SurfacePlusCal.instBifunctorMulticastFilter : Bifunctor MulticastFilter

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBitraversableMulticastFilter : Bitraversable MulticastFilter

Equations

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

inductive SurfacePlusCal.Statement (α β : Type) : Type

A PlusCal statement. α carries comment annotations (as in SurfaceTLAPlus), β is the embedded-expression type. A block (the body of if/while/with/either/…) is a flat List (String ⊕ Statement α β): a leading label and the statement it labels are elements of the same list; desugaring separates them into distinct fields.

• skip {α β : Type} : Statement α β
• goto {α β : Type} (label : String) : Statement α β
• print {α β : Type} (e : β) : Statement α β
• assign {α β : Type} : List (Ref β × β) → Statement α β
• if {α β : Type} (cond : β) (B₁ : List (String ⊕ Statement α β)) (B₂ : Option (List (String ⊕ Statement α β))) : Statement α β
• await {α β : Type} (e : β) : Statement α β
• with {α β : Type} (vars : List (String × α × Bool × β)) (B : List (String ⊕ Statement α β)) : Statement α β

  with (* @type: ... *) x = e do B / with (* @type: ... *) x ∈ e do B — the Bool is true for =, false for ∈.

• assert {α β : Type} (e : β) : Statement α β
• either {α β : Type} (branches : List (List (String ⊕ Statement α β))) : Statement α β
• while {α β : Type} (cond : β) (B : List (String ⊕ Statement α β)) : Statement α β
• receive {α β : Type} (c r : Ref β) : Statement α β
• send {α β : Type} (c : Ref β) (e : β) : Statement α β
• multicast {α β : Type} (c : String) (filter : MulticastFilter α β) : Statement α β

partial def SurfacePlusCal.instReprStatement.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Statement α✝ β✝ → ℕ → Std.Format

@[implicit_reducible]

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

Equations

• SurfacePlusCal.instReprStatement = { reprPrec := SurfacePlusCal.instReprStatement.repr }

@[implicit_reducible]

instance SurfacePlusCal.instInhabitedStatement {a✝ a✝¹ : Type} : Inhabited (Statement a✝ a✝¹)

Equations

• SurfacePlusCal.instInhabitedStatement = { default := SurfacePlusCal.instInhabitedStatement.default }

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

@[implicit_reducible]

instance SurfacePlusCal.instBifunctorStatement : Bifunctor Statement

Equations

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

@[implicit_reducible]

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

Equations

• SurfacePlusCal.instInhabitedOfApplicative_core = { default := pure default }

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

@[implicit_reducible]

instance SurfacePlusCal.instBitraversableStatement : Bitraversable Statement

Equations

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

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

The declarations at the top of an algorithm or process block.

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

  (* annotations *) v (("=" | "∈") expr)?; the Bool is true for =, false for ∈.

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBifunctorDeclarations : Bifunctor Declarations

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBitraversableDeclarations : Bitraversable Declarations

Equations

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

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

process(x ∈ S) ⋆ … / process(x = e) ⋆ ….

• ann : α
• isFair : Bool

  Carried through for round-tripping only — this compiler never acts on it.

• name : String
• =|∈ : Bool

  true for =, false for ∈.

• id : β
• localState : Declarations α β
• threads : List (List (String ⊕ Statement α β))

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBifunctorProcess : Bifunctor Process

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBitraversableProcess : Bitraversable Process

Equations

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

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

fifos c₁ : τ₁, …; P₁ ∥ … ∥ Pₙ.

• isFair : Bool

  Round-tripped only, per Process.isFair.

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBifunctorAlgorithm : Bifunctor Algorithm

Equations

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

@[implicit_reducible]

instance SurfacePlusCal.instBitraversableAlgorithm : Bitraversable Algorithm

Equations

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