Exposes the default value of the #:attempt-size argument

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 '#:attempt-size #'default-attempt-size 
-        (list #'(-> natural-number/c natural-number/c) "#:attempt-size argument")))
+        (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)
 

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?]{
+@defproc[(default-attempt-size [n natural-number/c]) natural-number/c]{
-  Recognizes the exceptions raised by @racket[generate-term], 
+The default value of the @racket[#:attempt-size] argument to 
-  @racket[redex-check], etc. when those forms are unable to produce
+@racket[redex-check] and the other randomized testing forms, this 
-  a term matching some pattern.
+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

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])