[racket-dev] composing contexts in Redex?

On Mon, May 2, 2011 at 2:27 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> 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.
>

I think that would work for Stephen's original definition. The matcher
could watch for the situation where it gets back to A without either L
or F consuming any input and consider that outcome a failure.

There are other languages, though, where this strategy misses matches.
For example, take this one:

(define-language trouble
    (W hole
       (in-hole W (hole))))

It should be the case that (term (hole)) matches W, but producing that
match requires passing back through W before consuming any input.