[plt-scheme] About redex

On Dec 6, 2007 3:59 AM,  <yug at ios.ac.cn> wrote:
> 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

You've got two functions, however, that do different things. They
can't both have the same name, right?

> second, how can I reuse the definitions in fv?

When you write an extended metafunction (like fv1), the cases from the
original metafunction (in this case fv) are automatically copied into
the new one. Is that what you're asking?

> btw, is there also a demo show on "define-multi-arg-metafunction"?

Not yet, I'm sorry to say, but the definition of a multi-arg
metafunction looks just like a regular one (except for any recursive
calls). It is the calls that change. Instead of (F (x y z)), you write
(F x y z).

> 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

Unfortunately, Redex cannot tell, just by looking at the grammar,
which non-terminals you intend to be contexts and which ones you
don't, so I'm not sure that there is a simple check one could do here.
In other words, why would the static check say that "C" is bad, but
that "e" is good?

Robby