Since Val contains functions, its Show instance cannot be
derived in the usual way without exposing a non-standard Show
instance for (Val a -> Val a). Instead, we rely on the user to
provide a fitting instance, e.g. by importing Text.Show.Functions.
* Warning action about missing cache dir
* Add warning to executable
* Correct duplicate cacheName in getCacheFile
* Warn if dhall-haskell cache dir is not usable
* Improve warn message
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Correct plural
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Improve syntax
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Use runMaybeT to make 2 step warnings
* Add FlexibleContexts to make happy lts-6
* Catch IOException's when handling cache dir
This make the haskell impl follow the standard.
* Correct unwanted identantion
* Push warnings to get* wrapper functions
* Remove unnecessary lang extension
* Inline warnings in get* functions
* Being consistent with break lines
* Apply suggestions from code review
About phrasing, formatting, syntax, etc
Co-Authored-By: Gabriel Gonzalez <Gabriel439@gmail.com>
* doesPathExist is not in directory-1.2.2.0
* Make message fit in 80 cols
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1306
The following comment describe how this works in depth:
https://github.com/dhall-lang/dhall-haskell/issues/1129#issuecomment-532928798
The short explanation is that we can substantially speed up type-checking
by not substituting `let` expressions and instead adding the bound variable
to the context. This is the same as the type-checking "fast path" that
we had before adding dependent types, except this time it works even in the
presence of dependent types.
The main difference is that we add the `let`-bound type *and* value to the
context and use `Dhall.Eval.conv` to perform equivalence checking instead of
`Dhall.Core.judgmentallyEqual`.
* Add `--censor` flag support for censoring type errors
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1294
* Reuse `censorText`
... as caught by @sjakobi
* Remove `typeWith` refactor
... as caught by @sjakobi
This is a vestige of a refactor that I reverted incompletely
* Reuse `Dhall.Core.censorText` in `Dhall.Parser` module
... as suggested by @sjakobi
* Disable 1-field simplification by default
This builds on top of #1315 to minimize disruption by disabling the
breaking change by default and instead requiring the user to opt in
by setting a new `collapseSingletonRecords` option to `True`.
The additional tests added to verify this also caught a bug in the
`Interpret` instance for functions, which this change also fixes.
* Change to three-valued option
... based on feedback from @sjakobi
This change the option to a three-valued option:
* `Bare` - 1-field constructor does not include a nested record
* `Wrapped` - 1-field constructor always includes a nested record
* `Smart` - Named fields that don't begin with `_` include a nested record
The default is `Wrapped` (for backwards compatibility), but users will
probably want to eventually switch to `Smart`
* Don't depend on `fieldModifier` for determining if a field is anonymous
... as suggested by @sjakobi
* Refactor `Dhall.Eval`
This updates the style of `Dhall.Eval` to match the stylistic
and naming conventions of the rest of the `dhall` package.
* Import `Data.Set` fully qualified
... as suggested by @sjakobi
* Re-enable warnings
... as wished by @sjakobi
* Remove `{eval,conv,quote}E` synonyms
... as suggested by @sjakobi
* INLINE `qVar`
... literally
... as suggested by @sjakobi
* Remove unnecessary `MIN_VERSION_base(4,8,0)`
... as caught by @sjakobi
We still need `CPP` elsewhere within the same file, though
* Fix style of `vProjectByFields` function
... as caught by @sjakobi
* Simplify `Inject`/`Interpret` for 1-field records
Fixes https://github.com/dhall-lang/dhall-haskell/issues/346
Now a Haskell type like:
```haskell
data Example = Foo Bool | Bar Text
```
... corresponds to this Dhall type:
```dhall
{ Foo : Bool | Bar : Text }
```
* Fix documentation
* Add additional test cases
... as suggested by @sjakobi
* Test all permutations of:
* 0, 1, or 2 fields
* Fields of type `()` or `Double`
* Named or anonymous fields
To type-check and evaluate inputs in the context of previous
inputs, the repl constructs a let-expression that includes
the previous input and variable assignments as bindings.
Previously these bindings would also be annotated with
inferred types. For example a session like
⊢ Kind
⊢ "foo"
would be represented as
let it : Sort = Kind
in "foo"
However `Sort` does not typecheck as an annotation of a let-binding,
resulting in the confusing message
Error: ❰Sort❱ has no type, kind, or sort
Constructing the let-bindings without the type annotations fixes the
problem.
Fixes#1193.
Since some inferred types are in non-normal form, `dhall type`
would previously return types that weren't strictly
standard-conforming. This change prevents further confusion.
Closes#1300.
* Add `--censor` switch for disabling source code display
Related to #1294
This currently only affects parse errors, but can later be extended
to type errors, too
* Fix type blindiness
... as requested by @sjakobi
* Replace `Bool` with `Censor`
* Replace `Maybe FilePath` with `Input`
* Simplify recursive `Interpret` instance
Related to https://github.com/dhall-lang/dhall-haskell/issues/1297
The motivation behind this change is to:
* Remove the dependency on `free` and `distributive`
* Simplify the API and the implementation
* Fix `stack-lts-6` build
* Remove now-unused test files
... as caught by @sjakobi
When enabled, we handle protected imports as if the semantic cache was
empty:
* Protected imports are resolved again, downloaded or read from
the filesystem as necessary.
* Protected imports are β-normalized, not αβ-normalized.
* Protected imports are checked against their SHA256 hashes,
failing to resolve if they don't match.
Context:
https://github.com/dhall-lang/dhall-haskell/pull/1275#issuecomment-528847192
* Add a haddock to explain the various `Binding` fields.
* Add combinators to make dealing with `Binding` less awkward.
With all of the source information flying around, manually
deconstructing and reconstructing `Binding`s is a pain. These
combinators cover some very common cases.
* Use `bindingExprs` to simplify `subExpressions`.
* Use bindingExprs and chunkExprs to simplify another traversal.
Full coverage of all Expr constructors is now checked by the
type-checker. This revealed that that the IntegerToDouble, TextShow,
Some and None constructors were missing.
Also:
* Increase frequency for Lam, Pi and App
* Fix a few inconsistencies in normalization
* Remove some dead code in D.T.QuickCheck
Closes#1256.
* Change `dhall type` to resolve imports
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1277
The original motivation was that `dhall type` would represent a
type-inference-only phase. However, in practice that wasn't very useful
so `dhall type` now performs import resolution followed by type inference.
* Fix loading relative to root directory
... as caught by @sjakobi
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
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
* Small fixes to `dhall diff`
Related to https://github.com/dhall-lang/dhall-haskell/issues/1255
* Simplify function type diffs by omitting the bound variable name when possible
* Non-zero exit code when `dhall diff` is non-empty
Note that this is a breaking change to the `Dhall.Diff` API by changing the
exposed utilities to all expose the more general `Diff` type instead of a
`Doc`. This means that we also no longer need separate exports for
`diff` and `diffExpression`.
* Fix build failure for tests
* Fix golden test result
* Rename `diffExpression` to `diff`
... as suggested by @sjakobi
* Add test coverage for diffing function types
* Fix `Inject` instance for lists
Fixes#1254
This also adds tests for conversions back and forth between Dhall and
Haskell values
* Add `Inject` instances for `Scientific` and `String`
... so that we don't need to comment them out!
This is essentially the exact same problem and fix as #1213
Normally I would add a test, except that our test suite for diffs doesn't
yet support escape codes. However, the basic problem was the following
output:
```
$ dhall diff '"1"' '"2"'
- "…"
+ "…"
```
... which now displays (with color highlighting) this output:
```
$ dhall diff '"1"' '"2"'
"12" -- Imagine that the 1 is red and the 2 is green
```
* Improve HTTP errors
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1251
This improves HTTP error messages by:
* Expanding the set of recognized status codes
* Adding up to 7 lines of the response body
For example:
```
Error: Remote file missing
URL:
↳ https://httpbin.org/statu
Message:
1│ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
2│ <title>404 Not Found</title>
3│ <h1>Not Found</h1>
4│ <p>The requested URL was not found on the server. If you entered the URL manually please check your spelling and try again.</p>
```
* Always include HTTP status code in output
... as suggested by @sjakobi
* Use "not found" wording for 404 message
This is closer to the official wording for the error message
* Compress error message formatting
There's no need to put the URL and status code on separate lines since
they are compact
* [dhall format] Prefer unquoted URLs
This updates `dhall format` to prefer unquoted URLs.
I included the test cases described in #1109, but along the way I
discovered a standard bug so I have opened dhall-lang/dhall-lang#704 to
fix it. This change depends on that upstream fix.
Fixes#1109.
* pull in latest dhall-lang
* skip unimplemented tests
The new tests were introduced in dhall-lang/dhall-lang#698.
Also:
* Document shortcommings of Expr's Eq and Ord instances.
Haddock for GHC-7.10.3 can't handle haddocks on vanilla derived
instances, so we use StandaloneDeriving.
* Add explanation for skipped AssertNaN test
* Make equivalences of terms of different types fail during typechecking
This fixes the `EquivalenceNotSameType` test from
https://github.com/dhall-lang/dhall-lang/pull/698.
* s/assertion/equivalence
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1211
The original implementation of diffing two lists in #450 attempted to add a
special case in the logic for when the list had no common elements.
However, this led to a bug where the two lists would display different
if they were both empty.
lists would never render.
This change fixes that by removing the special case.
The new output for the linked example is:
```
Use "dhall --explain" for detailed errors
Error: Assertion failed
[ …
, - 1
, …
, + 55
]
16│ assert : fibs 10 ≡ [ 0, 1, 2, 3, 5, 8, 13, 21, 34, 55 ]
17│
(stdin):16:16
```
Previously, normalizing `Natural/subtract 0` would result in this
error:
⊢ Natural/subtract 0
Error: Compiler bug
An ill-typed expression was encountered during normalization.
Explanation: This error message means that there is a bug in the Dhall compiler.
You didn't do anything wrong, but if you would like to see this problem fixed
then you should report the bug at:
https://github.com/dhall-lang/dhall-haskell/issues
CallStack (from HasCallStack):
error, called at src/Dhall/Eval.hs:865:38 in dhall-1.25.0-FCOZ7uxqivz8dkVwuN7aED:Dhall.Eval
This updates the dhall-lang submodule to include a new testcase added
in https://github.com/dhall-lang/dhall-lang/pull/692.
* 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
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
