Modified test-judgment-holds to report failing sub-derivations

When called on a modeless judgment, if the test fails, test-judgment-holds will
isolate all failing sub-derivations and report them as part of the error message.

Author: wilbowma

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

@@ -3072,7 +3072,7 @@
                            "expected a modeless judgment-form"
                            #'jf))
      #`(let ([derivation e])
-         (test-modeless-jf/proc 'jf derivation (judgment-holds jf derivation) #,(get-srcloc stx)))]
+         (test-modeless-jf/proc '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
@@ -3141,25 +3141,42 @@
         ;; this case should always result in a syntax error
         #`(judgment-holds #,orig-jf-stx)])]))
 
-(define (test-modeless-jf/proc jf derivation val srcinfo)
+(define (derivation-pretty-printer pad)
+  (λ (new-line-number op old-len col)
+    (cond
+      [(number? new-line-number)
+       (unless (= new-line-number 0) (newline op))
+       (display pad op)
+       2]
+      [else
+       (newline op)
+       0])))
+
+(define (print-failing-subderivations f d)
+  (define (print-derivation-error d)
+    (parameterize ([pretty-print-print-line (derivation-pretty-printer "    ")])
+      (pretty-print d (current-error-port))))
+  (let loop ([d d])
+    (let ([ls (derivation-subs d)])
+      (for ([d ls])
+        (unless (loop d)
+          (print-derivation-error d)))
+      (unless (f d)
+        (print-derivation-error d)))))
+
+(define (test-modeless-jf/proc jf jf-pred derivation val srcinfo)
   (cond
     [val
      (inc-successes)]
     [else
      (inc-failures)
      (print-failed srcinfo)
      (eprintf "  derivation does not satisfy ~a\n" jf)
-     (parameterize ([pretty-print-print-line
-                     (λ (new-line-number op old-len col)
-                       (cond
-                         [(number? new-line-number)
-                          (unless (= new-line-number 0) (newline op))
-                          (display "  " op)
-                          2]
-                         [else
-                          (newline op)
-                          0]))])
-       (pretty-print derivation (current-error-port)))]))
+     (parameterize ([pretty-print-print-line (derivation-pretty-printer "  ")])
+       (pretty-print derivation (current-error-port)))
+     (when (not (null? (derivation-subs derivation)))
+       (eprintf"  because the following sub-derivations fail:\n")
+       (print-failing-subderivations jf-pred derivation))]))
 
 (define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?)
   (define results (thunk))

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

@@ -185,6 +185,47 @@
   (test (capture-output (test-results))
         "1 test failed (out of 2 total).\n"))
 
+(let ()
+  (define-judgment-form empty-language
+    [----------- "Base"
+     (J natural 1)]
+
+    [(J any_1 any_3)
+     -------------- "Pair"
+     (J (any_1 any_2) any_3)])
+
+  (test
+   (capture-output
+    (test-judgment-holds J (derivation `(J (x 0) 0) "Pair"
+                                       (list
+                                        (derivation `(J x 0) "Base" (list))))))
+   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J x 0) \"Base\" '())\n    (derivation '(J (x 0) 0) \"Pair\" (list (derivation '(J x 0) \"Base\" '())))\n")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J (derivation `(J (1 x) 0) "Pair"
+                                       (list
+                                        (derivation `(J 1 0) "Base" (list))))))
+   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J 1 0) \"Base\" '())\n    (derivation '(J (1 x) 0) \"Pair\" (list (derivation '(J 1 0) \"Base\" '())))\n")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J (derivation `(J x 0) "Base" (list))))
+   (regexp
+    (string-append
+     (regexp-quote "derivation does not satisfy J\n  (derivation '(J x 0) \"Base\" '())\n")
+     "$")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J (derivation `(J (1 x) 1) "Pair"
+                                       (list
+                                        (derivation `(J 1 1) "Base" (list))))))
+   "")
+
+  (test (capture-output (test-results))
+        "3 tests failed (out of 4 total).\n"))
+
 (let ()
   (define-judgment-form empty-language
     #:mode (broken-swap I I O O)