From b86e4473f00656040c93be6a3e8145f306f38d4d Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Thu, 29 Jan 2009 00:41:30 +0000 Subject: [PATCH] Changed redex-check's #:source keyword to always generate from the LHSs of the metafunction/relation. svn: r13310 --- collects/redex/private/rg-test.ss | 79 +++++++++---------- collects/redex/private/rg.ss | 122 +++++++++++++----------------- collects/redex/redex.scrbl | 46 +++++++---- 3 files changed, 127 insertions(+), 120 deletions(-) diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss index 761f2a5ec0..2d8554c3f0 100644 --- a/collects/redex/private/rg-test.ss +++ b/collects/redex/private/rg-test.ss @@ -574,54 +574,57 @@ (test m "error: pred-raised") (test (get-output-string p) #rx"checking 5 raises.*\n$") (close-output-port p)) - (test (parameterize ([check-randomness (make-random 0 0)]) - (output - (λ () - (redex-check lang n (eq? 42 (term n)) - #:attempts 1 - #:source (reduction-relation lang (--> 42 x)))))) - "") + (test (output (λ () - (parameterize ([check-randomness (make-random 0 0)]) - (redex-check lang n (eq? 42 (term n)) - #:attempts 1 - #:source (reduction-relation lang (--> 0 x z)))))) - "counterexample found (z) after 1 attempts:\n0\n") - (test (output - (λ () - (parameterize ([check-randomness (make-random 1)]) - (redex-check lang d (eq? 42 (term n)) - #:attempts 1 - #:source (reduction-relation lang (--> 0 x z)))))) - "counterexample found after 1 attempts:\n5\n") - (test (let ([r (reduction-relation lang (--> 0 x z))]) - (output + (redex-check lang n (eq? 42 (term n)) + #:attempts 1 + #:source (reduction-relation + lang + (--> 42 dontcare) + (--> 0 dontcare z))))) + "counterexample found after 1 attempts with z:\n0\n") + + (let ([generated null]) + (test (output (λ () - (redex-check lang n (number? (term n)) - #:attempts 10 - #:source r)))) - "") + (redex-check lang n (set! generated (cons (term n) generated)) + #:attempts 5 + #:source (reduction-relation + lang + (--> 1 dontcare) + (--> 2 dontcare))))) + "") + (test generated '(2 2 1 1))) + (let () (define-metafunction lang - [(mf 0) 0] - [(mf 42) 0]) - (test (parameterize ([check-randomness (make-random 0 1)]) - (output - (λ () - (redex-check lang (n) (eq? 42 (term n)) - #:attempts 1 - #:source mf)))) - "")) + [(mf 42) dontcare] + [(mf 0) dontcare]) + (test (output + (λ () + (redex-check lang (n) (eq? 42 (term n)) + #:attempts 1 + #:source mf))) + "counterexample found after 1 attempts with clause #2:\n(0)\n")) + (let () - (define-language L) - (test (with-handlers ([exn:fail? exn-message]) - (redex-check lang any #t #:source (reduction-relation L (--> 1 1)))) - #rx"language for secondary source")) + (define-metafunction lang + [(mf d e) dontcare]) + (test (output + (λ () + (redex-check lang (number_1 number_2) + (and (= (term number_1) 5) + (= (term number_2) 4)) + #:attempts 1 + #:source mf))) + "")) + (let () (test (with-handlers ([exn:fail? exn-message]) (redex-check lang n #t #:source (reduction-relation lang (--> x 1)))) #rx"x does not match n")) + (let ([stx-err (λ (stx) (with-handlers ([exn:fail:syntax? exn-message]) diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss index 56fe698ed9..3b24973b45 100644 --- a/collects/redex/private/rg.ss +++ b/collects/redex/private/rg.ss @@ -669,8 +669,6 @@ To do a better job of not generating programs with free variables, [(_ lang pat size) (syntax/loc stx (generate-term lang pat size #:attempt 1))])) -(define check-randomness (make-parameter random)) - (define-syntax (redex-check stx) (syntax-case stx () [(_ lang pat property . kw-args) @@ -693,57 +691,48 @@ To do a better job of not generating programs with free variables, (with-syntax ([(name ...) names] [(name/ellipses ...) names/ellipses] [attempts (or attempts-stx #'default-check-attempts)]) - (quasisyntax/loc stx - (let ([att attempts]) - (assert-nat 'redex-check att) - (check-property - (cons (list #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check) #f) - (let ([lang-gen (generate lang random-decisions@)]) - #,(if (not source-stx) - #'null - #`(let-values - ([(pats srcs src-lang) - #,(cond [(and (identifier? source-stx) (metafunc source-stx)) - => - (λ (m) #`(values (metafunc-proc-lhs-pats #,m) - (metafunc-srcs #,m) - (metafunc-proc-lang #,m)))] - [else - #`(let ([r #,source-stx]) - (unless (reduction-relation? r) - (raise-type-error 'redex-check "reduction-relation" r)) - (values - (map rewrite-proc-lhs (reduction-relation-make-procs r)) - (reduction-relation-srcs r) - (reduction-relation-lang r)))])]) - (unless (eq? src-lang lang) - (error 'redex-check "language for secondary source must match primary pattern's language")) - (zip (map lang-gen pats) srcs))))) - #,(and source-stx #'(test-match lang pat)) - (λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat)) - (λ (_ bindings) - (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) - property)) - att - (λ (term attempt source port) - (fprintf port "counterexample found~aafter ~a attempts:\n" - (if source (format " (~a) " source) " ") attempt) - (pretty-print term port)) - (check-randomness)) - (void)))))])) + (with-syntax ([property (syntax + (λ (_ bindings) + (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) + property)))]) + (quasisyntax/loc stx + (let ([att attempts]) + (assert-nat 'redex-check att) + (unsyntax + (if source-stx + #`(let-values + ([(pats srcs src-lang) + #,(cond [(and (identifier? source-stx) (metafunc source-stx)) + => + (λ (m) #`(values (metafunc-proc-lhs-pats #,m) + (metafunc-srcs #,m) + (metafunc-proc-lang #,m)))] + [else + #`(let ([r #,source-stx]) + (unless (reduction-relation? r) + (raise-type-error 'redex-check "reduction-relation" r)) + (values + (map rewrite-proc-lhs (reduction-relation-make-procs r)) + (reduction-relation-srcs r) + (reduction-relation-lang r)))])]) + (check-property-many + lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) + (test-match lang pat) + (λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat)))) + #`(check-property + #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check) + property att))) + (void))))))])) -(define (check-property gens-srcs match match-fail property attempts display [random random]) +(define (check-property generator property attempts + #:source [source #f] + #:match [match #f] + #:match-fail [match-fail #f]) (let loop ([remaining attempts]) (if (zero? remaining) #t (let ([attempt (add1 (- attempts remaining))]) - (let*-values ([(generator source) - (apply values - (if (and (not (null? (cdr gens-srcs))) (zero? (random 10))) - (pick-from-list (cdr gens-srcs) random) - (car gens-srcs)))] - [(term bindings) - (generator (attempt->size attempt) attempt)]) + (let-values ([(term bindings) (generator (attempt->size attempt) attempt)]) (if (andmap (λ (bindings) (with-handlers ([exn:fail? (λ (exn) (fprintf (current-error-port) @@ -757,7 +746,11 @@ To do a better job of not generating programs with free variables, [else (list bindings)])) (loop (sub1 remaining)) (begin - (display term attempt source (current-output-port)) + (fprintf (current-output-port) + "counterexample found after ~a attempts~a:\n" + attempt + (if source (format " with ~a" source) "")) + (pretty-print term (current-output-port)) #f))))))) (define-syntax (check-metafunction-contract stx) @@ -775,32 +768,23 @@ To do a better job of not generating programs with free variables, [att attempts]) (assert-nat 'check-metafunction-contract att) (check-property - (list (list ((generate lang decisions@) (if dom dom '(any (... ...)))) #f)) - #f - #f + ((generate lang decisions@) (if dom dom '(any (... ...)))) (λ (t _) (with-handlers ([exn:fail:redex? (λ (_) #f)]) (begin (term (name ,@t)) #t))) - att - (λ (term attempt _ port) - (fprintf port "counterexample found after ~a attempts:\n" attempt) - (pretty-print term port))) + att) (void))))])) -(define (check-property-many lang pats srcs prop decisions@ attempts) +(define (check-property-many lang pats srcs prop decisions@ attempts [match #f] [match-fail #f]) (let ([lang-gen (generate lang decisions@)]) (for/and ([pat pats] [src srcs]) (check-property - (let ([gen (lang-gen pat)]) - (list (list (λ (size attempt) (gen size attempt)) src))) - #f - #f - (λ (term _) (prop term)) + (lang-gen pat) + prop attempts - (λ (term attempt source port) - (fprintf port "counterexample found after ~a attempts with ~a:\n" - attempt source) - (pretty-print term port)))) + #:source src + #:match match + #:match-fail match-fail)) (void))) (define (metafunc-srcs m) @@ -820,7 +804,7 @@ To do a better job of not generating programs with free variables, (metafunc-proc-lang m) (metafunc-proc-lhs-pats m) (metafunc-srcs m) - property + (λ (term _) (property term)) (generation-decisions) att))))])) @@ -836,7 +820,7 @@ To do a better job of not generating programs with free variables, (reduction-relation-lang relation) (map rewrite-proc-lhs (reduction-relation-make-procs relation)) (reduction-relation-srcs relation) - property + (λ (term _) (property term)) decisions@ attempts)) @@ -868,7 +852,7 @@ To do a better job of not generating programs with free variables, (struct-out ellipsis) (struct-out mismatch) (struct-out class) (struct-out binder) check-metafunction-contract prepare-lang pick-number parse-language check-reduction-relation - preferred-production-threshold check-metafunction check-randomness + preferred-production-threshold check-metafunction generation-decisions pick-preferred-productions) (provide/contract diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 8f93b17c3c..c79e650b06 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1058,6 +1058,16 @@ these free @pattech[term]-variables by generating random terms matching @scheme[pattern] and extracting the sub-terms bound by the @pattech[names] and non-terminals in @scheme[pattern]. +@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[100]) +random terms in its search. The size and complexity of terms it generates +gradually increases with each failed attempt. + +When passed a metafunction or reduction relation via the optional @scheme[#:source] +argument, @scheme[redex-check] distributes its attempts across the left-hand sides +of that metafunction/relation by using those patterns, rather than @scheme[pattern], +as the basis of its generation. It is an error if any left-hand side generates a +term that does not match @scheme[pattern].} + @examples[ #:eval redex-eval (define-language empty-lang) @@ -1081,27 +1091,37 @@ these free @pattech[term]-variables by generating random terms matching (term (number_2 ...)))) (append (reverse (term (number_2 ...))) (reverse (term (number_1 ...))))) - #:attempts 200)] - -@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[100]) -random terms in its search. The size and complexity of terms it generates -gradually increases with each failed attempt. - -When the optional @scheme[#:source] argument is present, @scheme[redex-check] -generates @math{10%} of its terms by randomly choosing a pattern from the -left-hand sides the definition of the supplied metafunction or relation. -@scheme[redex-check] raises an exception if a term generated from an alternate -pattern does not match the @scheme[pattern].} + #:attempts 200) + + (let ([R (reduction-relation + empty-lang + (--> (Σ) 0) + (--> (Σ number) number) + (--> (Σ number_1 number_2 number_3 ...) + (Σ ,(+ (term number_1) (term number_2)) + number_3 ...)))]) + (redex-check + empty-lang + (Σ number ...) + (printf "~s\n" (term (number ...))) + #:attempts 3 + #:source R))] @defproc[(check-reduction-relation [relation reduction-relation?] [property (-> any/c any/c)] [#:attempts attempts natural-number/c 100]) void?]{ -Tests a @scheme[relation] as follows: for each case of @scheme[relation], +Tests @scheme[relation] as follows: for each case of @scheme[relation], @scheme[check-reduction-relation] generates @scheme[attempts] random terms that match that case's left-hand side and applies @scheme[property] -to each random term.} +to each random term. + +This function provides a more convenient notation for +@schemeblock[(redex-check L any (property (term any)) + #:attempts (* n attempts) + #:source relation)] +when @scheme[relation] is a relation on @scheme[L] and has @scheme[n] rules.} @defform*[[(check-metafunction metafunction property) (check-metafunction metafunction property #:attempts attempts)]