simple, low level rewriters for PLT Redex typesetting
Racket
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
LICENSE
README.md
info.rkt
main.rkt

README.md

typeset-rewriter

Simple, low level rewriters for PLT Redex typesetting.

See the PLT Redex docs on typesetting for more details. These macros are just a thin layer on top of these mechanics.

Provides the following syntax:

rw-lambda

Allows for simple compound-rewriter definitions (refer to redex docs for specific requirements on what a compound rewriter is). Named to highlight similarity to Racket's own match-lambda. Basically, a compound-rewriter for a symbol 'name' will be called for redex terms being typeset that look like (name any ...)

The rw-lambda macro builds rewriters from quasiquote like patterns of the form (rw-lambda [`(name pats ...) => output] ...)

Things not unquoted are matched as literal symbols in the redex term, while things unquoted are treated like standard match patterns.

Example usage:

(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 ")")))]))

This defines a rewriter with two cases, which together allow this rewriter to successfully rewrite PLT Redex terms of the form (lambda ([any : any]) any any ...). Our particular definition removes the parens from around the lambda and adds a begin if there is more than one body expression. In other words, (lambda ([x : t]) e) is typeset to look like λx:t.e, and (lambda ([x : t]) e e) is typeset to look like λx:t.(begin e e).

Note that the sub-terms we are not altering but merely rearranging (e.g. t) will have any other applicablerewriters applied to them as well. So if we had an atomic rewriter converting t to τ, that would still occur, etc...

For more info on compound rewriters, see the redex docs. They are supposed to be functions with signature (listof lw) -> (listof (or/c lw? string? pict?)) which is "rewritten appropriately."

with-atomic-rws

Like with-compound-rewriters for atomic rewriters.

Example usage:

(with-atomic-rws (['lambda "λ"] ['-> ""]) 
 body-expr)

with-rws

Allows for atomic and/or compound rewriters to be specified.

Example usage:

(with-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])
 body-expr)

define-rw-context

Defines a macro to reuse sets of rewriters.

Example usage:

(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]))
              
(with-stlc-rws render-expr1)
(with-stlc-rws render-expr2)