[plt-scheme] About redex

On Dec 6, 2007 9:38 PM, Robby Findler <robby at cs.uchicago.edu> wrote:

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


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

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

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


>
> Robby
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>



-- 
Gang
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20071207/35c5dc1a/attachment.html>