5 Model

We present a formal model of set-of-scope expansion following the style of Flatt et al. (2012). Complete models, both in typeset form and executable form using PLT Redex, are available as model.zip.

As a first step, we present a model where only run-time expressions are expanded, and implementations of macros are simply parsed. As a second step, we generalize the model to include phase-specific scope sets and macro expansion at all phases. The third step adds support for local expansion, and the fourth step adds first-class definition contexts. The model does not cover modules or top-level namespaces.

5.1 Single-Phase Expansion

The model’s evaluator is standard and relies on a function to implement primitives:

where extracts the content of a syntax object, and creates a new syntax object with a given content and the scopes of a given existing syntax object:

Macro expansion takes a program that is represented as as a syntax object and produces a fully expanded syntax object. To evaluate the program, the syntax object must be parsed into an AST. The parser uses a metafunction that takes an identifier and a binding store, . The names , , and , represent the core syntactic forms, along with the implicit forms of function calls and variable reference:

The metafunction extracts an identifier’s name and its binding context. For now, we ignore phases and define a binding context as simply a set of scopes. A binding store maps a name to a mapping from scope sets to bindings, where bindings are represented by fresh names.

The metafunction uses these pieces along with a helper function to select a binding. If no binding is available in the store, the identifier’s symbol’s name is returned, which effectively allows access to the four primitive syntactic forms; the macro expander will reject any other unbound reference.

Finally, we’re ready to define the metafunction. In addition to a syntax object (for a program to expand) and a binding store, the expander needs an environment, , that maps bindings to compile-time meanings. The possible meanings of a binding are the three primitive syntactic forms recognized by , the primitive form, a reference to a function argument, or a compile-time value—where a compile-time function represents a macro transformer.

The process of macro expansion creates new bindings, so the metafunction produces a tuple containing an updated binding store along with the expanded program. For example, the simplest case is for the form, which leaves the body of the form and the store as-is:

Since we are not yet dealing with expansion of compile-time terms, no scope pruning is needed for , and it can be essentially the same as .

Expansion of a form creates a fresh name and fresh scope for the argument binding. Adding the new scope to the formal argument (we define the metafunction later) creates the binding identifier. The new binding is added to the store, , and it is also recorded in the compile-time environment, , as a variable binding. The body of the function is expanded with those extensions after receiving the new scope, and the pieces are reassembled into a form.

A local macro binding via is similar to an argument binding, but the compile-time environment records a macro transformer instead of a variable. The transformer is produced by using and then on the compile-time expression for the transformer. After the body is expanded, the macro binding is no longer needed, so the body expansion is the result.

Finally, when the expander encounters an identifier that resolves to a binding mapped to a macro transformer, the transformer is applied to the macro use. Fresh scopes are generated to represent the use site, , and introduced syntax, , where the introduced-syntax scope is applied using to both the macro argument and result, where corresponds to an exclusive-or operation to leave the scope intact on syntax introduced by the macro (see below).

The only remaining case of is to recur for function-call forms, threading through the binding store using an accumulator-style helper:

For completeness, here are the and metafunctions for propagating scopes to all parts of a syntax object, where adds to if is not already in or removes it otherwise:

To take a program from source to value, use , then , then .

5.2 Multi-Phase Expansion

To support phase-specific scope sets, we change the definition of so that it is a mapping from phases to scope sets:This model is "phases-model.rkt" in model.zip.

With this change, many metafunctions must be indexed by the current phase of expansion. For example, the result of depends on the current phase:

Phase-specific expansion allows to expand the compile-time expression for a macro implementation, instead of just parsing the expression. Note that the uses of and on the transformer expression are indexed by :

In addition to carrying a phase index, the revised takes a set of scopes created for bindings. Those scopes are the ones to be pruned from quoted syntax by the revised expansion:

The metafunction recurs through a syntax object to remove all of the given scopes at the indicated phase:

5.3 Local Expansion

Environment inspection via syntax-local-value and local expansion via local-expand are accommodated in the model essentially as in Flatt et al. (2012), but since local expansion can create bindings, the metafunction must consume and produce a binding store. The metafunction also must be index by the phase used for syntax operations.

Local expansion needs the current macro expansion’s introduction scope, if any. In addition, local expansions that move identifiers into binding positions need syntax-local-identifier-as-binding, which requires information about scopes in the current expansion context. Local expansion, meanwhile, can create new such scopes. To support those interactions, and must both consume and produce scope sets for the current use-site scopes, and binding scopes must also be available for local expansion of forms. To facilitate threading through all of that information, we define as an optional current scope and as an extended store:This model is "local-model.rkt" in model.zip.

The second part of a tuple is a set of scopes to be pruned at forms. The third part is a subset of those scopes that are the current expansion context’s use-site scopes, which are pruned by syntax-local-identifier-as-binding. The different parts of a tuple vary in different ways: the part is consistently threaded through evaluation and expansion, while the scope-set parts are stack-like for expansion and threaded through evaluation. In the case of a macro-application step, the scope-set parts of the tuple are threaded through expansion, too, more like evaluation.

In the model, the , , and primitives represent syntax-local-value, local-expand, and syntax-local-identifier-as-binding, respectively:

The implementation of uses a new transformer to make an identifier a stopping point for expansion while remembering the former mapping of the identifier. The helper function strips away a constructor:

The expander must recognize transformers to halt expansion at that point:

The revised macro-application rule for shows how the use-site scopes component of is updated and how the current application’s macro-introduction scope is passed to :

In contrast, the revised rule shows how the pruning scope set is extended for expanding the body of the function, the use-site scope set is reset to empty, and all extensions are discarded in the expansion’s resulting store tuple.

5.4 First-Class Definition Contexts

Supporting first-class definition contexts requires no further changes to the metafunction, but the metafunction must be extended to implement the and primitives, which model the syntax-local-make-definition-context and syntax-local-bind-syntaxes functions. This model is "defs-model.rkt" in model.zip.

The primitive allocates a new scope to represent the definition context, and it also allocates a mutable reference to a compile-time environment that initially references the current environment. The two pieces are combined with a value constructor:

The primitive works in two modes. In the first mode, it is given only a definition context and an identifier, and it creates a new binding for the identifier that includes the definition context’s scope. The new binding is mapped to variable in an updated environment for definition context:

When is given an additional syntax object, it expands and evaluates the additional syntax object as a compile-time expression, and it adds a macro binding to the definition context’s environment:

Note that in this mode defines a potentially recursive macro, since the definition context’s scope is added to compile-time expression before expanding and parsing it.

Finally, a definition context is used to expand an expression by providing the definition context as an extra argument to . The implementation of the new case for is similar to the old one, but the definition context’s scope is applied to the given syntax object before expanding it, and the definition context’s environment is used for expansion.