[plt-scheme] redex: recursive metafunctions

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Sat May 2 12:02:08 EDT 2009


A beginner's question on recursive metafunctions in redex.

The documentation says:
"Each of the rhs-expressions is implicitly wrapped in term. In  
addition, recursive calls in the right-hand side of the metafunction  
clauses should appear inside term."

but none of the example metafunctions given afterward use (term...) to  
make recursive calls.
(define-metafunction lc-lang
     free-vars : e -> (x ...)
     [(free-vars (e_1 e_2 ...))
      (∪ (free-vars e_1) (free-vars e_2) ...)]
     [(free-vars x) (x)]
     [(free-vars (lambda (x ...) e))
      (- (free-vars e) (x ...))])

What is the reason for that?

On the other hand, I'm trying to define a recursive metafunction  
(called collect-d) and use it from my reductions.

I get an error "collect-d: (collect-d) is not in my domain"

The defintion of collect-d is:

(define-metafunction λenv
   collect-d : (env (x v s) ...) -> (env (x v s) ...)
   ((collect-d (env)) (env))
   ((collect-d (env (x_0 v_0 (b_0 true)) (x_1 v_1 s_1) ...))
    (env-append (env (x_0 v_0 (b_0 true))) (collect-d (x_1 v_1  
s_1) ...)))
   ((collect-d (env (x_0 v_0 (b_0 false)) (x_1 v_1 s_1) ...))
    (collect-d (x_1 v_1 s_1) ...)))

[env-append is another (non-recursive) metafunction, which works fine]

Note that I have tried to put all recursive calls to collect-d in a  
(term ...), but I get the same error.

To give an idea of how I actually call the metafunction, this is a  
reduction rule that uses it:

    (--> ((env (x v s) ...) (in-hole E_1 (λ (x_1) e)))
         ((env (x v s) ...) (in-hole E_1 (closure x_1 e
                                                  (collect-d (env (x v  
s) ...)))))

Any idea what I'm doing plain wrong here?


-- Éric

Posted on the users mailing list.