[racket] redex: default matching behavior of patterns

From: Jon Rafkind (rafkind at cs.utah.edu)
Date: Tue May 1 19:45:09 EDT 2012

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

Posted on the users mailing list.