Computable2Guarded's entry point — 𝒞_D→G := 𝒞_reord ∘ 𝒞_flat ∘ 𝒞_par ∘ 𝒞_cflow, matching the <InputType>.<verb> convention the other passes use. 𝒞_cflow/𝒞_par run first, both whole-Algorithm rewrites within ComputablePlusCal's own type (their order doesn't matter); only then does the merged 𝒞_flat/𝒞_reord walk change shape, applied per (label, Block) pair across every thread of every process. Declarations/Process/Algorithm's outer shape is otherwise a plain structural copy — ComputablePlusCal's Typ/Expression and this pass's own pinning of GuardedPlusCal's are the identical types, so only threads genuinely changes shape. Declarations is still a distinct (if identically-shaped) structure between the two namespaces, so Declarations.toGuarded below is a one-line field-for-field repackaging, not a real translation.

def ComputablePlusCal.Declarations.toGuarded (d : Declarations) : ComputableGuardedPlusCal.Declarations

ElaboratedPlusCal.Declarations and GuardedPlusCal.Declarations share every field's name and type (see the module doc above) — this only exists because they're nominally distinct structures, not because anything actually needs converting.

Equations

• d.toGuarded = { «variables» := d.variables, channels := d.channels, fifos := d.fifos }

def ComputablePlusCal.Algorithm.toGuarded {m : Type → Type} [Monad m] [MonadFresh m] [MonadDiagnostic Empty GuardedError m] (algo : Algorithm) : m ComputableGuardedPlusCal.Algorithm

Equations

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