diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 88b1752716..fcc8c216a7 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -479,6 +479,19 @@ (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x)))) (extract-pattern-binds pat))) +(define-for-syntax (check-judgment-arity judgment) + (syntax-case judgment () + [(form-name pat ...) + (judgment-form-id? #'form-name) + (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))] + [actual (length (syntax->list #'(pat ...)))]) + (unless (= actual expected) + (raise-syntax-error + #f + (format "mode specifies a ~a-ary relation but use supplied ~a term~a" + expected actual (if (= actual 1) "" "s")) + judgment)))])) + (define-syntax-set (do-reduction-relation) (define (do-reduction-relation/proc stx) (syntax-case stx () @@ -1073,13 +1086,13 @@ [(computed-name . _) (raise-syntax-error orig-name "malformed computed-name clause" stx (car extras))] [(judgment-holds judgment) - (cons #'judgment (loop (cdr extras)))] + (begin + (check-judgment-arity #'judgment) + (cons #'judgment (loop (cdr extras))))] [_ (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))]) (values the-name computed-name-stx sides/withs/freshs))) - - ;; table-cons! hash-table sym any -> void ;; extends ht at key by `cons'ing hd onto whatever is alrady bound to key (or the empty list, if nothing is) (define (table-cons! ht key hd) @@ -1783,14 +1796,6 @@ (cons (cadr more) arg-pats))] [else (values (reverse arg-pats) more)])))]))) -(define-for-syntax (check-judgment-arity judgment) - (syntax-case judgment () - [(form-name pat ...) - (judgment-form-id? #'form-name) - (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))]) - (unless (= (length (syntax->list #'(pat ...))) expected) - (raise-syntax-error #f "arity mismatch" judgment)))])) - (define-syntax (judgment-holds stx) (syntax-case stx () [(j-h judgment) @@ -1801,7 +1806,7 @@ [lang (judgment-form-lang (syntax-local-value #'form-name))] [nts (definition-nts lang stx syn-err-name)] [judgment (syntax-case stx () [(_ judgment _) #'judgment])]) - (check-judgment-arity #'(form-name . pats)) + (check-judgment-arity judgment) (bind-withs syn-err-name '() lang nts (list judgment) 'flatten #`(list (term #,#'tmpl)) '() '()))] [(_ (not-form-name . _) . _) 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 ebbbdfeebc..6d604fc8d0 100644 --- a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd +++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd @@ -106,14 +106,14 @@ (where number_2 unbound) (where (name q number) number_1)]) (void))) -(#rx"arity" +(#rx"J: mode specifies a 1-ary relation but use supplied 0 terms" ([bad-conc (J)]) ([name J]) (let () (define-judgment-form syn-err-lang #:mode (name I) [bad-conc]) (void))) -(#rx"arity" +(#rx"J: mode specifies a 1-ary relation but use supplied 0 terms" ([bad-prem (J)]) ([name J]) (let () (define-judgment-form syn-err-lang @@ -121,6 +121,14 @@ [(name number) bad-prem]) (void))) +(#rx"J: mode specifies a 0-ary relation but use supplied 1 term" + ([bad-prem (J a)]) ([name J]) + (let () + (define-judgment-form syn-err-lang + #:mode (name) + [(name) + bad-prem]) + (void))) (#rx"unquote unsupported" ([unq ,(+ 1)]) (let () diff --git a/collects/redex/tests/syn-err-tests/judgment-holds.rktd b/collects/redex/tests/syn-err-tests/judgment-holds.rktd index 2907d2aff2..dc2775e2d6 100644 --- a/collects/redex/tests/syn-err-tests/judgment-holds.rktd +++ b/collects/redex/tests/syn-err-tests/judgment-holds.rktd @@ -1,3 +1,12 @@ (#rx"expected a judgment form name" ([not-judgment-form junk]) - (judgment-holds (not-judgment-form z (s z)))) \ No newline at end of file + (judgment-holds (not-judgment-form z (s z)))) + +(#rx"a?: mode specifies a 1-ary relation but use supplied 2 terms" + ([bad-judgment (a? a q)]) + ([name a?]) + (let () + (define-judgment-form syn-err-lang + #:mode (name I) + [(name a)]) + (judgment-holds bad-judgment))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd index 32bbd3c688..5793d437ea 100644 --- a/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd +++ b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd @@ -123,4 +123,16 @@ (redex-match syn-err-lang (variable-prefix not-id))) (#rx"expected an identifier" ([not-id 7]) - (redex-match syn-err-lang (cross not-id))) \ No newline at end of file + (redex-match syn-err-lang (cross not-id))) + +(#rx"a?: mode specifies a 1-ary relation but use supplied 2 terms" + ([bad-judgment (a? a q)]) + ([name a?]) + (let () + (define-judgment-form syn-err-lang + #:mode (name I) + [(name a)]) + (reduction-relation + syn-err-lang + (--> 1 1 + (judgment-holds bad-judgment))))) \ No newline at end of file