[plt-scheme] Redex generating terms

On Fri, Apr 2, 2010 at 4:09 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> Given the following definitions:
>
> #lang scheme
> (require redex)
>
> (define-language L
>  [a (a ...)])
>
> (define (depth x)
>  (cond [(cons? x) (add1 (apply max (map depth x)))]
>        [else 0]))
>
> I'm surprised the following can produce a number greater than 5:
>
> (for/fold ([n 0])
>  ([i (in-range 100)])
>  (max n (depth (generate-term L a 5))))
>
> But the height of the generated terms can be far larger than 5, and
> consequently checking even trivial properties a small number of times is
> infeasible.  For example, this consumes all available memory on my machine:
>
> (redex-check L a ((lambda (x) #t) (term a))
>             #:attempts 30)
>
> Is this a bug in Redex, or am I misunderstanding the purpose of the size
> argument for generate-term?  And how can I work around this to test
> properties of this language?
>
> Actually, I was able to answer my own question.  Everything works fine with
> the equivalent grammar:
>
> (define-language L
>  [a () (a ...)])
>
> Is this intended or is there a bug in term generation?
>

There's a bug. I'll commit a fix shortly.

BTW, thanks for answering your own question. Your answer made finding
the bug very easy!