diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss index b335676808..0a29eccc60 100644 --- a/collects/redex/private/rg.ss +++ b/collects/redex/private/rg.ss @@ -152,11 +152,11 @@ who what attempts (if (= attempts 1) "" "s"))]) (raise (make-exn:fail:redex:generation-failure str (current-continuation-marks))))) -(define (generate lang decisions@ retries what) +(define (generate lang decisions@ what) (define-values/invoke-unit decisions@ (import) (export decisions^)) - (define ((generate-nt lang base-cases generate) + (define ((generate-nt lang base-cases generate retries) name cross? size attempt in-hole env) (let*-values ([(term _) @@ -171,7 +171,7 @@ ((next-non-terminal-decision) name cross? lang attempt)))]) (generate (max 0 (sub1 size)) attempt empty-env in-hole (rhs-pattern rhs)))) (λ (_ env) (mismatches-satisfied? env)) - size attempt)]) + size attempt retries)]) term)) (define (generate-sequence ellipsis generate env length) @@ -197,18 +197,18 @@ (values (cons term terms) (cons env envs)))))]) (values seq (merge-environments envs)))) - (define (generate/pred name gen pred init-sz init-att) + (define (generate/pred name gen pred init-sz init-att retries) (let ([pre-threshold-incr (ceiling (/ (- retry-threshold init-att) - (* proportion-before-threshold retries)))] + (* proportion-before-threshold (add1 retries))))] [incr-size? (λ (remain) (zero? (modulo (sub1 remain) (ceiling (* proportion-at-size retries)))))]) - (let retry ([remaining retries] + (let retry ([remaining (add1 retries)] [size init-sz] [attempt init-att]) (if (zero? remaining) @@ -254,18 +254,19 @@ (cons (make-bind (binder-name key) val) bindings) bindings)))) - (define (generate-pat lang sexp size attempt env in-hole pat) - (define recur (curry generate-pat lang sexp size attempt)) + (define (generate-pat lang sexp retries size attempt env in-hole pat) + (define recur (curry generate-pat lang sexp retries size attempt)) (define recur/pat (recur env in-hole)) (define ((recur/pat/size-attempt pat) size attempt) - (generate-pat lang sexp size attempt env in-hole pat)) + (generate-pat lang sexp retries size attempt env in-hole pat)) (define clang (rg-lang-clang lang)) (define gen-nt (generate-nt clang (rg-lang-base-cases lang) - (curry generate-pat lang sexp))) + (curry generate-pat lang sexp retries) + retries)) (match pat [`number (values ((next-number-decision) attempt) env)] @@ -276,7 +277,7 @@ (generate/pred 'variable (recur/pat/size-attempt 'variable) (λ (var _) (not (memq var vars))) - size attempt)] + size attempt retries)] [`variable (values ((next-variable-decision) (rg-lang-lits lang) attempt) env)] @@ -284,7 +285,7 @@ (generate/pred 'variable (recur/pat/size-attempt 'variable) (λ (var _) (not (memq var (compiled-lang-literals clang)))) - size attempt)] + size attempt retries)] [`(variable-prefix ,prefix) (define (symbol-append prefix suffix) (string->symbol (string-append (symbol->string prefix) (symbol->string suffix)))) @@ -297,7 +298,7 @@ (generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc) (recur/pat/size-attempt pat) (λ (_ env) (condition (bindings env))) - size attempt)] + size attempt retries)] [`(name ,(? symbol? id) ,p) (let-values ([(term env) (recur/pat p)]) (values term (hash-set env (make-binder id) term)))] @@ -310,6 +311,7 @@ (let*-values ([(new-lang nt) ((next-any-decision) lang sexp)] [(term _) (generate-pat new-lang sexp + retries size attempt empty-env @@ -354,7 +356,7 @@ [rg-sexp (prepare-lang sexp)]) (λ (pat) (let ([parsed (reassign-classes (parse-pattern pat lang 'top-level))]) - (λ (size attempt) + (λ (size attempt retries) (let-values ([(term env) (generate/pred pat @@ -362,13 +364,14 @@ (generate-pat rg-lang rg-sexp + retries size attempt empty-env the-hole parsed)) (λ (_ env) (mismatches-satisfied? env)) - size attempt)]) + size attempt retries)]) (values term (bindings env)))))))) (define-struct base-cases (cross non-cross)) @@ -640,34 +643,35 @@ x (raise-type-error 'redex-check "reduction-relation" x))) -(define (defer-all pat size in-hole acc env att recur defer) - (defer acc)) - -(define-for-syntax (term-generator lang pat decisions@ retries what) +(define-for-syntax (term-generator lang pat decisions@ what) (with-syntax ([pattern (rewrite-side-conditions/check-errs (language-id-nts lang what) what #t pat)]) - #`((generate #,lang #,decisions@ #,retries '#,what) `pattern))) + #`((generate #,lang #,decisions@ '#,what) `pattern))) (define-syntax (generate-term stx) (syntax-case stx () - [(_ lang pat size . kw-args) + [(name lang pat size . kw-args) (with-syntax ([(attempt retries) - (parse-kw-args `((#:attempt . 1) + (parse-kw-args `((#:attempt-num . 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))])) + (syntax/loc stx + ((generate-term lang pat) size #:attempt-num attempt #:retries retries)))] + [(name lang pat) + (with-syntax ([make-gen (term-generator #'lang + #'pat + #'(generation-decisions) + #'name)]) + (syntax/loc stx + (let ([generate make-gen]) + (λ (size #:attempt-num [attempt-num 1] #:retries [retries default-retries]) + (let ([att (assert-nat 'name attempt-num)] + [ret (assert-nat 'name retries)]) + (let-values ([(term _) (generate size att ret)]) + term))))))])) (define-for-syntax (show-message stx) (syntax-case stx () @@ -728,19 +732,19 @@ (test-match lang pat) (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat)))) #`(check-prop - #,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check) - property att show))) + #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check) + property att ret show))) (void))))))])) (define (format-attempts a) (format "~a attempt~a" a (if (= 1 a) "" "s"))) -(define (check-prop generator property attempts show) - (when (check generator property attempts show) +(define (check-prop generator property attempts retries show) + (when (check generator property attempts retries show) (show (format "no counterexamples in ~a\n" (format-attempts attempts))))) -(define (check generator property attempts show +(define (check generator property attempts retries show #:source [source #f] #:match [match #f] #:match-fail [match-fail #f]) @@ -748,7 +752,7 @@ (if (zero? remaining) #t (let ([attempt (add1 (- attempts remaining))]) - (let-values ([(term bindings) (generator (attempt->size attempt) attempt)]) + (let-values ([(term bindings) (generator (attempt->size attempt) attempt retries)]) (if (andmap (λ (bindings) (with-handlers ([exn:fail? @@ -787,18 +791,19 @@ [decisions@ (generation-decisions)] [att (assert-nat 'check-metafunction-contract attempts)]) (check-prop - ((generate lang decisions@ retries 'check-metafunction-contract) + ((generate lang decisions@ 'check-metafunction-contract) (if dom dom '(any (... ...)))) (λ (t _) (with-handlers ([exn:fail:redex? (λ (_) #f)]) (begin (term (name ,@t)) #t))) att + retries show))))])) (define (check-lhs-pats lang mf/rr 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@ what)]) (let-values ([(pats srcs) (cond [(metafunc-proc? mf/rr) (values (map metafunc-case-lhs-pat (metafunc-proc-cases mf/rr)) @@ -815,6 +820,7 @@ (lang-gen pat) prop attempts + retries show #:source src #:match match diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index a66ca1287a..9eb594b227 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1127,30 +1127,37 @@ metafunctions or unnamed reduction-relation cases) to application counts.} (values (covered-cases equals-coverage) (covered-cases plus-coverage))))] -@defform/subs[(generate-term language @#,ttpattern size-exp kw-args ...) - ([kw-args (code:line #:attempts attempts-expr) +@defform*/subs[[(generate-term language @#,ttpattern size-expr kw-args ...) + (generate-term language @#,ttpattern)] + ([kw-args (code:line #:attempt-num 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). + +In its first form, @scheme[generate-term] produces a random term matching +the given pattern (according to the given language). In its second, +@scheme[generate-term] produces a procedure for constructing the same. +This procedure expects @scheme[size-expr] (below) as its sole positional +argument and allows the same optional keyword arguments as the first form. +The second form may be more efficient when generating many terms. 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). +(measured as the height of its parse tree). The optional keyword argument @scheme[attempt-num-expr] (default @scheme[1]) provides coarse grained control over the random -decisions made during generation. For example, the expected length of -@pattech[pattern-sequence]s increases with @scheme[attempt-num-expr]. +decisions made during generation; increasing @scheme[attempt-num-expr] +tends to increase the complexity of the result. 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 +imposed by @pattech[side-condition] or @tt{_!_} @|pattern|s; instead, +it uses a ``guess and check'' strategy in which it freely generates +candidate terms then tests whether they happen to satisfy the constraints, +repeating as 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 pattern. If @scheme[generate-term] is unable to produce a satisfying term after @scheme[retries-expr] attempts, it raises an exception recognized by @scheme[exn:fail:redex:generation-failure?].} diff --git a/collects/redex/tests/rg-test.ss b/collects/redex/tests/rg-test.ss index af11812cef..881d82bb74 100644 --- a/collects/redex/tests/rg-test.ss +++ b/collects/redex/tests/rg-test.ss @@ -167,7 +167,7 @@ (syntax-rules () [(_ lang pat size attempt decisions) (parameterize ([generation-decisions decisions]) - (generate-term lang pat size #:attempt attempt))])) + (generate-term lang pat size #:attempt-num attempt))])) (let () (define-language lc @@ -197,6 +197,13 @@ #:var (list (λ _ 'x) (λ _ 'y)))) '(x y))) +(let () + (define-language L + (n 1)) + (test ((generate-term L n) 0) 1) + (test ((generate-term L n) 0 #:retries 0) 1) + (test ((generate-term L n) 0 #:attempt-num 0) 1)) + ;; variable-except pattern (let () (define-language var @@ -212,17 +219,17 @@ (n natural) (i integer) (r real)) - (test (let ([n (generate-term L n 0 #:attempt 10000)]) + (test (let ([n (generate-term L n 0 #:attempt-num 10000)]) (and (integer? n) (exact? n) (not (negative? n)))) #t) (test (generate-term/decisions L n 0 1 (decisions #:nat (λ (_) 42))) 42) - (test (let ([i (generate-term L i 0 #:attempt 10000)]) + (test (let ([i (generate-term L i 0 #:attempt-num 10000)]) (and (integer? i) (exact? i))) #t) (test (generate-term/decisions L i 0 1 (decisions #:int (λ (_) -42))) -42) - (test (real? (generate-term L r 0 #:attempt 10000)) #t) + (test (real? (generate-term L r 0 #:attempt-num 10000)) #t) (test (generate-term/decisions L r 0 1 (decisions #:real (λ (_) 4.2))) 4.2)) (let () diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt index df047febe0..8ade9006d4 100644 --- a/doc/release-notes/redex/HISTORY.txt +++ b/doc/release-notes/redex/HISTORY.txt @@ -1,3 +1,5 @@ + * Renamed the #:attempts keyword #:attempt-num in the `generate-term' form + v4.2.4 * minor bug fixes