<div class="gmail_quote">On Dec 6, 2007 9:38 PM, Robby Findler <<a href="mailto:robby@cs.uchicago.edu">robby@cs.uchicago.edu</a>> wrote: <blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> <div><div></div><div class="Wj3C7c">On Dec 6, 2007 3:59 AM,  <<a href="mailto:yug@ios.ac.cn">yug@ios.ac.cn</a>> 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 </div></div>You've got two functions, however, that do different things. They can't both have the same name, right? <div class="Ih2E3d"> > second, how can I reuse the definitions in fv? </div>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?</blockquote><div> let's do some tests:  > (term (fv ("lam" y ("lam" x (z (x y)))))) (z) > (term (fv ("lam" y ("lam" x (z (x 1)))))) fv: no clauses matched for (("lam" y ("lam" x (z (x 1))))) > (term (fv1 ("lam" y ("lam" x (z (x 1)))))) fv1: no clauses matched for (("lam" y ("lam" x (z (x 1))))) So, what I want is the "fv" function for grammar ext-grammar I just want a show case on the usage for define-metafunctions/extension, of course, no need to rename will be better, thanks </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> <div class="Ih2E3d"> > btw, is there also a demo show on "define-multi-arg-metafunction"? </div>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). <div class="Ih2E3d"> > 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 </div>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? </blockquote><div> I just think a process on scanning the non-terminals, and report something warnning: just like: e ----C ----prim e -----------prim there is a converge on prim for e matching, i.e a prim will make a two e matches, I think redex can do this statically, and report that thanks   </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> Robby _________________________________________________  For list-related administrative tasks:  <a href="http://list.cs.brown.edu/mailman/listinfo/plt-scheme" target="_blank">http://list.cs.brown.edu/mailman/listinfo/plt-scheme</a> </blockquote></div> -- Gang