[plt-scheme] redex: recursive metafunctions

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Sat May 2 13:31:43 EDT 2009

The ellipsis means "splice out what comes before into this place". You
had empty lists there, I believe.

Robby

On Sat, May 2, 2009 at 12:21 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> On May 2, 2009, at 13:17 , Robby Findler wrote:
>>
>> Well, the contract is written on the metafunction and since there are
>> no HO contracts, I didn't include that in the error message (altho if
>> you still think it would help, I could).
>
> I think so, yes.
>
>> But as for the other, that is what you got. The function was called like
>> this:
>>
>>  (collect-d)
>
> I don't get this. It rather seems to me that the function was called 1+
> arguments
> (the triple (x_1 v_1 s_1) and the "...")
>
> -- Éric
>
>> On Sat, May 2, 2009 at 11:34 AM, Eric Tanter <etanter at dcc.uchile.cl>
>> wrote:
>>>>>
>>>>> 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.