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