I am just trying to define a redex language that accepts 1, (1 + 1), (1 + 1 + 1), etc. As I have experienced, this is not trivial. Moreover (not included in my example) I want + to be available both monadic and diadic. Of course my example is a simplified version of what I want to do finally. Redex probably is not the fastest engine to do what I want; I am just curious how far redex can go theoretically.
As another example, consider how to describe the following in redex: t ::= a t ::= a b t Mark that the Backus-Naur form does allow, but does not require parentheses. Thanks. Jos -----Original Message----- From: William J. Bowman [mailto:w...@williamjbowman.com] Sent: domingo, 26 de abril de 2015 19:54 To: Jos Koot Cc: racket-users@googlegroups.com Subject: Re: [racket-users] define-language, trouble with parentheses. (resending due to issues posting to list) Jos, What are you trying to model with your language? Are you trying to model a binary + operation that can add only 2 numbers? Or maybe you are trying to model a binary + operation that can add any 2 terms? What about an n-ary + operation that can add any number of terms? -- William J. Bowman On Sun, Apr 26, 2015 at 05:44:19PM +0200, Jos Koot wrote: > Hi Matthias, > > Sofar I have the following: > > (require redex) > > (define-language jk > (t n v > (side-condition (t x_1 ...) (term (check (x_1 ...))))) > ; mark x_1 in stead of x. > ; without suffix _1 x is not bound in the guard. > (x + t) > (n number) > (v (variable-except +))) > > (define-metafunction jk check : any -> any > ((check ()) #t) > ((check (+ t x_1 ...)) (check (x_1 ...))) > ((check else) #f)) > > (redex-match? jk t 1) ; -> #t > (redex-match? jk t (term (1 + 1))) ; -> #t > (redex-match? jk t (term (1 + 1 + 1 + 1))) ; -> #t > (redex-match? jk t (term ((1 + 1 + 1) + a + (1 + 1 + 1)))) ; -> #t > > Or did you have something different in mind? > Thanks, Jos > > _____ > > From: racket-users@googlegroups.com [mailto:racket-users@googlegroups.com] > On Behalf Of Matthias Felleisen > Sent: sábado, 25 de abril de 2015 19:38 > To: Jos Koot > Cc: racket-users@googlegroups.com > Subject: Re: [racket-users] define-language, trouble with parentheses. > > > > Redex's term-language is about defining __abstract__ syntax not concrete > syntax. > For the former, the tricks of concrete syntax don't matter. > > So let's think, how would you generalize > > #lang racket > > (require redex) > > (define-language jk > (t n > (n + t) > (n + n + t) > (n + n + n + t)) > (n number)) > > (redex-match? jk t 1) > (redex-match? jk t (+ 1 1)) > (redex-match? jk t (+ 1 1 1)) > > with the tools you have in Redex? -- Matthias > > > > > > > On Apr 24, 2015, at 5:30 PM, Jos Koot wrote: > > > I have trouble translating the following into a define-language form: > > term ::= number > term ::= number + term > > An attempt like: > > (define-language my-language > (term number (number + term)) > > does not work. It accepts (1 + (2 + 3)) and ((1 + 2) +3) but not (1 + 2 + > 3). > > May be there already is a method to do something like: > > > (define-language my-language > (term number (number + ,@term-list)) > (term-list (term))) > > or > > (define-languafe my-language > (term (number + number ... ...))) > > where the first ... refers to + and the second one to number, alternating of > course. > > If something like the above two above already is possible in some way, > please direct me to the related parts of the docs. > If not, would it be a great efffort to allow ,@ or ... ... in a > language-definition-clause? > If not too big an effort may be I could try to implement it, but I warn you, > I would need much guidance. > > Thanks, Jos > > -- > 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. > > -- > 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.
