Fixes arity checks outside define-judgment-form

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 . _) . _)

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

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))))
+
+(#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)))

collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd

@@ -124,3 +124,15 @@
 (#rx"expected an identifier"
  ([not-id 7])
  (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)))))