feat: Provide formals and declarations type highlighting. #1630

MikaelMayer · 2021-12-04T02:27:56Z

I added hovering type annotations to formals (in parameters)

and out parameters

Local variable declarations.

Bound variables in set comprehensions

Bound variables in forall expressions

Bound variables in exists expressions

Bound variables in map comprehensions

Bound variables in lambdas

By method bodies in functions

Let expressions:

Note that not only this adds hovering annotations, but it also adds the ability to jump to the definition for all variables declared in set and map comprehensions, forall and exists expressions, and let expressions, using either the right-click menu or CTRL+click on the variable.

Previously, hovering such variables either at declaration sites or even on their use site (for comprehensions) did not show any hint about their type, even in specifications.
The reason why this is useful is that it removes the need to investigate a method call's signature to know what is the type of a variable that is declared and assigned at the same time, and for formals for consistency.

camrein

I like this improvement since it's sometimes useful to see what type the compiler infers.

I prefer that we stick to SingleOrDefault since for the lookup there must not be any overlapping ranges because a designator should not have multiple lookup entries.
Moreover, please add a new test for the now supported Formal lookup.

camrein · 2021-12-06T11:55:15Z

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs

+ var symbolsAtPosition = LookupTree.Query(position);
+ // TODO: Figure out why duplication crashes SingleOrDefault before using FirstOrDefault 
+ // Use case: function f(a: int) {}, and hover over a.
+ symbol = symbolsAtPosition.FirstOrDefault();


Since there should only be one LookUp entry per designator, one designator is registered twice or overlaps with the range of another.
This should be fixed as this probably hides another error.

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

MikaelMayer · 2021-12-06T17:01:32Z

I like this improvement since it's sometimes useful to see what type the compiler infers.

I prefer that we stick to SingleOrDefault since for the lookup there must not be any overlapping ranges because a designator should not have multiple lookup entries. Moreover, please add a new test for the now supported Formal lookup.

Thank you for letting me know how much it was important to keep SingleOrDefault. I will definitely sort this out and when this works, I'll confirm the behavior using a test and un-draft the PR.

MikaelMayer · 2021-12-06T18:48:25Z

I did not find documentation about how to run the tests in DafnyLanguageServer.Test
How to run them?

Removed autogenerated expressions from analysis

camrein · 2021-12-07T09:00:40Z

I did not find documentation about how to run the tests in DafnyLanguageServer.Test
How to run them?

I'm sorry that I haven't documented this yet. I tend not to document things that are standard for the utilized platform. That was the same for the VSCode extension until Robin asked for documentation.

You can either test it through the IDE. For example, in Visual Studio you can open the Test Explorer view:

This view allows you to run (and debug) the whole test suite using the Play button or individual tests by right-clicking them.

Alternatively, you can execute the tests through the command line:

dotnet test .\Source\DafnyLanguageServer.Test\DafnyLanguageServer.Test.csproj

It's important to note that you may have to place z3 in the build directory of the tests. That's DafnyLanguageServer.Test/bin/Debug/net5.0 and DafnyLanguageServer.Test/bin/Release/net5.0, depending on your build settings. Well, I guess that at least this special setup requirement should be documented.

MikaelMayer · 2021-12-07T15:04:42Z

Thanks for these instructions. I think they are relevant to any new user so that I added them in the wiki
https://github.com/dafny-lang/dafny/wiki/INSTALL#running-dafnylanguageserver-and-dafnypipeline-tests

Fixed function body hovering. ComprehensionSymbol is now a ScopeSymbol

Support for scopes in method and function specifications.

MikaelMayer · 2021-12-08T22:41:23Z

This PR is ready for review @camrein . Nothing new specific on my agenda. I did many upgrades in the highlighting system (see updated PR message)

camrein

That's a great improvement.
I haven't fully reviewed it since I have the feeling some changes might be irrelevant.

In general, the language server does not have any abbreviations so I'd prefer to keep this style. I have seen some things that would need improvement (probably in another PR) to make the design choices a bit more clear.

Feel free to tag me once you've included my suggested changes (note: I haven't marked everything since there are some repetitions of the same pattern).

Source/DafnyLanguageServer/Language/Symbols/ComprehensionSymbol.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs

Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

- Groupped LetExpr and ComprehensionExpr in a single interface for accessing bound variables - Added test case for result variable in functions + implemented it - New overloads for every type of comprehension expression + simplifications. - Fixed CI warnings about potential null initalization - Removed abbreviations - Moved AsEnumerable from Symbol to SymbolExtensions - Removed obsolete TODO

…ub.com/dafny-lang/dafny into ide-highlight-formals-and-declarations

MikaelMayer · 2021-12-09T20:18:16Z

@camrein These were great improvement suggestions. I carefully reviewed each of them and did my best to handle repetitions of the same patterns.
If needed, here are the changes since your last review
7de6a53

…rn type which cause symbol building to crash. Fixed potential errors with null tokens

…ub.com/dafny-lang/dafny into ide-highlight-formals-and-declarations

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

Fail-safe but debuggable TryGetSymbolAt.

camrein

Thanks a lot for these improvements. This looks way better now.

Source/Dafny/Cloner.cs

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs

- Use of pattern matching - Warning logging if duplicate symbol in lookup table - Adding to list of symbol instead of replacing the initialized list - Better naming of start and end token for scope symbol - Removed a canceled refactoring artefact (IToken? => IToken) - Removed extra whitespace -

camrein

This looks great so far. I've only had some minor input now. Thanks for taking your time.

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs

camrein

Looks great, thanks!
Since I might be biased by now, @keyboardDrummer would you mind giving a second look?

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

keyboardDrummer · 2021-12-17T14:58:44Z

Source/Dafny/AST/DafnyAst.cs

@@ -265,8 +266,9 @@ public class BuiltIns {
 /// the built-in total-arrow type (if "total", in which case "member" is expected to denote the "requires" member).
 /// The given "id" is expected to be already resolved.
 /// </summary>
- private Expression ArrowSubtypeConstraint(IToken tok, BoundVar id, Function member, List<TypeParameter> tps, bool total) {
+ private Expression ArrowSubtypeConstraint(IToken tok, IToken endTok, BoundVar id, Function member, List<TypeParameter> tps, bool total) {


Should we not use the IRegion interface here so we only need a single parameter?

The two places in which this ArrowSubtypeConstraint is being called actually give Token.NoToken as argument, so there is nothing close to IRegion to provide, so although this is a good suggestion, it's better to keep it this way until there is a compelling reason to change it.

Why not wrap the Tokens in a class Region : IRegion? I think it's common for AST nodes to know their start and end token, and to store both in a single object. Why have two parameters when you can have one?

After 1-1 discussion, we agreed that, since Expressions already use tok for the start token, it's better to leave this huge refactoring for an independent PR later.

We will eventually add start and end positions for every expression in Dafny's grammar, so it's not useful to do this change now in a way that would be half-baked.

@cpitclaudel ?

Thanks for the ping, I had a quick look. I'm not sure when the right time is to change the way end tokes are passed, but here's my 2¢:

Are these tokens used for anything else than position reporting? If not, they shouldn't even be passed into the various AST constructors, and only ranges instead. It's OK to implement a range variant that's based on a pair of tokens if we really want to keep the tokens around for some reason.

Exposing a pair of tokens directly is a risky business, because it's unclear (at least to me) what the semantics of end tokens are. For example when you convert to a range you use GetLSPPosition on both tokens, but that means the range ends on the beginning of the last token. If the last token is part of the range, the range should end at the end of that token instead. If the current code is right, then I expect others will make the same mistake as I did when proofreading this, so I think there's value in a level of indirection that encapsulates pairs of tokens and exposes a range.

I have no thoughts on when that change should be done. It would be OK to me to put a FIXME in there, but I don't know the context of this change.

HTH!

(Also, I props to you on completing that change; it's impressive me how complicated this conceptually simple change ended up being, so nice job on pushing it through — and the final feature is very cool.)

I have no thoughts on when that change should be done. It would be OK to me to put a FIXME in there, but I don't know the context of this change.

Do we all to agree that the desirable end state is for every expression AST Node to have a Range/Region field instead of a token field? I don't think there is a reason to work with tokens after parsing.

Given that end state, why make a detour by first introducing a second token field to expression AST nodes?

I think we all agree on the final state.

It's not a detour, it's actually reusing the same field name and interface as the statements, i.e. being consistent with the system already in place.

it's actually reusing the same field name and interface as the statements, i.e. being consistent with the system already in place.

Okay, let's settle with that then.

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

camrein · 2021-12-20T12:48:44Z

@MikaelMayer thanks for applying my suggested changes and explaining to me some of your decisions.
For me, it looks fine for now. If @keyboardDrummer doesn't have any other feedback a merge should be fine.

cpitclaudel · 2021-12-20T18:40:44Z

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

- new Range(scopeSymbol.Declaration.Tok.GetLspPosition(), scopeSymbol.Declaration.EndTok.GetLspPosition())
+ scopeSymbol.BodyStartToken,
+ scopeSymbol.BodyStartToken.GetLspRange(),
+ new Range(scopeSymbol.BodyStartToken.GetLspPosition(), endToken.GetLspPosition())


Don't you want ToLspPosition(token.line, token.col + token.val.Length) here? (as in GetLspRange?)

(I've added details about this above; copied here for context:)

It's unclear to me what the semantics of end tokens are. For example when you convert to a range you use GetLSPPosition on both tokens, but that means the range ends on the beginning of the last token. If the last token is part of the range, the range should end at the end of that token instead.

This PR fixes formals and declarations type highlighting.

861f9e6

MikaelMayer requested a review from camrein December 4, 2021 02:27

camrein reviewed Dec 6, 2021

View reviewed changes

MikaelMayer added 2 commits December 6, 2021 14:25

Tests++ && SingleOrDefault

99de7f2

Removed autogenerated expressions from analysis

Visit of all comprehensions to find bounded variables

dbea7ce

MikaelMayer added 3 commits December 7, 2021 09:07

Added missing ComprehensionSymbol.cs + fixed warnings

e85a386

Added missing keyword

d49e596

Fixed all the tests and added other comprehension tests

788f879

MikaelMayer marked this pull request as ready for review December 7, 2021 16:11

MikaelMayer requested a review from camrein December 7, 2021 16:11

MikaelMayer self-assigned this Dec 7, 2021

MikaelMayer marked this pull request as draft December 7, 2021 17:23

MikaelMayer and others added 4 commits December 7, 2021 12:41

WIP: Adding function bodies and by method bodies

abbba7f

by method body function hovering.

366e4c8

Fixed function body hovering. ComprehensionSymbol is now a ScopeSymbol

Support for Let Expressions

633aa60

Support for scopes in method and function specifications.

Merge branch 'master' into ide-highlight-formals-and-declarations

2b663c7

MikaelMayer marked this pull request as ready for review December 8, 2021 22:40

camrein reviewed Dec 9, 2021

View reviewed changes

MikaelMayer added 2 commits December 9, 2021 14:14

Merge branch 'ide-highlight-formals-and-declarations' of https://gith…

58a60d6

…ub.com/dafny-lang/dafny into ide-highlight-formals-and-declarations

MikaelMayer requested a review from camrein December 9, 2021 20:18

MikaelMayer enabled auto-merge (squash) December 9, 2021 20:20

MikaelMayer added 2 commits December 9, 2021 16:12

Fixed tests to measure more precise errors.

7144bd3

Fixed inferred type that has the same position as the function's retu…

90f845d

…rn type which cause symbol building to crash. Fixed potential errors with null tokens

MikaelMayer requested a review from camrein December 10, 2021 16:06

MikaelMayer added 3 commits December 10, 2021 16:31

Avoid registering the result type twice for functions

991b769

Merge branch 'master' into ide-highlight-formals-and-declarations

91b5b3c

Merge branch 'ide-highlight-formals-and-declarations' of https://gith…

37b7e52

…ub.com/dafny-lang/dafny into ide-highlight-formals-and-declarations

MikaelMayer commented Dec 10, 2021

View reviewed changes

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs Show resolved Hide resolved

MikaelMayer disabled auto-merge December 13, 2021 16:27

MikaelMayer and others added 2 commits December 13, 2021 10:28

Merge branch 'master' into ide-highlight-formals-and-declarations

7b75a8d

Added end tokens to expressions with bound variables.

c764c6c

Fail-safe but debuggable TryGetSymbolAt.

camrein reviewed Dec 15, 2021

View reviewed changes

MikaelMayer and others added 2 commits December 15, 2021 10:39

Merge branch 'master' into ide-highlight-formals-and-declarations

f906d80

MikaelMayer requested a review from camrein December 15, 2021 16:40

TryGetValue instead of ContainsKey and query

ebfbffc

camrein reviewed Dec 16, 2021

View reviewed changes

Source/DafnyLanguageServer/Language/Symbols/SymbolTable.cs Outdated Show resolved Hide resolved

List => IEnumerable, Where+Cast, ILogger<SymbolTable> first place,

d566628

MikaelMayer requested a review from camrein December 16, 2021 17:16

Fixed null logger

43054de

camrein reviewed Dec 17, 2021

View reviewed changes

keyboardDrummer reviewed Dec 17, 2021

View reviewed changes

MikaelMayer and others added 2 commits December 17, 2021 11:25

Fixed last PR review comments

84345ee

Merge branch 'master' into ide-highlight-formals-and-declarations

e7198a6

camrein approved these changes Dec 20, 2021

View reviewed changes

Merge branch 'master' into ide-highlight-formals-and-declarations

82fa861

MikaelMayer enabled auto-merge (squash) December 20, 2021 16:54

MikaelMayer merged commit 40db911 into master Dec 20, 2021

MikaelMayer deleted the ide-highlight-formals-and-declarations branch December 20, 2021 17:09

cpitclaudel reviewed Dec 20, 2021

View reviewed changes

camrein mentioned this pull request Jan 17, 2022

Parser crash on assert by { } true inside predicate dafny-lang/ide-vscode#118

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Provide formals and declarations type highlighting. #1630

feat: Provide formals and declarations type highlighting. #1630

MikaelMayer commented Dec 4, 2021 •

edited

Loading

camrein left a comment

camrein Dec 6, 2021

MikaelMayer commented Dec 6, 2021

MikaelMayer commented Dec 6, 2021

camrein commented Dec 7, 2021

MikaelMayer commented Dec 7, 2021

MikaelMayer commented Dec 8, 2021

camrein left a comment •

edited

Loading

MikaelMayer commented Dec 9, 2021

camrein left a comment

camrein left a comment

camrein left a comment

keyboardDrummer Dec 17, 2021

MikaelMayer Dec 17, 2021

keyboardDrummer Dec 17, 2021 •

edited

Loading

MikaelMayer Dec 20, 2021

MikaelMayer Dec 20, 2021

MikaelMayer Dec 20, 2021

cpitclaudel Dec 20, 2021 •

edited

Loading

keyboardDrummer Dec 20, 2021

MikaelMayer Dec 20, 2021

keyboardDrummer Dec 20, 2021

camrein commented Dec 20, 2021

cpitclaudel Dec 20, 2021

cpitclaudel Dec 20, 2021

feat: Provide formals and declarations type highlighting. #1630

feat: Provide formals and declarations type highlighting. #1630

Conversation

MikaelMayer commented Dec 4, 2021 • edited Loading

camrein left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Dec 6, 2021

MikaelMayer commented Dec 6, 2021

camrein commented Dec 7, 2021

MikaelMayer commented Dec 7, 2021

MikaelMayer commented Dec 8, 2021

camrein left a comment • edited Loading

Choose a reason for hiding this comment

MikaelMayer commented Dec 9, 2021

camrein left a comment

Choose a reason for hiding this comment

camrein left a comment

Choose a reason for hiding this comment

camrein left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 17, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel Dec 20, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

camrein commented Dec 20, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Dec 4, 2021 •

edited

Loading

camrein left a comment •

edited

Loading

keyboardDrummer Dec 17, 2021 •

edited

Loading

cpitclaudel Dec 20, 2021 •

edited

Loading