[plt-scheme] Generate fresh variables in REDEX metafunctions?

Yes, that won't work. In order to generate fresh variables in a
metafunction,  you have to use the lower-level interface to redex.
Specifically, you have to write something like this:

#lang scheme
(require (planet "reduction-semantics.ss" ("robby" "redex.plt" 4)))

(define-language lang)
(define-metafunction f
  lang
  [(any ...)
   ,(term-let ([x (variable-not-in (term (any ...)) 'x)])
      (term (x any ...)))])

(term (f (a b c))) ;; => (term (x a b c))
(term (f (x y z))) ;; => (term (x1 x y z))

Robby

On Fri, Mar 14, 2008 at 3:45 AM, Yu,Gang <wuhanyugang at gmail.com> wrote:
>
> Hi, all:
>
>     It seems the following does not work
>
> ===================================================================================
> (define-metafunction refT
>     basic-grammar
>     [(((T_4 x_4) ... (ptype_1 x_1) (T_2 x_2) ...) (x_1 x_3 ...))
>      (CH (((ptype_1 &) x_1 boxed_1) (refT (((T_4 x_4) ... (ptype_1 x_1) (T_2
> x_2) ...) (x_3 ...)))))
>      (side-condition (term (fresh boxed_1)))]
>     [(((T_4 x_4) ... (T_1 x_1) (T_2 x_2) ...) (x_1 x_3 ...))
>      (CH ((T_1 x_1 x_1) (refT ((T_4 x_4) ... (T_1 x_1) ((T_2 x_2) ...) (x_3
> ...)))))
>      ]
>     [(((T_1 x_1) ...) ()) ()])
>
> ===================================================================================
>
> I just want to generate the fresh variables like boxed_1 ,boxed_2 ..... in
> the meta-function not in the reduction rules?
>
> How can I ? or the redex version is too old?
>
> thanks
>
>
>
>
> Gang
>
>
>
>
>
>
>
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
>