[plt-dev] recent Redex developments

New recently in Redex:

- Redex's where patterns now accept the full pattern language of Redex
(this is another source of ambiguity, of course, so it may also give
rise to multiple ways that a rule may fire).

- Added define-relation. This represents a relation as a function to
booleans. define-relation definitions looks a lot like
define-metafunction definitions, but it relaxes the constraint that
there is only one case that applies and instead if any case produces
#t, the relation is considered to hold. Also, there can be multiple
expressions in the body of a single case; those must all hold for the
case to hold. The intention is that this matches a little bit better
relations that are written down in sequent style. (But do keep in mind
that there are no fundamental changes here -- Redex cannot do any
prolog-like search or anything like that).

- The restriction that a metafunction definition has a single way for
a pattern to match has been slightly relaxed; specifically if all of
the ways that a pattern can decompose produce the same results, then
no error is signalled. For example, that allows this definition of set
minus:

(define-language empty-language)
(define-metafunction empty-language
  [(minus (any_1 ... any_2 any_3 ...) (any_2 any_4 ...))
   (minus (any_1 ... any_3 ...) (any_2 any_4 ...))]
  [(minus (any_1 ...) (any_2 any_3 ...))
   (minus (any_1 ...) (any_3 ...))]
  [(minus (any_1 ...) ())
   (any_1 ...)])

whereas in the previous versions, this call: (term (minus (1 1 1)
(1))) would have signalled an error.

Robby