From f1bf9821512115eb7d3303bd058895746872999d Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Fri, 24 May 2013 18:25:30 -0500 Subject: [PATCH] adjust Redex to disallow certain patterns that are guaranteed never to fail When you have a named variable that is inside two different mismatch-named ellipses, e.g.: (any_1 ..._!_1 any_1 .._!_1) then this pattern cannot match anything, since the any_1 constraint insists that they are bound to the same thing, but the ..._!_1 insists that whatever any_1 is bound to has different lengths in the two places. So, make this kind of situation be a syntax error instead. --- .../redex/private/rewrite-side-conditions.rkt | 93 ++++++++++++++----- .../tests/rewrite-side-condition-test.rkt | 25 +++-- 2 files changed, 84 insertions(+), 34 deletions(-) diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index 46bdc348f6..a0b80be5c8 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -56,8 +56,19 @@ (define last-contexts (make-hasheq)) (define last-stx (make-hasheq)) ;; used for syntax error reporting (define assignments #hasheq()) - (define (record-binder pat-stx under) + + ;; hash[sym -o> (listof (list stx (listof id[mismatch-ellipsis-binders]))) + (define vars-under-mismatch-table (make-hash)) + + (define (record-binder pat-stx under under-mismatch-ellipsis) (define pat-sym (syntax->datum pat-stx)) + (hash-set! vars-under-mismatch-table + (syntax-e pat-stx) + (cons + (list pat-stx under-mismatch-ellipsis) + (hash-ref vars-under-mismatch-table + (syntax-e pat-stx) + '()))) (set! assignments (if (null? under) assignments @@ -95,15 +106,16 @@ (define-values (term names) (let loop ([term orig-stx] - [under '()]) + [under '()] + [under-mismatch-ellipsis '()]) (syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole cross unquote and) [(side-condition pre-pat (and)) ;; rewriting metafunctions (and possibly other things) that have no where, etc clauses ;; end up with side-conditions that are empty 'and' expressions, so we just toss them here. - (loop #'pre-pat under)] + (loop #'pre-pat under under-mismatch-ellipsis)] [(side-condition pre-pat exp) (let () - (define-values (pre-term pre-vars) (loop #'pre-pat under)) + (define-values (pre-term pre-vars) (loop #'pre-pat under under-mismatch-ellipsis)) (define names/ellipses (map build-dots pre-vars)) (with-syntax ([pre-term pre-term] [((name name/ellipses) ...) @@ -159,8 +171,8 @@ [hole (values term '())] [(name x y) (let () - (define-values (sub-term sub-vars) (loop #'y under)) - (record-binder #'x under) + (define-values (sub-term sub-vars) (loop #'y under under-mismatch-ellipsis)) + (record-binder #'x under under-mismatch-ellipsis) (values #`(name x #,sub-term) (cons (make-id/depth #'x (length under) #f) sub-vars)))] @@ -168,15 +180,15 @@ [name (expected-arguments 'name term)] [(in-hole a b) (let () - (define-values (a-term a-vars) (loop #'a under)) - (define-values (b-term b-vars) (loop #'b under)) + (define-values (a-term a-vars) (loop #'a under under-mismatch-ellipsis)) + (define-values (b-term b-vars) (loop #'b under under-mismatch-ellipsis)) (values #`(in-hole #,a-term #,b-term) (append a-vars b-vars)))] [(in-hole a ...) (expected-exact 'in-hole 2 term)] [in-hole (expected-arguments 'in-hole term)] [(hide-hole a) (let () - (define-values (sub-term vars) (loop #'a under)) + (define-values (sub-term vars) (loop #'a under under-mismatch-ellipsis)) (values #`(hide-hole #,sub-term) vars))] [(hide-hole a ...) (expected-exact 'hide-hole 1 term)] [hide-hole (expected-arguments 'hide-hole term)] @@ -210,14 +222,14 @@ orig-stx term)] [(memq prefix-sym all-nts) - (record-binder term under) + (record-binder term under under-mismatch-ellipsis) (record-syncheck-use term prefix-sym) (values (if mismatch? `(mismatch-name ,term (nt ,prefix-stx)) `(name ,term (nt ,prefix-stx))) (list (make-id/depth term (length under) mismatch?)))] [(memq prefix-sym underscore-allowed) - (record-binder term under) + (record-binder term under under-mismatch-ellipsis) (values (if mismatch? `(mismatch-name ,term ,prefix-stx) `(name ,term ,prefix-stx)) @@ -239,14 +251,14 @@ (record-syncheck-use term (syntax-e term)) (cond [bind-names? - (record-binder term under) + (record-binder term under under-mismatch-ellipsis) (values `(name ,term (nt ,term)) (list (make-id/depth term (length under) #f)))] [else (values `(nt ,term) '())])] [(memq (syntax-e term) underscore-allowed) (cond [bind-names? - (record-binder #'term under) + (record-binder #'term under under-mismatch-ellipsis) (values `(name ,term ,term) (list (make-id/depth term (length under) #f)))] [else (values term '())])] @@ -268,7 +280,7 @@ (cond [(null? terms) (values '() '())] [(null? (cdr terms)) - (define-values (term vars) (loop (car terms) under)) + (define-values (term vars) (loop (car terms) under under-mismatch-ellipsis)) (values (list term) vars)] [(is-ellipsis? (cadr terms)) (when (and (pair? (cddr terms)) @@ -300,9 +312,13 @@ (cadr terms) (string->symbol ellipsis-str) (cadr terms))) - (record-binder ellipsis+name under) + (record-binder ellipsis+name under under-mismatch-ellipsis) (define-values (fst-term fst-vars) - (loop (car terms) (cons (syntax-e ellipsis+name) under))) + (loop (car terms) + (cons (syntax-e ellipsis+name) under) + (if mismatch? + (cons (syntax-e (cadr terms)) under-mismatch-ellipsis) + under-mismatch-ellipsis))) (define-values (rst-terms rst-vars) (t-loop (cddr terms))) (values (cons `(repeat ,fst-term ,ellipsis+name @@ -310,7 +326,7 @@ rst-terms) (append fst-vars rst-vars))] [else - (define-values (fst-term fst-vars) (loop (car terms) under)) + (define-values (fst-term fst-vars) (loop (car terms) under under-mismatch-ellipsis)) (define-values (rst-terms rst-vars) (t-loop (cdr terms))) (values (cons fst-term rst-terms) (append fst-vars rst-vars))]))) @@ -328,7 +344,7 @@ (define closed-table (make-immutable-hasheq (hash-map assignments (λ (cls _) (cons cls (find cls assignments)))))) - + (define repeat-id-counts (make-hash)) (define ellipsis-normalized @@ -362,14 +378,18 @@ (syntax-case pat (repeat) [(repeat sub-pat name mismatch-name) (let () + (define final-match-repeat-name + (if (= 1 (hash-ref repeat-id-counts (syntax-e #'name))) + #f + #'name)) + (define final-mismatch-repeat-name + (if (and (syntax-e #'mismatch-name) + (= 1 (hash-ref repeat-id-counts (syntax-e #'mismatch-name)))) + #f + #'mismatch-name)) #`(repeat #,(loop #'sub-pat) - #,(if (= 1 (hash-ref repeat-id-counts (syntax-e #'name))) - #f - #'name) - #,(if (and (syntax-e #'mismatch-name) - (= 1 (hash-ref repeat-id-counts (syntax-e #'mismatch-name)))) - #f - #'mismatch-name)))] + #,final-match-repeat-name + #,final-mismatch-repeat-name))] [(a ...) (let () (define new (map loop (syntax->list #'(a ...)))) @@ -379,6 +399,29 @@ [_ pat]))) (filter-duplicates what orig-stx names) + + (for ([(id stx+mismatches) (in-hash vars-under-mismatch-table)]) + (define all-ids (map car stx+mismatches)) + (define all-mismatch-idss (map cadr stx+mismatches)) + (let loop ([all-mismatch-idss all-mismatch-idss]) + (cond + [(null? all-mismatch-idss) (void)] + [else + (define id-in-multiple-places/f + (for/or ([mismatch-id (in-list (car all-mismatch-idss))]) + (for/or ([other-mismatch-ids (in-list (cdr all-mismatch-idss))]) + (and (member mismatch-id other-mismatch-ids) + mismatch-id)))) + (when id-in-multiple-places/f + (raise-syntax-error what + (format "~a appears under ~a in multiple places (so this pattern would always fail)" + id + id-in-multiple-places/f) + orig-stx + (car all-ids) + (cdr all-ids))) + (loop (cdr all-mismatch-idss))]))) + (let ([without-mismatch-names (filter (λ (x) (not (id/depth-mismatch? x))) names)]) (with-syntax ([(name/ellipses ...) (map build-dots without-mismatch-names)] [(name ...) (map id/depth-id without-mismatch-names)] diff --git a/collects/redex/tests/rewrite-side-condition-test.rkt b/collects/redex/tests/rewrite-side-condition-test.rkt index 94389b54eb..494ea84fb3 100644 --- a/collects/redex/tests/rewrite-side-condition-test.rkt +++ b/collects/redex/tests/rewrite-side-condition-test.rkt @@ -7,15 +7,18 @@ (define-syntax (rsc stx) (syntax-case stx () [(_ pat (nts ...) bind-names?) - (with-syntax ([(ignore pat (vars ...) (vars/ellipses ...)) - (rewrite-side-conditions/check-errs - (syntax->datum #'(nts ...)) - 'rsc - (syntax-e #'bind-names?) - #'pat)]) - #'(list `pat - `(vars ...) - `(vars/ellipses ...)))])) + (with-handlers ((exn:fail:syntax? + (λ (x) + #`'#,(exn-message x)))) + (with-syntax ([(ignore pat (vars ...) (vars/ellipses ...)) + (rewrite-side-conditions/check-errs + (syntax->datum #'(nts ...)) + 'rsc + (syntax-e #'bind-names?) + #'pat)]) + #'(list `pat + `(vars ...) + `(vars/ellipses ...))))])) (check-equal? (rsc 1 () #t) `(1 () ())) (check-equal? (rsc (1) () #t) `((list 1) () ())) @@ -43,6 +46,10 @@ () ())) +(check-regexp-match + #rx"any_1 appears under ..._!_1 in multiple places" + (rsc (any_1 ..._!_1 any_1 ..._!_1) () #f)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; test the normalization of the ellipses underscores