adjust define-judgment-form so that it

a) avoids creating big intermediate lists of the same things over and over
   (this closes PR 12380)
b) generates less code (by generating calls to local functions)
c) normalizes its output (sorts by the printed representation)

collects/redex/private/reduction-semantics.rkt

@@ -1874,8 +1874,10 @@
             [nts (definition-nts lang stx syn-err-name)]
             [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
        (check-judgment-arity judgment)
-       (bind-withs syn-err-name '() lang nts (list judgment)
+       #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
-                   'flatten #`(list (term #,#'tmpl)) '() '()))]
+                             'flatten #`(list (term #,#'tmpl)) '() '())
+               string<=?
+               #:key (λ (x) (format "~s" x))))]
     [(_ (not-form-name . _) . _)
      (not (judgment-form-id? #'form-name))
      (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
@@ -1909,18 +1911,14 @@
                    [compiled-output-ctcs #,(contracts-compilation output-contracts)])
                (λ (input)
                  (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode)
-                 (define mtchs (match-pattern compiled-lhs input))
+                 (combine-judgment-rhses
-                 (define outputs
+                  compiled-lhs
-                   (if mtchs
+                  input
-                       (for/fold ([outputs '()]) ([m mtchs])
+                  (λ (m)
-                         (define os
                     (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
                               #,body))
-                         (if os (append os outputs) outputs))
+                  (λ (output)
-                       '()))
+                    (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))]))
-                 (for ([output outputs])
-                   (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode))
-                 outputs))))]))
   (with-syntax ([(clause-proc ...) (map compile-clause clauses)]
                 [(clause-proc-ids ...) (generate-temporaries clauses)])
     (with-syntax ([(backwards-ids ...) (reverse (syntax->list #'(clause-proc-ids ...)))])
@@ -1928,6 +1926,22 @@
           (λ (input)
             (append (backwards-ids input) ...))))))
 
+(define (combine-judgment-rhses compiled-lhs input rhs check-output)
+  (define mtchs (match-pattern compiled-lhs input))
+  (cond
+    [mtchs
+     (define output-table (make-hash))
+     (for ([m (in-list mtchs)])
+       (define os (rhs m))
+       (when os
+         (for ([x (in-list os)])
+           (hash-set! output-table x #t))))
+     (define outputs (hash-map output-table (λ (k v) k)))
+     (for ([output (in-list outputs)])
+       (check-output output))
+     outputs]
+    [else '()]))
+
 (define-for-syntax (do-compile-judgment-form-lws clauses)
   (syntax-case clauses ()
     [(((_ . conc-body) . prems) ...)

collects/redex/tests/tl-test.rkt

@@ -2018,8 +2018,8 @@
       (test (judgment-holds (sumo n_1 n_2 z) ([,'n_1 n_1] [,'n_2 n_2]))
             (list (term ([n_1 z] [n_2 z]))))
       (test (judgment-holds (sumo n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2]))
-            (list (term ([n_1 z] [n_2 (s z)]))
+            (list (term ([n_1 (s z)] [n_2 z]))
-                  (term ([n_1 (s z)] [n_2 z]))))
+                  (term ([n_1 z] [n_2 (s z)]))))
       
       (define-judgment-form nats
         #:mode (sumo-ls O O I)
@@ -2043,7 +2043,7 @@
         [(member n_i (n_0 ... n_i n_i+1 ...))])
       
       (test (judgment-holds (member n (z (s z) z (s (s z)))) n)
-            (list (term z) (term (s z)) (term z) (term (s (s z)))))
+            (list (term (s (s z))) (term (s z)) (term z)))
       
       (define-judgment-form nats
         #:mode (has-zero I)
@@ -2122,8 +2122,10 @@
         [(map-add-some-noz (n ...) (n_+ ...))
          (add-some-noz n n_+) ...])
       
-      (test (judgment-holds (map-add-some-noz (z (s z) (s (s z))) (n ...))
+      (test (sort (judgment-holds (map-add-some-noz (z (s z) (s (s z))) (n ...))
                                   (n ...))
+                  string<=?
+                  #:key (λ (x) (format "~s" x)))
             (list (term (z (s (s z)) (s (s (s z)))))
                   (term (z (s (s z)) (s (s z))))
                   (term (z (s z) (s (s (s z)))))