[racket-dev] composing contexts in Redex?
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).
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)
hth,
Robby
2011/5/2 Stephen Chang <stchang at ccs.neu.edu>:
> Is there any way to compose contexts in Redex? I want to represent a
> context where, at each level, the leftmost term is an arbitrary number
> of nested lambdas, and the hole is in the body of the innermost
> lambda.
>
> A ::= hole | (\x_1...\x_n.A) e_1 .. e_n
>
> Below is my (stripped down) attempt at representing this in redex, but
> trying to match (term hole) to an A context goes into an infinite
> loop.
>
> #lang racket
> (require redex)
>
> (define-language test
> (e x (λ x e) (e e))
> (x variable-not-otherwise-mentioned)
> (F hole (λ x F))
> (L hole (L e))
> (A hole (in-hole L (in-hole F A))))
>
> _________________________________________________
> For list-related administrative tasks:
> http://lists.racket-lang.org/listinfo/dev