[racket-dev] composing contexts in Redex?

Hmm, or maybe you've found a bug in my model. Either way, thanks for
looking into this.


2011/5/2 Casey Klein <clklein at eecs.northwestern.edu>:
> 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).
>