[racket-dev] composing contexts in Redex?

From: Stephen Chang (stchang at ccs.neu.edu)
Date: Mon May 2 14:35:33 EDT 2011

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))))



Posted on the dev mailing list.