Add warnings about possibly confused operator precedence #2783
Conversation
# This is the 1st commit message: Back out match handling and tests # This is the commit message dafny-lang#2: Rethink match
This is to put a band-aid on the fact that NestedMatchExpr is not resolved, so we have to look at MatchExpr’s instead.
| VisitLhsComponent(expr.tok, bin.E0, | ||
| // For | ||
| // a) LHS ==> RHS | ||
| // b) LHS ==> |
There was a problem hiding this comment.
This was unclear. My intention was to say the RHS is somewhere on the next line (in particular, the RHS is not on the same line as the ==>). I have clarified this in the source-file comments.
| } else if (expr is ITEExpr ifThenElse) { | ||
| VisitIndependentComponent(ifThenElse.Test); | ||
| VisitIndependentComponent(ifThenElse.Thn); | ||
| VisitRhsComponent(expr.tok, ifThenElse.Els, "else branch of if-then-else"); |
There was a problem hiding this comment.
what about
if A then B else match C {
case Z =>
}
The formatter is happy because it finds that the match's content does not need to be aligned (although there is a deactivated function for that)
Maybe in your case, you could issue the warning only if the expression after the else is a binary or a chaining operator ?
There was a problem hiding this comment.
What you're suggesting is what is happening. More precisely, the body of the match is visited independently of the context it's found in. So, no warning is generated for the example you gave.
There was a problem hiding this comment.
I added the example as a test case, showing that it does not generate any warnings.
| VisitIndependentComponent(quantifierExpr.Range); | ||
| } | ||
| VisitRhsComponent(expr.tok, quantifierExpr.Term, | ||
| expr.tok.line == quantifierExpr.Term.StartToken.line ? expr.tok.col + 1 : quantifierExpr.Term.StartToken.col, |
There was a problem hiding this comment.
So you are suggesting that, if there is no newline after the "::", then everything should be after the "::", correct ? If so, can you please add a comment in plain English about that.
Also, the following code is legitimate (the Dafny formatter will detect a match expression and allow the line wrap to be past before the :: column), and it would still trigger a warning in your setting.
(forall x: nat | x < 10 :: x match {
case P(x) => true
case Q(y) => x == false
})
To avoid that, you could put a warning only if the expression after :: is a parenthesesless expression, like for the else example above.
There was a problem hiding this comment.
Could you please ensure there is a test for the expression above, to show that it does not trigger errors? After that, I'm good approving it !
There was a problem hiding this comment.
I don't quite follow your example, because it is not legal Dafny. I added the following test case, which I hope captures the spirit of your example:
datatype PQ = P(int) | Q(bool)
method M(s: set<PQ>)
requires
(forall pq | pq in s :: match pq {
case P(x) => true
case Q(y) => y == false
})
{
}No precedence warning is generated for this example.
# Conflicts: # Source/DafnyCore/Resolver.cs
This uses `FormatTokens` to keep track of the beginning of a sequence of expressions prefixed by `&&` or `||` instead of a synthetic identity expression. Not quite complete, as it causes occasional null pointer exceptions when retrieving the range of certain `TokenWrapper` instances that seem to be wrapped around null.
This uses `FormatTokens` to keep track of the beginning of a sequence of expressions prefixed by `&&` or `||` instead of a synthetic identity expression. Fixes a performance regression caused by #2783. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
A common mistake is to write an expression like
with the intention of writing
This PR emits warnings when certain operator arguments seem to go on for too long, where "seem to" is judged based on identation.
The basic idea is to look where the right-hand operand of
==>starts and then insist that all tokens in the RHS are aligned at, or to the right of, the column of the RHS start. This same idea is used for other kinds of "right-hand sides", too, like theelsebranch of anif-then-elseexpression and the body ("term") of logical quantifiers.When looking at the RHS, certain parts of the RHS expression are ignored (or, rather, are treated separately). This happens when an expression has a "middle" part, like the
thenbranch of anif-then-elseexpression. For example, no warning is produced forIf an expression of interest
eis found in the RHS, thene's internal structure is analyzed forebut not for the enclosing expression. For example, no warning is produced forThe left-hand side of
==>is also analyzed. Some more details are found in theVisitOneExprmethod inPrecedenceLinter.cs.The binary operators
==>,<==, and<==>are treated as mentioned above, since these operators have relatively low binding powers. The linter does not do this processing for any other binary operators, like&&,||,+, and*.Fixes #1311
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.