[plt-scheme] redex: recursive metafunctions

On Sat, May 2, 2009 at 11:02 AM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> 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."

This sentence is at best confusing and at worse just plain wrong
depending on how you read it. I've just cut it from the docs.

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

The recursive call just above looks like it is missing "(env ..)"
around its argument.

>  ((collect-d (env (x_0 v_0 (b_0 false)) (x_1 v_1 s_1) ...))
>   (collect-d (x_1 v_1 s_1) ...)))

Same for this one.

Robby

> [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_________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>