diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt index 833e4b4549..86b67f962e 100644 --- a/collects/redex/private/rg.rkt +++ b/collects/redex/private/rg.rkt @@ -111,10 +111,12 @@ ; Determines a size measure for numbers, sequences, etc., using the ; attempt count. -(define default-attempt->size +(define default-attempt-size (λ (n) (inexact->exact (floor (/ (log (add1 n)) (log 5)))))) +(define attempt-size/c + (-> natural-number/c natural-number/c)) (define attempt->size - (make-parameter default-attempt->size)) + (make-parameter default-attempt-size)) (define (pick-number attempt #:top-threshold [top-threshold complex-threshold] [random generator-random]) (let loop ([threshold 0] @@ -748,8 +750,8 @@ (define-for-syntax print?-keyword (list '#:print? #t)) (define-for-syntax attempt-size-keyword - (list '#:attempt-size #'default-attempt->size - (list #'(-> natural-number/c natural-number/c) "#:attempt-size argument"))) + (list '#:attempt-size #'default-attempt-size + (list #'attempt-size/c "#:attempt-size argument"))) (define-for-syntax (prepare-keyword lists?) (list '#:prepare #f (list (if lists? #'(-> list? list?) #'(-> any/c any/c)) @@ -1008,6 +1010,8 @@ generate-term check-reduction-relation check-metafunction + default-attempt-size + 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 d1a5e63324..fba853226a 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1320,7 +1320,7 @@ random terms in its search. The size and complexity of these terms tend to incre 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 attempts (see @racket[generate-term]'s @racket[#:size] keyword). By default, the bound -grows logarithmically with failed attempts. +grows according to the @racket[default-attempt-size] function. When @racket[print?-expr] produces any non-@racket[#f] value (the default), @racket[redex-check] prints the test outcome on @racket[current-output-port]. @@ -1461,10 +1461,13 @@ produces and consumes argument lists.} (check-metafunction Σ (λ (args) (printf "~s\n" args)) #:attempts 2)] -@defproc[(exn:fail:redex:generation-failure? [v any/c]) boolean?]{ - Recognizes the exceptions raised by @racket[generate-term], - @racket[redex-check], etc. when those forms are unable to produce - a term matching some pattern. +@defproc[(default-attempt-size [n natural-number/c]) natural-number/c]{ +The default value of the @racket[#:attempt-size] argument to +@racket[redex-check] and the other randomized testing forms, this +procedure computes an upper bound on the size of the next +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[redex-pseudo-random-generator generator pseudo-random-generator?]{ @@ -1472,6 +1475,12 @@ produces and consumes argument lists.} use the parameter @racket[generator] to construct random terms. The parameter's initial value is @racket[(current-pseudo-random-generator)].} +@defproc[(exn:fail:redex:generation-failure? [v any/c]) boolean?]{ + Recognizes the exceptions raised by @racket[generate-term], + @racket[redex-check], etc. when those forms are unable to produce + a term matching some pattern. +} + @deftech{Debugging PLT Redex Programs} It is easy to write grammars and reduction rules that are diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index 278087beaa..8037b31292 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -77,4 +77,5 @@ (-> bindings? symbol? (-> any) any))] [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?)]) + [redex-pseudo-random-generator (parameter/c pseudo-random-generator?)] + [default-attempt-size attempt-size/c])