Adds a #:attempt-size keyword to the random testing forms

collects/redex/private/rg.rkt

@@ -104,8 +104,27 @@
 
 ; Determines a size measure for numbers, sequences, etc., using the
 ; attempt count.
-(define (attempt->size n)
+(define attempt->size
-  (inexact->exact (floor (/ (log (add1 n)) (log 5)))))
+  (make-parameter (λ (n) (inexact->exact (floor (/ (log (add1 n)) (log 5)))))))
+(define-for-syntax (with-attempt->size arg-stx redex-form body)
+  (if arg-stx
+      #`(parameterize ([attempt->size
+                        (contract (-> natural-number/c natural-number/c) #,arg-stx
+                                  #,(let ([m (syntax-source-module arg-stx)])
+                                      (cond [(module-path-index? m)
+                                             (format "~a" (module-path-index-resolve m))]
+                                            [(or (symbol? m) (path? m))
+                                             (format "~a" m)]
+                                            [else (format "~s client" redex-form)]))
+                                  '#,redex-form 
+                                  "#:attempt-size argument"
+                                  #(#,(syntax-source arg-stx)
+                                    #,(syntax-line arg-stx) 
+                                    #,(syntax-column arg-stx) 
+                                    #,(syntax-position arg-stx)
+                                    #,(syntax-span arg-stx)))])
+          #,body)
+      body))
 
 (define (pick-number attempt #:top-threshold [top-threshold complex-threshold] [random random])
   (let loop ([threshold 0] 
@@ -118,7 +137,7 @@
             (< attempt (caar levels))
             (< top-threshold (caar levels))
             (not (exotic-choice? random)))
-        (generator (expected-value->p (attempt->size (- attempt threshold))) random)
+        (generator (expected-value->p ((attempt->size) (- attempt threshold))) random)
         (loop (caar levels) (cdar levels) (cdr levels)))))
 
 (define (pick-natural attempt [random random])
@@ -131,7 +150,7 @@
   (pick-number attempt #:top-threshold real-threshold random))
 
 (define (pick-sequence-length attempt)
-  (random-natural (expected-value->p (attempt->size attempt))))
+  (random-natural (expected-value->p ((attempt->size) attempt))))
 
 (define (min-prods nt prods base-table)
   (let* ([sizes (hash-ref base-table nt)]
@@ -709,12 +728,13 @@
      (let-values ([(names names/ellipses) 
                    (extract-names (language-id-nts #'lang 'redex-check)
                                   'redex-check #t #'pat)]
-                  [(attempts-stx source-stx retries-stx print?-stx)
+                  [(attempts-stx source-stx retries-stx print?-stx size-stx)
                    (apply values
                           (parse-kw-args `((#:attempts . ,#'default-check-attempts)
                                            (#:source . #f)
                                            (#:retries . ,#'default-retries)
-                                           (#:print? . #t))
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
                                          (syntax kw-args)
                                          stx))])
        (with-syntax ([(name ...) names]
@@ -728,7 +748,8 @@
              (let ([att (assert-nat 'redex-check #,attempts-stx)]
                    [ret (assert-nat 'redex-check #,retries-stx)]
                    [print? #,print?-stx])
-               (unsyntax
+               #,(with-attempt->size
+                  size-stx 'redex-check
                   (if source-stx
                       #`(let-values ([(metafunc/red-rel num-cases) 
                                       #,(cond [(and (identifier? source-stx) (metafunc source-stx))
@@ -773,7 +794,7 @@
     (if (zero? remaining)
         #t
         (let ([attempt (add1 (- attempts remaining))])
-          (let-values ([(term bindings) (generator (attempt->size attempt) attempt retries)])
+          (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)])
             (if (andmap (λ (bindings) 
                           (with-handlers 
                               ([exn:fail?
@@ -866,25 +887,28 @@
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
     [(_ name property . kw-args)
-     (with-syntax ([m (metafunc/err #'name stx)]
+     (let-values ([(attempts retries print? size)
-                   [(attempts retries print?) 
+                   (apply values
                           (parse-kw-args `((#:attempts . , #'default-check-attempts)
                                            (#:retries . ,#'default-retries)
-                                     (#:print? . #t))
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
                                          (syntax kw-args)
-                                   stx)])
+                                         stx))]
-       (with-syntax ([show (show-message stx)])
+                  [(m) (metafunc/err #'name stx)])
-         (syntax/loc stx
+       (with-attempt->size
-           (let ([att (assert-nat 'check-metafunction attempts)]
+        size 'check-metafunction
-                 [ret (assert-nat 'check-metafunction retries)])
+        (quasisyntax/loc stx
+          (let ([att (assert-nat 'check-metafunction #,attempts)]
+                [ret (assert-nat 'check-metafunction #,retries)])
             (check-lhs-pats 
-              (metafunc-proc-lang m)
+             (metafunc-proc-lang #,m)
-              m
+             #,m
              (λ (term _) (property term))
              att
              ret
              'check-metafunction
-              (and print? show))))))]))
+             (and #,print? #,(show-message stx)))))))]))
 
 (define (reduction-relation-srcs r)
   (map (λ (proc) (or (rewrite-proc-name proc)
@@ -898,25 +922,28 @@
 (define-syntax (check-reduction-relation stx)
   (syntax-case stx ()
     [(_ relation property . kw-args)
-     (with-syntax ([(attempts retries print?)
+     (let-values ([(attempts retries print? size)
+                   (apply values
                           (parse-kw-args `((#:attempts . , #'default-check-attempts)
                                            (#:retries . ,#'default-retries)
-                                     (#:print? . #t))
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
                                          (syntax kw-args)
-                                   stx)]
+                                         stx))])
-                   [show (show-message stx)])
+       (with-attempt->size
-       (syntax/loc stx
+        size 'check-reduction-relation
-         (let ([att attempts]
+        (quasisyntax/loc stx
-               [ret (assert-nat 'check-reduction-relation retries)]
+          (let ([att (assert-nat 'check-reduction-relation #,attempts)]
+                [ret (assert-nat 'check-reduction-relation #,retries)]
                 [rel (assert-rel 'check-reduction-relation relation)])
             (check-lhs-pats
              (reduction-relation-lang rel)
              rel
              (λ (term _) (property term))
-            attempts
+             att
-            retries
+             ret
              'check-reduction-relation
-            (and print? show)))))]))
+             (and #,print? #,(show-message stx)))))))]))
 
 (define-signature decisions^
   (next-variable-decision

collects/redex/redex.scrbl

@@ -1209,12 +1209,14 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
                        (code:line #:source metafunction)
                        (code:line #:source relation-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property-expr any/c]
                            [attempts-expr natural-number/c]
                            [relation-expr reduction-relation?]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Searches for a counterexample to @racket[property-expr], interpreted
 as a predicate universally quantified over the pattern variables
 bound by @racket[pattern]. @racket[redex-check] constructs and tests 
@@ -1224,8 +1226,11 @@ 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])
-random terms in its search. The size and complexity of these terms increase with 
+random terms in its search. The size and complexity of these terms tend to increase 
-each failed attempt. 
+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.
 
 When @racket[print?-expr] produces any non-@racket[#f] value (the default), 
 @racket[redex-check] prints the test outcome on @racket[current-output-port].
@@ -1295,11 +1300,13 @@ and the @racket[exn:fail:redex:test-term] component contains the term that induc
 @defform/subs[(check-reduction-relation relation property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property (-> any/c any/c)]
                            [attempts-expr natural-number/c]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Tests @racket[relation] as follows: for each case of @racket[relation],
 @racket[check-reduction-relation] generates @racket[attempts] random
 terms that match that case's left-hand side and applies @racket[property] 
@@ -1314,11 +1321,13 @@ when @racket[relation] is a relation on @racket[L] with @racket[n] rules.}
 @defform/subs[(check-metafunction metafunction property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property (-> (listof any/c) any/c)]
                            [attempts-expr natural-number/c]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Like @racket[check-reduction-relation] but for metafunctions. 
 @racket[check-metafunction] calls @racket[property] with lists
 containing arguments to the metafunction.}

collects/redex/tests/rg-test.rkt

@@ -662,6 +662,15 @@
                           #:source mf)))
           #rx"no counterexamples"))
   
+  ; Without the #:attempt-size argument, the attempt would use size 0,
+  ; which does not require a non-terminal decision.
+  (test (let/ec k
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (redex-check lang d #t #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (test (raised-exn-msg 
          exn:fail:redex?
          (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
@@ -818,6 +827,15 @@
          (λ () (check-reduction-relation (reduction-relation L (--> 1 2) (--> 3 4 name)) (curry eq? 1))))
         #px"counterexample found after 1 attempt with name:\n3\n")
   
+  (test (let/ec k
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (check-reduction-relation 
+             (reduction-relation L (--> e e))
+             (λ _ #t) #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (let ([T (reduction-relation
             L
             (==> number number
@@ -909,6 +927,16 @@
           generated)
         '((4 4) (4 3) (3 4)))
   
+  (test (let/ec k
+          (define-language L (n number))
+          (define-metafunction L
+            [(f n) n])
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (check-metafunction f (λ _ #t) #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
   (test (output (λ () (check-metafunction m (curry eq? 1))))
         #px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")