The term generator now increases the size bound and attempt number
when it is having trouble satisfying a pattern. svn: r13422
This commit is contained in:
Casey Klein
parent
61419caf8b
commit
8f03dea7c3
|
|
@ -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"))
|
||||
|
|
|
|||
|
|
@ -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?)])
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user