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

Removes undocumented, unmaintained random testing form

Browse Source
This commit is contained in:
Casey Klein 2010-07-21 08:34:55 -05:00
parent 541a0c4ecb
commit ad308e32f1
3 changed files with 2 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
collects/redex/private/rg.rkt
View File

@ -775,14 +775,14 @@
(and print? show)
fix
#:term-match term-match))
#`(check-prop
#`(check-one
#,(term-generator #'lang #'pat 'redex-check)
property att ret (and print? show) fix (and fix term-match)))))))))]))
(define (format-attempts a)
(format "~a attempt~a" a (if (= 1 a) "" "s")))
(define (check-prop generator property attempts retries show term-fix term-match)
(define (check-one generator property attempts retries show term-fix term-match)
(let ([c (check generator property attempts retries show
#:term-fix term-fix
#:term-match term-match)])
@ -845,34 +845,6 @@
(pretty-print term (current-output-port)))
(make-counterexample term)))))))))
(define-syntax (check-metafunction-contract stx)
(syntax-case stx ()
[(_ name . kw-args)
(identifier? #'name)
(with-syntax ([m (metafunc/err #'name stx)]
[(attempts retries)
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
(#:retries . ,#'default-retries))
(syntax kw-args)
stx)]
[show (show-message stx)])
(syntax/loc stx
(let ([lang (metafunc-proc-lang m)]
[dom (metafunc-proc-dom-pat m)]
[att (assert-nat 'check-metafunction-contract attempts)])
(check-prop
((compile lang 'check-metafunction-contract)
(if dom dom '(any (... ...))))
(term-prop
(λ (t)
(with-handlers ([exn:fail:redex? (λ (_) #f)])
(begin (term (name ,@t)) #t))))
att
retries
show
#f
#f))))]))
(define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix
#:term-match [term-match #f])
(let ([lang-gen (compile lang what)])
@ -999,7 +971,6 @@
(provide redex-check
generate-term
check-metafunction-contract
check-reduction-relation
check-metafunction
exn:fail:redex:generation-failure?)

1
collects/redex/reduction-semantics.rkt
View File

@ -48,7 +48,6 @@
(provide redex-check
generate-term
check-metafunction
check-metafunction-contract
check-reduction-relation
exn:fail:redex:generation-failure?
(struct-out exn:fail:redex:test)

53
collects/redex/tests/rg-test.rkt
View File

@ -747,59 +747,6 @@
(--> (side-condition any #f) any impossible)
#rx"^redex-check: unable to generate LHS of impossible in 42"))))
;; check-metafunction-contract
(let ()
(define-language L
(C hole (1 hole)))
(define-metafunction L
f : (side-condition number_1 (odd? (term number_1))) -> number
[(f 1) 1]
[(f 3) 'NaN])
(define-metafunction L
g : (1 1) -> C
[(g (in-hole C any)) C])
(define-metafunction L
h : number -> number
[(h any) any])
(define-metafunction L
[(i any ...) (any ...)])
(define-metafunction L
j : (side-condition any #f) -> any
[(j any ...) (any ...)])
;; Dom(f) < Ctc(f)
(test (output
(λ ()
(parameterize ([generation-decisions
(decisions #:num (list (λ _ 2) (λ _ 5)))])
(check-metafunction-contract f))))
#rx"check-metafunction-contract:.*counterexample found after 1 attempt:\n\\(5\\)\n")
;; Rng(f) > Codom(f)
(test (output
(λ ()
(parameterize ([generation-decisions
(decisions #:num (list (λ _ 3)))])
(check-metafunction-contract f))))
#rx"counterexample found after 1 attempt:\n\\(3\\)\n")
;; LHS matches multiple ways
(test (output (λ () (check-metafunction-contract g)))
#rx"counterexample found after 1 attempt:\n\\(\\(1 1\\)\\)\n")
;; OK -- generated from Dom(h)
(test (output (λ () (check-metafunction-contract h))) #rx"no counterexamples")
;; OK -- generated from pattern (any ...)
(test (output (λ () (check-metafunction-contract i #:attempts 5))) #rx"no counterexamples")
;; Unable to generate domain
(test (raised-exn-msg
exn:fail:redex:generation-failure?
(check-metafunction-contract j #:attempts 1 #:retries 42))
#rx"^check-metafunction-contract: unable .* in 42"))
;; check-reduction-relation
(let ()
(define-language L