[racket-dev] composing contexts in Redex?

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)))))