[plt-scheme] redex: syntactic equality

On Sun, Oct 11, 2009 at 11:09 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> You're right, in the general case there is no way for redex to know what my
> language is doing...
>
> Actually, what I need is comparison of lambda terms:
> I want (let ((f (lambda (x) x)) (eq? f f)) to be true in my language
>
> So I'm going another way that consists in tagging lambda values with a
> unique identifier, and then having comparison check this:
>
> eg. (lambda (x) x) --> (lambda r1234 (x) x)
>
> The identifier is obtained with (gensym "r").
> This is working fine, except that I realize that I don't know how to write a
> test-->> for that, because when a lambda value ends up in the store, I have
> no way to know which r__ it has.
>
> Is there a way to do so?
>

No, you can't check this with test-->>.

Try formulating the expected result as a Redex pattern and comparing
the actual result to that pattern using redex-match. Use _!_ patterns
to force tags to be distinct.

http://docs.plt-scheme.org/redex/Patterns.html#%28idx._%28gentag._11._%28lib._redex/redex..scrbl%29%29%29

For example, if the expected result is the pair produced by λx.x and
λx.1, use this pattern:

   ((λ r_!_1 (x) x) (λ r_!_1 (x) 1))