diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt index 88f3e53ce5..b18e0a4397 100644 --- a/collects/redex/private/rg.rkt +++ b/collects/redex/private/rg.rkt @@ -21,7 +21,7 @@ (define (exotic-choice? [random generator-random]) (= 0 (random 5))) (define (use-lang-literal? [random generator-random]) (= 0 (random 20))) -(define default-check-attempts 1000) +(define default-check-attempts (make-parameter 1000)) (define ascii-chars-threshold 1000) (define tex-chars-threshold 1500) @@ -740,7 +740,7 @@ 'what (if loc (string-append loc "\n") "") msg)))])) (define-for-syntax attempts-keyword - (list '#:attempts #'default-check-attempts + (list '#:attempts #'(default-check-attempts) (list #'natural-number/c "#:attempts argument"))) (define-for-syntax source-keyword (list '#:source #f)) @@ -1011,6 +1011,7 @@ check-reduction-relation check-metafunction default-attempt-size + default-check-attempts attempt-size/c exn:fail:redex:generation-failure? redex-pseudo-random-generator) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 53b6ca4d2b..dece84125a 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1316,7 +1316,7 @@ matches @racket[pattern] then evaluating @racket[property-expr] using the @racket[match-bindings] produced by @racket[match]ing @math{t} against @racket[pattern]. -@racket[redex-check] generates at most @racket[attempts-expr] (default @racket[1000]) +@racket[redex-check] generates at most @racket[attempts-expr] (default @racket[(default-check-attempts)]) random terms in its search. The size and complexity of these terms tend to increase with each failed attempt. The @racket[#:attempt-size] keyword determines the rate at which terms grow by supplying a function that bounds term size based on the number of failed @@ -1470,7 +1470,11 @@ test case from the number of previously attempted tests @racket[n]. Currently, this procedure computes the base 5 logarithm, but that behavior may change in future versions. } - + +@defparam[default-check-attempts attempts natural-number/c]{Determines the default +value for @racket[redex-check]'s optional @racket[#:attempts] argument. By default, +@racket[attempts] is 1,000.} + @defparam[redex-pseudo-random-generator generator pseudo-random-generator?]{ @racket[generate-term] and the randomized testing forms (e.g., @racket[redex-check]) use the parameter @racket[generator] to construct random terms. The parameter's diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index 8037b31292..3d2b4c3b1d 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -78,4 +78,5 @@ [relation-coverage (parameter/c (listof coverage?))] [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))] [redex-pseudo-random-generator (parameter/c pseudo-random-generator?)] - [default-attempt-size attempt-size/c]) + [default-attempt-size attempt-size/c] + [default-check-attempts (parameter/c natural-number/c)]) diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index f73c48da4f..3f2b9fc2ef 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -621,6 +621,11 @@ (e e 4) (n number)) + (test (let ([checked 0]) + (parameterize ([default-check-attempts 1]) + (redex-check lang () (set! checked (add1 checked)) #:print? #f)) + checked) + 1) (test (redex-check lang d #t #:attempts 1 #:print? (not #t)) #t) (test (redex-check lang d #f #:print? #f) (make-counterexample 5))