On Wednesday, March 14, 2018 at 3:14:34 PM UTC-7, Robby Findler wrote: > > I usually use metafunctions for that purpose. It might be nice if there > were more such functions built into redex that came with their own renders, > I guess. > > More than once, I've gotten stuck typesetting in Redex and go back to LaTeX. It would be nice to have something like a Redex cookbook to demonstrate visually interesting outputs.
> Overall, I think we're missing a higher-level for rendering. I like the > low-level that is there, but it is, um, low level. I think the collection > of stuff in the unstable redex packae is a good start but we need more. > > I am profoundly interested in eliminating LaTeX from my workflow. A high-level rendering engine would go a long way towards that. > Robby > > > On Wed, Mar 14, 2018 at 4:33 PM, Andrew Kent <pnw...@gmail.com > <javascript:>> wrote: > >> Oh wow, yep that's exactly the piece-wise behavior I was hoping >> for, thanks! >> >> I guess my only question then is if there are better ways to get >> "and"/"or" behavior and rendering or if my hacky metafunctions are what >> people usually use for that purpose. >> >> Best, >> Andrew >> >> On Wed, Mar 14, 2018 at 4:23 PM, Robby Findler < >> ro...@eecs.northwestern.edu <javascript:>> wrote: >> >>> Maybe this is a helpful piece of part of the puzzle? >>> >>> #lang racket >>> (require redex) >>> (define-language L >>> (b ::= 1 0) >>> (n ::= natural)) >>> (define-metafunction L >>> ∪ : n n -> n >>> [(∪ n_1 n_2) >>> 0 >>> (side-condition (term (lt n_1 n_2))) >>> >>> or >>> 1 >>> (side-condition (term (gt n_1 n_2))) >>> >>> or >>> 2 >>> (side-condition (term (eq n_1 n_2)))]) >>> >>> (define (infix id lws) >>> (list "" >>> (list-ref lws 2) >>> (~a " " id " ") >>> (list-ref lws 3) >>> "")) >>> >>> (with-compound-rewriters >>> (['∪ (λ (lws) (infix "∪" lws))] >>> ['lt (λ (lws) (infix "<" lws))] >>> ['gt (λ (lws) (infix ">" lws))] >>> ['eq (λ (lws) (infix "=" lws))]) >>> (render-metafunction ∪)) >>> >>> >>> On Wed, Mar 14, 2018 at 10:46 AM, Andrew Kent <pnw...@gmail.com >>> <javascript:>> wrote: >>> >>>> In some recent redex tinkering I've been doing I've had to hack around >>>> two (somewhat related) things that I could easily imagine being "built-in" >>>> features for redex: >>>> >>>> 1. boolean combinators (e.g. and, or) >>>> 2. a piece-wise form (i.e. basically a "cond" that you can use on the >>>> rhs of a metafunction definition which renders in the classic piece-wise >>>> way using a large curly brace) >>>> >>>> Both of these are things that are used ubiquitously to describe >>>> mathematical algorithms in a clear way... neither adds actual >>>> expressiveness to redex (you can certainly model the functionality of both >>>> using the current tools), but I think it might be nice to be able to use >>>> these common mathematical "features" and have them "just work" (and >>>> render!!!) as expected without boilerplate and hoops. >>>> >>>> In case examples are more helpful, for "or" and "and" boolean operators >>>> I threw together some silly functions that give "or" and "and" behavior >>>> and >>>> allow me to render them how I want (e.g. OR is not parenthesized when >>>> rendered, POR is). Unfortunately you obviously don't get the >>>> short-cuirtining behavior we sometimes want with "or": >>>> >>>> ``` >>>> (define-metafunction sst >>>> OR : or-bool ... -> bool >>>> [(OR any_1 ... true any_2 ...) true] >>>> [(OR any_1 ...) false]) >>>> >>>> ;; duplicate definition that will be rendered with parens >>>> (define-metafunction sst >>>> POR : or-bool ... -> bool >>>> [(POR any_1 ... true any_2 ...) true] >>>> [(POR any_1 ...) false]) >>>> >>>> (define-metafunction sst >>>> AND : and-bool ... -> bool >>>> [(AND any_1 ... false any_2 ...) false] >>>> [(AND any_1 ...) true]) >>>> >>>> ;; duplicate definition that will be rendered with parens >>>> (define-metafunction sst >>>> PAND : and-bool ... -> bool >>>> [(PAND any_1 ... false any_2 ...) false] >>>> [(PAND any_1 ...) true]) >>>> ``` >>>> >>>> Here's an example function that uses some of those boolean operators: >>>> >>>> ``` >>>> (define-metafunction sst >>>> gamma : s s N -> bool >>>> [(gamma s_1 s_2 ∅) false] >>>> [(gamma s_1 s_2 (set-cons (× t_1 t_2) N)) >>>> (AND (POR (subtype s_1 t_1) or (gamma (t-diff s_1 t_1) s_2 N)) >>>> and (POR (subtype s_2 t_2) or (gamma s_1 (t-diff s_2 t_2) >>>> N)))]) >>>> ``` >>>> >>>> and here it is rendered: >>>> >>>> [image: Screen Shot 2018-03-14 at 11.29.58 AM.png] >>>> >>>> For a piecewise operator, again certainly you can model the behavior >>>> just using the current tools, but if you imagine a metafunction that wants >>>> to pattern-match on the lhs of the definition and then piece-wise dispatch >>>> on the right-hand side of the definition to clearly illustrate to a reader >>>> what is going on... I don't think there's really a nice way to get that >>>> sort of figure/behavior currently (although I certainly could be >>>> mistaken!). The only example I had for piecewise currently I've rewritten >>>> a >>>> decent amount to fit the current set of tools redex has: >>>> >>>> [image: Screen Shot 2018-03-14 at 11.34.21 AM.png] >>>> >>>> What I wanted to do initially was just pattern match on the n_1 and n_2 >>>> for a _single_ last clause (instead of the last 3 that appear there now) >>>> that then uses a piece-wise to determine what should happen. Instead, >>>> initially I had 3 identical pattern matching clauses that used "where" >>>> clauses to decide which to use... that was awful to look at (way to much >>>> identical pattern matching going on) so I refactored it and settled on >>>> using helper functions to pull out the fields of n_1 and n_2 (instead of >>>> pattern matching) and "where" clauses to determine which case to use. >>>> >>>> One more quick note -- part of the reason I'm bothering to write this >>>> email is because I think these features would support (what I believe is) >>>> one of the primary goals of redex: the ability to generate clear, tested >>>> figures for papers/talks/etc. This week I'm writing a tutorial that >>>> features tons of regex-generated figures that are heavily tested to help >>>> avoid silly mistakes (thank you redex!) and that's where this stream of >>>> thoughts emerged. >>>> >>>> Anyway, I know we're all busy, and I hope this doesn't come across too >>>> "feature request"-y, but I at least wanted to hear peoples thoughts on the >>>> matter (or possible other alternative approaches) if anyone has a sec and >>>> is interested ;-) >>>> >>>> Best, >>>> Andrew >>>> >>>> -- >>>> 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 <javascript:>. >>>> For more options, visit https://groups.google.com/d/optout. >>>> >>> >>> >> > -- 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+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
