4.8 Typesetting
(require redex/pict) | package: redex-pict-lib |
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)
> (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 ·))))))
> (let ([x (term (+ (1 (1 (1 ·))) (1 (0 (0 ·)))))]) (render-term nums x))
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)
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.
> (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)
If filename is provided, the pict is saved as a pdf to that file.
> (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)
> (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)
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.
> (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)
This function is primarily designed to be used with Slideshow or with other tools that combine picts together.
> (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)
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-> -->> >-- --< >>-- --<<
> (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)
This function is primarily designed to be used with Slideshow or with other tools that combine picts together.
> (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
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.
> (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?)
> (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 ...)
> (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))))])
> (metafunctions->pict add to-nat)
syntax
(render-relation relation-name)
(render-relation relation-name filename)
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)
> (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?
> (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)
syntax
(judgment-form->pict judgment-form-name)
4.8.2 Customization
parameter
(render-language-nts) → (or/c #f (listof symbol?))
(render-language-nts nts) → void? nts : (or/c #f (listof symbol?))
See also language-nts.
parameter
(non-terminal-gap-space gap-space) → void? gap-space : real?
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?)
(λ (nt-names) ((current-text) " ::= " (grammar-style) (default-font-size)))
Added in version 1.17 of package redex-pict-lib.
parameter
(extend-language-show-union show?) → void? show? : boolean?
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 ext-order?) → void? ext-order? : boolean?
Defaults to #f.
Added in version 1.2 of package redex-pict-lib.
parameter
→
(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?)))
parameter
(rule-pict-style style) → void? style : reduction-rule-style/c
> (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
(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
procedure
(rule-pict-info-arrow rule-pict-info) → symbol?
rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-lhs rule-pict-info) → pict-convertible?
rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-rhs rule-pict-info) → pict-convertible?
rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-label rule-pict-info) → (or/c symbol? #f)
rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-computed-label rule-pict-info)
→ (or/c pict-convertible? #f) rule-pict-info : rule-pict-info?
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
parameter
(arrow-space space) → void? space : natural-number/c
parameter
(label-space space) → void? space : natural-number/c
parameter
→
(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)
> (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—
parameter
(metafunction-up/down-indent) → (>=/c 0)
(metafunction-up/down-indent indent) → void? indent : (>=/c 0)
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? delimit?) → void? delimit? : any/c
parameter
(white-square-bracket make-white-square-bracket) → void? make-white-square-bracket : (-> boolean? pict-convertible?)
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
open? : boolean?
Added in version 1.1 of package redex-pict-lib.
procedure
open? : boolean?
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?))
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?))
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
→
(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?))
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
→
(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?)))
parameter
(judgment-form-show-rule-names show-rule-names?) → void? show-rule-names? : boolean?
Added in version 1.5 of package redex-pict-lib.
parameter
(label-style style) → void? style : text-style/c
parameter
(grammar-style style) → void? style : text-style/c
parameter
(paren-style style) → void? style : text-style/c
parameter
(literal-style style) → void? style : text-style/c
parameter
(metafunction-style style) → void? style : text-style/c
parameter
(non-terminal-style style) → void? style : text-style/c
parameter
(non-terminal-subscript-style style) → void? style : text-style/c
parameter
(non-terminal-superscript-style style) → void? style : text-style/c
parameter
(default-style style) → void? style : text-style/c
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?)
parameter
(reduction-relation-rule-separation sep) → void? sep : (parameter/c real?)
Horizontal and compact-vertical renderings add this parameter’s amount to (reduction-relation-rule-extra-separation) to compute the full separation.
parameter
→ (parameter/c real?) (reduction-relation-rule-extra-separation sep) → void? sep : (parameter/c real?)
Added in version 1.7 of package redex-pict-lib.
parameter
→ (parameter/c real?) (reduction-relation-rule-line-separation sep) → void? sep : (parameter/c real?)
Added in version 1.7 of package redex-pict-lib.
parameter
(curly-quotes-for-strings on?) → void? on? : boolean?
Defaults to #t.
parameter
→ (-> string? text-style/c number? pict-convertible?) (current-text proc) → void? proc : (-> string? text-style/c number? pict-convertible?)
procedure
(arrow->pict arrow) → pict-convertible?
arrow : symbol?
procedure
(set-arrow-pict! arrow proc) → void?
arrow : symbol? proc : (-> pict-convertible?)
parameter
→ (-> string? number? (values number? number? number? number?)) (white-bracket-sizing proc) → void? proc : (-> string? number? (values number? number? number? number?))
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).
(λ (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
→ (parameter/c exact-nonnegative-integer?) (horizontal-bar-spacing space) → void? space : (parameter/c exact-nonnegative-integer?)
parameter
(metafunction-gap-space gap-space) → void? gap-space : real?
Defaults to 2.
Added in version 1.7 of package redex-pict-lib.
parameter
(metafunction-rule-gap-space gap-space) → void? gap-space : real?
Defaults to 2.
Added in version 1.7 of package redex-pict-lib.
parameter
(metafunction-line-gap-space gap-space) → void? gap-space : real?
Defaults to 2.
Added in version 1.7 of package redex-pict-lib.
parameter
(metafunction-fill-acceptable-width width) → void? width : real?
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.
> (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
→ (pict-convertible? pict-convertible? . -> . pict-convertible?) (metafunction-combine-contract-and-rules combine) → void? combine : (pict-convertible? pict-convertible? . -> . pict-convertible?)
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
→
(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?))
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)
Added in version 1.9 of package redex-pict-lib.
parameter
→ (parameter/c (-> (listof pict-convertible?) pict-convertible?)) (relation-clauses-combine combine) → void? combine : (parameter/c (-> (listof pict-convertible?) pict-convertible?))
parameter
→ (parameter/c (-> pict-convertible?)) (metafunction-arrow-pict make-arrow) → void? make-arrow : (parameter/c (-> pict-convertible?))
parameter
→ (parameter/c (-> pict-convertible?)) (where-make-prefix-pict make-prefix) → void? make-prefix : (parameter/c (-> pict-convertible?))
parameter
→ (parameter/c (-> pict-convertible? pict-convertible? pict-convertible?)) (where-combine combine) → void? combine : (parameter/c (-> pict-convertible? pict-convertible? pict-convertible?))
parameter
→ (pict-convertible? symbol? . -> . pict-convertible?) (current-render-pict-adjust adjust) → void? adjust : (pict-convertible? symbol? . -> . pict-convertible?)
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)
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)
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.
> (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)
Added in version 1.4 of package redex-pict-lib.
syntax
(with-compound-rewriter name-symbol proc 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.
> (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)
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 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
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?
syntax
(to-lw arg)
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
(render-lw language/nts lw) → pict-convertible?
language/nts : (or/c (listof symbol?) compiled-lang?) lw : lw?
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?
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?
procedure
(fill-between stuff lw-before lw-after) → lw?
stuff : (or/c pict-convertible? string? symbol?) lw-before : lw? lw-after : lw?
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.
> (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)))
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)))
> (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)]))))]))
> (render-language L)