added support for where & side-condition & judgment-holds to define-relation

closes PR 12382

collects/redex/private/reduction-semantics.rkt

@@ -1424,6 +1424,33 @@
                     defs))
                  (syntax defs))))))]))
 
+(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx)
+  (for/list ([rhss (in-list (syntax->list raw-rhsss))])
+    (define rhses '())
+    (define sc/wheres '())
+    (for ([rhs (in-list (syntax->list rhss))])
+      (define (found-one) 
+        (set! sc/wheres (cons rhs sc/wheres)))
+      (syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds)
+        [(side-condition . stuff) (found-one)]
+        [(side-condition/hidden . stuff) (found-one)]
+        [(where . stuff) (found-one)]
+        [(where/hidden . stuff) (found-one)]
+        [(judgment-holds . stuff) (found-one)]
+        [_ 
+         (cond
+           [(null? sc/wheres)
+            (set! rhses (cons rhs rhses))]
+           [else
+            (raise-syntax-error 'define-relation
+                                (format "found a '~a' clause not at the end; followed by a normal, right-hand side clause"
+                                        (syntax-e (car (syntax-e (car sc/wheres)))))
+                                (last sc/wheres)
+                                #f
+                                (list  rhs))])]))
+    (list (reverse rhses)
+          (reverse sc/wheres))))
+
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
     [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats relation? syn-error-name)
@@ -1438,7 +1465,10 @@
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                      [(lhs-for-lw ...) (lhs-lws pats)])
          (with-syntax ([((rhs stuff ...) ...) (if relation?
-                                                  #'(((AND raw-rhses ...)) ...)
+                                                  (with-syntax ([(((rhses ...) (where/sc ...)) ...) 
+                                                                 (relation-split-out-rhs #'((raw-rhses ...) ...)
+                                                                                         #'orig-stx)])
+                                                    #'(((AND rhses ...) where/sc ...) ...))
                                                   #'((raw-rhses ...) ...))]
                        [(lhs ...) #'((lhs-clauses ...) ...)])
            (parse-extras #'((stuff ...) ...))
@@ -2157,7 +2187,9 @@
                                   [(not mtchs) (continue)]
                                   [relation? 
                                    (let ([ans
-                                          (ormap (λ (mtch) (ormap values (rhs traced-metafunc (mtch-bindings mtch))))
+                                          (ormap (λ (mtch) 
+                                                   (define rhs-ans (rhs traced-metafunc (mtch-bindings mtch)))
+                                                   (and rhs-ans (ormap values rhs-ans)))
                                                  mtchs)])
                                      (unless (ormap (λ (codom-compiled-pattern) (match-pattern codom-compiled-pattern ans))
                                                     codom-compiled-patterns)

collects/redex/private/rewrite-side-conditions.rkt

@@ -44,7 +44,7 @@
     (extract-names all-nts what bind-names? orig-stx) 
     
     (let loop ([term orig-stx])
-      (syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole side-condition cross unquote)
+      (syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole cross unquote)
         [(side-condition pre-pat (and))
          ;; rewriting metafunctions (and possibly other things) that have no where, etc clauses
          ;; end up with side-conditions that are empty 'and' expressions, so we just toss them here.

collects/redex/redex.scrbl

@@ -701,14 +701,14 @@ otherwise.
                                   shortcuts)
               ([domain (code:line) (code:line #:domain @#,ttpattern)]
                [base-arrow (code:line) (code:line #:arrow base-arrow-name)]
-               [reduction-case (arrow-name @#,ttpattern @#,tttterm extras ...)]
+               [reduction-case (arrow-name @#,ttpattern @#,tttterm red-extras ...)]
-               [extras rule-name
+               [red-extras rule-name
-                       (fresh fresh-clause ...)
+                           (fresh fresh-clause ...)
-                       (side-condition racket-expression)
+                           (side-condition racket-expression)
-                       (where @#,ttpattern @#,tttterm)
+                           (where @#,ttpattern @#,tttterm)
-                       (judgment-holds (judgment-form-id pat/term ...))
+                           (judgment-holds (judgment-form-id pat/term ...))
-                       (side-condition/hidden racket-expression)
+                           (side-condition/hidden racket-expression)
-                       (where/hidden @#,ttpattern @#,tttterm)]
+                           (where/hidden @#,ttpattern @#,tttterm)]
                [shortcuts (code:line)
                           (code:line with shortcut ...)]
                [shortcut [(old-arrow-name @#,ttpattern @#,tttterm)
@@ -974,7 +974,7 @@ reduce it further).
                           judgment-holds)
              (define-metafunction language
                metafunction-contract
-               [(name @#,ttpattern ...) @#,tttterm extras ...] 
+               [(name @#,ttpattern ...) @#,tttterm metafunction-extras ...] 
                ...)
              ([metafunction-contract (code:line) 
                                      (code:line id : @#,ttpattern ... -> range)]
@@ -982,12 +982,12 @@ reduce it further).
                      (code:line @#,ttpattern or range)
                      (code:line @#,ttpattern ∨ range)
                      (code:line @#,ttpattern ∪ range)]
-              [extras (side-condition racket-expression)
+              [metafunction-extras (side-condition racket-expression)
-                      (side-condition/hidden racket-expression)
+                                   (side-condition/hidden racket-expression)
-                      (where pat @#,tttterm)
+                                   (where pat @#,tttterm)
-                      (where/hidden pat @#,tttterm)
+                                   (where/hidden pat @#,tttterm)
-                      (judgment-holds 
+                                   (judgment-holds 
-                       (judgment-form-id pat/term ...))])]{
+                                    (judgment-form-id pat/term ...))])]{
 
 The @racket[define-metafunction] form builds a function on
 sexpressions according to the pattern and right-hand-side
@@ -1061,7 +1061,7 @@ match.
 
 @defform[(define-metafunction/extension f language 
            metafunction-contract
-           [(g @#,ttpattern ...) @#,tttterm extras ...] 
+           [(g @#,ttpattern ...) @#,tttterm metafunction-extras ...] 
            ...)]{
 
 Defines a metafunction @racket[g] as an extension of an existing
@@ -1271,7 +1271,9 @@ is an error elsewhere.
 @defform/subs[#:literals (⊂ ⊆ × x)
               (define-relation language
                 relation-contract
-                [(name @#,ttpattern ...) @#,tttterm ...] ...)
+                [(name @#,ttpattern ...) 
+                 @#,tttterm ...
+                 metafunction-extras ...] ...)
               ([relation-contract (code:line)
                                   (code:line form-id ⊂ @#,ttpattern x ... x @#,ttpattern)
                                   (code:line form-id ⊆ @#,ttpattern × ... × @#,ttpattern)])]{

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

@@ -13,3 +13,14 @@
 (#rx"expected a pattern"
  ([cross ×])
  (define-relation syn-err-lang foo ⊆ c cross))
+
+(#rx"found a 'where' clause not at the end"
+ ([first-where (where any_c any_a)]
+  [first-post-where (R () ())])
+ (define-relation syn-err-lang
+   [(R () ())]
+   [(R (any_a) (any_b)) 
+    (R anc_c any_d) 
+    first-where
+    (where any_d any_b)
+    first-post-where]))

collects/redex/tests/test-util.rkt

@@ -83,7 +83,8 @@
                                (syntax-case stx ()
                                  [(_ loc-name ... non-loc-name ...)
                                   #'body]))])
-                 (subst loc-piece ... non-loc-piece ...)))]))
+                 (subst loc-piece ... non-loc-piece ...)
+                 (void)))]))
 
 (define (source-location stx)
   (list (syntax-source stx) 

collects/redex/tests/tl-test.rkt

@@ -1138,6 +1138,49 @@
     (test (term (subtype (int num → int) (int int → int))) #t)
     (test (term (subtype (int int → int) (int int → num))) #t))
   
+  (let ()
+    (define-relation empty-language
+      [(R () ())]
+      [(R (any_a) (any_b)) 
+       (R any_c any_d) 
+       (where any_c any_a)
+       (where any_d any_b)])
+    
+    (test (term (R () ())) #t)
+    (test (term (R (()) (()))) #t)
+    (test (term (R (()) ())) #f))
+  
+  (let ()
+    (define-relation empty-language
+      [(R () ())]
+      [(R (any_a) (any_b)) 
+       (R any_c any_d) 
+       (where/hidden any_c any_a)
+       (where/hidden any_d any_b)])
+    
+    (test (term (R () ())) #t)
+    (test (term (R (()) (()))) #t)
+    (test (term (R (()) ())) #f))
+  
+  (let ()
+    (define-relation empty-language
+      [(R any_a any_b)
+       (side-condition (equal? (term any_a)
+                               (term any_b)))])
+    
+    (test (term (R (xx) (xx))) #t)
+    (test (term (R (()) ())) #f))
+  
+  (let ()
+    (define-relation empty-language
+      [(R any_a any_b)
+       (side-condition/hidden
+        (equal? (term any_a)
+                (term any_b)))])
+    
+    (test (term (R (xx) (xx))) #t)
+    (test (term (R (()) ())) #f))
+
   
   (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")