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