* Update `Dhall.Tutorial` module
This overhauls the `Dhall.Tutorial` module to reflect recent changes to
the language (and also to link to external documentation when possible).
* Fix doctests
* Rephrase import syntax caveat
... as suggested by @sjakobi
* Explain `<<<`
... as suggested by @sjakobi@
* Rephrase things
... as suggested by @sjakobi
* `s/The annotated/This/`
... as caught by @sjakobi
* Add commas to description of link to built-ins reference
... as caught by @sjakobi
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Remove paragraph describing role of Prelude
* Update dhall/src/Dhall/Tutorial.hs
... as suggested by @sjakobi
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Rename Interpret to FromDhall
The "Interpret" name remains in `InterpretOptions`, which are
actually used for marshalling in both directions.
* s/injectThenInterpretIsIdentity/embedThenExtractIsIdentity
* s/Inject/ToDhall
* s/shouldInjectInto*/shouldEmbedAs*
* Keep Interpret and Inject as constraint synonyms for compatibility
… as suggested by @Gabriel439.
* Move prefix out of renderSrc
This reduces the complexity of renderSrc slightly without affecting
anything else much.
* Make formatting of comments idempotent
Fixes#1413. Previously the formatter would insert an additional line
break before some comments whilst preserving existing line breaks. In
order to restore idempotent behaviour, we need to strip a leading
newline character from the comment string in those cases, if present.
* Test idempotency when formatting comments
Test case taken from @AJChapman's bug report (#1413).
* Change argument order of renderSrc
Reads a bit more idiomatic, as suggested by @sjakobi.
* [#1392] Injecting Data.Map
* injecting via Generic
* Explicit instance
* Cleanup code
* Minor code cleanup
* Property testing for Inject/Interpret
* Refactor test
* Adding TypeApplications to .cabal
* No more TypeApplications
* Simplified tests using extract
* Added test for Text amnf fixed Natural import
* Update dhall/dhall.cabal
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Update dhall/dhall.cabal
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
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
* [#1395] Marshalling Set and HashSet
* Update dhall/src/Dhall.hs
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Update dhall/src/Dhall.hs
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Added distinctList
* setFromDistinctList updates
* Doctests abour ordering
* both set and hashset can ignore or fail with duplicates
* Comments on instances
* Moved length computation deeper
* Little wibble
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Add support for leading separators
... as standardized in https://github.com/dhall-lang/dhall-lang/pull/755
Note that this does not yet change the formatter to use them
* Update `dhall-lang` submodule
* Fix `dhall.cabal` to mention new Prelude files
* Remove duplicate lines
* Resolves#1408: Add more detail in `--explain` when `toMap` has the wrong type.
Specifically, add common reason of using `{}` for record value.
For example,
``` shell
echo 'toMap {}' | ~/.local/bin/dhall
```
Outputs
> Error: ❰toMap❱ expects a record value
>
> Explanation: You can apply ❰toMap❱ to any homogenous record, like this:
>
>
> ┌─────────────────────────────────────────────────────────────────────┐
> │ let record = { one = 1, two = 2 }
> │
> │ in toMap record : List { mapKey : Text, mapValue : Natural}
> │
> └─────────────────────────────────────────────────────────────────────┘
>
>
> ... but the argument to ❰toMap❱ must be a record and not some other
> type.
>
> Some common reasons why you might get this error:
>
> ● You accidentally provide an empty record type instead of an empty
> record when
> using ❰toMap❱:
>
>
> ┌──────────┐
> │ toMap {} │
> └──────────┘
> ⇧
> This should be ❰{=}❱ instead
>
> ────────────────────────────────────────────────────────────────────────────────
>
> 1│ toMap {}
>
> (stdin):1:1
* Add type annotation to `toMap` suggestion.
* #1381 Word* to Natural
* Added instance for Word
* Got rid of linting issues
* Added docsets
* Added comments
* Revert Crypto to master version
* Spread the doctests
* Improve Docstring
This includes some simplifications/optimizations for the `ToTerm DhallDouble` instance.
Most notably we let `cborg` take care of the correct encoding of NaNs:
See `Codec.CBOR.Write.doubleMP`:
977c0c0820/cborg/src/Codec/CBOR/Write.hs (L571-L573)
merge-expressions with additional arguments are also formatted with
consistent indentation for all arguments. E.g.
merge
{ x = Natural/even }
< x >.x
1111111111111111111111111111111111111111111111111111111111
Fixes a small regression introduced in 7634ee7.
The loss of indentation for toMap and merge was due to
75e6cc5ca7. I have included Some for
consistency.
Fixes#1376.
Also improve format test failure messages
* Fix pretty-printing precedence of `toMap`
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1358
* Also correctly format `merge` expressions without a type annotation
... as suggested by @sjakobi
* Add test for formatting "function-like" expressions
This verifies that the code correctly handles `toMap` expressions with
type annotations as @sjakobi was asking about
… as standardized in https://github.com/dhall-lang/dhall-lang/pull/745.
This also adds proper error handling for the free variable case
discussed in https://github.com/dhall-lang/dhall-lang/issues/749:
Sample output for the MergeHandlerFreeVar test case:
Error: Disallowed handler type
Explanation: You can ❰merge❱ the alternatives of a union using a record with one
handler per alternative, like this:
┌─────────────────────────────────────────────────────────────────┐
│ let union = < Left : Natural | Right : Bool >.Left 2 │
│ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
│ in merge handlers union : Bool │
└─────────────────────────────────────────────────────────────────┘
... but the output type of a handler may not depend on the input value.
For example, the following expression is not valid:
Invalid: The output type is ❰Optional A❱, which references the input
value ❰A❱.
⇩
┌──────────────────────────────────────────┐
│ merge { x = None } (< x : Type >.x Bool) │
└──────────────────────────────────────────┘
Your handler for the following alternative:
↳ x
... has type:
↳ ∀(A : Type) → Optional A
... where the output type:
↳ Optional A
... references the handler's input value:
↳ A
────────────────────────────────────────────────────────────────────────────────
1│ merge { x = None } (<x: Type>.x Bool)
dhall/dhall-lang/tests/type-inference/failure/unit/MergeHandlerFreeVar.dhall:1:1
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
