From e788c6f49e979228701ce5b67cd18d971f354711 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Sun, 20 Nov 2011 22:50:07 -0600
Subject: [PATCH] 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)

---
 .../redex/private/reduction-semantics.rkt     | 42 ++++++++++++-------
 collects/redex/tests/tl-test.rkt              | 12 +++---
 2 files changed, 35 insertions(+), 19 deletions(-)

diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index fcafa37d73..d384888941 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/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)
-                   'flatten #`(list (term #,#'tmpl)) '() '()))]
+       #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
+                             '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))
-                 (define outputs
-                   (if mtchs
-                       (for/fold ([outputs '()]) ([m mtchs])
-                         (define os
-                           (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
-                                     #,body))
-                         (if os (append os outputs) outputs))
-                       '()))
-                 (for ([output outputs])
-                   (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode))
-                 outputs))))]))
+                 (combine-judgment-rhses
+                  compiled-lhs
+                  input
+                  (λ (m)
+                    (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
+                              #,body))
+                  (λ (output)
+                    (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))]))
   (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) ...)
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index c4e9fb99b8..236f498e83 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/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)]))
-                  (term ([n_1 (s z)] [n_2 z]))))
+            (list (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 ...))
-                            (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)))))