test-judgment-holds incorrectly blames sub-derivations from other judgments

[wilbowma]

See f10a062

When a test-judgment-holds test fails for a modeless judgment, the error message
will incorrectly blame any sub-derivation that is not from the same judgment as
the top-level judgment.

[wilbowma]

In my experiments, I was using this function as a predicate for whether a (sub)derivation is valid.

(define (check-modeless-derivation d)
  (eval `(judgment-holds ,(car (derivation-term d)) ,d)))

This worked fine, but I tried to get rid of eval and instead generated a predicate like the following from inside test-judgment-holds.

... #`(lambda (d) (judgment-holds #,jf-id d))

This change didn't work, since of course, jf-id refers to a single judgment, while check-modeless-derivation can refer to many judgments.

I tried using check-modeless-derivation in Redex, but the test suite fails with a bunch of namespace errors, so I'm back to avoiding eval. Unfortunately, I'm not sure how to implement check-modeless-derivation now...

As a temporary work-around, I could make print-failing-derivations ignore sub-derivations that it can't know how to check. This would provide sound but incomplete information.