[plt-scheme] About redex

On Dec 6, 2007 9:00 PM,  <yug at ios.ac.cn> wrote:
>
>
>
>
> 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

I understand now. Yes, you're right -- this cannot be done with the
current redex. I'll look into fixing this in a future version. The
basic problem is that the extended metafunction only uses the new
grammar for the new clauses, not for the old clauses.

The best I can offer you is something like the code at the end of this message.

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

Oh, I thought you were saying something completely different before.
Yes, such tools would be useful.

Robby

(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)]
    [("lam" x_1 any_1) (sub ((fv any_1) (x_1)))]
    [(any_1 ...) ,(apply append (term ((fv any_1) ...)))]
    [any_1 ()])

  (printf "~s\n" (term (fv ("lam" y ("lam" x (z (x y)))))))
  (printf "~s\n" (with-handlers ((exn? exn-message)) (term (fv ("lam"
y ("lam" x (z (x 1)))))))))