Commit Graph

11 Commits

Author SHA1 Message Date
Frederik Ramcke
2cd4ed948f dhall-lsp-server: Improve type-on-hover behaviour over binders (#1062)
* Improve type-on-hover behaviour over binders

Dhall's parser does not generate `Src` annotations for the names in
binders, which means that it's not quite as straight-forward to check
whether the user meant to hover over it and see its type as one would
hope. As a result, the current "naive" implementation sometimes behaves
slightly unintuitively and returns the type of the entire expression,
rather than the type of the bound variable. E.g.
  let x = 2 in "text"
      ~
would result in the type `Text` being displayed, rather than `Natural`
as one would expect. Since the language server also marks the expression
whose type is being displayed, the behaviour isn't quite that bad in
practice (we aren't falsely led to believe that `x` has type `Text`).

This change recovers the `Src` information describing the bound variable
names and handles those cases in a way that should be more in line with
the expectations of the user.

* Fix exprAt not handling multi-lets correctly

* Fix merge left-overs
2019-07-06 23:17:52 +00:00
Frederik Ramcke
53e1967754
dhall-lsp-server: Normalize types before displaying them to the user (#1060)
* Normalize types before displaying them to the user

Previously, the type displayed when hovering over the arrow in a lambda
(or forall) binder would not always be normal, e.g.
  \(n : {Left = Natural, Right = Natural}.Left) -> n + n
                                                ~
would result in
  forall (n : {Left = Natural, Right = Natural}.Left) -> Natural
being displayed.

The (expected) normal type would be:
  forall (n : Natural) -> Natural

This fix normalises types before displaying them to the user (fixes both
the type-on-hover and annotate-let behaviour).

* Move normalisation from typeAt' to typeAt

This way we only have to worry about it one place, rather than  in each
clause of `typeAt'`.
2019-07-05 03:58:44 +00:00
Frederik Ramcke
3a120d277f
Change rangeFromDhall to exclude trailing whitespace (#1046)
This gets rid of the separate `santiseRange` utility function that we
used to exclude trailing whitespace from source code ranges. As a result
of this change, we no longer have to carry around the original source
code everywhere to be able to santise ranges after the fact.
2019-07-03 09:25:24 +00:00
Frederik Ramcke
41161aa390
dhall-lsp-server: Implement caching (#1040)
* Rewriting Dhall.LSP.Backend.Dhall: Implement new API

The old "backend" consisted of a random collection of ways to invoke
Dhall:
- runDhall :: FilePath -> Text -> IO (Expr Src X)
- runDhallSafe :: FilePath -> Text -> IO (Maybe (Expr Src X))
- loadDhallExprSafe :: FilePath -> Text -> IO (Maybe (Expr Src X))

The new backend exposes a slightly more though-out API. This also lays
the foundation for performance improvements in the dhall lsp server via
caching.

* Reorder code in Dhall.LSP.Backend.Dhall

* Remove unused constructor

* Rewrite and document Backend.Formatting

* Refactor Dhall.LSP.Backend.Linting

* Refactor Dhall.LSP.Backend.ToJSON

* Adapt Diagnostics backend to the new Dhall API

* Remove old Dhall backend API

* Implement caching; revamp LSP frontend

This commit implements caching of Dhall expressions: we only need to
fetch, typecheck and normalise each import once per session, unless they
change! This means that `dhall-lsp-server` is now viable for non-trivial
Dhall projects, for example probing around in `dhall-nethack` everything
feels near-instantaneous once the imports have been resolved.

This implementation currently has a bug: we don't invalidate imports
transitively, i.e. if A.dhall loads B.dhall and B.dhall changes we do
not discard the cached version of A.dhall. This should be reasonably
easy to fix given some time with Dhall's import graph. Furthermore,
there is some cleaning up left to do:
  - Fix warnings
  - Reorganise things in a less ad-hoc way
  - Make the code a bit prettier

* Fix caching of errors

* Use `bimap` instead of `first` and `second`

* Re-export `Dhall.lint` rather than aliasing

Rids us of some boilderplate

* Use MVar instead of TVar for server state

The main benefit is that we get to use `modifyMVar_` which does updating
of the shared state for us (and gracefully handles any uncaught
exceptions).

* Don't invalidate hashed imports

Fixes a misinterpretation on my end of the correct behaviour regarding
the caching of imports. Quoting @Gabriel439:

> A hashed import is valid indefinitely once it is successfully
> resolved, even when the underlying import later becomes broken. That's
> why missing sha256:… works so long as the cache has that import cached
> (and this behavior is part of the standard).

* Cleanup Dhall.LSP.Backend.Dhall a little bit

* Add note about fixing cache invalidation

* Use TemplateHaskell to generate state lenses

* Make types of `typeAt` and `annotateLet` more expressive

Both assume the input to be well-typed; by using `WellTyped` rather than
`Expr Src X` as the type of their input we can make this explicit.

This change exposed a bug (also fixed in this commit) in the
type-on-hover functionality: we run `typeAt` only if the input was
well-typed _the last time we checked it_ (which was at the last save);
this means that if the code changed without being written to disk we
would happily try to normalise (in `typeAt`) non-well-typed code...

* Fix type of typecheck

Typecheck returned the well-typed _type_ of a given expression, while I
was assuming it would certify the input to be well-typed. Silly indeed.

* Remove `checkDhall` from Dhall.Backend.Diagnostics

Removes the left-over stub from the change to the new Dhall backend.

* Update comments and remove TODO note

* Remove superfluous parentheses

* Simplify MonadState code via lens combinators

* Use `guard` instead of matching on True

* Remove more superfluous parentheses
2019-07-01 17:30:32 +00:00
Frederik Ramcke
8d4aa0320e dhall-lsp-server: Correctly handle dependent lets (#1018)
While I do believe the previous version to be correct as well, this
certainly makes it easier to reason about it.
2019-06-22 09:35:52 -07:00
Frederik Ramcke
dc5f70011d dhall-lsp-server: (new feature) annotate lets (#1014) 2019-06-20 09:37:59 -07:00
Frederik Ramcke
66833cbfa5
dhall-lsp-server: Type on hover (#1008)
* Type on Hover 1/2: Backend

Adds a function typeAt that, given an annotated expression and a text
position finds the type of the subexpression at that position.

* Type on Hover 2/2: Frontend

Exposes the new type-on-hover functionality as part of the hover
handler.

* Simplify explainDiagnosis

As suggested by @Gabriel439

* Simplify `inside`

Adressing @Gabriel439's comment.

* Simplify typeAt' by assuming well-typedness

* Simply srcAt

Use choice operator `<|>` instead of case distinction
2019-06-17 10:37:38 +00:00
Frederik Ramcke
bed87530b5 dhall-lsp-server: Towards implementing a "convert to JSON" command (#1005)
At the moment the VSCode plugin contains a hacked-together prototype of
a dhall-to-json (and -to-yaml) preview feature. We should ultimately
move that kind of functionality to dhall-lsp-server to 1) minimise the
amount of VSCode specific code and 2) avoid having to work with and fix
bugs in typescript code ;)

This commit takes us most of the way there; what is missing is the
ability to create files (via a WorkspaceEditRequest), which is not yet
implemented by haskell-lsp-types. I will wait with exposing the
corresponding command (and removing the existing preview code) in
vscode-dhall-lsp-server until this is fixed upstream.
2019-06-13 07:23:48 -07:00
Frederik Ramcke
af4ccc9db9 dhall-lsp-server: Implement linter diagnostics and "Lint and Format" command (#1003)
* Refactor Dhall.LSP.Backend.Formatting

Exposes `formatExpr :: Text -> Expr a Import -> Text` that can be reused
in the lintAndFormat command.

* Implement linting backend in Dhall.LSP.Backend.Linting

Exposes `suggest :: Eq a => Expr Src a -> [Suggestion]` and
`lintAndFormatDocument :: Text -> Either ParseError Text`.

* Fix unusedBindings

* Implement linter diagnostics

* Improve linting diagnostic ranges

In VSCode we now mark the "let" following a superfluous "in".
  let a = 0 in let b = a in b
               ~
Previously we got
  let a = 0 in let b = a in b
  ~
which was slightly confusing

* Implement executeCommand handler for "Lint and Format"

This exposes the command "dhall.server.lint", which should be called
from the vscode plugin to lint and format the current dhall file. Needs
a correspondingly patched vscode-dhall-lsp-server (branch lint).
2019-06-11 08:10:16 -07:00
Frederik Ramcke
05f4d5cd1e dhall-lsp-server: Use LSP VFS rather than disk IO (#994)
* Remove dummy LSP handlers

* Publish diagnostics directly

So far we were using haskell-lsp's diagnostics infrastructure.
haskell-lsp is geared towards plugin-based language servers like
haskell-ide-engine, which means that their approach to handling
diagnostics (on a per-plugin basis) doesn't really fit our use-case.
This commit changes our diagnostics implementation to send
protocol-level messages directly, rather than going through haskell-lsp.

* Refactor diagnostics handler

Reduce clutter and clean up Dhall.LSP.Handlers.Diagnostics a bit.

* Remove unused import

* Don't flush diagnostics on file close

The LSP protocol does not expect (or require) us to flush diagnostics at
any point. This change doesn't have any user-visible impact (since we
recompute diagnostics on file open anyway).

* Use LSP VFS instead of disk IO

Rather than reading the files from disk each time, we now simply query
haskell-lsp's "virtual file system". This also allows us to check code
before it has been saved (though we do not implement this).
2019-06-07 20:48:42 -07:00
Frederik Ramcke
dfee2fbbca
Simplify dhall-lsp-server and reorganise its modules (#992)
* Clean up dhall-lsp-server's Main.hs

Also adds haddock comments.

* Remove TODO comment

The comment talks about adding a mechanism for protocol-level logging to
dhall-lsp-server. Since the VSCode LSP implementation has this feature
already baked in on the client side, we don't have to implement it
ourselves.

* Simplify dhall-lsp-server's infrastructure

So far we had a system where we set up the LSP message handlers to relay
messages to a separate dispatcher thread via a shared channel. Since our
language server is at the same time designed in a completely synchronous
manner, this complication turns out to be unnecessary.

* Remove sample code

* Fix unused variable warning

* Reorganise dhall-lsp-server's module hierarchy

Prefixes all modules with "Dhall.LSP.".

Previously:
  Backend.Dhall.
               .Diagnostics
               .Formatting
  LSP.
     .Handlers
     .Handlers.
              .Diagnostics
              .DocumentFormatting
              .Server

Now:
  Dhall.LSP.
           .Backend.
                   .Diagnostics
                   .Formatting
           .Handlers
           .Handlers.
                    .Diagnostics
                    .DocumentFormatting
           .Server

* Make dhall-lsp-server tests compile again

They still fail though!
2019-06-07 07:47:07 +00:00