From 494f32084addbca15f59fe0e97740763c9cb25a7 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 26 Mar 2014 00:33:38 -0500 Subject: [PATCH] change redex-check's default strategy to do both enumeration and random generation in a manner supported by our study --- .../redex-doc/redex/scribblings/ref.scrbl | 11 +++- .../redex-lib/redex/private/generate-term.rkt | 62 +++++++++++++++++-- .../redex-test/redex/tests/rg-test.rkt | 9 ++- 3 files changed, 73 insertions(+), 9 deletions(-) diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 40a11ce555..1dda48423d 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -2027,8 +2027,15 @@ 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]: - In this case, @racket[redex-check] randomly generates terms that match - @racket[_pattern].} + In this case, @racket[redex-check] uses an ad hoc strategy for + generating @racket[_pattern]. For the first 10 seconds, it uses + in-order enumeration to pick terms. After that, it + alternates back and forth between in-order enumeration + and the ad hoc random generator. After the 10 minute mark, + it switches over to using just the ad hoc random generator.} + @item{@racket[language @#,ttpattern #:ad-hoc]: + In this case, @racket[redex-check] uses an ad hoc random generator + to generate terms that match @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} 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 568300acf3..85baf6b52c 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -93,6 +93,7 @@ (define-syntax (redex-check stx) (define valid-kws (list* '#:satisfying + '#:ad-hoc '#:enum '#:uniform-at-random '#:in-order @@ -126,13 +127,15 @@ [(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 #f #f #'kw-args)] + (redex-check/pat stx #'form #'lang #'pat #'property #'biggest-e #f #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)] + (redex-check/pat stx #'form #'lang #'pat #'property #f #'p-value #f #f #'kw-args)] [(form lang pat #:in-order property . kw-args) - (redex-check/pat stx #'form #'lang #'pat #'property #f #f #t #'kw-args)] + (redex-check/pat stx #'form #'lang #'pat #'property #f #f #t #f #'kw-args)] + [(form lang pat #:ad-hoc property . kw-args) + (redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #t #'kw-args)] [(form lang pat property . kw-args) - (redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #'kw-args)])) + (redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #f #'kw-args)])) (define-struct gen-fail ()) @@ -217,7 +220,7 @@ #,keep-going-stx))))))) (define-for-syntax (redex-check/pat orig-stx form lang pat property - enum-bound-e enum-p-value in-order? + enum-bound-e enum-p-value in-order? ad-hoc? kw-args) (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...)) (rewrite-side-conditions/check-errs @@ -290,12 +293,59 @@ (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 + [ad-hoc? #`(check-one #,(term-generator lang #'pattern 'redex-check) property att ret (and print? show) fix (and fix term-match) + keep-going?)] + [else + #`(check-one + (default-generator #,lang `pattern) + property att ret (and print? show) (or fix (λ (x) x)) term-match keep-going?)])]))))))) +(define (default-generator lang pat) + (define ad-hoc-generator ((compile lang 'redex-check) pat)) + (define enum (with-handlers ([exn:fail? (λ (x) #f)]) + ;; would be better if the pat-enumerator were to + ;; return something to indicate failure instead of + ;; raising an exception so that bugs in there wouldn't + ;; turn into #f here + (pat-enumerator (compiled-lang-enum-table lang) pat))) + (cond + [enum + (define in-bounds (if (= +inf.0 (enum-size enum)) + (λ (x) x) + (λ (x) (modulo x (enum-size enum))))) + (define start-time (current-inexact-milliseconds)) + (define interleave-start-attempt #f) + (define interleave-time (+ start-time (* 1000 10))) ;; 10 seconds later + (define pure-random-start-attempt #f) + (define pure-random-time (+ start-time (* 1000 60 10))) ;; 10 minutes later + (λ (_size _attempt _retries) + (define now (current-inexact-milliseconds)) + (cond + [(<= now interleave-time) + (values (enum-ith enum (in-bounds (- _attempt 1))) 'ignored)] + [(<= now pure-random-time) + (unless interleave-start-attempt (set! interleave-start-attempt _attempt)) + (define interleave-attempt (- _attempt interleave-start-attempt)) + (cond + [(odd? interleave-attempt) + (ad-hoc-generator _size (/ (- interleave-attempt 1) 2) _retries)] + [else + (define enum-id (in-bounds (+ interleave-start-attempt (/ interleave-attempt 2) -1))) + (values (enum-ith enum enum-id) 'ignored)])] + [else + (unless pure-random-start-attempt (set! pure-random-start-attempt _attempt)) + (ad-hoc-generator _size + (+ (- _attempt pure-random-start-attempt) + (quotient (- pure-random-start-attempt pure-random-start-attempt) + 2)) + _retries)]))] + [else + ad-hoc-generator])) + (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)) 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 df42730f18..82a47cc827 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt @@ -803,7 +803,7 @@ (test (let/ec k (parameterize ([generation-decisions (decisions #:nt (list (λ _ (k #t))))]) - (redex-check lang d #t #:attempts 1 #:print? #f #:attempt-size add1) + (redex-check lang d #:ad-hoc #t #:attempts 1 #:print? #f #:attempt-size add1) #f)) #t) @@ -893,6 +893,13 @@ #rx"^redex-check: unable to generate LHS of impossible in 42"))) + (test (let ([checked 0]) + (redex-check lang n #:ad-hoc (set! checked (add1 checked)) + #:print? #f + #:attempts 10) + checked) + 10) + (test (let ([checked 0]) (redex-check lang n #:enum 100 (set! checked (add1 checked)) #:print? #f