suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

change the meaning of the #:enum argument to redex-check

Browse Source 
Thanks to Neil Toronto for suggesting how to do this!
This commit is contained in:
Robby Findler 2014-02-23 09:24:03 -06:00
parent 6a0d387ac4
commit e0a1a40fd4
4 changed files with 43 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
View File

@ -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.}

2
pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt
View File

@ -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

47
pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
View File

@ -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

2
pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt
View File

@ -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)