-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Feat: Added ranges to expression #1985
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
👍 lovely
Source/Dafny/AST/DafnyAst.cs
Outdated
private void RecomputeStartEnd() { | ||
startTok = tok; | ||
endTok = tok; | ||
foreach (var e in SubExpressions) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Possibly out of scope: it would help if SubExpressions
was a IReadOnlyList
so you could retrieve the first and last element without having to iterate.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You mean, we could cache the SubExpressions? That's a good point, but yes, let's leave it out of scope for this PR.
Source/Dafny/AST/DafnyAst.cs
Outdated
endTok = tok; | ||
foreach (var e in SubExpressions) { | ||
if (e.tok.pos < startTok.pos) { | ||
startTok = e.tok; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't this be e.StartTok
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes that would be even better, thanks. I'm also adding a check that the filename should be the same.
Source/Dafny/AST/DafnyAst.cs
Outdated
public IToken RangeToken => new RangeToken(StartTok, EndTok); | ||
|
||
// Computes the start and end token of this expression | ||
private void RecomputeStartEnd() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this called Re
compute, isn't it only called once?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I imagine it could be called multiple times if we modify the AST, e.g. by adding elements in a set comprehension. But we can always clone and expression, modify it and then access the new range so that's not useful. Will remove this method.
Source/Dafny/AST/DafnyAst.cs
Outdated
if (e.tok.pos < startTok.pos) { | ||
startTok = e.tok; | ||
} else if (e.tok.pos > endTok.pos) { | ||
endTok = e.tok; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't this be e.EndTok
?
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -9070,6 +9086,48 @@ public abstract class Expression { | |||
get { yield break; } | |||
} | |||
|
|||
private IToken startTok; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not store the RangeToken instead of two ITokens?
Source/Dafny/AST/DafnyAst.cs
Outdated
|
||
// Creates a token on the entire range of the expression. | ||
// Used only for error reporting. | ||
public IToken RangeToken => new RangeToken(StartTok, EndTok); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you think we could move all the new code to a class
class SyntaxNode {
public readonly IToken tok;
public abstract IEnumerable<SyntaxNode> ChildNodes {get;}
public IToken RangeToken =>
..
}
and then have
class Expression : SyntaxNode {
public IEnumerable<SyntaxNode> ChildNodes => SubExpressions;
}
Or do you feel that's too early for this PR ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We could as well use the bounded polymorphism pattern:
class SyntaxNode<T> where T: SyntaxNode {
public readonly IToken tok;
public abstract IEnumerable<T> Children{get;}
public IToken RangeToken =>
..
}
class Expression : SyntaxNode<Expression> {
}
However, we should do this refactoring later, when I see a compelling reason to do so. We might as well replace the "tok" by a Format or trait to keep track of concrete syntax tree elements.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
However, we should do this refactoring later
Alright. Indeed, I think it only makes sense to do this if we have multiple subclasses of SyntaxNode.
@@ -110,6 +111,10 @@ public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame) | |||
Contract.Requires(modifiesFrame != null); | |||
} | |||
|
|||
internal IToken GetTok(Expression e) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not name it GetToken
? Also, I'm not a fan of e
even though this is such as short method ^^
@@ -44,6 +44,7 @@ public partial class Translator { | |||
public class TranslatorFlags { | |||
public bool InsertChecksums = 0 < DafnyOptions.O.VerifySnapshots; | |||
public string UniqueIdPrefix = null; | |||
public bool ReportRanges = false; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When do we not want to report ranges? Looks like it's turned on for the IDE but not the CLI. Why the difference?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, because the IDE will highlight ranges. However, in the CLI, there is a format to report positions only, so that would mean 1) to change that format to support ranges of positions, which would be cluttering 2) or we could also decide so activate this option when -showSnipptes is enabled, but it's not the option by default yet and it will require to change the way we display errors anyway.
I though we should first add these ranges in the Dafny Language Server, where they are the most useful, and then we can always do this later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Alright
@@ -582,7 +582,7 @@ modifies this | |||
Assert.AreEqual("This is the postcondition that might not hold.", relatedInformation[0].Message); | |||
Assert.AreEqual(new Range((14, 16), (14, 21)), relatedInformation[0].Location.Range); | |||
Assert.AreEqual("Related location", relatedInformation[1].Message); | |||
Assert.AreEqual(new Range((9, 13), (9, 14)), relatedInformation[1].Location.Range); | |||
Assert.AreEqual(new Range((9, 11), (9, 16)), relatedInformation[1].Location.Range); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we have tests with more nested expressions as well?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
tests added
Nice change! |
Failed function call highlight Other cases of extended range highlighting
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -8997,6 +9026,38 @@ public abstract class Expression { | |||
get { yield break; } | |||
} | |||
|
|||
private RangeToken rangeToken; | |||
|
|||
// Creates a token on the entire range of the expression. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpick: I'd prefer documentation comments ///
above members.
Before (possibly failing assertions are barely visible):
After (assertions are clearly visible)
Although it cannot be seen yet, related positions on postconditions also now cover an entire expression instead of just a token.
This PR:
RangeToken
if an translator option ``ReportRange` is activatedIn the translator, the method
GetTok
replaces.tok
to perform the switch.After searching for 30 minutes, I didn't find what else to change to get an entire function or method call to be entirely highlighted, any hint @RustanLeino ?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.