Added a #retries keyword to the forms that generate random terms.
svn: r13484
This commit is contained in:
parent
12560f3a23
commit
6d5f966019
46
collects/redex/private/keyword-macros-test.ss
Normal file
46
collects/redex/private/keyword-macros-test.ss
Normal file
|
@ -0,0 +1,46 @@
|
|||
#lang scheme
|
||||
|
||||
(require "keyword-macros.ss"
|
||||
"test-util.ss")
|
||||
|
||||
(reset-count)
|
||||
|
||||
(let* ([formals `((#:b . ,#'1) (#:c . ,#'2))]
|
||||
[parse
|
||||
(λ (actuals)
|
||||
(map syntax-e
|
||||
(parse-kw-args formals (cdr (syntax-e actuals)) actuals)))])
|
||||
(let-syntax ([msg-src
|
||||
(syntax-rules ()
|
||||
[(_ expr)
|
||||
(with-handlers ([exn:fail:syntax?
|
||||
(λ (exn)
|
||||
(values (exn-message exn)
|
||||
(exn:fail:syntax-exprs exn)))])
|
||||
(begin expr (values 'no-msg 'no-src)))])])
|
||||
(let ()
|
||||
(test (parse #'(a #:c 3 #:b 4)) '(4 3))
|
||||
(test (parse #'(a #:b 4 #:c 3)) '(4 3))
|
||||
(test (parse #'(a #:c 3)) '(1 3))
|
||||
(let*-values ([(kw) #'#:b]
|
||||
[(msg src) (msg-src (parse #`(a #,kw)))])
|
||||
(test msg #rx"a: missing argument expression after keyword")
|
||||
(test src (list kw)))
|
||||
(let*-values ([(arg) #'1]
|
||||
[(msg src) (msg-src (parse #`(a #:b 1 #,arg)))])
|
||||
(test msg #rx"a: expected a keyword")
|
||||
(test src (list arg)))
|
||||
(let*-values ([(kw) #'#:c]
|
||||
[(msg src) (msg-src (parse #`(a #:c 1 #:b 2 #,kw 3)))])
|
||||
(test msg #rx"a: repeated keyword")
|
||||
(test src (list kw)))
|
||||
(let*-values ([(kw) #'#:c]
|
||||
[(msg src) (msg-src (parse #`(a #:b #,kw 3)))])
|
||||
(test msg #rx"a: expected an argument expression")
|
||||
(test src (list kw)))
|
||||
(let*-values ([(kw) #'#:typo]
|
||||
[(msg src) (msg-src (parse #`(a #:b 3 #,kw 4)))])
|
||||
(test msg #rx"a: invalid keyword")
|
||||
(test src (list kw))))))
|
||||
|
||||
(print-tests-passed 'keyword-macros-test.ss)
|
28
collects/redex/private/keyword-macros.ss
Normal file
28
collects/redex/private/keyword-macros.ss
Normal file
|
@ -0,0 +1,28 @@
|
|||
#lang scheme
|
||||
|
||||
(define (parse-kw-args formals actuals source)
|
||||
(let loop ([current (for/hash ([arg formals]) (values (car arg) #f))]
|
||||
[rest actuals])
|
||||
(syntax-case rest ()
|
||||
[() (map (λ (arg) (or (hash-ref current (car arg)) (cdr arg))) formals)]
|
||||
[(kw . rest)
|
||||
(not (keyword? (syntax-e (syntax kw))))
|
||||
(raise-syntax-error #f "expected a keyword" source (syntax kw))]
|
||||
[(kw arg . rest)
|
||||
(keyword? (syntax-e (syntax arg)))
|
||||
(raise-syntax-error #f "expected an argument expression" source (syntax arg))]
|
||||
[(kw arg . rest)
|
||||
(let ([none (gensym)])
|
||||
(eq? none (hash-ref current (syntax-e (syntax kw)) none)))
|
||||
(raise-syntax-error #f "invalid keyword" source (syntax kw))]
|
||||
[(kw arg . rest)
|
||||
(hash-ref current (syntax-e (syntax kw)))
|
||||
(raise-syntax-error #f "repeated keyword" source (syntax kw))]
|
||||
[(kw)
|
||||
(raise-syntax-error #f "missing argument expression after keyword" source (syntax kw))]
|
||||
[(kw arg . rest)
|
||||
(loop (hash-set current (syntax-e (syntax kw)) (syntax arg))
|
||||
(syntax rest))]
|
||||
[else (raise-syntax-error #f "bad keyword argument syntax" source rest)])))
|
||||
|
||||
(provide parse-kw-args)
|
|
@ -5,6 +5,7 @@
|
|||
"matcher.ss"
|
||||
"term.ss"
|
||||
"rg.ss"
|
||||
"keyword-macros.ss"
|
||||
"error.ss")
|
||||
|
||||
(reset-count)
|
||||
|
@ -258,8 +259,8 @@
|
|||
null)
|
||||
(test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
|
||||
'(4 4 4 4 (4 4) (4 4)))
|
||||
(test (raised-exn-msg exn:fail:redex? (generate-term lang e 5))
|
||||
#rx"generate-term: unable to generate pattern e")
|
||||
(test (raised-exn-msg exn:fail:redex? (generate-term lang e 5 #:retries 42))
|
||||
#rx"generate-term: unable to generate pattern e in 42")
|
||||
(test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
|
||||
(test (generate-term/decisions
|
||||
lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
|
@ -520,7 +521,7 @@
|
|||
; followed by the choices that produce 'y on the first size 2 attempt.
|
||||
(decisions
|
||||
#:nt (apply patterns
|
||||
(append (build-list (* generation-retries proportion-at-size)
|
||||
(append (build-list (* default-retries proportion-at-size)
|
||||
(λ (_) first))
|
||||
(list second second first)))))
|
||||
'e)
|
||||
|
@ -669,27 +670,17 @@
|
|||
#rx"x does not match n"))
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex?
|
||||
(redex-check lang (side-condition any #f) #t #:attempts 1))
|
||||
#rx"^redex-check: unable")
|
||||
|
||||
(let ([stx-err (λ (stx)
|
||||
(with-handlers ([exn:fail:syntax? exn-message])
|
||||
(expand stx)
|
||||
'no-syntax-error))])
|
||||
(parameterize ([current-namespace (make-base-namespace)])
|
||||
(eval '(require "../reduction-semantics.ss"
|
||||
"rg.ss"))
|
||||
(eval '(define-language empty))
|
||||
(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 '(redex-check empty any #t #:attempts))
|
||||
#rx"bad keyword syntax")
|
||||
(test (stx-err '(redex-check empty any #t #:attempts 3 4))
|
||||
#rx"bad keyword syntax")
|
||||
(test (stx-err '(redex-check empty any #t #:source #:attempts))
|
||||
#rx"bad keyword syntax"))))
|
||||
(redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
|
||||
#rx"^redex-check: unable .* in 42")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex?
|
||||
(redex-check lang any #t
|
||||
#:source (reduction-relation
|
||||
lang
|
||||
(--> (side-condition any #f) any))
|
||||
#:retries 42
|
||||
#:attempts 1))
|
||||
#rx"^redex-check: unable .* in 42"))
|
||||
|
||||
;; check-metafunction-contract
|
||||
(let ()
|
||||
|
@ -744,8 +735,8 @@
|
|||
;; Unable to generate domain
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex?
|
||||
(check-metafunction-contract j #:attempts 1))
|
||||
#rx"^check-metafunction-contract: unable"))
|
||||
(check-metafunction-contract j #:attempts 1 #:retries 42))
|
||||
#rx"^check-metafunction-contract: unable .* in 42"))
|
||||
|
||||
;; check-reduction-relation
|
||||
(let ()
|
||||
|
@ -827,8 +818,8 @@
|
|||
#rx"check-metafunction: expected")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex?
|
||||
(check-metafunction n (λ (_) #t)))
|
||||
#rx"check-metafunction: unable"))
|
||||
(check-metafunction n (λ (_) #t) #:retries 42))
|
||||
#rx"check-metafunction: unable .* in 42"))
|
||||
|
||||
;; parse/unparse-pattern
|
||||
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
|
||||
|
|
|
@ -24,6 +24,7 @@ To do a better job of not generating programs with free variables,
|
|||
(for-syntax "rewrite-side-conditions.ss")
|
||||
(for-syntax "term-fn.ss")
|
||||
(for-syntax "reduction-semantics.ss")
|
||||
(for-syntax "keyword-macros.ss")
|
||||
mrlib/tex-table)
|
||||
|
||||
(define (allow-free-var? [random random]) (= 0 (random 30)))
|
||||
|
@ -133,7 +134,7 @@ To do a better job of not generating programs with free variables,
|
|||
(define real-threshold 1000)
|
||||
(define complex-threshold 2000)
|
||||
|
||||
(define generation-retries 100)
|
||||
(define default-retries 100)
|
||||
(define retry-threshold (max chinese-chars-threshold complex-threshold))
|
||||
(define proportion-before-threshold 9/10)
|
||||
(define proportion-at-size 1/10)
|
||||
|
@ -179,7 +180,7 @@ To do a better job of not generating programs with free variables,
|
|||
(let ([lits (map symbol->string (compiled-lang-literals lang))])
|
||||
(make-rg-lang (parse-language lang) lits (unique-chars lits) (find-base-cases lang))))
|
||||
|
||||
(define (generate lang decisions@ what)
|
||||
(define (generate lang decisions@ retries what)
|
||||
(define-values/invoke-unit decisions@
|
||||
(import) (export decisions^))
|
||||
|
||||
|
@ -230,21 +231,21 @@ To do a better job of not generating programs with free variables,
|
|||
(let ([pre-threshold-incr
|
||||
(ceiling
|
||||
(/ (- retry-threshold init-att)
|
||||
(* proportion-before-threshold generation-retries)))]
|
||||
(* proportion-before-threshold retries)))]
|
||||
[incr-size?
|
||||
(λ (remain)
|
||||
(zero?
|
||||
(modulo (sub1 remain)
|
||||
(ceiling (* proportion-at-size
|
||||
generation-retries)))))])
|
||||
(let retry ([remaining generation-retries]
|
||||
retries)))))])
|
||||
(let retry ([remaining retries]
|
||||
[size init-sz]
|
||||
[attempt init-att])
|
||||
(if (zero? remaining)
|
||||
(redex-error what "unable to generate pattern ~s in ~a attempt~a"
|
||||
name
|
||||
generation-retries
|
||||
(if (= generation-retries 1) "" "s"))
|
||||
retries
|
||||
(if (= retries 1) "" "s"))
|
||||
(let-values ([(term state) (gen size attempt)])
|
||||
(if (pred term (state-env state))
|
||||
(values term state)
|
||||
|
@ -681,23 +682,25 @@ To do a better job of not generating programs with free variables,
|
|||
(unless (and (integer? x) (>= x 0))
|
||||
(raise-type-error name "natural number" x)))
|
||||
|
||||
(define-for-syntax (term-generator lang pat decisions@ what)
|
||||
(define-for-syntax (term-generator lang pat decisions@ retries what)
|
||||
(with-syntax ([pattern
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts lang what)
|
||||
what #t pat)]
|
||||
[lang lang]
|
||||
[decisions@ decisions@]
|
||||
[what what])
|
||||
(syntax ((generate lang decisions@ 'what) `pattern))))
|
||||
what #t pat)])
|
||||
#`((generate #,lang #,decisions@ #,retries '#,what) `pattern)))
|
||||
|
||||
(define-syntax (generate-term stx)
|
||||
(syntax-case stx ()
|
||||
[(_ lang pat size #:attempt attempt)
|
||||
(with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) 'generate-term)])
|
||||
(syntax/loc stx
|
||||
(let-values ([(term _) (generate size attempt)])
|
||||
term)))]
|
||||
[(_ lang pat size . kw-args)
|
||||
(with-syntax ([(attempt retries)
|
||||
(parse-kw-args `((#:attempt . 1)
|
||||
(#:retries . ,#'default-retries))
|
||||
(syntax kw-args)
|
||||
stx)])
|
||||
(with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) #'retries 'generate-term)])
|
||||
(syntax/loc stx
|
||||
(let-values ([(term _) (generate size attempt)])
|
||||
term))))]
|
||||
[(_ lang pat size)
|
||||
(syntax/loc stx (generate-term lang pat size #:attempt 1))]))
|
||||
|
||||
|
@ -707,29 +710,26 @@ To do a better job of not generating programs with free variables,
|
|||
(let-values ([(names names/ellipses)
|
||||
(extract-names (language-id-nts #'lang 'redex-check)
|
||||
'redex-check #t #'pat)]
|
||||
[(attempts-stx source-stx)
|
||||
(let loop ([args (syntax kw-args)]
|
||||
[attempts #f]
|
||||
[source #f])
|
||||
(syntax-case args ()
|
||||
[() (values attempts source)]
|
||||
[(#:attempts a . rest)
|
||||
(not (or attempts (keyword? (syntax-e #'a))))
|
||||
(loop #'rest #'a source)]
|
||||
[(#:source s . rest)
|
||||
(not (or source (keyword? (syntax-e #'s))))
|
||||
(loop #'rest attempts #'s)]
|
||||
[else (raise-syntax-error #f "bad keyword syntax" stx args)]))])
|
||||
[(attempts-stx source-stx retries-stx)
|
||||
(apply values
|
||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||
(#:source . #f)
|
||||
(#:retries . ,#'default-retries))
|
||||
(syntax kw-args)
|
||||
stx))])
|
||||
(with-syntax ([(name ...) names]
|
||||
[(name/ellipses ...) names/ellipses]
|
||||
[attempts (or attempts-stx #'default-check-attempts)])
|
||||
[attempts attempts-stx]
|
||||
[retries retries-stx])
|
||||
(with-syntax ([property (syntax
|
||||
(λ (_ bindings)
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property)))])
|
||||
(quasisyntax/loc stx
|
||||
(let ([att attempts])
|
||||
(let ([att attempts]
|
||||
[ret retries])
|
||||
(assert-nat 'redex-check att)
|
||||
(assert-nat 'redex-check ret)
|
||||
(unsyntax
|
||||
(if source-stx
|
||||
#`(let-values
|
||||
|
@ -748,12 +748,12 @@ To do a better job of not generating programs with free variables,
|
|||
(reduction-relation-srcs r)
|
||||
(reduction-relation-lang r)))])])
|
||||
(check-property-many
|
||||
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats))))
|
||||
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret
|
||||
'redex-check
|
||||
(test-match lang pat)
|
||||
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
|
||||
#`(check-property
|
||||
#,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
|
||||
#,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check)
|
||||
property att)))
|
||||
(void))))))]))
|
||||
|
||||
|
@ -789,12 +789,14 @@ To do a better job of not generating programs with free variables,
|
|||
|
||||
(define-syntax (check-metafunction-contract stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name)
|
||||
(syntax/loc stx
|
||||
(check-metafunction-contract name #:attempts default-check-attempts))]
|
||||
[(_ name #:attempts attempts)
|
||||
[(_ name . kw-args)
|
||||
(identifier? #'name)
|
||||
(with-syntax ([m (metafunc/err #'name stx)])
|
||||
(with-syntax ([m (metafunc/err #'name stx)]
|
||||
[(attempts retries)
|
||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||
(#:retries . ,#'default-retries))
|
||||
(syntax kw-args)
|
||||
stx)])
|
||||
(syntax/loc stx
|
||||
(let ([lang (metafunc-proc-lang m)]
|
||||
[dom (metafunc-proc-dom-pat m)]
|
||||
|
@ -802,7 +804,7 @@ To do a better job of not generating programs with free variables,
|
|||
[att attempts])
|
||||
(assert-nat 'check-metafunction-contract att)
|
||||
(check-property
|
||||
((generate lang decisions@ 'check-metafunction-contract)
|
||||
((generate lang decisions@ retries 'check-metafunction-contract)
|
||||
(if dom dom '(any (... ...))))
|
||||
(λ (t _)
|
||||
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
||||
|
@ -810,8 +812,8 @@ To do a better job of not generating programs with free variables,
|
|||
att)
|
||||
(void))))]))
|
||||
|
||||
(define (check-property-many lang pats srcs prop decisions@ attempts what [match #f] [match-fail #f])
|
||||
(let ([lang-gen (generate lang decisions@ what)])
|
||||
(define (check-property-many lang pats srcs prop decisions@ attempts retries what [match #f] [match-fail #f])
|
||||
(let ([lang-gen (generate lang decisions@ retries what)])
|
||||
(for/and ([pat pats] [src srcs])
|
||||
(check-property
|
||||
(lang-gen pat)
|
||||
|
@ -830,10 +832,16 @@ To do a better job of not generating programs with free variables,
|
|||
(syntax-case stx ()
|
||||
[(_ name property)
|
||||
(syntax/loc stx (check-metafunction name property #:attempts default-check-attempts))]
|
||||
[(_ name property #:attempts attempts)
|
||||
(with-syntax ([m (metafunc/err #'name stx)])
|
||||
[(_ name property . kw-args)
|
||||
(with-syntax ([m (metafunc/err #'name stx)]
|
||||
[(attempts retries)
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries))
|
||||
(syntax kw-args)
|
||||
stx)])
|
||||
(syntax/loc stx
|
||||
(let ([att attempts])
|
||||
(let ([att attempts]
|
||||
[ret retries])
|
||||
(assert-nat 'check-metafunction att)
|
||||
(check-property-many
|
||||
(metafunc-proc-lang m)
|
||||
|
@ -842,6 +850,7 @@ To do a better job of not generating programs with free variables,
|
|||
(λ (term _) (property term))
|
||||
(generation-decisions)
|
||||
att
|
||||
ret
|
||||
'check-metafunction))))]))
|
||||
|
||||
(define (reduction-relation-srcs r)
|
||||
|
@ -851,7 +860,8 @@ To do a better job of not generating programs with free variables,
|
|||
(define (check-reduction-relation
|
||||
relation property
|
||||
#:decisions [decisions@ random-decisions@]
|
||||
#:attempts [attempts default-check-attempts])
|
||||
#:attempts [attempts default-check-attempts]
|
||||
#:retries [retries default-retries])
|
||||
(check-property-many
|
||||
(reduction-relation-lang relation)
|
||||
(map rewrite-proc-lhs (reduction-relation-make-procs relation))
|
||||
|
@ -859,6 +869,7 @@ To do a better job of not generating programs with free variables,
|
|||
(λ (term _) (property term))
|
||||
decisions@
|
||||
attempts
|
||||
retries
|
||||
'check-reduction-relation))
|
||||
|
||||
(define-signature decisions^
|
||||
|
@ -891,7 +902,7 @@ To do a better job of not generating programs with free variables,
|
|||
pick-number parse-language check-reduction-relation
|
||||
preferred-production-threshold check-metafunction
|
||||
generation-decisions pick-preferred-productions
|
||||
generation-retries proportion-at-size retry-threshold
|
||||
default-retries proportion-at-size retry-threshold
|
||||
proportion-before-threshold post-threshold-incr)
|
||||
|
||||
(provide/contract
|
||||
|
|
|
@ -9,6 +9,7 @@
|
|||
"tl-test.ss"
|
||||
"term-test.ss"
|
||||
"rg-test.ss"
|
||||
"keyword-macros-test.ss"
|
||||
"core-layout-test.ss"
|
||||
"bitmap-test.ss"
|
||||
"pict-test.ss"))
|
||||
|
|
|
@ -1029,10 +1029,12 @@ an association list mapping names to application counts.}
|
|||
(apply-reduction-relation* equals (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])]{
|
||||
@defform/subs[(generate-term language #, @|ttpattern| size-exp kw-args ...)
|
||||
([kw-args (code:line #:attempts attempts-expr)
|
||||
(code:line #:retries retries-expr)])
|
||||
#:contracts ([size-expr natural-number/c]
|
||||
[attempt-num-expr natural-number/c]
|
||||
[retries-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
|
||||
|
@ -1041,16 +1043,28 @@ 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]).}
|
||||
decisions made during generation. For example, the expected length of
|
||||
@pattech[pattern-sequence]s increases with @scheme[attempt-num-expr].
|
||||
|
||||
The random generation process does not actively consider the constraints
|
||||
imposed by @pattech[side-condition] or @tt{_!_} @|pattern|s when
|
||||
constructing a term; instead, it tests the satisfaction of
|
||||
such constraints after it freely generates the relevant portion of the
|
||||
sub-term---regenerating the sub-term if necessary. The optional keyword
|
||||
argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times that
|
||||
@scheme[generate-term] retries the generation of any sub-term. If
|
||||
@scheme[generate-term] is unable to produce a satisfying term after
|
||||
@scheme[retries-expr] attempts, it raises an error}
|
||||
|
||||
@defform/subs[(redex-check language #, @|ttpattern| property-expr kw-arg ...)
|
||||
([kw-arg (code:line #:attempts attempts-expr)
|
||||
(code:line #:source metafunction)
|
||||
(code:line #:source relation-expr)])
|
||||
(code:line #:source relation-expr)
|
||||
(code:line #:retries retries-expr)])
|
||||
#:contracts ([property-expr any/c]
|
||||
[attempts-expr natural-number/c]
|
||||
[relation-expr reduction-relation?])]{
|
||||
[relation-expr reduction-relation?]
|
||||
[retries-expr natural-number/c])]{
|
||||
Searches for a counterexample to @scheme[property-expr], interpreted
|
||||
as a predicate universally quantified over its free
|
||||
@pattech[term]-variables. @scheme[redex-check] chooses substitutions for
|
||||
|
@ -1058,7 +1072,7 @@ 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])
|
||||
@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
|
||||
gradually increases with each failed attempt.
|
||||
|
||||
|
@ -1110,7 +1124,8 @@ term that does not match @scheme[pattern].}
|
|||
@defproc[(check-reduction-relation
|
||||
[relation reduction-relation?]
|
||||
[property (-> any/c any/c)]
|
||||
[#:attempts attempts natural-number/c 100])
|
||||
[#:attempts attempts natural-number/c 1000]
|
||||
[#:retries retries natural-number/c])
|
||||
void?]{
|
||||
Tests @scheme[relation] as follows: for each case of @scheme[relation],
|
||||
@scheme[check-reduction-relation] generates @scheme[attempts] random
|
||||
|
@ -1123,10 +1138,12 @@ This function provides a more convenient notation for
|
|||
#: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)]
|
||||
#:contracts ([property (-> any/c any/c)]
|
||||
[attempts natural-number/c])]{
|
||||
@defform/subs[(check-metafunction metafunction property kw-args ...)
|
||||
([kw-arg (code:line #:attempts attempts-expr)
|
||||
(code:line #:retries retries-expr)])
|
||||
#:contracts ([property (-> any/c any/c)]
|
||||
[attempts-expr natural-number/c]
|
||||
[retries-expr natural-number/c])]{
|
||||
Like @scheme[check-reduction-relation] but for metafunctions.}
|
||||
|
||||
@deftech{Debugging PLT Redex Programs}
|
||||
|
|
|
@ -66,7 +66,8 @@
|
|||
[variable-not-in (any/c symbol? . -> . symbol?)]
|
||||
[variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]
|
||||
[check-reduction-relation (->* (reduction-relation? (-> any/c any/c))
|
||||
(#:attempts natural-number/c)
|
||||
(#:attempts natural-number/c
|
||||
#:retries natural-number/c)
|
||||
(one-of/c #t (void)))]
|
||||
[relation-coverage (parameter/c (or/c false/c coverage?))]
|
||||
[make-coverage (-> reduction-relation? coverage?)]
|
||||
|
|
Loading…
Reference in New Issue
Block a user