Typesetting Redex definitions

20 views
Skip to first unread message

Mallku Ernesto Soldevila Raffa

unread,
Oct 26, 2021, 2:55:52 PM10/26/21
to Racket Users
Hi community!,
a colleague of mine is trying to typeset a grammar from a model in Redex,
using redex/pict. So far, he has obtained a nice-looking typesetting of
the productions, but with the inconvenience that they are not abstract. In
particular, there are parentheses around every list of symbols,
as in Redex. Since it seems that redex/pict does not generate the latex code
(or does it?), we are not able to get rid of those concrete-syntax details. Is
there any known/simple way of doing it?

Thanks in advance!,
Mallku

Robby Findler

unread,
Oct 26, 2021, 5:40:49 PM10/26/21
to Mallku Ernesto Soldevila Raffa, Racket Users
The only way to do that currently is to use the compound rewriters (they rewrite anything with parens) and the atomic rewriters (they rewrite anything without parens). The interface that redex provides is pretty low-level and I'd like to find time to improve it, but in the meantime there are some libraries on the package server that build higher-level ways to do this.

There's an example of with-compound-rewriter here: https://docs.racket-lang.org/redex/reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-compound-rewriter%29%29 and redex doesn't care if the thing it is rewriting is defined as a judgment form or as the syntax of a term; it'll apply the rewriter in either case.

As for what Redex generates, it isn't generating latex, it is generating picts (which basically boils down to postscript-style drawing commands when you think about them from the perspective of interoperating with other tools -- one nice thing to do is to use scribble (which generates latex) as it has handling to make them look nice in the rendered output, although getting the right fonts set up can sometimes be tricky).

hth,
Robby


--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/3c6330fe-a048-4561-98bf-495c9b92e06an%40googlegroups.com.

Mallku Ernesto Soldevila Raffa

unread,
Oct 26, 2021, 6:20:50 PM10/26/21
to Racket Users
Thank you very much for the information provided! We have a lot to experiment with.
Regards,
Mallku
Reply all
Reply to author
Forward
0 new messages