[plt-scheme] redex: syntactic equality

Thanks Casey, I'm now using test-predicate in conjunction with redex- 
match, it works fine.

-- Éric


On Oct 12, 2009, at 6:15 AM, Casey Klein wrote:

> 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))