Redex- rendering multiple where clauses on separate lines

Questions & Answers
1

I'm writing a semantics for egglog and struggling to get good output from render-reduction-relation.

I often use many where clauses to bind intermediate values, and these are all rendered in-line:

image
image1984×116 32.6 KB

Is there a way to get these conditions rendered on separate lines? Seems like not based on this redex source code.

Most of my problems I can fix with manual control using with-compound-rewriter, but I think not this one. @robby, maybe you have advice for me. It may be that I need to add a hook to redex.

1 Like
2

It looks like metafunction-fill-acceptable-width affects the rendering when rule-pict-style is in 'compact-vertical mode. Here's an example. Looks like the docs need updating!

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

(define-metafunction L
  long-name-for-the-identity-function : any -> any
  [(long-name-for-the-identity-function any) any])

(define r
  (reduction-relation
   L
   (--> e e_4
        (where e_1 (long-name-for-the-identity-function e))
        (where e_2 (long-name-for-the-identity-function e_1))
        (where e_3 (long-name-for-the-identity-function e_2))
        (where e_4 (long-name-for-the-identity-function e_3)))))

(parameterize ([rule-pict-style 'compact-vertical]
               [metafunction-fill-acceptable-width 10])
  (reduction-relation->pict r))
3

That looks a lot better, thanks!
Should I ask more redex questions here or make new posts for each? Maybe new posts in the Questions & Answers category?

4

The docs for metafunction-fill-acceptable-width are pretty good actually, I just didn't see that one

Maybe should be renamed to where-clause-acceptable-width?

5

I'm happy with anything!

I guess renaming things like that will break existing code. Probably it is best to add more cross references or maybe add some nice starting examples so that folks can more easily find existing things. I'm happy to take ideas, especially based on where you looked but didn't find something or what kind of new examples would have helped you.

6

Cross-references are a good idea. I followed the first tutorial and found it very helpful. Extending that with more formatting examples would be great!

7

For some of my projects, I have created files with names such as should be racket. They contain simple compositions of Racket functions and renames that I consider better sign-posts for eventual readers. Consider starting a should-be-redex.rkt file where where-clause-acceptable-width is a renaming of metafunction-fill-acceptable-width. You may find that the former is the only name you use — in which case we should probably add this secondary name to redex — or you may find that you use it only once and then a local file is good enough.