From 495e5c94cf85b76c25c4bfe9e98f1ae916abd0b4 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Mon, 8 Apr 2013 15:03:01 -0500 Subject: [PATCH] redex: bug fix for gerating terms including #f please include in the release --- collects/redex/private/generate-term.rkt | 8 ++--- collects/redex/private/jdg-gen.rkt | 35 ++++++++++-------- collects/redex/private/pat-unify.rkt | 16 +++++---- collects/redex/private/search.rkt | 8 ++--- collects/redex/tests/gen-test.rkt | 46 +++++++++++++++++++++++- collects/redex/tests/unify-tests.rkt | 28 ++++++++------- 6 files changed, 98 insertions(+), 43 deletions(-) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index ed180a31e8..96fd940aad 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -501,9 +501,9 @@ (define gen (search/next (mk-clauses) pat size lang)) (define (termify search-res) (cond - [search-res + [(not-failed? search-res) (define exp (pat->term lang (p*e-p search-res) (p*e-e search-res))) - (and exp + (and (not-failed? exp) (cons jf-id exp))] [else #f])) (λ () @@ -516,11 +516,11 @@ size lang)) (define (termify res) - (and res + (and (not-failed? res) (match res [(p*e lhs+rhs env) (define lhs+rhs-term (pat->term lang lhs+rhs env)) - (and lhs+rhs-term + (and (not-failed? lhs+rhs-term) (match lhs+rhs-term [(list lhs-term rhs-term) `((,fn ,@lhs-term) = ,rhs-term)]))]))) diff --git a/collects/redex/private/jdg-gen.rkt b/collects/redex/private/jdg-gen.rkt index 4393750ce5..bc659cfe43 100644 --- a/collects/redex/private/jdg-gen.rkt +++ b/collects/redex/private/jdg-gen.rkt @@ -41,35 +41,42 @@ (match pat [`(nt ,p-nt) (define all-nts (cons p-nt nts)) - (for/or ([nt-pat all-nts]) + (for/not-failed ([nt-pat all-nts]) (define term (recur `(nt ,nt-pat))) - (and (for/and ([nt (remove nt-pat all-nts)]) - ((get-matcher nt) term)) - term))] + (and/fail (for/and ([nt (remove nt-pat all-nts)]) + ((get-matcher nt) term)) + term))] [`any - (for/or ([nt-pat nts]) + (for/not-failed ([nt-pat nts]) (define term (recur `(nt ,nt-pat))) - (and (for/and ([nt (remove nt-pat nts)]) - ((get-matcher nt) term)) - term))] + (and/fail (for/and ([nt (remove nt-pat nts)]) + ((get-matcher nt) term)) + term))] [else (define term (recur pat)) - (and (for/and ([nt nts]) - ((get-matcher nt) term)) - term)])] + (and/fail (for/and ([nt nts]) + ((get-matcher nt) term)) + term)])] [`(name ,var ,pat) (error 'make-term "can't instantiate a term with an unbound variable: ~s" p)] [`(list ,ps ...) (call/ec (λ (fail) (for/list ([p ps]) (let ([res (recur p)]) - (unless res (fail #f)) + (unless (not-failed? res) (fail (unif-fail))) res))))] [else (let-values ([(p bs) (gen-term p lang 2)]) p)]))) - (and (check-dqs (remove-empty-dqs (env-dqs full-env)) term-e lang eqs) - res-term)) + (and/fail (check-dqs (remove-empty-dqs (env-dqs full-env)) term-e lang eqs) + res-term)) + +(define-syntax-rule (for/not-failed ((x xs)) b ...) + (for/fold ([res (unif-fail)]) + ([x xs]) + #:break (not-failed? res) + b ...)) + (define (check-dqs dqs term-e lang eqs) (for/and ([dq dqs]) diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt index 8718b14616..293543c2ff 100644 --- a/collects/redex/private/pat-unify.rkt +++ b/collects/redex/private/pat-unify.rkt @@ -23,7 +23,9 @@ pat*-clause-p?s bind-names remove-empty-dqs + and/fail (struct-out unif-fail) + not-failed? dq) @@ -157,7 +159,7 @@ (define res (and/fail (not-failed? t*) (not-failed? u*) (unify* t* u* eqs L))) - (and (not-failed? res) + (and/fail (not-failed? res) (let* ([static-eqs (hash/mut->imm eqs)] [found-pre-dqs (apply set-union (set) @@ -166,12 +168,12 @@ [found-dqs (for/list ([pdq found-pre-dqs]) (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))]) - (and (for/and ([d found-dqs]) d) - (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)] - [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)]) - (and new-dqs - (p*e res - (env static-eqs new-dqs))))))))) + (and/fail (for/and ([d found-dqs]) d) + (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)] + [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)]) + (and/fail new-dqs + (p*e res + (env static-eqs new-dqs))))))))) (define (list->dq-pairs dq-sides) (cond diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt index b3230cbee3..5ee682fee2 100644 --- a/collects/redex/private/search.rkt +++ b/collects/redex/private/search.rkt @@ -61,10 +61,10 @@ (define-values (ans fails) (with-handlers ([exn:fail:redex:search-failure? (λ (e) (define f-conts (exn:fail:redex:search-failure-fails e)) - (values #f (trim-fails f-conts)))]) + (values (unif-fail) (trim-fails f-conts)))]) (define-values (env/f fails) (fail-back fs)) - (values (and env/f (unify fresh-pat 'any env/f lang)) + (values (and/fail env/f (unify fresh-pat 'any env/f lang)) fails))) (set-last-gen-trace! (generation-trace)) (set! fs (shuffle-fails fails)) ;; how to test if we're randomizing here? @@ -174,9 +174,9 @@ (define u-res (disunify ps lhs rhs e lang)) (and u-res (loop u-res rest))]))) - (define head-p*e (and env1 (unify input head-pat env1 lang))) + (define head-p*e (and/fail env1 (unify input head-pat env1 lang))) (cond - [head-p*e + [(not-failed? head-p*e) (define res-p (p*e-p head-p*e)) (let loop ([e (p*e-e head-p*e)] [eqs eqs]) diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 8f38c422f7..061a3c21de 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -710,4 +710,48 @@ (f any) = 1 5) [`((f (,a ,b)) = 1) #f] - [else #t])))) \ No newline at end of file + [else #t])))) + +(let () + (define-language L0) + + (define-relation L0 + [(R (#f #f #f) 3)] + [(R (#f #f) 2)] + [(R #f 1)]) + + (is-not-false + (generate-term + L0 + #:satisfying + (R any_1 any_2) + +inf.0)) + + (is-not-false + (generate-term + L0 + #:satisfying + (R (any_1 any_2) any_3) + +inf.0)) + + (is-not-false + (generate-term + L0 + #:satisfying + (R (any_1 any_2 any_3) any_4) + +inf.0)) + + (is-false + (generate-term + L0 + #:satisfying + (R (any_1 any_2) 3) + +inf.0)) + + (is-not-false + (generate-term + L0 + #:satisfying + (R #f any) + +inf.0)) + ) \ No newline at end of file diff --git a/collects/redex/tests/unify-tests.rkt b/collects/redex/tests/unify-tests.rkt index 41aa13561e..db3c07863a 100644 --- a/collects/redex/tests/unify-tests.rkt +++ b/collects/redex/tests/unify-tests.rkt @@ -226,8 +226,8 @@ (p*e? res-pe-bkwd) (p*e-equivalent? res-pe res-pe-bkwd eqs)) (p*e (p*e-p res-pe) (env-eqs (p*e-e res-pe)))] - [(and (not res-pe) - (not res-pe-bkwd)) + [(and (unif-fail? res-pe) + (unif-fail? res-pe-bkwd)) #f] [else (list 'different-orders=>different-results @@ -241,13 +241,13 @@ (define res-p (unify*/lt p1 p2 e L)) (define res-p-bkwd (unify*/lt p2 p1 e2 L)) (cond - [(and res-p - res-p-bkwd + [(and (not-failed? res-p) + (not-failed? res-p-bkwd) (p*e-equivalent? (p*e res-p (env e '())) (p*e res-p-bkwd (env e2 '())) eqs)) res-p] - [(and (not res-p) - (not res-p-bkwd)) + [(and (unif-fail? res-p) + (unif-fail? res-p-bkwd)) #f] [else (list 'different-orders=>different-results @@ -852,12 +852,14 @@ (name e2 ,(bound)))) (env (m-hash (lvar 'e1) `(cstr (e) (nt e)) (lvar 'e2) `(nt e)) '())))) -(check-false (pat->term λn `(cstr (x) (list (nt e) (nt e))) (env (hash) '()))) +(check-equal? (pat->term λn `(cstr (x) (list (nt e) (nt e))) (env (hash) '())) + (unif-fail)) (check-not-false (pat->term λn `(cstr (e) (list (nt e) (nt e))) (env (hash) '()))) -(check-false (pat->term λn `(cstr (x) (list (name e1 ,(bound)) - (name e2 ,(bound)))) - (env (m-hash (lvar 'e1) `(cstr (e) (nt e)) - (lvar 'e2) `(nt e)) '()))) +(check-equal? (pat->term λn `(cstr (x) (list (name e1 ,(bound)) + (name e2 ,(bound)))) + (env (m-hash (lvar 'e1) `(cstr (e) (nt e)) + (lvar 'e2) `(nt e)) '())) + (unif-fail)) (check-not-false (redex-match λn (e_1 e_1) (pat->term λn `(list (name x1 ,(bound)) (name x2 ,(bound))) @@ -955,8 +957,8 @@ [dqs-in (make-dqs dqs)] [res (unify/lt t u (env eqs-in dqs-in) L0)]) (if true/false - (check-not-false res) - (check-false res))))])) + (check-not-false (not-failed? res)) + (check-equal? res (unif-fail)))))])) (test-disunify/no-params 1 2 '() '() '() '()) (test-disunify/no-params '(list 1 2) '(list 1 3) '() '() '() '())