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