Adds support for `judgment-holds' clauses in metafunctions

collects/redex/private/reduction-semantics.rkt

@@ -328,7 +328,7 @@
               [env (make-immutable-hash
                     (map (λ (x e) (cons (syntax-e x) e))
                          names w/ellipses))])
-     (syntax-case stx (fresh)
+     (syntax-case stx (fresh judgment-holds)
        [() body]
        [((-where x e) y ...)
         (where-keyword? #'-where)
@@ -390,6 +390,8 @@
                         (verify-names-ok '#,orig-name the-names len-counter)
                         (variables-not-in #,to-not-be-in the-names))])
                     #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
+       [((judgment-holds j) . after)
+        (loop (cons #'j #'after) to-not-be-in env)]
        [((form-name . pats) . after)
         (judgment-form-id? #'form-name)
         (let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
@@ -1763,7 +1765,7 @@
    (λ (stuffs)
      (for-each
       (λ (stuff)
-        (syntax-case stuff (where side-condition where/hidden side-condition/hidden)
+        (syntax-case stuff (where side-condition where/hidden side-condition/hidden judgment-holds)
           [(side-condition tl-side-conds ...) 
            (void)]
           [(side-condition/hidden tl-side-conds ...) 
@@ -1780,6 +1782,11 @@
            (raise-syntax-error 'define-metafunction 
                                "malformed where/hidden clause"
                                stuff)]
+          [(judgment-holds (form-name . _))
+           (unless (judgment-form-id? #'form-name)
+             (raise-syntax-error 'define-metafunction
+                                 "expected the name of a judgment-form"
+                                 #'form-name))]
           [_
            (raise-syntax-error 'define-metafunction 
                                "expected a side-condition or where clause"
@@ -1876,16 +1883,6 @@
         (for/fold ([outputs '()]) ([rule (list clause-proc ...)])
                   (append (rule input) outputs)))))
 
-(define-for-syntax (in-order-non-hidden extras)
-  (reverse 
-   (filter (λ (extra)
-             (syntax-case extra (where/hidden
-                               side-condition/hidden)
-               [(where/hidden pat exp) #f]
-               [(side-condition/hidden x) #f]
-               [_ #t])) 
-           (syntax->list extras))))
-
 (define-for-syntax (do-compile-judgment-form-lws clauses)
   (syntax-case clauses ()
     [(((_ . conc-body) . prems) ...)
@@ -2000,6 +1997,9 @@
                   (map
                    (λ (lst)
                      (syntax-case lst (unquote side-condition where)
+                       [(form-name . _)
+                        (judgment-form-id? #'form-name)
+                        #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
                        [(form-name . _)
                         (judgment-form-id? #'form-name)
                         #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
@@ -2054,6 +2054,17 @@
                      rhs/lw)
                ...))]))
 
+(define-for-syntax (in-order-non-hidden extras)
+  (for/fold ([visible empty]) ([extra (syntax->list extras)])
+            (syntax-case extra (where/hidden
+                                side-condition/hidden
+                                judgment-holds)
+              [(where/hidden pat exp) visible]
+              [(side-condition/hidden x) visible]
+              [(judgment-holds judgment)
+               (cons #'judgment visible)]
+              [_ (cons extra visible)])))
+
 (define-syntax (compile-judgment-form-proc stx)
   (syntax-case stx ()
     [(_ judgment-form-name lang mode clauses ctcs full-def syn-err-name)

collects/redex/redex.scrbl

@@ -706,7 +706,7 @@ otherwise.
                        (fresh fresh-clause ...)
                        (side-condition racket-expression)
                        (where @#,ttpattern @#,tttterm)
-                       (judgment-holds (judgment-form-id pat/term))
+                       (judgment-holds (judgment-form-id pat/term ...))
                        (side-condition/hidden racket-expression)
                        (where/hidden @#,ttpattern @#,tttterm)]
                [shortcuts (code:line)
@@ -960,7 +960,10 @@ it is traversing through the reduction graph.
 
 @declare-exporting[redex/reduction-semantics redex]
 
-@defform/subs[#:literals (: -> where side-condition side-condition/hidden where/hidden)
+@defform/subs[#:literals (: -> 
+                          where side-condition 
+                          side-condition/hidden where/hidden 
+                          judgment-holds)
              (define-metafunction language
                metafunction-contract
                [(name @#,ttpattern ...) @#,tttterm extras ...] 
@@ -974,7 +977,9 @@ it is traversing through the reduction graph.
               [extras (side-condition racket-expression)
                       (side-condition/hidden racket-expression)
                       (where pat @#,tttterm)
-                      (where/hidden pat @#,tttterm)])]{
+                      (where/hidden pat @#,tttterm)
+                      (judgment-holds 
+                       (judgment-form-id pat/term ...))])]{
 
 The @racket[define-metafunction] form builds a function on
 sexpressions according to the pattern and right-hand-side

collects/redex/tests/bitmap-test.rkt

@@ -98,6 +98,18 @@
 (test (render-metafunction S)
       "metafunction.png")
 
+(let ()
+  (define-metafunction lang
+    [(f (e_1 e_2))
+     (e_3 e_4)
+     (judgment-holds (J e_1 e_3))
+     (judgment-holds (J e_2 e_4))])
+  (define-judgment-form lang
+    #:mode (J I O)
+    [(J e e)])
+  (test (render-metafunction f)
+        "metafunction-judgment-holds.png"))
+
 (define-metafunction lang
   [(T x y)
    1

collects/redex/tests/tl-test.rkt

@@ -977,6 +977,29 @@
                  x)
           '(2 1)))
   
+  (let ()
+    (define-language L
+      (n z (s n)))
+    
+    (define-metafunction L
+      [(f n)
+       n_1
+       (judgment-holds (p n n_1))])
+    
+    (define-judgment-form L
+      #:mode (p I O)
+      #:contract (p n n)
+      [(p z z)]
+      [(p (s n) n)]
+      [(p (s n) z)])
+    
+    (test (term (f (s z)))
+          (term z))
+    (test (with-handlers ([exn:fail:redex? exn-message])
+            (term (f (s (s z))))
+            "")
+          #rx"different ways and returned different results"))
+  
   (parameterize ([current-namespace (make-base-namespace)])
     (eval '(require redex/reduction-semantics))
     (exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd"))