Undo the extra expressions added by PR #2783 #3179
Conversation
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.
Source/DafnyCore/Dafny.atg
Outdated
| { IF(IsAndOp()) /* read a conjunction as far as possible */ | ||
| AndOp (. x = t; .) | ||
| RelationalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .) | ||
| RelationalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1, prefixOp); .) |
There was a problem hiding this comment.
Yes right, it's the outermost && that gets the prefix, as you guessed &&1 ((a &&2 b) &&1 c)
| @@ -1928,21 +1929,25 @@ public enum AccumulationOperand { None, Left, Right } | |||
| Contract.Invariant(E1 != null); | |||
| } | |||
|
|
|||
| public BinaryExpr(IToken tok, Opcode op, Expression e0, Expression e1) | |||
| public BinaryExpr(IToken tok, Opcode op, Expression e0, Expression e1, IToken prefixOp) | |||
There was a problem hiding this comment.
| public BinaryExpr(IToken tok, Opcode op, Expression e0, Expression e1, IToken prefixOp) | |
| public BinaryExpr(IToken tok, Opcode op, Expression e0, Expression e1, IToken prefixOp = null) |
Wouldn't this be less invasive?
There was a problem hiding this comment.
It would be, and that's how I originally wrote it, but @MikaelMayer pointed out that it would make it easier to make mistakes during cloning by not cloning the prefixOp. Does avoiding those mistakes outweigh the extra change complexity? I'm undecided.
Source/DafnyCore/PrecedenceLinter.cs
Outdated
| @@ -92,6 +92,8 @@ class PrecedenceLinterVisitor : TopDownVisitor<LeftMargin> { | |||
| // a SeqSelectExpr is the open-bracket). To avoid looking at that internal structure, we instead | |||
| // use the .StartToken for these expressions. | |||
| column = expr.StartToken.col; | |||
| } else if (expr is BinaryExpr binaryExpr && binaryExpr.PrefixOp is not null) { | |||
There was a problem hiding this comment.
Are you not able to do something like binaryExpr.E0.RangeToken.EndToken.Next so you don't need binaryExpr.PrefixOp and all the related changes?
There was a problem hiding this comment.
I think that you're right that this entire branch of the condition isn't necessary.
The prefixOp parameter is still necessary, I think, to ensure that it can go into the FormatTokens property (which is used to compute the StartToken property used in the previous branch).
There was a problem hiding this comment.
Then this comment applies to where FormatTokens is updated 😄
| : base(tok) { | ||
| Contract.Requires(tok != null); | ||
| Contract.Requires(e0 != null); | ||
| Contract.Requires(e1 != null); | ||
| this.Op = op; | ||
| this.E0 = e0; | ||
| this.E1 = e1; | ||
| this.PrefixOp = prefixOp; | ||
| if (prefixOp != null) { |
There was a problem hiding this comment.
Can't you compute prefixOp using e0.RangeToken.End.Next ? Not having prefixOp as an extra parameter seems quite valuable. It seems wrong to me to have custom fields for tokens in our AST when we already have generic fields that contain all tokens.
There was a problem hiding this comment.
Ah, that may be possible. That's an artifact of doing most of this work before merging with PR #3070. Previously, RangeToken wasn't updated to include the leading || or &&, but now it is. I'll investigate.
There was a problem hiding this comment.
It is in fact possible to remove prefixOp, and it's much nicer that way. Thanks for pointing it out!
| @@ -69,6 +69,10 @@ public abstract class INode { | |||
| } | |||
|
|
|||
| void updateStartEndTokRecursive(INode node) { | |||
| if (node is null) { | |||
There was a problem hiding this comment.
I purposedly not included the check because it should never be called on null node. Well I guess we can now put a breakpoint in this if for later!
There was a problem hiding this comment.
Yeah, I suspect one of the elements of Children winds up being null, even though I agree it should be left out in that case.
I'm not too worried about this, because, if we decided to allow null children, this is clearly the right thing to do with them. :)
Simplifies the fix from PR #3179 significantly, removing the need for an extra parameter to the constructor for `BinaryExpr`. <small>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).</small>
This uses
FormatTokensto 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.