Changed redex-check's #:source keyword to always generate from the
LHSs of the metafunction/relation. svn: r13310
This commit is contained in:
Casey Klein
parent
46300fd96e
commit
b86e4473f0
|
|
@ -574,55 +574,58 @@
|
|||
(test m "error: pred-raised")
|
||||
(test (get-output-string p) #rx"checking 5 raises.*\n$")
|
||||
(close-output-port p))
|
||||
(test (parameterize ([check-randomness (make-random 0 0)])
|
||||
(output
|
||||
(λ ()
|
||||
(redex-check lang n (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source (reduction-relation lang (--> 42 x))))))
|
||||
"")
|
||||
|
||||
(test (output
|
||||
(λ ()
|
||||
(parameterize ([check-randomness (make-random 0 0)])
|
||||
(redex-check lang n (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source (reduction-relation lang (--> 0 x z))))))
|
||||
"counterexample found (z) after 1 attempts:\n0\n")
|
||||
(test (output
|
||||
(λ ()
|
||||
(parameterize ([check-randomness (make-random 1)])
|
||||
(redex-check lang d (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source (reduction-relation lang (--> 0 x z))))))
|
||||
"counterexample found after 1 attempts:\n5\n")
|
||||
(test (let ([r (reduction-relation lang (--> 0 x z))])
|
||||
(output
|
||||
(redex-check lang n (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source (reduction-relation
|
||||
lang
|
||||
(--> 42 dontcare)
|
||||
(--> 0 dontcare z)))))
|
||||
"counterexample found after 1 attempts with z:\n0\n")
|
||||
|
||||
(let ([generated null])
|
||||
(test (output
|
||||
(λ ()
|
||||
(redex-check lang n (number? (term n))
|
||||
#:attempts 10
|
||||
#:source r))))
|
||||
"")
|
||||
(redex-check lang n (set! generated (cons (term n) generated))
|
||||
#:attempts 5
|
||||
#:source (reduction-relation
|
||||
lang
|
||||
(--> 1 dontcare)
|
||||
(--> 2 dontcare)))))
|
||||
"")
|
||||
(test generated '(2 2 1 1)))
|
||||
|
||||
(let ()
|
||||
(define-metafunction lang
|
||||
[(mf 0) 0]
|
||||
[(mf 42) 0])
|
||||
(test (parameterize ([check-randomness (make-random 0 1)])
|
||||
(output
|
||||
(λ ()
|
||||
(redex-check lang (n) (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source mf))))
|
||||
""))
|
||||
[(mf 42) dontcare]
|
||||
[(mf 0) dontcare])
|
||||
(test (output
|
||||
(λ ()
|
||||
(redex-check lang (n) (eq? 42 (term n))
|
||||
#:attempts 1
|
||||
#:source mf)))
|
||||
"counterexample found after 1 attempts with clause #2:\n(0)\n"))
|
||||
|
||||
(let ()
|
||||
(define-language L)
|
||||
(test (with-handlers ([exn:fail? exn-message])
|
||||
(redex-check lang any #t #:source (reduction-relation L (--> 1 1))))
|
||||
#rx"language for secondary source"))
|
||||
(define-metafunction lang
|
||||
[(mf d e) dontcare])
|
||||
(test (output
|
||||
(λ ()
|
||||
(redex-check lang (number_1 number_2)
|
||||
(and (= (term number_1) 5)
|
||||
(= (term number_2) 4))
|
||||
#:attempts 1
|
||||
#:source mf)))
|
||||
""))
|
||||
|
||||
(let ()
|
||||
(test (with-handlers ([exn:fail? exn-message])
|
||||
(redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
|
||||
#rx"x does not match n"))
|
||||
|
||||
|
||||
(let ([stx-err (λ (stx)
|
||||
(with-handlers ([exn:fail:syntax? exn-message])
|
||||
(expand stx)
|
||||
|
|
|
|||
|
|
@ -669,8 +669,6 @@ To do a better job of not generating programs with free variables,
|
|||
[(_ lang pat size)
|
||||
(syntax/loc stx (generate-term lang pat size #:attempt 1))]))
|
||||
|
||||
(define check-randomness (make-parameter random))
|
||||
|
||||
(define-syntax (redex-check stx)
|
||||
(syntax-case stx ()
|
||||
[(_ lang pat property . kw-args)
|
||||
|
|
@ -693,57 +691,48 @@ To do a better job of not generating programs with free variables,
|
|||
(with-syntax ([(name ...) names]
|
||||
[(name/ellipses ...) names/ellipses]
|
||||
[attempts (or attempts-stx #'default-check-attempts)])
|
||||
(quasisyntax/loc stx
|
||||
(let ([att attempts])
|
||||
(assert-nat 'redex-check att)
|
||||
(check-property
|
||||
(cons (list #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check) #f)
|
||||
(let ([lang-gen (generate lang random-decisions@)])
|
||||
#,(if (not source-stx)
|
||||
#'null
|
||||
#`(let-values
|
||||
([(pats srcs src-lang)
|
||||
#,(cond [(and (identifier? source-stx) (metafunc source-stx))
|
||||
=>
|
||||
(λ (m) #`(values (metafunc-proc-lhs-pats #,m)
|
||||
(metafunc-srcs #,m)
|
||||
(metafunc-proc-lang #,m)))]
|
||||
[else
|
||||
#`(let ([r #,source-stx])
|
||||
(unless (reduction-relation? r)
|
||||
(raise-type-error 'redex-check "reduction-relation" r))
|
||||
(values
|
||||
(map rewrite-proc-lhs (reduction-relation-make-procs r))
|
||||
(reduction-relation-srcs r)
|
||||
(reduction-relation-lang r)))])])
|
||||
(unless (eq? src-lang lang)
|
||||
(error 'redex-check "language for secondary source must match primary pattern's language"))
|
||||
(zip (map lang-gen pats) srcs)))))
|
||||
#,(and source-stx #'(test-match lang pat))
|
||||
(λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))
|
||||
(λ (_ bindings)
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property))
|
||||
att
|
||||
(λ (term attempt source port)
|
||||
(fprintf port "counterexample found~aafter ~a attempts:\n"
|
||||
(if source (format " (~a) " source) " ") attempt)
|
||||
(pretty-print term port))
|
||||
(check-randomness))
|
||||
(void)))))]))
|
||||
(with-syntax ([property (syntax
|
||||
(λ (_ bindings)
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property)))])
|
||||
(quasisyntax/loc stx
|
||||
(let ([att attempts])
|
||||
(assert-nat 'redex-check att)
|
||||
(unsyntax
|
||||
(if source-stx
|
||||
#`(let-values
|
||||
([(pats srcs src-lang)
|
||||
#,(cond [(and (identifier? source-stx) (metafunc source-stx))
|
||||
=>
|
||||
(λ (m) #`(values (metafunc-proc-lhs-pats #,m)
|
||||
(metafunc-srcs #,m)
|
||||
(metafunc-proc-lang #,m)))]
|
||||
[else
|
||||
#`(let ([r #,source-stx])
|
||||
(unless (reduction-relation? r)
|
||||
(raise-type-error 'redex-check "reduction-relation" r))
|
||||
(values
|
||||
(map rewrite-proc-lhs (reduction-relation-make-procs r))
|
||||
(reduction-relation-srcs r)
|
||||
(reduction-relation-lang r)))])])
|
||||
(check-property-many
|
||||
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats))))
|
||||
(test-match lang pat)
|
||||
(λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))))
|
||||
#`(check-property
|
||||
#,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
|
||||
property att)))
|
||||
(void))))))]))
|
||||
|
||||
(define (check-property gens-srcs match match-fail property attempts display [random random])
|
||||
(define (check-property generator property attempts
|
||||
#:source [source #f]
|
||||
#:match [match #f]
|
||||
#:match-fail [match-fail #f])
|
||||
(let loop ([remaining attempts])
|
||||
(if (zero? remaining)
|
||||
#t
|
||||
(let ([attempt (add1 (- attempts remaining))])
|
||||
(let*-values ([(generator source)
|
||||
(apply values
|
||||
(if (and (not (null? (cdr gens-srcs))) (zero? (random 10)))
|
||||
(pick-from-list (cdr gens-srcs) random)
|
||||
(car gens-srcs)))]
|
||||
[(term bindings)
|
||||
(generator (attempt->size attempt) attempt)])
|
||||
(let-values ([(term bindings) (generator (attempt->size attempt) attempt)])
|
||||
(if (andmap (λ (bindings)
|
||||
(with-handlers ([exn:fail? (λ (exn)
|
||||
(fprintf (current-error-port)
|
||||
|
|
@ -757,7 +746,11 @@ To do a better job of not generating programs with free variables,
|
|||
[else (list bindings)]))
|
||||
(loop (sub1 remaining))
|
||||
(begin
|
||||
(display term attempt source (current-output-port))
|
||||
(fprintf (current-output-port)
|
||||
"counterexample found after ~a attempts~a:\n"
|
||||
attempt
|
||||
(if source (format " with ~a" source) ""))
|
||||
(pretty-print term (current-output-port))
|
||||
#f)))))))
|
||||
|
||||
(define-syntax (check-metafunction-contract stx)
|
||||
|
|
@ -775,32 +768,23 @@ To do a better job of not generating programs with free variables,
|
|||
[att attempts])
|
||||
(assert-nat 'check-metafunction-contract att)
|
||||
(check-property
|
||||
(list (list ((generate lang decisions@) (if dom dom '(any (... ...)))) #f))
|
||||
#f
|
||||
#f
|
||||
((generate lang decisions@) (if dom dom '(any (... ...))))
|
||||
(λ (t _)
|
||||
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
||||
(begin (term (name ,@t)) #t)))
|
||||
att
|
||||
(λ (term attempt _ port)
|
||||
(fprintf port "counterexample found after ~a attempts:\n" attempt)
|
||||
(pretty-print term port)))
|
||||
att)
|
||||
(void))))]))
|
||||
|
||||
(define (check-property-many lang pats srcs prop decisions@ attempts)
|
||||
(define (check-property-many lang pats srcs prop decisions@ attempts [match #f] [match-fail #f])
|
||||
(let ([lang-gen (generate lang decisions@)])
|
||||
(for/and ([pat pats] [src srcs])
|
||||
(check-property
|
||||
(let ([gen (lang-gen pat)])
|
||||
(list (list (λ (size attempt) (gen size attempt)) src)))
|
||||
#f
|
||||
#f
|
||||
(λ (term _) (prop term))
|
||||
(lang-gen pat)
|
||||
prop
|
||||
attempts
|
||||
(λ (term attempt source port)
|
||||
(fprintf port "counterexample found after ~a attempts with ~a:\n"
|
||||
attempt source)
|
||||
(pretty-print term port))))
|
||||
#:source src
|
||||
#:match match
|
||||
#:match-fail match-fail))
|
||||
(void)))
|
||||
|
||||
(define (metafunc-srcs m)
|
||||
|
|
@ -820,7 +804,7 @@ To do a better job of not generating programs with free variables,
|
|||
(metafunc-proc-lang m)
|
||||
(metafunc-proc-lhs-pats m)
|
||||
(metafunc-srcs m)
|
||||
property
|
||||
(λ (term _) (property term))
|
||||
(generation-decisions)
|
||||
att))))]))
|
||||
|
||||
|
|
@ -836,7 +820,7 @@ To do a better job of not generating programs with free variables,
|
|||
(reduction-relation-lang relation)
|
||||
(map rewrite-proc-lhs (reduction-relation-make-procs relation))
|
||||
(reduction-relation-srcs relation)
|
||||
property
|
||||
(λ (term _) (property term))
|
||||
decisions@
|
||||
attempts))
|
||||
|
||||
|
|
@ -868,7 +852,7 @@ To do a better job of not generating programs with free variables,
|
|||
(struct-out ellipsis) (struct-out mismatch) (struct-out class)
|
||||
(struct-out binder) check-metafunction-contract prepare-lang
|
||||
pick-number parse-language check-reduction-relation
|
||||
preferred-production-threshold check-metafunction check-randomness
|
||||
preferred-production-threshold check-metafunction
|
||||
generation-decisions pick-preferred-productions)
|
||||
|
||||
(provide/contract
|
||||
|
|
|
|||
|
|
@ -1058,6 +1058,16 @@ these free @pattech[term]-variables by generating random terms matching
|
|||
@scheme[pattern] and extracting the sub-terms bound by the
|
||||
@pattech[names] and non-terminals in @scheme[pattern].
|
||||
|
||||
@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[100])
|
||||
random terms in its search. The size and complexity of terms it generates
|
||||
gradually increases with each failed attempt.
|
||||
|
||||
When passed a metafunction or reduction relation via the optional @scheme[#:source]
|
||||
argument, @scheme[redex-check] distributes its attempts across the left-hand sides
|
||||
of that metafunction/relation by using those patterns, rather than @scheme[pattern],
|
||||
as the basis of its generation. It is an error if any left-hand side generates a
|
||||
term that does not match @scheme[pattern].}
|
||||
|
||||
@examples[
|
||||
#:eval redex-eval
|
||||
(define-language empty-lang)
|
||||
|
|
@ -1081,27 +1091,37 @@ these free @pattech[term]-variables by generating random terms matching
|
|||
(term (number_2 ...))))
|
||||
(append (reverse (term (number_2 ...)))
|
||||
(reverse (term (number_1 ...)))))
|
||||
#:attempts 200)]
|
||||
#:attempts 200)
|
||||
|
||||
@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[100])
|
||||
random terms in its search. The size and complexity of terms it generates
|
||||
gradually increases with each failed attempt.
|
||||
|
||||
When the optional @scheme[#:source] argument is present, @scheme[redex-check]
|
||||
generates @math{10%} of its terms by randomly choosing a pattern from the
|
||||
left-hand sides the definition of the supplied metafunction or relation.
|
||||
@scheme[redex-check] raises an exception if a term generated from an alternate
|
||||
pattern does not match the @scheme[pattern].}
|
||||
(let ([R (reduction-relation
|
||||
empty-lang
|
||||
(--> (Σ) 0)
|
||||
(--> (Σ number) number)
|
||||
(--> (Σ number_1 number_2 number_3 ...)
|
||||
(Σ ,(+ (term number_1) (term number_2))
|
||||
number_3 ...)))])
|
||||
(redex-check
|
||||
empty-lang
|
||||
(Σ number ...)
|
||||
(printf "~s\n" (term (number ...)))
|
||||
#:attempts 3
|
||||
#:source R))]
|
||||
|
||||
@defproc[(check-reduction-relation
|
||||
[relation reduction-relation?]
|
||||
[property (-> any/c any/c)]
|
||||
[#:attempts attempts natural-number/c 100])
|
||||
void?]{
|
||||
Tests a @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
|
||||
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
|
||||
@schemeblock[(redex-check L any (property (term any))
|
||||
#:attempts (* n attempts)
|
||||
#:source relation)]
|
||||
when @scheme[relation] is a relation on @scheme[L] and has @scheme[n] rules.}
|
||||
|
||||
@defform*[[(check-metafunction metafunction property)
|
||||
(check-metafunction metafunction property #:attempts attempts)]
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user