[racket] Typesetting with subscripts in Redex

At Mon, 10 Sep 2012 00:25:29 +0200, Nada Amin wrote:
> Hello,
> 
> Redex has been really useful in exploring examples in a calculus we're
> developing. Now, I would like to use Redex's typesetting facility to
> render these examples (to avoid introducing bugs when translating them
> to TeX). For this, it would be great if I could specify that something
> should be rendered as a subscript.
> 
> Here is a dummy example just to illustrate what I mean:
> #lang racket
> (require redex)
> 
> (define-language dummy
>   (e (p natural) (n natural)))
> 
> (define (dummy-rewriters thunk)
>   (with-compound-rewriters
>    (['p (lambda (lws) (list (list-ref lws 2)))]
>     ['n (lambda (lws) (list "-" (list-ref lws 2)))])
>    (thunk)))
> 
> > (dummy-rewriters (lambda () (render-term dummy (p 1))))
> 1
> > (dummy-rewriters (lambda () (render-term dummy (n 1))))
> -1
> 
> Let's say, I'd like to render (n 1) as the equivalent of TeX $1_n$. Is
> that possible?

I think you must drop down to the pict-construction layer to do that.
The example below uses `text' with the 'subscript option.

Getting the line, column, and span for a rewriter result can be tricky.
Usually, you want the result of a rewriter to have the same start and
span as the input. I think I got that part right, below, too.

> Incidentally, is there a better way to re-use compound
> rewriters?

No, I usually write a function like your `dummy-rewriters'.

------------------------------------------------------------

#lang racket
(require redex
         slideshow/pict)

(define-language dummy
  (e (p natural) (n natural)))

(define (collapse a b)
  ;; Build a zero-width element that takes the same columns
  ;; as a through b
  (build-lw "" 
            (lw-line a) (+ (- (lw-line b) (lw-line a))
                           (lw-line-span b))
            (lw-column a) (+ (- (lw-column b) (lw-column a))
                             (lw-column-span b))))

(define (dummy-rewriters thunk)
  (with-compound-rewriters
   (['n (lambda (lws) 
          (list (collapse (first lws) (list-ref lws 1))
                (list-ref lws 2)
                (text (symbol->string (lw-e (list-ref lws 1)))
                      `(subscript . ,(default-style))
                      (default-font-size))                          
                (collapse (list-ref lws 3) (last lws))))])
   (thunk)))

(dummy-rewriters (lambda () (render-term dummy (n 1))))