[racket-dev] composing contexts in Redex?

2011/5/5 Stephen Chang <stchang at ccs.neu.edu>:
> 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'm not quite sure what you're going for, but I have some guesses below.

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

Can you define an "other stuff" non-terminal O:

(O hole ....)

and sprinkle some Os in A:

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

?

I'm not sure if I have the Os in the right spots, but this should be
OK termination-wise as long as O does not have any productions that
lead directly to A (e.g., the production A, a production B where B is
a non-terminal with production A, etc.). If it does, then the
outermost in-hole O would need to be reworked.

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

There would be no loop if C didn't include hole:

(L (λ x hole) (hole e))
(C L (in-hole L C))

Can you still define what you want using this C?

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