Previously the annotated type would have too many line-breaks, e.g. when
the result of annotating
let id = \(A : Type) -> \(a : A) -> a
was
let id : ∀ ( A
: Type
)
→ ∀ ( a
: A
)
→ A = \(A : Type) -> \(a : A) -> a
while it should be
let id : ∀(A : Type) → ∀(a : A) → A = \(A : Type) -> \(a : A) -> a
This restricts the clickable link part of an import to just the actual
link; previously we also underline hash and headers if those were
present.
Now:
./Bool/package.dhall sha256:7ee950e7c2142be5923f76d00263e536b71d96cb9c190d7743c1679501ddeb0a
~~~~~~~~~~~~~~~~~~~~
Previously:
./Bool/package.dhall sha256:7ee950e7c2142be5923f76d00263e536b71d96cb9c190d7743c1679501ddeb0a
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Implement completion support
Completes the following:
- environment variables
- local imports
- identifiers in scope (as well as built-ins)
- record projections
- union constructors
* Add support for general dependent types
Removes the non-dependent let path. Needed since #1164 added support for
general dependent types.
* Remove unused import
* Use monad instance to cast between `Expr Src _`
As suggested by @Gabriel439: Use `typeOf (do _ <- expr; holeExpr)`
instead of `fmap undefined expr`. In the absence of `Embed` constructors
(in this case `Import`s) the two are equivalent.
* Simplify completeFromContext
Caught by @Gabriel439
* Remove debug code
* Add 1s timeout to listDirectory call
As pointed out by @Gabriel439, listDirectory can be a potentially
expensive operation. Adding a timeout should improve the user
experience.
* Fix unclean merge
* Remove Dhall.X and replace with Data.Void
This commit removes the Dhall.X module and the Dhall.X.X type,
preferring the use of Data.Void.Void. As I'm sure a lot of people are
actually using X, I've added a type-alias type X = Void. However,
pattern matching on X would be a breaking change.
Fixes#1120.
* Restore unsafeCoerce
* Fix regression
* Unused
* Reorganise exports
* Fix dhall-nix
* Another fix
* Fix Dhall.LSP.Backend.Typing
* Fix dhall-bash
* Remove most uses of `StandardVersion` from the API
We no longer support multiple versions of the standard, except for
supporting old integrity checks, so this change removes all inessential
uses of `StandardVersion` from the API and command-line interface.
* Fix `dhall-lsp-server` build
* Load imports recursively
This is the big change that enables us to implement 'semi-semantic'
caching.
* Use `throwM` instead of `liftIO . throwIO`
* Fix build with __GHCJS__
* Fix exceptions in Dhall.Import
* Fix dhall-lsp-server
* Revert exception behaviour on typecheck errors
This is one for a separate pull request!
* Make sure loadImportFresh returns alpha-normal expression
As caught by @Gabriel439, `loadImportFresh` violated the invariant that
`ImportSemantics` should be alpha-beta-normal. This fix also means that
we don't have to alpha-normalise again in `loadImportWithSemanticCache`.
* Remove old comment
* Fix regression test for issue 216
Turns out the test was testing the wrong thing, because it was
pretty-printing an import. This worked previously because when importing
uncached expressions we would not alpha-normalise them.
* Restore `dhall freeze` bevhaviour
Newly frozen imports should also be present in the cache.
* Implement dhall.freezeImport and dhall.freezeAllImports
* Remove old (broken) test suite
* Rename `relativePosition` to `subtractPosition`
as suggested by @Gabriel439
* Add doctest for `subtractPosition`
as suggested by @Gabriel439
* Simplify getImportHashPosition
As spotted by @Gabriel439
* Use `forM` instead of `mapM` for prettier code
As suggested by @Gabriel439
* Fix misleading comment
* Add `Chained` type to capture fully chained imports
Until now we used `Import` two mean two different things:
- The syntactic construct; e.g. `./a.dhall` corresponds to the following
AST:
```
Embed
(Import
(ImportHashed Nothing (Local Here (Directory ["."]) "a.dhall"))
Code)
```
- The physical location the import is pointing to, computed by
'chaining' the syntactical import with the the 'physical' parent import.
For example the syntactic import `./a.dhall` might actually refer to the
remote file `http://host/directory/a.dhall`.
This commit adds a `Chained` newtype on top of `Import` to make this
distinction explicit at type level.
* Use `HTTPHeaders` alias for binary headers
I claim that `HTTPHeaders` is more readable and informative than the
unfolded type `(CI ByteString, ByteString)`.
* Typecheck and normalise http headers earlier
Previously we would typecheck and normalise http headers in
`exprFromImport`, i.e. while loading the import. This commit adds the
invariant that any headers in 'Chained' imports are already typechecked
and normalised, and moves this step into `loadWith` accordingly.
This causes a subtle difference in behaviour when importing remote files
with headers `as Location`: previously, nonsensical expressions like
`http://a using 0 0 as Location` were valid, while they would now cause
a type error.
* Fix dhall-lsp-server
* Fix Dhall.Import API regarding `Chained` imports
Do not expose the `Chained` constructor; we don't want external code
breaking our invariants! Also further clarifies the comment describing
the `Chained` type.
* Fix dhall-lsp-server
Since we are no longer able to construct `Chained` imports directly we
need to export a few additional helper functions from Dhall.Import.
Furthermore, since VSCode (and presumably the other editors out there
implementing the LSP protocol) does not support opening remote files
anyway we can get rid of some complications by dropping support for
remote files entirely on the back-end.
* Generalise decodeExpression, fixes TODO
* Fix tests
* Fix benchmarks
* Remove Travis cache for `~/.local/bin`
* Fix copy-pasted comment
Thanks to @Gabriel439 for spotting this!
* Add clarifying comment to `toHeaders`
* Expose `localToPath` in Dhall.Import
Also modifies `localToPath` to return a relative path if the input was
relative, rather than resolving relative paths by appending the current
directory.
* Turn imports into clickable links
This implements a handler for 'Document Link' requests. As a result,
imports are now clickable!
* Recover original behaviour
* Move "Dot" import graph generation to Dhall.Main
Previously `Dhall.Import` would generate the import graph in "dot"
format while resolving imports. This change simplifies `Dhall.Import` to
only keep track of the adjacency list representing the import graph,
moving the logic for generating "dot" files to Dhall.Main.
This change will allow us to implement proper cache invalidation for
`dhall-lsp-server`.
* Correctly invalidate transitive dependencies
Fixes dhall-lsp-server`s caching behaviour to correctly invalidate
cached imports that (possibly indirectly) depend on the changed file.
Example:
Suppose we have the following three files:
{- In A.dhall -} 2 : ./B.dhall
{- In B.dhall -} ./C.dhall
{- In C.dhall -} Natural
Previously, changing C.dhall to `Text` would not cause `A.dhall` to stop
type-checking, since the old version of `B.dhall` (which evaluated to
`Natural`) would still have been in the cache. This change fixes that
behaviour.
* Make edges of import graph self-documenting
As suggested by @Gabriel439
* Don't cache expressions manually
After computing the diagnostics for a given file we added its normal
form to the cache, but forgot to add its dependencies to the dependency
graph. This bug points out that keeping the import graph consistent
manually is probably not a good idea. With this commit we never mess
with the import cache manually; this means that files are only cached
once they are depended upon by some other file, potentially causing us
to duplicate work (but no more than once).
* Fix left-overs from previous commit
* 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
* 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'`.
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.
* 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
* 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
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.
* 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).
* 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!
