feat: support Find References LSP request

[alex-chew]

Fixes #2320.

• Implement basic functionality
• Add tests (WIP)
• Update release notes

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Probably resolved by adding implementing IHasUsages on more AST nodes, but we can fix that in another PR.

Relevant, I would like to change the way resolver is implemented so there's a stronger integration between the resolver and building the usage graph, so that if a usage if resolved then it automatically becomes available to the language server and there's no longer the possibility of forgetting to add IHasUsages

[alex-chew]

I think that's a good idea, and I agree that it would be better to address in another PR.

On a related note, it would be nice if the declaration graph were reflexive on declarations, i.e. GetDeclarations(myDecl.Position) would include myDecl itself. This seems moreintuitive to me, and it would also simplify the implementation of DafnyDefinitionHandler.Handle.

[keyboardDrummer]

I don't follow. Instead of GetDeclarations and DafnyDefinitionHandler.Handle, do you mean GetUsages and DafnyReferencesHandler.Handle ?

Note that LSP allows the client to request usages of a declaration that doesn't return the declaration itself:

[alex-chew]

Yes, I did mean GetUsages and DafnyReferencesHandle.Handle.

I'll implement support for includeDeclaration being false.

[keyboardDrummer]

I wonder whether find references on definitions that may be visible outside of the file, should be enabled when not in project mode, since it might cause too few results to be returned leading to confusion.

One option is to do the least amount of work, which is to have it be enabled as you have now, and then gather feedback from users.

The other option is to for each definition say whether it's local to the file or not, and only if it is to return references results outside of project mode.

What do you think we should do?

[alex-chew]

I think whether or not we return references of definitions outside of the current file, it will be true that (a) the list of references will be incomplete in the general case (and so users may be confused), and (b) we will want to somehow encourage users to adopt the project mode.

To address (b) I'll look into ways we can warn the users that results may be incomplete, and guide the users towards documentation on how to add an appropriate project file. But then under those circumstances, I'd rather give a "best effort" list of references, i.e. including some-but-maybe-not-all references/declarations outside the current file, rather than intentionally withholding them.

[keyboardDrummer]

For (b), I'm thinking of a notification that pops up whenever a file is opened that's not using project mode, that does include other files, and then ideally you could say "OK" or "OK and don't warn me again"

[keyboardDrummer]

This implementation doesn't respect request.context.includeDeclaration

[alex-chew]

(The force-push rebases this branch onto master.)

[keyboardDrummer]

Nit: I think it's easier to read tests if all the relevant code is in the test. Alternatives to this are either opening these files in memory, or writing them to disk in the test.

[keyboardDrummer]

Nit: I feel the method call implies what the comment says.

[keyboardDrummer]

Nit: I would move this and the next method to the bottom of the file, so the file is more callgraph topologically ordered.

[keyboardDrummer]

Nit: I would replace this with:

// The declaration graph is not reflexive, so the position might be on a declaration
FilePosition declarationPosition = declaration == null 
  ? new FilePosition(requestUri, request.Position) 
  : new FilePosition(declaration.Uri.ToUri(), declaration.Range.Start)

return state.SymbolTable.GetUsages(declarationPosition.Uri, declarationPosition.Position).ToArray();

[keyboardDrummer]

Looks great! Amazing