From 145828527f2665bac77c3bc97de618759e6060e3 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 31 Aug 2011 11:09:38 -0500 Subject: [PATCH] Fixes handling of pattern variables that look like metafunctions --- .../redex/private/reduction-semantics.rkt | 11 +++++---- .../redex/private/rewrite-side-conditions.rkt | 3 +-- .../judgment-form-definition.rktd | 24 +++++++++++++++++++ collects/redex/tests/tl-test.rkt | 13 ++++++++++ 4 files changed, 45 insertions(+), 6 deletions(-) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index d82651e81e..f59b444e8f 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -1895,15 +1895,18 @@ (loop (cdr rest-modes) rest-terms rest-ctcs (+ 1 pos))))))) (define-for-syntax (mode-check mode clauses nts syn-err-name) - (define ((check-template named-vars) temp bound) + (define ((check-template bound-anywhere) temp bound) (let check ([t temp]) (syntax-case t (unquote) [(unquote . _) (raise-syntax-error syn-err-name "unquote unsupported" t)] [x (identifier? #'x) - (when (and (or (id-binds? nts #t #'x) (free-id-table-ref named-vars #'x #f)) - (not (free-id-table-ref bound #'x #f))) + (unless (cond [(free-id-table-ref bound-anywhere #'x #f) + (free-id-table-ref bound #'x #f)] + [(id-binds? nts #t #'x) + (term-fn? (syntax-local-value #'x (λ () #f)))] + [else #t]) (raise-syntax-error syn-err-name "unbound pattern variable" #'x))] [(u ...) (for-each check (syntax->list #'(u ...)))] @@ -1956,7 +1959,7 @@ (for ([clause clauses]) (define do-tmpl (check-template - (fold-clause (bind 'name-only) void (make-immutable-free-id-table) clause))) + (fold-clause (bind 'rhs-only) void (make-immutable-free-id-table) clause))) (fold-clause (bind 'rhs-only) do-tmpl (make-immutable-free-id-table) clause))) ;; Defined as a macro instead of an ordinary phase 1 function so that the diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index 577402c8a5..57d0413ea6 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -161,8 +161,7 @@ (and (identifier? (syntax x)) ((case mode [(rhs-only) binds-in-right-hand-side?] - [(binds-anywhere) binds?] - [(name-only) (λ (_1 _2 _3) #f)]) + [(binds-anywhere) binds?]) all-nts bind-names? (syntax x))) (cons (make-id/depth (syntax x) depth) names)] [else names]))] diff --git a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd index 1cb8d0d51a..284564f050 100644 --- a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd +++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd @@ -182,4 +182,28 @@ #:mode (name I) [(name binder) premise ellipsis]) + (void))) + +(#rx"unbound pattern variable" + ([x f_7]) + (let () + (define-language L + (f any)) + (define-judgment-form L + #:mode (J1 O) + [(J1 x)]) + (void))) + +(#rx"unbound pattern variable" + ([use f_2]) ([outer-def f_2] [inner-def f_2]) + (let () + (define-language L + (f any)) + (define-metafunction L + [(outer-def) ()]) + (define-judgment-form L + #:mode (K I I O) + [(K a any_1 x) + (K b (use) (name inner-def any))] + [(K b any K-b-out)]) (void))) \ No newline at end of file diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 9b31935a95..6a9ab71b79 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -1822,6 +1822,19 @@ (judgment-holds (R a any)))) 'a) '(a b))) + + ; a call to a metafunction that looks like a pattern variable + (let () + (define result 'result) + (define-language L + (f any)) + (define-judgment-form L + #:mode (J O) + [(J (f_2))]) + (define-metafunction L + [(f_2) ,result]) + (test (judgment-holds (J any) any) + (list result))) ; ;