TypedPlusCal.{Ref,Multicast,Statement,Block,Branches,Declarations,Process,Algorithm} .toComputable — translates a checked PlusCal algorithm (and its pieces) into ComputablePlusCal, delegating every leaf TypedTLAPlus.Expression to Expression.toComputable (Typed2Computable/TLAPlus.lean). τ fields (Ref.baseType, Statement.with's ann, Declarations's per-binding annotations, …) pass through unconverted, same reason as Typed2Computable/TLAPlus.lean's own note: ComputableTLAPlus.Typ is a literal reuse of TypedTLAPlus.Typ, not a second copy.

Position-carrying nodes (Statement, Process, Algorithm) are re-registered at their source node's own span via match_source/@@, the same convention CorePlusCal.Statement.bitraverse and Elaborator/PlusCal.lean follow. Ref/Block/Branches/Declarations are not position-carrying anywhere in this codebase, and nothing reads a span off one.

ElaboratedPlusCal (Core/TypedPlusCal/Syntax.lean, the shared generic layer both TypedPlusCal and ComputablePlusCal pin) doesn't derive Bifunctor/Bitraversable instances of its own the way CorePlusCal's equivalently-shaped types do — so Ref/Statement/Block/ Branches/Declarations/Process/Algorithm each get a hand-written toComputable below, mirroring CorePlusCal.Statement.bitraverse's own per-constructor shape with f := pure (the τ-side function, always the identity here) folded away. Multicast is the one exception: it's reused generically from CorePlusCal, which does carry a registered Bitraversable instance, so its toComputable is just bitraverse pure Expression.toComputable.

Every ElaboratedPlusCal-family conversion below is invoked via qualified call (TypedPlusCal.Block.toComputable B, not B.toComputable) rather than dot-notation: dot-notation on a TypedPlusCal.X-typed value resolves through the abbrev to ElaboratedPlusCal's own namespace, which has no such method. Only TypedTLAPlus.Expression- typed leaves stay dot-called (e.toComputable), since Expression is a real inductive matching its own declared name, not an abbrev layer.

def TypedPlusCal.Ref.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] (r : Ref) : m ComputablePlusCal.Ref

Ref.args' .inr (index) entries delegated to Expression.toComputable; .inl (field) entries and name/baseType pass through unconverted.

Equations

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

def TypedPlusCal.Multicast.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] (filter : Multicast) : m ComputablePlusCal.Multicast

CorePlusCal.Multicast's own registered Bitraversable instance, with the τ-side function fixed to pure (identity) — see the module doc above.

Equations

• filter.toComputable = bitraverse pure TypedTLAPlus.Expression.toComputable filter

partial def TypedPlusCal.Statement.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] {b : Bool} (s : Statement b) : m (ComputablePlusCal.Statement b)

Mirrors CorePlusCal.Statement.bitraverse's own per-constructor shape, f := pure folded away, and reattaches the source statement's own span to the translated one exactly the way Statement.bitraverse and TypedTLAPlus.Expression.toComputable do — a ComputablePlusCal.Statement whose position is never registered is a position posOf cannot answer for, and it answers with an unrelated node's span rather than failing (Common/Position.lean). partial: same reason Statement.bitraverse itself is — structural recursion isn't visibly decreasing to Lean through the mutual Block/Branches nesting.

partial def TypedPlusCal.Block.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] {b : Bool} : Block b → m (ComputablePlusCal.Block b)

Mirrors CorePlusCal.Block.bitraverse.

partial def TypedPlusCal.Branches.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] {b : Bool} : Branches b → m (ComputablePlusCal.Branches b)

Mirrors CorePlusCal.Branches.bitraverse.

def TypedPlusCal.Declarations.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] (d : Declarations) : m ComputablePlusCal.Declarations

Mirrors CorePlusCal.Declarations.bitraverse — every field carries leaf expressions, so nothing passes through via {d with ...} the way Process/Algorithm below can.

Equations

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

def TypedPlusCal.Process.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] (p : Process) : m ComputablePlusCal.Process

Mirrors CorePlusCal.Process.bitraverse; isFair/name/«=|∈» pass through unconverted via {p with ...}.

Equations

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

def TypedPlusCal.Algorithm.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] (algo : Algorithm) : m ComputablePlusCal.Algorithm

Mirrors CorePlusCal.Algorithm.bitraverse; isFair/name pass through unconverted via {algo with ...}.

Equations

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