Adds an alternative syntax for define-judgment-form rules

The conclusion may come last instead of first when a sequence of
dashes precedes it.

collects/redex/private/reduction-semantics.rkt

@@ -1539,6 +1539,16 @@
     (define-syntax-class contract-spec
       #:description "contract specification"
       (pattern (_:id _:expr ...)))
+    (define (horizontal-line? id)
+      (regexp-match? #rx"^-+$" (symbol->string (syntax-e id))))
+    (define-syntax-class horizontal-line
+      (pattern x:id #:when (horizontal-line? #'x)))
+    (define (parse-rules rules)
+      (for/list ([rule rules])
+        (syntax-parse rule
+          [(prem ... _:horizontal-line conc)
+           #'(conc prem ...)]
+          [_ rule])))
     (define-values (name/mode mode name/contract contract rules)
       (syntax-parse body #:context full-stx
         [((~or (~seq #:mode ~! mode:mode-spec)
@@ -1558,7 +1568,7 @@
                           (raise-syntax-error 
                            syn-err-name "expected at most one contract specification"
                            #f #f (syntax->list #'dups))])])
-           (values name/mode mode name/ctc ctc #'rules))]))
+           (values name/mode mode name/ctc ctc (parse-rules #'rules)))]))
     (check-clauses full-stx syn-err-name rules #t)
     (check-arity-consistency mode contract full-stx)
     (define-values (form-name dup-names)

collects/redex/redex.scrbl

@@ -1069,7 +1069,7 @@ legtimate inputs according to @racket[metafunction-name]'s contract,
 and @racket[#f] otherwise.
 }
 
-@defform/subs[#:literals (I O where)
+@defform/subs[#:literals (I O where etc.)
              (define-judgment-form language
                option ...
                rule ...)
@@ -1079,12 +1079,22 @@ and @racket[#f] otherwise.
               [contract-spec (code:line #:contract (form-id @#,ttpattern ...))]
               [pos-use I
                        O]
-              [rule [conclusion premise ...]]
+              [rule [conclusion 
+                     premise 
+                     ...]
+                    [premise
+                     ...
+                     dashes
+                     conclusion]]
               [conclusion (form-id pat/term ...)]
               [premise (judgment-form-id pat/term ...)
                        (where @#,ttpattern @#,tttterm)]
               [pat/term @#,ttpattern
-                        @#,tttterm])]{
+                        @#,tttterm]
+              [dashes ---
+                      ----
+                      -----
+                      etc.])]{
 Defines @racket[form-id] as a relation on terms via a set of inference rules.
 Each rule must be such that its premises can be evaluated left-to-right
 without ``guessing'' values for any of their pattern variables. Redex checks this

collects/redex/tests/tl-test.rkt

@@ -1975,6 +1975,17 @@
       (test (judgment-holds (uses-add2 (s (s (s (s z)))) n) n)
             (list (term (s (s (s z))))))
       
+      (define-judgment-form nats
+        #:mode (hyphens I)
+        [(hyphens b)
+         -----------
+         (hyphens a)]
+        [(hyphens c)
+         -
+         (hyphens b)]
+        [(hyphens c)])
+      (test (judgment-holds (hyphens a)) #t)
+      
       (let-syntax ([test-trace 
                     (syntax-rules ()
                       [(_ expr trace-spec expected)