Improved the error reported when the term generate is unable to

satisfy a pattern.

svn: r13464
This commit is contained in:
Casey Klein 2009-02-06 12:04:40 +00:00
parent 6d4b1025b5
commit fba31b310a
2 changed files with 67 additions and 33 deletions

View File

@ -4,7 +4,8 @@
"reduction-semantics.ss"
"matcher.ss"
"term.ss"
"rg.ss")
"rg.ss"
"error.ss")
(reset-count)
@ -113,10 +114,11 @@
(test (pick-nt 'b L null preferred-production-threshold #f)
(nt-rhs (cadr (compiled-lang-lang L)))))
(define-syntax exn:fail-message
(define-syntax raised-exn-msg
(syntax-rules ()
[(_ expr)
(with-handlers ([exn:fail? exn-message])
[(_ expr) (raised-exn-msg exn:fail? expr)]
[(_ exn? expr)
(with-handlers ([exn? exn-message])
(begin
expr
(let ()
@ -139,7 +141,7 @@
(let ([iter (iterator 'test-iterator '(a b))])
(test (iter) 'a)
(test (iter) 'b)
(test (exn:fail-message (iter)) #rx"empty"))
(test (raised-exn-msg (iter)) #rx"empty"))
(define (decisions #:var [var pick-var]
#:nt [nt pick-nt]
@ -216,7 +218,7 @@
(e (e e) x (e (x) λ) #:binds x e)
(x (variable-except λ)))
(test
(exn:fail-message
(raised-exn-msg
(generate-term/decisions
postfix e 2 0
(decisions #:var (list (λ _ 'x) (λ _ 'y))
@ -256,8 +258,8 @@
null)
(test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
'(4 4 4 4 (4 4) (4 4)))
(test (exn:fail-message (generate-term lang e 5))
#rx"generate: unable to generate pattern e")
(test (raised-exn-msg exn:fail:redex? (generate-term lang e 5))
#rx"generate-term: unable to generate pattern e")
(test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
(test (generate-term/decisions
lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
@ -336,7 +338,7 @@
(decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
'(1 1 2))
(test
(exn:fail-message (generate-term lang b 5000))
(raised-exn-msg exn:fail:redex? (generate-term lang b 5000))
#rx"unable"))
(let ()
@ -361,7 +363,7 @@
(x variable))
(test (generate-term lang b 5) 43)
(test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
(test (exn:fail-message (generate-term lang c 5))
(test (raised-exn-msg exn:fail:redex? (generate-term lang c 5))
#rx"unable to generate")
(test ; binding works for with side-conditions failure/retry
(let/ec k
@ -661,10 +663,14 @@
""))
(let ()
(test (with-handlers ([exn:fail? exn-message])
(test (raised-exn-msg
exn:fail:redex?
(redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
#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])
@ -704,6 +710,10 @@
(define-metafunction empty
[(i any ...) (any ...)])
(define-metafunction empty
j : (side-condition any #f) -> any
[(j any ...) (any ...)])
;; Dom(f) < Ctc(f)
(test (output
(λ ()
@ -729,7 +739,13 @@
;; OK -- generated from Dom(h)
(test (output (λ () (check-metafunction-contract h))) "")
;; OK -- generated from pattern (any ...)
(test (output (λ () (check-metafunction-contract i #:attempts 5))) ""))
(test (output (λ () (check-metafunction-contract i #:attempts 5))) "")
;; Unable to generate domain
(test (raised-exn-msg
exn:fail:redex?
(check-metafunction-contract j #:attempts 1))
#rx"^check-metafunction-contract: unable"))
;; check-reduction-relation
(let ()
@ -781,7 +797,13 @@
T (curry equal? '(9 4))
#:attempts 1
#:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))))
"")))
""))
(let ([U (reduction-relation L (--> (side-condition any #f) any))])
(test (raised-exn-msg
exn:fail:redex?
(check-reduction-relation U (λ (_) #t)))
#rx"^check-reduction-relation: unable")))
; check-metafunction
(let ()
@ -789,6 +811,8 @@
(define-metafunction empty
[(m 1) whatever]
[(m 2) whatever])
(define-metafunction empty
[(n (side-condition any #f)) any])
(let ([generated null])
(test (begin
(check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)
@ -797,9 +821,14 @@
(test (output (λ () (check-metafunction m (λ (_) #t)))) "")
(test (output (λ () (check-metafunction m (curry eq? 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"))
(test (raised-exn-msg
exn:fail:contract?
(check-metafunction m (λ (_) #t) #:attempts 'NaN))
#rx"check-metafunction: expected")
(test (raised-exn-msg
exn:fail:redex?
(check-metafunction n (λ (_) #t)))
#rx"check-metafunction: unable"))
;; parse/unparse-pattern
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])

View File

@ -179,7 +179,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@)
(define (generate lang decisions@ what)
(define-values/invoke-unit decisions@
(import) (export decisions^))
@ -241,7 +241,7 @@ To do a better job of not generating programs with free variables,
[size init-sz]
[attempt init-att])
(if (zero? remaining)
(error 'generate "unable to generate pattern ~s in ~a attempt~a"
(redex-error what "unable to generate pattern ~s in ~a attempt~a"
name
generation-retries
(if (= generation-retries 1) "" "s"))
@ -377,7 +377,7 @@ To do a better job of not generating programs with free variables,
[(rest-term state) (recur state in-hole rest)])
(values (cons pat-term rest-term) state))]
[else
(error 'generate "unknown pattern ~s\n" pat)]))
(error what "unknown pattern ~s\n" pat)]))
(define (extract-bound-vars pat state)
(let loop ([found-vars-table (state-fvt state)])
@ -400,7 +400,7 @@ To do a better job of not generating programs with free variables,
(cons res (found-vars-bound-vars found-vars))
#f)])
(when (found-vars-found-nt? found-vars)
(error 'generate "kludge in #:binds was exposed! #:binds ~s ~s"
(error what "kludge in #:binds was exposed! #:binds ~s ~s"
(found-vars-nt found-vars)
(found-vars-source found-vars)))
new-found-vars)]
@ -687,8 +687,9 @@ To do a better job of not generating programs with free variables,
(language-id-nts lang what)
what #t pat)]
[lang lang]
[decisions@ decisions@])
(syntax ((generate lang decisions@) `pattern))))
[decisions@ decisions@]
[what what])
(syntax ((generate lang decisions@ 'what) `pattern))))
(define-syntax (generate-term stx)
(syntax-case stx ()
@ -748,8 +749,9 @@ To do a better job of not generating programs with free variables,
(reduction-relation-lang r)))])])
(check-property-many
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats))))
'redex-check
(test-match lang pat)
(λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))))
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
#`(check-property
#,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
property att)))
@ -800,15 +802,16 @@ 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@) (if dom dom '(any (... ...))))
((generate lang decisions@ 'check-metafunction-contract)
(if dom dom '(any (... ...))))
(λ (t _)
(with-handlers ([exn:fail:redex? (λ (_) #f)])
(begin (term (name ,@t)) #t)))
att)
(void))))]))
(define (check-property-many lang pats srcs prop decisions@ attempts [match #f] [match-fail #f])
(let ([lang-gen (generate lang decisions@)])
(define (check-property-many lang pats srcs prop decisions@ attempts what [match #f] [match-fail #f])
(let ([lang-gen (generate lang decisions@ what)])
(for/and ([pat pats] [src srcs])
(check-property
(lang-gen pat)
@ -838,7 +841,8 @@ To do a better job of not generating programs with free variables,
(metafunc-srcs m)
(λ (term _) (property term))
(generation-decisions)
att))))]))
att
'check-metafunction))))]))
(define (reduction-relation-srcs r)
(map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
@ -854,7 +858,8 @@ To do a better job of not generating programs with free variables,
(reduction-relation-srcs relation)
(λ (term _) (property term))
decisions@
attempts))
attempts
'check-reduction-relation))
(define-signature decisions^
(next-variable-decision