[racket-dev] composing contexts in Redex?

2011/5/2 Stephen Chang <stchang at ccs.neu.edu>:
>> 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)))
>
> Yes, you are right. But I left out a part of my grammar, which is that
> I need the number of nested lambdas and the number of arguments to be
> equal. I couldnt figure out a way to define that with only one
> context.
>
> Here's what I'm currently working with:
>
>  (F (λ x hole) (λ x F))
>  (L (hole e) (L e))
>  (A hole
>     (side-condition
>      (in-hole L_1 (in-hole F_1 A))
>      (= (term (num-λs F_1))
>         (term (num-args L_1)))))
>
>

(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