A flag to make the random testing forms return results instead of
printing on stdout. svn: r17858
This commit is contained in:
Casey Klein
parent
8733e7f233
commit
1b22ce82cd
|
|
@ -695,11 +695,12 @@
|
|||
(let-values ([(names names/ellipses)
|
||||
(extract-names (language-id-nts #'lang 'redex-check)
|
||||
'redex-check #t #'pat)]
|
||||
[(attempts-stx source-stx retries-stx)
|
||||
[(attempts-stx source-stx retries-stx print?-stx)
|
||||
(apply values
|
||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||
(#:source . #f)
|
||||
(#:retries . ,#'default-retries))
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:print? . #t))
|
||||
(syntax kw-args)
|
||||
stx))])
|
||||
(with-syntax ([(name ...) names]
|
||||
|
|
@ -711,7 +712,8 @@
|
|||
property)))])
|
||||
(quasisyntax/loc stx
|
||||
(let ([att (assert-nat 'redex-check #,attempts-stx)]
|
||||
[ret (assert-nat 'redex-check #,retries-stx)])
|
||||
[ret (assert-nat 'redex-check #,retries-stx)]
|
||||
[print? #,print?-stx])
|
||||
(unsyntax
|
||||
(if source-stx
|
||||
#`(let-values ([(metafunc/red-rel num-cases)
|
||||
|
|
@ -728,21 +730,27 @@
|
|||
(max 1 (floor (/ att num-cases)))
|
||||
ret
|
||||
'redex-check
|
||||
show
|
||||
(and print? show)
|
||||
(test-match lang pat)
|
||||
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
|
||||
#`(check-prop
|
||||
#,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
|
||||
property att ret show)))
|
||||
(void))))))]))
|
||||
property att ret (and print? show)))))))))]))
|
||||
|
||||
(define (format-attempts a)
|
||||
(format "~a attempt~a" a (if (= 1 a) "" "s")))
|
||||
|
||||
(define (check-prop generator property attempts retries show)
|
||||
(when (check generator property attempts retries show)
|
||||
(show (format "no counterexamples in ~a\n"
|
||||
(format-attempts attempts)))))
|
||||
(define (check-prop generator property attempts retries show)
|
||||
(let ([c (check generator property attempts retries show)])
|
||||
(if (counterexample? c)
|
||||
(unless show c) ; check printed it
|
||||
(if show
|
||||
(show (format "no counterexamples in ~a\n"
|
||||
(format-attempts attempts)))
|
||||
#t))))
|
||||
|
||||
(define-struct (exn:fail:redex:test exn:fail:redex) (source term))
|
||||
(define-struct counterexample (term))
|
||||
|
||||
(define (check generator property attempts retries show
|
||||
#:source [source #f]
|
||||
|
|
@ -757,9 +765,16 @@
|
|||
(with-handlers
|
||||
([exn:fail?
|
||||
(λ (exn)
|
||||
(show
|
||||
(format "checking ~s raises an exception\n" term))
|
||||
(raise exn))])
|
||||
(when show
|
||||
(show (format "checking ~s raises an exception\n" term)))
|
||||
(raise
|
||||
(if show
|
||||
exn
|
||||
(make-exn:fail:redex:test
|
||||
(format "checking ~s raises an exception:\n~a" term (exn-message exn))
|
||||
(current-continuation-marks)
|
||||
exn
|
||||
term))))])
|
||||
(property term bindings)))
|
||||
(cond [(and match match-fail (match term))
|
||||
=> (curry map (compose make-bindings match-bindings))]
|
||||
|
|
@ -767,12 +782,13 @@
|
|||
[else (list bindings)]))
|
||||
(loop (sub1 remaining))
|
||||
(begin
|
||||
(show
|
||||
(format "counterexample found after ~a~a:\n"
|
||||
(format-attempts attempt)
|
||||
(if source (format " with ~a" source) "")))
|
||||
(pretty-print term (current-output-port))
|
||||
#f)))))))
|
||||
(when show
|
||||
(show
|
||||
(format "counterexample found after ~a~a:\n"
|
||||
(format-attempts attempt)
|
||||
(if source (format " with ~a" source) "")))
|
||||
(pretty-print term (current-output-port)))
|
||||
(make-counterexample term))))))))
|
||||
|
||||
(define-syntax (check-metafunction-contract stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -801,8 +817,8 @@
|
|||
show))))]))
|
||||
|
||||
(define (check-lhs-pats lang mf/rr prop decisions@ attempts retries what show
|
||||
[match #f]
|
||||
[match-fail #f])
|
||||
[match #f]
|
||||
[match-fail #f])
|
||||
(let ([lang-gen (generate lang decisions@ what)])
|
||||
(let-values ([(pats srcs)
|
||||
(cond [(metafunc-proc? mf/rr)
|
||||
|
|
@ -811,46 +827,53 @@
|
|||
[(reduction-relation? mf/rr)
|
||||
(values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr))
|
||||
(reduction-relation-srcs mf/rr))])])
|
||||
(when (for/and ([pat pats] [src srcs])
|
||||
(with-handlers ([exn:fail:redex:generation-failure?
|
||||
; Produce an error message that blames the LHS as a whole.
|
||||
(λ (_)
|
||||
(raise-gen-fail what (format "LHS of ~a" src) retries))])
|
||||
(check
|
||||
(lang-gen pat)
|
||||
prop
|
||||
attempts
|
||||
retries
|
||||
show
|
||||
#:source src
|
||||
#:match match
|
||||
#:match-fail match-fail)))
|
||||
(show
|
||||
(format "no counterexamples in ~a (with each clause)\n"
|
||||
(format-attempts attempts)))))))
|
||||
(let loop ([pats pats] [srcs srcs])
|
||||
(if (and (null? pats) (null? srcs))
|
||||
(if show
|
||||
(show
|
||||
(format "no counterexamples in ~a (with each clause)\n"
|
||||
(format-attempts attempts)))
|
||||
#t)
|
||||
(let ([c (with-handlers ([exn:fail:redex:generation-failure?
|
||||
; Produce an error message that blames the LHS as a whole.
|
||||
(λ (_)
|
||||
(raise-gen-fail what (format "LHS of ~a" (car srcs)) retries))])
|
||||
(check
|
||||
(lang-gen (car pats))
|
||||
prop
|
||||
attempts
|
||||
retries
|
||||
show
|
||||
#:source (car srcs)
|
||||
#:match match
|
||||
#:match-fail match-fail))])
|
||||
(if (counterexample? c)
|
||||
(unless show c)
|
||||
(loop (cdr pats) (cdr srcs)))))))))
|
||||
|
||||
(define-syntax (check-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name property . kw-args)
|
||||
(with-syntax ([m (metafunc/err #'name stx)]
|
||||
[(attempts retries)
|
||||
[(attempts retries print?)
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries))
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:print? . #t))
|
||||
(syntax kw-args)
|
||||
stx)]
|
||||
[show (show-message stx)])
|
||||
(syntax/loc stx
|
||||
(let ([att (assert-nat 'check-metafunction attempts)]
|
||||
[ret (assert-nat 'check-metafunction retries)])
|
||||
(check-lhs-pats
|
||||
(metafunc-proc-lang m)
|
||||
m
|
||||
(λ (term _) (property term))
|
||||
(generation-decisions)
|
||||
att
|
||||
ret
|
||||
'check-metafunction
|
||||
show))))]))
|
||||
stx)])
|
||||
(with-syntax ([show (show-message stx)])
|
||||
(syntax/loc stx
|
||||
(let ([att (assert-nat 'check-metafunction attempts)]
|
||||
[ret (assert-nat 'check-metafunction retries)])
|
||||
(check-lhs-pats
|
||||
(metafunc-proc-lang m)
|
||||
m
|
||||
(λ (term _) (property term))
|
||||
(generation-decisions)
|
||||
att
|
||||
ret
|
||||
'check-metafunction
|
||||
(and print? show))))))]))
|
||||
|
||||
(define (reduction-relation-srcs r)
|
||||
(map (λ (proc) (or (rewrite-proc-name proc)
|
||||
|
|
@ -864,10 +887,11 @@
|
|||
(define-syntax (check-reduction-relation stx)
|
||||
(syntax-case stx ()
|
||||
[(_ relation property . kw-args)
|
||||
(with-syntax ([(attempts retries decisions@)
|
||||
(with-syntax ([(attempts retries decisions@ print?)
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:decisions . ,#'random-decisions@))
|
||||
(#:decisions . ,#'random-decisions@)
|
||||
(#:print? . #t))
|
||||
(syntax kw-args)
|
||||
stx)]
|
||||
[show (show-message stx)])
|
||||
|
|
@ -883,7 +907,7 @@
|
|||
attempts
|
||||
retries
|
||||
'check-reduction-relation
|
||||
show))))]))
|
||||
(and print? show)))))]))
|
||||
|
||||
(define-signature decisions^
|
||||
(next-variable-decision
|
||||
|
|
@ -921,7 +945,9 @@
|
|||
(struct-out mismatch)
|
||||
(struct-out class)
|
||||
(struct-out binder)
|
||||
(struct-out base-cases))
|
||||
(struct-out base-cases)
|
||||
(struct-out counterexample)
|
||||
(struct-out exn:fail:redex:test))
|
||||
|
||||
(provide pick-from-list pick-sequence-length pick-nts
|
||||
pick-char pick-var pick-string pick-any
|
||||
|
|
|
|||
|
|
@ -1166,11 +1166,13 @@ repeating as necessary. The optional keyword argument @scheme[retries-expr]
|
|||
([kw-arg (code:line #:attempts attempts-expr)
|
||||
(code:line #:source metafunction)
|
||||
(code:line #:source relation-expr)
|
||||
(code:line #:retries retries-expr)])
|
||||
(code:line #:retries retries-expr)
|
||||
(code:line #:print? print?-expr)])
|
||||
#:contracts ([property-expr any/c]
|
||||
[attempts-expr natural-number/c]
|
||||
[relation-expr reduction-relation?]
|
||||
[retries-expr natural-number/c])]{
|
||||
[retries-expr natural-number/c]
|
||||
[print?-expr any/c])]{
|
||||
Searches for a counterexample to @scheme[property-expr], interpreted
|
||||
as a predicate universally quantified over the pattern variables
|
||||
bound by @scheme[pattern]. @scheme[redex-check] constructs and tests
|
||||
|
|
@ -1180,8 +1182,18 @@ using the @scheme[match-bindings] produced by @scheme[match]ing
|
|||
@math{t} against @scheme[pattern].
|
||||
|
||||
@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[1000])
|
||||
random terms in its search. The size and complexity of terms it generates
|
||||
gradually increases with each failed attempt.
|
||||
random terms in its search. The size and complexity of these terms increase with
|
||||
each failed attempt.
|
||||
|
||||
When @scheme[print?-expr] produces any non-@scheme[#f] value (the default),
|
||||
@scheme[redex-check] prints the test outcome on @scheme[current-output-port].
|
||||
When @scheme[print?-expr] produces @scheme[#f], @scheme[redex-check] prints
|
||||
nothing, instead
|
||||
@itemlist[
|
||||
@item{returning a @scheme[counterexample] structure when the test reveals a counterexample,}
|
||||
@item{returning @scheme[#t] when all tests pass, or}
|
||||
@item{raising a @scheme[exn:fail:redex:test] when checking the property raises an exception.}
|
||||
]
|
||||
|
||||
When passed a metafunction or reduction relation via the optional @scheme[#:source]
|
||||
argument, @scheme[redex-check] distributes its attempts across the left-hand sides
|
||||
|
|
@ -1228,6 +1240,16 @@ term that does not match @scheme[pattern].}
|
|||
#:attempts 3
|
||||
#:source R))]
|
||||
|
||||
@defstruct[counterexample ([term any/c])]{
|
||||
Produced by @scheme[redex-check], @scheme[check-reduction-relation], and
|
||||
@scheme[check-metafunction] when testing falsifies a property.}
|
||||
|
||||
@defstruct[(exn:fail:redex:test exn:fail:redex) ([source exn:fail?] [term any/c])]{
|
||||
Raised by @scheme[redex-check], @scheme[check-reduction-relation], and
|
||||
@scheme[check-metafunction] when testing a property raises an exception.
|
||||
The @scheme[exn:fail:redex:test-source] component contains the exception raised by the property,
|
||||
and the @scheme[exn:fail:redex:test-term] component contains the term that induced the exception.}
|
||||
|
||||
@defform/subs[(check-reduction-relation relation property kw-args ...)
|
||||
([kw-arg (code:line #:attempts attempts-expr)
|
||||
(code:line #:retries retries-expr)])
|
||||
|
|
|
|||
|
|
@ -50,7 +50,9 @@
|
|||
check-metafunction
|
||||
check-metafunction-contract
|
||||
check-reduction-relation
|
||||
exn:fail:redex:generation-failure?)
|
||||
exn:fail:redex:generation-failure?
|
||||
(struct-out exn:fail:redex:test)
|
||||
(struct-out counterexample))
|
||||
|
||||
(provide/contract
|
||||
[current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
|
||||
|
|
|
|||
|
|
@ -540,6 +540,16 @@
|
|||
(d 5)
|
||||
(e e 4)
|
||||
(n number))
|
||||
|
||||
(test (redex-check lang d #t #:attempts 1 #:print? (not #t)) #t)
|
||||
(test (counterexample-term (redex-check lang d #f #:print? #f)) 5)
|
||||
(let ([exn (with-handlers ([exn:fail:redex:test? values])
|
||||
(redex-check lang d (error 'boom ":(") #:print? #f)
|
||||
'not-an-exn)])
|
||||
(test (exn-message exn) "checking 5 raises an exception:\nboom: :(")
|
||||
(test (exn-message (exn:fail:redex:test-source exn)) "boom: :(")
|
||||
(test (exn:fail:redex:test-term exn) 5))
|
||||
|
||||
(test (output (λ () (redex-check lang d #f)))
|
||||
#rx"redex-check: .*:.*\ncounterexample found after 1 attempt:\n5\n")
|
||||
(test (output (λ () (redex-check lang d #t)))
|
||||
|
|
@ -574,17 +584,29 @@
|
|||
(--> 0 dontcare z)))))
|
||||
#rx"counterexample found after 1 attempt with z:\n0\n")
|
||||
|
||||
(let ([generated null])
|
||||
(let ([generated null]
|
||||
[R (reduction-relation
|
||||
lang
|
||||
(--> 1 dontcare)
|
||||
(--> 2 dontcare))])
|
||||
(test (output
|
||||
(λ ()
|
||||
(redex-check lang n (set! generated (cons (term n) generated))
|
||||
#:attempts 5
|
||||
#:source (reduction-relation
|
||||
lang
|
||||
(--> 1 dontcare)
|
||||
(--> 2 dontcare)))))
|
||||
#:source R)))
|
||||
#rx"no counterexamples.*with each clause")
|
||||
(test generated '(2 2 1 1)))
|
||||
(test generated '(2 2 1 1))
|
||||
|
||||
(test (redex-check lang any #t
|
||||
#:attempts 1
|
||||
#:source R
|
||||
#:print? (not #t))
|
||||
#t)
|
||||
(test (counterexample-term
|
||||
(redex-check lang any (= (term any) 1)
|
||||
#:source R
|
||||
#:print? #f))
|
||||
2))
|
||||
|
||||
(let ()
|
||||
(define-metafunction lang
|
||||
|
|
@ -595,7 +617,17 @@
|
|||
(redex-check lang (n) (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source mf)))
|
||||
#px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n"))
|
||||
#px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n")
|
||||
(test (redex-check lang any #t
|
||||
#:attempts 1
|
||||
#:source mf
|
||||
#:print? (not #t))
|
||||
#t)
|
||||
(test (counterexample-term
|
||||
(redex-check lang any (= (car (term any)) 42)
|
||||
#:source mf
|
||||
#:print? #f))
|
||||
'(0)))
|
||||
|
||||
(let ()
|
||||
(define-metafunction lang
|
||||
|
|
@ -720,6 +752,14 @@
|
|||
(E* hole E*)
|
||||
(n 4))
|
||||
|
||||
(let ([R (reduction-relation
|
||||
L
|
||||
(--> 1 2)
|
||||
(--> 2 3))])
|
||||
(test (check-reduction-relation R (λ (_) #t) #:print? #f) #t)
|
||||
(test (counterexample-term (check-reduction-relation R (curry = 1) #:print? #f))
|
||||
2))
|
||||
|
||||
(let ([generated null]
|
||||
[R (reduction-relation
|
||||
L
|
||||
|
|
@ -787,6 +827,11 @@
|
|||
(define-metafunction empty
|
||||
[(n (side-condition any #f)) any])
|
||||
|
||||
(test (check-metafunction m (λ (_) #t) #:print? #f) #t)
|
||||
(test (counterexample-term
|
||||
(check-metafunction m (compose (curry = 1) car) #:print? #f))
|
||||
'(2))
|
||||
|
||||
(let ([generated null])
|
||||
(test (begin
|
||||
(output
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user