Assembling compiled declarations into a Go source file: the package clause, the import block, and the declarations themselves.

Kept out of Core/Go/Pretty.lean, which prints the AST and nothing else. A file's framing is not part of the Go fragment the semantics covers, and the import paths are Network2Go's knowledge — Naming.lean is where the runtime's package qualifiers are decided, so this is where the paths they resolve to belong.

Imports are computed, never assumed. Go rejects an unused import, so emitting every runtime package unconditionally would break every program that happens not to need one — a specification whose processes never exchange a message uses no comm, one with no process-local variables uses no locks (or condlocks, under -Xgo-cond). usedPackages walks the declarations for qualified names instead.

def Network2Go.runtimeImports : List (String × String)

Where each runtime package qualifier resolves to. Keyed by the qualifier Naming.lean emits, since that is what appears in the compiled AST.

Equations

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

def Network2Go.usedPackages (decls : List ComputableGo.Declaration) : List String

Every runtime package a declaration list actually names, in runtimeImports order.

Equations

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

def Network2Go.emitFile (packageName : String) (decls : List ComputableGo.Declaration) : String

A complete .go file: package clause, the imports the declarations need, then the declarations.

package defaults to main — the shape a user most often wants to drop a func main beside — and -Xgo-pkg:<name> overrides it. The compiler emits no main of its own: which processes run, where, and how they find each other is not something a specification says, so the generated file is a library its caller drives.

Equations

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