# [plt-scheme] About redex

Hi, all:
some issues around the redex
the code snippet:
(module test mzscheme
(require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3)))
(define basic-grammar
(language
(e x (e e) ("lam" x e))
(x variable-not-otherwise-mentioned)
))
(define ext-grammar
(extend-language
basic-grammar
(C number string )
(e .... C)
))
(define-metafunction sub
basic-grammar
[(((x_1) ... x_2 x_3 ...) (x_4 ... x_2 x_5 ...))
(sub (((x_1) ... x_3 ...) (x_4 ... x_2 x_5 ...)))]
[(((x_1) ... x_2 x_3 ...) (x_4 ... ))
(sub (((x_1) ... (x_2) x_3 ...) (x_4 ...)))]
[(((x_1) ...) (x_4 ... ))
(x_1 ...)])
(define-metafunction fv
basic-grammar
[x_1 (x_1)]
[(e_1 e_2) ,(append (term (fv e_1)) (term (fv e_2)))]
[("lam" x_1 e_1) (sub ((fv e_1) (x_1)))]
)
;;?
(define-metafunction/extension fv1
ext-grammar
fv
[C_1 ()]
)
(define ext2-grammar
(extend-language
ext-grammar
(prim + - * /)
(C .... prim)
(e .... prim)
)
)
#;(define test (term (fv1 ("lam" y ("lam" x (+ x y))))))
#;(define test2 (test-match ext2-grammar e_1 '(+ ("lam" x (+ 1)))))
)
1. how can I use "define-metafunction/extension"?
firstly, it is inconvenient to rename fv to fv1
second, how can I reuse the definitions in fv?
btw, is there also a demo show on "define-multi-arg-metafunction"?
2. a little suggestion: we see that ext2-grammar is something wrong which
makes e and C all terminate on
prim. however, redex just accept it. so , test2 make multiple matches. For
someone experienced to redex,
there is a quickly respond to the grammar. But, for the freshes, it takes
time to handle. So, I suggest redex
do a static check on this case and report a warning
thanks
Gang
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20071206/8afb8833/attachment.html>