[plt-dev] Re: recent Redex developments

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<robby at 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
>