8.0
Redex Miscellanea
This library is under development;
compatibility will not be maintained.
This package implements miscellaneous
metafunctions, macros, and functions
for Redex.
For the purposes of illustration,
we will use the following language
in our examples.
1 Metafunctions
Given an environment, a list of keys and values, replaces instances
of key with value in the target term.
Shorthand for a call to
substitute-env with the given
key-
value pairs as an environment.
(lookup ([key value] ...) needle)
|
Returns the first value whose key matches the needle.
If none match, #f is returned.
(ext ([key value] ...) [new-key new-value] ...)
|
Extends the given environment with the new key-value pairs,
adding where the key isn’t already present,
and overriding the value if the key is present.
Example:
| > (term (ext ([x 1] [y 2]) [x 2] [z 3])) |
'((z 3) (x 2) (y 2)) |
Returns whether the given elements are unique.
(rem ([key value] ...) old-key ...)
|
Removes the associations with the old-key if they are present
in the environment. Does nothing otherwise.
Example:
| > (term (rem ([x 1] [y 2]) x z)) |
'((y 2)) |
2 Macros
(match-term lang expression [pattern expression] ...)
|
Matches the given term against a series of patterns,
choosing the expression corresponding to the first matching pattern.
3 Functions
Returns an evaluation function that applies the given reduction relation
until reaching a normal form. The evaluation function will
inject into an initial machine configuration
and
project out of the final configuration.
Initial and final expressions will be checked against
program?
and
answer? respectively.
The evaluation function takes a maximum of
current-max-steps steps
before aborting.
Additionally it will throw an error
on a non-deterministic or non-terminating result.
Examples:
A parameter that determines the maximum number of steps the evaluation
function created by
make-eval will take before quitting.
Example:
| > (⇓ (term ((λ (x) ((x x) x)) (λ (y) ((y y) y))))) |
make-eval: exceeded maximum number of steps |
4 Typography
Redex has the ability to typeset your model
for use directly in a paper.
Sadly,
the default typesetting options
are out of place in
acmart
papers.
What follows are a bunch of
“stylish” rendering utilities
that typeset the model
with my preferences.
|
| |
| non-terminal-def | | = | | (nt ...+ ∈ nt-set ::= pattern ...+ maybe-rhs) | | | | | | | | maybe-rhs | | = | | | | | | | | | #:define | | | | | | | #:define rhs-expr |
|
Defines a language like
define-language,
but also defines non-terminal set names.
Predicate that recognizes an
nt-set.
Maps symbols to strings for the arrows in a reduction relation.
Fonts and font preferences for stylish renderers.
5 Rewriting
Rewriter for substitutions.
Rewriter for lookups.
Rewriter for typing.
Rewriter for adding an element to a set.
Rewriters for font families.
Unquoted rewriter.
The rewriters to use when rendering stylish.
