From abd035aec2f1f9ebc56757820a409a2b7d9881c3 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Mon, 7 Jun 2010 10:51:31 -0500 Subject: [PATCH] Fixes a bug in the way Redex generates tests to exercise the LHSs of a meta-function or reduction relation. --- collects/redex/private/reduction-semantics.rkt | 12 ++++++------ collects/redex/tests/rg-test.rkt | 13 +++++++++++++ 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index aa16494ca5..cb10860145 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -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 ...) diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index 82321396c7..da279f97fa 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -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+")