8 Typesetting
The redex/pict library provides functions
designed to automatically typeset grammars, reduction
relations, and metafunction written with plt redex.
Each grammar, reduction relation, and metafunction can be
saved in a .ps file (as encapsulated postscript), or can be
turned into a pict for viewing in the REPL or using with
Slideshow (see
Slideshow: Racket Figure and Presentation Tools).
8.1 Picts & PostScript
This section documents two classes of operations, one for
direct use of creating postscript figures for use in papers
and for use in DrRacket to easily adjust the typesetting:
render-term,
render-language,
render-reduction-relation,
render-metafunctions, and
render-lw,
and one
for use in combination with other libraries that operate on picts
term->pict,
language->pict,
reduction-relation->pict,
metafunction->pict, and
lw->pict.
The primary difference between these functions is that the former list
sets dc-for-text-size and the latter does not.
Renders the term
term. If
file is
#f,
it produces a pict; if
file is a path, it saves
Encapsulated PostScript in the provided filename. See
render-language for details on the construction of the pict.
This function is primarily designed to be used with
Slideshow or with other tools that combine picts together.
Renders a language. If
file is
#f,
it produces a pict; if
file is a path, it saves
Encapsulated PostScript in the provided filename. See
render-language-nts for information on the
nts argument.
This function parameterizes dc-for-text-size to install a
relevant dc: a bitmap-dc% or a post-script-dc%, depending on
whether file is a path.
See language->pict if you are using Slideshow or
are otherwise setting dc-for-text-size.
This function is primarily designed to be used with
Slideshow or with other tools that combine picts together.
Renders a reduction relation. If
file is
#f,
it produces a pict; if
file is a path, it saves
Encapsulated PostScript in the provided filename. See
rule-pict-style for information on the
style argument.
This function parameterizes dc-for-text-size to install a
relevant dc: a bitmap-dc% or a post-script-dc%, depending on
whether file is a path. See also
reduction-relation->pict.
The following forms of arrows can be typeset:
--> -+> ==> -> => ..> >-> ~~> ~> :-> :–> c-> –>> >– –< >>– –<<
This function is
primarily designed to be used with Slideshow or with
other tools that combine picts together.
If provided with one argument,
render-metafunction
produces a pict that renders properly in the definitions
window in DrRacket. If given two arguments, it writes
postscript into the file named by
filename (which
may be either a string or bytes).
Similarly, render-metafunctions accepts multiple
metafunctions and renders them together, lining up all of the
clauses together.
This function sets dc-for-text-size. See also
metafunction->pict and
metafunctions->pict.
This produces a pict, but without setting
dc-for-text-size.
It is suitable for use in Slideshow or other libraries that combine
picts.
8.2 Customization
The value of this parameter controls which non-terminals
render-language and
language->pict render by default. If it
is
#f (the default), all non-terminals are rendered.
If it is a list of symbols, only the listed symbols are rendered.
See also language-nts.
If this is #t, then a language constructed with
extend-language is shown as if the language had been
constructed directly with language. If it is #f, then only
the last extension to the language is shown (with
four-period ellipses, just like in the concrete syntax).
Defaultly #f.
Note that the #t variant can look a little bit strange if
.... are used and the original version of the language has
multi-line right-hand sides.
This parameter controls which rules in a reduction relation
will be rendered.
This parameter controls the style used by default for the reduction
relation. It can be 'horizontal, where the left and
right-hand sides of the reduction rule are beside each other or
'vertical, where the left and right-hand sides of the
reduction rule are above each other. The 'compact-vertical
style moves the reduction arrow to the second line and uses less space
between lines. The 'vertical-overlapping-side-conditions
variant, the side-conditions don’t contribute to the width of the
pict, but are just overlaid on the second line of each rule. The
'horizontal-left-align style is like the 'horizontal
style, but the left-hand sides of the rules are aligned on the left,
instead of on the right.
A contract equivalent to
| (symbols 'vertical |
| 'compact-vertical |
| 'vertical-overlapping-side-conditions |
| 'horizontal) |
This parameter controls the amount of extra horizontal space
around the reduction relation arrow. Defaults to 0.
This parameter controls the amount of extra space before the
label on each rule, but only in horizontal mode. Defaults to
0.
| (metafunction-pict-style) |
| | → | | | (or/c 'left-right | | 'up-down | | 'left-right/vertical-side-conditions | | 'up-down/vertical-side-conditions | | 'left-right/compact-side-conditions | | 'up-down/compact-side-conditions | | 'left-right/beside-side-conditions) |
|
|
| (metafunction-pict-style style) → void? |
| | style | | : | | | (or/c 'left-right | | 'up-down | | 'left-right/vertical-side-conditions | | 'up-down/vertical-side-conditions | | 'left-right/compact-side-conditions | | 'up-down/compact-side-conditions | | 'left-right/beside-side-conditions) |
|
|
This parameter controls the style used for typesetting
metafunctions. The 'left-right style means that the
results of calling the metafunction are displayed to the
right of the arguments and the 'up-down style means that
the results are displayed below the arguments.
The 'left-right/vertical-side-conditions and
'up-down/vertical-side-conditions variants format side
conditions each on a separate line, instead of all on the same line.
The 'left-right/compact-side-conditions and
'up-down/compact-side-conditions variants move side
conditions to separate lines to avoid making the rendered form wider
than it would be otherwise.
The 'left-right/beside-side-conditions variant is like
'left-right, except it puts the side-conditions on the
same line, instead of on a new line below the case.
This parameter controls which cases in a metafunction are rendered. If it is #f (the default), then all of the
cases appear. If it is a list of numbers, then only the selected cases appear (counting from 0).
These parameters determine the font used for various text in
the picts. See
text in the texpict collection for
documentation explaining
text-style/c. One of the more
useful things it can be is one of the symbols
'roman,
'swiss, or
'modern, which are a serif, sans-serif, and
monospaced font, respectively. (It can also encode style
information, too.)
The label-style is used for the reduction rule label
names. The literal-style is used for names that aren’t
non-terminals that appear in patterns. The
metafunction-style is used for the names of
metafunctions.
The non-terminal-style is used for the names of non-terminals.
Two parameters style the text in the (optional) "underscore" component
of a non-terminal reference. The first, non-terminal-subscript-style,
applies to the segment between the underscore and the first caret (^)
to follow it; the second, non-terminal-superscript-style, applies
to the segment following that caret. For example, in the non-terminal
reference x_y_z, x has style non-terminal-style,
y has style non-terminal-subscript-style, and z
has style non-terminal-superscript-style.
The
non-terminal-subscript-style is used for the portion
after the underscore in non-terminal references.
The default-style is used for parenthesis, the dot in dotted
lists, spaces, the separator words in the grammar, the
"where" and "fresh" in side-conditions, and other places
where the other parameters aren’t used.
These parameters control the various font sizes. The
default-font-size is used for all of the font sizes except
labels and metafunctions.
Controls the amount of space between clauses in a reduction
relation. Defaults to 4.
Controls if the open and close quotes for strings are turned
into “ and ” or are left as merely ".
Defaults to #t.
This parameter’s function is called whenever Redex typesets
some part of a grammar, reduction relation, or
metafunction. It defaults to slideshow’s
text function.
This functions sets the pict for a given reduction-relation
symbol. When typesetting a reduction relation that uses the
symbol, the thunk will be invoked to get a pict to render
it. The thunk may be invoked multiple times when rendering a
single reduction relation.
This parameter is used when typesetting metafunctions to
determine how to create the 〚〛
characters. Rather than using those characters directory
(since glyphs tend not to be available in PostScript
fonts), they are created by combining two ‘[’ characters
or two ‘]’ characters together.
The procedure accepts a string that is either "["
or "]", and returns four numbers. The first two
numbers determine the offset (from the left and from the
right respectively) for the second square bracket, and the
second two two numbers determine the extra space added (to
the left and to the right respectively).
The default value of the parameter is:
where floor/even returns the nearest even number
below its argument. This means that for sizes 9, 10, and
11, inset-amt will be 4, and for 12, 13, 14, and
15, inset-amt will be 6.
Removing the pink background from PLT Redex rendered picts and ps files
When reduction rules, a metafunction, or a grammar contains
unquoted Racket code or side-conditions, they are rendered
with a pink background as a guide to help find them and
provide alternative typesettings for them. In general, a
good goal for a PLT Redex program that you intend to typeset
is to only include such things when they correspond to
standard mathematical operations, and the Racket code is an
implementation of those operations.
To replace the pink code, use:
It installs proc the current unqoute rewriter and
evaluates expression. If that expression computes any picts,
the unquote rewriter specified is used to remap them.
The proc should be a function of one argument. It receives
a lw struct as an argument and should return
another lw that contains a rewritten version of the
code.
This extends the current set of atomic-rewriters with one
new one that rewrites the value of name-symbol to
string-or-pict-returning-thunk (applied, in the case of a
thunk), during the evaluation of expression.
name-symbol is expected to evaluate to a symbol. The value
of string-or-thunk-returning-pict is used whever the symbol
appears in a pattern.
This extends the current set of compound-rewriters with one
new one that rewrites the value of name-symbol via proc,
during the evaluation of expression.
name-symbol is expected to evaluate to a symbol. The value
of proc is called with a (listof lw), and is expected to
return a new (listof (or/c lw? string? pict?)),
rewritten appropriately.
The list passed to the rewriter corresponds to the
lw for the sequence that has name-symbol’s value at
its head.
The result list is constrained to have at most 2 adjacent
non-lws. That list is then transformed by adding
lw structs for each of the non-lws in the
list (see the description of lw below for an
explanation of logical-space):
If there are two adjacent lws, then the logical
space between them is filled with whitespace.
If there is a pair of lws with just a single
non-lw between them, a lw will be
created (containing the non-lw) that uses all
of the available logical space between the lws.
If there are two adjacent non-lws between two
lws, the first non-lw is rendered
right after the first lw with a logical space
of zero, and the second is rendered right before the
last lw also with a logical space of zero, and
the logical space between the two lws is
absorbed by a new lw that renders using no
actual space in the typeset version.
8.3 LW
The lw data structure corresponds represents a pattern or a Racket
expression that is to be typeset. The functions listed above
construct lw structs, select fields out of them, and
recognize them. The lw binding can be used with
copy-struct.
This form turns its argument into lw structs that
contain all of the spacing information just as it would appear
when being used to typeset.
Each sub-expression corresponds to its own lw, and
the element indicates what kind of subexpression it is. If
the element is a list, then the lw corresponds to a
parenthesized sequence, and the list contains a lw
for the open paren, one lw for each component of the
sequence and then a lw for the close
parenthesis. In the case of a dotted list, there will also
be a lw in the third-to-last position for the dot.
For example, this expression:
(a)
becomes this lw (assuming the above expression
appears as the first thing in the file):
If there is some whitespace in the sequence, like this one:
(a b)
then there is no lw that corresponds to that
whitespace; instead there is a logical gap between the
lws.
In general, identifiers are represented with symbols and
parenthesis are represented with strings and picts can be
inserted to render arbitrary pictures.
The line, line-span, column, and column-span correspond to
the logical spacing for the redex program, not the actual
spacing that will be used when they are rendered. The
logical spacing is only used when determining where to place
typeset portions of the program. In the absense of any
rewriters, these numbers correspond to the line and column
numbers in the original program.
The line and column are absolute numbers from the beginning
of the file containing the expression. The column number is
not necessarily the column of the open parenthesis in a
sequence – it is the leftmost column that is occupied by
anything in the sequence. The line-span is the number of
lines, and the column span is the number of columns on the
last line (not the total width).
When there are multiple lines, lines are aligned based on
the logical space (ie, the line/column &
line-span/column-span) fields of the lws. As an
example, if this is the original pattern:
| (all good boys |
| deserve fudge) |
then the leftmost edges of the words "good" and "deserve"
will be lined up underneath each other, but the relative
positions of "boys" and "fudge" will be determined by the
natural size of the words as they rendered in the
appropriate font.
When 'spring appears in the list in the e
field of a lw struct, then it absorbs all of the
space around it. It is also used by to-lw when
constructing the picts for unquoted strings. For example, this expression
,x
corresponds to these structs:
and the 'spring causes there to be no space between
the empty string and the x in the typeset output.
Produces a pict that corresponds to the lw object
argument, using language/nts to determine which
of the identifiers in the lw argument are
non-terminals.
This function sets dc-for-text-size. See also
lw->pict.
Produces a pict that corresponds to the lw object
argument, using language/nts to determine which
of the identifiers in the lw argument are
non-terminals.
This does not set the dc-for-text-size parameter. See also
render-lw.
These two helper functions build new lws whose contents are
the first argument, and whose line and column are based on
the second argument, making the new loc wrapper be either
just before or just after that argument. The line-span and
column-span of the new lw is always zero.