search

racket / redex

Other
93 stars 36 forks source link

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

Open wilbowma opened 5 years ago

wilbowma commented 5 years ago

closes #204

wilbowma commented 5 years ago

Rebased on master

wilbowma commented 5 years ago

Added a new optional argument for test-judgment-holds to support reporting sub-derivations from other judgments.

wilbowma commented 5 years ago

Not sure #:mutuals is the right name for that keyword... and I want something that will make sense when I scale this to moded judgments.

rfindler commented 5 years ago

I don't think the interface to the user has to change. Redex should be able to do this on its own.

On Sat, Oct 5, 2019 at 2:16 AM William J. Bowman notifications@github.com wrote:

Not sure #:mutuals is the right name for that keyword... and I want something that will make sense when I scale this to moded judgments.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/pull/205?email_source=notifications&email_token=AADBNMHBBA6GJAYNBP7IC2TQNA5M5A5CNFSM4I5WBSZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEANMHYA#issuecomment-538624992, or mute the thread https://github.com/notifications/unsubscribe-auth/AADBNMFOLRDNWR54KRQNOWDQNA5M5ANCNFSM4I5WBSZA .

wilbowma commented 5 years ago

I believe that, but so far I haven't i figured out how to do it.

I’ll stare at call-modeless-judgment a bit more but I’m going to run out of time to work on it soon.

-- Sent from my phoneamajig

On Oct 5, 2019, at 05:06, Robby Findler notifications@github.com wrote:

I don't think the interface to the user has to change. Redex should be able to do this on its own.

On Sat, Oct 5, 2019 at 2:16 AM William J. Bowman notifications@github.com wrote:

Not sure #:mutuals is the right name for that keyword... and I want something that will make sense when I scale this to moded judgments.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/pull/205?email_source=notifications&email_token=AADBNMHBBA6GJAYNBP7IC2TQNA5M5A5CNFSM4I5WBSZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEANMHYA#issuecomment-538624992, or mute the thread https://github.com/notifications/unsubscribe-auth/AADBNMFOLRDNWR54KRQNOWDQNA5M5ANCNFSM4I5WBSZA .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

wilbowma commented 5 years ago

If we merge up to c3bfe1d60eac2d7dea9f1cbaf8c42a81eb3b58c4, we'll get sound but incomplete information without a change in interface. This could be a good compromise for the time being, until I can figure out call-modeless-judgment.

rfindler commented 5 years ago

Lets just leave it off master for now; people who are savvy enough to get the improvement outside of a release are savvy enough to get the commits from the pull request, I'd say.

wilbowma commented 5 years ago

For context, all of this was born out of this tutorial I wrote: https://www.williamjbowman.com/doc/experimenting-with-redex/sec_judgment.html#%28part._.Testing_.Judgments%29

The hacks I wrote there work okay in userland code, but are painfully inefficient and rely on eval.

So far, looking over call-modeless-judgment, it seems quite hard to isolate exactly which premise fails, since many of the premises and sub-derivations get checked "all at once". For example, modeless-jf-process-rule-candidates checks all the patterns for all the sub-derivations at one time. I'm sure there's a reason for this that I don't understand yet. But it means I can't report which "one" failed to match without significant and possibly inefficient refactoring.

Also, collecting lists of derivations is making the code ugly and unmaintainable so

rfindler commented 5 years ago

It checks things one rule at a time. So it checks the conclusion of the rule and then it does a single match to check all the premises of the rules. If that match worked, it moves on, recursively, to try to check the rules for the subderivations.

The reason it has to do that is you can write an ellipsis "between" premises and we need redex's matcher's functionality to actually do that matching properly. So we take the premises and build up a single pattern for the "above the rule part" (with some new names added in to be able to pull out things later), do that match, and then pull out what are supposed to be conclusions (using those new names) for the next layer in the derivation. (At least I think that's the strategy I settled on. I tried a few before that that didn't work out.)

Does this make sense?

[ edit was to fix the end of the first paragraph ]