From b5cfb7affe408b5dac190caee48273ced55c1ef9 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Tue, 14 Jan 2014 22:35:15 -0600 Subject: [PATCH] Adjust rewrite-side-conditions/check-errs so that it returns the ellipses names in addition to the regular names keeping the names in the pattern and including them in the last two results closes PR 14291 --- .../redex-lib/redex/private/generate-term.rkt | 21 +++-- .../redex-lib/redex/private/judgment-form.rkt | 18 ++-- .../redex/private/reduction-semantics.rkt | 65 +++++++++------ .../redex/private/rewrite-side-conditions.rkt | 69 ++++++++++------ .../redex-lib/redex/private/term.rkt | 82 +++++++++++-------- .../tests/rewrite-side-condition-test.rkt | 9 +- 6 files changed, 166 insertions(+), 98 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt index d61d81bf12..390d4f9619 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt @@ -147,8 +147,10 @@ [res-term-stx #`(#,jf-id #,@args-stx)] [property #`(bind-prop (λ (bindings) - (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) - #,property)))]) + #,(bind-pattern-names 'redex-check + #'(names/ellipses ...) + #'((lookup-binding bindings 'names) ...) + property)))]) (quasisyntax/loc orig-stx (let ([term-match (λ (generated) (cond [(test-match #,lang res-term-stx generated) => values] @@ -183,9 +185,12 @@ [show (show-message orig-stx)] [property #`(bind-prop (λ (bindings) - (term-let ([lhs-names/ellipses (lookup-binding bindings 'lhs-names)] ... - [rhs-names/ellipses (lookup-binding bindings 'rhs-names)] ...) - #,property)))]) + #,(bind-pattern-names 'redex-check + #'(lhs-names/ellipses ... + rhs-names/ellipses ...) + #'((lookup-binding bindings 'lhs-names) ... + (lookup-binding bindings 'rhs-names) ...) + property)))]) (quasisyntax/loc orig-stx (let ([term-match (λ (generated) (cond [(test-match #,lang res-term-stx generated) => values] @@ -214,8 +219,10 @@ (parse-redex-check-kw-args kw-args orig-stx form)) (with-syntax ([property #`(bind-prop (λ (bindings) - (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) - #,property)))]) + #,(bind-pattern-names 'redex-check + #'(name/ellipses ...) + #'((lookup-binding bindings 'name) ...) + property)))]) (quasisyntax/loc orig-stx (let ([att #,attempts-stx] [ret #,retries-stx] diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt index 0b588d9490..a067104907 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt @@ -154,8 +154,10 @@ (λ (bindings) (let ([x (lookup-binding bindings 'names)] ...) (and binding-constraints ... - (term-let ([names/ellipses x] ...) - #,rest-body)))))))))] + #,(bind-pattern-names orig-name + #'(names/ellipses ...) + #'(x ...) + rest-body)))))))))] [((-side-condition s ...) y ...) (side-condition-keyword? #'-side-condition) (if side-condition-unquoted? @@ -239,8 +241,10 @@ (λ (bindings #,(if jf-results-id jf-results-id '_ignored)) (let ([temp (lookup-binding bindings 'output-name)] ...) (and binding-constraint ... - (term-let ([output-name/ellipsis temp] ...) - #,rest-body))))))))])))) + #,(bind-pattern-names orig-name + #'(output-name/ellipsis ...) + #'(temp ...) + rest-body))))))))])))) (define (judgment-form-bind-withs/proc lang output-pattern output under-ellipsis? old-maps do-something) (let ([compiled-pattern (compile-pattern lang output-pattern #t)]) @@ -816,8 +820,10 @@ compiled-lhs input (λ (bnds) - (term-let ([names/ellipses (lookup-binding bnds 'names)] ...) - #,body)) + #,(bind-pattern-names 'judgment-form + #'(names/ellipses ...) + #'((lookup-binding bnds 'names) ...) + body)) #,(if output-contracts #`(λ (output) (check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode)) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt index fc6a959a98..c2921b9527 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -47,17 +47,24 @@ (syntax->list (syntax (pattern ...))))] [(cp-x ...) (generate-temporaries #'(pattern ...))] [make-matcher make-matcher]) - #'(begin - syncheck-expr ... - (make-matcher - 'form-name lang - (list 'pattern ...) - (list (compile-pattern lang `side-conditions-rewritten #t) ...) - (list (λ (match) - (term-let/error-name - form-name - ([names/ellipses (lookup-binding (mtch-bindings match) 'names)] ...) - rhs)) ...)))))])) + (with-syntax ([(mtch-procs ...) + (for/list ([names/ellipses (in-list (syntax->list #'((names/ellipses ...) ...)))] + [names (in-list (syntax->list #'((names ...) ...)))] + [rhs (in-list (syntax->list #'(rhs ...)))]) + (with-syntax ([(names ...) names]) + #`(λ (match) + #,(bind-pattern-names + #'form-name + names/ellipses + #'((lookup-binding (mtch-bindings match) 'names) ...) + rhs))))]) + #`(begin + syncheck-expr ... + (make-matcher + 'form-name lang + (list 'pattern ...) + (list (compile-pattern lang `side-conditions-rewritten #t) ...) + (list mtch-procs ...))))))])) (define-syntax (term-match/single stx) (term-matcher stx #'term-match/single/proc)) @@ -683,10 +690,12 @@ 'lhs-frm-id 'lhs-to-id `side-conditions-rewritten - (λ (bindings rhs-binder) - (term-let ([lhs-to-id rhs-binder] - [names/ellipses (lookup-binding bindings 'names)] ...) - (term rhs-to #:lang lang))) + (λ (bindings rhs-binder) + (term-let ([lhs-to-id rhs-binder]) + #,(bind-pattern-names 'reduction-relation + #'(names/ellipses ...) + #'((lookup-binding bindings 'names) ...) + #'(term rhs-to #:lang lang)))) #,child-proc `fresh-rhs-from))) (get-choices stx orig-name bm #'lang @@ -779,13 +788,16 @@ [body-code body-code]) #`(begin lhs-syncheck-expr - (build-rewrite-proc/leaf `side-conditions-rewritten - (λ (main-exp bindings) - (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) - body-code)) - lhs-source - name - (λ (lang-id2) `lhs-w/extras)))))) + (build-rewrite-proc/leaf + `side-conditions-rewritten + (λ (main-exp bindings) + #,(bind-pattern-names 'reduction-relation + #'(names/ellipses ...) + #'((lookup-binding bindings 'names) ...) + #'body-code)) + lhs-source + name + (λ (lang-id2) `lhs-w/extras)))))) (define (process-extras stx orig-name name-table extras) (let* ([the-name #f] @@ -1085,12 +1097,15 @@ (let ([ans (match-pattern cpat exp)]) (and ans (map (λ (m) (make-match (sort-bindings - (filter (λ (x) (memq (bind-name x) binders)) + (filter (λ (x) (and (memq (bind-name x) binders) + (not-ellipsis-name (bind-name x)))) (bindings-table (mtch-bindings m)))))) ans)))))) (if name (procedure-rename redex-match-proc name) redex-match-proc)) +(define (not-ellipsis-name x) + (not (regexp-match? #rx"^[.][.][.]" (symbol->string x)))) (define (sort-bindings bnds) (sort @@ -1704,6 +1719,10 @@ "cannot use pattern language keyword as a non-terminal name") (check-each names (λ (x) (regexp-match? #rx"_" (symbol->string (syntax-e x)))) "cannot use _ in a non-terminal name") + (check-each names (λ (x) (regexp-match? #rx"^[.][.][.]$" (symbol->string (syntax-e x)))) + "cannot name a non-terminal `...'") + (check-each names (λ (x) (regexp-match? #rx"^[.][.][.]_" (symbol->string (syntax-e x)))) + "cannot start a non-terminal name with `..._'") (when (null? prods) (raise-syntax-error #f "expected at least one production to follow" diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt index e03ece49a2..c0de07df96 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt @@ -14,7 +14,8 @@ (rename-out [binds? id-binds?]) raise-ellipsis-depth-error make-language-id - language-id-nts) + language-id-nts + bind-pattern-names) (provide (struct-out id/depth)) @@ -59,6 +60,11 @@ ;; hash[sym -o> (listof stx)] (define var-locs-table (make-hash)) + ;; hash[sym -o> sym] + ;; tells the original names for any given repeat to be replaced after + ;; normalization and checking has finished + (define original-repeat-names (make-hash)) + (define (record-binder pat-stx under under-mismatch-ellipsis) (define pat-sym (syntax->datum pat-stx)) (hash-set! var-locs-table pat-sym (cons pat-stx (hash-ref var-locs-table pat-sym '()))) @@ -288,24 +294,29 @@ orig-stx (cadr terms) (list (caddr terms)))) - (define ellipsis-sym (syntax-e (cadr terms))) - (define ellipsis-pre-str (symbol->string ellipsis-sym)) + (define ellipsis-pre-sym (syntax-e (cadr terms))) + (define ellipsis-pre-str (symbol->string ellipsis-pre-sym)) (define mismatch? (regexp-match? #rx"^[.][.][.]_!_" ellipsis-pre-str)) - (define ellipsis-str (cond - [mismatch? - (set! ellipsis-number (+ ellipsis-number 1)) - (format "..._r~a" ellipsis-number)] - [(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str) - (string-append (substring ellipsis-str 0 4) - "r" - (substring ellipsis-str - 4 - (string-length ellipsis-str)))] - [(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str) - ellipsis-pre-str] - [else - (set! ellipsis-number (+ ellipsis-number 1)) - (format "..._r~a" ellipsis-number)])) + (define-values (ellipsis-str was-named-ellipsis?) + (cond + [mismatch? + (set! ellipsis-number (+ ellipsis-number 1)) + (values (format "..._r~a" ellipsis-number) #f)] + [(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str) + (values (string-append (substring ellipsis-str 0 4) + "r" + (substring ellipsis-str + 4 + (string-length ellipsis-str))) + #t)] + [(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str) + (values ellipsis-pre-str #t)] + [else + (set! ellipsis-number (+ ellipsis-number 1)) + (values (format "..._r~a" ellipsis-number) #f)])) + (define ellipsis-sym (string->symbol ellipsis-str)) + (when was-named-ellipsis? + (hash-set! original-repeat-names ellipsis-sym ellipsis-pre-sym)) (define ellipsis+name (datum->syntax (cadr terms) (string->symbol ellipsis-str) @@ -318,11 +329,13 @@ (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 - ,(if mismatch? (cadr terms) #f)) + (values (cons `(repeat ,fst-term ,ellipsis+name ,(if mismatch? (cadr terms) #f)) rst-terms) - (append fst-vars rst-vars))] + (append fst-vars + (if was-named-ellipsis? + (list (id/depth (cadr terms) (length under) #f)) + '()) + rst-vars))] [else (define-values (fst-term fst-vars) (loop (car terms) under under-mismatch-ellipsis)) @@ -425,7 +438,7 @@ (let () (define final-match-repeat-name (if (= 1 (hash-ref repeat-id-counts (syntax-e #'name))) - #f + (hash-ref original-repeat-names (syntax-e #'name) #f) #'name)) (define final-mismatch-repeat-name (if (and (syntax-e #'mismatch-name) @@ -569,3 +582,13 @@ orig-stx))) (not same-id?))) (loop (cdr dups))))]))) + + + + (define (bind-pattern-names err-name names/ellipses vals body) + (with-syntax ([(names/ellipsis ...) names/ellipses] + [(val ...) vals]) + #`(term-let/error-name + #,err-name + ([names/ellipsis val] ...) + #,body))) \ No newline at end of file diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt index 9f304b2791..442a5e2b8f 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt @@ -168,7 +168,9 @@ (judgment-form-id? #'jf-name)) (begin (unless (not (memq 'O (judgment-form-mode (syntax-local-value #'jf-name)))) - (raise-syntax-error 'term "judgment forms with output mode (\"O\") positions disallowed" arg-stx stx)) + (raise-syntax-error 'term + "judgment forms with output mode (\"O\") positions disallowed" + arg-stx stx)) (rewrite-application #'jf-name (syntax/loc stx (arg ...)) depth))] [f (and (identifier? (syntax f)) @@ -255,7 +257,9 @@ (define m (regexp-match #rx"^([^_]*)_" (symbol->string id))) (when m (unless (memq (string->symbol (list-ref m 1)) (append pattern-symbols lang-nts)) - (raise-syntax-error 'term "before underscore must be either a non-terminal or a built-in pattern" arg-stx stx))))) + (raise-syntax-error 'term + "before underscore must be either a non-terminal or a built-in pattern" + arg-stx stx))))) (values (with-syntax ([rewritten (rewrite arg-stx)]) @@ -374,40 +378,46 @@ (define-syntax (term-let/error-name stx) (syntax-case stx () [(_ error-name ([x1 rhs1] [x rhs] ...) body1 body2 ...) - (let-values ([(orig-names new-names depths new-x1) - (let loop ([stx #'x1] [depth 0]) - (define ((combine orig-names new-names depths new-pat) - orig-names* new-names* depths* new-pat*) - (values (append orig-names orig-names*) - (append new-names new-names*) - (append depths depths*) - (cons new-pat new-pat*))) - (syntax-case stx (...) - [x - (and (identifier? #'x) - (not (free-identifier=? (quote-syntax ...) #'x))) - (let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)]) - (values (list #'x) - (list new-name) - (list depth) - new-name))] - [(x (... ...) . xs) - (let-values ([(orig-names new-names depths new-pat) - (call-with-values - (λ () (loop #'xs depth)) - (call-with-values - (λ () (loop #'x (add1 depth))) - combine))]) - (values orig-names new-names depths - (list* (car new-pat) #'(... ...) (cdr new-pat))))] - [(x . xs) - (call-with-values - (λ () (loop #'xs depth)) - (call-with-values - (λ () (loop #'x depth)) - combine))] - [_ - (values '() '() '() stx)]))]) + (let () + (unless (identifier? #'error-name) + (raise-syntax-error 'term-let/error-name + "expected an identifier as the first argument" + stx + #'error-name)) + (define-values (orig-names new-names depths new-x1) + (let loop ([stx #'x1] [depth 0]) + (define ((combine orig-names new-names depths new-pat) + orig-names* new-names* depths* new-pat*) + (values (append orig-names orig-names*) + (append new-names new-names*) + (append depths depths*) + (cons new-pat new-pat*))) + (syntax-case stx (...) + [x + (and (identifier? #'x) + (not (free-identifier=? (quote-syntax ...) #'x))) + (let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)]) + (values (list #'x) + (list new-name) + (list depth) + new-name))] + [(x (... ...) . xs) + (let-values ([(orig-names new-names depths new-pat) + (call-with-values + (λ () (loop #'xs depth)) + (call-with-values + (λ () (loop #'x (add1 depth))) + combine))]) + (values orig-names new-names depths + (list* (car new-pat) #'(... ...) (cdr new-pat))))] + [(x . xs) + (call-with-values + (λ () (loop #'xs depth)) + (call-with-values + (λ () (loop #'x depth)) + combine))] + [_ + (values '() '() '() stx)]))) (with-syntax ([(orig-names ...) orig-names] [(new-names ...) new-names] [(depths ...) depths] diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt index 5aeec908df..8849e83f28 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt @@ -24,8 +24,9 @@ (check-equal? (rsc (1) () #t) `((list 1) () ())) (check-equal? (rsc (_ _ (name x _)) () #t) `((list any any (name x any)) (x) (x))) (check-equal? (rsc (1 ...) () #t) `((list (repeat 1 #f #f)) () ())) -(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 #f #f)) () ())) -(check-equal? (rsc (1 ..._2 1 ..._2) () #t) `((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) () ())) +(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 ..._2 #f)) (..._2) (..._2))) +(check-equal? (rsc (1 ..._2 1 ..._2) () #t) + `((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) (..._2 ..._2) (..._2 ..._2))) (check-equal? (rsc (1 ..._!_3) () #t) `((list (repeat 1 #f #f)) () ())) (check-equal? (rsc (1 ..._!_3 1 ..._!_3) () #t) `((list (repeat 1 #f ..._!_3) (repeat 1 #f ..._!_3)) () ())) @@ -42,7 +43,9 @@ `((list (repeat (list (repeat (name x (nt x)) #f #f)) #f #f)) (x) (((x ...) ...)))) - +(check-equal? (rsc (any_1 any_1) (x) #f) `((list (name any_1 any) (name any_1 any)) + (any_1 any_1) + (any_1 any_1))) (check-equal? (rsc (in-hole (hole a #f (hide-hole hole)) (cross x)) '(x) #f) `((in-hole (list hole a #f (hide-hole hole)) (cross x-x)) ()