Skip to content

Commit

Permalink
Collect failing sub-derviations from call-modeless-judgment-form and …
Browse files Browse the repository at this point in the history 
…friends
  • Loading branch information
@wilbowma
wilbowma committed Oct 10, 2019
1 parent 905b8b7 commit 0dcbe78
Showing 1 changed file with 25 additions and 16 deletions.
41 changes: 25 additions & 16 deletions redex-lib/redex/private/modeless-jf.rkt
View file
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
;; -> 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
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 (cons sub-derivations 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 '())])]
[else (fail-to-next-candidate '())])]))


(define (modeless-jf-process-other-conditions lang
Expand All @@ -376,7 +382,8 @@
premise-jf-procs
fail)
(match conc+sub-bindings
[`() (fail)]
; TODO: Should this include some additional subderivations?
[`() (fail '())]
[(cons conc+sub-binding conc+sub-bindings)
(cond
[(and (not-failure-value? (other-conditions conc+sub-binding))
Expand All @@ -385,7 +392,8 @@
conc+sub-binding
premises-repeat-names
premise-jf-procs
#f))
#f
fail))
#t]
[else
(modeless-jf-process-other-conditions lang
Expand All @@ -406,7 +414,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,7 +439,7 @@
(cond
[(premise-jf-proc sub-derivation contract-checking-only?)
(n-loop (- n 1) sub-derivations)]
[else #f])]
[else (fail sub-derivation)])]
[_ #f])]))])))

(struct modeless-jf-clause (conclusion-compiled-pattern
Expand Down

2 comments on commit 0dcbe78

@rfindler
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we need to work from examples here. So maybe starting by working on opening the right private functions to a test suite that can test modeless judgment forms (unless you think we can test by parsing error messages?).

Also, as I recall, there are tricky bits to this code to deal with premises that have ellipses in them.

One simplification that I would support is that if a judgment form doesn't name the premises then we can just not include nice information in the error messages. With that assumption, you can commit to specific rules right away and, as soon as something fails, we know where the failure is (so no lists are needed anymore).

If we did want to support judgment forms that have #fs in the names then we could say that we're committed to a judgment as soon as a conclusion matches, so we either say "at this point in the tree, no conclusions matched" and that's the error message, or we say "at this point in the tree, this conclusion matched but the premises for it didn't match" (or maybe we have to offer multiple in this last case when multiple rules match at the conclusion but none match at the premise).

@wilbowma
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the feedback!

Don't consider this real code yet; this is me playing to figure out what's going on, and I figured I'd just play in this branch for now. I'll let you know when I think I have something worth looking at.

Please sign in to comment.