6.1
Unstable Redex: May Change Without Warning
This library is unstable;
compatibility will not be maintained.
See Unstable: May Change Without Warning
for more information.
This library provides functions to help typesetting for
redex models. The following example program provides
an overview of the features:
| > (define-language ZF | | [e empty | | (Set e) | | (Union e_1 e_2) | | (Powerset e) | | ZZ | | variable-not-otherwise-mentioned] | | [formula (same? e_1 e_2) | | (in? e_1 e_2) | | true | | false | | (implies formula_1 formula_2)]) |
|
|
By default, Redex models are typeset as S-expressions with some basic
styling that distinguishes literals from nonterminal names, handles
subscripting, etc.
This library provides helper functions for creating and using
rewriters that transform the S-expression model terms into other
notations.
Contract for even-length lists of alternating key/c and
value/c values.
Equivalent to
Contract for compound rewriters, which take a list of
lw
structs and returns a list of
lws,
picts, or
strings.
Equivalent to
Typesets (sym term1 term2) using operator as a
binary operator between term1 and term2.
Redex terms may become ambiguous when typeset. To avoid ambiguity, use
#:parenthesize-arg to direct when arguments should be
parenthesized. If parenthesize-arg is #t, then
arguments are always parenthesized; if it is #f, never; if it
is a list of symbols, then an argument is parenthesized only if the
argument is a term starting with a symbol in the list; if it is a
procedure, then the argument is parenthesized if the procedure applied
to the argument’s lw struct returns a true value.
The parenthesization rules for left and right arguments can be
supplied separately through #:parenthesize-left and
#:parenthesize-right, for example to create left-associated
or right-associated operators:
Typesets (sym term) by placing prefix before
term.
Typesets (sym term) by placing postfix after
term.
Typesets
(sym term ...) by placing
function before
the parenthesized, comma-separated list of
terms.
Typesets
(sym term1 term2 ...) as
term1. Useful
for hiding parameters that are necessary for defining the semantics
but can be glossed over in its explanation, such as state parameters
used for generating unique names.
Typesets
(sym term ...) by rendering the
terms
side-by-side.
Typesets
(sym term ...) as
constant.
Typesets
(sym term ...) by surrounding the comma-separated
(or space-separated, if
comma? is false) sequence of
terms with brackets. If
brackets is a list, the
first element is the left bracket and the second is the right bracket;
'round is equivalent to
'("(" ")");
'square
is equivalent to
'("[" "]");
'curly is equivalent to
'("{" "}"); and
'angle is equivalent to
'("〈" "〉").
Rewriter that typesets (sym elem-term set-term) as the
union of the singleton set containing elem-term with the set
set-term.
