Support reporting sub-derivation failures from any specified judgment

Author: wilbowma

redex-lib/redex/private/reduction-semantics.rkt

@@ -3060,7 +3060,8 @@
 
 (define-syntax (test-judgment-holds stx)
   (syntax-parse stx
-    [(_ jf e:expr)
+    [(_ jf e:expr (~optional (~seq #:mutuals (mjf:id ...))
+                             #:defaults ([(mjf 1) '()])))
      (unless (judgment-form-id? #'jf)
        (raise-syntax-error 'test-judgment-holds
                            "expected a modeless judgment-form"
@@ -3072,7 +3073,13 @@
                            "expected a modeless judgment-form"
                            #'jf))
      #`(let ([derivation e])
-         (test-modeless-jf/proc 'jf (lambda (x) (judgment-holds jf x)) derivation (judgment-holds jf derivation) #,(get-srcloc stx)))]
+         (test-modeless-jf/proc 'jf
+                                (make-hasheq
+                                 `((jf . ,(lambda (x) (judgment-holds jf x)))
+                                   #,@(for/list ([jf (attribute mjf)])
+                                        `(,jf . ,#`,(lambda (x) (judgment-holds #,jf x))))))
+                                derivation (judgment-holds jf derivation)
+                                #,(get-srcloc stx)))]
     [(_ (jf . rest))
      (unless (judgment-form-id? #'jf)
        (raise-syntax-error 'test-judgment-holds
@@ -3159,23 +3166,24 @@
 ;; Sub-derivations from other judgments get ignored.
 ;; TODO: Can we create a generic sub-derivation checker that does not,
 ;; statically, know the name of the judgment it is checking?
-(define (print-failing-subderivations jf f d)
+(define (print-failing-subderivations jf jf-pred-hash d)
   (define (print-derivation-error d)
     (parameterize ([pretty-print-print-line (derivation-pretty-printer "    ")])
       (pretty-print d (current-error-port))))
-  (define (checkable-derivation d)
-    (equal? jf (car (derivation-term d))))
+  (define (check-derivation d)
+    (define f (hash-ref jf-pred-hash (car (derivation-term d)) (lambda () #f)))
+    (if f
+        (f d)
+        #t))
   (let loop ([d d])
     (let ([ls (derivation-subs d)])
       (for ([d ls])
         (unless (loop d)
           (print-derivation-error d)))
-      (unless (if (checkable-derivation d)
-                  (f d)
-                  #t)
+      (unless (check-derivation d)
         (print-derivation-error d)))))
 
-(define (test-modeless-jf/proc jf jf-pred derivation val srcinfo)
+(define (test-modeless-jf/proc jf jf-preds derivation val srcinfo)
   (cond
     [val
      (inc-successes)]
@@ -3187,7 +3195,7 @@
        (pretty-print derivation (current-error-port)))
      (when (not (null? (derivation-subs derivation)))
        (eprintf"  because the following sub-derivations fail:\n")
-       (print-failing-subderivations jf jf-pred derivation))]))
+       (print-failing-subderivations jf jf-preds derivation))]))
 
 (define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?)
   (define results (thunk))

redex-test/redex/tests/tl-test.rkt

@@ -257,6 +257,25 @@
           (derivation '(J1 1 x) \"Base\" '())
           (derivation '(J2 1 1) \"Base\" '())))")))
 
+  (test
+   (capture-output
+    (test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair"
+                                        (list
+                                         (derivation `(J1 1 x) "Base"
+                                                     (list))
+                                         (derivation `(J2 1 1) "Base"
+                                                     (list))))
+                         #:mutuals (J1)))
+   (regexp
+    (regexp-quote "because the following sub-derivations fail:
+    (derivation '(J1 1 x) \"Base\" '())
+    (derivation
+       '(J2 (1 x) 1)
+       \"Pair\"
+       (list
+          (derivation '(J1 1 x) \"Base\" '())
+          (derivation '(J2 1 1) \"Base\" '())))")))
+
   (test
    (capture-output
     (test-judgment-holds J2 (derivation `(J2 (1 1) 2) "Pair"
@@ -286,7 +305,7 @@
    "")
 
   (test (capture-output (test-results))
-        "2 tests failed (out of 3 total).\n"))
+        "3 tests failed (out of 4 total).\n"))
 
 (let ()
   (define-judgment-form empty-language