Add NAME_ASSUMS_TAC and PRINT_GOAL_TAC, improve error messages of a few decision procedures #90
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ew decision procedures This patch adds two simple tactics and improves error messages of a few decision procedures. The added tactics are PRINT_GOAL_TAC and NAME_ASSUMS_TAC. PRINT_GOAL_TAC simply prints the current goal. This is useful for debugging failures from a complicated tactic. NAME_ASSUMS_TAC labels all unnamed assumptions in the goal. This is useful when it is hard to pick an assumption using ASSUME or FIRST_ASSUM. The improved error message now contains the goal term that the decision procedure tried to solve but failed. Updated conversions and tactics are WORD_ARITH, WORD_ARITH_TAC, WORD_BLAST, WORD_RULE, WORD_BITWISE_RULE, ARITH_RULE, ARITH_TAC, INT_ARITH, INT_ARITH_TAC, REAL_ARITH, REAL_ARITH_TAC and TAUT. ``` > ARITH_RULE `1 = 0`;; Exception: Failure "ARITH_RULE `1 = 0`: linear_ineqs: no contradiction". > prove(`1=2`, ARITH_TAC);; Exception: Failure "ARITH_RULE `1 = 2`: linear_ineqs: no contradiction". ```
|
These all look like good improvements to usability. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patch adds two simple tactics and improves error messages of a few decision procedures.
The added tactics are PRINT_GOAL_TAC and NAME_ASSUMS_TAC. PRINT_GOAL_TAC simply prints the current goal. This is useful for debugging failures from a complicated tactic. NAME_ASSUMS_TAC labels all unnamed assumptions in the goal. This is useful when it is hard to pick an assumption using ASSUME or FIRST_ASSUM.
The improved error message now contains the goal term that the decision procedure tried to solve but failed. Updated conversions and tactics are WORD_ARITH, WORD_ARITH_TAC, WORD_BLAST, WORD_RULE, WORD_BITWISE_RULE, ARITH_RULE, ARITH_TAC, INT_ARITH, INT_ARITH_TAC, REAL_ARITH, REAL_ARITH_TAC and TAUT.