2011/5/5 Stephen Chang <stch...@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) ()]) > > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
