* Fix `yaml-to-dhall` support for empty objects
`yaml-to-dhall` was decoding an empty object into:
```dhall
[] : { mapKey : Text, mapValue : Text }
```
... instead of:
```dhall
[] : List { mapKey : Text, mapValue : Text }
```
... which this change fixes
* Add missing test files
* Hopefully fix test failure on Windows
I suspect that the test failure is due to the locale for the test suite
not being set to UTF8
* 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
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Try to cache the extra-deps from stack-lts-6.yaml
* Limit `stack bench` to the dhall package
For some reason `stack bench` triggers a rebuild of _all_ the local
packages, which we don't need.
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
```
* 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
You can now _increase_ the number of QuickCheck tests with
the --quickcheck-tests CLI option, e.g.
cabal test dhall:tasty --test-options "--quickcheck-tests 1000000"
* This might fix a syntax problem:
https://www.appveyor.com/docs/build-cache/#configuring-cache-items
says:
Note the use of single quotes around the entire line, when
environment variables are used.
* This adds the AppVeyor config to the files which invalidate the cache
when changed.
Context: #1063.
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.
* Fix `--version` flag handling for `dhall-json` package
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1198
This changes version to be a separate constructor for options parsing,
in order to make invalid states unrepresentable and to fix issues like
the above one.
* Undo `allowImports` changed
This was a change I forgot to stash while working on the fix for the
`--version` flag
* Fix missing `Paths_dhall_json` in `dhall-json.cabal`
* 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
…to fix build failures due to the submodule pointing at an unreachable commit.
* Disable a currently failing testcase.
* Update the extra-source-files in dhall.cabal.
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.
This adds a new `--records-loose` flag and changes the default behavior
to `--records-strict`
The rationale for this change is so that this default behavior helps
more when users are still experimenting with the appropriate type to
use to decode a large and messy YAML file.
For example, suppose a user is trying to translate the following YAML
to Dhall:
```yaml
foo: 1
bar: true
```
... and they start with a empty Dhall type which they plan to fix in
response to error messages. They'd get a surprising success:
```bash
$ yaml-to-dhall '{}' < ./example.yaml
{=}
```
... because the old default behavior is to ignore extra fields in the
YAML. However, if we're strict by default then users don't have to
apply the `--records-strict` flag to get feedback on what they need
to change.
* Make it no buildable in windows as suggested by @sjakobi
* Use last lts resolver for ghc-8.6.5
* Remove unused stack yaml file
* Use default stack yaml
Note that `dhall-nix` cannot be built on Windows due to its transitive
dependency on the `unix` package.
Also:
* Nix: Enable `-Werror` for `dhall-nix`
* Add support for `toMap` in `dhall-nix`:
\(x : { a : Bool }) -> toMap x
is translated as
x:
(kvs:
map (k:
{
mapKey = k;
mapValue = builtins.getAttr k kvs;
}) (builtins.attrNames kvs)) x
* 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`
From dhall/tests/Dhall/Test/Regression.hs:
These two examples contain the following expression that loops
infinitely if you normalize the expression before type-checking the
expression:
(λ(x : A) → x x) (λ(x : A) → x x)
The problem is typechecking that snipped already fails even before we
hit the self-application with the following error:
Unbound variable: A
This is fixed by quantifying over `A`, resulting in the desired type
error:
Error: Not a function
1│ x x
