feat: Trivia stored in the AST #1801
Conversation
# Conflicts: # Source/Dafny.sln # Source/Dafny/AST/DafnyAst.cs # Source/Dafny/Resolver.cs # Source/Directory.Build.props # Test/libraries
MikaelMayer
changed the title
…into feat-add-trivia
# Conflicts: # Source/Dafny/Verifier/Translator.ClassMembers.cs # Source/Dafny/Verifier/Translator.cs
| ) { | ||
| if(triviaTrailing && (ch == '\r' || ch == '\n')) { | ||
| if(ch == '\r' || (ch == '\n' && !lastWasCr)) { // Don't count \r\n as two newlines. | ||
| triviaNewlines++; |
There was a problem hiding this comment.
What's the definition of trailing trivia in this PR? Shouldn't any newlines set triviaTrailing = false; ?
For example, if I have a statement block:
var y := 4; // comment about y;
var x := 3; // comment about x;
if (x == 3) {
// only usage of y;
}And I do a refactoring on y called "move to innermost scope" that moves the declaration inside the if, then we should end up with:
var x := 3; // comment about x;
if (x == 3) {
var y := 4; // comment about y;
// only usage of y;
}How does the trivia parsing in this PR achieve that?
I get the impression that you changed the definition of trailing trivia because of what we want for docstrings, but I don't understand why that was necessary.
I thought a docstring is any block comment that occurs after the signature of the function/method (callable?), which according to our original definition of leading and trailing trivia, would be leading trivia of one of the tokens belonging to the callable, like ensures, requires or {.
Is there a downside to having that extra rewrite step? |
| /// | ||
| /// ``` | ||
| /// const /*for const*/ x /*for x*/ := /* for := */ 1/* for 1 */ | ||
| /// // for 1 again |
There was a problem hiding this comment.
This example makes me doubtful about our choices.
Since we decided docstrings on const declarations should occur after the const, // for 1 again is a docstring for the const right? So the implementation for finding the docstrings for constants is then:
Const.Docstring => Const.DeepChildren.Last().TrailingTriviaIt seems inconsistent to me to have the docstring for a node not be attached to that node. Suppose you have
const x := 3 + 42 // docstring for xand then I use an "extract variable" refactoring on 42 and name the new variable magicNumber, we get:
const magicNumber := 42 // docstring for x
const x := 3 + magicNumberThat's not intuitive right?
What if we let docstrings occur after the signature but before the body, also for consts, in which case it would occur right before the :=. If we do that, then we could also use our original definition of leading and trailing trivia, where comments generally attach to the current or next node, but not the previous one, which I feel is more intuitive.
Then we get
const x /* docstring for x */ := 3 + 42or
const x
// really elaborate
// docstring for x
:= 3 + 42and refactoring anything in the body will keep the docstring in the same place.
@cpitclaudel could you chime in what behavior we want regarding what nodes trivia attach to?
For example, for
var x := 1;
// which statement does this comment belong to?
var y := 2;| /// All the remaining trivia is for the LeadingTrivia of the next token | ||
| /// | ||
| /// ``` | ||
| /// const /*for const*/ x /*for x*/ := /* for := */ 1/* for 1 */ |
There was a problem hiding this comment.
I think it's more import to know which AST nodes the trivia attach to than which tokens, so I would replace /* for := */ with `/* for const */
Source/Dafny/AST/DafnyAst.cs
Outdated
| @@ -24,32 +24,56 @@ public class FilledInDuringResolutionAttribute : System.Attribute { } | |||
| public interface IToken : Microsoft.Boogie.IToken { | |||
| // Inherited for now. | |||
There was a problem hiding this comment.
I think we can drop this comment and the subsequent block comment.
Source/Dafny/AST/DafnyAst.cs
Outdated
| int col { get; set; } | ||
| int line { get; set; } | ||
| string val { get; set; } | ||
| int kind { get; set; } // Used by coco, so we can't rename it to Kind |
There was a problem hiding this comment.
Could you move these comments so they occur on the lowercase properties?
…into feat-add-trivia
…into feat-add-trivia
This PR brings the following changes to Dafny
Boogie.ITokenby a derivativeDafny.IToken, and same forToken(no need to change Boogie like in a previous attempt)leadingTriviaandtrailingTriviaFirstDeclarationToken, so that it's possible to recover the trivia before itThis fixes #1528 for all trivia technically accessible a token stored in the AST.
Implementation details:
I ignored the following very relevant advice here:
https://github.com/terrajobst/minsk/blob/master/docs/episode-24.md
because we will visibly put comments after definitions, except when using /** */ before a top-level definition and separated by at least an empty newline
Work in Progress
This PR is the first step towards having a full Dafny formatter.
What to review
This PR seems huge, but there isn't as much to review. Here is what to look for, in the same order as when you click on the "files" tab. In bold, files that are important reviewing. Other files are just automated refactorings.
ITokenandToken, and fieldFirstDeclarationTokento declarationsITokenandTokenBpl.Token=>Tokenand same forITokenBpl.Token=>TokenBpl.Token=>TokenTranslator.ToDafnyTokenused when doing roundtrips with translating to BoogiesplitExpr.Tok(defined later)splitExpr.Tok,ToDafnyTokenand use of Dafny Token.