* Use foldl' over foldl
As suggested by @sjakobi. Germans banding together in the fight against
laziness!
* Add missing foldl' imports
* Ups, forgot one!
* Fix hacked-together parsers
Back when we changed the linter to preserve let comments we made
whitespace parsing explicit (previously combinators swallowed any
trailing whitespace), but we forgot to update the hacked-together
parsers used by the LSP server. As a result, various convenience
features broke, but that's easy enough to fix.
* Fix 'annotate lets' and 'type on hover' features
Both features only work as intended if as much of the Dhall code as
possible is wrapped in Note annotations, since we use that to figure out
where the user was pointing. Since the removal of explicit multi-lets in
the syntax the parser no longer wraps immediately nested lets (i.e.
multilets) in Notes, which means we need to split them manually (like we
used to).
* Fix hovering test
Now the behaviour expected by the test matches what we would want in
reality.
This raises the lower bound on prettyprinter to 1.5.1 since
`removeTrailingWhitespace` is buggy in earlier versions.
This jailbreaks hnix, which isn't compatible with prettyprinter-1.5.1 yet.
Fixes#183, #1400, #1525.
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
* Add config support
The config so far consists of a single `asciiOnly` flag (whose intended
behaviour is not yet implemented).
* Implement 'ascii-only' option when formatting and linting
This commit adds functionality to the 'asciiOnly' flag, i.e. when turned
on we don't output fancy non-ascii characters. Needs a recent version of
the client to function -- the version on the marketplace does not relay
configuration data to the server yet!
This causes text literals to be formatted as multi-line strings
whenever they contain at least one newline and at least one non-newline
character. "Spacers" like `"\n\n"` continue be formatted as single-line
strings. If the heuristic turns out to be too eager to choose a
multi-line layout, we can refine it later.
This partially addresses #1496.
Also
* update some variable names
* use 80-column "smart" layout consistently
This is preparatory work for #1454.
This also fixes some cases where dhall would previously accept
malformatted inputs.
The changes to dhall-lsp-server are mostly untested. See #1510.
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
... by not going through a `Term` intermediate
This gives a ~28% performance in decoding improvement, which means that
cache looks are not faster.
Here are the new decoding benchmarks before and after this change:
Before:
```
benchmarked Issue #108/Binary
time 266.5 μs (265.7 μs .. 267.4 μs)
1.000 R² (1.000 R² .. 1.000 R²)
mean 266.3 μs (265.6 μs .. 267.1 μs)
std dev 2.418 μs (1.891 μs .. 3.436 μs)
benchmarking Kubernetes/Binary ... took 36.94 s, total 56 iterations
benchmarked Kubernetes/Binary
time 641.3 ms (623.0 ms .. 655.4 ms)
0.999 R² (0.997 R² .. 1.000 R²)
mean 679.7 ms (665.5 ms .. 702.6 ms)
std dev 29.48 ms (14.15 ms .. 39.05 ms)
```
After:
```
benchmarked Issue #108/Binary
time 282.2 μs (279.6 μs .. 284.7 μs)
1.000 R² (0.999 R² .. 1.000 R²)
mean 281.9 μs (280.7 μs .. 287.7 μs)
std dev 7.089 μs (2.550 μs .. 15.44 μs)
variance introduced by outliers: 11% (moderately inflated)
benchmarking Kubernetes/Binary ... took 27.57 s, total 56 iterations
benchmarked Kubernetes/Binary
time 499.1 ms (488.1 ms .. 506.6 ms)
0.999 R² (0.998 R² .. 1.000 R²)
mean 498.9 ms (494.4 ms .. 503.9 ms)
std dev 8.539 ms (6.236 ms .. 12.56 ms)
```
There's a slight performance regression for the decoding microbenchmark, but
in practice my testing on real examples matches performance improvements seen
in the larger benchmark based on an example cache product from
`dhall-kubernetes`.
Note that is a breaking change because:
* There is no longer a `FromTerm` nor `ToTerm` class. Now we use the
`Serialise` class and `{encode,decode}Expression` now work on `ByteString`s
instead of `Term`s
* I further narrowed the types of several encoding/decoding utilites to expect a
`Void` for the first type parameter of `Expr`
* This is a regression with respect to stripping 55799 CBOR tags, mainly
because properly handling the tags at every possible point in the syntax tree
would considerably complicate the code
* dhall-lsp-server: Fix lower bound on dhall
… as reported in https://github.com/dhall-lang/dhall-haskell/issues/1494.
* Require base >= 4.11
Previously there were build failures with GHC-8.2 and 8.0 due to `(<>)` being out of scope.
* Improve parsing error messages
The main changes are:
* Don't quote expected tokens in the error message (to avoid visual clutter)
* Consolidate expected tokens into simpler categories (e.g. "operator" or
"literal") instead of listing them all
For example, this would be an error message before this change:
```
$ dhall <<< '1 + [1'
dhall:
Error: Invalid input
(stdin):2:1:
|
2 | <empty line>
| ^
unexpected end of input
expecting "!=", "&&", "++", "->", "//", "//\\", "/\", "==", "===", "merge", "toMap", "||", "→", "∧", "≡", "⩓", "⫽", '#', '(', '*', '+', ',', '.', ':', '?', ']', built-in expression, double infinity, double literal, import, integer literal, label, list literal, natural literal, record type or literal, text literal, union type, or whitespace
```
... and this would be an error message after this change:
```
$ dhall <<< '1 + [1'
dhall:
Error: Invalid input
(stdin):1:4:
|
1 | 1 + [1
| ^^^^
unexpected " [1<newline>"
expecting (, import, keyword, label, or literal
```
* Fix test failures
* Fix warnings
This updates the `dhall` package to have 100% haddock coverage and
also updates CI to enforce this going forward.
This also includes a change to deprecate the `X` type synonym, which
I noticed along the way
* Functional tests setup for the LSP server
* Add nix derivation for lsp-test-0.6.1.0
* Register fixture files
* Enable functional tests on appveyor
* Attempt to fix Position errors
* Fix `dhall-lsp-server` to specify a UTF8 locale
Related to https://github.com/dhall-lang/dhall-haskell/issues/1356#issuecomment-536840612
* Specify utf8 encoding for tests
* Add test for hovering functionality
* Add glob to list fixture files
* Remove extra do
Closes#1185.
This mostly reverts "Add support for multi-`let` (#675)" /
8a5bfaa3b9.
Also:
* Add fields for Src
This is useful for to make 'Note's less noisy during debugging:
first srcText expr
Previously, hovering over any part of a non-dependent function type like
`Bool -> Bool` would result in the type of the domain being displayed
(`Bool` in this example). The correct type is `Type`.
This bug resulted from the fact that we
expected all functions types to be syntactically of the form
`forall (b : Bool) -> Bool`, disregarding the simpler syntax for the
non-dependent function space (which desugars to
`forall (_ : Bool) -> Bool`).
* Remove superfluous language extensions
* Remove use of ScopedTypeVariables
In order to make the code more accessible it makes sense to refrain from
using ScopedTypeVariables, which we only used in two places.
* Remove use of LambdaCase extension
* Correctly handle dependent types in dhall-lsp-server
Removes the "fast path" when typechecking `let`s whose bound expression
has a small type. This optimisation is no longer legal in the presence
of dependent types (as introduced in #1164).
* Fix bad merge
* Remove redundant import
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
* Clean up dhall-lsp-server.cabal
Removes unused dependencies.
* Upgrade to haskell-lsp-0.15.0.0
The stackage LTS version is still 0.8.2 so we need to add this as an
'extra-dep'.
* Display type information as plaintext rather than markdown
* Fix nix build
* Update nix haskell-lsp-types
* 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
Gabriel Gonzalez
Simon Jakobi
Frederik Ramcke
Basile Henry
Sergei Dolgov
mujx
quasicomputational
Ollie Charles
Fabrizio Ferrai
Mario