[plt-scheme] redex: recursive metafunctions
Hi,
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.
eg:
(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) ...)))))
"fun")
Any idea what I'm doing plain wrong here?
Thanks,
-- Éric