language, reduction-relation,
define-metafunction,
stepper, and apply-reduction-relation*. There are
many other functions in the library that build on these four
(and provide variations and extensions), but these four
illustrate the key services that PLT Redex provides.
The first,
(define-language name
(non-terminal-name rhs-pattern ...)
...)
specifies a BNF grammar for a regular tree language. Each right-hand
side is written in PLT Redex's pattern language (consisting of a
mixture of concrete syntax elements and non-terminals, roughly
speaking). With a language definition in place, the
reduction-relation form
is used to define the reduction relation:
(reduction-relation language-name
(--> lhs-pattern consequence) ...)
Syntactically, it consists of three sub-expressions: a language to
which the reduction applies, a source pattern specifying which terms
the rule matches, and Scheme code that, when evaluated, produces the
resulting term as an S-expression.
Metafunctions are defined like this:
(define-metafunction name
lang
[lhs-pattern result] ...)
The define-metafunction form defines a
metafunction by cases. Unlike the reduction relation, the
branches for a metafunction are ordered. As soon as one of
the patterns matches, that branch is taken regardless of
other matches that might happen.
The functions
stepper : language reduction-relation term -> any
traces : language reduction-relation term -> any
open GUI windows that let you explore the reduction graph of
terms reachable from the initial
term. The stepper behaves in a manner similar
to DrScheme's stepper, and traces shows the
reduction graph in a graph-viewing window.
Finally,
apply-reduction-relation* : reduction-relation term -> (listof term)
can be used to develop test
suites for PLT Redex programs. It accepts a reduction
relation and an example term and applies the reduction
relation until it cannot reduce any further, at which point
it returns the irreducible terms.