[racket] does render-term or term->pict work in a metafunction?

From: Asumu Takikawa (asumu at ccs.neu.edu)
Date: Wed Apr 18 23:08:05 EDT 2012

Stephen directed me to this mailing list post from a while back about
Redex term rendering since I was having the same issue.

On 2012-04-18 18:33:56 -0400, Stephen Chang wrote:
> Something like:
> 
> (define-metafunction L
>  [(x->pict x) ,(lw->pict (language-nts L) (to-lw x))])
> 
> still gives a pict of x for (term (x->pict y)).
> 
> 
> To get what I want, I figured out I can do:
> 
> (define-metafunction L
>  [(x->pict x) ,(text (symbol->string (term x)))])

Similar to what Stephen wanted to do, I wanted to write a function that
will apply a reduction relation and then create a composed pict out of
the reduction steps. Something like this:

  ;; term -> pict
  ;; renders the reductions steps of a term t
  (define (render-steps t)
    ;; term -> (list term)
    (define (reduction-steps t)
      (define results (apply-reduction-relation ISWIM-red t))
      (if (null? results)
          '()
          (cons (car results) (reduction-steps (car results)))))

    (define picts (map render (λ (t) (render-term ISWIM t #f))
                              (cons t (reduction-steps t))))
    (apply vl-append picts))

Unfortunately, this doesn't work. Since `render-term` is a macro, this
will render each pict as just "t" rather than using the value bound to
`t`.

I ended up having to do something like this (at Tony Garnock-Jones'
suggestion):

  ;; term -> pict
  ;; renders the reductions steps of a term t
  (define (render-steps t)
    ;; term -> (list term)
    (define (reduction-steps t)
      ...) ; same as above
  
    ;; term -> pict
    (define (render t)
      (eval (append '(render-term ISWIM) (list t) (list #f))
            (namespace-anchor->namespace iswim-anchor)))
  
    (define picts (map render (cons t (reduction-steps t))))
    (apply vl-append picts))

The use of eval is pretty bad and I'd like to get rid of it if possible.
Also, the spacing looks off for an `eval`ed term for some reason.

It'd be great if there were a composable functional abstraction for
this. Does one exist and I just can't find it?

Cheers,
Asumu

Posted on the users mailing list.