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

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Sun Jul 8 07:49:32 EDT 2012

I'm not sure of another way (but there might be one I just haven't
found), but do you want this program to reduce?

  ((+ 1 2) 3)

That is, a program that has a value in parallel with a computation?

Robby

On Sat, Jul 7, 2012 at 10:37 PM, Lindsey Kuper <lkuper at cs.indiana.edu> wrote:
> 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

Posted on the users mailing list.