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