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

From: Lindsey Kuper (lkuper at cs.indiana.edu)
Date: Sat Jul 7 22:29:49 EDT 2012

Hi,

I have a Redex model for a language witih an explicitly parallel
reduction semantics, where an application (e1 e2) can step to (e1'
e2') -- that is, where both the operator and the operand can step at
once.  Because we wanted to explicitly model this parallel reduction,
we first thought of using multi-hole evaluation contexts, but a
mailing list thread that I found from 2009
(http://lists.racket-lang.org/users/archive/2009-October/036237.html)
indicated that Redex didn't support those (in fact, that person was
trying to solve a similar problem).

So, instead, we use an inference-rule-based semantics (defined using
`define-judgment-form`, with the reduction relation defined as a thin
wrapper around `judgment-holds`, something like in
http://git.racket-lang.org/plt/blob/HEAD:/collects/redex/examples/define-judgment-form/sos.rkt).
 This has been working fine, but I'm curious if it's still necessary
to do it that way, or if Redex now supports multi-hole contexts -- or
if there is yet another way to do explicit parallel reductions that
I've not yet considered.

Thanks,
Lindsey

Posted on the users mailing list.