[racket-dev] composing contexts in Redex?

So I'm struggling with redex again and I cant figure out a way to
utilize any of the previously mentioned tricks. I just included what I
have below and I described what I'm trying to do. Hopefully someone
will have some time to take a look? :)

I have a context A, where the focus is in the body of the lambda(s) of
an application, and for every lambda, there is an argument to match.
I'm using Casey's definition from earlier in this thread (you did
uncover a bug in my model, thanks for that!).

(A hole (in-hole (A e) (λ x A)))


However, I also want to be able to split A's so that other stuff can
go in between, so I defined a more general context C and a
metafunction balance where if (balance C) = 0, then C \in A. The
balance fn (defined below) returns the number of extra unmatched args
available in a C, and #f otherwise (ie - if there's too many lambdas).

(C hole (λ x C) (C e))


Finally, I have evaluation contexts E that use the previous definitions:

  (E ;; hole (E e) (in-hole A E)
     (side-condition (in-hole C_1 E) (term (balance C_1)))
     ... other Es ...)
I'd like to be able to use the (commented out) productions on the
first line of E, but I was getting infinite loops. Then I realized
that the productions on the first line are equivalent to a subset of C
that have a nonnegative balance, so I tried using the production on
the second line instead, thinking it would work bc I got rid of the
hole in E, but it still infinite loops when trying to match hole.
Finally, I want to be able to use these contexts in conjunction with
other, more complicated E productions.


I included the relevant snippets of my language definition below:

(define-language test
  (e x (λ x e) (e e))
  (x (variable-except e λ v a A n C E hole any))
  (n integer)
  (C hole (λ x C) (C e))
  (A hole (in-hole (A e) (λ x A))) ; via Casey
  (E #;hole #;(E e) #;(in-hole A E)
     (side-condition (in-hole C_1 E) (term (balance C_1)))
     (side-condition
      (in-hole C_1 ((in-hole A_1 (λ x_1 (in-hole C_2 (in-hole E x_1)))) E))
      (and (redex-match test A (term (in-hole C_1 C_2)))
           (not (member (term x_1) (term (bound-vars-C C_2)))))))
  )

(define-metafunction test
;  balance : C -> n or #f
  [(balance C) (balance_ C 0 0)])
(define-metafunction test
;  balance_ : C n n -> n or #f
  [(balance_ hole n_1 n_2)    ,(- (term n_2) (term n_1))]
  [(balance_ (C e) n_1 n_2)    (balance_ C n_1 ,(add1 (term n_2)))]
  [(balance_ (λ x C) n_1 n_2) ,(if (< (term n_1) (term n_2))
                                   (term (balance_ C ,(add1 (term n_1)) n_2))
                                   #f)])

;; bound-vars
;;  compute the set/list of bound variables in a given term
(define-metafunction test
  bound-vars-C : C -> (x ...)
  [(bound-vars-C (λ x C))
   (x ,@(term (bound-vars-C C)))]
  [(bound-vars-C (C e)) (bound-vars-C C)]
  [(bound-vars-C hole)  ()])