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

Even without the productions on the first line, the one on the second
line is enough to send the matcher into a loop. Since C_1 matches
hole, matching (in-hole C_1 E) loops back to matching E without
consuming any input.

I'll take a closer look tomorrow and hopefully have a more production
suggestion.

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