Dear Robby, Thank you for the response. It is what I expected. I think for current goal typesetting isn't that important, so I'll define a macro for reduction-relation.
Thank you a lot, Anton BR, Anton Podkopaev podkopaev.net On Thu, Feb 25, 2016 at 3:41 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote: > reduction-relation doesn't expand its body, it just looks at it and > processes it. So if you write: > > #lang racket > (require redex) > > (define-language L > (E ::= (list v ... E e ...) (car E) (cdr E) hole) > (v ::= (list v ...) natural) > (e ::= (list e ...) (car e) (cdr e) natural)) > > (define-syntax-rule (==> a b) (--> (in-hole E a) (in-hole E b))) > > (define red > (reduction-relation > L > (==> (car (list v_1 v_2 ...)) v_1) > (==> (cdr (list v_1 v_2 ...)) (list v_2 ...)))) > > (test-->> red > (term (list (car (cdr (cdr (cdr (list 0 1 2 3 4))))))) > (term (list 3))) > > > then redex is going to ignore your macro definition. > > In general, redex doesn't work well with macros like this because of > typesetting reasons. But if you don't want to typeset the model, then > you can use a macro that expands into the entire reduction-relation. > (I recommend typesetting not because it is beautiful enough (yet) but > because it avoids errors in transcription later when you publish your > model.) > > For the specific example above and maybe in you use-case, you can use > 'with', removing the define-syntax-rule and writing this definition of > red instead: > > (define red > (reduction-relation > L > (==> (car (list v_1 v_2 ...)) v_1) > (==> (cdr (list v_1 v_2 ...)) (list v_2 ...)) > with > [(--> (in-hole E a) (in-hole E b)) > (==> a b)])) > > Robby > > > On Thu, Feb 25, 2016 at 6:13 AM, Anton Podkopaev <podkoav...@gmail.com> > wrote: > > Dear colleagues, > > > > I'm working on a semantics in Redex, which reduction rules have a lot in > > common. > > To reduce duplicate code I want to define a macros (say `==>`) for > reduction > > rule definition. > > Unfortunately, I haven't managed to do that: > > I've got "reduction-relation: the ==> relation is not defined". > > Could anyone help me with it? > > > > BR, > > Anton Podkopaev > > podkopaev.net > > > > -- > > 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. > -- 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.
