From c083335ca5815e7a3fd05e52eff463a2c097814d Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Tue, 22 Jun 2010 13:19:45 -0500 Subject: [PATCH] Changes the matching of `where' clauses to the one most people expect. --- .../redex/private/reduction-semantics.rkt | 141 ++++++++++-------- collects/redex/tests/rg-test.rkt | 34 +++++ collects/redex/tests/tl-test.rkt | 33 ++++ doc/release-notes/redex/HISTORY.txt | 6 + 4 files changed, 149 insertions(+), 65 deletions(-) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 62d8e127a2..56c3ca2162 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -7,11 +7,9 @@ "loc-wrapper.ss" "error.ss" mzlib/trace - racket/set (lib "list.ss") (lib "etc.ss") - (for-syntax syntax/parse) - (for-syntax racket/set)) + (for-syntax syntax/parse)) (require (for-syntax (lib "name.ss" "syntax") "loc-wrapper-ct.ss" @@ -225,32 +223,45 @@ (syntax/loc stx (do-reduction-relation orig-stx extend-reduction-relation orig-reduction-relation #t lang args ...)))])) ;; the withs, freshs, and side-conditions come in backwards order -(define-for-syntax bind-withs - (λ (orig-name main lang lang-nts stx where-mode body [lhs-bound #'()]) - (let loop ([stx stx] - [to-not-be-in main] - [bound (apply set lhs-bound)]) - (syntax-case stx (fresh) - [() body] - [((-where x e) y ...) - (or (free-identifier=? #'-where #'where) - (free-identifier=? #'-where #'where/hidden)) - (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) +(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses) + (let loop ([stx stx] + [to-not-be-in main] + [env (make-immutable-hash + (map (λ (x e) (cons (syntax-e x) e)) + names w/ellipses))]) + (syntax-case stx (fresh) + [() body] + [((-where x e) y ...) + (or (free-identifier=? #'-where #'where) + (free-identifier=? #'-where #'where/hidden)) + (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) + (let ([env+ (for/fold ([env env]) + ([name names] + [w/ellipses names/ellipses]) + (hash-set env (syntax-e name) w/ellipses))]) (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs lang-nts 'reduction-relation #f #'x)] [(names ...) names] - [(names/ellipses ...) names/ellipses]) - (with-syntax ([(x ...) (generate-temporaries #'(names ...))]) - (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) bound)]) + [(names/ellipses ...) names/ellipses] + [(x ...) (generate-temporaries names)]) + (with-syntax ([(binding-constraints ...) + (for/fold ([cs '()]) + ([n (syntax->list #'(names ...))] + [x (syntax->list #'(x ...))]) + (cond [(hash-ref env (syntax-e n) #f) + => (λ (b) (cons #`(equal? #,x (term #,b)) cs))] + [else cs]))]) + (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+)]) #`(let* ([mtchs (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))] [result (λ (mtch) (let ([bindings (mtch-bindings mtch)]) (let ([x (lookup-binding bindings 'names)] ...) - (term-let ([names/ellipses x] ...) - #,rest-body))))]) + (and binding-constraints ... + (term-let ([names/ellipses x] ...) + #,rest-body)))))]) (if mtchs #, (case where-mode @@ -259,34 +270,34 @@ [(predicate) #`(ormap result mtchs)] [else (error 'unknown-where-mode "~s" where-mode)]) - #f))))))] - [((-side-condition s ...) y ...) - (or (free-identifier=? #'-side-condition #'side-condition) - (free-identifier=? #'-side-condition #'side-condition/hidden)) - #`(and s ... #,(loop #'(y ...) to-not-be-in bound))] - [((fresh x) y ...) - (identifier? #'x) - #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) - #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) bound))] - [((fresh x name) y ...) - (identifier? #'x) - #`(term-let ([x (let ([the-name (term name)]) - (verify-name-ok '#,orig-name the-name) - (variable-not-in #,to-not-be-in the-name))]) - #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) bound))] - [((fresh (y) (x ...)) z ...) - #`(term-let ([(y #,'...) - (variables-not-in #,to-not-be-in - (map (λ (_ignore_) 'y) - (term (x ...))))]) - #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) bound))] - [((fresh (y) (x ...) names) z ...) - #`(term-let ([(y #,'...) - (let ([the-names (term names)] - [len-counter (term (x ...))]) - (verify-names-ok '#,orig-name the-names len-counter) - (variables-not-in #,to-not-be-in the-names))]) - #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) bound))])))) + #f)))))))] + [((-side-condition s ...) y ...) + (or (free-identifier=? #'-side-condition #'side-condition) + (free-identifier=? #'-side-condition #'side-condition/hidden)) + #`(and s ... #,(loop #'(y ...) to-not-be-in env))] + [((fresh x) y ...) + (identifier? #'x) + #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) + #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))] + [((fresh x name) y ...) + (identifier? #'x) + #`(term-let ([x (let ([the-name (term name)]) + (verify-name-ok '#,orig-name the-name) + (variable-not-in #,to-not-be-in the-name))]) + #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))] + [((fresh (y) (x ...)) z ...) + #`(term-let ([(y #,'...) + (variables-not-in #,to-not-be-in + (map (λ (_ignore_) 'y) + (term (x ...))))]) + #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))] + [((fresh (y) (x ...) names) z ...) + #`(term-let ([(y #,'...) + (let ([the-names (term names)] + [len-counter (term (x ...))]) + (verify-names-ok '#,orig-name the-names len-counter) + (variables-not-in #,to-not-be-in the-names))]) + #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]))) (define-syntax-set (do-reduction-relation) (define (do-reduction-relation/proc stx) @@ -702,7 +713,7 @@ sides/withs/freshs 'flatten #`(list (term #,to)) - names/ellipses)] + names names/ellipses)] [(test-case-body-code) ;; this contains some redundant code (bind-withs orig-name @@ -712,7 +723,7 @@ sides/withs/freshs 'predicate #'#t - names/ellipses)]) + names names/ellipses)]) (with-syntax ([side-conditions-rewritten (rw-sc from)] [lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))] [lhs-source (format "~a:~a:~a" @@ -1153,38 +1164,38 @@ (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction))) (raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction)) (parse-extras #'((stuff ...) ...)) - (let-values ([(lhs-namess lhs-namess/ellipsess) - (let loop ([lhss (syntax->list (syntax (lhs ...)))]) - (if (null? lhss) - (values null null) - (let-values ([(namess namess/ellipsess) - (loop (cdr lhss))] - [(names names/ellipses) - (extract-names lang-nts syn-error-name #t (car lhss))]) - (values (cons names namess) - (cons names/ellipses namess/ellipsess)))))]) + (let*-values ([(lhs-namess lhs-namess/ellipsess) + (let loop ([lhss (syntax->list (syntax (lhs ...)))]) + (if (null? lhss) + (values null null) + (let-values ([(namess namess/ellipsess) + (loop (cdr lhss))] + [(names names/ellipses) + (extract-names lang-nts syn-error-name #t (car lhss))]) + (values (cons names namess) + (cons names/ellipses namess/ellipsess)))))]) (with-syntax ([(rhs/wheres ...) - (map (λ (sc/b rhs names/ellipses) + (map (λ (sc/b rhs names names/ellipses) (bind-withs syn-error-name '() #'lang lang-nts sc/b 'flatten #`(list (term #,rhs)) - names/ellipses)) + names names/ellipses)) (syntax->list #'((stuff ...) ...)) (syntax->list #'(rhs ...)) - lhs-namess/ellipsess)] + lhs-namess lhs-namess/ellipsess)] [(rg-rhs/wheres ...) - (map (λ (sc/b rhs names/ellipses) + (map (λ (sc/b rhs names names/ellipses) (bind-withs syn-error-name '() #'lang lang-nts sc/b 'predicate #`#t - names/ellipses)) + names names/ellipses)) (syntax->list #'((stuff ...) ...)) (syntax->list #'(rhs ...)) - lhs-namess/ellipsess)]) + lhs-namess lhs-namess/ellipsess)]) (with-syntax ([(side-conditions-rewritten ...) (map (λ (x) (rewrite-side-conditions/check-errs lang-nts diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index da279f97fa..bab60b4856 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -787,6 +787,23 @@ generated) (reverse '((+ (+)) 0)))) + (test (let* ([generated null] + [R (reduction-relation + L + (--> (name t (number_1 number_3)) + dontcare + (side-condition (set! generated (cons (term t) generated))) + (where number_1 4) + (where number_2 number_1) + (where number_3 number_2)))]) + (parameterize ([generation-decisions + (decisions #:num (list (λ _ 3) (λ _ 4) + (λ _ 4) (λ _ 3) + (λ _ 4) (λ _ 4)))]) + (check-reduction-relation R (λ (_) #t) #:attempts 1 #:print? #f)) + generated) + '((4 4) (4 3) (3 4))) + (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))]) (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) #rx"check-reduction-relation:.*no counterexamples") @@ -875,6 +892,23 @@ (check-metafunction f (λ (_) #t) #:retries 1 #:print? #f #:attempts 1)) #t)) + (test (let ([generated null]) + (define-language L) + (define-metafunction L + [(f (name t (number_1 number_3))) + dontcare + (side-condition (set! generated (cons (term t) generated))) + (where number_1 4) + (where number_2 number_1) + (where number_3 number_2)]) + (parameterize ([generation-decisions + (decisions #:num (list (λ _ 3) (λ _ 4) + (λ _ 4) (λ _ 3) + (λ _ 4) (λ _ 4)))]) + (check-metafunction f (λ (_) #t) #:attempts 1 #:print? #f)) + generated) + '((4 4) (4 3) (3 4))) + (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+") diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index dd549be8d8..4578319b37 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -704,6 +704,23 @@ (test (term (f 8)) 12345)) + (let () + (define-metafunction empty-language + [(f number_1 number_2 ... (number_s ...) ...) + yes + (where number_1 1) + (where (number_3 ...) ,(cdr (term (number_2 ...)))) + (where (number_3 ...) (3 4 5)) + (where (number_1 (number_s ...) ...) + ,(if (null? (term ((number_s ...) ...))) + (term (number_1)) + (term (number_1 () (6) (7 8) (9 10 11)))))] + [(f any ...) + no]) + (test (term (f 1 2 3 4 5)) 'yes) + (test (term (f 1 2 3 4)) 'no) + (test (term (f 0 2 3 4 5)) 'no) + (test (term (f 1 2 3 4 5 () (6) (7 8) (9 10 11))) 'yes)) (let () (test-syn-err @@ -1072,6 +1089,22 @@ 11) '(1))) + (let ([R (reduction-relation + grammar + (--> (number_1 number_2 ... (number_s ...) ...) + yes + (where number_1 1) + (where (number_3 ...) ,(cdr (term (number_2 ...)))) + (where (number_3 ...) (3 4 5)) + (where (number_1 (number_s ...) ...) + ,(if (null? (term ((number_s ...) ...))) + (term (number_1)) + (term (number_1 () (6) (7 8) (9 10 11)))))))]) + (test (apply-reduction-relation R (term (1 2 3 4 5))) '(yes)) + (test (apply-reduction-relation R (term (1 2 3 4))) '()) + (test (apply-reduction-relation R (term (0 2 3 4 5))) '()) + (test (apply-reduction-relation R (term (1 2 3 4 5 () (6) (7 8) (9 10 11)))) '(yes))) + (test-syn-err (reduction-relation grammar (~~> (number_1 number_2) diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt index ce7d3701e4..c4c12d38cd 100644 --- a/doc/release-notes/redex/HISTORY.txt +++ b/doc/release-notes/redex/HISTORY.txt @@ -1,3 +1,9 @@ + * changed the matching of `where' clauses in a + backwards-incompatible way. Previously, pattern variables bound by + a `where' left-hand side shadowed bindings from earlier clause's + and the case's left-hand side; now, `where' clauses match only + when their bindings match the existing ones. + v5.0 * added an optional term-equivalence predicate to the test--> and