Wow!, that was fast! No need to thank, I'm just using your awesome tool to perform random testing. Thanks, Mallku
El martes, 21 de diciembre de 2021 a las 18:22:09 UTC-3, Robby Findler escribió: > There was a bug in the matcher; I've pushed a fix. > > With that fix, you'll get > > (list > (match > (list > (bind 'A '(hole (hole hole))) > (bind 'x '(hole (hole hole)))))) > > as the result. That's different than the matcher because the pattern `A` > is really shorthand for something like `(name A (nt A))`, where the `name` > part introduces the name and the `nt` pattern matching construct matches > only non-terminals without binding a name. > > Thanks for finding the bug! > > Robby > > > On Tue, Dec 21, 2021 at 2:50 PM Mallku Ernesto Soldevila Raffa wrote: > >> Just to clarify, I understand that the several binds of x correspond to >> the several patterns name in the productions, and the pattern against with >> we are matching, but I would have expected for the firsts to be discarded, >> or, if still considered in the resulting match for some reason, that I >> don't >> know, I would have expected for the application of the constraint of >> names, >> that would have rendered #f the match. >> >> thanks!, >> Mallku >> >> El martes, 21 de diciembre de 2021 a las 17:38:28 UTC-3, Mallku Ernesto >> Soldevila Raffa escribió: >> >>> Hi to everyone!, >>> I'm trying to test the mechanization of Redex's semantics done in [1], >>> against the present version of racket, 8.3. I'm using the >>> random-match-test.rkt >>> >>> module from [1] to generate random grammars, patterns and terms, and to >>> test them >>> using the proposed mechanization of Redex in [1] and the actual >>> implementation of >>> it, in racket 8.3. >>> >>> In doing it, I've found an example that I cannot explain in terms of my >>> understanding >>> of the behavior of the name pattern: >>> >>> (define-language L [A (name x B)] >>> [B (hole (name x (hole hole)))]) >>> >>> (redex-match L (name x A) >>> (term (hole (hole hole)))) >>> >>> The result of the previous match is: >>> >>> (list (match (list >>> (bind 'A '(hole (hole hole))) >>> (bind 'x '(hole hole)) >>> (bind 'x '(hole (hole hole))) >>> (bind 'x '(hole (hole hole)))))) >>> >>> Which shows that 'x' is bound to different, non-equivalent, terms. While >>> I've never used the pattern name explicitly in such a way, while >>> defining >>> grammars, I'm still curious about what is going on here. Even more, I >>> would >>> have thought that the following match would return the same result as the >>> previous: >>> >>> (redex-match L (name x (name x B)) >>> (term (hole (hole hole)))) >>> >>> where I just replaced the non-term A by the rhs of its only production, >>> but >>> what I obtain is: >>> >>> #f >>> >>> As a side note, the mechanization of Redex in [1] just returns something >>> equivalent to: >>> >>> (bind 'x '(hole (hole hole))) >>> >>> In both cases. Does anyone understand the behavior of the shown example >>> under racket 8.3? >>> >>> Thanks in advance!, >>> Mallku >>> >>> [1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>> El jueves, 9 de diciembre de 2021 a las 13:20:31 UTC-3, Mallku Ernesto >>> Soldevila Raffa escribió: >>> >>>> Thanks a lot for the info! If I found any mismatches, I'll report it. >>>> >>>> Regards, >>>> Mallku >>>> >>>> El miércoles, 8 de diciembre de 2021 a las 23:32:25 UTC-3, Robby >>>> Findler escribió: >>>> >>>>> I'm sorry, my sentence was ambiguous! I'm saying that I don't know of >>>>> any other work that is specifically focused on the semantics of Redex. >>>>> (Of >>>>> course, there may be work I'm not aware of.) >>>>> >>>>> The paper is still a good match, I believe, yes. You're right that the >>>>> syntactic checks for well-formed grammars have tightened since that era, >>>>> but if the program is valid, then I think it should match; the underlying >>>>> algorithms have not changed, only bug fixes have happened. >>>>> >>>>> Of course, if you find that this isn't the case, I'd be very >>>>> interested to hear more :) >>>>> >>>>> Robby >>>>> >>>>> >>>>> >>>>> On Wed, Dec 8, 2021 at 6:34 PM Mallku Ernesto Soldevila Raffa wrote: >>>>> >>>>>> I beg your pardon!, I'm not understanding the answer, what is it that >>>>>> might be specific of Redex? >>>>>> >>>>>> I suspect that the answer is that there isn't some recent work on >>>>>> formal >>>>>> semantics specifically about Redex. In that case, does anybody know >>>>>> if the >>>>>> already mentioned paper [1] is still a good match for today's >>>>>> semantics of >>>>>> Redex? The paper provides a mechanization of the model in Redex, >>>>>> together >>>>>> with some tools to test it. Of interest is a tool that asks Redex to >>>>>> generate >>>>>> random patterns and terms that match against them, and tests if the >>>>>> mechanized model is capable of reproducing the matching (or that is >>>>>> what >>>>>> I suspect that the tests are doing :P ). It was possible to run the >>>>>> mechanization >>>>>> on a recent version of Redex, but the generated patterns are >>>>>> ill-formed >>>>>> (e.g., in-hole p1 p2, where p1 contains more than 1 hole). Of course >>>>>> I could >>>>>> provide more details about the error, but I don't know if it is of >>>>>> interest, it's >>>>>> a mechanization written for the Redex version that comes with Racket >>>>>> 5.* >>>>>> or something like that. >>>>>> >>>>>> Thanks!, >>>>>> Mallku >>>>>> >>>>>> >>>>>> [1] : >>>>>> https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>>>>> >>>>>> El miércoles, 8 de diciembre de 2021 a las 21:03:44 UTC-3, Robby >>>>>> Findler escribió: >>>>>> >>>>>>> I think that might be it specifically about redex, I am sorry to >>>>>>> say. >>>>>>> >>>>>>> Robby >>>>>>> >>>>>>> On Wed, Dec 8, 2021 at 5:28 PM Mallku Ernesto Soldevila Raffa wrote: >>>>>>> >>>>>>>> Hi community!, >>>>>>>> I'm interested in understanding the semantics of PLT Redex, since >>>>>>>> we are working on a tool >>>>>>>> to translate fragments of Redex models to Coq. At the moment, we >>>>>>>> just have a >>>>>>>> mechanization in Coq of the semantics proposed in a ~10 years old >>>>>>>> paper [1]. Does >>>>>>>> anybody know if there is an updated work on formal semantics of >>>>>>>> Redex? >>>>>>>> >>>>>>>> Thanks in advance!, >>>>>>>> Mallku >>>>>>>> >>>>>>>> [1] : >>>>>>>> https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>>>>>>> >>>>>>>> -- >>>>>>>> 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 >>>>>>>> >>>>>>> -- >>>>>> 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 >>>>>> >>>>> >>>>> -- >> 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 >> > > -- 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]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/dcfd3db0-13f7-4fd0-9054-b40be4fcf00bn%40googlegroups.com.
