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 <[email protected] > <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 < >> [email protected] <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 <[email protected] >>> <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 [email protected] <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 [email protected]. For more options, visit https://groups.google.com/d/optout.
