diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index c554052a4d..480b8728f5 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -236,24 +236,40 @@ (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] - [(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]))]) + ([name names] + [w/ellipses names/ellipses]) + (hash-set env (syntax-e name) w/ellipses))] + [temporaries (generate-temporaries names)]) + (define (id/depth stx) + (syntax-case stx () + [(s (... ...)) + (let ([r (id/depth #'s)]) + (make-id/depth (id/depth-id r) (add1 (id/depth-depth r))))] + [s (make-id/depth #'s 0)])) + (with-syntax ([(binding-constraints ...) + (for/fold ([cs '()]) + ([n names] + [w/e names/ellipses] + [x temporaries]) + (cond [(hash-ref env (syntax-e n) #f) + => (λ (b) + (let ([b-id/depth (id/depth b)] + [n-id/depth (id/depth w/e)]) + (if (= (id/depth-depth b-id/depth) (id/depth-depth n-id/depth)) + (cons #`(equal? #,x (term #,b)) cs) + (raise-ellipsis-depth-error + orig-name + (id/depth-id n-id/depth) (id/depth-depth n-id/depth) + (id/depth-id b-id/depth) (id/depth-depth b-id/depth)))))] + [else cs]))]) + (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs + lang-nts + 'reduction-relation + #f + #'x)] + [(names ...) names] + [(names/ellipses ...) names/ellipses] + [(x ...) temporaries]) (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) diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index 5904356edb..07830a0e3e 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -8,9 +8,12 @@ (provide rewrite-side-conditions/check-errs extract-names + raise-ellipsis-depth-error make-language-id language-id-nts) + (provide (struct-out id/depth)) + (define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0)) (define (language-id-nts stx id) (language-id-getter stx id 1)) @@ -176,6 +179,17 @@ (and (not (regexp-match #rx"^\\.\\.\\._" str)) (not (regexp-match #rx"_!_" str)))))) + (define (raise-ellipsis-depth-error what one-binder one-depth another-binder another-depth) + (raise + (make-exn:fail:syntax + (format "~a: found the same binder, ~s, at different depths, ~a and ~a" + what + (syntax->datum one-binder) + one-depth + another-depth) + (current-continuation-marks) + (list one-binder another-binder)))) + (define (filter-duplicates what orig-stx dups) (let loop ([dups dups]) (cond @@ -189,14 +203,9 @@ (when same-id? (unless (equal? (id/depth-depth x) (id/depth-depth (car dups))) - (raise - (make-exn:fail:syntax - (format "~a: found the same binder, ~s, at different depths, ~a and ~a" - what - (syntax->datum (id/depth-id x)) - (id/depth-depth x) - (id/depth-depth (car dups))) - (current-continuation-marks) - (list (id/depth-id x) (id/depth-id (car dups))))))) + (raise-ellipsis-depth-error + what + (id/depth-id x) (id/depth-depth x) + (id/depth-id (car dups)) (id/depth-depth (car dups))))) (not same-id?))) (loop (cdr dups))))])))) diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 40fcf655b0..ca30f77b81 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -1155,6 +1155,14 @@ #rx"same name on multiple rules" 2) + (test-syn-err (reduction-relation + grammar + (--> number_1 + () + (where (number_1 ...) '()))) + #rx"different depths" + 2) + (test-syn-err (reduction-relation grammar (--> 1 2)