diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt index b2230a0397..f130453423 100644 --- a/collects/redex/private/rg.rkt +++ b/collects/redex/private/rg.rkt @@ -102,29 +102,27 @@ ;; E = 0 => p = 1, which breaks random-natural (/ 1 (+ (max 1 E) 1))) +(define-for-syntax (apply-contract ctc expr desc redex-form) + #`(contract #,ctc #,expr + #,(let ([m (syntax-source-module expr)]) + (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 #,desc + #(#,(syntax-source expr) + #,(syntax-line expr) + #,(syntax-column expr) + #,(syntax-position expr) + #,(syntax-span expr)))) + ; Determines a size measure for numbers, sequences, etc., using the ; attempt count. -(define attempt->size - (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 default-attempt->size + (λ (n) (inexact->exact (floor (/ (log (add1 n)) (log 5)))))) +(define attempt->size + (make-parameter default-attempt->size)) (define (pick-number attempt #:top-threshold [top-threshold complex-threshold] [random random]) (let loop ([threshold 0] @@ -722,60 +720,72 @@ "~a: ~a~a" 'what (if loc (string-append loc "\n") "") msg)))])) +(define-for-syntax (contracted-fix stx form [ctc #'(-> any/c any/c)]) + (and stx (apply-contract ctc stx "#:attempt-size argument" form))) +(define-for-syntax (contracted-attempt-size stx form) + (apply-contract #'(-> natural-number/c natural-number/c) stx "#:prepare argument" form)) + (define-syntax (redex-check stx) (syntax-case stx () [(_ lang pat property . kw-args) (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 size-stx) + [(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx) (apply values (parse-kw-args `((#:attempts . ,#'default-check-attempts) (#:source . #f) (#:retries . ,#'default-retries) (#:print? . #t) - (#:attempt-size . #f)) + (#:attempt-size . ,#'default-attempt->size) + (#:prepare . #f)) (syntax kw-args) stx))]) (with-syntax ([(name ...) names] [(name/ellipses ...) names/ellipses] [show (show-message stx)]) (with-syntax ([property (syntax - (λ (_ bindings) - (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) - property)))]) + (bind-prop + (λ (bindings) + (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) + property))))]) (quasisyntax/loc stx (let ([att (assert-nat 'redex-check #,attempts-stx)] [ret (assert-nat 'redex-check #,retries-stx)] - [print? #,print?-stx]) - #,(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)) - => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))] - [else - #`(let ([r (assert-rel 'redex-check #,source-stx)]) - (values r (length (reduction-relation-make-procs r))))])]) - (check-lhs-pats - lang - metafunc/red-rel - property - (max 1 (floor (/ att num-cases))) - ret - 'redex-check - (and print? show) - (test-match lang pat) - (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat)))) - #`(check-prop - #,(term-generator #'lang #'pat 'redex-check) - property att ret (and print? show)))))))))])) + [print? #,print?-stx] + [fix #,(contracted-fix fix-stx 'redex-check)] + [term-match (λ (generated) + (cond [(test-match lang pat generated) => values] + [else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))]) + (parameterize ([attempt->size #,(contracted-attempt-size size-stx 'redex-check)]) + #,(if source-stx + #`(let-values ([(metafunc/red-rel num-cases) + #,(cond [(and (identifier? source-stx) (metafunc source-stx)) + => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))] + [else + #`(let ([r (assert-rel 'redex-check #,source-stx)]) + (values r (length (reduction-relation-make-procs r))))])]) + (check-lhs-pats + lang + metafunc/red-rel + property + (max 1 (floor (/ att num-cases))) + ret + 'redex-check + (and print? show) + fix + #:term-match term-match)) + #`(check-prop + #,(term-generator #'lang #'pat 'redex-check) + property att ret (and print? show) fix (and fix term-match)))))))))])) (define (format-attempts a) (format "~a attempt~a" a (if (= 1 a) "" "s"))) -(define (check-prop generator property attempts retries show) - (let ([c (check generator property attempts retries show)]) +(define (check-prop generator property attempts retries show term-fix term-match) + (let ([c (check generator property attempts retries show + #:term-fix term-fix + #:term-match term-match)]) (if (counterexample? c) (unless show c) ; check printed it (if show @@ -786,43 +796,54 @@ (define-struct (exn:fail:redex:test exn:fail:redex) (source term)) (define-struct counterexample (term) #:transparent) +(define-struct term-prop (pred)) +(define-struct bind-prop (pred)) + (define (check generator property attempts retries show #:source [source #f] - #:match [match #f] - #:match-fail [match-fail #f]) + #:term-fix [term-fix #f] + #:term-match [term-match #f]) (let loop ([remaining attempts]) (if (zero? remaining) #t (let ([attempt (add1 (- attempts remaining))]) - (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)]) - (if (andmap (λ (bindings) - (with-handlers - ([exn:fail? - (λ (exn) - (when show - (show (format "checking ~s raises an exception\n" term))) - (raise - (if show - exn - (make-exn:fail:redex:test - (format "checking ~s raises an exception:\n~a" term (exn-message exn)) - (current-continuation-marks) - exn - term))))]) - (property term bindings))) - (cond [(and match match-fail (match term)) - => (curry map (compose make-bindings match-bindings))] - [match (match-fail term)] - [else (list bindings)])) - (loop (sub1 remaining)) - (begin - (when show - (show - (format "counterexample found after ~a~a:\n" - (format-attempts attempt) - (if source (format " with ~a" source) ""))) - (pretty-print term (current-output-port))) - (make-counterexample term)))))))) + (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)] + [(handler) + (λ (action term) + (λ (exn) + (let ([msg (format "~a ~s raises an exception" action term)]) + (when show (show (format "~a\n" msg))) + (raise + (if show + exn + (make-exn:fail:redex:test + (format "~a:\n~a" msg (exn-message exn)) + (current-continuation-marks) + exn + term))))))]) + (let ([term (with-handlers ([exn:fail? (handler "fixing" term)]) + (if term-fix (term-fix term) term))]) + (if (if term-match + (let ([bindings (make-bindings + (match-bindings + (pick-from-list (term-match term))))]) + (with-handlers ([exn:fail? (handler "checking" term)]) + (match property + [(term-prop pred) (pred term)] + [(bind-prop pred) (pred bindings)]))) + (with-handlers ([exn:fail? (handler "checking" term)]) + (match (cons property term-fix) + [(cons (term-prop pred) _) (pred term)] + [(cons (bind-prop pred) #f) (pred bindings)]))) + (loop (sub1 remaining)) + (begin + (when show + (show + (format "counterexample found after ~a~a:\n" + (format-attempts attempt) + (if source (format " with ~a" source) ""))) + (pretty-print term (current-output-port))) + (make-counterexample term))))))))) (define-syntax (check-metafunction-contract stx) (syntax-case stx () @@ -842,16 +863,18 @@ (check-prop ((compile lang 'check-metafunction-contract) (if dom dom '(any (... ...)))) - (λ (t _) - (with-handlers ([exn:fail:redex? (λ (_) #f)]) - (begin (term (name ,@t)) #t))) + (term-prop + (λ (t) + (with-handlers ([exn:fail:redex? (λ (_) #f)]) + (begin (term (name ,@t)) #t)))) att retries - show))))])) + show + #f + #f))))])) -(define (check-lhs-pats lang mf/rr prop attempts retries what show - [match #f] - [match-fail #f]) +(define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix + #:term-match [term-match #f]) (let ([lang-gen (compile lang what)]) (let-values ([(pats srcs) (cond [(metafunc-proc? mf/rr) @@ -878,8 +901,8 @@ retries show #:source (car srcs) - #:match match - #:match-fail match-fail))]) + #:term-match term-match + #:term-fix term-fix))]) (if (counterexample? c) (unless show c) (loop (cdr pats) (cdr srcs))))))))) @@ -887,28 +910,30 @@ (define-syntax (check-metafunction stx) (syntax-case stx () [(_ name property . kw-args) - (let-values ([(attempts retries print? size) + (let-values ([(attempts retries print? size fix) (apply values (parse-kw-args `((#:attempts . , #'default-check-attempts) (#:retries . ,#'default-retries) (#:print? . #t) - (#:attempt-size . #f)) + (#:attempt-size . ,#'default-attempt->size) + (#:prepare . #f)) (syntax kw-args) stx))] [(m) (metafunc/err #'name stx)]) - (with-attempt->size - size 'check-metafunction - (quasisyntax/loc stx - (let ([att (assert-nat 'check-metafunction #,attempts)] - [ret (assert-nat 'check-metafunction #,retries)]) - (check-lhs-pats - (metafunc-proc-lang #,m) - #,m - (λ (term _) (property term)) - att - ret - 'check-metafunction - (and #,print? #,(show-message stx)))))))])) + (quasisyntax/loc stx + (parameterize ([attempt->size #,(contracted-attempt-size size 'check-metafunction)]) + (let ([att (assert-nat 'check-metafunction #,attempts)] + [ret (assert-nat 'check-metafunction #,retries)] + [fix #,(contracted-fix fix 'check-metafunction #'(-> (listof any/c) (listof any/c)))]) + (check-lhs-pats + (metafunc-proc-lang #,m) + #,m + (term-prop property) + att + ret + 'check-metafunction + (and #,print? #,(show-message stx)) + fix)))))])) (define (reduction-relation-srcs r) (map (λ (proc) (or (rewrite-proc-name proc) @@ -922,28 +947,30 @@ (define-syntax (check-reduction-relation stx) (syntax-case stx () [(_ relation property . kw-args) - (let-values ([(attempts retries print? size) + (let-values ([(attempts retries print? size fix) (apply values (parse-kw-args `((#:attempts . , #'default-check-attempts) (#:retries . ,#'default-retries) (#:print? . #t) - (#:attempt-size . #f)) + (#:attempt-size . ,#'default-attempt->size) + (#:prepare . #f)) (syntax kw-args) stx))]) - (with-attempt->size - size 'check-reduction-relation - (quasisyntax/loc stx - (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)) - att - ret - 'check-reduction-relation - (and #,print? #,(show-message stx)))))))])) + (quasisyntax/loc stx + (parameterize ([attempt->size #,(contracted-attempt-size size 'check-reduction-relation)]) + (let ([att (assert-nat 'check-reduction-relation #,attempts)] + [ret (assert-nat 'check-reduction-relation #,retries)] + [rel (assert-rel 'check-reduction-relation relation)] + [fix #,(contracted-fix fix 'check-reduction-relation)]) + (check-lhs-pats + (reduction-relation-lang rel) + rel + (term-prop property) + att + ret + 'check-reduction-relation + (and #,print? #,(show-message stx)) + fix)))))])) (define-signature decisions^ (next-variable-decision diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 7da2bab25a..278a5405fe 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1210,13 +1210,15 @@ repeating as necessary. The optional keyword argument @racket[retries-expr] (code:line #:source relation-expr) (code:line #:retries retries-expr) (code:line #:print? print?-expr) - (code:line #:attempt-size attempt-size-expr)]) + (code:line #:attempt-size attempt-size-expr) + (code:line #:prepare prepare-expr)]) #:contracts ([property-expr any/c] [attempts-expr natural-number/c] [relation-expr reduction-relation?] [retries-expr natural-number/c] [print?-expr any/c] - [attempt-size-expr (-> natural-number/c natural-number/c)])]{ + [attempt-size-expr (-> natural-number/c natural-number/c)] + [prepare-expr (-> any/c any/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 @@ -1242,6 +1244,14 @@ nothing, instead @item{raising a @racket[exn:fail:redex:test] when checking the property raises an exception.} ] +The optional @racket[#:prepare] keyword supplies a function that transforms each +generated example before @racket[redex-check] checks @racket[property-expr]. +This keyword may be useful when @racket[property-expr] takes the form +of a conditional, and a term chosen freely from the grammar is unlikely to +satisfy the conditional's hypothesis. In some such cases, the @racket[prepare] +keyword can be used to increase the probability that an example satifies the +hypothesis. + When passed a metafunction or reduction relation via the optional @racket[#:source] argument, @racket[redex-check] distributes its attempts across the left-hand sides of that metafunction/relation by using those patterns, rather than @racket[pattern], @@ -1285,7 +1295,18 @@ term that does not match @racket[pattern].} (Σ number ...) (printf "~s\n" (term (number ...))) #:attempts 3 - #:source R))] + #:source R)) + + (redex-check + empty-lang + number + (begin + (printf "checking ~s\n" (term number)) + (positive? (term number))) + #:prepare (λ (n) + (printf "preparing ~s; " n) + (add1 (abs n))) + #:attempts 3)] @defstruct[counterexample ([term any/c]) #:inspector #f]{ Produced by @racket[redex-check], @racket[check-reduction-relation], and @@ -1301,12 +1322,14 @@ and the @racket[exn:fail:redex:test-term] component contains the term that induc ([kw-arg (code:line #:attempts attempts-expr) (code:line #:retries retries-expr) (code:line #:print? print?-expr) - (code:line #:attempt-size attempt-size-expr)]) + (code:line #:attempt-size attempt-size-expr) + (code:line #:prepare prepare-expr)]) #:contracts ([property (-> any/c any/c)] [attempts-expr natural-number/c] [retries-expr natural-number/c] [print?-expr any/c] - [attempt-size-expr (-> natural-number/c natural-number/c)])]{ + [attempt-size-expr (-> natural-number/c natural-number/c)] + [prepare-expr (-> any/c any/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] @@ -1322,15 +1345,18 @@ when @racket[relation] is a relation on @racket[L] with @racket[n] rules.} ([kw-arg (code:line #:attempts attempts-expr) (code:line #:retries retries-expr) (code:line #:print? print?-expr) - (code:line #:attempt-size attempt-size-expr)]) + (code:line #:attempt-size attempt-size-expr) + (code:line #:prepare prepare-expr)]) #:contracts ([property (-> (listof any/c) any/c)] [attempts-expr natural-number/c] [retries-expr natural-number/c] [print?-expr any/c] - [attempt-size-expr (-> natural-number/c natural-number/c)])]{ + [attempt-size-expr (-> natural-number/c natural-number/c)] + [prepare-expr (-> (listof any/c) (listof any/c))])]{ Like @racket[check-reduction-relation] but for metafunctions. @racket[check-metafunction] calls @racket[property] with lists -containing arguments to the metafunction.} +containing arguments to the metafunction. Similarly, @racket[prepare-expr] +produces and consumes argument lists.} @examples[ #:eval redex-eval diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index b4fda93812..719729a236 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -671,6 +671,46 @@ #f)) #t) + (let ([generated '()] + [fixed '()] + [fix add1]) + (redex-check lang number (set! fixed (cons (term number) fixed)) + #:prepare (λ (n) + (set! generated (cons n generated)) + (fix n)) + #:attempts 10 + #:print? #f) + (test fixed (map fix generated))) + (test (parameterize ([generation-decisions + (decisions #:num (list (λ _ 0)))]) + (redex-check lang number (= 0 (term number)) + #:prepare add1 + #:print? #f)) + (counterexample 1)) + (test (raised-exn-msg + exn:fail? + (redex-check lang 0 #t #:prepare (λ (_) (error 'fixer)) #:print? #f)) + #rx"fixing 0") + (test (raised-exn-msg + exn:fail:redex? + (redex-check lang natural #t #:prepare (compose - add1))) + #rx"does not match natural") + (test (raised-exn-msg + exn:fail:redex? + (redex-check lang natural #t + #:prepare - + #:source (reduction-relation lang (--> 47 1)))) + #rx"-47 does not match natural") + (test (redex-check lang number (= 0 (term number)) + #:prepare add1 + #:source (reduction-relation lang (--> 0 1)) + #:print? #f) + (counterexample 1)) + (test (raised-exn-msg + exn:fail:contract:blame? + (redex-check lang natural #t #:prepare (λ () 0))) + #rx"rg-test broke the contract") + (test (raised-exn-msg exn:fail:redex? (redex-check lang n #t #:source (reduction-relation lang (--> x 1)))) @@ -813,6 +853,42 @@ generated) '((4 4) (4 3) (3 4))) + (let ([generated '()] + [fixed '()] + [fix add1]) + (check-reduction-relation + (reduction-relation L (--> number number)) + (λ (n) (set! fixed (cons n fixed))) + #:prepare (λ (n) + (set! generated (cons n generated)) + (fix n)) + #:attempts 10 + #:print? #f) + (test fixed (map fix generated))) + (test (parameterize ([generation-decisions + (decisions #:num (list (λ _ 0)))]) + (check-reduction-relation + (reduction-relation L (--> number number)) + (curry = 0) + #:prepare add1 + #:print? #f)) + (counterexample 1)) + (test (raised-exn-msg + exn:fail? + (check-reduction-relation + (reduction-relation L (--> 0 0)) + (λ (_) #t) + #:prepare (λ (_) (error 'fixer)) + #:print? #f)) + #rx"fixing 0") + (test (raised-exn-msg + exn:fail:contract:blame? + (check-reduction-relation + (reduction-relation L (--> 0 0)) + void + #:prepare (λ () 0))) + #rx"rg-test broke the contract") + (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))]) (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) #rx"check-reduction-relation:.*no counterexamples") @@ -937,6 +1013,46 @@ #f)) #t) + (let ([generated '()] + [fixed '()] + [fix add1]) + (define-metafunction empty + [(f number) number]) + (check-metafunction + f (λ (n) (set! fixed (cons (car n) fixed))) + #:prepare (λ (n) + (set! generated (cons (car n) generated)) + (list (fix (car n)))) + #:attempts 10 + #:print? #f) + (test fixed (map fix generated))) + (test (parameterize ([generation-decisions + (decisions #:num (list (λ _ 0)))]) + (define-metafunction empty + [(f number) number]) + (check-metafunction + f (compose (curry = 0) car) + #:prepare (compose list add1 car) + #:print? #f)) + (counterexample '(1))) + (test (let () + (define-metafunction empty + [(f 0) 0]) + (raised-exn-msg + exn:fail? + (check-metafunction + f (λ (_) #t) + #:prepare (λ (_) (error 'fixer)) + #:print? #f))) + #rx"fixing \\(0\\)") + (test (raised-exn-msg + exn:fail? + (let () + (define-metafunction empty + [(f 0) 0]) + (check-metafunction f void #:prepare car #:print? #f))) + #rx"rg-test broke the contract") + (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+")