Re: [racket-users] Formal semantics of PLT Redex

2021-12-21 Thread Mallku Ernesto Soldevila Raffa
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 > (ma

Re: [racket-users] Formal semantics of PLT Redex

2021-12-21 Thread Robby Findler
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))

Re: [racket-users] Formal semantics of PLT Redex

2021-12-21 Thread Mallku Ernesto Soldevila Raffa
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

Re: [racket-users] Formal semantics of PLT Redex

2021-12-21 Thread Mallku Ernesto Soldevila Raffa
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 [

Re: [racket-users] Formal semantics of PLT Redex

2021-12-09 Thread Mallku Ernesto Soldevila Raffa
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

Re: [racket-users] Formal semantics of PLT Redex

2021-12-08 Thread Robby Findler
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 gram

Re: [racket-users] Formal semantics of PLT Redex

2021-12-08 Thread Mallku Ernesto Soldevila Raffa
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

Re: [racket-users] Formal semantics of PLT Redex

2021-12-08 Thread Robby Findler
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 < mallkuerne...@gmail.com> wrote: > Hi community!, > I'm interested in understanding the semantics of PLT Redex, since we are > working on a tool > to transla

[racket-users] Formal semantics of PLT Redex

2021-12-08 Thread Mallku Ernesto Soldevila Raffa
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 u