Adds a parameter that provides a default for redex-check's #:attempt argument

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)

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

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

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