Computable2Guarded's diagnostics: a single defense-in-depth catch-all. Every case it reports is one this pass's own invariants rule out (𝒞_cflow finding a while not at block-front, say); the pass introduces no user-facing restriction of its own.

inductive GuardedError : Type

Computable2Guarded's errors.

• internalInvariantViolated (pos : SourceSpan) (description : String) : GuardedError

  Defense-in-depth: an input shape this pass's own invariants guarantee can't occur (e.g. a while not immediately preceded by a labelled block) still turned up. No proof of unreachability exists yet, so this stays a runtime check rather than absurd/nomatch. pos is SourceSpan.placeholder at callers past the point where a real position is still available (ElaboratedPlusCal/GuardedPlusCal.Statement carry none), matching Typed2Computable.lean's own precedent.

def instReprGuardedError.repr : GuardedError → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprGuardedError : Repr GuardedError

Equations

• instReprGuardedError = { reprPrec := instReprGuardedError.repr }

@[implicit_reducible]

instance instInhabitedGuardedError : Inhabited GuardedError

Equations

• instInhabitedGuardedError = { default := instInhabitedGuardedError.default }

@[implicit_reducible]

instance instBEqGuardedError : BEq GuardedError

Equations

• instBEqGuardedError = { beq := instBEqGuardedError.beq }

def instBEqGuardedError.beq : GuardedError → GuardedError → Bool

Equations

• instBEqGuardedError.beq (GuardedError.internalInvariantViolated a a_1) (GuardedError.internalInvariantViolated b b_1) = (a == b && a_1 == b_1)
• instBEqGuardedError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instCompilerDiagnosticGuardedErrorString : CompilerDiagnostic GuardedError String

Equations

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