2011/5/2 Casey Klein <clkl...@eecs.northwestern.edu>:
> On Mon, May 2, 2011 at 1:56 PM, Robby Findler
> <ro...@eecs.northwestern.edu> wrote:
>> Since L and F can both just be hole, this means that A has effectively
>> has this as a sublanguage:
>>
>> A ::= A
>>
>> and Redex can't cope with that. This should probably be a bug tho (not
>> sure if that should be an error or it should work, tho; hopefully
>> Casey will have an opinion).
>
> I'd like to support definitions like Stephen's, but I'm not sure how.
> They seem to require Redex to guess where to position the hole (i.e.,
> how many times to unroll the context definition) then check that its
> choice fits.
>
> I think I know how to recognize definitions that could send the
> matcher into a loop, so at the very least, we should make them syntax
> errors.
>
>> To work around the problem, you would have to separate the situations
>> where L and F are both empty and have that be a separate case.
>>
>> Sometimes, possibly in your larger program, the simplest thing is to
>> have a non-terminal that is just a single layer of an L context and
>> then use that to make both A and L, eg:
>>
>> L1 ::= (hole e) | presumably | lots | of | other | stuff ...
>> L ::= hole | (in-hole L1 L)
>>
>
> For example,
>
> (define-language test
> (e x (λ x e) (e e))
> (x variable-not-otherwise-mentioned)
> (F (λ x hole))
> (L (hole e))
> (A (in-hole F A)
> (in-hole L A)
> hole))
>
>> (redex-match test A (term hole))
> `(,(make-match `(,(make-bind 'A (make-hole)))))
>> (redex-match test A (term (hole x)))
> `(,(make-match `(,(make-bind 'A `(,(make-hole) x)))))
>> (redex-match test A (term ((λ x hole) x)))
> `(,(make-match `(,(make-bind 'A `((λ x ,(make-hole)) x)))))
>> (redex-match test A (term ((λ x (λ x hole)) x)))
> `(,(make-match `(,(make-bind 'A `((λ x (λ x ,(make-hole))) x)))))
>> (redex-match test A (term ((λ x (λ x (hole x))) x)))
> `(,(make-match `(,(make-bind 'A `((λ x (λ x (,(make-hole) x))) x)))))
>> (redex-match test A (term ((λ x ((λ x (λ x (hole x))) x)) x)))
> `(,(make-match `(,(make-bind 'A `((λ x ((λ x (λ x (,(make-hole) x))) x))
> x)))))
>
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)))
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/dev
