Feat: Code action support

[MikaelMayer]

This PR introduces the DafnyLanguageServer support for QuickFixes, which are a kind of code actions, restricted to same-file edits.

• The class QuickFixer in dafny plugins only requires a plugin instantiation to implement the method public abstract QuickFix[] GetQuickFixes(IQuickFixInput input, IToken selection); (the current selection is passed as a token).
• QuickFix have a title and a lazily computed list of text edits.
• IQuickFixInput notably contains the code and the last program.

I make use of this class in DafnyLanguageServer in the file DafnyCodeActionHandler, with two major functions called Handle, one is for returning a list of title + data to identity the command, the other is for resolving the code action to concrete edits.

I included 1 battery:

• A built-in starter plugin VerificationQuickFixer in its own file, which can currently inline a failing postcondition when there is no return statement, in method bodies only. It also work in nested blocks.

This PR includes tests with a unified representation of code, designated hover space with >>> and expected insertion with [[message|insertedText]] that should be pretty straightforward to understand and to maintain.

It also includes a test where a plugin provides quick fixes to ensure plugins can correctly provide this functionality.

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

[keyboardDrummer]

Could you reduce indentation of the remaining code by inverting the condition and returning early?

[keyboardDrummer]

I think the intention of the CodeAction API is to use the field command or edit to define what happens when a user triggers the action, so here you could have

Command = new Command(fixWithId.QuickFix.Title, "dafnyCodeAction", new JArray(documentUri, fixWithId.Id))

Instead of the Data field

[MikaelMayer]

I'm not sure about what you mean.
The code that handles the code action is this one:

public override Task<CodeAction> Handle(CodeAction request..., which explicitly requires an unresolved code action. So I don't understand why I should send a command?

[keyboardDrummer]

I'm saying you could return a CodeAction that includes a Command instead of one that includes Data, since this seems how the API is intended to be used. From the documentation:

A CodeAction must set either edit and/or a command. If both are supplied, the edit is applied first, then the command is executed.

[MikaelMayer]

Looks like the documentation of the API is incomplete. Although what you say works well theoretically, it has the side-effect that it creates an error in VSCode.

And that's what I thought: Code actions can either give edits on the text or more general actions.
However, the API documentation you describe don't talk about the construction of code actions which is two phases, which I've seen while browing the code online

1. Creation of the code action with possible data attached
2. Resolution of the code action when it's being clicked.

In 1) there is no need to create an edit or a command if all the edits and commands are going to be computed on 2.

As a conclusion, adding a "command" would require us to change the VSCode extension to support this command, which would have to manually invoke the code action resolver... which would be useless and hard to maintain
So I'm going to revert my changes there and just use the regular data field which is there for this purpose - the data between code action creation and code action resolution.

[keyboardDrummer]

As a conclusion, adding a "command" would require us to change the VSCode extension to support this command, which would have to manually invoke the code action resolver... which would be useless and hard to maintain

That indeed seems bad.

OK, let's keep this as it is. Thanks for trying.

[keyboardDrummer]

Newline here seems unneeded

[keyboardDrummer]

Given that this API only supports actions whose edits span a single file, is the idea to start with this API and evolve it over time?

[MikaelMayer]

Yes, we could add a field Uri to this down the road, so now we can start with this simpler API.

[keyboardDrummer]

One of the fields of a CodeAction is diagnostics, and filling this field causes the code action to show up grouped under the diagnostic in the Problems view. The code action provided by VerificationQuickFixer relates to a diagnostic, so shouldn't we connect those two using the API ?

[keyboardDrummer]

Why not use DafnyDocument instead of this?

[MikaelMayer]

I prefer to have an interface for the API rather than a concrete implementation that might be evolving.

Also, for a suitable API, we don't want to expose plugin developers with more information than necessary, do we?

[keyboardDrummer]

To me the name ..Input doesn't tell me much about what to expect from this interface. I think ICompilation or IDocumentCompilation is more telling, since it contains information collected during compilation, such as the AST and diagnostics.

[MikaelMayer]

Interesting point of view!
I think the convention in C# is to usually name interfaces in what purpose they serve, not about how they are implemented. A document compilation (report?) would seem like an implementation detail.
So let's keep this naming for now.

[keyboardDrummer]

What's Verification doing in the name here?

Why don't we use DafnyDocument to implement IDafnyCodeActionInput ?

[MikaelMayer]

Verification is obsolete. It dates from the time when I had the quick fixer be defined in Dafny core instead of DafnyLanguageServer
I renamed it DafnyCodeActionInput. And what do you mean by your question? This class uses DafnyDocument to implement IDafnyCodeActionInput (which is the interface plugins implementers are going to work with)

[keyboardDrummer]

To me a name ending in Input is a code smell.

When I read a function signature SomeFunction(SomeFunctionInput x) then the name SomeFunctionInput doesn't give me more information than what the rest of the function signature already did. What I'd like to know is what information can I get from x, and the name of the type of x should help with that.

Instead of IDafnyCodeActionInput, I think something like IResolvedCompilation or IResolvedDocument would tell me better what information I can get from it. If it's resolved then I expect that I can get the document text, the document AST, and the resolved types.

I think the convention in C# is to usually name interfaces in what purpose they serve, not about how they are implemented. A document compilation (report?) would seem like an implementation detail.

Do you feel the names I suggested reveal unnecessary information?

[keyboardDrummer]

This call will only happen when the user places their caret on a line with a verification diagnostic.

How come? Code actions are available on lines without diagnostics, are they not?

[keyboardDrummer]

This call still seems like an O(N) operation. Why don't you get a DocumentTextBuffer from IDafnyCodeActionInput and let DocumentTextBuffer store a mapping from line to index that can be used to extract text using a Range in constant time?

[MikaelMayer]

How come? Code actions are available on lines without diagnostics, are they not?

Not every code action requires extracting some substring of the code all the time. If no code action is returned, or a code action is returned that does not call this particular method, then this line is not called. I won't go into more details as I removed this call.

This call still seems like an O(N) operation. Why don't you get a DocumentTextBuffer from IDafnyCodeActionInput and let DocumentTextBuffer store a mapping from line to index that can be used to extract text using a Range in constant time?

Well, it's a O(N*C) where C is the number of code actions and N is the size of the file, and C is expected to be very small, so I wouldn't have worried about it.
However, I implemented such a conversion in the implementation DafnyCodeActionInput, so that the interface can expose the method Extract, and I removed the three ToToken methods that were converting relative positions to absolute positions.

[keyboardDrummer]

Consider having record DafnyCodeAction(string Title, Container<Diagnostic> Diagnostics, Func<DafnyCodeActionEdit[]> GetEdits) instead of the current InstantDafnyCodeAction and DafnyCodeAction.

[MikaelMayer]

I would like to avoid this, since I know some implementers of code actions in F# and since it's an abstract class, they would need to implement boilerplate methods such as clone, copy, etc.
But even if you make it concrete, I'm not sure how the Func<> interfaces which are C# specific would translate to F#. So, let's avoid the complexity and keep the API as simple as possible.

[keyboardDrummer]

I think it might be good to take some time to agree on what language we're writing the API for. You seem to have settled on a particular style of API that sits between what is idiomatic for C# and F#, while I'm still trying to optimise for C#.

My reasoning is that if you want to have great APIs, you will need two APIs anyways, one for C# and one for F#, and if you start with a mixed API now you'll have to still create both idiomatic APIs later, while if you start with a C# optimised one now, you'll only have to add the F# one later. Secondly, for now, most of our API consumption will be from the dafny-lang/dafny codebase, which is only C#.

The mixed API approach seems great if that's also what you plan on ending up with, which makes sense if you want to reduce the API maintenance cost by having only 1 for both C# and F#. However, investing in idiomatic APIs seems worth the effort to me.

---

In this particular case, wouldn't record DafnyCodeAction(string Title, Container<Diagnostic> Diagnostics, Func<DafnyCodeActionEdit[]> GetEdits) work well for F# as well, since there is no abstract class, and F# can use a lambda expression for the GetEdits argument?

Relevant: https://stackoverflow.com/a/3239179/93197

[keyboardDrummer]

This can return an IEnumerable<DafnyCodeActionEdit>. Generally in C#, IEnumerable is used whenever a collection is required, and this is only changed when performance requires something else. In this case, returning an array does not improve performance over returning an IEnumerable, so the latter is preferred.

Regardless of C# conventions, returning an IEnumerable here gives more flexibility to the API users, without downsides.

[MikaelMayer]

without downsides.

It forces API users to link to the library System.Collection.Generic (I have to add one more import to the file as well). I can't call this "without downside".
Nevertheless, I did as you suggested.

[keyboardDrummer]

It forces API users to link to the library System.Collection.Generic

But that's part of the .NET framework is it not? Any C# application will use that namespace. Does this relate to C# vs F#?

[keyboardDrummer]

I don't think this linear time complexity method should exist. We can add an Extract(Range range) to DocumentTextBuffer though.

[keyboardDrummer]

I find the API of DafnyCodeActionHelpers.GetInformationToInsertAtEndOfBlock hard to understand. How about something like

static class RefactorTools {

  public DafnyCodeActionEdit? InsertBlockAtReturnLocation(
    DocumentTextBuffer text, 
    Range returnLocationRange,
    IEnumerable<string> statementsToInsert)

}

?

[MikaelMayer]

Thanks for this refactoring suggestion, I applied it.
Note that I only need one statement to insert. For multiple statement, it's sufficient to call this function repeatedly and store the edits in the same order, because this is how they are going to be applied.

[keyboardDrummer]

In the long run, I imagine we might want to provide a different API for creating refactorings in Dafny, one that doesn't require thinking about formatting.

Here's a bad example:

Edit AddStatementToEnd(method: DafnyMethod) {
  var original = method.Snapshot();
  method.Body = method.Body.Concat(new SomeStatement(..));
  Formatter.Format(method);
  return DiffEngine.ComputeEdit(original, method);
}

I'm sure Roslyn has some interesting APIs for this very same purpose. I'd be great if we could get familiar with them, although I imagine it's quite a learning curve.

Here's an example: https://github.com/dotnet/roslyn/blob/main/src/Analyzers/CSharp/CodeFixes/MisplacedUsingDirectives/MisplacedUsingDirectivesCodeFixProvider.cs

With test: https://github.com/dotnet/roslyn/blob/main/src/Analyzers/CSharp/Tests/MisplacedUsingDirectives/MisplacedUsingDirectivesCodeFixProviderTests.cs

[MikaelMayer]

Yes yes ! That's also part of what I envision we will be able to do with the Dafny formater.
In any case, in the short-term after this PR, we will need to handle expressions, substitutions, etc. So formatting them might be a good idea.

[keyboardDrummer]

Ok,

Just want us and our users to be aware that the API might still change (a lot)

[atomb]

Yeah, I hope we can move toward AST-based rewrites relatively soon. All this string processing makes me nervous.

[keyboardDrummer]

Why not pass a Position openingBrace instead of a line and col ?

[MikaelMayer]

Because we need to compare the line and the column to a lot of tokens, and Position is offset by tokens by 1, so we would be computing unnecessary affine transformations all the time.
This is a private method anyway, we can always upgrade this later.

[keyboardDrummer]

This seems like a slow approach to find the end token. Your program might have 10k methods so we should avoid traversing over all of them. I think something like the IIntervalTree used here, or a position directed search like here would be better since both are O(logN) instead of O(N) complexity.

[MikaelMayer]

I agree we should do a better job at indexing the program to access various definitions, as we get more and more features about navigation.
For this PR, implementing a tree system is out of scope, because the verification completion plugin is a toy example and is meant to evolve; to avoid traversing the body of 10k methods, I added a check about line numbers, so that it will be very fast. I think that's the best reasonable we should aim at for now if we want this PR to be merged.

[atomb]

This looks like it's in pretty good shape. Thanks! I requested a few changes, but they should be pretty quick.

[atomb]

Given that you changed DafnyCodeActionProvider to return an IEnumerable, would it make sense to do so here, too? If you don't do that, I think you could instead remove using System.Collections.Generic above.

[MikaelMayer]

Good suggestion. For consistency with the original Dafny.Plugins.PluginConfiguration that returns Compiler[] and Rewriter[], I prefer to keep returning an array here. So I removed using System.Collections.Generic

[atomb]

Is this no longer true?

[MikaelMayer]

Yes, this is no longer true. Plugins can write to stdout now, and this information is recorded in a log file.

dafny/Source/DafnyLanguageServer/Program.cs

Lines 30 to 32 in 1472e40

	// Prevent any other parts of the language server to actually write to standard output.
	await using var logWriter = new LogWriter();
	Console.SetOut(logWriter);

[atomb]

I don't see logic in here related to whether there's a return keyword or not. I'm not sure it's necessary to have that, but I'd update the comment to match the code.

[MikaelMayer]

I rephrased it to

/// For now, it offers to inline a failing postcondition if its failure is
/// indicated on the '{' -- meaning there is no explicit return.

[atomb]

Could you update this to start with a summary of what the method does?

[atomb]

I'm not sure I understand what's happening here. Does this do anything different from line 150?

[MikaelMayer]

Ahah interesting ! the code there used to be

      var result = Document.Errors.GetDiagnostics(Document.Uri).ToArray();
      if (result.Length == 0) {
        // For anonymous documents opened in VSCode
        result = Document.Errors.GetDiagnostics(DocumentUri).ToArray();
      }

so that it would handle separatedly the document URI for anonymous documents. However, since the recent refactorings, and the fact that URI are universally used, the case split is no longer user. Thanks for pointing out.

[atomb]

Yeah, I hope we can move toward AST-based rewrites relatively soon. All this string processing makes me nervous.

[MikaelMayer]

Yeah, I hope we can move toward AST-based rewrites relatively soon. All this string processing makes me nervous.

Me too. It's just that, with the guarantee that we don't need to replace variables for inlining postconditions, we should be fine. But with the PR of the formatter, we'll have access to tokens, so this will be even easier to print things (and indent them correctly!)

[atomb]

Looks good!