adjust #:enum arg to redex-check to be back like 6.0,
add #:uniform-at-random argument and #:in-order argument
This commit is contained in:
Robby Findler
parent
55cb28168e
commit
89ef6f831e
|
|
@ -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.}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user