5 Metafunctions

All of the exports in this section are provided both by redex/reduction-semantics (which includes all non-GUI portions of Redex) and also exported by redex (which includes all of Redex).

(define-metafunction language-exp  contract  [(name pattern ...) term (side-condition scheme-expression) ...]  ...)

contract   =       |   id : pattern ... -> pattern

The define-metafunction form builds a function on sexpressions according to the pattern and right-hand-side expressions. The first argument indicates the language used to resolve non-terminals in the pattern expressions. Each of the rhs-expressions is implicitly wrapped in `term’. In addition, recursive calls in the right-hand side of the metafunction clauses should appear inside `term’.

If specified, the side-conditions are collected with and and used as guards on the case being matched. The argument to each side-condition should be a Scheme expression, and the pattern variables in the <pattern> are bound in that expression.

As an example, these metafunctions finds the free variables in an expression in the lc-lang above:

(define-metafunction lc-lang

free-vars : e -> (listof x)

[(free-vars (e_1 e_2 ...))

(∪ (free-vars e_1) (free-vars e_2) ...)]

[(free-vars x) (x)]

[(free-vars (lambda (x ...) e))

(- (free-vars e) (x ...))])

The first argument to define-metafunction is the grammar (defined above). Following that are three cases, one for each variation of expressions (e in lc-lang). The right-hand side of each clause begins with a comma, since they are implicitly wrapped in `term’. The free variables of an application are the free variables of each of the subterms; the free variables of a variable is just the variable itself, and the free variables of a lambda expression are the free variables of the body, minus the bound parameters.

Here are the helper metafunctions used above.

(define-metafunction lc-lang

∪ : (x ...) ... -> (x ...)

[(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...)

(∪ (x_1 ... x_2 ...) (x_3 ...) ...)]

[(∪ (x_1 ...))

(x_1 ...)]

[(∪) ()])

(define-metafunction lc-lang

- : (x ...) (x ...) -> (x ...)

[(- (x ...) ()) (x ...)]

[(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...))

(- (x_1 ... x_3 ...) (x_2 x_4 ...))

(side-condition (not (memq (term x_2) (term (x_3 ...)))))]

[(- (x_1 ...) (x_2 x_3 ...))

(- (x_1 ...) (x_3 ...))])

Note the side-condition in the second case of -. It ensures that there is a unique match for that case. Without it, (term (- (x x) x)) would lead to an ambiguous match.

(define-metafunction/extension extending-name language-exp   contract   [(name pattern ...) term (side-condition scheme-expression) ...]   ...)

This defines a metafunction as an extension of an existing one. The extended metafunction behaves as if the original patterns were in this definitions, with the name of the function fixed up to be extending-name.

(in-domain? (metafunction-name term ...))

Returns #t if the inputs specified to metafunction-name are legtimate inputs according to metafunction-name’s contract, and #f otherwise.