simonhorlick / kind-vscode

A language server protocol implementation and vscode plugin for the Formality programming language.

kind-vscode

A Visual Studio Code plugin for the Kind programming language. This plugin provides output from the kind typechecker to VSCode.

Architecture

This extension is structured as three pieces:

• A vscode extension that launches kind-lsp
• A language server, kind-lsp, that's written in node and contains the state
• A set of functions for computing results, written in Kind.

Structure

.
├── client // Language Client
│   ├── src
│   │   ├── test // End to End tests for Language Client / Server
│   │   └── extension.ts // Language Client entry point
├── package.json // The extension manifest.
└── server // Language Server
    └── src
        └── server.ts // Language Server entry point

Getting Started

To install all of the necessary dependencies, run

npm install

In VSCode there is a launch configuration named "Launch Client" that will start an instance of VSCode with the plugin enabled.

Roadmap

The following features are planned:

• Hover over a symbol to view its documentation
• Jump to definition
• Autocompletion
• Rename symbol
• Support for other editors, for example: Atom, vim

kind-vscode's Issues

Create architecture document

Outline how the various pieces talk to each other.

vscode <> extension <> lsp server (javascript) <> formality (compiled to javascript)

Make parser more robust in the face of syntax errors

The extension doesn't provide useful information if there is a syntax error anywhere in the file.

Messages from holes contain shell colour codes

To get an example, write ?hole- somewhere. There will be un-printable characters where the colour codes are.

Show documentation when hovering over functions

One key feature of the language server is to support contextual information via hovering over code. It's useful for developers to not only be able to see the types that a function deals with, but also it's documentation.

When hovering over String.flatten below:

      let str = String.flatten([err, "\n", hig]);

The user should be able to see something like:

String.flatten(xs: List(String)): String

flatten takes a List of Strings and concatenates them into a single String.

Fix correctness issue with reverse dependencies

If a term is changed in the editor we must re-check those terms that depend on it.

Show inferred types on hover

In the below screenshot, if a user hovers over b we should display its inferred type - i.e. Pair(Nat, String).

Watch the filesystem for changes to files

If files change on the filesystem, the language server should re-check those files. This can happen if the file is edited outside of the editor or if a tool like git modifies the files.

This plugin should rely on the lsp client to watch for changes via the workspace/didChangeWatchedFiles message.

Case auto-completion

It would be great to insert the branches of a case statement while typing. For example

Example.show(obj: JSON): String
  case obj {

should auto-fill the following:

Example.show(obj: JSON): String
  case obj {
    null:
    bool:
    number:
    string:
    array:
    object:
  }

Context-aware autocompletion

The extension should present a list of variables that are provided by the current context while typing.

Error in hello world

Make goals interactive

In that case it may be useful to make the numbers that appear when you write a ?hole, clickable... Then this number would be written automatically in the file and compiled again... Do you think it is possible to make something like this?

Handle deletion of source files

Currently this causes things to break. For example:

(node:53366) UnhandledPromiseRejectionWarning: Error: ENOENT: no such file or directory, open '/Users/simon/src/github.com/moonad/Kind/base/Fmt/motive2.kind'
(node:53366) UnhandledPromiseRejectionWarning: Unhandled promise rejection. This error originated either by throwing inside of an async function without a catch block, or by rejecting a promise which was not handled with .catch(). To terminate the node process on unhandled promise rejection, use the CLI flag `--unhandled-rejections=strict` (see https://nodejs.org/api/cli.html#cli_unhandled_rejections_mode). (rejection id: 1)
(node:53366) [DEP0018] DeprecationWarning: Unhandled promise rejections are deprecated. In the future, promise rejections that are not handled will terminate the Node.js process with a non-zero exit code.
TypeError: Cannot read property 'positionAt' of undefined
    at /Users/simon/src/github.com/simonhorlick/formality-vscode/server/out/fm.js:30:33
    at Array.map (<anonymous>)
    at lspResponseToDiagnostics (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/out/fm.js:27:16)
    at Object.computeDiagnostics (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/out/fm.js:61:29)
    at /Users/simon/src/github.com/simonhorlick/formality-vscode/server/out/server.js:104:23
    at CallbackList.invoke (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/node_modules/vscode-jsonrpc/lib/events.js:62:39)
    at Emitter.fire (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/node_modules/vscode-jsonrpc/lib/events.js:121:36)
    at /Users/simon/src/github.com/simonhorlick/formality-vscode/server/node_modules/vscode-languageserver/lib/main.js:171:38
    at handleNotification (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/node_modules/vscode-jsonrpc/lib/main.js:502:43)
    at processMessageQueue (/Users/simon/src/github.com/simonhorlick/formality-vscode/server/node_modules/vscode-jsonrpc/lib/main.js:273:17)

Add support for semantic tokens

We can expose semantic information about the source code via the https://microsoft.github.io/language-server-protocol/specification#textDocument_semanticTokens message. This would allow us to re-use the actual parser and not have to maintain separate regular expressions for highlighting.

One possible downside of this is that the Formality parser doesn't provide recovery from syntax errors - so files with bad syntax won't have any highlighting.

Add support for the Language Server Index Format (LSIF)

This allows offline (without an LSP) code intelligence. This gives the ability to show hover and jump-to-definition information in a web browser.

Checks don't always agree with the kind cli

There shouldn't be any difference, but, for example base/Fmt/sprintf.kind does not check with the cli tool, but does with the extension. Similarly base/Nat/add/cancel_left.kind doesn't check with the extension, but does with the cli tool.

Provide visual feedback when the extension is busy

During the initial type check there's no feedback in the UI, so it doesn't appear that anything is happening.

Expose parse errors to the UI

Show parse errors as diagnostics.

Make goals produce warnings

Goals are currently displayed as errors - make them warnings.

Goals do not contain a source location

Any messages from goals appear at the top of the file rather than the place the goal appears. It should appear inline with the goal definition.