From 755dc28e55b72e0819bbf1a846f6413eba5cfe8c Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Thu, 17 Nov 2011 16:59:36 -0600
Subject: [PATCH] Fixes define-relation's handling of ellipses across clauses

closes PR 12378
---
 .../redex/private/reduction-semantics.rkt     | 11 +++++++++-
 collects/redex/tests/tl-test.rkt              | 22 +++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index e6afc9a0f5..3bc6ec9484 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -1438,7 +1438,7 @@
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                      [(lhs-for-lw ...) (lhs-lws pats)])
          (with-syntax ([((rhs stuff ...) ...) (if relation?
-                                                  #'((,(and (term raw-rhses) ...)) ...)
+                                                  #'(((AND raw-rhses ...)) ...)
                                                   #'((raw-rhses ...) ...))]
                        [(lhs ...) #'((lhs-clauses ...) ...)])
            (parse-extras #'((stuff ...) ...))
@@ -2920,3 +2920,12 @@
          covered-cases
          (rename-out [fresh-coverage make-coverage])
          coverage?)
+
+;; the AND metafunction is defined here to be used
+;; in define-relation so that ellipses work properly
+;; across clauses in relations
+(define-language L)
+(define-metafunction L
+  AND : any ... -> any
+  [(AND any ...) 
+   ,(andmap values (term (any ...)))])
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index c7475b7802..335347b056 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -1117,6 +1117,28 @@
             'failed)
           'passed))
   
+  (let ()
+    (define-language types
+      ((τ σ) int
+             num
+             (τ ... → τ)))
+    
+    (define-relation types
+      subtype ⊆ τ × τ
+      [(subtype int num)]
+      [(subtype (τ_1 ..._1 → τ_2) (σ_1 ..._1 → σ_2))
+       (subtype σ_1 τ_1) ...
+       (subtype τ_2 σ_2)]
+      [(subtype τ τ)])
+    
+    (test (term (subtype int int)) #t)
+    (test (term (subtype int num)) #t)
+    (test (term (subtype (int int int → int) (int int → int))) #f)
+    (test (term (subtype (int int → int) (int num → int))) #f)
+    (test (term (subtype (int num → int) (int int → int))) #t)
+    (test (term (subtype (int int → int) (int int → num))) #t))
+
+  
   (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")
   
 ;                    ;;                         ;                                        ;;                    ;