[racket-dev] composing contexts in Redex?

2011/5/2 Casey Klein <clklein at eecs.northwestern.edu>:
>
> (define-language test
>  (e x (λ x e) (e e))
>  (x variable-not-otherwise-mentioned)
>  (A hole
>     (in-hole (A e) (λ x A))))
>
>> (redex-match test A (term hole))
> `(,(make-match `(,(make-bind 'A (make-hole)))))
>> (redex-match test A (term (((λ y (λ x hole)) a) b)))
> `(,(make-match `(,(make-bind 'A `(((λ y (λ x ,(make-hole))) a) b)))))
>> (redex-match test A (term (((λ y hole) a) b)))
> false
>> (redex-match test A (term ((λ y (λ x hole)) a)))
> false
>> (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)))))
>> (redex-match test A (term ((λ x ((λ y (λ z hole)) a)) b)))
> false
>

(Oops, hit Send before typing the rest of my message.)

Does that work?