suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixes a bug in the way Redex generates tests to exercise the LHSs of a

Browse Source 
meta-function or reduction relation.
This commit is contained in:
Casey Klein 2010-06-07 10:51:31 -05:00
parent 93d7ec9446
commit abd035aec2
2 changed files with 19 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
collects/redex/private/reduction-semantics.rkt
View File

@ -259,12 +259,12 @@
#,rest-body))))
mtchs))]
[(predicate)
#`(andmap (λ (mtch)
(let ([bindings (mtch-bindings mtch)])
(let ([x (lookup-binding bindings 'names)] ...)
(term-let ([names/ellipses x] ...)
#,rest-body))))
mtchs)]
#`(ormap (λ (mtch)
(let ([bindings (mtch-bindings mtch)])
(let ([x (lookup-binding bindings 'names)] ...)
(term-let ([names/ellipses x] ...)
#,rest-body))))
mtchs)]
[else (error 'unknown-where-mode "~s" where-mode)])
#f))))))]
[((-side-condition s ...) y ...)

13
collects/redex/tests/rg-test.rkt
View File

@ -862,6 +862,19 @@
(check-metafunction f (λ (_) #t)))
4)
(let ()
(define-language L
((m n) number))
(define-metafunction L
[(f m_0 m_1 ...)
()
(where (n_0 ... n_i ...) (m_0 m_1 ...))
(side-condition (null? (term (n_0 ...))))])
(test
(with-handlers ([exn:fail:redex:generation-failure? (λ (_) #f)])
(check-metafunction f (λ (_) #t) #:retries 1 #:print? #f #:attempts 1))
#t))
(test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
(test (output (λ () (check-metafunction m (curry eq? 1))))
#px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")