Makes it a syntax error for a `where' clause to reuse a pattern variable at a different depth

This commit is contained in:
Casey Klein 2010-07-19 10:36:16 -05:00
parent 72b98b77fb
commit 310f9ce05a
3 changed files with 60 additions and 27 deletions

View File

@ -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)

View File

@ -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))))]))))

View File

@ -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)