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:
#fAs 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