2 The Redex Reference

Alternatively, use the redex/reduction-semantics and redex/pict modules, which provide only non-GUI functionality (i.e., everything except redex/gui), making them suitable for programs which should not depend on racket/gui/base.

2.1 Patterns

This section covers Redex’s pattern language, used in many of Redex’s forms.

Note that pattern matching is caching (including caching the results of side-conditions). This means that once a pattern has matched a given term, Redex assumes that it will always match that term.

This is the grammar for the Redex pattern language. Non-terminal references are wrapped with angle brackets; otherwise identifiers in the grammar are terminals.

• The any pattern matches any sexpression. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The _ pattern matches any sexpression, but does not bind _ as a name, nor can it be suffixed to bind a name.

• The number pattern matches any number. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The natural pattern matches any exact non-negative integer. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The integer pattern matches any exact integer. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The real pattern matches any real number. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The string pattern matches any string. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The boolean pattern matches #true and #false (which are the same as #t and #f, respectively). This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The variable pattern matches any symbol. This pattern may also be suffixed with an underscore and another identifier, in which case they bind the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The variable-except pattern matches any symbol except those listed in its argument. This is useful for ensuring that keywords in the language are not accidentally captured by variables.

• The variable-prefix pattern matches any symbol that begins with the given prefix.

• The variable-not-otherwise-mentioned pattern matches any symbol except those that are used as literals elsewhere in the language.

• The hole pattern matches anything when inside the first argument to an in-hole pattern. Otherwise, it matches only a hole.

• The symbol pattern stands for a literal symbol that must match exactly, unless it is the name of a non-terminal in a relevant language or contains an underscore.

  If it is a non-terminal, it matches any of the right-hand sides of that non-terminal. If the non-terminal appears twice in a single pattern, then the match is constrained to expressions that are the same, unless the pattern is part of a grammar, in which case there is no constraint.

  If the symbol is a non-terminal followed by an underscore, for example e_1, it is implicitly the same as a name pattern that matches only the non-terminal, (name e_1 e) for the example. Accordingly, repeated uses of the same name are constrained to match the same expression.

  If the symbol is a non-terminal followed by _!_, for example e_!_1, it is also treated as a pattern, but repeated uses of the same pattern are constrained to be different. For example, this pattern:

  (e_!_1 e_!_1 e_!_1)

  matches lists of three es, but where all three of them are distinct.

  If the _!_ is used under the ellipsis then the ellipsis is effectively ignored. That is, a pattern like this:

  (e_!_1 ... e_!_1)

  matches all sequences of es that have at least one element and are all distinct.

  Unlike a _ pattern, the _!_ patterns do not bind names.

  If _ names and _!_ are mixed, they are treated as separate. That is, this pattern (e_1 e_!_1) matches just the same things as (e e), but the second doesn’t bind any variables.

  If the symbol otherwise has an underscore, it is an error.

• The pattern (name symbol pattern) matches pattern and binds using it to the name symbol.

• The (in-hole pattern pattern) pattern matches the first pattern. This match must include exactly one match against the second pattern. If there are zero matches or more than one match, an exception is raised.

  When matching the first argument of in-hole, the hole pattern matches any sexpression. Then, the sexpression that matched the hole pattern is used to match against the second pattern.

• The (hide-hole pattern) pattern matches what the embedded pattern matches but if the pattern matcher is looking for a decomposition, it ignores any holes found in that pattern.

• The (side-condition pattern guard) pattern matches what the embedded pattern matches, and then the guard expression is evaluated. If it returns #f, the pattern fails to match, and if it returns anything else, the pattern matches. Any occurrences of name in the pattern (including those implicitly there via _ patterns) are bound using term-let in the guard.

• The (cross symbol) pattern is used for the compatible closure functions. If the language contains a non-terminal with the same name as symbol, the pattern (cross symbol) matches the context that corresponds to the compatible closure of that non-terminal.

• The (pattern-sequence ...) pattern matches a sexpression list, where each pattern-sequence element matches an element of the list. In addition, if a list pattern contains an ellipsis, the ellipsis is not treated as a literal, instead it matches any number of duplicates of the pattern that came before the ellipses (including 0). Furthermore, each (name symbol pattern) in the duplicated pattern binds a list of matches to symbol, instead of a single match. (A nested duplicated pattern creates a list of list matches, etc.) Ellipses may be placed anywhere inside the row of patterns, except in the first position or immediately after another ellipses.

  Multiple ellipses are allowed. For example, this pattern:

  ((name x a) ... (name y a) ...)

  matches this sexpression:

  (term (a a))

  three different ways. One where the first a in the pattern matches nothing, and the second matches both of the occurrences of a, one where each named pattern matches a single a and one where the first matches both and the second matches nothing.

  If the ellipses is named (i.e., has an underscore and a name following it, like a variable may), the pattern matcher records the length of the list and ensures that any other occurrences of the same named ellipses must have the same length.

  As an example, this pattern:

  ((name x a) ..._1 (name y a) ..._1)

  only matches this sexpression:

  (term (a a))

  one way, with each named pattern matching a single a. Unlike the above, the two patterns with mismatched lengths is ruled out, due to the underscores following the ellipses.

  Also, like underscore patterns above, if an underscore pattern begins with ..._!_, then the lengths must be different.

  Thus, with the pattern:

  ((name x a) ..._!_1 (name y a) ..._!_1)

  and the expression

  (term (a a))

  two matches occur, one where x is bound to '() and y is bound to '(a a) and one where x is bound to '(a a) and y is bound to '().

If redex-match receives only two arguments, it builds a procedure for efficiently testing if expressions match the pattern, using the language lang. The procedures accepts a single expression and if the expression matches, it returns a list of match structures describing the matches. If the match fails, the procedure returns #f.

Caching should be disabled when matching a pattern that depends on values other than the in-scope pattern variables or evaluating a metafunction that reads or writes mutable external state.

The default size is 350.

2.2 Terms

Object language expressions in Redex are written using term. It is similar to Racket’s quote (in many cases it is identical) in that it constructs lists as the visible representation of terms.

The grammar of terms is (note that an ellipsis stands for repetition unless otherwise indicated):

• A term written identifier is equivalent to the corresponding symbol, unless the identifier is bound by term-let, define-term, or a pattern variable or the identifier is hole (as below).

• A term written (term-sequence ...) constructs a list of the terms constructed by the sequence elements.

• A term written ,racket-expression evaluates the racket-expression and substitutes its value into the term at that point.

• A term written ,@racket-expression evaluates the racket-expression, which must produce a list. It then splices the contents of the list into the expression at that point in the sequence.

• A term written (in-hole term term) is the dual to the pattern in-hole – it accepts a context and an expression and uses plug to combine them.

• A term written hole produces a hole.

• A term written as a literal boolean or a string produces the boolean or the string.

It behaves similarly to quasiquote, except for a few special forms that are recognized (listed below) and that names bound by term-let are implicitly substituted with the values that those names were bound to, expanding ellipses as in-place sublists (in the same manner as syntax-case patterns).

The optional #:lang keyword must supply an identifier bound by define-language, and adds a check that any symbol containing an underscore in term could have been bound by a pattern in the language referenced by lang-id. In practice, this means that the underscore must be preceded by a non-terminal in that language or a built-in pattern such as number. This form of term is used internally by default, so this check is applied to terms that are constructed by Redex forms such as reduction-relation and define-metafunction.

For example,

(term-let ([body '(+ x 1)]

[(expr ...) '(+ - (values * /))]

[((id ...) ...) '((a) (b) (c d))])

(term (let-values ([(id ...) expr] ...) body)))

evaluates to

'(let-values ([(a) +]

[(b) -]

[(c d) (values * /)])

(+ x 1))

It is an error for a term variable to appear in an expression with an ellipsis-depth different from the depth with which it was bound by term-let. It is also an error for two term-let-bound identifiers bound to lists of different lengths to appear together inside an ellipsis.

Note that each ellipsis should be the literal symbol consisting of three dots (and the ... elsewhere indicates repetition as usual). If tl-pat is an identifier, it matches any value and binds it to the identifier, for use inside term. If it is a list, it matches only if the value being matched is a list value and only if every subpattern recursively matches the corresponding list element. There may be a single ellipsis in any list pattern; if one is present, the pattern before the ellipses may match multiple adjacent elements in the list value (possibly none).

This form is a lower-level form in Redex, and not really designed to be used directly. For let-like forms that use Redex’s full pattern matching facilities, see redex-let, redex-let*, term-match, term-match/single.

This form raises an exception recognized by exn:fail:redex? if any right-hand side does not match its left-hand side in exactly one way.

In some contexts, it may be more efficient to use term-match/single (lifted out of the context).

When evaluating a term-match expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.

Raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways.

When evaluating a term-match/single expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.

Does not expect the input symbols to be distinct, but does produce variables that are always distinct.

2.3 Languages

A non-terminal-def comprises one or more non-terminal names (considered aliases) followed by one or more productions.

For example, the following defines lc-lang as the grammar of the λ-calculus:

(define-language lc-lang

(e (e e ...)

x

v)

(c (v ... c e ...)

hole)

(v (λ (x ...) e))

(x variable-not-otherwise-mentioned))

with non-terminals e for the expression language, x for variables, c for the evaluation contexts and v for values.

(define-extended-language lc-num-lang

lc-lang

(v ....     ; extend the previous `v' non-terminal

number

+)

(x (variable-except λ +)))

extends lc-lang with two new alternatives (+ and number) for the v non-terminal, carries forward the e and c non-terminals, and replaces the x non-terminal with a new one (which happens to be equivalent to the one that would have been inherited).

The four-period ellipses indicates that the new language’s non-terminal has all of the alternatives from the original language’s non-terminal, as well as any new ones. If a non-terminal occurs in both the base language and the extension, the extension’s non-terminal replaces the originals. If a non-terminal only occurs in either the base language, then it is carried forward into the extension. And, of course, extend-language lets you add new non-terminals to the language.

If a language is has a group of multiple non-terminals defined together, extending any one of those non-terminals extends all of them.

If a language has a prefix, then all of the non-terminals from that language have the corresponding prefix in the union language. The prefix helps avoid unintended collisions between the constituent language’s non-terminals.

2.4 Reduction Relations

The optional domain clause provides a contract for the relation, in the form of a pattern that defines the relation’s domain and codomain.

The arrow-name in each reduction-case clause is either base-arrow-name (default -->) or an arrow name defined by shortcuts (described below). In either case, the pattern refers to language and binds variables in the corresponding term. Following the pattern and term can be the name of the reduction rule and declarations of fresh variables and side-conditions.

For example, the expression

(reduction-relation

lc-lang

(--> (in-hole c_1 ((λ (variable_i ...) e_body) v_i ...))

(in-hole c_1 ,(foldl lc-subst

(term e_body)

(term (v_i ...))

(term (variable_i ...))))

beta-v))

defines a reduction relation for the lc-lang grammar.

A rule’s name (used in typesetting, the stepper, traces, and apply-reduction-relation/tag-with-names) can be given as a literal (an identifier or a string) or as an expression that computes a name using the values of the bound pattern variables (much like the rule’s right-hand side). Some operations require literal names, so a rule definition may provide both a literal name and a computed name. In particular, only rules that include a literal name may be replaced using extend-reduction-relation, used as breakpoints in the stepper, and selected using render-reduction-relation-rules. The output of apply-reduction-relation/tag-with-names, traces, and the stepper prefers the computed name, if it exists. Typesetting a rule with a computed name shows the expression that computes the name only when the rule has no literal name or when it would not typeset in pink due to with-unquote-rewriters in the context; otherwise, the literal name (or nothing) is shown.

Fresh variable clauses generate variables that do not occur in the term being reduced. If the fresh-clause is a variable, that variable is used both as a binding in the term and as the prefix for the freshly generated variable. (The variable does not have to be a non-terminal in the language of the reduction relation.)

The second form of fresh-clauses generates a sequence of variables. In that case, the ellipses are literal ellipses; that is, you must actually write ellipses in your rule. The variable var1 is like the variable in first case of a fresh-clause; namely it is used to determine the prefix of the generated variables and it is bound in the right-hand side of the reduction rule, but unlike the single-variable fresh clause, it is bound to a sequence of variables. The variable var2 is used to determine the number of variables generated and var2 must be bound by the left-hand side of the rule.

The expressions within side-condition clauses and side-condition/hidden clauses are collected with and and used as guards on the case being matched. The argument to each side-condition should be a Racket expression, and the pattern variables in the pattern are bound in that expression. A side-condition/hidden clause is the same as a side-condition clause, except that the condition is not rendered when typesetting via redex/pict.

Each where clause acts as a side condition requiring a successful pattern match, and it can bind pattern variables in the side-conditions (and where clauses) that follow and in the metafunction result. The bindings are the same as bindings in a term-let expression. A where/hidden clause is the same as a where clause, but the clause is not rendered when typesetting via redex/pict.

Each judgment-holds clause acts like a where clause, where the left-hand side pattern incorporates each of the patterns used in the judgment form’s output positions.

Each shortcut clause defines arrow names in terms of base-arrow-name and earlier shortcut definitions. The left- and right-hand sides of a shortcut definition are identifiers, not patterns and terms. These identifiers need not correspond to non-terminals in language.

For example, this expression

(reduction-relation

lc-num-lang

(==> ((λ (variable_i ...) e_body) v_i ...)

,(foldl lc-subst

(term e_body)

(term (v_i ...))

(term (variable_i ...))))

(==> (+ number_1 ...)

,(apply + (term (number_1 ...))))

with

[(--> (in-hole c_1 a) (in-hole c_1 b))

(==> a b)])

defines reductions for the λ-calculus with numbers, where the ==> shortcut is defined by reducing in the context c.

A fresh clause in reduction-case defined by shortcut refers to the entire term, not just the portion matched by the left-hand side of shortcut’s use.

If the original reduction-relation has a rule with the same name as one of the rules specified in the extension, the old rule is removed.

If the cache-all? argument is #t, then apply-reduction-relation* keeps a cache of all visited terms when traversing the graph and does not revisit any of them. This cache can, in some cases, use a lot of memory, so it is off by default and the cycle checking happens by keeping track only of the current path it is traversing through the reduction graph.

The stop-when argument controls the stopping criterion. Specifically, it is called with each term that apply-reduction-relation* encounters. If it ever returns a true value (anything except #f), then apply-reduction-relation* considers the term to be irreducible (and so returns it and does not try to reduce it further).

2.5 Other Relations

The contract, if present, is matched against every input to the metafunction and, if the match fails, an exception is raised. If present, the term inside the maybe-pre-condition is evaluated after a successful match to the input pattern in the contract (with any variables from the input contract bound). If it returns #f, then the input contract is considered to not have matched and an error is also raised. When a metafunction returns, the expression in the maybe-post-condition is evaluated (if present), with any variables from the input or output contract bound.

The side-condition, hidden-side-condition, where, and where/hidden clauses behave as in the reduction-relation form.

The resulting metafunction raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways (and that leads to different results for the different matches).

The side-condition extra is evaluated after a successful match to the corresponding argument pattern. If it returns #f, the clause is considered not to have matched, and the next one is tried. The side-condition/hidden extra behaves the same, but is not typeset.

The where and where/hidden extra are like side-condition and side-condition/hidden, except the match guards the clause.

The judgment-holds clause is like side-condition and where, except the given judgment must hold for the clause to be taken.

The clause-name is used only when typesetting. See metafunction-cases.

Note that metafunctions are assumed to always return the same results for the same inputs, and their results are cached, unless caching-enabled? is set to #f. Accordingly, if a metafunction is called with the same inputs twice, then its body is only evaluated a single time.

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

(define-metafunction lc-lang

free-vars : e -> (x ...)

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

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

[(free-vars x) (x)]

[(free-vars (λ (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 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 λ 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.

Changed in version 1.4 of package redex-lib: Added #:post conditions.

For example, define-metafunction/extension may be used to extend the free-vars function above to the forms introduced by the language lc-num-lang.

(define-metafunction/extension free-vars lc-num-lang

free-vars-num : e -> (x ...)

[(free-vars-num number)

()]

[(free-vars-num (+ e_1 e_2))

(∪ (free-vars-num e_1)

(free-vars-num e_2))])