From 1e910fcfbc744e1c5bbf2889899058df9b3d0a7f Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 17 Mar 2013 20:35:48 -0500 Subject: [PATCH] make check-metafunction and check-reduction-relation pay attention to the contract/#:domain spec closes PR 13616 --- collects/redex/private/generate-term.rkt | 119 +++++++++++++---------- collects/redex/tests/rg-test.rkt | 25 +++++ doc/release-notes/redex/HISTORY.txt | 7 ++ 3 files changed, 97 insertions(+), 54 deletions(-) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index 3a4f31a094..ed180a31e8 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -159,7 +159,8 @@ (define (check generator property attempts retries show #:source [source #f] #:term-fix [term-fix #f] - #:term-match [term-match #f]) + #:term-match [term-match #f] + #:skip-term? [skip-term? (λ (x) #f)]) (let loop ([remaining attempts]) (if (zero? remaining) #t @@ -180,62 +181,72 @@ 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-write term (current-output-port))) - (make-counterexample term))))))))) + (cond + [(skip-term? term) (loop (- remaining 1))] + [else + (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-write term (current-output-port))) + (make-counterexample term)))]))))))) (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) - (values (map (λ (case) ((metafunc-case-lhs+ case) lang)) - (metafunc-proc-cases mf/rr)) - (metafunction-srcs mf/rr))] - [(reduction-relation? mf/rr) - (values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr)) - (reduction-relation-srcs mf/rr))])]) - (let loop ([pats pats] [srcs srcs]) - (if (and (null? pats) (null? srcs)) - (if show - (show - (format "no counterexamples in ~a (with each clause)\n" - (format-attempts attempts))) - #t) - (let ([c (with-handlers ([exn:fail:redex:generation-failure? - ; Produce an error message that blames the LHS as a whole. - (λ (_) - (raise-gen-fail what (format "LHS of ~a" (car srcs)) retries))]) - (check - (lang-gen (car pats)) - prop - attempts - retries - show - #:source (car srcs) - #:term-match term-match - #:term-fix term-fix))]) - (if (counterexample? c) - (unless show c) - (loop (cdr pats) (cdr srcs))))))))) + (define lang-gen (compile lang what)) + (define-values (pats srcs skip-term?) + (cond [(metafunc-proc? mf/rr) + (values (map (λ (case) ((metafunc-case-lhs+ case) lang)) + (metafunc-proc-cases mf/rr)) + (metafunction-srcs mf/rr) + (compose not (metafunc-proc-in-dom? mf/rr)))] + [(reduction-relation? mf/rr) + (values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr)) + (reduction-relation-srcs mf/rr) + (let ([pat (compile-pattern (reduction-relation-lang mf/rr) + (reduction-relation-domain-pat mf/rr) + #f)]) + (λ (x) (not (match-pattern? pat x)))))])) + + (let loop ([pats pats] [srcs srcs]) + (if (and (null? pats) (null? srcs)) + (if show + (show + (format "no counterexamples in ~a (with each clause)\n" + (format-attempts attempts))) + #t) + (let ([c (with-handlers ([exn:fail:redex:generation-failure? + ; Produce an error message that blames the LHS as a whole. + (λ (_) + (raise-gen-fail what (format "LHS of ~a" (car srcs)) retries))]) + (check + (lang-gen (car pats)) + prop + attempts + retries + show + #:skip-term? skip-term? + #:source (car srcs) + #:term-match term-match + #:term-fix term-fix))]) + (if (counterexample? c) + (unless show c) + (loop (cdr pats) (cdr srcs))))))) (define-syntax (check-metafunction stx) (syntax-case stx () diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index 3f7a5fa107..e58bd70e23 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -1048,6 +1048,17 @@ #:attempts 1)))) #rx"no counterexamples")) + ;; just check that this doesn't raise an errors. + (let () + (define-language empty) + (define red (reduction-relation + empty + #:domain 1 + (--> any any))) + (check-reduction-relation + red + (λ (x) (apply-reduction-relation red x)))) + (let ([U (reduction-relation L (--> (side-condition any #f) any))]) (test (raised-exn-msg exn:fail:redex:generation-failure? @@ -1229,6 +1240,20 @@ (check-metafunction n (λ (_) #t) #:retries 42)) #rx"check-metafunction: unable .* in 42") + + (let () + (define-metafunction empty + mf : 1 -> 1 + [(mf any) any]) + + ;; just make sure no errors + (test (begin + (check-metafunction + mf + (λ (args) (term (mf ,@args)))) + 42) + 42)) + (let () (define-metafunction empty bogo : any -> any) diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt index a037257f10..44d12f18ae 100644 --- a/doc/release-notes/redex/HISTORY.txt +++ b/doc/release-notes/redex/HISTORY.txt @@ -4,6 +4,13 @@ v5.3.4 have overlapping non-terminals; in that case the productions are combined + * Adjust check-metafunction and check-reduction-relation so that + they skip over randomly generated terms that don't match the + contract spec (or #:domain spec). This means that when there is a + case in the metafunction (or reduction-relation) whose nominal + pattern is more general than the contract would allow, that those + terms are discarded instead of used as inputs to the predicate. + v5.3.3 No changes