PLT Redex is a great tool for tinkering with and examining various aspects of programming languages. Although it can be used to programmatically generate mathematical figures for papers and the like (awesome!), the actual machinery for doing so is a little lower level than you want 99% of the time.
To alleviate this, I developed a package (typeset-rewriter) with a few simple tools that make it much easier to build the rewriters redex natively supports.
To demonstrate, let’s take a simple redex model and look at typesetting it.
First we define the language, like the simply typed lambda calculus:
1 2 3 4 5 6 7 8 9 10
Note: In this definition we could have used unicode characters directly (and then typesetting will use those same characters) but we shouldn’t feel obligated to. We can throw in all the greek we want when typesetting.
And maybe we have some judgments and metafunctions:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(define-judgment-form STLC #:mode (typeof I I O) #:contract (typeof Env exp ty) [----------------- "T-Val" (typeof Env v (val-type v))] [(where ty (lookup Env x)) ---------- "T-Var" (typeof Env x ty)] ....) (define-metafunction STLC val-type : v -> ty ....) (define-metafunction STLC extend : Env x ty -> Env ....) (define-metafunction STLC lookup : Env x -> ty ....)
"…" in this case is not special syntax, but just to stand in for the obvious definitions
If we were to try and typeset these definitions now, we probably wouldn’t be too happy with the result:
(render-judgment-form typeof) (with-rws (render-language STLC #:nts '(v exp ty Env)))
Sure, the figures will have the expected shape overall, but maybe we wanted the more traditional
Γ for type environments instead of
Env, and we probably want our typing judgments to look like
Γ ⊢ e : τ instead of the default typesetting
typeof〚Γ, e, τ〛.
In addition to a few simple knobs and switches, PLT Redex model typesetting can be enhanced with two forms of rewriters.
Atomic rewriters will get us part of the way there. They allow us to rewrite symbols with provided strings (or thunks returning picts), and things like subscripts are preserved just the way we would hope:
1 2 3 4 5
(with-atomic-rewriter 'Env "Γ" (with-atomic-rewriter 't 'τ (render-language STLC #:nts '(v exp ty Env))))
I’m not sure why there isn’t a plural version of this form… so I went ahead and defined one in the
1 2 3
But if we want to get our typing judgment to look correct, we’re going to need just a little more muscle.
The hooks for compound rewriters are pretty powerful. They allow us to transform arbitrary redex terms by letting us specify compound rewriters to be applied to parenthesized terms with a particular symbol at the head. So if we install a rewriter
lambda-rw before typesetting
any term of the form
(lambda any ...) will be passed to our
This gives us great power… but if we look at the signature for these rewriters we see theirs a subtle catch:
We have to work with lists of the
lw structs that redex uses to typeset code if we want to tweak how our figures will look.
To make this more palatable, I built a
match-lambda-like macro that abstracts away all the struct details of our redex terms and lets us use the much simpler
unquote syntax we’re used to working with in Racket pattern matching.
With these tools, we can define the following rewriters and rewriting context:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
(require typeset-rewriter) (define lambda-rw (rw-lambda [`(lambda ([,x : ,t]) ,body) => (list "λ" x ":" t ". " body)] [`(lambda ([,x : ,t]) ,body ,bodies ...) => (list* "λ" x ":" t ". (begin " body (append bodies (list ")")))])) (define typeof-rw (rw-lambda [`(typeof ,Γ ,e ,t) => (list "" Γ " ⊢ " e " : " t)])) (define extend-rw (rw-lambda [`(extend ,Γ ,x ,t) => (list "" Γ ", " x ":" t)])) (define lookup-rw (rw-lambda [`(lookup ,Γ ,x) => (list "" Γ "(" x ")")])) (define val-type-rw (rw-lambda [`(val-type ,v) => (list "type-of(" v ")")])) (define-rw-context with-stlc-rws #:atomic (['Env "Γ"] ['exp "e"] ['ty "τ"] ['-> "→"] ['integer "n"]) #:compound (['lambda lambda-rw] ['typeof typeof-rw] ['extend extend-rw] ['lookup lookup-rw] ['val-type val-type-rw]))
This allows us to produce figures looking just the way we want:
(with-stlc-rws (render-language STLC #:nts '(v exp ty Env))) (with-stlc-rws (render-judgment-form typeof))
You may have noticed I used a more complex definition for
lambda-rw than seemed necessary:
1 2 3 4 5 6
This was just to show that the
rw macro is merely a thin layer of syntax that expands into Racket’s powerful
match form. Anything following an
unquote (e.g. a
,) in the
quasiquote pattern can be an arbitrary match pattern, and things like elipses—since they are supported by
match—are supported as well.
Installing and using
From the command line, enter
raco pkg install typeset-rewriter
Or from within DrRacket, open the Package Manager (
File>Package Manager on Mac), enter
typeset-rewriter in the
Package Source field and install.
After installation, simply add
typeset-rewriter to the list of required packages in your module. Ex