[racket-dev] composing contexts in Redex?

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Mon May 2 15:27:29 EDT 2011

2011/5/2 Casey Klein <clklein at eecs.northwestern.edu>:
> On Mon, May 2, 2011 at 1:56 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> Since L and F can both just be hole, this means that A has effectively
>> has this as a sublanguage:
>>
>>  A ::= A
>>
>> and Redex can't cope with that. This should probably be a bug tho (not
>> sure if that should be an error or it should work, tho; hopefully
>> Casey will have an opinion).
>
> I'd like to support definitions like Stephen's, but I'm not sure how.
> They seem to require Redex to guess where to position the hole (i.e.,
> how many times to unroll the context definition) then check that its
> choice fits.
>
> I think I know how to recognize definitions that could send the
> matcher into a loop, so at the very least, we should make them syntax
> errors.

Another thing that occurs to me now (and perhaps in the past) is to
detect this during matching and treat it as a match failure. If that
makes the language Stephen wrote work, then perhaps that's the right
choice.

Robby



Posted on the dev mailing list.