Oh -- and I should have pointed out that the where change is a backwards incompatible change. Specifically, if you used a variable in a where clause before that wasn't a non-terminal, Redex now treats that like a literal (just like in other patterns).
I hope this won't cause too much confusion. Robby On Thu, Jun 25, 2009 at 8:35 PM, Robby Findler<ro...@eecs.northwestern.edu> wrote: > 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 > _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
