4.8 Typesetting

8.15.0.5

4.8 Typesetting🔗ℹ

The redex/pict library provides functions designed to typeset grammars, reduction relations, and metafunctions.

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 the pict library).

For producing papers with Scribble, just include the picts inline in the paper and pass the --dvipdf flag to generate the ".pdf" file. For producing papers with LaTeX, create ".ps" files from Redex and use latex and dvipdf to create ".pdf" files (using pdflatex with ".pdf" files will work but the results will not look as good onscreen).

4.8.1 Picts, PDF, & 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-relation, render-judgment-form, 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, relation->pict, judgment-form->pict, derivation->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.

syntax
(render-term lang term)
(render-term lang term file)

Renders the term term. If file is #f or not present, render-term produces a pict; if file is a path, it saves Encapsulated PostScript in the provided filename, unless the filename ends with ".pdf", in which case it saves PDF.

Examples:

> (define-language nums
    (AE K
        (+ AE AE))
    ; binary digits
    (k 1 0)
    ; binary constants
    (K · (k K)))
> (render-term nums (+ (1 (0 (1 ·))) (+ (1 (1 (1 ·))) (1 (0 (0 ·))))))

The term argument must be a literal; it is not an evaluated position. For example:

Example:

> (let ([x (term (+ (1 (1 (1 ·))) (1 (0 (0 ·)))))])
(render-term nums x))

but also see render-term/pretty-write.

See render-language for more details on the construction of the pict.

Changed in version 1.16 of package redex-pict-lib: Changed how in-hole renders when its second argument is hole, avoiding a special case for that situation.

syntax
(term->pict lang term)

Produces a pict like render-term, but without adjusting dc-for-text-size.

The first argument is expected to be a compiled-lang? and the second argument is expected to be a term (without the term wrapper). The formatting in the term argument is used to determine how the resulting pict will look.

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

Example:

> (term->pict nums (+ 1 (+ 3 4)))

procedure
(render-term/pretty-write lang
term
[ filename
#:width width])
→ (or/c void? pict-convertible?)
  lang : compiled-lang?
  term : any/c
  filename : (or/c path-string? #f) = #f
   width : (or/c exact-positive-integer? 'infinity)
= (pretty-print-columns)

Like render-term, except that the term argument is evaluated, and expected to return a term. Then, pretty-write is used to determine where the line breaks go, using the width argument as a maximum width (via pretty-print-columns).

If filename is provided, the pict is saved as a pdf to that file.

Example:

> (render-term/pretty-write nums '(+ (1 1 1) (1 0 1)))

procedure
(term->pict/pretty-write lang
term
[ #:width width]) → pict-convertible?
  lang : compiled-lang?
  term : any/c
   width : (or/c exact-positive-integer? 'infinity)
= (pretty-print-columns)

Like term->pict, but with the same change that render-term/pretty-write has from render-term.

Example:

> (term->pict/pretty-write nums '(+ (1 1 1) (1 0 1)))

procedure
(render-language lang [file #:nts nts])
→ (if file void? pict-convertible?)
  lang : compiled-lang?
  file : (or/c #f path-string?) = #f
   nts : (or/c #f (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, unless the filename ends with ".pdf", in which case it saves PDF. 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.

Example:

> (render-language nums)

procedure
(language->pict lang [#:nts nts]) → pict-convertible?
lang : compiled-lang?
nts : (or/c #f (listof (or/c string? symbol?)))
= (render-language-nts)

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

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

Example:

> (language->pict nums)

procedure
(render-reduction-relation rel
[ file
#:style style])
→ (if file void? pict-convertible?)
  rel : reduction-relation?
  file : (or/c #f 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, unless the filename ends with ".pdf", in which case it saves PDF. 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-> -->> >-- --< >>-- --<<

Examples:

> (define simplify-ae
    (reduction-relation
     nums
     (--> (+ AE ())
          AE)
     (--> (+ AE_1
             AE_2)
          (+ AE_2
             AE_1))))
> (render-reduction-relation
   simplify-ae)

procedure
(reduction-relation->pict r [#:style style]) → pict-convertible?
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.

Example:

> (reduction-relation->pict
   (reduction-relation
    nums
    (--> (+ (+ AE_1 AE_2) AE_3)
         (+ AE_1 (+ AE_2 AE_3)))))

syntax
(render-metafunction metafunction-name maybe-contract)
(render-metafunction metafunction-name filename maybe-contract)
syntax
(render-metafunctions metafunction-name ...
maybe-filename maybe-contract maybe-only-contract)

maybe-filename =
| #:file filename
| #:filename filename

maybe-contract? =
| #:contract? bool-expr

maybe-only-contract? =
| #:only-contract? bool-expr

Like render-reduction-relation but for metafunctions.

Similarly, render-metafunctions accepts multiple metafunctions and renders them together, lining up all of the clauses together.

There are a number of different styles that affect the overall rendering of the metafunction, controlled by metafunction-pict-style. Other parameters that affect rendering include linebreaks, sc-linebreaks, and metafunction-cases.

If the metafunctions have contracts, they are typeset as the first lines of the output unless the expression following #:contract? evaluates to #f (which is the default). If the expression following #:only-contract? is not #false (the default) then only the contract is typeset.

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

Examples:

> (define-metafunction nums
    add : K K -> K
    [(add K ·) K]
    [(add · K) K]
    [(add (0 K_1) (0 K_2)) (0 (add K_1 K_2))]
    [(add (1 K_1) (0 K_2)) (1 (add K_1 K_2))]
    [(add (0 K_1) (1 K_2)) (1 (add K_1 K_2))]
    [(add (1 K_1) (1 K_2)) (0 (add (1 ·) (add K_1 K_2)))])
> (render-metafunction add #:contract? #t)

Changed in version 1.3 of package redex-pict-lib: Added #:contract? keyword argument.
Changed in version 1.7: Added #:only-contract? keyword argument.

syntax
(metafunction->pict metafunction-name maybe-contract? maybe-only-contract?)

Produces a pict like render-metafunction, but without setting dc-for-text-size. It is suitable for use in Slideshow or other libraries that combine picts.

Example:

> (metafunction->pict add)

Changed in version 1.3 of package redex-pict-lib: Added #:contract? keyword argument.
Changed in version 1.7: Added #:only-contract? keyword argument.

syntax
(metafunctions->pict metafunction-name ...)

Like metafunction->pict, this produces a pict, but without setting dc-for-text-size and is suitable for use in Slideshow or other libraries that combine picts. Like render-metafunctions, it accepts multiple metafunctions and renders them together.

Example:

> (define-metafunction nums
    to-nat : K -> natural
    [(to-nat ·) 0]
    [(to-nat (0 K)) ,(* 2 (term (to-nat K)))]
    [(to-nat (1 K)) ,(+ 1 (* 2 (term (to-nat K))))])

Example:

> (metafunctions->pict add to-nat)

syntax
(render-relation relation-name)
(render-relation relation-name filename)

Like render-metafunction but for relations.

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

syntax
(render-judgment-form judgment-form-name)
(render-judgment-form judgment-form-name filename)

Like render-metafunction but for judgment forms. The judgment-form-cases parameter can be used to control which clauses are rendered.

Examples:

> (define-judgment-form nums
    #:mode (eq I I)
    #:contract (eq K K)

    [--------- eq-·
     (eq · ·)]

    [(eq K ·)
     ------------ eq-0-l
     (eq (0 K) ·)]

    [(eq · K)
     ------------ eq-0-r
     (eq · (0 K))]

    [(eq K_1 K_2)
     -------------------- eq-0
     (eq (0 K_1) (0 K_2))]

    [(eq K_1 K_2)
     -------------------- eq-1
     (eq (1 K_1) (1 K_2))])
> (render-judgment-form eq)
> (parameterize ([judgment-form-cases '("eq-·")])
    (render-judgment-form eq))

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

procedure
(derivation->pict language derivation) → pict-convertible?
language : compiled-lang?
derivation : derivation?

Produces a pict that looks like the derivation in show-derivations, except that it uses term->pict/pretty-write to draw the individual terms in the derivation.

Example:

> (derivation->pict nums (car (build-derivations (eq (0 (1 (0 ·))) (0 (1 ·))))))

Added in version 1.8 of package redex-pict-lib.

syntax
(relation->pict relation-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.

syntax
(judgment-form->pict judgment-form-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.

4.8.2 Customization🔗ℹ

parameter
(render-language-nts) → (or/c #f (listof symbol?))
(render-language-nts nts) → void?
nts : (or/c #f (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.

parameter
(non-terminal-gap-space) → real?
(non-terminal-gap-space gap-space) → void?
gap-space : real?

Controls the amount of vertical space between non-terminals in a typeset language.

Defaults to 0.

Added in version 1.1 of package redex-pict-lib.

parameter
(language-make-::=-pict) → (-> (listof symbol?) pict?)
(language-make-::=-pict make-::=) → void?
make-::= : (-> (listof symbol?) pict?)

Controls the pict used after the names of the non-terminals and before the first production in a grammar.

Defaults to

(λ (nt-names)
  ((current-text) " ::= "
                  (grammar-style)
                  (default-font-size)))

Added in version 1.17 of package redex-pict-lib.

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

A parameter that controls the rendering of extended languages. If the parameter value is #t, then a language constructed with define-extended-language is shown as if the language had been constructed directly with define-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).

Defaults to #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.

parameter
(extend-language-show-extended-order) → boolean?
(extend-language-show-extended-order ext-order?) → void?
ext-order? : boolean?

A parameter that controls the rendering of extended languages when extend-language-show-union has a true value. If this parameter’s value is #t, then productions are shown as ordered in the language extension instead of the order of the original, unextended language.

Defaults to #f.

Added in version 1.2 of package redex-pict-lib.

parameter
(render-reduction-relation-rules)
→
(or/c #f
      (listof (or/c symbol?
                    string?
                    exact-nonnegative-integer?)))
(render-reduction-relation-rules rules) → void?
   rules :
(or/c #f
      (listof (or/c symbol?
                    string?
                    exact-nonnegative-integer?)))

This parameter controls which rules in a reduction relation will be rendered. The strings and symbols match the names of the rules and the integers match the position of the rule in the original definition.

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

> (parameterize ([rule-pict-style 'horizontal])
(render-reduction-relation simplify-ae))
> (parameterize ([rule-pict-style 'vertical])
(render-reduction-relation simplify-ae))

The 'compact-vertical style moves the reduction arrow to the second line and uses less space between lines.

> (parameterize ([rule-pict-style 'compact-vertical])
(render-reduction-relation simplify-ae))

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.

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.

> (parameterize ([rule-pict-style 'horizontal-left-align])
(render-reduction-relation simplify-ae))

The 'horizontal-side-conditions-same-line is like 'horizontal, except that side-conditions are on the same lines as the rule, instead of on their own line below.

value
reduction-rule-style/c : contract?

A contract equivalent to

(or/c 'vertical
      'compact-vertical
      'vertical-overlapping-side-conditions
      'horizontal
      'horizontal-left-align
      'horizontal-side-conditions-same-line
      (-> (listof rule-pict-info?) pict-convertible?))

The symbols indicate various pre-defined styles. The procedure implements new styles; it is give the rule-pict-info? values, one for each clause in the reduction relation, and is expected to combine them into a single pict-convertible?

procedure
(rule-pict-info? x) → boolean?
x : any/c

A predicate that recognizes information about a rule for use in rendering the rule as a pict-convertible?.

procedure
(rule-pict-info-arrow rule-pict-info) → symbol?
rule-pict-info : rule-pict-info?

Extracts the arrow used for this rule. See also arrow->pict.

procedure
(rule-pict-info-lhs rule-pict-info) → pict-convertible?
rule-pict-info : rule-pict-info?

Extracts a pict for the left-hand side of this rule.

procedure
(rule-pict-info-rhs rule-pict-info) → pict-convertible?
rule-pict-info : rule-pict-info?

Extracts a pict for the right-hand side of this rule.

procedure
(rule-pict-info-label rule-pict-info) → (or/c symbol? #f)
rule-pict-info : rule-pict-info?

Returns the label used for this rule, unless there is no label for the rule or computed-label was used, in which case this returns #f.

procedure
(rule-pict-info-computed-label rule-pict-info)
→ (or/c pict-convertible? #f)
rule-pict-info : rule-pict-info?

Returns a pict for the typeset version of the label of this rule, when computed-label was used. Otherwise, returns #f.

procedure
(rule-pict-info->side-condition-pict rule-pict-info
[ max-width])
→ pict-convertible?
rule-pict-info : rule-pict-info?
max-width : real? = +inf.0

Builds a pict for the side-conditions and where clauses for rule-pict-info, attempting to keep the width under max-width.

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

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

This parameter controls the amount of extra space before the label on each rule, except in the 'vertical and 'vertical-overlapping-side-conditions modes, where it has no effect. Defaults to 0.

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

> (parameterize ([metafunction-pict-style 'left-right])
(render-metafunction add #:contract? #t))
> (parameterize ([metafunction-pict-style 'up-down])
(render-metafunction add #:contract? #t))

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

> (define-metafunction nums
    to-nat/sc : K -> natural
    [(to-nat/sc ·) 0]
    [(to-nat/sc (k K))
     ,(* 2 (term natural_K))
     (where k 0)
     (where natural_K (term (to-nat/sc K)))]
    [(to-nat/sc (k K))
     ,(+ 1 (* 2 (term natural_K)))
     (where k 1)
     (where natural_K (term (to-nat/sc K)))])
> (parameterize ([metafunction-pict-style 'left-right])
    (render-metafunction to-nat/sc #:contract? #t))
> (parameterize ([metafunction-pict-style 'left-right/vertical-side-conditions])
    (render-metafunction to-nat/sc #:contract? #t))
> (parameterize ([metafunction-pict-style 'left-right/beside-side-conditions])
    (render-metafunction to-nat/sc #:contract? #t))

Sometimes, some cases have side-conditions that are wider than other cases in such a way that they should break across lines differently in different cases. 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 would be otherwise—except that the rendered form is allowed to be up to the width specified by metafunction-fill-acceptable-width.

parameter
(metafunction-up/down-indent) → (>=/c 0)
(metafunction-up/down-indent indent) → void?
indent : (>=/c 0)

Controls the indentation of the right-hand side clauses when typesetting metafunctions in one of the up/down styles (see metafunction-pict-style).

The value is the amount to indent and it defaults to 0.

Added in version 1.2 of package redex-pict-lib.

parameter
(delimit-ellipsis-arguments?) → any/c
(delimit-ellipsis-arguments? delimit?) → void?
delimit? : any/c

This parameter controls the typesetting of metafunction definitions and applications. When it is non-#f (the default), commas precede ellipses that represent argument sequences; when it is #f no commas appear in those positions.

parameter
(white-square-bracket) → (-> boolean? pict-convertible?)
(white-square-bracket make-white-square-bracket) → void?
make-white-square-bracket : (-> boolean? pict-convertible?)

This parameter controls the typesetting of the brackets in metafunction definitions and applications. It is called to supply the two white bracket picts. If #t is supplied, the function should return the open white bracket (to be used at the left-hand side of an application) and if #f is supplied, the function should return the close white bracket.

It’s default value is default-white-square-bracket. See also homemade-white-square-bracket.

Added in version 1.1 of package redex-pict-lib.

procedure
(homemade-white-square-bracket open?) → pict-convertible?
open? : boolean?

This function implements the default way that older versions of Redex typeset whitebrackets. It uses two overlapping [ and ] chars with a little whitespace between them.

Added in version 1.1 of package redex-pict-lib.

procedure
(default-white-square-bracket open?) → pict-convertible?
open? : boolean?

This function returns picts built using 〚 and 〛 in the style default-style, using current-text and default-font-size.

If these result in picts that are more than 1/2 whitespace, then 1/3 of the whitespace is trimmed from sides (trimmed only from the left of the open and the right of the close).

Added in version 1.1 of package redex-pict-lib.

parameter
(linebreaks) → (or/c #f (listof boolean?))
(linebreaks breaks) → void?
breaks : (or/c #f (listof boolean?))

This parameter controls which cases in the metafunction are rendered on two lines and which are rendered on one.

If its value is a list, the length of the list must match the number of cases plus one if there is a contract that is rendered. Each boolean indicates if that case has a linebreak or not.

This parameter’s value influences the 'left/right styles only.

parameter
(sc-linebreaks) → (or/c #f (listof boolean?))
(sc-linebreaks breaks) → void?
breaks : (or/c #f (listof boolean?))

This parameter controls which cases in the metafunction have the side-conditions rendered on the next line instead of the same line as the right-hand side of the metafunction clause.

Its value must have the same shape as the value of the linebreaks parameter.

This parameter’s value influences the 'left-right/beside-side-conditions style only.

Added in version 1.6 of package redex-pict-lib.

parameter
(metafunction-cases)
→
(or/c #f (and/c (listof (or/c symbol?
                              string?
                              exact-nonnegative-integer?))
                pair?))
(metafunction-cases cases) → void?
   cases :
(or/c #f (and/c (listof (or/c symbol?
                              string?
                              exact-nonnegative-integer?))
                pair?))

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, then only the selected cases appear. The numbers indicate the cases counting from 0 and the strings and symbols indicate cases named with clause-name.

This parameter also controls how which clauses in judgment forms are rendered, but only in the case that judgment-form-cases is #f (and in that case, only the numbers are used).

parameter
(judgment-form-cases)
→
(or/c #f
      (non-empty-listof (or/c symbol?
                              string?
                              exact-nonnegative-integer?)))
(judgment-form-cases cases) → void?
   cases :
(or/c #f
      (non-empty-listof (or/c symbol?
                              string?
                              exact-nonnegative-integer?)))

Controls which clauses in a judgment form are rendered. If it is #f (the default), then all of them are rendered. If it is a list, then only the selected clauses appear (numbers count from 0, and strings and symbols correspond to the labels in a judgment form).

parameter
(judgment-form-show-rule-names) → boolean?
(judgment-form-show-rule-names show-rule-names?) → void?
show-rule-names? : boolean?

Determines if the names of the cases are shown beside the rules in a rendered judgment form. Defaults to #t.

Added in version 1.5 of package redex-pict-lib.

parameter
(label-style) → text-style/c
(label-style style) → void?
  style : text-style/c
parameter
(grammar-style) → text-style/c
(grammar-style style) → void?
  style : text-style/c
parameter
(paren-style) → text-style/c
(paren-style style) → void?
  style : text-style/c
parameter
(literal-style) → text-style/c
(literal-style style) → void?
  style : text-style/c
parameter
(metafunction-style) → text-style/c
(metafunction-style style) → void?
  style : text-style/c
parameter
(non-terminal-style) → text-style/c
(non-terminal-style style) → void?
  style : text-style/c
parameter
(non-terminal-subscript-style) → text-style/c
(non-terminal-subscript-style style) → void?
  style : text-style/c
parameter
(non-terminal-superscript-style) → text-style/c
(non-terminal-superscript-style style) → void?
  style : text-style/c
parameter
(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 a style can be is the symbol 'roman, 'swiss, or 'modern, which corresponds to serif, sans-serif, and monospaced font, respectively. (A style can encode additional information, too, such as boldface or italic configuration.)

The label-style parameter is used for reduction-rule labels. The literal-style parameter is used for names that aren’t non-terminals that appear in patterns. The metafunction-style parameter is used for the names of metafunctions. The paren-style parameter is used for parentheses (including “[”, “]”, “{”, and “}”, as well as “(” and “)”) and for keywords, but it is not used for the square brackets of in-hole decompositions, which use the default-style parameter. The grammar-style parameter is used for the “::=” and “|” in grammars.

The non-terminal-style parameter 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 only exception to this is when the subscript section consists only of unicode prime characters (′), in which case the non-terminal-style is used instead of the non-terminal-subscript-style.

The default-style parameter is used for parenthesis, the dot in dotted lists, spaces, the “where” and “fresh” in side-conditions, and other places where the other parameters aren’t used.

Changed in version 1.4 of package redex-pict-lib: Use paren-style for keywords.

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

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

parameter
(reduction-relation-rule-separation) → (parameter/c real?)
(reduction-relation-rule-separation sep) → void?
sep : (parameter/c real?)

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

Horizontal and compact-vertical renderings add this parameter’s amount to (reduction-relation-rule-extra-separation) to compute the full separation.

parameter
(reduction-relation-rule-extra-separation)
→ (parameter/c real?)
(reduction-relation-rule-extra-separation sep) → void?
sep : (parameter/c real?)

Controls the amount of space between rule in a reduction relation for a horizontal or compact-vertical rendering, in addition to (reduction-relation-rule-separation). Defaults to 4.

Added in version 1.7 of package redex-pict-lib.

parameter
(reduction-relation-rule-line-separation)
→ (parameter/c real?)
(reduction-relation-rule-line-separation sep) → void?
sep : (parameter/c real?)

Controls the amount of space between lines within a reduction-relation rule. Defaults to 2.

Added in version 1.7 of package redex-pict-lib.

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

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

A parameter whose value is a function to be called whenever Redex typesets some part of a grammar, reduction relation, or metafunction. It defaults to the pict library’s text function.

procedure
(arrow->pict arrow) → pict-convertible?
arrow : symbol?

Returns the pict corresponding to arrow.

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

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.

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

A parameter whose value is a function to be used when typesetting metafunctions to determine how to create the ⟦⟧ characters with homemade-white-square-bracket, which combines two [ characters or two ] characters together.

The procedure accepts a string that is either "[" or "]", and it 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.

parameter
(horizontal-bar-spacing)
→ (parameter/c exact-nonnegative-integer?)
(horizontal-bar-spacing space) → void?
space : (parameter/c exact-nonnegative-integer?)

Controls the amount of space around the horizontal bar when rendering a relation (that was created by define-relation). Defaults to 4.

parameter
(metafunction-gap-space) → real?
(metafunction-gap-space gap-space) → void?
gap-space : real?

Controls the amount of vertical space between different metafunctions rendered together with render-metafunctions.

Defaults to 2.

Added in version 1.7 of package redex-pict-lib.

parameter
(metafunction-rule-gap-space) → real?
(metafunction-rule-gap-space gap-space) → void?
gap-space : real?

Controls the amount of vertical space between different rules within a metafunction as rendered with render-metafunction or render-metafunctions.

Defaults to 2.

Added in version 1.7 of package redex-pict-lib.

parameter
(metafunction-line-gap-space) → real?
(metafunction-line-gap-space gap-space) → void?
gap-space : real?

Controls the amount of vertical space between different lines within a metafunction rule as rendered with render-metafunction or render-metafunctions.

Defaults to 2.

Added in version 1.7 of package redex-pict-lib.

parameter
(metafunction-fill-acceptable-width) → real?
(metafunction-fill-acceptable-width width) → void?
width : real?

Determines a width that is used for putting metafunction side conditions on a single line when using a style like 'left-right/compact-side-conditions (as the value of metafunction-pict-style). The default value is 0, which means that side conditions are joined on a line only when joining them does not change the overall width of the rendered metafunction. A larger value allows side conditions to be joined when they would make the rendered form wider, as long as the overall width of the metafunction does not exceed the specified value.

For example, if the side conditions of a particular rule in a metafunction are all shorter than the rule itself, metafunction-fill-acceptable-width has no effect. In contrast, if the rule itself is shorter than the side conditions and narrower than the space available to render (in a document for printing, for example), setting metafunction-fill-acceptable-width can help. Setting it to the available width causes rendering to use the available horizontal space for joining side conditions.

Examples:

> (define-metafunction nums
    [(f K_1)
     ·
     (where (0 K_2) K_1)
     (where (1 K_3) K_2)
     (where (0 K_4) K_3)
     (where (1 K_5) K_4)
     (where (1 ·) K_5)]
    [(f K) (0 ·)])
> (parameterize ([metafunction-pict-style 'left-right/compact-side-conditions])
    (render-metafunction f))
> (parameterize ([metafunction-pict-style 'left-right/compact-side-conditions]
                 [metafunction-fill-acceptable-width 300])
    (render-metafunction f))
> (parameterize ([metafunction-pict-style 'left-right/compact-side-conditions]
                 [metafunction-fill-acceptable-width 400])
    (render-metafunction f))

Added in version 1.11 of package redex-pict-lib.

parameter
(metafunction-combine-contract-and-rules)
→ (pict-convertible? pict-convertible? . -> . pict-convertible?)
(metafunction-combine-contract-and-rules combine) → void?
combine : (pict-convertible? pict-convertible? . -> . pict-convertible?)

Controls the combination of a contract with the rules of a metafunction when contract rendering is enabled. The first argument to the combining function is a pict for the contract, and the second argument is a pict for the rules.

The default combining function uses vl-append with a separation of (metafunction-rule-gap-space).

Added in version 1.7 of package redex-pict-lib.

parameter
(relation-clause-combine)
→
(parameter/c
(-> (listof (listof pict-convertible?))
     pict-convertible?
     (or/c string? #f)
     pict-convertible?))
(relation-clause-combine combine) → void?
   combine :
(parameter/c
(-> (listof (listof pict-convertible?))
     pict-convertible?
     (or/c string? #f)
     pict-convertible?))

Controls the construction of a particular clause of a reduction relation or judgment form. The first argument are the premises (each inner list of premises are on the same line as each other), the second argument is the conclusion and the third argument is the name of the rule (if the rule is named).

The default value is default-relation-clause-combine.

Added in version 1.9 of package redex-pict-lib.

procedure
(default-relation-clause-combine premises
conclusion
rule-name)
→ pict-convertible?
  premises : (listof (listof pict-convertible?))
  conclusion : pict-convertible?
  rule-name : (or/c string? #f)

Builds a pict for the premises as

(apply vc-append 4
(for/list ([premises (in-list premises)])
(apply hbl-append 20 premises)))

and then adds a line below it and the conclusion pict below that. If rule-name is not #f, then it adds the name next to the bar.

Added in version 1.9 of package redex-pict-lib.

parameter
(relation-clauses-combine)
→ (parameter/c (-> (listof pict-convertible?) pict-convertible?))
(relation-clauses-combine combine) → void?
combine : (parameter/c (-> (listof pict-convertible?) pict-convertible?))

The combine function is called with the list of picts that are obtained by rendering a relation; it should put them together into a single pict. It defaults to (λ (l) (apply vc-append 20 l))

parameter
(metafunction-arrow-pict)
→ (parameter/c (-> pict-convertible?))
(metafunction-arrow-pict make-arrow) → void?
make-arrow : (parameter/c (-> pict-convertible?))

Specifies the pict to use for the arrow when typesetting a metafunction contract.

parameter
(where-make-prefix-pict)
→ (parameter/c (-> pict-convertible?))
(where-make-prefix-pict make-prefix) → void?
make-prefix : (parameter/c (-> pict-convertible?))

The make-prefix function is called with no arguments to generate a pict that prefixes where clauses. It defaults to a function that produces a pict for “where” surrounded by spaces using the default style.

parameter
(where-combine)
→ (parameter/c (-> pict-convertible? pict-convertible? pict-convertible?))
(where-combine combine) → void?
combine : (parameter/c (-> pict-convertible? pict-convertible? pict-convertible?))

The combine function is called with picts for the left and right side of a where clause, and it should put them together into a single pict. It defaults to (λ (l r) (hbl-append l =-pict r)), where =-pict is an equal sign surrounded by spaces using the default style.

parameter
(current-render-pict-adjust)
→ (pict-convertible? symbol? . -> . pict-convertible?)
(current-render-pict-adjust adjust) → void?
adjust : (pict-convertible? symbol? . -> . pict-convertible?)

A parameter whose value is a function to adjusts picts generated as various parts of a rendering. The symbol that is provided to the function indicates the role of the pict. A pict-adjusting function might be installed to ensure consistent spacing among multiple lines in a metafunction’s rendering, for example, or to adjust the color of side-condition terms.

The set of roles is meant to be extensible, and the currently provided role symbols are as follows:

'lw-line — a line with a render term (including any term that fits on a single line)
'language-line — a line on the right-hand side of a production in a language grammar.
'language-production — a production (possibly multiple lines) within a language grammar.
'side-condition-line — a line within a side condition for a reduction-relation rule or metafunction rule
'side-condition — a single side condition with a group of side conditions for a reduction-relation rule or a metafunction rule
'side-conditions — a group of side conditions for a reduction-relation rule or a metafunction rule including the “where” prefix added by (where-make-prefix-pict)
'reduction-relation-line — a single line within a reduction-relation rule
'reduction-relation-rule — a single rule within a reduction relation
'metafunction-contract — a contract for a metafunction
'metafunction-line — a line within a metafunction rule
'metafunction-rule — a single rule within a metafunction
'metafunctions-metafunction — a single metafunction within a group of metafunctions that are rendered together

Added in version 1.7 of package redex-pict-lib.

4.8.3 Removing the Pink Background🔗ℹ

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 an alternative typesetting 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:

syntax
(with-unquote-rewriter proc expression)

Installs proc as the current unquote rewriter and evaluates expression. If that expression computes any picts, the unquote rewriter specified is used to remap them.

The proc must match the contract (-> lw? lw?). Its result should be the rewritten version version of the input.

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

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 whenever the symbol appears in a pattern.

Examples:

> (define-language lam-lang
    (e (lambda (x) e)))
> (with-atomic-rewriter
   'lambda
   "λ"
   (render-term lam-lang (term (lambda (x) e))))

syntax
(with-atomic-rewriters ([name-symbol string-or-thunk-returning-pict] ...)
expression)

Shorthand for nested with-atomic-rewriter expressions.

Added in version 1.4 of package redex-pict-lib.

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

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-convertible?)), 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 text just below the description of lw for a 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.

One useful way to take advantage of with-compound-rewriters is to return a list that begins and ends with "" (the empty string). In that situation, any extra logical space that would have been just outside the sequence is replaced with an lw that does not draw anything at all.

Example:

> (with-compound-rewriter
   'eq
   (λ (lws)
     (define lhs (list-ref lws 2))
     (define rhs (list-ref lws 3))
     (list "" lhs " = " rhs ""))
   (render-judgment-form eq))

syntax
(with-compound-rewriters ([name-symbol proc] ...)
expression)

Shorthand for nested with-compound-rewriter expressions.

4.8.4 LWs🔗ℹ

struct
(struct lw ( e
line
line-span
column
column-span
unq?
metafunction?)
    #:extra-constructor-name make-lw
    #:mutable)
   e :
(or/c string?
      symbol?
      pict-convertible?
      (listof (or/c (symbols 'spring) lw?)))
  line : exact-positive-integer?
  line-span : exact-positive-integer?
  column : exact-positive-integer?
  column-span : exact-positive-integer?
  unq? : boolean?
  metafunction? : boolean?

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.

The values of the unq? and metafunction? fields, respectively, indicate whether the lw represents an unquoted expression or a metafunction application. See to-lw for the meanings of the other fields.

procedure
(build-lw e line line-span column column-span) → lw?
   e :
(or/c string?
      symbol?
      pict-convertible?
      (listof (or/c 'spring lw?)))
  line : exact-positive-integer?
  line-span : exact-positive-integer?
  column : exact-positive-integer?
  column-span : exact-positive-integer?

Like make-lw but specialized for constructing lws that do not represent unquoted expressions or metafunction applications.

syntax
(to-lw arg)

Turns arg 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 sub-expression 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 absence 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 (i.e., 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.

procedure
(to-lw/stx stx) → lw?
stx : syntax?

A procedure variant of to-lw; it accepts a syntax object and returns the corresponding lw structs. It only uses the location information in the syntax object, so metafunctions will not be rendered properly.

procedure
(render-lw language/nts lw) → pict-convertible?
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.

procedure
(lw->pict language/ntw lw) → pict-convertible?
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 function does not set the dc-for-text-size parameter. See also render-lw.

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

procedure
(fill-between stuff lw-before lw-after) → lw?
  stuff : (or/c pict-convertible? string? symbol?)
  lw-before : lw?
  lw-after : lw?

Builds a new lw whose content is stuff and whose location information makes it occupy all of the space between lw-before and lw-after.

If lw-before and lw-after are not on the same line, fill-between raises an error.

4.8.5 Macros and Typesetting🔗ℹ

When you have a macro that abstracts over variations in Redex programs, then typesetting is unlikely to work without some help from your macros.

To see the issue, consider this macro abstraction over a Redex grammar:

> (define-syntax-rule
    (def-my-lang L prim ...)
    (define-language L
      (e ::=
         (λ (x) e)
         (e e)
         prim ...
         x)
      (x ::= variable-not-otherwise-mentioned)))
> (def-my-lang L + - *)
> (render-language L)
eject: lines going backwards (current-line 2 line 1 atom
#<pict> tokens (#(struct:string-token 0 1 "*" swiss)
#(struct:pict-token 1 0 #<pict>) #(struct:string-token 0 1
"-" swiss) #(struct:pict-token 1 0 #<pict>)
#(struct:string-token 0 1 "+" swiss) #(struct:pict-token 0 0
#<pict>) #(struct:spacer-token 0 0)))

Redex thinks that the grammar is going “backwards” because of the way macro expansion synthesizes source locations. In particular, in the result of the macro expansion, the third production for e appears to come later in the file than the fourth production and this confuses Redex, making it unable to typeset this language.

One simple, not-very-general work-around is to just avoid typesetting the parts that come from the macro arguments. For example if you move the primitives into their own non-terminal and then just avoid typesetting that, Redex can cope:

(define-syntax-rule
  (def-my-lang/separate-prims L prim ...)
  (define-language L
    (e ::=
       (λ (x) e)
       (e e)
       prims
       x)
    (prims ::= prim ...)
    (x ::= variable-not-otherwise-mentioned)))

(def-my-lang/separate-prims L + - *)

> (render-language L #:nts '(e x))

You can also, however, exploit Racket’s macro system to rewrite the source locations in a way that tells Redex where the macro-introduced parts of the language are supposed to be, and then typesetting will work normally. For example, here is one way to do this with the original language:

(define-syntax (def-my-lang stx)
  (syntax-case stx ()
    [(_ L a ...)
     (let ()
       (define template
         #'(define-language L
             (e (λ (x) e)
                (e e)
                HERE
                x)
             (x variable-not-otherwise-mentioned)))
       (car
        (let loop ([stx template])
          (syntax-case stx (HERE)
            [HERE
             (let loop ([as (syntax->list #'(a ...))]
                        [pos (syntax-position stx)]
                        [col (syntax-column stx)])
               (cond
                 [(null? as) '()]
                 [else
                  (define a (car as))
                  (define span
                    (string-length
                     (symbol->string (syntax-e a))))
                  (define srcloc
                    (vector (syntax-source stx)
                            (syntax-line stx)
                            col
                            pos
                            span))
                  (cons
                   (datum->syntax a
                                  (syntax-e a)
                                  srcloc
                                  a)
                   (loop (cdr as)
                         (+ pos span 1)
                         (+ col span 1)))]))]
            [(a ...)
             (list
              (datum->syntax
               stx
               (apply append (map loop (syntax->list #'(a ...))))
               stx
               stx))]
            [a
             (list stx)]))))]))

> (def-my-lang L + - *)

> (render-language L)

1	Amb: A Redex Tutorial
2	Long Tutorial
3	Extended Exercises
4	The Redex Reference
5	Automated Testing Benchmark
	Bibliography
	Index

4.1	Patterns
4.2	Terms
4.3	Languages
4.4	Reduction Relations
4.5	Other Relations
4.6	Testing
4.7	GUI
4.8	Typesetting

4.8.1	Picts, PDF, & Post Script
4.8.2	Customization
4.8.3	Removing the Pink Background
4.8.4	LWs
4.8.5	Macros and Typesetting