# [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!