Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix sub-derivations failure reporting in test-judgment-holds #205

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Fix sub-derivations failure reporting in test-judgment-holds #205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
dec519a
Added tests that expose problem in test-judgment-holds
wilbowma Oct 5, 2019
c3bfe1d
Only report proper sub-derivations from test-judgment-holds
wilbowma Oct 5, 2019
2807a59
Support reporting sub-derivation failures from any specified judgment
wilbowma Oct 5, 2019
905b8b7
Documentation for test-judgment-holds with sub-derivation reporting
wilbowma Oct 5, 2019
0dcbe78
Collect failing sub-derviations from call-modeless-judgment-form and …
wilbowma Oct 10, 2019
178c1a2
Balls of hacks that are somewhat closer to doing the right thing
wilbowma Oct 11, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 42 additions & 2 deletions redex-doc/redex/scribblings/ref/testing.scrbl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]{
Expand Down
54 changes: 32 additions & 22 deletions redex-lib/redex/private/modeless-jf.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,9 +245,13 @@
;; hash[rulename -o> (listof modeless-jf-clause?)]
;; compiled-pattern
;; derivation
;; -> match or #f
;; boolean
;; fail: (list/c derivation?) -> 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?)
only-check-contracts?
[fail (λ _ #f)])
(match deriv
[(derivation (cons deriv-jf-name jf-args) rule-name sub-derivations)
(cond
Expand All @@ -262,16 +266,16 @@
rules
jf-args
sub-derivations
(λ () #f))]
fail)]
[else
(define known-rules (sort (hash-keys modeless-jf-clause-table) string<?))
(error jf-name "unknown rule in derivation\n rule: ~.s\n known rules:~a"
rule-name
(apply string-append
(for/list ([rule (in-list known-rules)])
(format "\n ~s" rule))))]))]
[else #f])]
[_ #f]))
[else (fail (list deriv))])]
[_ (fail (list deriv))]))

(define (modeless-judgment-form-check-contract jf-name contract-cp jf-args)
(when contract-cp
Expand Down Expand Up @@ -300,9 +304,9 @@
first-set-of-args
maybe-more-args)))))

(define (modeless-jf-process-rule-candidates lang candidates jf-args sub-derivations fail)
(define (modeless-jf-process-rule-candidates lang candidates jf-args sub-derivations fail [bad-derivs '()])
(match candidates
[`() (fail)]
[`() (fail bad-derivs)]
[(cons (modeless-jf-clause conclusion-compiled-pattern
conclusion-ids-to-duplicate
premises-compiled-pattern
Expand All @@ -313,12 +317,13 @@
premise-jf-procs)
more-candidates)
(define conc-mtch (match-pattern conclusion-compiled-pattern jf-args))
(define (fail-to-next-candidate)
(define (fail-to-next-candidate bad-subderivs)
(modeless-jf-process-rule-candidates lang
more-candidates
jf-args
sub-derivations
fail))
fail
(append bad-subderivs bad-derivs)))
(cond
[conc-mtch
(define sub-derivations-arguments-term-list
Expand Down Expand Up @@ -363,9 +368,10 @@
(mtch-bindings sub-derivations-mtch)
premises-repeat-names
premise-jf-procs
#t)))
(fail-to-next-candidate)])]
[else (fail-to-next-candidate)])]))
#t
(λ _ #f))))
(fail-to-next-candidate sub-derivations)])]
[else (fail-to-next-candidate '())])]))


(define (modeless-jf-process-other-conditions lang
Expand All @@ -376,16 +382,19 @@
premise-jf-procs
fail)
(match conc+sub-bindings
[`() (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))
; 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
Expand All @@ -406,7 +415,8 @@
conc+sub-binding
premises-repeat-names
premise-jf-procs
contract-checking-only?)
contract-checking-only?
fail)
(let loop ([premise-jf-procs premise-jf-procs]
[premises-repeat-names premises-repeat-names]
[sub-derivations sub-derivations])
Expand All @@ -430,8 +440,8 @@
(cond
[(premise-jf-proc sub-derivation contract-checking-only?)
(n-loop (- n 1) sub-derivations)]
[else #f])]
[_ #f])]))])))
[else (fail (list sub-derivation))])]
[_ (fail (list sub-derivations))])]))])))

(struct modeless-jf-clause (conclusion-compiled-pattern
conclusion-ids-to-duplicate
Expand Down
44 changes: 26 additions & 18 deletions redex-lib/redex/private/reduction-semantics.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
"loc-wrapper.rkt"
"error.rkt"
"judgment-form.rkt"
"modeless-jf.rkt"
"search.rkt"
"enum.rkt"
(only-in "binding-forms.rkt"
Expand Down Expand Up @@ -3060,7 +3061,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"
Expand All @@ -3071,8 +3073,19 @@
(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 (lambda (x) (judgment-holds jf x)) derivation (judgment-holds jf derivation) #,(get-srcloc stx)))]
(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)
(raise-syntax-error 'test-judgment-holds
Expand Down Expand Up @@ -3152,31 +3165,26 @@
(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)

(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)
(print-failed srcinfo)
(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-pred derivation))]))
(print-failing-subderivations val))]))

(define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?)
(define results (thunk))
Expand Down
67 changes: 65 additions & 2 deletions redex-test/redex/tests/tl-test.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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\" '())")))

(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\" '())")))

(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\" '())")))

(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))
"3 tests failed (out of 4 total).\n"))

(let ()
(define-judgment-form empty-language
#:mode (broken-swap I I O O)
Expand Down