[racket] redex: default matching behavior of patterns

Ok after 2 minutes more of thought I guess the response will most likely be "which integer will you be referencing in the result of the metafunction" -- so maybe it can be an error to use an unadorned pattern variable twice in a pattern?

On 05/01/2012 05:45 PM, Jon Rafkind wrote:
> The default matching behavior of patterns in redex will try to match duplicate pattern variables to the same term. Thus
>
> #lang racket
>
> (require redex)
>
> (define-language Z [x integer])
> (define-metafunction Z
>   simple : integer integer -> integer
>   [(simple integer integer) 1])
>
> (term (simple 1 2))
>> simple: no clauses matched for (simple 1 2)
> Won't match because the pattern (simple integer integer) will match the first `integer' to 1, and wants to the second reference to `integer' to the same thing. To get it to work I need to adorn the pattern variables with _1 and _2 to make them unique.
>
> (define-language Z [x integer])
> (define-metafunction Z
>   simple : integer integer -> integer
>   [(simple integer_1 integer_2) 1])
>
> I would prefer (if possible) if the default behavior treated unadorned pattern variables as fresh so that I don't have to remember to attach a suffix. I guess this might break existing programs but I can't imagine anyone really relies on this behavior (unadorned variables matching duplicate terms).
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users