[plt-scheme] redex is great

Thanks,
I made the change and all is still working.
I also uploaded the corrected version to :
www.telefonica.net/web2/koot/rdx-d.scm
Jos

----- Original Message ----- 
From: "Casey Klein" <clklein at cs.uchicago.edu>
To: "Jos Koot" <jos.koot at telefonica.net>
Cc: "Robby Findler" <robby at eecs.northwestern.edu>; 
<plt-scheme at list.cs.brown.edu>
Sent: Sunday, February 22, 2009 9:52 PM
Subject: Re: [plt-scheme] redex is great


On Sun, Feb 22, 2009 at 8:34 AM, Jos Koot <jos.koot at telefonica.net> wrote:
> You mean this?
>
> (write
>  (time
>   (redex-check cλ T
>    (lambda (t) (< (length (apply-reduction-relation reductor t)) 2))
>    #:attempts 10000
>    #:source reductor
>    #:retries 100)))
> cpu time: 46250 real time: 49094 gc time: 3810
> #<void>
>
> Jos

Almost, but you've made what I suspect might be a common mistake: the
third position in a redex-check expression shouldn't be a function --
redex-check won't call it. Instead, just write the "body" of the
function:

(redex-check
 cλ T
 (< (length (apply-reduction-relation reductor (term T))) 2)
 #:attempts 10000
 #:source reductor
 #:retries 100)

The names bound by the generated pattern (just `T' here) are available
as term variables in the "test" expression (as the LHS of a
reduction-relation case binds term variables in its RHS).

See the documentation for an example.

http://docs.plt-scheme.org/redex/Testing.html#(form._((lib._redex/main..ss)._redex-check))