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

Made counterexample structure transparent

Browse Source 
svn: r17882
This commit is contained in:
Casey Klein 2010-01-29 13:42:13 +00:00
parent da79980114
commit 2d2a95de1e
3 changed files with 10 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/private/rg.ss
View File

@ -750,7 +750,7 @@
#t)))) #t))))
(define-struct (exn:fail:redex:test exn:fail:redex) (source term)) (define-struct (exn:fail:redex:test exn:fail:redex) (source term))
(define-struct counterexample (term)) (define-struct counterexample (term) #:transparent)
(define (check generator property attempts retries show (define (check generator property attempts retries show
#:source [source #f] #:source [source #f]

2
collects/redex/redex.scrbl
View File

@ -1240,7 +1240,7 @@ term that does not match @scheme[pattern].}
#:attempts 3 #:attempts 3
#:source R))] #:source R))]
@defstruct[counterexample ([term any/c])]{ @defstruct[counterexample ([term any/c]) #:inspector #f]{
Produced by @scheme[redex-check], @scheme[check-reduction-relation], and Produced by @scheme[redex-check], @scheme[check-reduction-relation], and
@scheme[check-metafunction] when testing falsifies a property.} @scheme[check-metafunction] when testing falsifies a property.}

17
collects/redex/tests/rg-test.ss
View File

@ -542,7 +542,8 @@
(n number)) (n number))
(test (redex-check lang d #t #:attempts 1 #:print? (not #t)) #t) (test (redex-check lang d #t #:attempts 1 #:print? (not #t)) #t)
(test (counterexample-term (redex-check lang d #f #:print? #f)) 5) (test (redex-check lang d #f #:print? #f)
(make-counterexample 5))
(let ([exn (with-handlers ([exn:fail:redex:test? values]) (let ([exn (with-handlers ([exn:fail:redex:test? values])
(redex-check lang d (error 'boom ":(") #:print? #f) (redex-check lang d (error 'boom ":(") #:print? #f)
'not-an-exn)]) 'not-an-exn)])
@ -602,11 +603,10 @@
#:source R #:source R
#:print? (not #t)) #:print? (not #t))
#t) #t)
(test (counterexample-term (test (redex-check lang any (= (term any) 1)
(redex-check lang any (= (term any) 1)
#:source R #:source R
#:print? #f)) #:print? #f)
2)) (make-counterexample 2)))
(let () (let ()
(define-metafunction lang (define-metafunction lang
@ -623,11 +623,10 @@
#:source mf #:source mf
#:print? (not #t)) #:print? (not #t))
#t) #t)
(test (counterexample-term (test (redex-check lang any (= (car (term any)) 42)
(redex-check lang any (= (car (term any)) 42)
#:source mf #:source mf
#:print? #f)) #:print? #f)
'(0))) (make-counterexample '(0))))
(let () (let ()
(define-metafunction lang (define-metafunction lang