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

Exported and documented the term generator's public interface.

Browse Source 
svn: r13053
This commit is contained in:
Casey Klein 2009-01-09 21:53:53 +00:00
parent 1edd3544d7
commit 65fad6047d
5 changed files with 152 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -504,62 +504,62 @@
(get-output-string p)
(close-output-port p))))
;; check
;; redex-check
(let ()
(define-language lang
(d 5)
(e e 4)
(n number))
(test (current-output (λ () (check lang d #f)))
(test (current-output (λ () (redex-check lang d #f)))
"counterexample found after 1 attempts:\n5\n")
(test (check lang d #t) #t)
(test (check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
(test (check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
(test (current-output (λ () (check lang (d e) #f)))
(test (redex-check lang d #t) #t)
(test (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
(test (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
(test (current-output (λ () (redex-check lang (d e) #f)))
"counterexample found after 1 attempts:\n(5 4)\n")
(test (current-output (λ () (check lang d (error 'pred-raised))))
(test (current-output (λ () (redex-check lang d (error 'pred-raised))))
"counterexample found after 1 attempts:\n5\n")
(test (parameterize ([check-randomness (make-random 0 0)])
(check lang n (eq? 42 (term n))
#:attempts 1
#:source (reduction-relation lang (--> 42 x))))
(redex-check lang n (eq? 42 (term n))
#:attempts 1
#:source (reduction-relation lang (--> 42 x))))
#t)
(test (current-output
(λ ()
(parameterize ([check-randomness (make-random 0 0)])
(check lang n (eq? 42 (term n))
#:attempts 1
#:source (reduction-relation lang (--> 0 x z))))))
(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 (current-output
(λ ()
(parameterize ([check-randomness (make-random 1)])
(check lang d (eq? 42 (term n))
#:attempts 1
#:source (reduction-relation lang (--> 0 x z))))))
(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))])
(check lang n (number? (term n))
#:attempts 10
#:source r))
(redex-check lang n (number? (term n))
#:attempts 10
#:source r))
#t)
(let ()
(define-metafunction lang
[(mf 0) 0]
[(mf 42) 0])
(test (parameterize ([check-randomness (make-random 0 1)])
(check lang (n) (eq? 42 (term n))
#:attempts 1
#:source mf))
(redex-check lang (n) (eq? 42 (term n))
#:attempts 1
#:source mf))
#t))
(let ()
(define-language L)
(test (with-handlers ([exn:fail? exn-message])
(check lang any #t #:source (reduction-relation L (--> 1 1))))
(redex-check lang any #t #:source (reduction-relation L (--> 1 1))))
#rx"language for secondary source"))
(let ()
(test (with-handlers ([exn:fail? exn-message])
(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"))
(let ([stx-err (λ (stx)
@ -570,15 +570,15 @@
(eval '(require "../reduction-semantics.ss"
"rg.ss"))
(eval '(define-language empty))
(test (stx-err '(check empty any #t #:typo 3))
#rx"check: bad keyword syntax")
(test (stx-err '(check empty any #t #:attempts 3 #:attempts 4))
(test (stx-err '(redex-check empty any #t #:typo 3))
#rx"redex-check: bad keyword syntax")
(test (stx-err '(redex-check empty any #t #:attempts 3 #:attempts 4))
#rx"bad keyword syntax")
(test (stx-err '(check empty any #t #:attempts))
(test (stx-err '(redex-check empty any #t #:attempts))
#rx"bad keyword syntax")
(test (stx-err '(check empty any #t #:attempts 3 4))
(test (stx-err '(redex-check empty any #t #:attempts 3 4))
#rx"bad keyword syntax")
(test (stx-err '(check empty any #t #:source #:attempts))
(test (stx-err '(redex-check empty any #t #:source #:attempts))
#rx"bad keyword syntax"))))
;; check-metafunction-contract

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

@ -655,11 +655,12 @@ To do a better job of not generating programs with free variables,
(define check-randomness (make-parameter random))
(define-syntax (check stx)
(define-syntax (redex-check stx)
(syntax-case stx ()
[(_ lang pat property . kw-args)
(let-values ([(names names/ellipses)
(extract-names (language-id-nts #'lang 'check) 'check #t #'pat)]
(extract-names (language-id-nts #'lang 'redex-check)
'redex-check #t #'pat)]
[(attempts-stx source-stx)
(let loop ([args (syntax kw-args)]
[attempts #f]
@ -678,9 +679,9 @@ To do a better job of not generating programs with free variables,
[attempts (or attempts-stx #'default-check-attempts)])
(quasisyntax/loc stx
(let ([att attempts])
(assert-nat 'check att)
(assert-nat 'redex-check att)
(or (check-property
(cons (list #,(term-generator #'lang #'pat #'random-decisions 'check) #f)
(cons (list #,(term-generator #'lang #'pat #'random-decisions 'redex-check) #f)
(let ([lang-gen (generate lang (random-decisions lang))])
#,(if (not source-stx)
#'null
@ -694,16 +695,16 @@ To do a better job of not generating programs with free variables,
[else
#`(let ([r #,source-stx])
(unless (reduction-relation? r)
(raise-type-error 'check "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 'check "language for secondary source must match primary pattern's language"))
(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 'check "~s does not match ~s" generated 'pat))
(λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))
(λ (_ bindings)
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
property))
@ -842,7 +843,7 @@ To do a better job of not generating programs with free variables,
(define generation-decisions (make-parameter random-decisions))
(provide pick-from-list pick-var min-prods decisions^ pick-sequence-length
is-nt? pick-char random-string pick-string check nt-by-name
is-nt? pick-char random-string pick-string redex-check nt-by-name
pick-nt unique-chars pick-any sexp generate-term parse-pattern
class-reassignments reassign-classes unparse-pattern
(struct-out ellipsis) (struct-out mismatch) (struct-out class)

2
collects/redex/private/tl-test.ss
View File

@ -1,7 +1,5 @@
(module tl-test mzscheme
(require "../reduction-semantics.ss"
(only "reduction-semantics.ss"
relation-coverage make-coverage covered-cases)
"test-util.ss"
(only "matcher.ss" make-bindings make-bind)
scheme/match

102
collects/redex/redex.scrbl
View File

@ -47,9 +47,12 @@
#'((tech "term") args ...)]
[x (identifier? #'x) #'(tech "term")]))
@(define redex-eval (make-base-eval))
@(interaction-eval #:eval redex-eval (require redex/reduction-semantics))
@title{@bold{Redex}: Debugging Operational Semantics}
@author["Robert Bruce Findler"]
@author["Robert Bruce Findler" "Casey Klein"]
PLT Redex consists of a domain-specific language for specifying
reduction semantics, plus a suite of tools for working with the
@ -982,6 +985,103 @@ counters so that next time this function is called, it
prints the test results for the next round of tests.
}
@defproc[(make-coverage [r reduction-relation?]) coverage?]{
Constructs a structure to contain the per-case test coverage of
the relation @scheme[r]. Use with @scheme[relation-coverage]
and @scheme[covered-cases].
}
@defproc[(coverage? [v any/c]) boolean?]{
Returns @scheme[#t] for a value produced by @scheme[make-coverage]
and @scheme[#f] for any other.}
@defparam[relation-coverage c (or/c false/c coverage?)]{
When @scheme[c] is a @scheme[coverage] structure, rather than
@scheme[#f] (the default), procedures such as
@scheme[apply-reduction-relation], @scheme[traces], etc. count
the number applications of each case of the
@scheme[reduction-relation], storing the results in @scheme[c].
}
@defproc[(covered-cases
[c coverage?])
(listof (cons/c string? natural-number/c))]{
Extracts the coverage information recorded in @scheme[c], producing
an association list mapping names to application counts.}
@examples[
#:eval redex-eval
(define-language addition
(e (+ number ...)))
(define reduce
(reduction-relation
addition
(--> (+) 0 "zero")
(--> (+ number) number)
(--> (+ number_1 number_2 number ...)
(+ ,(+ (term number_1) (term number_2))
number ...)
"add")))
(let ([coverage (make-coverage reduce)])
(parameterize ([relation-coverage coverage])
(apply-reduction-relation* reduce (term (+ 1 2 3)))
(covered-cases coverage)))]
@defform*[[(generate-term language #, @|ttpattern| size-exp)
(generate-term language #, @|ttpattern| size-exp #:attempt attempt-num-expr)]
#:contracts ([size-expr natural-number/c]
[attempt-num-expr natural-number/c])]{
Generates a random term matching @scheme[pattern] (in the given language).
The argument @scheme[size-expr] bounds the height of the generated term
(measured as the height of the derivation tree used to produce
the term).
The optional keyword argument @scheme[attempt-num-expr]
(default @scheme[1]) provides coarse grained control over the random
decisions made during generation (e.g., the expected length of
@pattech[pattern-sequence]s increases with @scheme[attempt-num-expr]).}
@defform/subs[(check language #, @|ttpattern| property-expr kw-arg ...)
([kw-arg (code:line #:attempts attempts-expr)
(code:line #:source metafunction)
(code:line #:source relation-expr)])
#:contracts ([property-expr any/c]
[attempts-expr natural-number/c]
[relation-expr reduction-relation?])]{
Searches for a counterexample to @scheme[property-expr], interpreted
as a predicate universally quantified over its free
@pattech[term]-variables. @scheme[check] chooses substitutions for
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[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[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[check] raises an exception if a term generated from an alternate
pattern does not match the @scheme[pattern].}
@defproc[(check-reduction-relation
[relation reduction-relation?]
[property (-> any/c any/c)]
[#:attempts attempts natural-number/c 100])
(or/c true/c void?)]{
Tests a @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.}
@defform*[[(check-metafunction metafunction property)
(check-metafunction metafunction property #:attempts attempts)]
#:contracts ([property (-> any/c any/c)]
[attempts natural-number/c])]{
Like @scheme[check-reduction-relation] but for metafunctions.}
@deftech{Debugging PLT Redex Programs}
It is easy to write grammars and reduction rules that are

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

@ -7,8 +7,6 @@
"private/rg.ss"
"private/error.ss")
#;(provide (all-from-out "private/rg.ss"))
(provide exn:fail:redex?) ;; from error.ss
(provide reduction-relation
@ -43,6 +41,11 @@
test-predicate
test-results)
(provide redex-check
generate-term
check-metafunction
check-metafunction-contract)
(provide/contract
[current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
[reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
@ -61,4 +64,10 @@
(-> bindings? symbol? any)
(-> bindings? symbol? (-> any) any))]
[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)
(one-of/c #t (void)))]
[relation-coverage (parameter/c (or/c false/c coverage?))]
[make-coverage (-> reduction-relation? coverage?)]
[covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))])