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

'render-term' is not a function because it looks at the source
location information and uses that in the rendering process. For
example, compare these:

#lang racket
(require redex)
(define-language L
  (e (e e)
     x
     (λ (x) e))
  (x variable-not-otherwise-mentioned))

(term->pict L ((λ (x) (x x))
               (λ (x) (x x))))
(term->pict L ((λ (x) (x x)) (λ (x) (x x))))


The simplest thing is probably to use to-lw/stx (you could use
pretty-print to build the syntax object too, if you wanted some
automatic layout stuff), assuming you don't have any metafunction
calls you want to render. If you do, then Redex would have to be
changed so you could communicate the metafunctions to it somehow.
Patches welcome.

Robby

On Wed, Apr 18, 2012 at 10:08 PM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:
> 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