Get redex traces result as picture?

Questions & Answers
1

traces function in redex given a nice GUI result, but what if I want to put it into scribble manual? How can I do that?

2

I'm not sure there is a very nice way, sadly. In order to get it into scribble, it would need to be a pict, but traces is operating at the pasteboard% layer and that doesn't convert to picts.

But just to be sure this is the right answer, are you looking for a particular layout of a graph, or just the layout of a particular term?

1 Like
3

I think one possible approach is to use traces/ps to generate a Postscript file, then use an external tool to convert the Postscript file to a png, and then include this png in the doc.

There’s also https://docs.racket-lang.org/scriblib/gui-eval.html, but I’m not sure if it can actually be used here.

1 Like
4

An approach like that can be made to work, and now that you mention it we did something like that for the redex book.

One small tweak: if you go to PDF and then use the latex backend to drop the PDF in, you won't have to rasterize.

1 Like
5

This is output from trace

εœ–η‰‡
εœ–η‰‡860Γ—482 53.1 KB

This is output from trace/ps
εœ–η‰‡
εœ–η‰‡1070Γ—312 59.6 KB

then for gui-eval, I have tried but also cannot figure out how to use it XD

6

The arrows don't show in the second one because the terms are too close together. Is that the difference you're asking about?

1 Like
7

yes, the problem is I cannot get adjusted picture

8

This is code that does some layout for you. It isn't the prettiest layout but maybe it will get you started?

#lang racket
(require redex)

(define-language L
  (e ::= (op e e) tt ff)
  (op ::= ∧ ∨)
  (C ::= (op hole e) (op e hole) hole))

(define-judgment-form L
  #:contract (--> e e)
  #:mode (--> I O)

  [------------------------- "∧ tt"
   (--> (in-hole C (∧ tt e))
        (in-hole C e))]

  [------------------------- "∧ ff"
   (--> (in-hole C (∧ ff e))
        (in-hole C ff))]

  [------------------------- "∨ tt"
   (--> (in-hole C (∨ tt e))
        (in-hole C tt))]

  [------------------------- "∨ ff"
   (--> (in-hole C (∨ ff e))
        (in-hole C e))])

(define (layout terms)
  (define root
    (for/or ([term (in-list terms)])
      (and (null? (term-node-parents term))
           term)))
  
  (define visited (make-hash))
  (let loop ([depth 0]
             [width 0]
             [node root])
    (cond
      [(hash-ref visited node #f) (void)]
      [else
       (hash-set! visited node #t)
       (term-node-set-position! node (* width 200) (* depth 100))
       (for ([child (in-list (term-node-children node))]
             [width (in-naturals)])
         (loop (+ depth 1)
               width
               child))])))

(traces -->
        (term (∨ (∧ tt ff) (∧ ff tt)))
        #:layout layout)
1 Like
9

Another approach might be to use traces with a custom #:graph-pasteboard-mixin that uses all the incoming information to draw a pict. I am unsure how easy/difficult that is in practice, but if you get it to work it may be the most flexible in allowing you to change the output however you want it to be.

The following is speculation and details may be wrong, because I would have to actually start to try to implement it, to see whether certain details need to be changed / adapted, so this is just a rough idea of a plan.

Looking at [1] I think this is the method which ends up rendering the graphics for the pasteboard.
One neat thing about rackets dc<%> is that there are many different implementations, so what if we were to create a modified/derived version of the mixin in [1] that basically wraps the original mixin (to reuse all the drawing implementation details), but then does the following:

  1. the new mixin is parameterized/constructed with a bitmap-dc% or maybe even a record-dc%
  2. on-paint is overridden to call the original mixins implementation with the custom dc
  3. convert the custom dc to a pict via:

[1] gui/graph.rkt at d1fef7a43a482c0fdd5672be9a6e713f16d8be5c Β· racket/gui Β· GitHub

1 Like