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 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.