[plt-scheme] Redex q. about using 'with' for parallel composition

Sorry, I (for one) don't see an easier way. This seems like it would
be a good argument for multi-hole context support in Redex, but that's
a pretty major change.

Robby

On Mon, Oct 26, 2009 at 12:11 PM, John Clements
<clements at brinckerhoff.org> wrote:
> I'd like to use redex to extend a small relation to parallel composition.
>  That is: if a list contains a and b that reduce to a' and b', then I'd like
> to be able to extend this relation to
>
> blah ... a blah ... b blah ...
>
> reduces to
>
> blah ... blah ... blah ... a' b'
>
> (I'm just moving the a' and b' to the end for readability.)
>
> Put differently, I'd like a with clause like this:
>
>
> [(--> (sel-or-act_1 ... a sel-or-act_2 ... b sel-or-act_3 ...)
>         (sel-or-act_1 ... sel-or-act_2 ... sel-or-act_3 ... c d))
>    (==> (a b) (c d))]
>
> Unfortunately, redex's 'with' won't let me do this, because it's unhappy
> about the shape of (==> (a b) (c d)).  I also can't write it as (==> a b c
> d).
>
> Naturally, I can accomplish this differently by just not using the 'with'
> clause and expanding the individual reductions into the desired form.
>  However, I thought I'd ask whether there's another easy way to accomplish
> this.
>
> John
>
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
>