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
____________________
Racket Users list:
http://lists.racket-lang.org/users
