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 < [email protected]> 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 < >>>> [email protected]> 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 < >>>>>> [email protected]> 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 [email protected]. >>>>>>> To view this discussion on the web visit >>>>>>> https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com >>>>>>> <https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>>> . >>>>>>> >>>>>> -- >>>>> 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/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com >>>>> <https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>> -- > 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/1d7cb5b7-d7c2-44a7-b513-bb8280a54f13n%40googlegroups.com > <https://groups.google.com/d/msgid/racket-users/1d7cb5b7-d7c2-44a7-b513-bb8280a54f13n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAL3TdOMWKMNXscoFvGUrbMiGGgkQzS-VmiK_N%2Bix_i8WdGXvSg%40mail.gmail.com.
