This library is under development;
compatibility will not be maintained.
This package implements miscellaneous
metafunctions, macros, and functions
For the purposes of illustration,
we will use the following language
in our examples.
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
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.
|> (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.
|> (term (rem ([x 1] [y 2]) x z))|
(match-term lang expression [pattern expression] ...)
Matches the given term against a series of patterns,
choosing the expression corresponding to the first matching pattern.
Returns if the given pattern doesn’t match the term.
Returns an evaluation function that applies the given reduction relation
until reaching a normal form. The evaluation function will
into an initial machine configuration
out of the final configuration.
Initial and final expressions will be checked against program?
The evaluation function takes a maximum of current-max-steps
Additionally it will throw an error
on a non-deterministic or non-terminating result.
A parameter that determines the maximum number of steps the evaluation
function created by make-eval
will take before quitting.
|> (⇓ (term ((λ (x) ((x x) x)) (λ (y) ((y y) y)))))|
make-eval: exceeded maximum number of steps
Redex has the ability to typeset your model
for use directly in a paper.
the default typesetting options
are out of place in
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.
Rewriter for substitutions.
Rewriter for lookups.
Rewriter for typing.
Rewriter for adding an element to a set.
Rewriters for font families.
The rewriters to use when rendering stylish.