diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss index 2d8554c3f0..f00d02b262 100644 --- a/collects/redex/private/rg-test.ss +++ b/collects/redex/private/rg-test.ss @@ -500,6 +500,46 @@ #:var (list (λ _ 'x) (λ _ 'y)))) (term (λ (x) (hole y))))) +;; generation failures increase size and attempt +(let () + (define-language L + (a d b) + (b d c) + (c e) + + (x variable)) + (test + (generate-term/decisions + L (side-condition a (eq? (term a) 'e)) 0 0 + ; It isn't possible for `a' to generate 'y until size is 2. + ; When size is 0, the generator has no choice but the 'x production. + ; When size is 1, the generator has a choice for `a' but not for `b'. + ; Supply enough first-production choices to cover the size 1 attempts + ; 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) + (λ (_) first)) + (list second second first))))) + 'e) + + (test + (generate-term/decisions + L (side-condition x (number? (term x))) 0 0 + (decisions #:var (λ (lang-chars lang-lits bound-vars attempt) + (if (>= attempt retry-threshold) 0 'x)))) + 0) + + (let ([attempts null] + [start (sub1 retry-threshold)] + [finish (+ retry-threshold post-threshold-incr)]) + (generate-term/decisions + L (side-condition x (number? (term x))) 0 start + (decisions #:var (λ (lang-chars lang-lits bound-vars attempt) + (set! attempts (cons attempt attempts)) + (if (= attempt finish) 0 'x)))) + (test attempts (list finish retry-threshold start)))) + ;; preferred productions (let ([make-pick-nt (λ opt (λ req (apply pick-nt (append req opt))))]) (define-language L @@ -558,14 +598,14 @@ (e e 4) (n number)) (test (output (λ () (redex-check lang d #f))) - "counterexample found after 1 attempts:\n5\n") + "counterexample found after 1 attempt:\n5\n") (test (output (λ () (redex-check lang d #t))) "") (test (output (λ () (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2))) "") (test (output (λ () (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2))) "") (test (output (λ () (redex-check lang (d e) #f))) - "counterexample found after 1 attempts:\n(5 4)\n") + "counterexample found after 1 attempt:\n(5 4)\n") (let* ([p (open-output-string)] [m (parameterize ([current-error-port p]) (with-handlers ([exn:fail? exn-message]) @@ -583,7 +623,7 @@ lang (--> 42 dontcare) (--> 0 dontcare z))))) - "counterexample found after 1 attempts with z:\n0\n") + "counterexample found after 1 attempt with z:\n0\n") (let ([generated null]) (test (output @@ -606,7 +646,7 @@ (redex-check lang (n) (eq? 42 (term n)) #:attempts 1 #:source mf))) - "counterexample found after 1 attempts with clause #2:\n(0)\n")) + "counterexample found after 1 attempt with clause #2:\n(0)\n")) (let () (define-metafunction lang @@ -670,14 +710,14 @@ (parameterize ([generation-decisions (decisions #:num (list (λ _ 2) (λ _ 5)))]) (check-metafunction-contract f)))) - "counterexample found after 1 attempts:\n(5)\n") + "counterexample found after 1 attempt:\n(5)\n") ;; Rng(f) > Codom(f) (test (output (λ () (parameterize ([generation-decisions (decisions #:num (list (λ _ 3)))]) (check-metafunction-contract f)))) - "counterexample found after 1 attempts:\n(3)\n") + "counterexample found after 1 attempt:\n(3)\n") ;; LHS matches multiple ways (test (output (λ () @@ -685,7 +725,7 @@ (decisions #:num (list (λ _ 1) (λ _ 1)) #:seq (list (λ _ 2)))]) (check-metafunction-contract g)))) - "counterexample found after 1 attempts:\n(1 1)\n") + "counterexample found after 1 attempt:\n(1 1)\n") ;; OK -- generated from Dom(h) (test (output (λ () (check-metafunction-contract h))) "") ;; OK -- generated from pattern (any ...) @@ -720,10 +760,10 @@ (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) "") (test (output (λ () (check-reduction-relation S (λ (x) #f)))) - "counterexample found after 1 attempts with name:\n1\n") + "counterexample found after 1 attempt with name:\n1\n") (test (output (λ () (check-reduction-relation S (curry eq? 1)))) - "counterexample found after 1 attempts with unnamed:\n3\n")) + "counterexample found after 1 attempt with unnamed:\n3\n")) (let ([T (reduction-relation L @@ -756,7 +796,7 @@ (reverse '((1) (2))))) (test (output (λ () (check-metafunction m (λ (_) #t)))) "") (test (output (λ () (check-metafunction m (curry eq? 1)))) - #rx"counterexample found after 1 attempts with clause #1") + #rx"counterexample found after 1 attempt with clause #1") (test (with-handlers ([exn:fail:contract? exn-message]) (check-metafunction m #t #:attempts 'NaN)) #rx"check-metafunction: expected")) diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss index b3d6657a4c..4c7d63dbf8 100644 --- a/collects/redex/private/rg.ss +++ b/collects/redex/private/rg.ss @@ -42,16 +42,12 @@ To do a better job of not generating programs with free variables, (hash-set! uniq char #t))) (hash-map uniq (λ (k v) k)))) -(define generation-retries 100) - (define default-check-attempts 1000) (define ascii-chars-threshold 50) (define tex-chars-threshold 500) (define chinese-chars-threshold 2000) -(define preferred-production-threshold 3000) - (define (pick-var lang-chars lang-lits bound-vars attempt [random random]) (if (or (null? bound-vars) (allow-free-var? random)) (let ([length (add1 (random-natural 4/5 random))]) @@ -137,6 +133,15 @@ 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 retry-threshold (max chinese-chars-threshold complex-threshold)) +(define proportion-before-threshold 9/10) +(define proportion-at-size 1/10) +(define post-threshold-incr 50) + +(define preferred-production-threshold + (+ retry-threshold 2000)) + ;; Determines the parameter p for which random-natural's expected value is E (define (expected-value->p E) ;; E = 0 => p = 1, which breaks random-natural @@ -185,7 +190,7 @@ To do a better job of not generating programs with free variables, [(term _) (generate/pred name - (λ () + (λ (size attempt) (let ([rhs (pick-from-list (if (zero? size) (min-prods (nt-by-name lang name) base-table) @@ -193,7 +198,8 @@ To do a better job of not generating programs with free variables, (generate bound-vars (max 0 (sub1 size)) attempt (make-state (map fvt-entry (rhs-var-info rhs)) #hash()) in-hole (rhs-pattern rhs)))) - (λ (_ env) (mismatches-satisfied? env)))]) + (λ (_ env) (mismatches-satisfied? env)) + size attempt)]) (values term (extend-found-vars fvt-id term state)))) (define (generate-sequence ellipsis generate state length) @@ -220,17 +226,34 @@ To do a better job of not generating programs with free variables, (values (cons term terms) (cons (state-env state) envs) fvt))))]) (values seq (make-state fvt (merge-environments envs))))) - (define (generate/pred name gen pred) - (let retry ([remaining generation-retries]) - (if (zero? remaining) - (error 'generate "unable to generate pattern ~s in ~a attempt~a" - name - generation-retries - (if (= generation-retries 1) "" "s")) - (let-values ([(term state) (gen)]) - (if (pred term (state-env state)) - (values term state) - (retry (sub1 remaining))))))) + (define (generate/pred name gen pred init-sz init-att) + (let ([pre-threshold-incr + (ceiling + (/ (- retry-threshold init-att) + (* proportion-before-threshold generation-retries)))] + [incr-size? + (λ (remain) + (zero? + (modulo (sub1 remain) + (ceiling (* proportion-at-size + generation-retries)))))]) + (let retry ([remaining generation-retries] + [size init-sz] + [attempt init-att]) + (if (zero? remaining) + (error 'generate "unable to generate pattern ~s in ~a attempt~a" + name + generation-retries + (if (= generation-retries 1) "" "s")) + (let-values ([(term state) (gen size attempt)]) + (if (pred term (state-env state)) + (values term state) + (retry (sub1 remaining) + (if (incr-size? remaining) (add1 size) size) + (+ attempt + (if (>= attempt retry-threshold) + post-threshold-incr + pre-threshold-incr))))))))) (define (generate/prior name state generate) (let* ([none (gensym)] @@ -273,6 +296,8 @@ To do a better job of not generating programs with free variables, (define (generate-pat lang sexp pref-prods bound-vars size attempt state in-hole pat) (define recur (curry generate-pat lang sexp pref-prods bound-vars size attempt)) (define recur/pat (recur state in-hole)) + (define ((recur/pat/size-attempt pat) size attempt) + (generate-pat lang sexp pref-prods bound-vars size attempt state in-hole pat)) (define clang (rg-lang-clang lang)) (define gen-nt (generate-nt @@ -285,16 +310,18 @@ To do a better job of not generating programs with free variables, [`number (values ((next-number-decision) attempt) state)] [`(variable-except ,vars ...) (generate/pred 'variable - (λ () (recur/pat 'variable)) - (λ (var _) (not (memq var vars))))] + (recur/pat/size-attempt 'variable) + (λ (var _) (not (memq var vars))) + size attempt)] [`variable (values ((next-variable-decision) (rg-lang-chars lang) (rg-lang-lits lang) bound-vars attempt) state)] [`variable-not-otherwise-mentioned (generate/pred 'variable - (λ () (recur/pat 'variable)) - (λ (var _) (not (memq var (compiled-lang-literals clang)))))] + (recur/pat/size-attempt 'variable) + (λ (var _) (not (memq var (compiled-lang-literals clang)))) + size attempt)] [`(variable-prefix ,prefix) (define (symbol-append prefix suffix) (string->symbol (string-append (symbol->string prefix) (symbol->string suffix)))) @@ -305,8 +332,9 @@ To do a better job of not generating programs with free variables, state)] [`(side-condition ,pat ,(? procedure? condition)) (generate/pred (unparse-pattern pat) - (λ () (recur/pat pat)) - (λ (_ env) (condition (bindings env))))] + (recur/pat/size-attempt pat) + (λ (_ env) (condition (bindings env))) + size attempt)] [`(name ,(? symbol? id) ,p) (let-values ([(term state) (recur/pat p)]) (values term (set-env state (make-binder id) term)))] @@ -393,11 +421,12 @@ To do a better job of not generating programs with free variables, (let-values ([(term state) (generate/pred pat - (λ () + (λ (size attempt) (generate-pat rg-lang rg-sexp ((next-pref-prods-decision) (rg-lang-clang rg-lang)) null size attempt new-state the-hole parsed)) - (λ (_ env) (mismatches-satisfied? env)))]) + (λ (_ env) (mismatches-satisfied? env)) + size attempt)]) (values term (bindings (state-env state))))))))) ;; find-base-cases : compiled-language -> hash-table @@ -856,7 +885,9 @@ To do a better job of not generating programs with free variables, (struct-out binder) check-metafunction-contract prepare-lang pick-number parse-language check-reduction-relation preferred-production-threshold check-metafunction - generation-decisions pick-preferred-productions) + generation-decisions pick-preferred-productions + generation-retries proportion-at-size retry-threshold + proportion-before-threshold post-threshold-incr) (provide/contract [find-base-cases (-> compiled-lang? hash?)])