[plt-scheme] Redex generating terms
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?
David