[racket-dev] composing contexts in Redex?

On Mon, May 2, 2011 at 3:30 PM, Stephen Chang <stchang at ccs.neu.edu> wrote:
>>> (define-language test
>>>  (e x (λ x e) (e e))
>>>  (x variable-not-otherwise-mentioned)
>>>  (A hole
>>>     (in-hole (A e) (λ x A))))
>
> Cool, that works! I didnt think to do that with in-hole. Can you
> explain how it keeps the number of lambdas and arguments the same
> though? I'm cant quite figure out what's going on.
>

I spent some time trying to come up with a convincing explanation. I
didn't get anywhere. It turns out my problem was that it doesn't
actually work:

> (redex-match test A (term (((λ x ((λ y (λ z hole)) a)) b) c)))
`(,(make-match `(,(make-bind 'A `(((λ x ((λ y (λ z ,(make-hole))) a)) b) c)))))

One of these days maybe I'll learn that the redex-check step comes
before the email step (and way before the paper publishing step).