Programs

The preceding chapters define the elaboration and evaluation of the phrases of Nex. This short chapter assembles them into the meaning of a whole program: how its declarations and statements are processed, and in what order.

7.1The Two Worlds of a Program

Recall from Section 3.1 that a program is a sequence of top-level items in any order, and that these fall into two kinds. The declarations—the classes, free functions, and type aliases, together with the module links that bring further declarations into scope—form the static world. The top-level statements form the dynamic world. A program is processed by first building the static world in full, and then executing the dynamic world against it.

This order is not the textual order of the items but a reordering imposed by the Definition: every declaration is in scope throughout every other, so that classes and functions may refer to one another freely, while a top-level statement runs only after the entire static world exists. The benefit is that the programmer need not arrange declarations in dependency order, and that forward reference among classes and functions is always available.

7.2Building the Static World

The static world is built in stages, against the standard environment \(E_0\) of Appendix B—the classes and values that exist before any user code.

1. Module links. Each import declaration adds a host class to the environment; each intern declaration elaborates the named unit—recursively, by this same procedure—and adds its declarations under the given name or alias. A unit is elaborated once however often it is interned.
2. Class and function registration. The names of all classes and all functions (including the signatures announced by declare) are entered into the class bindings \(\Sigma\), so that every later step sees every name.
3. Elaboration. Each class is elaborated—its parents resolved, its fields and routines typed, its contracts checked for well-formedness—and each function body is typed against the registered signatures. The class well-formedness conditions of Section 4.9 (acyclic inheritance, conformant overriding, complete deferral, sealed-implies-deferred) are verified here.

If any step fails, the program is rejected and nothing is executed. A program that survives all three stages is statically valid, and yields a static environment \(C\) together with the initial dynamic bindings \(E_1\) and store \(s_0\), extending the standard environment \(E_0\) with the elaborated classes and the function and constructor closures.

7.3Executing the Dynamic World

The top-level statements are then evaluated in source order, against \(E_1\), by the statement judgement of Chapter 5. The bindings thread from one statement to the next, so a top-level let is visible to the statements that follow it; the store threads likewise. The program’s observable behaviour—its output, the host effects of its imported classes, the final store—is the cumulative effect of this evaluation.

Here \(\mathit{decs}\) are the declarations of the program and \(\mathit{stmts}\) its top-level statements; the relation \(\leadsto\) is the construction of Section 7.2, \(E_1\) and \(s_0\) the initial dynamic bindings and store, and \(\Downarrow\) the evaluation of the whole program to a final store.

An uncaught exception raised by a top-level statement terminates the program; its value and position are reported, and no further statement runs. A program that spawns tasks (Chapter 6) completes when its top-level statements have been evaluated and the policy of the host for outstanding tasks has been applied; the Definition fixes the meaning of each communication but, as in Section 6.4, leaves the disposal of unawaited tasks to the realisation.

7.4The Definition and the Implementation

The procedure of this chapter mirrors the reference interpreter, which registers imports and interns, then classes, then functions, and only then executes the top-level statements—loading the static world before running the dynamic one. That correspondence is intentional: the Definition is meant to describe the same language the interpreter implements. Where the bytecode and JavaScript back ends are concerned, they are required to reproduce the behaviour defined here; a back end that diverges is, by the project’s own rule, in error, and the divergence is a defect to be repaired rather than a second meaning to be admitted.