From dec519ac86264446acbc992c3724ea44e37a1c28 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 4 Oct 2019 19:16:10 -0700 Subject: [PATCH 1/6] Added tests that expose problem in test-judgment-holds 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. --- redex-test/redex/tests/tl-test.rkt | 63 ++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/redex-test/redex/tests/tl-test.rkt b/redex-test/redex/tests/tl-test.rkt index 8d6aef4e..c56072dc 100644 --- a/redex-test/redex/tests/tl-test.rkt +++ b/redex-test/redex/tests/tl-test.rkt @@ -226,6 +226,69 @@ (test (capture-output (test-results)) "3 tests failed (out of 4 total).\n")) +(let () + (define-judgment-form empty-language + [----------- "Base" + (J1 natural 1)]) + + (define-judgment-form empty-language + [----------- "Base" + (J2 natural 1)] + + [(J1 any_1 any_2) + (J2 any_1 any_3) + -------------- "Pair" + (J2 (any_1 any_2) any_3)]) + + (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)))))) + (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" + (list + (derivation `(J1 1 1) "Base" + (list)) + (derivation `(J2 1 2) "Base" + (list)))))) + (regexp + (regexp-quote "because the following sub-derivations fail: + (derivation '(J2 1 2) \"Base\" '()) + (derivation + '(J2 (1 1) 2) + \"Pair\" + (list + (derivation '(J1 1 1) \"Base\" '()) + (derivation '(J2 1 2) \"Base\" '())))"))) + + (test + (capture-output + (test-judgment-holds J2 (derivation `(J2 (2 1) 1) "Pair" + (list + (derivation `(J1 2 1) "Base" + (list)) + (derivation `(J2 2 1) "Base" + (list)))))) + "") + + (test (capture-output (test-results)) + "2 tests failed (out of 3 total).\n")) + (let () (define-judgment-form empty-language #:mode (broken-swap I I O O) From c3bfe1d60eac2d7dea9f1cbaf8c42a81eb3b58c4 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 4 Oct 2019 20:04:05 -0700 Subject: [PATCH 2/6] Only report proper sub-derivations from test-judgment-holds --- redex-lib/redex/private/reduction-semantics.rkt | 17 ++++++++++++++--- redex-test/redex/tests/tl-test.rkt | 1 - 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/redex-lib/redex/private/reduction-semantics.rkt b/redex-lib/redex/private/reduction-semantics.rkt index 5f1b888c..0671099e 100644 --- a/redex-lib/redex/private/reduction-semantics.rkt +++ b/redex-lib/redex/private/reduction-semantics.rkt @@ -3152,16 +3152,27 @@ (newline op) 0]))) -(define (print-failing-subderivations f d) +;; Takes a judgment-form name `jf`, a sub-derivation predicate for testing whether a +;; sub-derivation of `jf` is valid. +;; The derivation predicate will only be called on sub-derivations of the +;; judgment `jf`. +;; 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-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)))) (let loop ([d d]) (let ([ls (derivation-subs d)]) (for ([d ls]) (unless (loop d) (print-derivation-error d))) - (unless (f d) + (unless (if (checkable-derivation d) + (f d) + #t) (print-derivation-error d))))) (define (test-modeless-jf/proc jf jf-pred derivation val srcinfo) @@ -3176,7 +3187,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-pred derivation))])) + (print-failing-subderivations jf jf-pred derivation))])) (define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?) (define results (thunk)) diff --git a/redex-test/redex/tests/tl-test.rkt b/redex-test/redex/tests/tl-test.rkt index c56072dc..8da531aa 100644 --- a/redex-test/redex/tests/tl-test.rkt +++ b/redex-test/redex/tests/tl-test.rkt @@ -250,7 +250,6 @@ (list)))))) (regexp (regexp-quote "because the following sub-derivations fail: - (derivation '(J1 1 x) \"Base\" '()) (derivation '(J2 (1 x) 1) \"Pair\" From 2807a598de1a5217c7c10b25d2549421d74b9ad5 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 4 Oct 2019 23:58:54 -0700 Subject: [PATCH 3/6] Support reporting sub-derivation failures from any specified judgment --- .../redex/private/reduction-semantics.rkt | 28 ++++++++++++------- redex-test/redex/tests/tl-test.rkt | 21 +++++++++++++- 2 files changed, 38 insertions(+), 11 deletions(-) diff --git a/redex-lib/redex/private/reduction-semantics.rkt b/redex-lib/redex/private/reduction-semantics.rkt index 0671099e..c365abe7 100644 --- a/redex-lib/redex/private/reduction-semantics.rkt +++ b/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)) diff --git a/redex-test/redex/tests/tl-test.rkt b/redex-test/redex/tests/tl-test.rkt index 8da531aa..abe7cb2e 100644 --- a/redex-test/redex/tests/tl-test.rkt +++ b/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 From 905b8b74390004087fee90bf8dd32d527ed2f372 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Sat, 5 Oct 2019 00:10:20 -0700 Subject: [PATCH 4/6] Documentation for test-judgment-holds with sub-derivation reporting --- redex-doc/redex/scribblings/ref/testing.scrbl | 44 ++++++++++++++++++- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/redex-doc/redex/scribblings/ref/testing.scrbl b/redex-doc/redex/scribblings/ref/testing.scrbl index 41d57aad..c8cca86f 100644 --- a/redex-doc/redex/scribblings/ref/testing.scrbl +++ b/redex-doc/redex/scribblings/ref/testing.scrbl @@ -153,11 +153,51 @@ relation @racket[rel-expr] to a term specified by @racket[goal-expr] in (test-results)] -@defform*[((test-judgment-holds (judgment-form-or-relation pat/term ...)) - (test-judgment-holds modeless-judgment-form derivation-expr))]{ +@defform*/subs[((test-judgment-holds (judgment-form-or-relation pat/term ...) mutuals) + (test-judgment-holds modeless-judgment-form derivation-expr)) + ([mutuals (code:line) + (code:line #:mutuals (judgment-form-id ...))])]{ In the first form, tests to see if @racket[(judgment-form-or-relation pat/term ...)] holds. In the second form, tests to see if the result of @racket[derivation-expr] is a derivation and, if so, that it is derivable using @racket[modeless-judgment-form]. + + For modeless judgments, if the derivation is invalid, the test will report the + all the proper sub-derivations of @racket[modeless-judgment-form] that fail to hold. + If @racket[modeless-judgment-form] has other judgment premises, these + identifiers can be supplied in the optional #racket[#:mutuals] arguments, and + the form will report each invalid sub-derivations from all the specified judgment forms. + +@examples[ +#:eval redex-eval +(define-language L) +(define-judgment-form L + [----------- "Base" + (J1 natural 1)]) + +(define-judgment-form L + [----------- "Base" + (J2 natural 1)] + + [(J1 any_1 any_2) + (J2 any_1 any_3) + -------------- "Pair" + (J2 (any_1 any_2) any_3)]) + +(test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair" + (list + (derivation `(J1 1 x) "Base" + (list)) + (derivation `(J2 1 1) "Base" + (list))))) + +(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)) +] } @defform[(test-predicate p? e)]{ From 0dcbe789eb82cd40bdbfc07a2b8a5bb5c6da1a81 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 10 Oct 2019 15:26:37 -0700 Subject: [PATCH 5/6] Collect failing sub-derviations from call-modeless-judgment-form and friends --- redex-lib/redex/private/modeless-jf.rkt | 41 +++++++++++++++---------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/redex-lib/redex/private/modeless-jf.rkt b/redex-lib/redex/private/modeless-jf.rkt index 4a40a84e..e68d1b90 100644 --- a/redex-lib/redex/private/modeless-jf.rkt +++ b/redex-lib/redex/private/modeless-jf.rkt @@ -245,9 +245,13 @@ ;; hash[rulename -o> (listof modeless-jf-clause?)] ;; compiled-pattern ;; derivation -;; -> match or #f +;; boolean +;; fail: (list/c derivation?) -> any/c +;; -> match or any/c +;; a list of derivations indicates the list of sub-derivations that did not match. (define (call-modeless-judgment-form lang jf-name modeless-jf-clause-table contract-cp deriv - only-check-contracts?) + only-check-contracts? + [fail (λ _ #f)]) (match deriv [(derivation (cons deriv-jf-name jf-args) rule-name sub-derivations) (cond @@ -262,7 +266,7 @@ rules jf-args sub-derivations - (λ () #f))] + fail)] [else (define known-rules (sort (hash-keys modeless-jf-clause-table) string Date: Thu, 10 Oct 2019 17:31:21 -0700 Subject: [PATCH 6/6] Balls of hacks that are somewhat closer to doing the right thing --- redex-lib/redex/private/modeless-jf.rkt | 29 +++++----- .../redex/private/reduction-semantics.rkt | 57 ++++++++----------- redex-test/redex/tests/tl-test.rkt | 30 ++-------- 3 files changed, 44 insertions(+), 72 deletions(-) diff --git a/redex-lib/redex/private/modeless-jf.rkt b/redex-lib/redex/private/modeless-jf.rkt index e68d1b90..b8a78a18 100644 --- a/redex-lib/redex/private/modeless-jf.rkt +++ b/redex-lib/redex/private/modeless-jf.rkt @@ -247,7 +247,7 @@ ;; derivation ;; boolean ;; fail: (list/c derivation?) -> any/c -;; -> match or any/c +;; -> #t or any/c ;; a list of derivations indicates the list of sub-derivations that did not match. (define (call-modeless-judgment-form lang jf-name modeless-jf-clause-table contract-cp deriv only-check-contracts? @@ -306,7 +306,7 @@ (define (modeless-jf-process-rule-candidates lang candidates jf-args sub-derivations fail [bad-derivs '()]) (match candidates - [`() (fail (cons sub-derivations bad-derivs))] + [`() (fail bad-derivs)] [(cons (modeless-jf-clause conclusion-compiled-pattern conclusion-ids-to-duplicate premises-compiled-pattern @@ -370,7 +370,7 @@ premise-jf-procs #t (λ _ #f)))) - (fail-to-next-candidate '())])] + (fail-to-next-candidate sub-derivations)])] [else (fail-to-next-candidate '())])])) @@ -382,18 +382,19 @@ premise-jf-procs fail) (match conc+sub-bindings - ; TODO: Should this include some additional subderivations? - [`() (fail '())] + [`() (fail sub-derivations)] [(cons conc+sub-binding conc+sub-bindings) (cond [(and (not-failure-value? (other-conditions conc+sub-binding)) - (modeless-jf-check-sub-derivations lang - sub-derivations - conc+sub-binding - premises-repeat-names - premise-jf-procs - #f - fail)) + ; BLEH + (equal? #t + (modeless-jf-check-sub-derivations lang + sub-derivations + conc+sub-binding + premises-repeat-names + premise-jf-procs + #f + fail))) #t] [else (modeless-jf-process-other-conditions lang @@ -439,8 +440,8 @@ (cond [(premise-jf-proc sub-derivation contract-checking-only?) (n-loop (- n 1) sub-derivations)] - [else (fail sub-derivation)])] - [_ #f])]))]))) + [else (fail (list sub-derivation))])] + [_ (fail (list sub-derivations))])]))]))) (struct modeless-jf-clause (conclusion-compiled-pattern conclusion-ids-to-duplicate diff --git a/redex-lib/redex/private/reduction-semantics.rkt b/redex-lib/redex/private/reduction-semantics.rkt index c365abe7..f4e1828e 100644 --- a/redex-lib/redex/private/reduction-semantics.rkt +++ b/redex-lib/redex/private/reduction-semantics.rkt @@ -8,6 +8,7 @@ "loc-wrapper.rkt" "error.rkt" "judgment-form.rkt" + "modeless-jf.rkt" "search.rkt" "enum.rkt" (only-in "binding-forms.rkt" @@ -3072,13 +3073,18 @@ (raise-syntax-error 'test-judgment-holds "expected a modeless judgment-form" #'jf)) + (define judgment-form-record (lookup-judgment-form-id #'jf)) #`(let ([derivation e]) - (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) + (test-modeless-jf/proc 'jf derivation + ; Circumvents some of the error checking and judgment tracing of judgment-holds + (call-modeless-judgment-form #,(judgment-form-lang judgment-form-record) + 'jf + #,(judgment-form-proc judgment-form-record) + #,(judgment-form-compiled-input-contract-pat-id + judgment-form-record) + derivation + #f + values) #,(get-srcloc stx)))] [(_ (jf . rest)) (unless (judgment-form-id? #'jf) @@ -3159,33 +3165,15 @@ (newline op) 0]))) -;; Takes a judgment-form name `jf`, a sub-derivation predicate for testing whether a -;; sub-derivation of `jf` is valid. -;; The derivation predicate will only be called on sub-derivations of the -;; judgment `jf`. -;; 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 jf-pred-hash d) - (define (print-derivation-error d) - (parameterize ([pretty-print-print-line (derivation-pretty-printer " ")]) - (pretty-print d (current-error-port)))) - (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 (check-derivation d) - (print-derivation-error d))))) - -(define (test-modeless-jf/proc jf jf-preds derivation val srcinfo) + +(define (print-failing-subderivations bad-sub-derivations) + (parameterize ([pretty-print-print-line (derivation-pretty-printer " ")]) + (for ([d (remove-duplicates bad-sub-derivations)]) + (pretty-print d (current-error-port))))) + +(define (test-modeless-jf/proc jf derivation val srcinfo) (cond - [val + [(equal? #t val) (inc-successes)] [else (inc-failures) @@ -3193,9 +3181,10 @@ (eprintf " derivation does not satisfy ~a\n" jf) (parameterize ([pretty-print-print-line (derivation-pretty-printer " ")]) (pretty-print derivation (current-error-port))) - (when (not (null? (derivation-subs derivation))) + ; A list indicates a list of bad sub-derivations + (when (and val (not (null? val))) (eprintf" because the following sub-derivations fail:\n") - (print-failing-subderivations jf jf-preds derivation))])) + (print-failing-subderivations val))])) (define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?) (define results (thunk)) diff --git a/redex-test/redex/tests/tl-test.rkt b/redex-test/redex/tests/tl-test.rkt index abe7cb2e..c87e6161 100644 --- a/redex-test/redex/tests/tl-test.rkt +++ b/redex-test/redex/tests/tl-test.rkt @@ -199,14 +199,14 @@ (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"))) + (regexp (regexp-quote "because the following sub-derivations fail:\n (derivation '(J x 0) \"Base\" '())"))) (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"))) + (regexp (regexp-quote "because the following sub-derivations fail:\n (derivation '(J 1 0) \"Base\" '())"))) (test (capture-output @@ -250,12 +250,7 @@ (list)))))) (regexp (regexp-quote "because the following sub-derivations fail: - (derivation - '(J2 (1 x) 1) - \"Pair\" - (list - (derivation '(J1 1 x) \"Base\" '()) - (derivation '(J2 1 1) \"Base\" '())))"))) + (derivation '(J1 1 x) \"Base\" '())"))) (test (capture-output @@ -264,17 +259,10 @@ (derivation `(J1 1 x) "Base" (list)) (derivation `(J2 1 1) "Base" - (list)))) - #:mutuals (J1))) + (list)))))) (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\" '())))"))) + (derivation '(J1 1 x) \"Base\" '())"))) (test (capture-output @@ -286,13 +274,7 @@ (list)))))) (regexp (regexp-quote "because the following sub-derivations fail: - (derivation '(J2 1 2) \"Base\" '()) - (derivation - '(J2 (1 1) 2) - \"Pair\" - (list - (derivation '(J1 1 1) \"Base\" '()) - (derivation '(J2 1 2) \"Base\" '())))"))) + (derivation '(J2 1 2) \"Base\" '())"))) (test (capture-output