From 89ef6f831e9d30fad845f807ec258cb380d7fdcb Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Tue, 25 Mar 2014 21:40:36 -0500 Subject: [PATCH] adjust #:enum arg to redex-check to be back like 6.0, add #:uniform-at-random argument and #:in-order argument --- .../redex-doc/redex/scribblings/ref.scrbl | 18 +++-- pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt | 2 +- .../redex-lib/redex/private/generate-term.rkt | 68 +++++++++++++++---- .../redex-test/redex/tests/rg-test.rkt | 19 +++++- 4 files changed, 85 insertions(+), 22 deletions(-) diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 5ab55a5562..40a11ce555 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -2026,17 +2026,23 @@ on @racket[template] and then evaluating @racket[property-expr] using the @racket[match-bindings] produced by @racket[match]ing @math{t} against @racket[pattern]. The form of @racket[template] controls how @math{t} is generated: -@itemlist[ - @item{@racket[language @#,ttpattern]: +@itemlist[@item{@racket[language @#,ttpattern]: In this case, @racket[redex-check] randomly generates terms that match @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]. + @item{@racket[language @#,ttpattern #:in-order]: + In this case, @racket[redex-check] uses an enumeration + of @racket[_pattern], checking each @math{t} one at a time} + @item{@racket[language @#,ttpattern #:uniform-at-random p-value]: + 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 + distribution with @racket[p-value] as its probability of zero + 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 @#,ttpattern #:enum bound]: + This is similar to @racket[#:uniform-at-random], except + that Redex always picks a random natural number less than @racket[bound] + to index into the enumeration} @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 fc2615d350..2e7b0e2b75 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt +++ b/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt @@ -4,7 +4,7 @@ v6.1 * added default-equiv - * changed the meaning of the redex-check #:enum keyword + * added the #:enum-p 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 95050728cf..568300acf3 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -94,6 +94,8 @@ (define valid-kws (list* '#:satisfying '#:enum + '#:uniform-at-random + '#:in-order (map car (list attempts-keyword source-keyword retries-keyword @@ -123,10 +125,14 @@ (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 property . kw-args) - (redex-check/pat stx #'form #'lang #'pat #'property #t #'kw-args)] + [(form lang pat #:enum biggest-e property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #'biggest-e #f #f #'kw-args)] + [(form lang pat #:uniform-at-random p-value property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #f #'p-value #f #'kw-args)] + [(form lang pat #:in-order property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #f #f #t #'kw-args)] [(form lang pat property . kw-args) - (redex-check/pat stx #'form #'lang #'pat #'property #f #'kw-args)])) + (redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #'kw-args)])) (define-struct gen-fail ()) @@ -210,7 +216,9 @@ 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? kw-args) +(define-for-syntax (redex-check/pat orig-stx form lang pat property + enum-bound-e enum-p-value in-order? + kw-args) (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...)) (rewrite-side-conditions/check-errs lang @@ -237,11 +245,21 @@ (parameterize ([attempt->size #,size-stx]) #,(cond [source-stx - (when enum? + (when enum-bound-e (raise-syntax-error #f "#:enum cannot be used with the #:source keyword" orig-stx)) + (when enum-p-value + (raise-syntax-error + #f + "#:uniform-at-random cannot be used with the #:source keyword" + orig-stx)) + (when in-order? + (raise-syntax-error + #f + "#:in-order cannot be used with the #:source keyword" + orig-stx)) #`(let-values ([(metafunc/red-rel num-cases) #,(cond [(metafunc source-stx) => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))] @@ -262,9 +280,14 @@ #:term-match term-match))] [else (cond - [enum? + [in-order? #`(check-one - (ith-generator #,lang `pattern) + (in-order-generator #,lang `pattern) + property att ret (and print? show) (or fix (λ (x) x)) term-match + keep-going?)] + [(or enum-bound-e enum-p-value) + #`(check-one + (ith-generator #,lang `pattern #,enum-bound-e #,enum-p-value) property att ret (and print? show) (or fix (λ (x) x)) term-match keep-going?)] [else @@ -273,19 +296,38 @@ property att ret (and print? show) fix (and fix term-match) keep-going?)])]))))))) -(define (ith-generator lang pat) +(define (ith-generator lang pat enum-bound enum-p-value) (define enum-lang (compiled-lang-enum-table lang)) (define enum (pat-enumerator enum-lang pat)) (define the-size (enum-size enum)) (cond - [(equal? the-size +inf.0) + [enum-bound + (define bound (if (equal? the-size +inf.0) + enum-bound + (min enum-bound the-size))) (λ (_size _attempt _retries) - (values (enum-ith enum (pick-an-index)) + (values (enum-ith enum (random-natural bound)) 'ignored))] [else - (λ (_size _attempt _retries) - (values (enum-ith enum (random-natural the-size)) - 'ignored))])) + (cond + [(equal? the-size +inf.0) + (λ (_size _attempt _retries) + (values (enum-ith enum (pick-an-index enum-p-value)) + 'ignored))] + [else + (λ (_size _attempt _retries) + (values (enum-ith enum (random-natural the-size)) + 'ignored))])])) + +(define (in-order-generator lang pat) + (define enum-lang (compiled-lang-enum-table lang)) + (define enum (pat-enumerator enum-lang pat)) + (define the-size (enum-size enum)) + (λ (_size _attempt _retries) + (values (enum-ith enum (if (= +inf.0 the-size) + (- _attempt 1) + (modulo (- _attempt 1) the-size))) + 'ignored))) ;; pick-an-index : ([0,1] -> Nat) ∩ (-> Nat) (define (pick-an-index [prob-of-zero 0.01]) 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 e25bc10a45..df42730f18 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt @@ -894,11 +894,26 @@ (test (let ([checked 0]) - (redex-check lang n #:enum (set! checked (add1 checked)) + (redex-check lang n #:enum 100 (set! checked (add1 checked)) #:print? #f #:attempts 10) checked) - 10)) + 10) + + (test (let ([checked 0]) + (redex-check lang n #:uniform-at-random 0.1 (set! checked (add1 checked)) + #:print? #f + #:attempts 10) + checked) + 10) + + (test (let ([checked '()]) + (redex-check lang natural #:in-order + (set! checked (cons (term natural) checked)) + #:print? #f + #:attempts 5) + checked) + '(4 3 2 1 0))) ;; check-reduction-relation (let ()