[plt-scheme] redex: recursive metafunctions

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

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

Just wondering: since the contract of the metafunction is clear,  
couldn't it be possible to report more precisely what the problem is  
(similarly to contract violations), something along the lines of:
"collect-d broken contract: expected (env (x v s) ...) given (x v s)  
(other arguments were ...)"

?

-- Éric

Posted on the users mailing list.