diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 9f64f3950f..5ab55a5562 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -1997,7 +1997,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 @#,ttpattern #:enum) (code:line language #:satisfying (judgment-form-id @#,ttpattern ...)) (code:line language #:satisfying @@ -2028,12 +2028,15 @@ 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 randomly generates terms that match + In this case, @racket[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 @#,ttpattern #:enum]: + In this case, @racket[redex-check] picks a random natural number + and then uses that to index into an enumeration of @racket[_pattern]. + If the enumeration is finite, @racket[redex-check] picks a natural number + uniformly at random; if it isn't, @racket[redex-check] uses a geometric + distribution to pick the number of bits in the index and then picks a + number uniformly at random with that number of bits.} @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/HISTORY.txt b/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt index 7df8cc34cb..fc2615d350 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt +++ b/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt @@ -4,6 +4,8 @@ v6.1 * added default-equiv + * changed the meaning of the redex-check #:enum keyword + (based on statistics help from Neil Toronto) v6.0 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 390d4f9619..b1f97906e3 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -21,7 +21,8 @@ "rewrite-side-conditions.rkt" "term-fn.rkt" "keyword-macros.rkt") - math/base) + math/base + math/distributions) (define-for-syntax (metafunc name) (and (identifier? name) @@ -122,8 +123,8 @@ (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 #:enum property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #t #'kw-args)] [(form lang pat property . kw-args) (redex-check/pat stx #'form #'lang #'pat #'property #f #'kw-args)])) @@ -209,7 +210,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 enum-bound-e kw-args) +(define-for-syntax (redex-check/pat orig-stx form lang pat property enum? kw-args) (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...)) (rewrite-side-conditions/check-errs lang @@ -236,12 +237,11 @@ (parameterize ([attempt->size #,size-stx]) #,(cond [source-stx - (when enum-bound-e + (when enum? (raise-syntax-error #f "#:enum cannot be used with the #:source keyword" - orig-stx - enum-bound-e)) + orig-stx)) #`(let-values ([(metafunc/red-rel num-cases) #,(cond [(metafunc source-stx) => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))] @@ -262,9 +262,9 @@ #:term-match term-match))] [else (cond - [enum-bound-e + [enum? #`(check-one - (ith-generator #,lang `pattern #,enum-bound-e) + (ith-generator #,lang `pattern) property att ret (and print? show) (or fix (λ (x) x)) term-match keep-going?)] [else @@ -273,16 +273,31 @@ property att ret (and print? show) fix (and fix term-match) keep-going?)])]))))))) -(define (ith-generator lang pat orig-bound) +(define (ith-generator lang pat) (define enum-lang (compiled-lang-enum-table lang)) (define enum (pat-enumerator enum-lang pat)) (define the-size (enum-size enum)) - (define bound (if (equal? the-size +inf.0) - orig-bound - (min orig-bound the-size))) - (λ (_size _attempt _retries) - (values (enum-ith enum (random-natural bound)) - 'ignored))) + (cond + [(equal? the-size +inf.0) + (λ (_size _attempt _retries) + (values (enum-ith enum (pick-an-index)) + 'ignored))] + [else + (λ (_size _attempt _retries) + (values (enum-ith enum (random-natural the-size)) + 'ignored))])) + +(define (pick-an-index) + (max (random-natural/no-mean 0.01) + (random-natural/no-mean 0.01) + (random-natural/no-mean 0.01))) + +;; (: random-natural/no-mean (-> Real Natural)) +(define (random-natural/no-mean prob-zero) + (define n (exact-floor (sample (geometric-dist prob-zero)))) + (define m1 (expt 2 n)) + (define m0 (quotient m1 2)) + (random-integer m0 m1)) (define-for-syntax (parse-redex-check-kw-args kw-args orig-stx form-name) (apply values 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 3e1404f8f7..e25bc10a45 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt @@ -894,7 +894,7 @@ (test (let ([checked 0]) - (redex-check lang n #:enum 100 (set! checked (add1 checked)) + (redex-check lang n #:enum (set! checked (add1 checked)) #:print? #f #:attempts 10) checked)