Add async API for F* IDE requests

[gebner]

Currently the F* IDE interface is handled by sending requests and separately registering global handlers for responses. This approach makes it awkward/impossible to wait for the response in async LSP handlers.

A cleaner API would be to have a request function on FStarConnection that returns a promise. This would also make it trivial to define well-typed functions for the various requests:

class FStarConnection {
  async request(query: string, args: any): Promise<any> { ... }

  async lookupQuery(position: Position, word: string, range: FStarRange): Promise<IdeSymbol> {
    const res = this.request('lookup', { symbol: word, ... });
    if (res.status == 'failure') throw new Exception(res.response);
    return res.response;
  }
}

Implementation-wise, this basically requires a Map<string, Promise> field in FStarConnection (going from query id to unfulfilled promise). The response handler would then look up the query id of the response and fulfill the promise if successful, or fail it otherwise with an exception derived from the error message.

Unfortunately, the F* IDE protocol doesn't follow the neat request-response scheme:

• Some requests---like full-buffer and co.---return multiple response messages. But push is a special case anyhow.
• The lookup request sometimes returns no response at all, which means we might need to add a timeout there. (The comment says "behavior for the vscode mode"....)
• I don't know how request cancellation works exactly, this might also result in dropped responses.

See also #20 (comment)

[gebner]

Another issue with the current approach is that we need to guess what type the response is. We have heuristics like "if the response is an array, then it's a autocomplete response." This is clearly neither scalable, nor particularly robust.

With the async request approach, we don't need to guess what kind of response a message from the server is. We just resume execution in the code that made this particular request (as determined by the query id), and there we can reasonably assume that response is a valid response to this particular request. (For example, a response to a symbol request is either an error or an IdeSymbol.)

[klinvill]

• The lookup request sometimes returns no response at all, which means we might need to add a timeout there. (The comment says "behavior for the vscode mode"....)

@nikswamy it looks like this behavior (where a failed lookup sends an error message for the emacs version and not for the vscode version) is just an artifact of the emacs version evolving. In that case, is there any reason not to also have an error message returned for the vscode version as well (assuming the vscode extension is written to handle a failure message in that case)?

[klinvill]

• Some requests---like push and co.---return multiple response messages. But push is a special case anyhow.

It looks like the vscode extension doesn't issue push queries, so we should be ok for now. But even so, the push queries return a single query response message from F* that just has multiple responses within its response field right? In that case, could we just have the promise return an array of responses? So it would look something kind of like:

async pushQuery(code: String, line: number, column: number): Promise<PushResponse[]> {
...
}

[nikswamy]

We could send a response for failed lookups. I don't see a problem with that.

We send full-buffer queries. F* chunks the buffer into fragments and responds with several messages, one for each fragment until the first failing fragment. The series of messages ends with a full-buffer-finished. I wanted this to be several messages, since it takes a while to check each fragment and this allows us to display progress in the IDE while the suffix of the buffer is still being checked, rather than waiting to get the full array of responses before displaying anything.

[gebner]

It looks like the vscode extension doesn't issue push queries, so we should be ok for now. But even so, the push queries return a single query response message from F* that just has multiple responses within its response field right?

Oops, I got that request name wrong. Thanks for noticing that. It's full-buffer like Nik said. Under the hood full-buffer is implemented using push, hence the confusion.

Fortunately, I think it's the only request that returns a stream of responses. So as I said, we can just special case it.

[klinvill]

F* chunks the buffer into fragments and responds with several messages, one for each fragment until the first failing fragment. The series of messages ends with a full-buffer-finished.

Ah ok, thanks for correcting my understanding! Since there's a definitive end to the series of messages (full-buffer-finished) we should be able to return a new promise for the next chunk once we've received a non-final chunk. So maybe a signature kind of like:

type partialQueryResult = Promise<[IdeProgress, partialQueryResult | undefined]>;

async fullBufferQuery(code: String): partialQueryResult {
...
}

Alternatively maybe we could have the promise return a Stream

[gebner]

I don't know how request cancellation works exactly, this might also result in dropped responses.

I've read through the F* IDE code and I think I understand it now. There a couple of protocol requirements for the full-buffer request:

1. Cancellation is only supported while full-buffer is running, the cancel notification is ignored at all other times.
2. No request should be sent while full-buffer is running, otherwise cancellation does not work.

We don't try to ensure either of those in the VS Code extension right now. Fortunately, all other requests are processed completely serially.