▼ |  | Redex: Debugging Operational Semantics

1 | Patterns
2 | Terms
3 | Languages
4 | Reduction Relations
5 | Metafunctions
6 | Testing
7 | GUI
8 | Typesetting
| Index

► | 8 | Typesetting

8.1 | Picts & Post Script
8.2 | Customization
8.3 | LW

On this page:

8.1`` Picts & Post Script
render-language
language->pict
render-reduction-relation
reduction-relation->pict
render-metafunction
metafunction->pict
8.2`` Customization
render-language-nts
extend-language-show-union
render-reduction-relation-rules
rule-pict-style
reduction-rule-style/ c
arrow-space
horizontal-label-space
metafunction-pict-style
label-style
literal-style
metafunction-style
non-terminal-style
non-terminal-subscript-style
default-style
label-font-size
metafunction-font-size
default-font-size
reduction-relation-rule-separation
curly-quotes-for-strings
current-text
set-arrow-pict!
white-bracket-sizing
with-unquote-rewriter
with-atomic-rewriter
with-compound-rewriter
8.3`` LW
build-lw
lw-e
lw-line
lw-line-span
lw-column
lw-column-span
lw?
lw
to-lw
render-lw
lw->pict
just-before
just-after

Version: 4.1.4
top← prev up next →

### 8`` Typesetting

(require redex/pict)

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: PLT 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 DrScheme to easily adjust the typesetting: render-language, render-reduction-relation, render-metafunction, and render-lw, and one for use in combination with other libraries that operate on picts 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.

(render-language lang [file #:nts nts]) → (if file void? pict?)
lang : compiled-lang?
file : (or/c false/c path-string?) = #f

| nts |  | : |  | (or/c false/c (listof (or/c string? symbol?)))
|  |  | = |  | (render-language-nts)

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.

(language->pict lang [#:nts nts]) → pict?
lang : compiled-lang?

| nts |  | : |  | (or/c false/c (listof (or/c string? symbol?)))
|  |  | = |  | (render-language-nts)

Produce a pict like render-language, but without adjust dc-for-text-size.

This function is primarily designed to be used with Slideshow or with other tools that combine picts together.

(render-reduction-relation |  | rel |
| [ | file |
|  | #:style style]) |

→ (if file void? pict?)
rel : reduction-relation?
file : (or/c false/c path-string?) = #f
style : reduction-rule-style/c = (rule-pict-style)

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.

(reduction-relation->pict r [#:style style]) → pict?
r : reduction-relation?
style : reduction-rule-style/c = (rule-pict-style)

Produces a pict like render-reduction-relation, but without setting dc-for-text-size.

This function is primarily designed to be used with Slideshow or with other tools that combine picts together.

(render-metafunction metafunction-name)

(render-metafunction metafunction-name filename)

If provided with one argument, render-metafunction produces a pict that renders properly in the definitions window in DrScheme. If given two argument, it writes postscript into the file named by filename (which may be either a string or bytes).

This function sets dc-for-text-size. See also metafunction->pict.

(metafunction->pict metafunction-name)

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

(render-language-nts) → (or/c false/c (listof symbol?))
(render-language-nts nts) → void?
nts : (or/c false/c (listof symbol?))

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.

(extend-language-show-union) → boolean?
(extend-language-show-union show?) → void?
show? : boolean?

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.

(render-reduction-relation-rules)
→ (or/c false/c (listof (or/c symbol? string?)))
(render-reduction-relation-rules rules) → void?
rules : (or/c false/c (listof (or/c symbol? string?)))

This parameter controls which rules in a reduction relation will be rendered.

(rule-pict-style) → reduction-rule-style/c
(rule-pict-style style) → void?
style : reduction-rule-style/c

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. Finally, in 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.

reduction-rule-style/c : flat-contract?

A contract equivalent to

(symbols 'vertical
'compact-vertical
'vertical-overlapping-side-conditions
'horizontal)

(arrow-space) → natural-number/c
(arrow-space space) → void?
space : natural-number/c

This parameter controls the amount of extra horizontal space around the reduction relation arrow. Defaults to 0.

(horizontal-label-space) → natural-number/c
(horizontal-label-space space) → void?
space : natural-number/c

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)
→ (parameter/c (symbols 'left-right 'up-down))
(metafunction-pict-style style) → void?
style : (parameter/c (symbols 'left-right 'up-down))

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.

(label-style) → text-style/c
(label-style style) → void?
style : text-style/c

(literal-style) → text-style/c
(literal-style style) → void?
style : text-style/c

(metafunction-style) → text-style/c
(metafunction-style style) → void?
style : text-style/c

(non-terminal-style) → text-style/c
(non-terminal-style style) → void?
style : text-style/c

(non-terminal-subscript-style) → text-style/c
(non-terminal-subscript-style style) → void?
style : text-style/c

(default-style) → text-style/c
(default-style style) → void?
style : text-style/c

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 for non-terminals and 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.

(label-font-size) → (and/c (between/c 1 255) integer?)
(label-font-size size) → void?
size : (and/c (between/c 1 255) integer?)

(metafunction-font-size) → (and/c (between/c 1 255) integer?)
(metafunction-font-size size) → void?
size : (and/c (between/c 1 255) integer?)

(default-font-size) → (and/c (between/c 1 255) integer?)
(default-font-size size) → void?
size : (and/c (between/c 1 255) integer?)

These parameters control the various font sizes. The default-font-size is used for all of the font sizes except labels and metafunctions.

(reduction-relation-rule-separation)
→ (parameter/c (and/c integer? positive? exact?))
(reduction-relation-rule-separation sep) → void?
sep : (parameter/c (and/c integer? positive? exact?))

Controls the amount of space between clauses in a reduction relation. Defaults to 4.

(curly-quotes-for-strings) → boolean?
(curly-quotes-for-strings on?) → void?
on? : boolean?

Controls if the open and close quotes for strings are turned into “ and ” or are left as merely ".

Defaults to #t.

(current-text) → (-> string? text-style/c number? pict?)
(current-text proc) → void?
proc : (-> string? text-style/c number? pict?)

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.

(set-arrow-pict!) → (-> symbol? (-> pict?) void?)
(set-arrow-pict! proc) → void?
proc : (-> symbol? (-> pict?) void?)

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.

(white-bracket-sizing)
→ (-> string? number? (values number? number? number? number?))
(white-bracket-sizing proc) → void?
proc : (-> string? number? (values number? number? number? number?))

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:

(λ (str size)
(let ([inset-amt (floor/even (max 4 (* size 1/2)))])
(cond
[(equal? str "[")
(values inset-amt
0
0
(/ inset-amt 2))]
[else
(values 0
inset-amt
(/ inset-amt 2)
0)])))

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 Scheme 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 Scheme code is an implementation of those operations.

To replace the pink code, use:

(with-unquote-rewriter proc expression)

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.

(with-atomic-rewriter name-symbol string-or-thunk-returning-pict expression)

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.

(with-compound-rewriter name-symbol proc expression)

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) – see below for details on the shape of lw, and is expected to return a new (listof (union 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

(build-lw e line line-span column column-span) → lw?

e

:

(or/c string?
symbol?
pict?
(listof (or/c (symbols 'spring) lw?)))

line : exact-positive-integer?
line-span : exact-positive-integer?
column : exact-positive-integer?
column-span : exact-positive-integer?

(lw-e lw)

→

(or/c string?
symbol?
pict?
(listof (or/c (symbols 'spring) lw?)))

lw : lw?

(lw-line lw) → exact-positive-integer?
lw : lw?

(lw-line-span lw) → exact-positive-integer?
lw : lw?

(lw-column lw) → exact-positive-integer?
lw : lw?

(lw-column-span lw) → exact-positive-integer?
lw : lw?

(lw? v) → boolean?
v : any/c

lw

The lw data structure corresponds represents a pattern or a Scheme 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.

(to-lw arg)

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):

(build-lw (list (build-lw "(" 0 0 0 1)
(build-lw 'a 0 0 1 1)
(build-lw ")" 0 0 2 1))
0 0 0 3)

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.

(build-lw (list (build-lw "(" 0 0 0 1)
(build-lw 'a 0 0 1 1)
(build-lw 'b 0 0 3 1)
(build-lw ")" 0 0 4 1))
0 0 0 5)

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:

(build-lw (list (build-lw "" 1 0 9 0)
'spring
(build-lw x 1 0 10 1))
1 0 9 2)

and the 'spring causes there to be no space between the empty string and the x in the typeset output.

(render-lw language/nts lw) → pict?
language/nts : (or/c (listof symbol?) compiled-lang?)
lw : lw?

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.

(lw->pict language/ntw lw) → pict?
language/ntw : (or/c (listof symbol?) compiled-lang?)
lw : lw?

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.

(just-before stuff lw) → lw?
stuff : (or/c pict? string? symbol?)
lw : lw?

(just-after stuff lw) → lw?
stuff : (or/c pict? string? symbol?)
lw : 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.

top← prev up next →