Several failed remote import messages didn't include the URL that
the interpreter failed to resolve. This change fixes that and includes
some slight tweaks to improve consistency in how the messages are
formatted.
* 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
The motivation for this is two-fold:
* To get rid of the standard version from the output
Currently it's just "None", which could be fixed, but keeping it up to
date is error-prone, so I prefer to just remove it.
* To make the output machine-readable
Example:
```
$ dhall version
1.24.0
```
The motivation for this change is to avoid α-normalizing all imported
expressions.
For example, before this change you would get the following behavior
beginning with an empty cache
```
$ cat ./example.dhall
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(_ : Type) → _
```
The reason why is that the current code α-normalizes all imported
expressions, even when returning them fresh.
To fix this, I changed the `ImportSemantics` type to not require that
expressions are α-normalized. Instead, the α-normalization only
happens at the last minute when interacting with the semantic cache, but
nowhere else.
I figured that this change would also be fine from the perspective of
the semi-semantic cache because false-negatives for this cache are
fine. In particular, we probably don't mind if we get a cache miss for
the semi-semantic cache if the user renames a variable.
After this change imports are no longer α-normalized, whether loaded
from a hot or cold cache:
```
$ cat ./example.dhall
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(a : Type) → a
```
* Allow customization of remote import resolution
Makes the `Status` type more general; previously support for
`Network.HTTP.Client` was hardcoded. In short:
```
data Status = Status
{ _stack :: NonEmpty Chained
[...]
-- , _manager :: Maybe Dynamic
-- -- importing the same expression twice with different values
++ , _remote :: URL -> StateT Status IO Data.Text.Text
++ -- ^ The remote resolver, fetches the content at the given URL.
[...]
}
```
* Simplify and expose `toHeaders`
`toHeaders` will be needed for mock http testing
* Fix compilation without `with-http` flag
* Fix compilation with `with-http` flag
* Fix tests without `with-http` flag
Implements a mock http client that handles requests to:
- `https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/`
- `https://test.dhall-lang.org/Bool/package.dhall`
- `https://httpbin.org/user-agent`
This allows tests involving remote imports to succeed even when compiled
without the `with-http` flag.
* Build `dhall` with HTTP support compiled out in CI
... to prevent regressions from occurring in the future
* Tag ImportSemantics with their semantic hashes
This is in preparation for semi-semantic caching.
* Collect the list of imports during import resolution
The final step needed in preparation for semi-semantic caching!
* Implement semi-semantic caching
This completes the implementation of the "semi-semantic caching"
proposal (issue #1098).
We compute the semi-semantic hash of a dhall import/file/expression as
follows:
- Parse the input;
- compute the semantic hashes of all imports referenced in the AST, i.e.
the hashes of their normal forms;
- compute the syntactic hash of the input (hashing the parsed AST);
- concatenate the syntactic hash of the input with the semantic hashes
of its imports and hash the result.
The "semi-semantic" cache (normal forms, indexed by semi-semantic
hashes) has the following properties:
- For a given input we can quickly find out if it is in the cache: we
only need to parse the input – we don't need to typecheck or normalise
it!
- The cache stays consistent, that is, we don't need to ‘invalidate’ old
cache entries if their dependencies change!
* Simplify semi-semantic hash
As suggested by @Gabriel439.
* Simplify code
We don't actually need to carry the list of imports around when loading.
* Restore `load`
* Fix `isNormalized` test
The test in question failed intermittently because `isNormalized` is
more thorough than `normalize`, in the sense that it throws exceptions
for more non-welltyped expressions. As a result, we need to use `spoon`
not just when computing the normal form of a raw expression, but also
when calling `isNormalized` on the result. Note that the test may still
randomly fail in the future, because normalizing non-welltyped
expressions needn't terminate!
* Comment on non-totality of `isNormalized`
Previously, `BAD="0 0" dhall <<< "env:BAD ? 0"` resulted in the
following error:
```
↳ env:BAD
Error: Not a function
1│ 0 0
BAD:1:1
```
According to the standard the above expression was supposed to evaluate
successfully to `0`. See #1146 for further discussion.
* 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.
* Forbid invalid codepoints
... as standardized in https://github.com/dhall-lang/dhall-lang/pull/640
* Don't validate code points outside of escape sequences
... as suggested by @sjakobi
It's not necessary (since the `text` package forbids invalid UTF8) and
slows down performance as verified by the `dhall-parser` comment parsing
benchmarks
* Restore `nonCharacter` parsing test
Previously, ill-typed expressions like this one got into normalization:
toMap {=} : <>.x
Also:
* Tweak Expr's Arbitrary instance:
- Boring nullary constructors don't need to be so frequent.
- Large NaturalLits can cause normalization to OOM, which we don't
want when running the testsuite.
* Add property test to check that all well-typed expressions can be
normalized.
* 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
* Check normalizeWithM for consistency with normalize
* Implements constant folding of Natural/fold applications normalizeWithM.
* Changes the Arbitrary Var instance to generate only non-negative indices.
Otherwise failures like this one would pop up:
normalizeWithM should be consistent with normalize: FAIL (8.51s)
*** Failed! Falsified (after 318133 tests and 6 shrinks):
Let (Binding {variable = "", annotation = Nothing, value = List} :| []) (Var (V "" (-1)))
Var (V "" (-1)) /= Var (V "" (-2))
Use --quickcheck-replay=180244 to reproduce.
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1114.
* QuickCheck tests: Specialize the 'natural' Gen to Naturals
Previously it could produce about any number, not just non-negative
ones.
To be more precise (citing the haddocks):
Given a well-typed expression e, (isNormalized e) is equivalent to
(e == normalize e).
Given an ill-typed expression, isNormalized may return True or False.
An even closer correspondence between isNormalized and 'normalize' is
currently tricky to achieve as 'normalize' returns errors only for some
ill-typed expressions. Once 'normalize' is more principled in this
regard, isNormalized could be changed to return a (Maybe Bool).
This re-enables a property test checking this consistency. Since
'normalize' returns errors for some ill-typed expressions, we
catch have to catch these, which requires an NFData for Expr.
* 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`
It is not the case that
canonicalize (a <> b) = canonicalize a <> canonicalize b.
For example
canonicalize (Directory ["asd"] <> Directory [".."])
= Directory [],
but
canonicalize (Directory ["asd"]) <> canonicalize (Directory [".."])
= Directory ["..", "asd"].
The law we want instead is:
canonicalize (a <> b)
= canonicalize (canonicalize a <> canonicalize b)
* 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
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1082
All of the successes are due to accepting expressions that would not
have been produced by a compliant encoder, such as:
* Expressions that use a variable name of `_` that could have been
encoded more compactly
* An expression tagged as a `Natural` number storing a negative number
* An expression encoding a function appled to 0 arguments
Fixes#973
The formatter was behaving inconsistently for multi-line strings
depending on whether or not they were at the top level or nested as
a subexpression. For example, the same multi-line string would be
rendered in multi-line form if it was at the top level and rendered
compactly if nested within another expression.
The root cause was that the pretty-printing logic was missing a top-level
`Pretty.group` call (which is the function responsible for enabling
compact representations if they fit), which this change fixes.
While benchmarking the example from #769 I saw that a significant
amount of time was spent benchmarking record literals. When I looked
at the code more closely I saw that the first key in the record literal
was being type-checked twice (once to figure out the record's associated
type-checking constant and once as part of the `process` loop).
This change fixes that, which speeds up interpretation of the large
example by 9%:
Before:
```
time 18.13 s (18.11 s .. 18.16 s)
1.000 R² (1.000 R² .. 1.000 R²)
mean 18.09 s (18.07 s .. 18.11 s)
std dev 21.92 ms (10.66 ms .. 29.76 ms)
variance introduced by outliers: 19% (moderately inflated)
```
After:
```
time 16.53 s (16.49 s .. 16.60 s)
1.000 R² (1.000 R² .. 1.000 R²)
mean 16.59 s (16.56 s .. 16.64 s)
std dev 43.65 ms (6.227 ms .. 56.35 ms)
variance introduced by outliers: 19% (moderately inflated)
```
Related to: https://github.com/dhall-lang/dhall-haskell/issues/1039
We'll probably never see indices that exceed the space of an `Int` and
the interpreter would probably not be able to handle 9223372036854775807
nested binders anyway.
This reduces the runtime of the `deep-nested-large-record` benchmark by about 50%.
Note that previously, contrary to its name and documentation, this function traversed a Dhall.Map in insertion order due to its use of Dhall.Map.toList! With this change, the traversal is changed to ascending key order.
Also:
- Fix the deep-nested-large-record benchmark
- Remove the map-operations benchmark: This benchmark actually reports a ~20% loss of performance for the unorderedTraverseWithKey_ change. Since we eventually care about dhall's performance we it's better not to be mislead by a questionable micro-benchmark.
This separates the source from the line numbers using vertical bars
instead of colons. The main reason for this is to more clearly
delimit the two and to also prevent the old colon from being confused
as a type annotation.
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1025
There were two error constructors related to invalid field types:
* `InvalidField`: for field types whose types were invalid type-checking
constants
* `InvalidFieldType`: for all other invalid field types
As @sjakobi noted, there are no invalid field types for the former
category, so we can remove that category of error entirely.
Note that `InvalidField` was still being used in a few places, but each
of those uses should actually have been using `InvalidFieldType`
instead, which this change also fixes.
This improves the error message when users attempt to apply `merge` to only
one argument, as suggested by:
https://github.com/dhall-lang/dhall-lang/issues/106#issuecomment-503523358
For example:
```
$ dhall <<< 'merge { Foo = True }'
Error: Invalid input
(stdin):2:1:
|
2 | <empty line>
| ^
unexpected end of input
expecting '.', second argument to ❰merge❱, or whitespace
```
`dhall diff` slightly misbehaves when diffing the following expression with
itself:
```dhall
λ(f : List Bool -> Bool) → f ([] : List Bool)
```
... producing the following diff:
```
λ(… : …
→ …)
→ …@…
- [ … ] : List …
+ [ … ] : List …
```
This is because there are two places in the `Dhall.Diff` module responsible
for comparing lists:
* Once in `diffApplicationExpression`, which compares two lists with at least
one type annotation between them
* Once in `diffPrimitiveExpression`, which compares two lists if neither one has
a type annotation
Those cases exhaustively cover all possible pairs of lists, but there was a
third (incorrect) fallback case that prematurely gave up and displayed them as
different. This fallback would trigger when applying a function to an empty
list, since the diffing algorithm wouldn't have a chance to return back to the
top-level `diffExpression` and try to compare the lists correctly in
`diffApplicationExpression`.
After this change, the diff now doesn't include a spurious difference:
```
λ(… : …
→ …)
→ …@…
…
```
The `--file` option was essentially broken since it passed in the
file path instead of the directory, meaning that transitive imports
would not be computed correctly (they'd be off by one path component).
* Find unused bindings inside nested lets
The removeUnusedBindings rule only matches the first bound variable in a
nested let block (of the form "let ... let ... in ..."). This means that
so far the linter missed cases like
let a = 0 let b = 0 in a.
This simple fix unfolds all let blocks (syntactically this means
inserting `in's everywhere) before applying the linting rules; the
LetInLet rule folds everything back together in the end. Applied to the
example from above we now return the correct result,
let a = 0 in a.
* Rewrite `lint` in a more explicit style; add comments
* Don't export implementation details
* Fix `freeIn` to correctly handle de Briujn indices
Previously we had "x@0" `freeIn` "x@1" == True (but "x@1" `freeIn` "x@0"
== False). The fix is to use subst instead of shift to change
occurrences of the given variable.
* Fix `removeUnusedBindings` to update de Bruijn indices
Whenever we remove an unused binding we need to update any references to
variables outside the let block, so that
let a = 0 let a = 0 in a@1
gets correctly rewritten into
let a = 0 in a (a = a@0)
instead of
let a = 0 let a = 0 in a@1
~> let a = 0 in a@1
~> a@1
Fixes https://github.com/dhall-lang/dhall-lang/issues/579
`Natural/fold` was misbehaving on GHCJS due to the use of `Natural`
arithmetic (for some reason). This is a problem I've seen and fixed
before, but needed to be fixed again after the migration to the new
`Dhall.Eval` normalization engine.
The fix is easy: use `Integer` instead of `Natural` for the accumulator
of the fold and the bug disappears.
Part of https://github.com/dhall-lang/dhall-lang/issues/563
This flag freezes imports in the same way as the Prelude by providing a
fallback unprotected import without an integrity check. The primary use
case for this is caching imports with a graceful fallback, which is why
the flag is named `--cache`
As Dhall's bounds don't allow base 4.13, this doesn't actually affect
anyone running in a supported configuration (i.e., without
--allow-newer). Further note that base 4.13 (i.e., GHC 8.8) isn't
tested in CI at present.
This could well be the last GHC 8.8-related change needed to
code (bounds will definitely need to be adjusted). In this case, a
Dhall release with relaxed bounds will suffice to finish off GHC 8.8
support.
However, it's also possible that dependencies might bundle together
breaking changes with 8.8 support, in which case adaptations will
still need to be made.
Fixes https://github.com/dhall-lang/dhall-haskell/issues/882
This allows users to supply the Dhall expression by path instead of via
standard input. This also ensures that transitive imports are resolved
appropriately relative to the file's path.
In other words, instead of this:
```
$ dhall <<< './foo/bar.dhall'
```
Users can now do:
```
$ dhall --file foo/bar.dhall
```