[racket-dev] composing contexts in Redex?

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Mon May 2 14:56:46 EDT 2011

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



Posted on the dev mailing list.