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

Changed the output of Redex's check forms.

Browse Source 
svn: r14307
This commit is contained in:
Casey Klein 2009-03-27 00:26:11 +00:00
parent fb237a13ae
commit c39e5dfa38
4 changed files with 182 additions and 126 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

118
collects/redex/private/rg-test.ss
View File

@ -579,6 +579,16 @@
(if (= attempt finish) 0 'x)))) (if (= attempt finish) 0 'x))))
(test attempts (list finish retry-threshold start)))) (test attempts (list finish retry-threshold start))))
;; output : (-> (-> void) string)
(define (output thunk)
(let ([p (open-output-string)])
(parameterize ([current-output-port p])
(unless (void? (thunk))
(error 'output "expected void result")))
(begin0
(get-output-string p)
(close-output-port p))))
;; preferred productions ;; preferred productions
(let ([make-pick-nt (λ opt (λ req (apply pick-nt (append req opt))))]) (let ([make-pick-nt (λ opt (λ req (apply pick-nt (append req opt))))])
(define-language L (define-language L
@ -606,30 +616,22 @@
'(+ (+ 7 7) (+ 7 7))) '(+ (+ 7 7) (+ 7 7)))
(test (test
(let ([generated null]) (let ([generated null])
(check-reduction-relation (output
(reduction-relation L (--> e e)) (λ ()
(λ (t) (set! generated (cons t generated))) (check-reduction-relation
#:decisions (decisions #:nt (make-pick-nt (make-random) (reduction-relation L (--> e e))
(λ (att rand) #t)) (λ (t) (set! generated (cons t generated)))
#:pref (list (λ (_) 'dontcare) #:decisions (decisions #:nt (make-pick-nt (make-random)
(λ (_) 'dontcare) (λ (att rand) #t))
(λ (_) 'dontcare) #:pref (list (λ (_) 'dontcare)
(λ (L) (make-immutable-hash `((e ,(car (pats L)))))) (λ (_) 'dontcare)
(λ (L) (make-immutable-hash `((e ,(cadr (pats L)))))))) (λ (_) 'dontcare)
#:attempts 5) (λ (L) (make-immutable-hash `((e ,(car (pats L))))))
(λ (L) (make-immutable-hash `((e ,(cadr (pats L))))))))
#:attempts 5)))
generated) generated)
'((* 7 7) (+ 7 7) 7 7 7)))) '((* 7 7) (+ 7 7) 7 7 7))))
;; output : (-> (-> void) string)
(define (output thunk)
(let ([p (open-output-string)])
(parameterize ([current-output-port p])
(unless (void? (thunk))
(error 'output "expected void result")))
(begin0
(get-output-string p)
(close-output-port p))))
;; redex-check ;; redex-check
(let () (let ()
(define-language lang (define-language lang
@ -637,16 +639,22 @@
(e e 4) (e e 4)
(n number)) (n number))
(test (output (λ () (redex-check lang d #f))) (test (output (λ () (redex-check lang d #f)))
"counterexample found after 1 attempt:\n5\n") #rx"redex-check: .*:.*\ncounterexample found after 1 attempt:\n5\n")
(test (output (λ () (redex-check lang d #t))) "") (test (output (λ () (redex-check lang d #t)))
#rx"redex-check: .*:.*\nno counterexamples in 1000 attempts\n")
(let-syntax ([noloc (λ (stx)
(syntax-case stx ()
[(_ e) (datum->syntax stx (syntax->datum #'e) #f)]))])
(test (output (λ () (noloc (redex-check lang d #t))))
"redex-check: no counterexamples in 1000 attempts\n"))
(test (output (λ () (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2))) (test (output (λ () (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2)))
"") #rx"no counterexamples")
(test (output (λ () (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2))) (test (output (λ () (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2)))
"") #rx"no counterexamples")
(test (output (λ () (redex-check lang (d e) #f))) (test (output (λ () (redex-check lang (d e) #f)))
"counterexample found after 1 attempt:\n(5 4)\n") #rx"counterexample found after 1 attempt:\n\\(5 4\\)\n")
(let* ([p (open-output-string)] (let* ([p (open-output-string)]
[m (parameterize ([current-error-port p]) [m (parameterize ([current-output-port p])
(with-handlers ([exn:fail? exn-message]) (with-handlers ([exn:fail? exn-message])
(redex-check lang d (error 'pred-raised)) (redex-check lang d (error 'pred-raised))
'no-exn-raised))]) 'no-exn-raised))])
@ -662,7 +670,7 @@
lang lang
(--> 42 dontcare) (--> 42 dontcare)
(--> 0 dontcare z))))) (--> 0 dontcare z)))))
"counterexample found after 1 attempt with z:\n0\n") #rx"counterexample found after 1 attempt with z:\n0\n")
(let ([generated null]) (let ([generated null])
(test (output (test (output
@ -673,7 +681,7 @@
lang lang
(--> 1 dontcare) (--> 1 dontcare)
(--> 2 dontcare))))) (--> 2 dontcare)))))
"") #rx"no counterexamples.*with each clause")
(test generated '(2 2 1 1))) (test generated '(2 2 1 1)))
(let () (let ()
@ -685,7 +693,7 @@
(redex-check lang (n) (eq? 42 (term n)) (redex-check lang (n) (eq? 42 (term n))
#:attempts 1 #:attempts 1
#:source mf))) #:source mf)))
"counterexample found after 1 attempt with clause #2:\n(0)\n")) #rx"counterexample found after 1 attempt with clause #2:\n\\(0\\)\n"))
(let () (let ()
(define-metafunction lang (define-metafunction lang
@ -697,13 +705,12 @@
(= (term number_2) 4)) (= (term number_2) 4))
#:attempts 1 #:attempts 1
#:source mf))) #:source mf)))
"")) #rx"no counterexamples"))
(let () (test (raised-exn-msg
(test (raised-exn-msg exn:fail:redex?
exn:fail:redex? (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
(redex-check lang n #t #:source (reduction-relation lang (--> x 1)))) #rx"x does not match n")
#rx"x does not match n"))
(test (raised-exn-msg (test (raised-exn-msg
exn:fail:redex? exn:fail:redex?
(redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1)) (redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
@ -747,14 +754,14 @@
(parameterize ([generation-decisions (parameterize ([generation-decisions
(decisions #:num (list (λ _ 2) (λ _ 5)))]) (decisions #:num (list (λ _ 2) (λ _ 5)))])
(check-metafunction-contract f)))) (check-metafunction-contract f))))
"counterexample found after 1 attempt:\n(5)\n") #rx"check-metafunction-contract:.*counterexample found after 1 attempt:\n\\(5\\)\n")
;; Rng(f) > Codom(f) ;; Rng(f) > Codom(f)
(test (output (test (output
(λ () (λ ()
(parameterize ([generation-decisions (parameterize ([generation-decisions
(decisions #:num (list (λ _ 3)))]) (decisions #:num (list (λ _ 3)))])
(check-metafunction-contract f)))) (check-metafunction-contract f))))
"counterexample found after 1 attempt:\n(3)\n") #rx"counterexample found after 1 attempt:\n\\(3\\)\n")
;; LHS matches multiple ways ;; LHS matches multiple ways
(test (output (test (output
(λ () (λ ()
@ -762,11 +769,11 @@
(decisions #:num (list (λ _ 1) (λ _ 1)) (decisions #:num (list (λ _ 1) (λ _ 1))
#:seq (list (λ _ 2)))]) #:seq (list (λ _ 2)))])
(check-metafunction-contract g)))) (check-metafunction-contract g))))
"counterexample found after 1 attempt:\n(1 1)\n") #rx"counterexample found after 1 attempt:\n\\(1 1\\)\n")
;; OK -- generated from Dom(h) ;; OK -- generated from Dom(h)
(test (output (λ () (check-metafunction-contract h))) "") (test (output (λ () (check-metafunction-contract h))) #rx"no counterexamples")
;; OK -- generated from pattern (any ...) ;; OK -- generated from pattern (any ...)
(test (output (λ () (check-metafunction-contract i #:attempts 5))) "") (test (output (λ () (check-metafunction-contract i #:attempts 5))) #rx"no counterexamples")
;; Unable to generate domain ;; Unable to generate domain
(test (raised-exn-msg (test (raised-exn-msg
@ -791,22 +798,25 @@
[(--> (in-hole E a) whatever) [(--> (in-hole E a) whatever)
(==> a b)])]) (==> a b)])])
(test (begin (test (begin
(check-reduction-relation (output
R (λ (term) (set! generated (cons term generated))) (λ ()
#:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0)) (check-reduction-relation
#:num (list (λ _ 1) (λ _ 1) (λ _ 0))) R (λ (term) (set! generated (cons term generated)))
#:attempts 1) #:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
#:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
#:attempts 1)))
generated) generated)
(reverse '((+ (+)) 0)))) (reverse '((+ (+)) 0))))
(let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))]) (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
(test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) "") (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1)))
#rx"check-reduction-relation:.*no counterexamples")
(test (output (test (output
(λ () (check-reduction-relation S (λ (x) #f)))) (λ () (check-reduction-relation S (λ (x) #f))))
"counterexample found after 1 attempt with name:\n1\n") #rx"counterexample found after 1 attempt with name:\n1\n")
(test (output (test (output
(λ () (check-reduction-relation S (curry eq? 1)))) (λ () (check-reduction-relation S (curry eq? 1))))
"counterexample found after 1 attempt with unnamed:\n3\n")) #rx"counterexample found after 1 attempt with unnamed:\n3\n"))
(let ([T (reduction-relation (let ([T (reduction-relation
L L
@ -824,7 +834,7 @@
T (curry equal? '(9 4)) T (curry equal? '(9 4))
#:attempts 1 #:attempts 1
#:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x))))))) #:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))))
"")) #rx"no counterexamples"))
(let ([U (reduction-relation L (--> (side-condition any #f) any))]) (let ([U (reduction-relation L (--> (side-condition any #f) any))])
(test (raised-exn-msg (test (raised-exn-msg
@ -842,12 +852,14 @@
[(n (side-condition any #f)) any]) [(n (side-condition any #f)) any])
(let ([generated null]) (let ([generated null])
(test (begin (test (begin
(check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1) (output
(λ ()
(check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)))
generated) generated)
(reverse '((1) (2))))) (reverse '((1) (2)))))
(test (output (λ () (check-metafunction m (λ (_) #t)))) "") (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
(test (output (λ () (check-metafunction m (curry eq? 1)))) (test (output (λ () (check-metafunction m (curry eq? 1))))
#rx"counterexample found after 1 attempt with clause #1") #rx"check-metafunction:.*counterexample found after 1 attempt with clause #1")
(test (raised-exn-msg (test (raised-exn-msg
exn:fail:contract? exn:fail:contract?
(check-metafunction m (λ (_) #t) #:attempts 'NaN)) (check-metafunction m (λ (_) #t) #:attempts 'NaN))

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

@ -696,6 +696,9 @@ To do a better job of not generating programs with free variables,
(define (assert-nat name x) (define (assert-nat name x)
(unless (and (integer? x) (>= x 0)) (unless (and (integer? x) (>= x 0))
(raise-type-error name "natural number" x))) (raise-type-error name "natural number" x)))
(define (assert-rel name x)
(unless (reduction-relation? x)
(raise-type-error 'redex-check "reduction-relation" x)))
(define-for-syntax (term-generator lang pat decisions@ retries what) (define-for-syntax (term-generator lang pat decisions@ retries what)
(with-syntax ([pattern (with-syntax ([pattern
@ -719,6 +722,22 @@ To do a better job of not generating programs with free variables,
[(_ lang pat size) [(_ lang pat size)
(syntax/loc stx (generate-term lang pat size #:attempt 1))])) (syntax/loc stx (generate-term lang pat size #:attempt 1))]))
(define-for-syntax (show-message stx)
(syntax-case stx ()
[(what . _)
(identifier? #'what)
(with-syntax ([loc (if (and (path? (syntax-source stx))
(syntax-line stx))
(format "~a:~a"
(path->string (syntax-source stx))
(syntax-line stx))
#f)])
#`(λ (msg)
(fprintf
(current-output-port)
"~a: ~a~a"
'what (if loc (string-append loc "\n") "") msg)))]))
(define-syntax (redex-check stx) (define-syntax (redex-check stx)
(syntax-case stx () (syntax-case stx ()
[(_ lang pat property . kw-args) [(_ lang pat property . kw-args)
@ -735,7 +754,8 @@ To do a better job of not generating programs with free variables,
(with-syntax ([(name ...) names] (with-syntax ([(name ...) names]
[(name/ellipses ...) names/ellipses] [(name/ellipses ...) names/ellipses]
[attempts attempts-stx] [attempts attempts-stx]
[retries retries-stx]) [retries retries-stx]
[show (show-message stx)])
(with-syntax ([property (syntax (with-syntax ([property (syntax
(λ (_ bindings) (λ (_ bindings)
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...) (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
@ -756,49 +776,57 @@ To do a better job of not generating programs with free variables,
(metafunc-proc-lang #,m)))] (metafunc-proc-lang #,m)))]
[else [else
#`(let ([r #,source-stx]) #`(let ([r #,source-stx])
(unless (reduction-relation? r) (assert-rel 'redex-check r)
(raise-type-error 'redex-check "reduction-relation" r))
(values (values
(map rewrite-proc-lhs (reduction-relation-make-procs r)) (map rewrite-proc-lhs (reduction-relation-make-procs r))
(reduction-relation-srcs r) (reduction-relation-srcs r)
(reduction-relation-lang r)))])]) (reduction-relation-lang r)))])])
(check-property-many (check-prop-srcs
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret
'redex-check 'redex-check
show
(test-match lang pat) (test-match lang pat)
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat)))) (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
#`(check-property #`(check-prop
#,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check) #,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check)
property att))) property att show)))
(void))))))])) (void))))))]))
(define (check-property generator property attempts (define (format-attempts a)
#:source [source #f] (format "~a attempt~a" a (if (= 1 a) "" "s")))
#:match [match #f]
#:match-fail [match-fail #f]) (define (check-prop generator property attempts show)
(when (check generator property attempts show)
(show (format "no counterexamples in ~a\n"
(format-attempts attempts)))))
(define (check generator property attempts show
#:source [source #f]
#:match [match #f]
#:match-fail [match-fail #f])
(let loop ([remaining attempts]) (let loop ([remaining attempts])
(if (zero? remaining) (if (zero? remaining)
#t #t
(let ([attempt (add1 (- attempts remaining))]) (let ([attempt (add1 (- attempts remaining))])
(let-values ([(term bindings) (generator (attempt->size attempt) attempt)]) (let-values ([(term bindings) (generator (attempt->size attempt) attempt)])
(if (andmap (λ (bindings) (if (andmap (λ (bindings)
(with-handlers ([exn:fail? (λ (exn) (with-handlers
(fprintf (current-error-port) ([exn:fail?
"checking ~s raises an exception\n" (λ (exn)
term) (show
(raise exn))]) (format "checking ~s raises an exception\n" term))
(raise exn))])
(property term bindings))) (property term bindings)))
(cond [(and match (match term)) (cond [(and match match-fail (match term))
=> (curry map (compose make-bindings match-bindings))] => (curry map (compose make-bindings match-bindings))]
[match (match-fail term)] [match (match-fail term)]
[else (list bindings)])) [else (list bindings)]))
(loop (sub1 remaining)) (loop (sub1 remaining))
(begin (begin
(fprintf (current-output-port) (show
"counterexample found after ~a attempt~a~a:\n" (format "counterexample found after ~a~a:\n"
attempt (format-attempts attempt)
(if (= attempt 1) "" "s") (if source (format " with ~a" source) "")))
(if source (format " with ~a" source) ""))
(pretty-print term (current-output-port)) (pretty-print term (current-output-port))
#f))))))) #f)))))))
@ -811,33 +839,39 @@ To do a better job of not generating programs with free variables,
(parse-kw-args `((#:attempts . ,#'default-check-attempts) (parse-kw-args `((#:attempts . ,#'default-check-attempts)
(#:retries . ,#'default-retries)) (#:retries . ,#'default-retries))
(syntax kw-args) (syntax kw-args)
stx)]) stx)]
[show (show-message stx)])
(syntax/loc stx (syntax/loc stx
(let ([lang (metafunc-proc-lang m)] (let ([lang (metafunc-proc-lang m)]
[dom (metafunc-proc-dom-pat m)] [dom (metafunc-proc-dom-pat m)]
[decisions@ (generation-decisions)] [decisions@ (generation-decisions)]
[att attempts]) [att attempts])
(assert-nat 'check-metafunction-contract att) (assert-nat 'check-metafunction-contract att)
(check-property (check-prop
((generate lang decisions@ retries 'check-metafunction-contract) ((generate lang decisions@ retries 'check-metafunction-contract)
(if dom dom '(any (... ...)))) (if dom dom '(any (... ...))))
(λ (t _) (λ (t _)
(with-handlers ([exn:fail:redex? (λ (_) #f)]) (with-handlers ([exn:fail:redex? (λ (_) #f)])
(begin (term (name ,@t)) #t))) (begin (term (name ,@t)) #t)))
att) att
(void))))])) show))))]))
(define (check-property-many lang pats srcs prop decisions@ attempts retries what [match #f] [match-fail #f]) (define (check-prop-srcs lang pats srcs prop decisions@ attempts retries what show
[match #f]
[match-fail #f])
(let ([lang-gen (generate lang decisions@ retries what)]) (let ([lang-gen (generate lang decisions@ retries what)])
(for/and ([pat pats] [src srcs]) (when (for/and ([pat pats] [src srcs])
(check-property (check
(lang-gen pat) (lang-gen pat)
prop prop
attempts attempts
#:source src show
#:match match #:source src
#:match-fail match-fail)) #:match match
(void))) #:match-fail match-fail))
(show
(format "no counterexamples in ~a (with each clause)\n"
(format-attempts attempts))))))
(define (metafunc-srcs m) (define (metafunc-srcs m)
(build-list (length (metafunc-proc-lhs-pats m)) (build-list (length (metafunc-proc-lhs-pats m))
@ -845,20 +879,19 @@ To do a better job of not generating programs with free variables,
(define-syntax (check-metafunction stx) (define-syntax (check-metafunction stx)
(syntax-case stx () (syntax-case stx ()
[(_ name property)
(syntax/loc stx (check-metafunction name property #:attempts default-check-attempts))]
[(_ name property . kw-args) [(_ name property . kw-args)
(with-syntax ([m (metafunc/err #'name stx)] (with-syntax ([m (metafunc/err #'name stx)]
[(attempts retries) [(attempts retries)
(parse-kw-args `((#:attempts . , #'default-check-attempts) (parse-kw-args `((#:attempts . , #'default-check-attempts)
(#:retries . ,#'default-retries)) (#:retries . ,#'default-retries))
(syntax kw-args) (syntax kw-args)
stx)]) stx)]
[show (show-message stx)])
(syntax/loc stx (syntax/loc stx
(let ([att attempts] (let ([att attempts]
[ret retries]) [ret retries])
(assert-nat 'check-metafunction att) (assert-nat 'check-metafunction att)
(check-property-many (check-prop-srcs
(metafunc-proc-lang m) (metafunc-proc-lang m)
(metafunc-proc-lhs-pats m) (metafunc-proc-lhs-pats m)
(metafunc-srcs m) (metafunc-srcs m)
@ -866,26 +899,39 @@ To do a better job of not generating programs with free variables,
(generation-decisions) (generation-decisions)
att att
ret ret
'check-metafunction))))])) 'check-metafunction
show))))]))
(define (reduction-relation-srcs r) (define (reduction-relation-srcs r)
(map (λ (proc) (or (rewrite-proc-name proc) 'unnamed)) (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
(reduction-relation-make-procs r))) (reduction-relation-make-procs r)))
(define (check-reduction-relation (define-syntax (check-reduction-relation stx)
relation property (syntax-case stx ()
#:decisions [decisions@ random-decisions@] [(_ relation property . kw-args)
#:attempts [attempts default-check-attempts] (with-syntax ([(attempts retries decisions@)
#:retries [retries default-retries]) (parse-kw-args `((#:attempts . , #'default-check-attempts)
(check-property-many (#:retries . ,#'default-retries)
(reduction-relation-lang relation) (#:decisions . ,#'random-decisions@))
(map rewrite-proc-lhs (reduction-relation-make-procs relation)) (syntax kw-args)
(reduction-relation-srcs relation) stx)]
(λ (term _) (property term)) [show (show-message stx)])
decisions@ (syntax/loc stx
attempts (let ([att attempts]
retries [ret retries]
'check-reduction-relation)) [rel relation])
(assert-nat 'check-reduction-relation att)
(assert-rel 'check-reduction-relation rel)
(check-prop-srcs
(reduction-relation-lang rel)
(map rewrite-proc-lhs (reduction-relation-make-procs rel))
(reduction-relation-srcs rel)
(λ (term _) (property term))
decisions@
attempts
retries
'check-reduction-relation
show))))]))
(define-signature decisions^ (define-signature decisions^
(next-variable-decision (next-variable-decision

27
collects/redex/redex.scrbl
View File

@ -1101,11 +1101,12 @@ argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times
[relation-expr reduction-relation?] [relation-expr reduction-relation?]
[retries-expr natural-number/c])]{ [retries-expr natural-number/c])]{
Searches for a counterexample to @scheme[property-expr], interpreted Searches for a counterexample to @scheme[property-expr], interpreted
as a predicate universally quantified over its free as a predicate universally quantified over the pattern variables
@pattech[term]-variables. @scheme[redex-check] chooses substitutions for bound by @scheme[pattern]. @scheme[redex-check] constructs and tests
these free @pattech[term]-variables by generating random terms matching a candidate counterexample by choosing a random term @math{t} that
@scheme[pattern] and extracting the sub-terms bound by the matches @scheme[pattern] then evaluating @scheme[property-expr]
@pattech[names] and non-terminals in @scheme[pattern]. 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]) @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 random terms in its search. The size and complexity of terms it generates
@ -1156,22 +1157,22 @@ term that does not match @scheme[pattern].}
#:attempts 3 #:attempts 3
#:source R))] #:source R))]
@defproc[(check-reduction-relation @defform/subs[(check-reduction-relation relation property kw-args ...)
[relation reduction-relation?] ([kw-arg (code:line #:attempts attempts-expr)
[property (-> any/c any/c)] (code:line #:retries retries-expr)])
[#:attempts attempts natural-number/c 1000] #:contracts ([property (-> any/c any/c)]
[#:retries retries natural-number/c 100]) [attempts-expr natural-number/c]
void?]{ [retries-expr natural-number/c])]{
Tests @scheme[relation] as follows: for each case of @scheme[relation], Tests @scheme[relation] as follows: for each case of @scheme[relation],
@scheme[check-reduction-relation] generates @scheme[attempts] random @scheme[check-reduction-relation] generates @scheme[attempts] random
terms that match that case's left-hand side and applies @scheme[property] terms that match that case's left-hand side and applies @scheme[property]
to each random term. to each random term.
This function provides a more convenient notation for This form provides a more convenient notation for
@schemeblock[(redex-check L any (property (term any)) @schemeblock[(redex-check L any (property (term any))
#:attempts (* n attempts) #:attempts (* n attempts)
#:source relation)] #:source relation)]
when @scheme[relation] is a relation on @scheme[L] and has @scheme[n] rules.} when @scheme[relation] is a relation on @scheme[L] with @scheme[n] rules.}
@defform/subs[(check-metafunction metafunction property kw-args ...) @defform/subs[(check-metafunction metafunction property kw-args ...)
([kw-arg (code:line #:attempts attempts-expr) ([kw-arg (code:line #:attempts attempts-expr)

7
collects/redex/reduction-semantics.ss
View File

@ -45,7 +45,8 @@
(provide redex-check (provide redex-check
generate-term generate-term
check-metafunction check-metafunction
check-metafunction-contract) check-metafunction-contract
check-reduction-relation)
(provide/contract (provide/contract
[current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))] [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
@ -66,10 +67,6 @@
(-> bindings? symbol? (-> any) any))] (-> bindings? symbol? (-> any) any))]
[variable-not-in (any/c symbol? . -> . symbol?)] [variable-not-in (any/c symbol? . -> . symbol?)]
[variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))] [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]
[check-reduction-relation (->* (reduction-relation? (-> any/c any/c))
(#:attempts natural-number/c
#:retries natural-number/c)
(one-of/c #t (void)))]
[relation-coverage (parameter/c (or/c false/c coverage?))] [relation-coverage (parameter/c (or/c false/c coverage?))]
[make-coverage (-> reduction-relation? coverage?)] [make-coverage (-> reduction-relation? coverage?)]
[covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))]) [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))])