Model

<

Model      ::= Files Imports Block

<

The nonterminal Model is treated like the body of a function definition (i.e., like a FuncDef (Section A.3.3.11), but without the identifier naming the function and with an empty list of formal parameters). More precisely:

Eval( Files Imports Block , C) =
{
  val C0 = Eval( Files Imports , emptybinding);
  return Eval( LAMBDA () Block , _append(C0, C));
}

As this rule indicates, the Files and Imports constructs are evaluated in an empty context, and they add to the closure context in which the model's LAMBDA is evaluated. In practice, the context C will always be the initial context C-initial when this rule is applied (cf. Sections A.3.3 and A.3.3.15).

The Files nonterminal introduces values corresponding to the contents of ordinary files and directories. The Imports nonterminal introduces closure values corresponding to other Vesta SDL models.

The evaluation rules handle Files and Imports clauses by augmenting the context using the _append primitive, thereby ensuring that the names introduced by these clauses are all distinct, just as if the Files and Imports clauses of the Model were a single binding constructor. The Files and Imports clauses are evaluated independently:

Eval( Files Imports , C) =
  _append(Eval( Files , C), Eval( Imports , C))

The following two sections give the rules for evaluating Files and Imports clauses individually. It is worth noting that the evaluation context C is ignored in those rules.