Documentation

Core.Go.Pretty

Pretty-printing for Core/Go/Syntax.lean. Unlike every other Pretty.lean in this repo, this one is not a debug dump — it is Network2Go's code generator: the .go file the compiler ships is whatever this module prints. (Guarded2Network has no pretty-printer at all and dumps via reprStr; that path stays for -d dump-network, and -d dump-go will reuse this one.)

keywords and predeclared are two tables, not one: Go's reserved words are escaped by the printer, while its predeclared identifiers are not — escaping those would rewrite the generated code's own references to int/any/comparable/len into int__/comparable__. predeclared is exported for Network2Go to rename user-chosen names against, since only the pass knows which names came from the specification; identifier hygiene is enforced per pass, not only by the printer.
Precedence levels are Go's own: || 1, && 2, comparisons 3, +/- 4, *///% 5, unary 6, selector/index/call 7. Common/Pretty.lean's infixl/prefix combinators parenthesize against them, so no expression is over-parenthesized.
Blocks always break (Std.Format.indent without a surrounding group): generated Go is read and gofmt-ed by whoever consumes it, so a stable one-statement-per-line layout is worth more than a compact one.
Expressions and statements print from one mutual block, since Expression.funcLit carries a statement body. Statement cases therefore call Expression.pretty · 0 directly rather than going through the Std.ToFormat instance, which is only available once the block closes.
String literals print as Go raw strings (`…`), so no escaping pass is needed. A source string containing a backtick would break this; TLA⁺'s own string syntax has no way to write one.
print compiles to Go's builtin println, not fmt.Println, so that generated code needs no import beyond the runtime library.

def Go.keywords :

Std.HashSet String

Go's 25 reserved words. These can never be identifiers, in any position, so the printer escapes them unconditionally.

Exported alongside predeclared so that Network2Go can rename a user-chosen name out of this set rather than leaving it to sanitize below — a rename that knows the name's provenance can pick a spelling that stays distinct from every other name, which a blind suffix cannot.

Equations

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

Instances For

def Go.predeclared :

Std.HashSet String

Go's predeclared identifiers — types, constants and builtin functions living in the universe block. Unlike keywords these are ordinary identifiers that a declaration may legally shadow, so the printer must not escape them: the generated code refers to int, any, comparable, error and append/len/make by name constantly, and escaping them would turn those into int__/comparable__.

A user-chosen name colliding with one of these still has to be renamed — shadowing int in a file that also emits int for TLA⁺'s Int would silently change what the generated code means. That rename belongs to Network2Go, which is the only place that knows whether a name came from the specification or from the compiler; this set is exported for it to consult. Hygiene is enforced per pass, not only by the printer.

Equations

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

Instances For

@[inline]

def Go.sanitize (name : String) :

Escape an identifier that would otherwise be a Go reserved word. Applied at every identifier-print site — a backstop, not the whole hygiene story: see predeclared.

Unreachable for anything Network2Go emits, which renames user-chosen names out of keywords itself; this catches only a name reaching the printer from somewhere that did not.

The suffix is a single _, because Network2Go spends underscore-run parity to separate user-written names from compiler-introduced ones: a doubled suffix lands in the user half, so type and a user's own type_ would both print type__. An odd-length suffix cannot collide with either.

Equations

Go.sanitize name = if name ∈ Go.keywords then name ++ "_" else name

Instances For

partial def Go.Typ.pretty :

Typ → Std.Format

@[implicit_reducible]

instance Go.instToFormatTyp :

Std.ToFormat Typ

Equations

Go.instToFormatTyp = { format := Go.Typ.pretty }

def Go.UnaryOperator.symbol :

UnaryOperator → String

Equations

Go.UnaryOperator.not.symbol = "!"
Go.UnaryOperator.neg.symbol = "-"

Instances For

def Go.BinaryOperator.symbol :

BinaryOperator → String

Equations

Instances For

def Go.BinaryOperator.precedence :

BinaryOperator → ℕ

Go's binary-operator precedence: *///% bind tighter than +/-, which bind tighter than the comparisons, then &&, then ||.

Equations

Instances For

def Go.Builtin.name :

Builtin → String

Equations

Instances For

partial def Go.Ref.pretty {Expr : Type} (f : Expr → Std.Format) :

Ref Expr → Std.Format

Takes the expression formatter as an argument rather than resolving it from Std.ToFormat: Ref is printed from inside the Expression/Statement mutual block below, where the instance for Expression does not exist yet.

@[implicit_reducible]

instance Go.instToFormatRef {Expr : Type} [Std.ToFormat Expr] :

Std.ToFormat (Ref Expr)

Equations

Go.instToFormatRef = { format := Go.Ref.pretty Std.format }

partial def Go.Expression.pretty {α : Type} [Std.ToFormat α] (e : Expression α) (prec : ℕ) :

partial def Go.Statement.pretty {α : Type} [Std.ToFormat α] :

Statement α → Std.Format

@[implicit_reducible]

instance Go.instToFormatExpression {α : Type} [Std.ToFormat α] :

Std.ToFormat (Expression α)

Equations

Go.instToFormatExpression = { format := fun (x : Go.Expression α) => x.pretty 0 }

@[implicit_reducible]

instance Go.instToFormatStatement {α : Type} [Std.ToFormat α] :

Std.ToFormat (Statement α)

Equations

Go.instToFormatStatement = { format := Go.Statement.pretty }

def Go.Function.pretty {α : Type} [Std.ToFormat α] (F : Function α) :

Equations

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

Instances For

@[implicit_reducible]

instance Go.instToFormatFunction {α : Type} [Std.ToFormat α] :

Std.ToFormat (Function α)

Equations

Go.instToFormatFunction = { format := Go.Function.pretty }

def Go.Declaration.pretty {α : Type} [Std.ToFormat α] :

Declaration α → Std.Format

A top-level declaration. The var form spells its type even when there is an initializer, so that a nil-valued or otherwise uninferable right-hand side still declares the right thing, and because the compilation listings do.

Equations

One or more equations did not get rendered due to their size.
(Go.Declaration.function F).pretty = F.pretty
(Go.Declaration.typ name τ).pretty = Std.format "type " ++ Std.format (Go.sanitize name) ++ Std.format " " ++ Std.format τ

Instances For

@[implicit_reducible]

instance Go.instToFormatDeclaration {α : Type} [Std.ToFormat α] :

Std.ToFormat (Declaration α)

Equations

Go.instToFormatDeclaration = { format := Go.Declaration.pretty }