From cf78ce0c6ea3469b656a9b863329db672af9d13c Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Wed, 10 Apr 2013 12:59:15 -0500 Subject: [PATCH] redex: elminate another #f/failure confusion (cherry picked from commit 468d2b192e833747feaa3cac0726bac515c11ddb) --- collects/redex/private/search.rkt | 2 +- collects/redex/tests/gen-test.rkt | 33 +++++++++++++++++++++++-------- 2 files changed, 26 insertions(+), 9 deletions(-) diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt index 5ee682fee2..e396349a84 100644 --- a/collects/redex/private/search.rkt +++ b/collects/redex/private/search.rkt @@ -186,7 +186,7 @@ [(cons (eqn lhs rhs) rest) (eqn lhs rhs) (define u-res (unify lhs rhs e lang)) - (and u-res + (and (not-failed? u-res) (loop (p*e-e u-res) rest))]))] [else #f])])) diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 061a3c21de..9005df37d3 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -15,8 +15,9 @@ (define-syntax-rule (is-false e) (test e #f)) +(define-language L0) + (let () - (define-language L0) (test (check-dq (dq '() (list `a `a)) (make-hash) L0 (hash)) #f) @@ -590,7 +591,6 @@ (g))))) (let () - (define-language L0) (define-relation L0 [(a any)]) (define-relation L0 @@ -629,9 +629,6 @@ (let () - - (define-language L0) - (define-relation L0 [(R number) number] @@ -677,7 +674,6 @@ (is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5))) (let () - (define-language L0) (define-metafunction L0 [(f (any_1 any_2)) @@ -713,7 +709,6 @@ [else #t])))) (let () - (define-language L0) (define-relation L0 [(R (#f #f #f) 3)] @@ -754,4 +749,26 @@ #:satisfying (R #f any) +inf.0)) - ) \ No newline at end of file + ) + +(let () + + (define-relation L0 + [(not-mem any_1 (any_2 any_3)) + (not-mem any_1 any_3) + (where (any_!_4 any_!_4) (any_1 any_2))] + [(not-mem any_1 ())]) + + (is-not-false + (generate-term + L0 + #:satisfying + (not-mem d (a (b (c ())))) + +inf.0)) + + (is-false + (generate-term + L0 + #:satisfying + (not-mem b (a (b (c ())))) + +inf.0))) \ No newline at end of file