[racket-dev] composing contexts in Redex?
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))))