2011/5/2 Stephen Chang <stch...@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
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/dev
