From 48c719a3ee6c6533aaa7535d10f7c9bfe6addaf3 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Thu, 2 May 2013 09:58:14 -0500 Subject: [PATCH] Refactor Redex so that it tells Check Syntax that non-terminal references are binding/bound variables (beyond those appearing in the define-language itself) Specifically, - change define-language (and friends) so they record binding and source location information for non-terminals in the identifier that names the language (and to expand to disappeared bindings); - change rewrite-side-conditions/check-errs so that it accepts the language identifier (instead of a list of non-terminals) and returns one extra piece of syntax: that extra piece of syntax is just (void), but it has a bunch of disappeared uses on it that connect to the identifiers added to define-language; - similarly, adjust (term ...) so that it puts disappeared uses for non-terminal references. --- .../cont-mark-transform/randomized-tests.rkt | 2 +- collects/redex/private/generate-term.rkt | 65 ++-- collects/redex/private/judgment-form.rkt | 138 +++++---- .../redex/private/reduction-semantics.rkt | 281 ++++++++++-------- .../redex/private/rewrite-side-conditions.rkt | 32 +- collects/redex/private/term-fn.rkt | 30 +- collects/redex/private/term.rkt | 74 +++-- .../tests/rewrite-side-condition-test.rkt | 2 +- collects/redex/tests/unify-tests.rkt | 4 +- 9 files changed, 387 insertions(+), 241 deletions(-) diff --git a/collects/redex/examples/cont-mark-transform/randomized-tests.rkt b/collects/redex/examples/cont-mark-transform/randomized-tests.rkt index 155fcf052b..e0b6f87f1d 100644 --- a/collects/redex/examples/cont-mark-transform/randomized-tests.rkt +++ b/collects/redex/examples/cont-mark-transform/randomized-tests.rkt @@ -4,7 +4,7 @@ "TL-syntax.rkt" "TL-semantics.rkt" "CMT.rkt" "common.rkt" - redex) + redex/reduction-semantics) (provide main same-result?) (define (main . args) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index 4e072eaf5b..35fce4cca0 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -85,9 +85,9 @@ (define-syntax (redex-check stx) (syntax-case stx () [(form lang pat property . kw-args) - (with-syntax ([(pattern (name ...) (name/ellipses ...)) + (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...)) (rewrite-side-conditions/check-errs - (language-id-nts #'lang 'redex-check) + #'lang 'redex-check #t #'pat)] [show (show-message stx)]) (let-values ([(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx) @@ -114,6 +114,7 @@ [term-match (λ (generated) (cond [(test-match lang pat generated) => values] [else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))]) + syncheck-exp (parameterize ([attempt->size #,size-stx]) #,(if source-stx #`(let-values ([(metafunc/red-rel num-cases) @@ -329,19 +330,17 @@ (when (keyword? k) (unless (member k '(#:satisfying #:source #:attempt-num #:retries #:i-th)) (raise-syntax-error 'generate-term "unknown keyword" stx x)))))) - (define form-name (with-syntax ([(_ orig-name . args) stx]) - (syntax-e #'orig-name))) (syntax-case stx () [(_ orig-name lang pat #:i-th . rest) - (with-syntax ([(pattern (vars ...) (vars/ellipses ...)) + (with-syntax ([(syncheck-exp pattern (vars ...) (vars/ellipses ...)) (rewrite-side-conditions/check-errs - (language-id-nts #'lang form-name) - form-name #t #'pat)]) + #'lang + (syntax-e #'orig-name) #t #'pat)]) (syntax-case #'rest () [() - #'(generate-ith/proc lang `pattern)] + #'(begin syncheck-exp (generate-ith/proc lang `pattern))] [(i-expr) - #'((generate-ith/proc lang `pattern) i-expr)]))] + #'(begin syncheck-exp ((generate-ith/proc lang `pattern) i-expr))]))] [(_ orig-name language #:satisfying (jf/mf-id . args) . rest) (cond [(metafunc #'jf/mf-id) @@ -400,27 +399,27 @@ => (λ (f) #`(let* ([f #,f] [L (metafunc-proc-lang f)] - [compile-pat (compile L '#,form-name)] + [compile-pat (compile L 'orig-name)] [cases (metafunc-proc-cases f)]) (check-cases 'src cases) (map (λ (c) (compile-pat ((metafunc-case-lhs+ c) L))) cases)))] [else - #`(let* ([r #,(apply-contract #'reduction-relation? #'src "#:source argument" form-name)] + #`(let* ([r #,(apply-contract #'reduction-relation? #'src "#:source argument" (syntax-e #'orig-name))] [L (reduction-relation-lang r)] - [compile-pat (compile L '#,form-name)]) + [compile-pat (compile L 'orig-name)]) (map (λ (p) (compile-pat ((rewrite-proc-lhs p) L))) (reduction-relation-make-procs r)))]) #'rest)] [(lang pat . rest) - (with-syntax ([(pattern (vars ...) (vars/ellipses ...)) + (with-syntax ([(syncheck-exp pattern (vars ...) (vars/ellipses ...)) (rewrite-side-conditions/check-errs - (language-id-nts #'lang form-name) - form-name #t #'pat)]) - (values #`(list #,(term-generator #'lang #'pattern form-name)) + #'lang + (syntax-e #'orig-name) #t #'pat)]) + (values #`(begin syncheck-exp (list #,(term-generator #'lang #'pattern (syntax-e #'orig-name)))) #'rest))])) (define generator-syntax - #`(make-generator #,raw-generators '#,form-name)) + #`(make-generator #,raw-generators 'orig-name)) (syntax-case args () [() generator-syntax] @@ -473,16 +472,18 @@ [args-stx (if relation? (syntax/loc #'args (args)) #'args)]) - (with-syntax ([(pat (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs nts 'redex-generator #t args-stx)]) - (if relation? - #`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)]) - (λ () - (match (gen-proc) - [`(,jf-name (,trms (... ...))) - `(,jf-name ,@trms)] - [#f #f]))) - #`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))] + (with-syntax ([(syncheck-exp pat (names ...) (names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang-id 'redex-generator #t args-stx)]) + #`(begin + syncheck-exp + #,(if relation? + #`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)]) + (λ () + (match (gen-proc) + [`(,jf-name (,trms (... ...))) + `(,jf-name ,@trms)] + [#f #f]))) + #`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)))))] [_ (raise-syntax-error 'redex-generator "expected an integer depth bound" @@ -496,12 +497,12 @@ (let () (define mf (syntax-local-value #'jf/mf-id (λ () #f))) (define nts (definition-nts #'lang-id stx 'redex-generator)) - (with-syntax ([(lhs-pat (lhs-names ...) (lhs-names/ellipses ...)) - (rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'args)] - [(rhs-pat (rhs-names ...) (rhs-names/ellipses ...)) - (rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'res)] + (with-syntax ([(lhs-syncheck-exp lhs-pat (lhs-names ...) (lhs-names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang-id (syntax-e #'g-m-p) #t #'args)] + [(rhs-syncheck-exp rhs-pat (rhs-names ...) (rhs-names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang-id (syntax-e #'g-m-p) #t #'res)] [mf-id (term-fn-get-id mf)]) - #`(make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size)))] + #`(begin lhs-syncheck-exp rhs-syncheck-exp (make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size))))] [_ (raise-syntax-error 'redex-generator "expected \"=\" followed by a result pattern and an integer depth bound" diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt index 98ce128a44..91098a8317 100644 --- a/collects/redex/private/judgment-form.rkt +++ b/collects/redex/private/judgment-form.rkt @@ -64,13 +64,16 @@ [(a . b) (datum->syntax (identifier-prune-lexical-context #'whatever '(#%app)) (cons (loop #'a) (loop #'b)) + stx stx)] [x (identifier? #'x) (identifier-prune-lexical-context #'x (list (syntax-e #'x) '#%top))] [() (datum->syntax #f '() stx)] [_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum)) - (syntax->datum stx) stx)])))) + (syntax->datum stx) + stx + stx)])))) (define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation")) (define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation")) @@ -107,7 +110,12 @@ (hash-set extended (syntax-e name) w/ellipses)))) ;; 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 names w/ellipses side-condition-unquoted? jf-results-id) +;; rt-lang is an identifier that will be bound to a (runtime) language, +;; not necc bound via define-language. +;; ct-lang is an identifier guaranteed to be bound by define-language +;; that can be used to call rewrite-side-conditions/check-errs, but +;; some extension of that language may end up being bound to rt-lang +(define-for-syntax (bind-withs orig-name main rt-lang lang-nts ct-lang stx where-mode body names w/ellipses side-condition-unquoted? jf-results-id) (with-disappeared-uses (let loop ([stx stx] [to-not-be-in main] @@ -119,13 +127,13 @@ [((-where x e) y ...) (where-keyword? #'-where) (let () - (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) + (with-syntax ([(syncheck-exp side-conditions-rewritten (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs - lang-nts + ct-lang 'reduction-relation #t #'x)] - [lang-stx lang]) + [lang-stx rt-lang]) (define-values (binding-constraints temporaries env+) (generate-binding-constraints (syntax->list #'(names ...)) (syntax->list #'(names/ellipses ...)) @@ -134,18 +142,20 @@ (with-syntax ([(binding-constraints ...) binding-constraints] [(x ...) temporaries]) (define rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+)) - #`(#,(case where-mode + #`(begin + syncheck-exp + (#,(case where-mode [(flatten) #'combine-where-results/flatten] [(predicate) #'combine-where-results/predicate] [else (error 'unknown-where-mode "~s" where-mode)]) - (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term/nts e #,lang-nts)) + (match-pattern (compile-pattern #,rt-lang `side-conditions-rewritten #t) (term e #:lang #,ct-lang)) (λ (bindings) (let ([x (lookup-binding bindings 'names)] ...) (and binding-constraints ... (term-let ([names/ellipses x] ...) - #,rest-body))))))))] + #,rest-body)))))))))] [((-side-condition s ...) y ...) (side-condition-keyword? #'-side-condition) (if side-condition-unquoted? @@ -194,17 +204,18 @@ (let ([ellipsis (syntax/loc premise (... ...))]) (values #`(#,in #,ellipsis) #`(#,out #,ellipsis))) (values in out)))] - [(output-pattern output-names output-names/ellipses) - (with-syntax ([(output names names/ellipses) - (rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)]) - (values #'output + [(syncheck-exp output-pattern output-names output-names/ellipses) + (with-syntax ([(syncheck-exp output names names/ellipses) + (rewrite-side-conditions/check-errs ct-lang orig-name #t output-pre-pattern)]) + (values #'syncheck-exp + #'output (syntax->list #'names) (syntax->list #'names/ellipses)))] [(binding-constraints temporaries env+) (generate-binding-constraints output-names output-names/ellipses env orig-name)] [(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)] [(call) - (let ([input (quasisyntax/loc premise (term/nts #,input-template #,lang-nts))]) + (let ([input (quasisyntax/loc premise (term #,input-template #:lang #,ct-lang))]) (define (make-traced input) (quasisyntax/loc premise (call-judgment-form 'form-name #,judgment-proc '#,mode #,input #,(if jf-results-id #''() #f)))) @@ -217,9 +228,10 @@ [(temp ...) temporaries] [(binding-constraint ...) binding-constraints]) #`(begin + #,syncheck-exp (void #,(defined-check judgment-proc "judgment form" #:external #'form-name)) (judgment-form-bind-withs/proc - #,lang + #,rt-lang `#,output-pattern #,call #,under-ellipsis? @@ -674,7 +686,7 @@ (error 'syn-err-name "judgment forms with output mode positions cannot currently be used in term")) (with-syntax* ([(binding ...) (generate-temporaries (cdr (syntax->list #'mode)))] [(input) (generate-temporaries (list #'input))] - [body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts) + [body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts) #'lang (if (jf-is-relation? #'jdg-name) (list #'(jdg-name ((unquote-splicing input)))) (list #'(jdg-name (unquote binding) ...))) @@ -710,7 +722,8 @@ (car (generate-temporaries '(jf-derivation-lst))) #f)] [main-stx - (bind-withs syn-err-name '() lang nts (list judgment) + (bind-withs syn-err-name '() lang nts lang + (list judgment) 'flatten (if derivation? id-or-not @@ -749,7 +762,7 @@ [(_ jf-expr) #'(#%expression (judgment-holds/derivation build-derivations #t jf-expr any))])) -(define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses rule-names contracts nts orig stx syn-error-name) +(define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses rule-names contracts nts orig lang stx syn-error-name) (with-syntax ([(init-jf-derivation-id) (generate-temporaries '(init-jf-derivation-id))]) (define mode (cdr (syntax->datum mode-stx))) (define-values (input-contracts output-contracts) @@ -761,19 +774,19 @@ (syntax-case clause () [((_ . conc-pats) . prems) (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)]) - (with-syntax ([(lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts syn-error-name #t input-pats)] + (with-syntax ([(lhs-syncheck-exp lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs lang syn-error-name #t input-pats)] [(jf-derivation-id) (generate-temporaries '(jf-derivation-id))]) (define (contracts-compilation ctcs) - (and ctcs - (with-syntax ([(ctc ...) ctcs]) - #`(list (compile-pattern lang `ctc #f) ...)))) + (with-syntax ([(ctc ...) ctcs]) + #`(list (compile-pattern lang `ctc #f) ...))) (define body (parameterize ([judgment-form-pending-expansion (cons name (struct-copy judgment-form (lookup-judgment-form-id name) [proc #'recur]))]) - (bind-withs syn-error-name '() #'lang nts (syntax->list #'prems) - 'flatten #`(list (derivation-with-output-only (term/nts (#,@output-pats) #,nts) + (bind-withs syn-error-name '() lang nts lang + (syntax->list #'prems) + 'flatten #`(list (derivation-with-output-only (term (#,@output-pats) #:lang #,lang) #,clause-name jf-derivation-id)) (syntax->list #'(names ...)) @@ -786,16 +799,17 @@ #`( ;; pieces of a 'let' expression to be combined: first some bindings ([compiled-lhs (compile-pattern lang `lhs #t)] - #,@(if (contracts-compilation input-contracts) + #,@(if input-contracts (list #`[compiled-input-ctcs #,(contracts-compilation input-contracts)]) (list)) - #,@(if (contracts-compilation output-contracts) + #,@(if output-contracts (list #`[compiled-output-ctcs #,(contracts-compilation output-contracts)]) (list))) ;; and then the body of the let, but expected to be behind a (λ (input) ...). (let ([jf-derivation-id init-jf-derivation-id]) (begin - #,@(if (contracts-compilation input-contracts) + lhs-syncheck-exp + #,@(if input-contracts (list #`(check-judgment-form-contract '#,name input compiled-input-ctcs 'I '#,mode)) (list)) (combine-judgment-rhses @@ -804,7 +818,7 @@ (λ (bnds) (term-let ([names/ellipses (lookup-binding bnds 'names)] ...) #,body)) - #,(if (contracts-compilation output-contracts) + #,(if output-contracts #`(λ (output) (check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode)) #`void))))))))])) @@ -1086,14 +1100,22 @@ [mode (cdr (syntax->datum #'mode-arg))]) (unless (jf-is-relation? #'judgment-form-name) (mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx)) - (define contracts (syntax-case #'ctcs () - [#f #f] - [(p ...) - (map (λ (pat) - (with-syntax ([(pat (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs nts #'syn-error-name #f pat)]) - #'pat)) - (syntax->list #'(p ...)))])) + (define-values (syncheck-exprs contracts) + (syntax-case #'ctcs () + [#f (values '() #f)] + [(p ...) + (let loop ([pats (syntax->list #'(p ...))] + [ctcs '()] + [syncheck-exps '()]) + (cond + [(null? pats) (values syncheck-exps (reverse ctcs))] + [else + (define pat (car pats)) + (with-syntax ([(syncheck-exp pat (names ...) (names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang #'syn-error-name #f pat)]) + (loop (cdr pats) + (cons #'pat ctcs) + (cons #'syncheck-exp syncheck-exps)))]))])) (define proc-stx (do-compile-judgment-form-proc #'judgment-form-name #'mode-arg clauses @@ -1101,10 +1123,11 @@ contracts nts #'orig + #'lang #'full-def syn-err-name)) (define gen-stx (with-syntax* ([(comp-clauses ...) - (map (λ (c) (compile-gen-clause c mode nts syn-err-name + (map (λ (c) (compile-gen-clause c mode syn-err-name #'judgment-form-name #'lang)) clauses)]) (if (identifier? #'orig) @@ -1120,7 +1143,7 @@ (λ () #,(check-pats #'(list comp-clauses ...))))))) - #`(values #,proc-stx #,gen-stx))])) + #`(begin #,@syncheck-exprs (values #,proc-stx #,gen-stx)))])) (define-for-syntax (rewrite-relation-prems clauses) (map (λ (c) @@ -1189,7 +1212,7 @@ [syn-err-name (syntax-e #'syn-err-name)] [mode (cdr (syntax->datum #'mode-arg))]) (with-syntax* ([(comp-clauses ...) - (map (λ (c) (compile-gen-clause c mode nts syn-err-name + (map (λ (c) (compile-gen-clause c mode syn-err-name #'judgment-form-name #'lang)) clauses)]) (if (identifier? #'orig) @@ -1339,32 +1362,36 @@ -(define-for-syntax (compile-gen-clause clause-stx mode nts syn-error-name jdg-name lang) +(define-for-syntax (compile-gen-clause clause-stx mode syn-error-name jdg-name lang) (syntax-case clause-stx () [((conc-name . conc-body-raw) prems ...) (let*-values ([(conc/+ conc/-) (split-by-mode (syntax->list #'conc-body-raw) mode)] - [(conc/+rw names) (rewrite-pats conc/+ nts)] - [(ps-rw eqs p-names) (rewrite-prems #t (syntax->list #'(prems ...)) nts names 'define-judgment-form)] + [(syncheck-exps conc/+rw names) (rewrite-pats conc/+ lang)] + [(ps-rw eqs p-names) (rewrite-prems #t (syntax->list #'(prems ...)) names lang 'define-judgment-form)] [(conc/-rw conc-mfs) (rewrite-terms conc/- p-names)] [(conc) (fuse-by-mode conc/+rw conc/-rw mode)]) (with-syntax ([(c ...) conc] [(c-mf ...) conc-mfs] [(eq ...) eqs] [(prem-bod ...) (reverse ps-rw)]) - #`(clause '(list c ...) (list eq ...) (list c-mf ... prem-bod ...) effective-lang '#,jdg-name)))])) + #`(begin #,@syncheck-exps + (clause '(list c ...) (list eq ...) (list c-mf ... prem-bod ...) effective-lang '#,jdg-name))))])) -(define-for-syntax (rewrite-prems in-judgment-form? prems nts names what) +(define-for-syntax (rewrite-prems in-judgment-form? prems names lang what) (define (rewrite-jf prem-name prem-body ns ps-rw eqs) (define p-form (lookup-judgment-form-id prem-name)) (define p-mode (judgment-form-mode p-form)) (define p-clauses (judgment-form-gen-clauses p-form)) (define-values (p/-s p/+s) (split-by-mode (syntax->list prem-body) p-mode)) (define-values (p/-rws mf-apps) (rewrite-terms p/-s ns)) - (define-values (p/+rws new-names) (rewrite-pats p/+s nts)) + (define-values (syncheck-exps p/+rws new-names) (rewrite-pats p/+s lang)) (define p-rw (fuse-by-mode p/-rws p/+rws p-mode)) (with-syntax ([(p ...) p-rw]) - (values (cons #`(prem #,p-clauses '(list p ...)) (append mf-apps ps-rw)) + (values (cons #`(begin + #,@syncheck-exps + (prem #,p-clauses '(list p ...))) + (append mf-apps ps-rw)) eqs (append ns new-names)))) (define-values (prems-rev new-eqs new-names) @@ -1376,9 +1403,9 @@ [(-where pat term) (where-keyword? #'-where) (let-values ([(term-rws mf-cs) (rewrite-terms (list #'term) ns)]) - (with-syntax ([(pat-rw new-names) (rewrite/pat #'pat nts)]) + (with-syntax ([(syncheck-exp pat-rw new-names) (rewrite/pat #'pat lang)]) (values (append mf-cs ps-rw) - (cons #`(eqn 'pat-rw '#,(car term-rws)) eqs) + (cons #`(begin syncheck-exp (eqn 'pat-rw '#,(car term-rws))) eqs) (append (syntax->datum #'new-names) ns))))] [(side-cond rest) (side-condition-keyword? #'side-cond) @@ -1401,18 +1428,19 @@ [else (raise-syntax-error what "malformed premise" prem)]))) (values prems-rev new-eqs new-names)) -(define-for-syntax (rewrite-pats pats nts) - (with-syntax ([((pat-rw (names ...)) ...) - (map (λ (p) (rewrite/pat p nts)) +(define-for-syntax (rewrite-pats pats lang) + (with-syntax ([((syncheck-exp pat-rw (names ...)) ...) + (map (λ (p) (rewrite/pat p lang)) pats)]) - (values (syntax->list #'(pat-rw ...)) + (values #'(syncheck-exp ...) + (syntax->list #'(pat-rw ...)) (remove-duplicates (syntax->datum #'(names ... ...)))))) -(define-for-syntax (rewrite/pat pat nts) - (with-syntax ([(body (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs nts #'rewrite/pat #t pat)]) - #'(body (names ...)))) +(define-for-syntax (rewrite/pat pat lang) + (with-syntax ([(syncheck-exp body (names ...) (names/ellipses ...)) + (rewrite-side-conditions/check-errs lang #'rewrite/pat #t pat)]) + #'(syncheck-exp body (names ...)))) (define-for-syntax (rewrite-terms terms names) (with-syntax* ([((term-pattern ((res-pat ((metafunc f) args-pat)) ...) body-pat) ...) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 735975815a..987c4b20ea 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -42,13 +42,14 @@ (begin (unless (identifier? #'lang) (raise-syntax-error (syntax-e #'form-name) "expected an identifier in the language position" orig-stx #'lang)) - (let ([lang-nts (language-id-nts #'lang (syntax-e #'form-name))]) - (with-syntax ([((side-conditions-rewritten (names ...) (names/ellipses ...)) ...) - (map (λ (x) (rewrite-side-conditions/check-errs lang-nts (syntax-e #'form-name) #t x)) - (syntax->list (syntax (pattern ...))))] - [(cp-x ...) (generate-temporaries #'(pattern ...))] - [make-matcher make-matcher]) - #'(make-matcher + (with-syntax ([((syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) ...) + (map (λ (x) (rewrite-side-conditions/check-errs #'lang (syntax-e #'form-name) #t x)) + (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) ...) @@ -144,29 +145,32 @@ (syntax-case stx () [(_ red lang nt) (identifier? (syntax nt)) - (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs (language-id-nts #'lang 'compatible-closure) + (with-syntax ([(syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang 'compatible-closure #t (syntax (cross nt)))]) - (syntax (do-context-closure red lang `side-conditions-rewritten 'compatible-closure)))] + (syntax (begin syncheck-expr + (do-context-closure red lang `side-conditions-rewritten 'compatible-closure))))] [(_ red lang nt) (raise-syntax-error 'compatible-closure "expected a non-terminal as last argument" stx (syntax nt))])) (define-syntax (context-closure stx) (syntax-case stx () [(_ red lang pattern) - (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs (language-id-nts #'lang 'context-closure) + (with-syntax ([(syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) + (rewrite-side-conditions/check-errs #'lang 'context-closure #t (syntax pattern))]) (syntax - (do-context-closure - red - lang - `side-conditions-rewritten - 'context-closure)))])) + (begin + syncheck-expr + (do-context-closure + red + lang + `side-conditions-rewritten + 'context-closure))))])) (define (do-context-closure red lang pat name) (unless (reduction-relation? red) @@ -595,8 +599,7 @@ (for-each loop nexts))))) all-top-levels) - (let ([name-table (make-hasheq)] - [lang-nts (language-id-nts lang-id orig-name)]) + (let ([name-table (make-hasheq)]) (hash-set! name-table #f 0) ;; name table maps symbols for the rule names to their syntax objects and to a counter indicating what ;; order the names were encountered in. The current value of the counter is stored in the table at key '#f'. @@ -609,20 +612,21 @@ (map car (sort (hash-map name-table (λ (k v) (list k (list-ref v 1)))) < #:key cadr)))] [lws lws] - [(domain-pattern-side-conditions-rewritten (names ...) (names/ellipses ...)) + [(domain-syncheck-expr domain-pattern-side-conditions-rewritten (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs - lang-nts + lang-id orig-name #f domain-pattern)]) - - #`(build-reduction-relation - #,orig-red-expr - lang-id - (list top-level ...) - '(rule-names ...) - lws - `domain-pattern-side-conditions-rewritten))))) + #`(begin + domain-syncheck-expr + (build-reduction-relation + #,orig-red-expr + lang-id + (list top-level ...) + '(rule-names ...) + lws + `domain-pattern-side-conditions-rewritten)))))) #| ;; relation-tree = @@ -659,29 +663,32 @@ (syntax->list (syntax (extras ...))) lang-id))] [((rhs-arrow rhs-from rhs-to) (lhs-arrow lhs-frm-id lhs-to-id)) - (let* ([lang-nts (language-id-nts lang-id orig-name)] - [rewrite-side-conds - (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) - (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) + (let ([lang-nts (language-id-nts lang-id 'reduction-relation)] + [rewrite-side-conds + (λ (pat) (rewrite-side-conditions/check-errs lang-id orig-name #t pat))]) + (with-syntax ([(lhs-syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) (rewrite-side-conds (rewrite-node-pat (syntax-e (syntax lhs-frm-id)) (syntax rhs-from)))] - [(fresh-rhs-from (fresh-names ...) (fresh-names/ellipses ...)) + [(rhs-syncheck-expr fresh-rhs-from (fresh-names ...) (fresh-names/ellipses ...)) (rewrite-side-conds (freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))] [lang lang]) (map (λ (child-proc) - #`(do-node-match - '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))) - #,child-proc - `fresh-rhs-from)) + #`(begin + lhs-syncheck-expr + rhs-syncheck-expr + (do-node-match + '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))) + #,child-proc + `fresh-rhs-from))) (get-choices stx orig-name bm #'lang (syntax lhs-arrow) name-table lang-id @@ -726,54 +733,59 @@ p)]))))) (define (do-leaf stx orig-name lang name-table from to extras lang-id) - (let* ([lang-nts (language-id-nts lang-id orig-name)] - [rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) - (let-values ([(name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras)]) - (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)]) - (define body-code - (bind-withs orig-name - #'main-exp - lang - lang-nts - sides/withs/freshs - 'flatten - #`(list (cons #,(or computed-name #'none) - (term #,to #:lang #,lang))) - (syntax->list #'(names ...)) - (syntax->list #'(names/ellipses ...)) - #t - #f)) - (define test-case-body-code - ;; this contains some redundant code - (bind-withs orig-name - #'#t - #'lang-id2 - lang-nts - sides/withs/freshs - 'predicate - #'#t - (syntax->list #'(names ...)) - (syntax->list #'(names/ellipses ...)) - #t - #f)) - (with-syntax ([(lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...)) - (rw-sc #`(side-condition #,from #,test-case-body-code))] - [lhs-source (format "~a:~a:~a" - (and (path? (syntax-source from)) - (path->relative-string/library (syntax-source from))) - (syntax-line from) - (syntax-column from))] - [name name] - [lang lang] - [body-code body-code]) - #` + (define lang-nts (language-id-nts lang-id 'reduction-relation)) + (define (rw-sc pat) (rewrite-side-conditions/check-errs lang-id orig-name #t pat)) + (define-values (name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras)) + (with-syntax ([(from-syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)]) + (define body-code + (bind-withs orig-name + #'main-exp + lang + lang-nts + lang-id + sides/withs/freshs + 'flatten + #`(begin + from-syncheck-expr + (list (cons #,(or computed-name #'none) + (term #,to #:lang #,lang)))) + (syntax->list #'(names ...)) + (syntax->list #'(names/ellipses ...)) + #t + #f)) + (define test-case-body-code + ;; this contains some redundant code + (bind-withs orig-name + #'#t + #'lang-id2 + lang-nts + lang-id + sides/withs/freshs + 'predicate + #'#t + (syntax->list #'(names ...)) + (syntax->list #'(names/ellipses ...)) + #t + #f)) + (with-syntax ([(lhs-syncheck-expr lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...)) + (rw-sc #`(side-condition #,from #,test-case-body-code))] + [lhs-source (format "~a:~a:~a" + (and (path? (syntax-source from)) + (path->relative-string/library (syntax-source from))) + (syntax-line from) + (syntax-column from))] + [name name] + [lang lang] + [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))))))) + (λ (lang-id2) `lhs-w/extras)))))) (define (process-extras stx orig-name name-table extras) (let* ([the-name #f] @@ -1037,13 +1049,15 @@ (syntax-case stx () [(form-name lang-exp pattern) (identifier? #'lang-exp) - (let*-values ([(what) (syntax-e #'form-name)] - [(nts) (language-id-nts #'lang-exp what)]) - (with-syntax ([(side-condition-rewritten (vars ...) (ids/depths ...)) - (rewrite-side-conditions/check-errs nts what #t #'pattern)]) + (let () + (define what (syntax-e #'form-name)) + (with-syntax ([(syncheck-expr side-condition-rewritten (vars ...) (ids/depths ...)) + (rewrite-side-conditions/check-errs #'lang-exp what #t #'pattern)]) (with-syntax ([binders (map syntax-e (syntax->list #'(vars ...)))] [name (syntax-local-infer-name stx)]) - #`(do-test-match lang-exp `side-condition-rewritten 'binders 'name #,boolean-only?))))] + #`(begin + syncheck-expr + (do-test-match lang-exp `side-condition-rewritten 'binders 'name #,boolean-only?)))))] [(form-name lang-exp pattern expression) (identifier? #'lang-exp) (syntax @@ -1222,9 +1236,9 @@ [(lhs ...) #'((lhs-clauses ...) ...)]) (with-syntax ([((clause-name stuff ...) ...) (extract-clause-names #'((stuff+names ...) ...))]) (parse-extras #'((stuff ...) ...)) - (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) + (with-syntax ([((syncheck-expr side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) (map (λ (x) (rewrite-side-conditions/check-errs - lang-nts + #'lang syn-error-name #t x)) @@ -1233,7 +1247,7 @@ (map (λ (sc/b rhs names names/ellipses) (bind-withs syn-error-name '() - #'effective-lang lang-nts + #'effective-lang lang-nts #'lang sc/b 'flatten #`(list (term #,rhs #:lang lang)) (syntax->list names) @@ -1248,7 +1262,7 @@ (map (λ (sc/b rhs names names/ellipses) (bind-withs syn-error-name '() - #'effective-lang lang-nts + #'effective-lang lang-nts #'lang sc/b 'predicate #`#t (syntax->list names) @@ -1259,9 +1273,9 @@ (syntax->list #'(rhs ...)) (syntax->list #'(lhs-names ...)) (syntax->list #'(lhs-namess/ellipses ...)))]) - (with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...) + (with-syntax ([((rg-syncheck-expr rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...) (map (λ (x) (rewrite-side-conditions/check-errs - lang-nts + #'lang syn-error-name #t x)) @@ -1274,18 +1288,18 @@ (syntax-line lhs) (syntax-column lhs))) pats)] - [(dom-side-conditions-rewritten dom-names dom-names/ellipses) + [(dom-syncheck-expr dom-side-conditions-rewritten dom-names dom-names/ellipses) (if dom-ctcs (rewrite-side-conditions/check-errs - lang-nts + #'lang syn-error-name #f dom-ctcs) - #'(any () ()))] - [((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...) + #'((void) any () ()))] + [((codom-syncheck-expr codom-side-conditions-rewritten codom-names codom-names/ellipses) ...) (map (λ (codom-contract) (rewrite-side-conditions/check-errs - lang-nts + #'lang syn-error-name #f codom-contract)) @@ -1312,6 +1326,7 @@ (prune-syntax #`(let ([sc `(side-conditions-rewritten ...)] [dsc `dom-side-conditions-rewritten]) + syncheck-expr ... rg-syncheck-expr ... dom-syncheck-expr codom-syncheck-expr ... (let ([cases (map (λ (pat rhs-fn rg-lhs src) (make-metafunc-case (λ (effective-lang) (compile-pattern effective-lang pat #t)) @@ -1403,10 +1418,10 @@ (define-values (rev-clauses _1 _2) (for/fold ([clauses '()] [prev-lhs-pats '()] [prev-lhs-pats* '()]) ([lhs (in-list lhss)] [rhs (in-list rhss)] [extras (in-list extrass)]) - (with-syntax* ([(lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts err-name #t lhs)] + (with-syntax* ([(lhs-syncheck-expr lhs-pat (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs lang err-name #t lhs)] [((lhs-pat-ps* ...) lhs-pat*) (fix-and-extract-dq-vars #'lhs-pat)]) (define-values (ps-rw extra-eqdqs p-names) - (rewrite-prems #f (syntax->list extras) nts (syntax->datum #'(names ...)) 'define-metafunction)) + (rewrite-prems #f (syntax->list extras) (syntax->datum #'(names ...)) lang 'define-metafunction)) (define-values (rhs-pats mf-clausess) (rewrite-terms (list rhs) p-names)) (define clause-stx (with-syntax ([(prem-rw ...) ps-rw] @@ -1414,11 +1429,13 @@ [(((prev-lhs-pat-ps ...) prev-lhs-pat) ...) prev-lhs-pats*] [(mf-clauses ...) mf-clausess] [(rhs-pat) rhs-pats]) - #`((clause '(list lhs-pat rhs-pat) - (list eqs ... (dqn '(prev-lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...) - (list prem-rw ... mf-clauses ...) - #,lang - '#,name) + #`((begin + lhs-syncheck-expr + (clause '(list lhs-pat rhs-pat) + (list eqs ... (dqn '(prev-lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...) + (list prem-rw ... mf-clauses ...) + #,lang + '#,name)) lhs-pat ((lhs-pat-ps* ...) lhs-pat*)))) (values (cons clause-stx clauses) @@ -1708,11 +1725,29 @@ (unless (identifier? #'lang-name) (raise-syntax-error #f "expected an identifier" stx #'lang-name)) (with-syntax ([(define-language-name) (generate-temporaries #'(lang-name))]) - (let ([non-terms (parse-non-terminals #'nt-defs stx)]) - (with-syntax ([((names prods ...) ...) non-terms] - [(all-names ...) (apply append (map car non-terms))]) + (define non-terms (parse-non-terminals #'nt-defs stx)) + (with-syntax ([((names prods ...) ...) non-terms] + [(all-names ...) (apply append (map car non-terms))] + [(nt-ids ...) + (for/list ([nt-def (in-list (syntax->list #'nt-defs))]) + (syntax-case nt-def () + [(x . whatever) #'x]))]) + (with-syntax ([bindings + (let loop ([nt-ids (syntax->list #'(nt-ids ...))] + [stx #'(void)]) + (cond + [(null? nt-ids) stx] + [else + (define old (syntax-property stx 'disappeared-binding)) + (define new (syntax-local-introduce (car nt-ids))) + (loop (cdr nt-ids) + (syntax-property stx + 'disappeared-binding + (if old (cons new old) new)))]))]) + (quasisyntax/loc stx (begin + bindings (define-syntax lang-name (make-set!-transformer (make-language-id @@ -1724,10 +1759,15 @@ [x (identifier? #'x) #'define-language-name])) - '(all-names ...)))) + '(all-names ...) + (to-table #'(nt-ids ...))))) (define define-language-name #,(syntax/loc stx (language form-name lang-name (all-names ...) (names prods ...) ...)))))))))])) +(define-for-syntax (to-table x) + (for/hash ([id (in-list (syntax->list x))]) + (values (syntax-e id) id))) + (define-struct binds (source binds)) (define-syntax (language stx) @@ -1736,11 +1776,12 @@ (prune-syntax (let () (let ([all-names (syntax->list #'(all-names ...))]) - (with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...) + (with-syntax ([(((r-syncheck-expr r-rhs r-names r-names/ellipses) ...) ...) + ;; r-syncheck-expr has nothing interesting, I believe, so drop it (map (lambda (rhss) (map (lambda (rhs) (rewrite-side-conditions/check-errs - (map syntax-e all-names) + #'lang-id (syntax-e #'form-name) #f rhs)) @@ -1833,12 +1874,13 @@ [x (identifier? #'x) #'define-language-name])) - '(all-names ...))))))))])) + '(all-names ...) + (to-table #'()))))))))])) (define-syntax (extend-language stx) (syntax-case stx () [(_ lang (all-names ...) (name rhs ...) ...) - (with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...) + (with-syntax ([(((r-syncheck-expr r-rhs r-names r-names/ellipses) ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs (append (language-id-nts #'lang 'define-extended-language) (map syntax-e @@ -1854,7 +1896,7 @@ (map (λ (x) (if (identifier? x) (list x) x)) (syntax->list (syntax (name ...))))]) (syntax/loc stx - (do-extend-language lang + (do-extend-language (begin r-syncheck-expr ... ... lang) (list (make-nt '(uniform-names ...) (list (make-rhs `r-rhs) ...)) ...) (list (list '(uniform-names ...) rhs/lw ...) ...))))])) @@ -1992,7 +2034,8 @@ [x (identifier? #'x) #'define-language-name])) - '(all-names ...)))))))])) + '(all-names ...) + (to-table #'())))))))])) (define (union-language old-langs/prefixes) diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index b4847b645f..46bdc348f6 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -19,7 +19,19 @@ (provide (struct-out id/depth)) - (define (rewrite-side-conditions/check-errs all-nts what bind-names? orig-stx) + ;; the result is a four-tuple (as a list) syntax object + ;; - the first is an ordinary expression that evaluates + ;; to (void), but tells check syntax about binding information + ;; - the second is an expression that, when prefixed with a + ;; quasiquote, evaluates to a pattern that can be used with + ;; match-a-pattern (at runtime). + (define (rewrite-side-conditions/check-errs all-nts/lang-id what bind-names? orig-stx) + (define all-nts (if (identifier? all-nts/lang-id) + (language-id-nts all-nts/lang-id what) + all-nts/lang-id)) + (define id-stx-table (if (identifier? all-nts/lang-id) + (language-id-nt-identifiers all-nts/lang-id #f) + (hash))) (define (expected-exact name n stx) (raise-syntax-error what (format "~a expected to have ~a arguments" name @@ -39,6 +51,8 @@ (let recur ([chd e] [par (hash-ref sets e #f)]) (if (and par (not (eq? chd par))) (recur par (hash-ref sets par #f)) chd))) + (define void-stx #'(void)) + (define last-contexts (make-hasheq)) (define last-stx (make-hasheq)) ;; used for syntax error reporting (define assignments #hasheq()) @@ -67,6 +81,15 @@ [else (hash-set! last-contexts pat-sym under) assignments]))))) + + (define (record-syncheck-use stx nt) + (define the-use (build-disappeared-use id-stx-table nt stx)) + (when the-use + (define old (syntax-property void-stx 'disappeared-use)) + (set! void-stx + (syntax-property void-stx + 'disappeared-use + (if old (cons the-use old) the-use))))) (define ellipsis-number 0) @@ -188,6 +211,7 @@ term)] [(memq prefix-sym all-nts) (record-binder term under) + (record-syncheck-use term prefix-sym) (values (if mismatch? `(mismatch-name ,term (nt ,prefix-stx)) `(name ,term (nt ,prefix-stx))) @@ -212,6 +236,7 @@ orig-stx term)] [(memq (syntax-e term) all-nts) + (record-syncheck-use term (syntax-e term)) (cond [bind-names? (record-binder term under) @@ -357,8 +382,9 @@ (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)] - [term ellipsis-normalized/simplified]) - #'(term (name ...) (name/ellipses ...))))) + [term ellipsis-normalized/simplified] + [void-stx void-stx]) + #'(void-stx term (name ...) (name/ellipses ...))))) (define-struct id/depth (id depth mismatch?)) diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt index 2b942ce4cc..fac37cd35e 100644 --- a/collects/redex/private/term-fn.rkt +++ b/collects/redex/private/term-fn.rkt @@ -28,7 +28,10 @@ make-language-id language-id-nts - pattern-symbols) + language-id-nt-identifiers + pattern-symbols + + build-disappeared-use) (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) (make-struct-type 'term-fn #f 1 0)) @@ -57,7 +60,8 @@ (when (eq? (syntax-local-context) 'expression) (raise-syntax-error #f "not allowed in an expression context" stx))) -(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-values (language-id make-language-id language-id? language-id-get language-id-set) + (make-struct-type 'language-id #f 3 0 #f '() #f 0)) (define (language-id-nts stx id) (language-id-getter stx id 1)) (define (language-id-getter stx id n) @@ -68,6 +72,7 @@ (language-id? (set!-transformer-procedure val))) (raise-syntax-error id "expected an identifier defined by define-language" stx)) (language-id-get (set!-transformer-procedure val) n))) +(define (language-id-nt-identifiers stx id) (language-id-getter stx id 2)) (define pattern-symbols '(any number natural integer real string variable variable-not-otherwise-mentioned hole symbol)) @@ -84,3 +89,24 @@ (define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 8)) (define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9)) (define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10)) + + +(define (build-disappeared-use id-stx-table nt id-stx) + (cond + [id-stx-table + (define table-entry (hash-ref id-stx-table nt #f)) + (cond + [table-entry + (define the-srcloc (vector + (syntax-source id-stx) + (syntax-line id-stx) + (syntax-column id-stx) + (syntax-position id-stx) + ;; shorten the span so it covers only up to the underscore + (string-length (symbol->string nt)))) + (define the-id (datum->syntax table-entry nt the-srcloc id-stx)) + (syntax-property the-id 'syncheck-original #t)] + [else + #f])] + [else + #f])) diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt index b3de2f0199..5513ba9a68 100644 --- a/collects/redex/private/term.rkt +++ b/collects/redex/private/term.rkt @@ -15,7 +15,6 @@ (provide term term-let define-term hole in-hole term-let/error-name term-let-fn term-define-fn - term/nts (for-syntax term-rewrite term-temp->pat currently-expanding-term-fn @@ -39,30 +38,39 @@ (define-syntax (term stx) (syntax-case stx () [(term t . kw-args) - (with-syntax ([(lang-stx) (parse-kw-args (list lang-keyword) - (syntax kw-args) - stx - (syntax-e #'form))]) - (if (syntax->datum #'lang-stx) - (let ([lang-nts (let loop ([ls #'lang-stx]) - (define slv (syntax-local-value ls (λ () #'lang-stx))) - (if (term-id? slv) - (loop (term-id-prev-id slv)) - (language-id-nts ls 'term)))]) - #`(term/nts t #,lang-nts)) - #'(term/nts t #f)))])) + (let () + (define lang-stx (car + (parse-kw-args (list lang-keyword) + (syntax kw-args) + stx + (syntax-e #'form)))) + (cond + [lang-stx + (define-values (lang-nts lang-nt-ids) + (let loop ([ls lang-stx]) + (define slv (syntax-local-value ls (λ () lang-stx))) + (if (term-id? slv) + (loop (term-id-prev-id slv)) + (values (language-id-nts ls 'term) + (language-id-nt-identifiers ls 'term))))) + #`(term/nts t #,lang-nts #,lang-nt-ids)] + [else + #'(term/nts t #f #f)]))])) (define-syntax (term/nts stx) (syntax-case stx () - [(_ arg nts) - #'(#%expression (term/private arg nts))])) + [(_ arg nts nt-ids) + #'(#%expression (term/private arg nts nt-ids))])) + +(define-for-syntax current-id-stx-table (make-parameter #f)) (define-syntax (term/private stx) (syntax-case stx () - [(_ arg-stx nts-stx) - (with-disappeared-uses - (let-values ([(t a-mfs) (term-rewrite/private #'arg-stx #'nts-stx #f)]) - (term-temp->unexpanded-term t a-mfs)))])) + [(_ arg-stx nts-stx id-stx-table) + (parameterize ([current-id-stx-table (syntax-e #'id-stx-table)]) + (with-disappeared-uses + (let-values ([(t a-mfs) (term-rewrite/private #'arg-stx #'nts-stx #f)]) + (term-temp->unexpanded-term t a-mfs))))])) (define-for-syntax (term-rewrite t names) (let*-values ([(t-t a-mfs) (term-rewrite/private t #`#f names)] @@ -169,11 +177,25 @@ (term-fn? (syntax-local-value (syntax f) (λ () #f)))) (raise-syntax-error 'term "metafunction must be in an application" arg-stx stx)] [x - (and (identifier? (syntax x)) - (term-id? (syntax-local-value (syntax x) (λ () #f)))) - (let ([id (syntax-local-value/record (syntax x) (λ (x) #t))]) + (and (identifier? #'x) + (term-id? (syntax-local-value #'x (λ () #f)))) + (let ([id (syntax-local-value/record #'x (λ (x) #t))]) + (define stx-result (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) #'x)) + + (define raw-sym (syntax-e #'x)) + (define raw-str (symbol->string raw-sym)) + (define m (regexp-match #rx"^([^_]*)_" raw-str)) + (define prefix-sym (if m + (string->symbol (list-ref m 1)) + raw-sym)) (check-id (syntax->datum (term-id-id id)) stx) - (values (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) (syntax x)) + + (define new-id + (build-disappeared-use (current-id-stx-table) + prefix-sym + (syntax-local-introduce #'x))) + (when new-id (record-disappeared-uses (list new-id))) + (values stx-result (term-id-depth id)))] [x (defined-term-id? #'x) @@ -223,7 +245,7 @@ (i-loop (cdr xs))]) (values (cons fst rst) (max fst-max-depth rst-max-depth))))]))]) - (values (datum->syntax stx x-rewrite stx) max-depth))] + (values (datum->syntax stx x-rewrite stx stx) max-depth))] [_ (values stx 0)])) @@ -341,7 +363,7 @@ (define-syntax (term-define-fn stx) (syntax-case stx () [(_ id exp) - (with-syntax ([id2 (datum->syntax #'here (syntax-e #'id))]) + (with-syntax ([id2 (datum->syntax #'here (syntax-e #'id) #'id #'id)]) (syntax (begin (define id2 exp) @@ -363,7 +385,7 @@ [x (and (identifier? #'x) (not (free-identifier=? (quote-syntax ...) #'x))) - (let ([new-name (datum->syntax #'here (syntax-e #'x))]) + (let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)]) (values (list #'x) (list new-name) (list depth) diff --git a/collects/redex/tests/rewrite-side-condition-test.rkt b/collects/redex/tests/rewrite-side-condition-test.rkt index 44722f6c13..94389b54eb 100644 --- a/collects/redex/tests/rewrite-side-condition-test.rkt +++ b/collects/redex/tests/rewrite-side-condition-test.rkt @@ -7,7 +7,7 @@ (define-syntax (rsc stx) (syntax-case stx () [(_ pat (nts ...) bind-names?) - (with-syntax ([(pat (vars ...) (vars/ellipses ...)) + (with-syntax ([(ignore pat (vars ...) (vars/ellipses ...)) (rewrite-side-conditions/check-errs (syntax->datum #'(nts ...)) 'rsc diff --git a/collects/redex/tests/unify-tests.rkt b/collects/redex/tests/unify-tests.rkt index 27e335aff0..6b75815802 100644 --- a/collects/redex/tests/unify-tests.rkt +++ b/collects/redex/tests/unify-tests.rkt @@ -728,10 +728,10 @@ (λ (stx) (syntax-case stx () [(f-name lang t-1 t-2 env) - (with-syntax ([(pat-1 (names-1 ...) (names/ellipses-1 ...)) + (with-syntax ([(ignore-1 pat-1 (names-1 ...) (names/ellipses-1 ...)) (rewrite-side-conditions/check-errs (language-id-nts #'lang 'f-name) 'f-name stx #'t-1)] - [(pat-2 (names-2 ...) (names/ellipses-2 ...)) + [(ignore-2 pat-2 (names-2 ...) (names/ellipses-2 ...)) (rewrite-side-conditions/check-errs (language-id-nts #'lang 'f-name) 'f-name stx #'t-2)]) #'(unify/format 'pat-1 'pat-2 env lang))])))