[racket-dev] composing contexts in Redex?

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.
>
>> To work around the problem, you would have to separate the situations
>> where L and F are both empty and have that be a separate case.
>>
>> Sometimes, possibly in your larger program, the simplest thing is to
>> have a non-terminal that is just a single layer of an L context and
>> then use that to make both A and L, eg:
>>
>>  L1 ::= (hole e) | presumably | lots | of | other | stuff ...
>>  L ::= hole | (in-hole L1 L)
>>
>
> For example,
>
> (define-language test
>  (e x (λ x e) (e e))
>  (x variable-not-otherwise-mentioned)
>  (F (λ x hole))
>  (L (hole e))
>  (A (in-hole F A)
>     (in-hole L A)
>     hole))
>
>> (redex-match test A (term hole))
> `(,(make-match `(,(make-bind 'A (make-hole)))))
>> (redex-match test A (term (hole x)))
> `(,(make-match `(,(make-bind 'A `(,(make-hole) x)))))
>> (redex-match test A (term ((λ x hole) x)))
> `(,(make-match `(,(make-bind 'A `((λ x ,(make-hole)) x)))))
>> (redex-match test A (term ((λ x (λ x hole)) x)))
> `(,(make-match `(,(make-bind 'A `((λ x (λ x ,(make-hole))) x)))))
>> (redex-match test A (term ((λ x (λ x (hole x))) x)))
> `(,(make-match `(,(make-bind 'A `((λ x (λ x (,(make-hole) x))) x)))))
>> (redex-match test A (term ((λ x ((λ x (λ x (hole x))) x)) x)))
> `(,(make-match `(,(make-bind 'A `((λ x ((λ x (λ x (,(make-hole) x))) x)) x)))))
>

Oh, but this simpler definition seems to be equivalent:

(define-language test
  (e x (λ x e) (e e))
  (x variable-not-otherwise-mentioned)
  (A hole
     (λ x A)
     (A e)))