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 fixed number of times. It
translates into a general loop over a fresh counter.
\(\llbracket\) repeat e do b end \(\rrbracket\) | = | |
do let _n := e; from let _i := 0 until _i >= _n do b ; _i := _i + 1 end end | ||
The bound \(e\) is evaluated once, before the first iteration; a later change to any variable occurring in \(e\) does not alter the number of repetitions.
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.6What 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.