From f8ea4f46ef7bfe3a5410b6bdc8b0ae327d91df53 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Thu, 14 Nov 2013 18:28:21 -0600 Subject: [PATCH] use the enumerator in a new option to redex-check --- .../redex-doc/redex/scribblings/ref.scrbl | 9 +++- .../redex-lib/redex/private/generate-term.rkt | 48 ++++++++++++++----- .../redex-test/redex/tests/rg-test.rkt | 10 +++- 3 files changed, 53 insertions(+), 14 deletions(-) diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 3bd4815e0e..8f9a3c1d63 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -1841,6 +1841,7 @@ repeating as necessary. The optional keyword argument @racket[retries-expr] @defform/subs[(redex-check template property-expr kw-arg ...) ([template (code:line language @#,ttpattern) + (code:line language @#,ttpattern #:enum enum-expr) (code:line language #:satisfying (judgment-form-id @#,ttpattern ...)) (code:line language #:satisfying @@ -1871,8 +1872,12 @@ using the @racket[match-bindings] produced by @racket[match]ing how @math{t} is generated: @itemlist[ @item{@racket[language @#,ttpattern]: - In this case, redex-check generates terms that match - @racket[pattern].} + In this case, redex-check randomly generates terms that match + @racket[_pattern].} + @item{@racket[language @#,ttpattern]: + In this case, redex-check uniformly at random picks a number less + than the value of @racket[enum-expr] (which must be a non-negative integer) + and then uses that to index into an enumeration of @racket[_pattern].} @item{@racket[language #:satisfying (judgment-form-id @#,ttpattern ...)]: Generates terms that match @racket[pattern] and satisfy the judgment form.} diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt index 7731ca0170..8579f70fe2 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -20,7 +20,8 @@ setup/path-to-relative "rewrite-side-conditions.rkt" "term-fn.rkt" - "keyword-macros.rkt")) + "keyword-macros.rkt") + math/base) (define-for-syntax (metafunc name) (and (identifier? name) @@ -91,6 +92,7 @@ (define-syntax (redex-check stx) (define valid-kws (list* '#:satisfying + '#:enum (map car (list attempts-keyword source-keyword retries-keyword @@ -120,8 +122,10 @@ (redex-check/jf stx #'form #'lang #'jform-id #'pats #'property #'kw-args)] [(form lang #:satisfying . rest) (raise-syntax-error 'redex-check "#:satisfying expected judgment form or metafunction syntax followed by a property" stx #'rest)] + [(form lang pat #:enum biggest-e property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #'biggest-e #'kw-args)] [(form lang pat property . kw-args) - (redex-check/pat stx #'form #'lang #'pat #'property #'kw-args)])) + (redex-check/pat stx #'form #'lang #'pat #'property #f #'kw-args)])) (define-struct gen-fail ()) @@ -199,7 +203,7 @@ property #,attempts-stx 0 (and #,print?-stx show) #,fix-stx term-match #,keep-going-stx))))))) -(define-for-syntax (redex-check/pat orig-stx form lang pat property kw-args) +(define-for-syntax (redex-check/pat orig-stx form lang pat property enum-bound-e kw-args) (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...)) (rewrite-side-conditions/check-errs lang @@ -222,8 +226,15 @@ [else (redex-error 'redex-check "~s does not match ~s" generated '#,pat)]))]) syncheck-exp (parameterize ([attempt->size #,size-stx]) - #,(if source-stx - #`(let-values ([(metafunc/red-rel num-cases) + #,(cond + [source-stx + (when enum-bound-e + (raise-syntax-error + #f + "#:enum cannot be used with the #:source keyword" + orig-stx + enum-bound-e)) + #`(let-values ([(metafunc/red-rel num-cases) #,(cond [(metafunc source-stx) => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))] [else @@ -240,11 +251,26 @@ (and print? show) fix keep-going? - #:term-match term-match)) - #`(check-one - #,(term-generator lang #'pattern 'redex-check) - property att ret (and print? show) fix (and fix term-match) - keep-going?)))))))) + #:term-match term-match))] + [else + (cond + [enum-bound-e + #`(check-one + (ith-generator #,lang `pattern #,enum-bound-e) + property att ret (and print? show) (or fix (λ (x) x)) term-match + keep-going?)] + [else + #`(check-one + #,(term-generator lang #'pattern 'redex-check) + property att ret (and print? show) fix (and fix term-match) + keep-going?)])]))))))) + +(define (ith-generator lang pat bound) + (define enum-lang (compiled-lang-enum-table lang)) + (define enum (pat-enumerator enum-lang pat)) + (λ (_size _attempt _retries) + (values (enum-ith enum (random-natural bound)) + 'ignored))) (define-for-syntax (parse-redex-check-kw-args kw-args orig-stx form-name) (apply values @@ -557,7 +583,7 @@ (raise-argument-error 'generate-term "exact-nonnegative-integer?" i)) - (enum-ith enum i))) + (enum-ith enum i))) (define-syntax (generate-term/mf stx) (syntax-case stx () diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt index 87cabf9f6a..374962b720 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt @@ -888,7 +888,15 @@ (test-gen-fail (--> (side-condition any #f) any impossible) - #rx"^redex-check: unable to generate LHS of impossible in 42")))) + #rx"^redex-check: unable to generate LHS of impossible in 42"))) + + + (test (let ([checked 0]) + (redex-check lang n #:enum 100 (set! checked (add1 checked)) + #:print? #f + #:attempts 10) + checked) + 10)) ;; check-reduction-relation (let ()