Compiling TLA⁺ operator and function definitions into Go top-level declarations.

Four forms, and which one a declaration takes is read off its type, not its syntax:

• A parameter-less operator (X == e) becomes a package-level var X τ = ⟦e⟧. Not a const: Go accepts only a small class of types there, and a TLA⁺ definition generally has none of them. Immutability is a convention here rather than something Go enforces.
• A parametric operator (X(p₁, …, pₙ) == e) becomes an ordinary Go function. Go supports mutually recursive top-level functions natively, so nothing special is needed — and in this compiler an operator is never recursive at all: RECURSIVE is out of the accepted language, and Elaborator/Declarations.lean's [Operator definition] rule checks the body without the operator itself in Γ. The thesis's mutually-recursive Even/Odd example is unreachable.
• A non-recursive function definition (F[x ∈ D] == e) becomes var F = FnConstructor(…).
• A recursive function definition becomes var F = MkRecFn(…), which ties the knot: it allocates the LazyFunction with no generator, then overwrites the generator with a closure that captures the function itself. Unlike operators, a function definition always gets self-recursion ([Function definition] binds f while checking the body), so which of the two to emit is decided by looking for the self-reference rather than by a keyword.

Type variables reach only the parametric-operator form. A rigid type variable compiles to a Go type parameter, and each one carries a dictionary parameter beside it, since a polymorphic definition is called at many types and its ordering therefore cannot be a closed expression. Go has no generic package-level var, so the other three forms — all of which are vars — must reject one. That is a restriction of Go's, not a choice: there is nowhere to bind the parameter.

CONSTANT/VARIABLE declarations and ASSUME produce nothing. A CONSTANT is supplied by whoever wires the generated code into a runnable system, under the capitalized name every reference to it compiles to — the same boundary the absence of an emitted main sits on. An ASSUME is a proof obligation about a specification, with no computational content to emit.

partial def Network2Go.mentionsSelf (name : String) (e : ComputablePlusCal.Expression) : Bool

Does name occur in e as a reference to the enclosing function definition being checked?

A function definition's body sees its own name in scope, resolved through Ξ like any module-level name (.module); a bare occurrence of name inside name's own body is therefore a self-reference. The caller has already ruled out a parameter of the same name, so the check is exact and no binder-respecting scope walk is needed.

def Network2Go.compileDeclaration {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) : ComputableTLAPlus.Declaration ComputableTLAPlus.Typ → m (Option ComputableGo.Declaration)

Compiles one top-level declaration, or nothing for the ones with no computational content.

Equations

• One or more equations did not get rendered due to their size.
• Network2Go.compileDeclaration pos (Declaration.constants a) = pure none
• Network2Go.compileDeclaration pos (Declaration.variables a) = pure none
• Network2Go.compileDeclaration pos (Declaration.assume a) = pure none

def Network2Go.compileDeclarations {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (ds : List (ComputableTLAPlus.Declaration ComputableTLAPlus.Typ)) : m (List ComputableGo.Declaration)

A whole declaration list, keeping only what compiles to something. Order is preserved: Go resolves package-level declarations independently of the order they are written in, so this matters for readability rather than for correctness.

Equations

• Network2Go.compileDeclarations pos ds = do let __do_lift ← List.mapM (Network2Go.compileDeclaration pos) ds pure __do_lift.reduceOption