Fix sub-derivations failure reporting in test-judgment-holds #205
Conversation
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
force-pushed
the
test-subderivations
branch
from
b772c8c
to
c3bfe1d
Compare
|
Rebased on master |
wilbowma
changed the title
|
Added a new optional argument for |
|
Not sure |
|
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 ***@***.***> 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
<#205?email_source=notifications&email_token=AADBNMHBBA6GJAYNBP7IC2TQNA5M5A5CNFSM4I5WBSZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEANMHYA#issuecomment-538624992>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AADBNMFOLRDNWR54KRQNOWDQNA5M5ANCNFSM4I5WBSZA>
.
|
|
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 ***@***.***> 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 ***@***.***>
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
> <#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.
|
|
If we merge up to c3bfe1d, 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 |
|
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. |
|
For context, all of this was born out of this tutorial I wrote: The hacks I wrote there work okay in userland code, but are painfully inefficient and rely on So far, looking over Also, collecting lists of derivations is making the code ugly and unmaintainable so |
|
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 ] |
closes #204