A number of Nex’s surface forms are conveniences: they add no expressive power and are explained by translation into a smaller bare language. Defining them this way keeps the semantic rules of Chapters 4 and 5 few, since a derived form inherits its meaning from its translation. This appendix gives those translations.
We write \(\llbracket \phi \rrbracket\) for the bare form into which the surface phrase \(\phi\) is translated. A translation is performed before elaboration; the static and dynamic semantics see only the bare form. Fresh identifiers introduced by a translation (written \(\_i\), \(\_c\), and the like) are chosen distinct from every identifier in the program.
C.1Collection Displays
The array, map, and set displays abbreviate a creation followed by a sequence of insertions.
\(\llbracket\) [e₁, …, eₙ] \(\rrbracket\) | = | do let _a := create Array; _a.add(e₁); … ; _a.add(eₙ); _a end |
\(\llbracket\) {k₁: v₁, …, kₙ: vₙ} \(\rrbracket\) | = | do let _m := create Map; _m.put(k₁, v₁); … ; _m end |
\(\llbracket\) {} \(\rrbracket\) | = | create Map |
\(\llbracket\) #{e₁, …, eₙ} \(\rrbracket\) | = | do let _s := create Set; _s.add(e₁); … ; _s end |
\(\llbracket\) #{} \(\rrbracket\) | = | create Set |
The element type of the created collection is inferred from the display, or
taken from the annotation of the surrounding let or parameter when
the display is empty. The empty set must be written #{} and not
{}: the latter is the empty map. (A do…end
used here is the block-as-expression whose value is its final expression; the
displays are the one place the bare language needs it, and it may be read simply
as “build the collection and yield it.”)
C.2The Counted Loop
The repeat loop runs its body a number of times given by its
bound. It translates into a general loop over a fresh counter.
\(\llbracket\) repeat e do b end \(\rrbracket\) | = | |
from let _i := 0 until _i >= e do b ; _i := _i + 1 end | ||
The bound \(e\) appears in the until condition and so is
re-evaluated before each iteration; an assignment within the body to a
variable occurring in \(e\) therefore alters the number of repetitions. A
program that requires a count fixed in advance should bind the bound first
(let n := e) and repeat over n.
C.3The Cursor Loop
The across loop traverses any value that supplies the
Cursor protocol of Appendix B. It translates into a general loop
driven by that protocol.
\(\llbracket\) across e as x do b end \(\rrbracket\) | = | |
do let _c := e.cursor; _c.start; | ||
from until _c.at_end do let x := _c.item ; b ; _c.next end end | ||
The cursor variable x is bound afresh on each iteration to the
current item, and is in scope only within the body. An Array yields
its elements in order, a String its characters, and a
Map its entries as [key, value] pairs
(Section 2.8 and Appendix B).
C.4Cascaded Conditionals
The elseif chain abbreviates nested conditionals.
\(\llbracket\) if e₁ then b₁ elseif e₂ then b₂ else b₃ end \(\rrbracket\) | = | |
if e₁ then b₁ else (if e₂ then b₂ else b₃ end) end | ||
C.5Shared Parameter Types
Several parameters may share a single type annotation; this abbreviates the fully annotated list.
\(\llbracket\) (a, b: T) \(\rrbracket\) | = | (a: T, b: T) |
C.6Union Declarations
A union declaration (Section 3.2.2) abbreviates a sealed
hierarchy of data classes. The parent becomes a sealed deferred class, and each
variant becomes a class inheriting it, whose fields are the variant’s
payload and whose sole constructor takes and assigns them.
\(\llbracket\) union P⟨[G…]⟩ V₁ … Vₙ end \(\rrbracket\) | = | |
sealed deferred class P⟨[G…]⟩ end | ||
and, for each variant Vᵢ(f₁: T₁, …, fₖ: Tₖ), | ||
class Vᵢ inherit P⟨[G…]⟩ feature f₁: T₁ … fₖ: Tₖ | ||
create make(f₁: T₁, …, fₖ: Tₖ) do f₁ := f₁ ; … ; fₖ := fₖ end end | ||
A payload-free variant Vᵢ becomes a class with an empty feature
section and a nullary make. Because the translation names the parent
in each variant’s inherit clause, the generic arguments carry
through and the resulting classes are exactly those a hand-written sealed
hierarchy would produce; nothing further — no method, invariant, or contract
— is generated.
Prefixing the declaration with enum — permitted only when
every variant is payload-free and P is non-generic — enriches
the same hierarchy into an enumeration. On top of the translation above,
the parent gains an ordering and one interned constant per member, and each
variant’s make records its declaration index.
\(\llbracket\) enum union P V₁ … Vₙ end \(\rrbracket\) | = | |
sealed deferred class P inherit Comparable | ||
feature ordinal: Integer | ||
compare(o: P): Integer do result := ordinal − o.ordinal end | ||
feature V₁: P = create V₁.make() ; … ; Vₙ: P = create Vₙ.make() | ||
values: Array[P] = [V₁, …, Vₙ] end | ||
and, for each variant Vᵢ at 0-based declaration index i, | ||
class Vᵢ inherit P create make() do ordinal := i end end | ||
Thus P.Vᵢ is the one canonical Vᵢ value (a class
constant, evaluated once — Section 3.3 — so P.Vᵢ ==
P.Vⱼ tests identity), the members order by the sequence in which they are
written, and P.values lists them all. Because the enrichment claims
those three names, a variant may not be named ordinal,
compare, or values. A plain union never
gains this; the enrichment is requested, never inferred.
C.7Match Patterns and Guards
A match clause richer than the bare
when id as id dispatch of the core
(Section 2.8) is translated into it. A clause
when V(fp₁, …, fpₙ) as x if g then b becomes the bare clause
when V as _m (binding x to _m as well when
as x is present) whose body binds the field patterns and then tests
the field constraints together with the guard; if any test fails, control passes
to the clauses that follow, exactly as a false guard does.
Each field pattern fpᵢ on the field f contributes a
binding, a test, or both:
\(\llbracket\) f (bind) \(\rrbracket\) | = | let f := _m.f |
\(\llbracket\) f: y (rename) \(\rrbracket\) | = | let y := _m.f |
\(\llbracket\) _ (skip) \(\rrbracket\) | = | — nothing |
\(\llbracket\) ℓ (literal) \(\rrbracket\) | = | test _m.f = ℓ |
\(\llbracket\) Q(…) (nested) \(\rrbracket\) | = | test convert _m.f to _n: Q, then Q’s field patterns on _n |
The tests are conjoined with the guard g; a clause whose field
patterns are only binds, renames, and skips contributes no test, so once its
class matches it commits and never falls through — which is why such a clause
still counts toward exhaustiveness (Section 4.4), whereas a clause carrying a
literal, a nested pattern, or a guard does not. A top-level _ pattern
translates to the else block.
C.8What Is Not Derived
It is worth saying which apparent conveniences are not derived forms,
but primitive constructs with rules of their own. The conditional expression
when…then…else is primitive
(rule 4.14), not an abbreviation for an if statement, because it
yields a value. The short-circuit operators and and or
are primitive (rules 5.5–5.6), not abbreviations for conditionals,
because their evaluation order is part of the language’s definition. The
safe access ?. is primitive (rules 5.8–5.9). And the
contract clauses, though they could in principle be expanded into explicit checks
and raises, are treated as primitive so that the Definition can speak of
preconditions, postconditions, and invariants as first-class notions
(Section 5.6) rather than as a particular pattern of generated code.