use the enumerator in a new option to redex-check
This commit is contained in:
Robby Findler
parent
0993a029cd
commit
f8ea4f46ef
|
|
@ -1841,6 +1841,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 #:satisfying
|
||||
(judgment-form-id @#,ttpattern ...))
|
||||
(code:line language #:satisfying
|
||||
|
|
@ -1871,8 +1872,12 @@ 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 generates terms that match
|
||||
@racket[pattern].}
|
||||
In this case, 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 #:satisfying (judgment-form-id @#,ttpattern ...)]:
|
||||
Generates terms that match @racket[pattern] and satisfy
|
||||
the judgment form.}
|
||||
|
|
|
|||
|
|
@ -20,7 +20,8 @@
|
|||
setup/path-to-relative
|
||||
"rewrite-side-conditions.rkt"
|
||||
"term-fn.rkt"
|
||||
"keyword-macros.rkt"))
|
||||
"keyword-macros.rkt")
|
||||
math/base)
|
||||
|
||||
(define-for-syntax (metafunc name)
|
||||
(and (identifier? name)
|
||||
|
|
@ -91,6 +92,7 @@
|
|||
(define-syntax (redex-check stx)
|
||||
(define valid-kws
|
||||
(list* '#:satisfying
|
||||
'#:enum
|
||||
(map car (list attempts-keyword
|
||||
source-keyword
|
||||
retries-keyword
|
||||
|
|
@ -120,8 +122,10 @@
|
|||
(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 property . kw-args)
|
||||
(redex-check/pat stx #'form #'lang #'pat #'property #'kw-args)]))
|
||||
(redex-check/pat stx #'form #'lang #'pat #'property #f #'kw-args)]))
|
||||
|
||||
(define-struct gen-fail ())
|
||||
|
||||
|
|
@ -199,7 +203,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 kw-args)
|
||||
(define-for-syntax (redex-check/pat orig-stx form lang pat property enum-bound-e kw-args)
|
||||
(with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang
|
||||
|
|
@ -222,8 +226,15 @@
|
|||
[else (redex-error 'redex-check "~s does not match ~s" generated '#,pat)]))])
|
||||
syncheck-exp
|
||||
(parameterize ([attempt->size #,size-stx])
|
||||
#,(if source-stx
|
||||
#`(let-values ([(metafunc/red-rel num-cases)
|
||||
#,(cond
|
||||
[source-stx
|
||||
(when enum-bound-e
|
||||
(raise-syntax-error
|
||||
#f
|
||||
"#:enum cannot be used with the #:source keyword"
|
||||
orig-stx
|
||||
enum-bound-e))
|
||||
#`(let-values ([(metafunc/red-rel num-cases)
|
||||
#,(cond [(metafunc source-stx)
|
||||
=> (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
|
||||
[else
|
||||
|
|
@ -240,11 +251,26 @@
|
|||
(and print? show)
|
||||
fix
|
||||
keep-going?
|
||||
#:term-match term-match))
|
||||
#`(check-one
|
||||
#,(term-generator lang #'pattern 'redex-check)
|
||||
property att ret (and print? show) fix (and fix term-match)
|
||||
keep-going?))))))))
|
||||
#:term-match term-match))]
|
||||
[else
|
||||
(cond
|
||||
[enum-bound-e
|
||||
#`(check-one
|
||||
(ith-generator #,lang `pattern #,enum-bound-e)
|
||||
property att ret (and print? show) (or fix (λ (x) x)) term-match
|
||||
keep-going?)]
|
||||
[else
|
||||
#`(check-one
|
||||
#,(term-generator lang #'pattern 'redex-check)
|
||||
property att ret (and print? show) fix (and fix term-match)
|
||||
keep-going?)])])))))))
|
||||
|
||||
(define (ith-generator lang pat bound)
|
||||
(define enum-lang (compiled-lang-enum-table lang))
|
||||
(define enum (pat-enumerator enum-lang pat))
|
||||
(λ (_size _attempt _retries)
|
||||
(values (enum-ith enum (random-natural bound))
|
||||
'ignored)))
|
||||
|
||||
(define-for-syntax (parse-redex-check-kw-args kw-args orig-stx form-name)
|
||||
(apply values
|
||||
|
|
@ -557,7 +583,7 @@
|
|||
(raise-argument-error 'generate-term
|
||||
"exact-nonnegative-integer?"
|
||||
i))
|
||||
(enum-ith enum i)))
|
||||
(enum-ith enum i)))
|
||||
|
||||
(define-syntax (generate-term/mf stx)
|
||||
(syntax-case stx ()
|
||||
|
|
|
|||
|
|
@ -888,7 +888,15 @@
|
|||
|
||||
(test-gen-fail
|
||||
(--> (side-condition any #f) any impossible)
|
||||
#rx"^redex-check: unable to generate LHS of impossible in 42"))))
|
||||
#rx"^redex-check: unable to generate LHS of impossible in 42")))
|
||||
|
||||
|
||||
(test (let ([checked 0])
|
||||
(redex-check lang n #:enum 100 (set! checked (add1 checked))
|
||||
#:print? #f
|
||||
#:attempts 10)
|
||||
checked)
|
||||
10))
|
||||
|
||||
;; check-reduction-relation
|
||||
(let ()
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user