Ties the whole checker together: CoreTLAPlus.Module.check, threading Γ across
declarations₁ → the embedded PlusCal algorithm → declarations₂, and Module.runChecker,
the one concrete monad instantiation this pass is ever run at.
The embedded algorithm is checked but does not extend Γ any further — PlusCal-internal
declarations (variables/channels/fifos) don't leak into the surrounding TLA⁺ module's own
Γ. declarations₂ is checked against the same Γ that declarations₁ left behind, exactly
as if the algorithm weren't there at all.
The checker's own output type — a module's cached representation once checked.
Instances For
Γ ⊢ M typeok: declarations₁, then the embedded algorithm (if any), then declarations₂
against the same Γ declarations₁ left behind.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Run the checker against its one concrete monad instantiation: Γ's ReaderT, the
metavariable/pending-bounds contexts as nested StateTs, and MonadDiagnostic's TCError/
TCWarning reporting via DiagT, so a warning emitted before a later fatal error still
survives. No checking rule emits a TCWarning yet, but the capability is wired through
uniformly with every other pass. Γ₀ is the caller-supplied initial context. The base monad n
stays abstract, constrained only to supply the fresh-name counter (MonadStateOf Nat, which
Common/Fresh.lean's MonadFresh instance reads, needed here by Subtyping.lean): the counter
belongs to one compile, owned by Driver/Modules.lean's DriverState, not to the process.