Feat code actions forall calc #6044
Merged
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
# Conflicts: # Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs
| return new DafnyCodeActionEdit[] { }; | ||
| } | ||
|
|
||
| if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.EndToken is { val: ";" } endToken) { |
There was a problem hiding this comment.
Please extract the condition to a variable to make it easier to read what it does
| indentation2 + GetStatementToInsert(indentation2) + "\n" + | ||
| indentation + "}"; | ||
| return ReplaceWith(endToken, block); | ||
| } else if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.OwnedTokens.FirstOrDefault(t => t.val == "by") is { Next: { val: "{" } braceToken } byToken) { |
There was a problem hiding this comment.
Please extract the condition to a variable to make it easier to read what it checks
| private readonly Expression failingImplicitAssertion; | ||
| private readonly Node program; | ||
| private readonly Range selection; | ||
| public static INode? GetInsertionNode(Node program, Range selection, out List<INode>? nodesSinceFailure, out bool needsIsolation) { |
There was a problem hiding this comment.
What is an insertion node? Can you use a longer name to explain what this is?
What is nodesSinceFailure?
Can you move GetInsertionNode to after the method that calls is?
keyboardDrummer
approved these changes
Jan 24, 2025
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.
What was changed?
First, for implicit assertions, if they are surrounded by a declaration that supports by clause (like AssertStmt or CallStmt), the by clause is preferred to inserting the assertion before.
And that works also for well-formedness, since well-formedness is now proved by by-blocks (thanks @keyboardDrummer for that, and @alex-chew for creating Dafny expressions for well-formedness)
Moreover, if a by clause already exist, the code action will insert into it.
Second, assertion of foralls now support a proof sketch by inserting forall statement
Third, assertions of equalities or equivalence now support a proof sketch by inserting a calc statement.
The code for inserting such proof sketches has been refactored so that it will be even more easy to extend in the future.
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.