[racket] Does Redex have support for multi-hole evaluation contexts?

On Sat, Jul 7, 2012 at 8:04 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> No, there is no way to do that in Redex.
>
> Are you trying to model parallelism?

Yep.  We could have just used single-hole contexts "E ::= (E e) | (e
E) | ... " that allow for the two expressions in (e1 e2) to be
evaluated in arbitrary order, but we wanted to make parallelism
explicit in the model.  Using define-judgment-form, we can do
something along the lines of

(define-judgment-form my-lang

  [(small-step (e_1 e_2) (e_11 e_22))
   (small-step e_1 e_11)
   (small-step e_2 e_22)]

  ...more rules here...

  )

This works, but I was wondering if there was some other trick I hadn't
thought of for modeling parallelism.

Thanks,
Lindsey