diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,44 @@ +1.35.0 + +* [Supports version 18.0.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v18.0.0) + * [Implement more efficient `with` desugaring](https://github.com/dhall-lang/dhall-haskell/pull/1993) + * Chained `with` expressions will now be much more efficient +* [BREAKING CHANGE TO THE API: Preserve whitespace for `Lam` constructor](https://github.com/dhall-lang/dhall-haskell/pull/1980) + * This change extends the `Lam` constructor to preserve whitespace around + the variable binding + * The motivation for this change is to enable `dhall-docs` to support + jumping to definitions + * You can replace your existing `Lam` constructors with + `Dhall.Core.makeFunctionBinding` +* [BREAKING CHANGE TO THE API: Preserve whitespace for `Field` constructors](https://github.com/dhall-lang/dhall-haskell/pull/1991) + * This change extends the `Field` constructor to preserve whitespace around + the selected field + * The motivation for this change is to enable `dhall-docs` to support + jumping to definitions + * You can use `Dhall.Core.makeFieldSelection` and + `Dhall.Core.fieldSelectionLabel` to convert between the detailed and the + simple representation of the selected field. +* [Add `FromDhall` instances for `{Int,Word}{,8,16,32,64}`](https://github.com/dhall-lang/dhall-haskell/pull/2012) +* [Add `--output` option for `dhall text` subcommand](https://github.com/dhall-lang/dhall-haskell/pull/1974) +* [Add `Dhall.Crypto.toString`](https://github.com/dhall-lang/dhall-haskell/pull/1976) +* [Make the HTTP `Manager` configurable](https://github.com/dhall-lang/dhall-haskell/pull/2027) + * Several import-related functions now provide an alternative variants that + allows the user to supply a custom `Manager` + * You can use this to tweak HTTP request timeouts or use a different TLS + manager (e.g. one from `http-client-openssl`) +* Fixes and improvements to code formatting + * [#2000](https://github.com/dhall-lang/dhall-haskell/pull/2000) + * [#2021](https://github.com/dhall-lang/dhall-haskell/pull/2021) + + The formatter now preserves comments for record fields (both record types + and record literals) +* Fixes and improvements to documentation + * [#2011](https://github.com/dhall-lang/dhall-haskell/pull/2011) + * [#2013](https://github.com/dhall-lang/dhall-haskell/pull/2013) + * [#2014](https://github.com/dhall-lang/dhall-haskell/pull/2014) +* Fixes and improvements to test suite + * [#2020](https://github.com/dhall-lang/dhall-haskell/pull/2020) + 1.34.0 * [Supports version 17.1.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v17.1.0) diff --git a/benchmark/deep-nested-large-record/Main.hs b/benchmark/deep-nested-large-record/Main.hs --- a/benchmark/deep-nested-large-record/Main.hs +++ b/benchmark/deep-nested-large-record/Main.hs @@ -1,6 +1,7 @@ {-# LANGUAGE OverloadedStrings #-} module Main (main) where +import Data.Void (Void) import Gauge (defaultMain) import qualified Data.Sequence as Seq @@ -21,16 +22,19 @@ } } -issue412 :: Core.Expr s TypeCheck.X -> Gauge.Benchmarkable +issue412 :: Core.Expr s Void -> Gauge.Benchmarkable issue412 prelude = Gauge.whnf TypeCheck.typeOf expr where expr = Core.Let (Core.Binding Nothing "prelude" Nothing Nothing Nothing prelude) $ Core.ListLit Nothing $ Seq.replicate 5 - $ Core.Var (Core.V "prelude" 0) `Core.Field` "types" `Core.Field` "Little" `Core.Field` "Foo" + $ Core.Var (Core.V "prelude" 0) `Core.Field` types `Core.Field` little `Core.Field` foo + types = Core.makeFieldSelection "types" + little = Core.makeFieldSelection "little" + foo = Core.makeFieldSelection "Foo" -unionPerformance :: Core.Expr s TypeCheck.X -> Gauge.Benchmarkable +unionPerformance :: Core.Expr s Void -> Gauge.Benchmarkable unionPerformance prelude = Gauge.whnf TypeCheck.typeOf expr where expr = @@ -48,12 +52,14 @@ Nothing Nothing Nothing - (prelude `Core.Field` "types" `Core.Field` "Big") + (prelude `Core.Field` types `Core.Field` big) ) (Core.Prefer Core.PreferFromSource "big" "big") ) ) "x" + types = Core.makeFieldSelection "types" + big = Core.makeFieldSelection "Big" main :: IO () main = diff --git a/benchmark/parser/Main.hs b/benchmark/parser/Main.hs --- a/benchmark/parser/Main.hs +++ b/benchmark/parser/Main.hs @@ -6,11 +6,10 @@ import Control.Monad (forM) import Data.Map (Map, foldrWithKey, singleton, unions) import Data.Void (Void) -import Gauge (bench, bgroup, defaultMain, env, nf, nfIO, whnf) +import Gauge (bench, bgroup, defaultMain, env, nf, whnf) import System.Directory -import qualified Codec.Serialise import qualified Data.ByteString.Lazy import qualified Data.Text as T import qualified Data.Text.IO as TIO @@ -50,7 +49,7 @@ benchExprFromBytes :: String -> Data.ByteString.Lazy.ByteString -> Gauge.Benchmark -benchExprFromBytes name bytes = bench name (nf f bytes) +benchExprFromBytes name bs = bench name (nf f bs) where f bytes = case Dhall.Binary.decodeExpression bytes of diff --git a/dhall-lang/Prelude/Bool/and.dhall b/dhall-lang/Prelude/Bool/and.dhall --- a/dhall-lang/Prelude/Bool/and.dhall +++ b/dhall-lang/Prelude/Bool/and.dhall @@ -1,4 +1,4 @@ -{- +{-| The `and` function returns `False` if there are any `False` elements in the `List` and returns `True` otherwise -} diff --git a/dhall-lang/Prelude/Bool/build.dhall b/dhall-lang/Prelude/Bool/build.dhall --- a/dhall-lang/Prelude/Bool/build.dhall +++ b/dhall-lang/Prelude/Bool/build.dhall @@ -1,6 +1,4 @@ -{- -`build` is the inverse of `fold` --} +--| `build` is the inverse of `fold` let build : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → diff --git a/dhall-lang/Prelude/Bool/even.dhall b/dhall-lang/Prelude/Bool/even.dhall --- a/dhall-lang/Prelude/Bool/even.dhall +++ b/dhall-lang/Prelude/Bool/even.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` if there are an even number of `False` elements in the list and returns `False` otherwise. diff --git a/dhall-lang/Prelude/Bool/fold.dhall b/dhall-lang/Prelude/Bool/fold.dhall --- a/dhall-lang/Prelude/Bool/fold.dhall +++ b/dhall-lang/Prelude/Bool/fold.dhall @@ -1,6 +1,4 @@ -{- -`fold` is essentially the same as `if`/`then`/`else` except as a function --} +--| `fold` is essentially the same as `if`/`then`/`else` except as a function let fold : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool = λ(b : Bool) → diff --git a/dhall-lang/Prelude/Bool/not.dhall b/dhall-lang/Prelude/Bool/not.dhall --- a/dhall-lang/Prelude/Bool/not.dhall +++ b/dhall-lang/Prelude/Bool/not.dhall @@ -1,6 +1,4 @@ -{- -Flip the value of a `Bool` --} +--| Flip the value of a `Bool` let not : Bool → Bool = λ(b : Bool) → b == False diff --git a/dhall-lang/Prelude/Bool/odd.dhall b/dhall-lang/Prelude/Bool/odd.dhall --- a/dhall-lang/Prelude/Bool/odd.dhall +++ b/dhall-lang/Prelude/Bool/odd.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` if there are an odd number of `True` elements in the list and returns `False` otherwise. diff --git a/dhall-lang/Prelude/Bool/or.dhall b/dhall-lang/Prelude/Bool/or.dhall --- a/dhall-lang/Prelude/Bool/or.dhall +++ b/dhall-lang/Prelude/Bool/or.dhall @@ -1,4 +1,4 @@ -{- +{-| The `or` function returns `True` if there are any `True` elements in the `List` and returns `False` otherwise -} diff --git a/dhall-lang/Prelude/Bool/show.dhall b/dhall-lang/Prelude/Bool/show.dhall --- a/dhall-lang/Prelude/Bool/show.dhall +++ b/dhall-lang/Prelude/Bool/show.dhall @@ -1,4 +1,4 @@ -{- +{-| Render a `Bool` as `Text` using the same representation as Dhall source code (i.e. beginning with a capital letter) -} diff --git a/dhall-lang/Prelude/Double/show.dhall b/dhall-lang/Prelude/Double/show.dhall --- a/dhall-lang/Prelude/Double/show.dhall +++ b/dhall-lang/Prelude/Double/show.dhall @@ -1,4 +1,4 @@ -{- +{-| Render a `Double` as `Text` using the same representation as Dhall source code (i.e. a decimal floating point number with a leading `-` sign if negative) -} diff --git a/dhall-lang/Prelude/Function/compose.dhall b/dhall-lang/Prelude/Function/compose.dhall --- a/dhall-lang/Prelude/Function/compose.dhall +++ b/dhall-lang/Prelude/Function/compose.dhall @@ -1,6 +1,4 @@ -{- -Compose two functions into one. --} +--| Compose two functions into one. let compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c = λ(A : Type) → diff --git a/dhall-lang/Prelude/Function/identity.dhall b/dhall-lang/Prelude/Function/identity.dhall --- a/dhall-lang/Prelude/Function/identity.dhall +++ b/dhall-lang/Prelude/Function/identity.dhall @@ -1,6 +1,4 @@ -{- -The identity function simply returns its input --} +--| The identity function simply returns its input let identity : ∀(a : Type) → ∀(x : a) → a = λ(a : Type) → λ(x : a) → x diff --git a/dhall-lang/Prelude/Integer/abs.dhall b/dhall-lang/Prelude/Integer/abs.dhall --- a/dhall-lang/Prelude/Integer/abs.dhall +++ b/dhall-lang/Prelude/Integer/abs.dhall @@ -1,6 +1,4 @@ -{- -Returns the absolute value of an `Integer`, i.e. its non-negative value. --} +--| Returns the absolute value of an `Integer`, i.e. its non-negative value. let abs : Integer → Natural = λ(n : Integer) → diff --git a/dhall-lang/Prelude/Integer/add.dhall b/dhall-lang/Prelude/Integer/add.dhall --- a/dhall-lang/Prelude/Integer/add.dhall +++ b/dhall-lang/Prelude/Integer/add.dhall @@ -1,6 +1,4 @@ -{- -`add m n` computes `m + n`. --} +--| `add m n` computes `m + n`. let Integer/subtract = ./subtract sha256:a34d36272fa8ae4f1ec8b56222fe8dc8a2ec55ec6538b840de0cbe207b006fda ? ./subtract diff --git a/dhall-lang/Prelude/Integer/clamp.dhall b/dhall-lang/Prelude/Integer/clamp.dhall --- a/dhall-lang/Prelude/Integer/clamp.dhall +++ b/dhall-lang/Prelude/Integer/clamp.dhall @@ -1,4 +1,4 @@ -{- +{-| Convert an `Integer` to a `Natural` number, with negative numbers becoming zero. -} let clamp diff --git a/dhall-lang/Prelude/Integer/equal.dhall b/dhall-lang/Prelude/Integer/equal.dhall --- a/dhall-lang/Prelude/Integer/equal.dhall +++ b/dhall-lang/Prelude/Integer/equal.dhall @@ -1,6 +1,4 @@ -{- -`equal` checks if two Integers are equal. --} +--| `equal` checks if two Integers are equal. let Natural/equal = ../Natural/equal sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60 ? ../Natural/equal diff --git a/dhall-lang/Prelude/Integer/greaterThan.dhall b/dhall-lang/Prelude/Integer/greaterThan.dhall --- a/dhall-lang/Prelude/Integer/greaterThan.dhall +++ b/dhall-lang/Prelude/Integer/greaterThan.dhall @@ -1,6 +1,4 @@ -{- -`greaterThan` checks if one Integer is greater than another. --} +--| `greaterThan` checks if one Integer is greater than another. let Bool/not = ../Bool/not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4 ? ../Bool/not diff --git a/dhall-lang/Prelude/Integer/greaterThanEqual.dhall b/dhall-lang/Prelude/Integer/greaterThanEqual.dhall --- a/dhall-lang/Prelude/Integer/greaterThanEqual.dhall +++ b/dhall-lang/Prelude/Integer/greaterThanEqual.dhall @@ -1,4 +1,4 @@ -{- +{-| `greaterThanEqual` checks if one Integer is greater than or equal to another. -} let lessThanEqual = diff --git a/dhall-lang/Prelude/Integer/lessThan.dhall b/dhall-lang/Prelude/Integer/lessThan.dhall --- a/dhall-lang/Prelude/Integer/lessThan.dhall +++ b/dhall-lang/Prelude/Integer/lessThan.dhall @@ -1,6 +1,4 @@ -{- -`lessThan` checks if one Integer is less than another. --} +--| `lessThan` checks if one Integer is less than another. let greaterThan = ./greaterThan sha256:d23affd73029fc9aaf867c2c7b86510ca2802d3f0d1f3e1d1a93ffd87b7cb64b ? ./greaterThan diff --git a/dhall-lang/Prelude/Integer/lessThanEqual.dhall b/dhall-lang/Prelude/Integer/lessThanEqual.dhall --- a/dhall-lang/Prelude/Integer/lessThanEqual.dhall +++ b/dhall-lang/Prelude/Integer/lessThanEqual.dhall @@ -1,6 +1,4 @@ -{- -`lessThanEqual` checks if one Integer is less than or equal to another. --} +--| `lessThanEqual` checks if one Integer is less than or equal to another. let Natural/greaterThanEqual = ../Natural/greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4 ? ../Natural/greaterThanEqual diff --git a/dhall-lang/Prelude/Integer/multiply.dhall b/dhall-lang/Prelude/Integer/multiply.dhall --- a/dhall-lang/Prelude/Integer/multiply.dhall +++ b/dhall-lang/Prelude/Integer/multiply.dhall @@ -1,6 +1,4 @@ -{- -`multiply m n` computes `m * n`. --} +--| `multiply m n` computes `m * n`. let nonPositive = ./nonPositive sha256:e00a852eed5b84ff60487097d8aadce53c9e5301f53ff4954044bd68949fac3b diff --git a/dhall-lang/Prelude/Integer/negate.dhall b/dhall-lang/Prelude/Integer/negate.dhall --- a/dhall-lang/Prelude/Integer/negate.dhall +++ b/dhall-lang/Prelude/Integer/negate.dhall @@ -1,6 +1,4 @@ -{- -Invert the sign of an `Integer`, with zero remaining unchanged. --} +--| Invert the sign of an `Integer`, with zero remaining unchanged. let negate : Integer → Integer = Integer/negate diff --git a/dhall-lang/Prelude/Integer/negative.dhall b/dhall-lang/Prelude/Integer/negative.dhall --- a/dhall-lang/Prelude/Integer/negative.dhall +++ b/dhall-lang/Prelude/Integer/negative.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` for any `Integer` less than `+0`. `negative` is more efficient than `./lessThan +0` or `./lessThanEqual -1`. diff --git a/dhall-lang/Prelude/Integer/nonNegative.dhall b/dhall-lang/Prelude/Integer/nonNegative.dhall --- a/dhall-lang/Prelude/Integer/nonNegative.dhall +++ b/dhall-lang/Prelude/Integer/nonNegative.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` for `+0` and any positive `Integer`. `nonNegative` is more efficient than `./greaterThanEqual +0` or `./greaterThan -1`. diff --git a/dhall-lang/Prelude/Integer/nonPositive.dhall b/dhall-lang/Prelude/Integer/nonPositive.dhall --- a/dhall-lang/Prelude/Integer/nonPositive.dhall +++ b/dhall-lang/Prelude/Integer/nonPositive.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` for `+0` and any negative `Integer`. `nonPositive` is more efficient than `./lessThanEqual +0` or `./lessThan +1`. diff --git a/dhall-lang/Prelude/Integer/positive.dhall b/dhall-lang/Prelude/Integer/positive.dhall --- a/dhall-lang/Prelude/Integer/positive.dhall +++ b/dhall-lang/Prelude/Integer/positive.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` for any `Integer` greater than `+0`. `positive` is more efficient than `./greaterThan +0` or `./greaterThanEqual +1`. diff --git a/dhall-lang/Prelude/Integer/show.dhall b/dhall-lang/Prelude/Integer/show.dhall --- a/dhall-lang/Prelude/Integer/show.dhall +++ b/dhall-lang/Prelude/Integer/show.dhall @@ -1,4 +1,4 @@ -{- +{-| Render an `Integer` as `Text` using the same representation as Dhall source code (i.e. a decimal number with a leading `-` sign if negative and a leading `+` sign if non-negative) diff --git a/dhall-lang/Prelude/Integer/subtract.dhall b/dhall-lang/Prelude/Integer/subtract.dhall --- a/dhall-lang/Prelude/Integer/subtract.dhall +++ b/dhall-lang/Prelude/Integer/subtract.dhall @@ -1,6 +1,4 @@ -{- -`subtract m n` computes `n - m`. --} +--| `subtract m n` computes `n - m`. let nonPositive = ./nonPositive sha256:e00a852eed5b84ff60487097d8aadce53c9e5301f53ff4954044bd68949fac3b ? ./nonPositive diff --git a/dhall-lang/Prelude/Integer/toDouble.dhall b/dhall-lang/Prelude/Integer/toDouble.dhall --- a/dhall-lang/Prelude/Integer/toDouble.dhall +++ b/dhall-lang/Prelude/Integer/toDouble.dhall @@ -1,6 +1,4 @@ -{- -Convert an `Integer` to the corresponding `Double` --} +--| Convert an `Integer` to the corresponding `Double` let toDouble : Integer → Double = Integer/toDouble diff --git a/dhall-lang/Prelude/Integer/toNatural.dhall b/dhall-lang/Prelude/Integer/toNatural.dhall --- a/dhall-lang/Prelude/Integer/toNatural.dhall +++ b/dhall-lang/Prelude/Integer/toNatural.dhall @@ -1,4 +1,4 @@ -{- +{-| Convert an `Integer` to an `Optional Natural`, with negative numbers becoming `None Natural`. -} let nonNegative = diff --git a/dhall-lang/Prelude/JSON/Format.dhall b/dhall-lang/Prelude/JSON/Format.dhall --- a/dhall-lang/Prelude/JSON/Format.dhall +++ b/dhall-lang/Prelude/JSON/Format.dhall @@ -1,7 +1,8 @@ -{- An internal type used by `./renderAs` to select the output format. +{-| +An internal type used by `./renderAs` to select the output format. - You should not need to use this type directly, simply use `./render` - or `./renderYAML` as appropriate. +You should not need to use this type directly, simply use `./render` +or `./renderYAML` as appropriate. -} < YAML | JSON > diff --git a/dhall-lang/Prelude/JSON/Nesting.dhall b/dhall-lang/Prelude/JSON/Nesting.dhall --- a/dhall-lang/Prelude/JSON/Nesting.dhall +++ b/dhall-lang/Prelude/JSON/Nesting.dhall @@ -1,4 +1,4 @@ -{- +{-| This type is used as part of `dhall-json`'s support for preserving alternative names @@ -24,7 +24,7 @@ { "foo": 2, "name": "Left" - } +} ``` -} diff --git a/dhall-lang/Prelude/JSON/Tagged.dhall b/dhall-lang/Prelude/JSON/Tagged.dhall --- a/dhall-lang/Prelude/JSON/Tagged.dhall +++ b/dhall-lang/Prelude/JSON/Tagged.dhall @@ -1,4 +1,4 @@ -{- +{-| This is a convenient type-level function when using `dhall-to-json`'s support for preserving alternative names diff --git a/dhall-lang/Prelude/JSON/Type.dhall b/dhall-lang/Prelude/JSON/Type.dhall --- a/dhall-lang/Prelude/JSON/Type.dhall +++ b/dhall-lang/Prelude/JSON/Type.dhall @@ -1,12 +1,13 @@ -{- Dhall encoding of an arbitrary JSON value +{-| +Dhall encoding of an arbitrary JSON value - For example, the following JSON value: +For example, the following JSON value: ``` [ { "foo": null, "bar": [ 1.0, true ] } ] ``` - ... corresponds to the following Dhall expression: +... corresponds to the following Dhall expression: ``` λ(JSON : Type) → diff --git a/dhall-lang/Prelude/JSON/array.dhall b/dhall-lang/Prelude/JSON/array.dhall --- a/dhall-lang/Prelude/JSON/array.dhall +++ b/dhall-lang/Prelude/JSON/array.dhall @@ -1,4 +1,5 @@ -{- Create a JSON array from a `List` of JSON values +{-| +Create a JSON array from a `List` of JSON values ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/bool.dhall b/dhall-lang/Prelude/JSON/bool.dhall --- a/dhall-lang/Prelude/JSON/bool.dhall +++ b/dhall-lang/Prelude/JSON/bool.dhall @@ -1,4 +1,5 @@ -{- Create a JSON bool from a Dhall `Bool` +{-| +Create a JSON bool from a Dhall `Bool` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/core.dhall b/dhall-lang/Prelude/JSON/core.dhall --- a/dhall-lang/Prelude/JSON/core.dhall +++ b/dhall-lang/Prelude/JSON/core.dhall @@ -1,12 +1,11 @@ -{- A record of functions useful for constructing `JSON` values. +{-| +A record of functions useful for constructing `JSON` values. - This is only a subset of what `package.dhall` exports. If you are - not writing a JSON prelude function, you should use the - `package.dhall` file instead. +This is only a subset of what `package.dhall` exports. If you are not writing a +JSON prelude function, you should use the `package.dhall` file instead. - It is used internally by `render`, `renderYAML` and - `omitNullFields` instead of `package.dhall` to avoid import - cycles. +It is used internally by `render`, `renderYAML` and `omitNullFields` instead of +`package.dhall` to avoid import cycles. -} { Type = ./Type sha256:40edbc9371979426df63e064333b02689b969c4cfbbccfa481216d2d1a6e9759 diff --git a/dhall-lang/Prelude/JSON/double.dhall b/dhall-lang/Prelude/JSON/double.dhall --- a/dhall-lang/Prelude/JSON/double.dhall +++ b/dhall-lang/Prelude/JSON/double.dhall @@ -1,4 +1,5 @@ -{- Create a JSON number from a Dhall `Double` +{-| +Create a JSON number from a Dhall `Double` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/integer.dhall b/dhall-lang/Prelude/JSON/integer.dhall --- a/dhall-lang/Prelude/JSON/integer.dhall +++ b/dhall-lang/Prelude/JSON/integer.dhall @@ -1,4 +1,5 @@ -{- Create a JSON number from a Dhall `Integer` +{-| +Create a JSON number from a Dhall `Integer` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/natural.dhall b/dhall-lang/Prelude/JSON/natural.dhall --- a/dhall-lang/Prelude/JSON/natural.dhall +++ b/dhall-lang/Prelude/JSON/natural.dhall @@ -1,4 +1,5 @@ -{- Create a JSON number from a Dhall `Natural` +{-| +Create a JSON number from a Dhall `Natural` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/null.dhall b/dhall-lang/Prelude/JSON/null.dhall --- a/dhall-lang/Prelude/JSON/null.dhall +++ b/dhall-lang/Prelude/JSON/null.dhall @@ -1,4 +1,5 @@ -{- Create a JSON null +{-| +Create a JSON null ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/number.dhall b/dhall-lang/Prelude/JSON/number.dhall --- a/dhall-lang/Prelude/JSON/number.dhall +++ b/dhall-lang/Prelude/JSON/number.dhall @@ -1,4 +1,5 @@ -{- Create a JSON number from a Dhall `Double` +{-| +Create a JSON number from a Dhall `Double` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/object.dhall b/dhall-lang/Prelude/JSON/object.dhall --- a/dhall-lang/Prelude/JSON/object.dhall +++ b/dhall-lang/Prelude/JSON/object.dhall @@ -1,4 +1,5 @@ -{- Create a JSON object from a Dhall `Map` +{-| +Create a JSON object from a Dhall `Map` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/omitNullFields.dhall b/dhall-lang/Prelude/JSON/omitNullFields.dhall --- a/dhall-lang/Prelude/JSON/omitNullFields.dhall +++ b/dhall-lang/Prelude/JSON/omitNullFields.dhall @@ -1,4 +1,4 @@ -{- +{-| This utility omits all `null` record fields, which is often the idiomatic way for a configuration to encode absent fields -} diff --git a/dhall-lang/Prelude/JSON/render.dhall b/dhall-lang/Prelude/JSON/render.dhall --- a/dhall-lang/Prelude/JSON/render.dhall +++ b/dhall-lang/Prelude/JSON/render.dhall @@ -1,8 +1,8 @@ -{- Render a `JSON` value as `Text` - - This is useful for debugging `JSON` values or for tests. For anything - more sophisticated you should use `dhall-to-json` or `dhall-to-yaml` +{-| +Render a `JSON` value as `Text` +This is useful for debugging `JSON` values or for tests. For anything +more sophisticated you should use `dhall-to-json` or `dhall-to-yaml` -} let JSON = ./core.dhall sha256:5dc1135d5481cfd6fde625aaed9fcbdb7aa7c14f2e76726aa5fdef028a5c10f5 diff --git a/dhall-lang/Prelude/JSON/renderAs.dhall b/dhall-lang/Prelude/JSON/renderAs.dhall --- a/dhall-lang/Prelude/JSON/renderAs.dhall +++ b/dhall-lang/Prelude/JSON/renderAs.dhall @@ -1,4 +1,4 @@ -{- Render a `JSON` value as `Text` in either JSON or YAML format. -} +--| Render a `JSON` value as `Text` in either JSON or YAML format. let JSON = ./core.dhall sha256:5dc1135d5481cfd6fde625aaed9fcbdb7aa7c14f2e76726aa5fdef028a5c10f5 diff --git a/dhall-lang/Prelude/JSON/renderInteger.dhall b/dhall-lang/Prelude/JSON/renderInteger.dhall --- a/dhall-lang/Prelude/JSON/renderInteger.dhall +++ b/dhall-lang/Prelude/JSON/renderInteger.dhall @@ -1,5 +1,6 @@ -{- Render an `Integer` value as a `JSON number`, according to the JSON - standard, in which a number may not start with a plus sign (`+`). +{-| +Render an `Integer` value as a `JSON number`, according to the JSON standard, in +which a number may not start with a plus sign (`+`). -} let Integer/nonNegative = diff --git a/dhall-lang/Prelude/JSON/renderYAML.dhall b/dhall-lang/Prelude/JSON/renderYAML.dhall --- a/dhall-lang/Prelude/JSON/renderYAML.dhall +++ b/dhall-lang/Prelude/JSON/renderYAML.dhall @@ -1,12 +1,12 @@ -{- Render a `JSON` value as `Text` in YAML format. - - The generated YAML text will only contain escaped object keys and - string values and might therefore not be very human readable. +{-| +Render a `JSON` value as `Text` in YAML format. - However, it is useful for debugging `JSON` values or for tests. - For anything more sophisticated you should use `dhall-to-json` or - `dhall-to-yaml`. +The generated YAML text will only contain escaped object keys and +string values and might therefore not be very human readable. +However, it is useful for debugging `JSON` values or for tests. +For anything more sophisticated you should use `dhall-to-json` or +`dhall-to-yaml`. -} let JSON = diff --git a/dhall-lang/Prelude/JSON/string.dhall b/dhall-lang/Prelude/JSON/string.dhall --- a/dhall-lang/Prelude/JSON/string.dhall +++ b/dhall-lang/Prelude/JSON/string.dhall @@ -1,4 +1,5 @@ -{- Create a JSON string from Dhall `Text` +{-| +Create a JSON string from Dhall `Text` ``` let JSON = ./package.dhall diff --git a/dhall-lang/Prelude/JSON/tagInline.dhall b/dhall-lang/Prelude/JSON/tagInline.dhall --- a/dhall-lang/Prelude/JSON/tagInline.dhall +++ b/dhall-lang/Prelude/JSON/tagInline.dhall @@ -1,5 +1,4 @@ -{- Prepare a union value for JSON- or YAML-encoding with the inline layout --} +--| Prepare a union value for JSON- or YAML-encoding with the inline layout let Nesting = ./Nesting sha256:6284802edd41d5d725aa1ec7687e614e21ad1be7e14dd10996bfa9625105c335 ? ./Nesting diff --git a/dhall-lang/Prelude/JSON/tagNested.dhall b/dhall-lang/Prelude/JSON/tagNested.dhall --- a/dhall-lang/Prelude/JSON/tagNested.dhall +++ b/dhall-lang/Prelude/JSON/tagNested.dhall @@ -1,5 +1,4 @@ -{- Prepare a union value for JSON- or YAML-encoding with the nested layout --} +--| Prepare a union value for JSON- or YAML-encoding with the nested layout let Nesting = ./Nesting sha256:6284802edd41d5d725aa1ec7687e614e21ad1be7e14dd10996bfa9625105c335 ? ./Nesting diff --git a/dhall-lang/Prelude/List/all.dhall b/dhall-lang/Prelude/List/all.dhall --- a/dhall-lang/Prelude/List/all.dhall +++ b/dhall-lang/Prelude/List/all.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` if the supplied function returns `True` for all elements in the `List` -} diff --git a/dhall-lang/Prelude/List/any.dhall b/dhall-lang/Prelude/List/any.dhall --- a/dhall-lang/Prelude/List/any.dhall +++ b/dhall-lang/Prelude/List/any.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` if the supplied function returns `True` for any element in the `List` -} diff --git a/dhall-lang/Prelude/List/build.dhall b/dhall-lang/Prelude/List/build.dhall --- a/dhall-lang/Prelude/List/build.dhall +++ b/dhall-lang/Prelude/List/build.dhall @@ -1,6 +1,4 @@ -{- -`build` is the inverse of `fold` --} +--| `build` is the inverse of `fold` let build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → diff --git a/dhall-lang/Prelude/List/concat.dhall b/dhall-lang/Prelude/List/concat.dhall --- a/dhall-lang/Prelude/List/concat.dhall +++ b/dhall-lang/Prelude/List/concat.dhall @@ -1,6 +1,4 @@ -{- -Concatenate a `List` of `List`s into a single `List` --} +--| Concatenate a `List` of `List`s into a single `List` let concat : ∀(a : Type) → List (List a) → List a = λ(a : Type) → diff --git a/dhall-lang/Prelude/List/concatMap.dhall b/dhall-lang/Prelude/List/concatMap.dhall --- a/dhall-lang/Prelude/List/concatMap.dhall +++ b/dhall-lang/Prelude/List/concatMap.dhall @@ -1,4 +1,4 @@ -{- +{-| Transform a list by applying a function to each element and flattening the results -} diff --git a/dhall-lang/Prelude/List/default.dhall b/dhall-lang/Prelude/List/default.dhall --- a/dhall-lang/Prelude/List/default.dhall +++ b/dhall-lang/Prelude/List/default.dhall @@ -1,4 +1,4 @@ -{- +{-| Unpack an `Optional` containing a `List`, defaulting to an empty list when the `Optional` is `None` -} diff --git a/dhall-lang/Prelude/List/drop.dhall b/dhall-lang/Prelude/List/drop.dhall --- a/dhall-lang/Prelude/List/drop.dhall +++ b/dhall-lang/Prelude/List/drop.dhall @@ -1,4 +1,4 @@ --- Remove first `n` elements of a list +--| Remove first `n` elements of a list let Natural/greaterThanEqual = ../Natural/greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4 ? ../Natural/greaterThanEqual diff --git a/dhall-lang/Prelude/List/empty.dhall b/dhall-lang/Prelude/List/empty.dhall --- a/dhall-lang/Prelude/List/empty.dhall +++ b/dhall-lang/Prelude/List/empty.dhall @@ -1,6 +1,4 @@ -{- -An empty list of the given type --} +--| An empty list of the given type let empty : ∀(a : Type) → List a = λ(a : Type) → [] : List a diff --git a/dhall-lang/Prelude/List/filter.dhall b/dhall-lang/Prelude/List/filter.dhall --- a/dhall-lang/Prelude/List/filter.dhall +++ b/dhall-lang/Prelude/List/filter.dhall @@ -1,8 +1,4 @@ -{- -Only keep elements of the list where the supplied function returns `True` - -Examples: --} +--| Only keep elements of the list where the supplied function returns `True` let filter : ∀(a : Type) → (a → Bool) → List a → List a = λ(a : Type) → diff --git a/dhall-lang/Prelude/List/fold.dhall b/dhall-lang/Prelude/List/fold.dhall --- a/dhall-lang/Prelude/List/fold.dhall +++ b/dhall-lang/Prelude/List/fold.dhall @@ -1,4 +1,4 @@ -{- +{-| `fold` is the primitive function for consuming `List`s If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a diff --git a/dhall-lang/Prelude/List/generate.dhall b/dhall-lang/Prelude/List/generate.dhall --- a/dhall-lang/Prelude/List/generate.dhall +++ b/dhall-lang/Prelude/List/generate.dhall @@ -1,4 +1,4 @@ -{- +{-| Build a list by calling the supplied function on all `Natural` numbers from `0` up to but not including the supplied `Natural` number -} diff --git a/dhall-lang/Prelude/List/head.dhall b/dhall-lang/Prelude/List/head.dhall --- a/dhall-lang/Prelude/List/head.dhall +++ b/dhall-lang/Prelude/List/head.dhall @@ -1,6 +1,4 @@ -{- -Retrieve the first element of the list --} +--| Retrieve the first element of the list let head : ∀(a : Type) → List a → Optional a = List/head diff --git a/dhall-lang/Prelude/List/index.dhall b/dhall-lang/Prelude/List/index.dhall --- a/dhall-lang/Prelude/List/index.dhall +++ b/dhall-lang/Prelude/List/index.dhall @@ -1,6 +1,4 @@ -{- -Retrieve an element from a `List` using its 0-based index --} +--| Retrieve an element from a `List` using its 0-based index let drop = ./drop sha256:af983ba3ead494dd72beed05c0f3a17c36a4244adedf7ced502c6512196ed0cf ? ./drop diff --git a/dhall-lang/Prelude/List/indexed.dhall b/dhall-lang/Prelude/List/indexed.dhall --- a/dhall-lang/Prelude/List/indexed.dhall +++ b/dhall-lang/Prelude/List/indexed.dhall @@ -1,6 +1,4 @@ -{- -Tag each element of the list with its index --} +--| Tag each element of the list with its index let indexed : ∀(a : Type) → List a → List { index : Natural, value : a } = List/indexed diff --git a/dhall-lang/Prelude/List/iterate.dhall b/dhall-lang/Prelude/List/iterate.dhall --- a/dhall-lang/Prelude/List/iterate.dhall +++ b/dhall-lang/Prelude/List/iterate.dhall @@ -1,4 +1,4 @@ -{- +{-| Generate a list of the specified length given a seed value and transition function -} diff --git a/dhall-lang/Prelude/List/last.dhall b/dhall-lang/Prelude/List/last.dhall --- a/dhall-lang/Prelude/List/last.dhall +++ b/dhall-lang/Prelude/List/last.dhall @@ -1,6 +1,4 @@ -{- -Retrieve the last element of the list --} +--| Retrieve the last element of the list let last : ∀(a : Type) → List a → Optional a = List/last diff --git a/dhall-lang/Prelude/List/length.dhall b/dhall-lang/Prelude/List/length.dhall --- a/dhall-lang/Prelude/List/length.dhall +++ b/dhall-lang/Prelude/List/length.dhall @@ -1,6 +1,4 @@ -{- -Returns the number of elements in a list --} +--| Returns the number of elements in a list let length : ∀(a : Type) → List a → Natural = List/length diff --git a/dhall-lang/Prelude/List/map.dhall b/dhall-lang/Prelude/List/map.dhall --- a/dhall-lang/Prelude/List/map.dhall +++ b/dhall-lang/Prelude/List/map.dhall @@ -1,6 +1,4 @@ -{- -Transform a list by applying a function to each element --} +--| Transform a list by applying a function to each element let map : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b = λ(a : Type) → diff --git a/dhall-lang/Prelude/List/null.dhall b/dhall-lang/Prelude/List/null.dhall --- a/dhall-lang/Prelude/List/null.dhall +++ b/dhall-lang/Prelude/List/null.dhall @@ -1,6 +1,4 @@ -{- -Returns `True` if the `List` is empty and `False` otherwise --} +--| Returns `True` if the `List` is empty and `False` otherwise let null : ∀(a : Type) → List a → Bool = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) diff --git a/dhall-lang/Prelude/List/partition.dhall b/dhall-lang/Prelude/List/partition.dhall --- a/dhall-lang/Prelude/List/partition.dhall +++ b/dhall-lang/Prelude/List/partition.dhall @@ -1,4 +1,4 @@ -{- +{-| `partition` divides a `List` of elements into those that satisfy a predicate and those that do not -} diff --git a/dhall-lang/Prelude/List/replicate.dhall b/dhall-lang/Prelude/List/replicate.dhall --- a/dhall-lang/Prelude/List/replicate.dhall +++ b/dhall-lang/Prelude/List/replicate.dhall @@ -1,6 +1,4 @@ -{- -Build a list by copying the given element the specified number of times --} +--| Build a list by copying the given element the specified number of times let replicate : Natural → ∀(a : Type) → a → List a = λ(n : Natural) → diff --git a/dhall-lang/Prelude/List/reverse.dhall b/dhall-lang/Prelude/List/reverse.dhall --- a/dhall-lang/Prelude/List/reverse.dhall +++ b/dhall-lang/Prelude/List/reverse.dhall @@ -1,6 +1,4 @@ -{- -Reverse a list --} +--| Reverse a list let reverse : ∀(a : Type) → List a → List a = List/reverse diff --git a/dhall-lang/Prelude/List/shifted.dhall b/dhall-lang/Prelude/List/shifted.dhall --- a/dhall-lang/Prelude/List/shifted.dhall +++ b/dhall-lang/Prelude/List/shifted.dhall @@ -1,4 +1,4 @@ -{- +{-| Combine a `List` of `List`s, offsetting the `index` of each element by the number of elements in preceding lists -} diff --git a/dhall-lang/Prelude/List/take.dhall b/dhall-lang/Prelude/List/take.dhall --- a/dhall-lang/Prelude/List/take.dhall +++ b/dhall-lang/Prelude/List/take.dhall @@ -1,4 +1,4 @@ --- Truncate a list to the first `n` elements +--| Truncate a list to the first `n` elements let Natural/lessThan = ../Natural/lessThan sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c ? ../Natural/lessThan diff --git a/dhall-lang/Prelude/List/unpackOptionals.dhall b/dhall-lang/Prelude/List/unpackOptionals.dhall --- a/dhall-lang/Prelude/List/unpackOptionals.dhall +++ b/dhall-lang/Prelude/List/unpackOptionals.dhall @@ -1,6 +1,4 @@ -{- -Unpack Optionals in a List, omitting None items. --} +--| Unpack Optionals in a List, omitting None items. let List/concatMap = ./concatMap sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64 diff --git a/dhall-lang/Prelude/List/unzip.dhall b/dhall-lang/Prelude/List/unzip.dhall --- a/dhall-lang/Prelude/List/unzip.dhall +++ b/dhall-lang/Prelude/List/unzip.dhall @@ -1,6 +1,4 @@ -{- -Unzip a `List` into two separate `List`s --} +--| Unzip a `List` into two separate `List`s let unzip : ∀(a : Type) → ∀(b : Type) → diff --git a/dhall-lang/Prelude/List/zip.dhall b/dhall-lang/Prelude/List/zip.dhall --- a/dhall-lang/Prelude/List/zip.dhall +++ b/dhall-lang/Prelude/List/zip.dhall @@ -1,7 +1,7 @@ -{- +{-| Zip two `List` into a single `List` -Resulting `List` will have the length of the shortest of its arguments. +The resulting `List` will have the length of the shortest of its arguments. -} let List/index = ./index sha256:e657b55ecae4d899465c3032cb1a64c6aa6dc2aa3034204f3c15ce5c96c03e63 diff --git a/dhall-lang/Prelude/Location/Type.dhall b/dhall-lang/Prelude/Location/Type.dhall --- a/dhall-lang/Prelude/Location/Type.dhall +++ b/dhall-lang/Prelude/Location/Type.dhall @@ -1,5 +1,4 @@ -{- This is the union type returned when you import something `as Location` --} +--| This is the union type returned when you import something `as Location` let Location : Type = < Environment : Text | Local : Text | Missing | Remote : Text > diff --git a/dhall-lang/Prelude/Map/Entry.dhall b/dhall-lang/Prelude/Map/Entry.dhall --- a/dhall-lang/Prelude/Map/Entry.dhall +++ b/dhall-lang/Prelude/Map/Entry.dhall @@ -1,5 +1,4 @@ -{- The type of each key-value pair in a `Map` --} +--| The type of each key-value pair in a `Map` let Entry : Type → Type → Type = λ(k : Type) → λ(v : Type) → { mapKey : k, mapValue : v } diff --git a/dhall-lang/Prelude/Map/Type.dhall b/dhall-lang/Prelude/Map/Type.dhall --- a/dhall-lang/Prelude/Map/Type.dhall +++ b/dhall-lang/Prelude/Map/Type.dhall @@ -1,21 +1,22 @@ -{- This is the canonical way to encode a dynamic list of key-value pairs. +{-| +This is the canonical way to encode a dynamic list of key-value pairs. - Tools (such as `dhall-to-json`/`dhall-to-yaml` will recognize values of this - type and convert them to maps/dictionaries/hashes in the target language +Tools (such as `dhall-to-json`/`dhall-to-yaml` will recognize values of this +type and convert them to maps/dictionaries/hashes in the target language - For example, `dhall-to-json` converts a Dhall value like this: +For example, `dhall-to-json` converts a Dhall value like this: - ``` - [ { mapKey = "foo", mapValue = 1 } - , { mapKey = "bar", mapValue = 2 } - ] : ./Map Text Natural - ``` +``` +[ { mapKey = "foo", mapValue = 1 } +, { mapKey = "bar", mapValue = 2 } +] : ./Map Text Natural +``` - ... to a JSON value like this: +... to a JSON value like this: - ``` - { "foo": 1, "bar", 2 } - ``` +``` +{ "foo": 1, "bar", 2 } +``` -} let Map : Type → Type → Type diff --git a/dhall-lang/Prelude/Map/empty.dhall b/dhall-lang/Prelude/Map/empty.dhall --- a/dhall-lang/Prelude/Map/empty.dhall +++ b/dhall-lang/Prelude/Map/empty.dhall @@ -1,6 +1,4 @@ -{- -An empty `Map` of the given key and value types --} +--| An empty `Map` of the given key and value types let Map = ./Type sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed ? ./Type diff --git a/dhall-lang/Prelude/Map/keyText.dhall b/dhall-lang/Prelude/Map/keyText.dhall --- a/dhall-lang/Prelude/Map/keyText.dhall +++ b/dhall-lang/Prelude/Map/keyText.dhall @@ -1,4 +1,4 @@ -{- +{-| Builds a key-value record such that a `List` of them will be converted to a homogeneous record by dhall-to-json and dhall-to-yaml. diff --git a/dhall-lang/Prelude/Map/keyValue.dhall b/dhall-lang/Prelude/Map/keyValue.dhall --- a/dhall-lang/Prelude/Map/keyValue.dhall +++ b/dhall-lang/Prelude/Map/keyValue.dhall @@ -1,4 +1,4 @@ -{- +{-| Builds a key-value record such that a List of them will be converted to a homogeneous record by dhall-to-json and dhall-to-yaml. -} diff --git a/dhall-lang/Prelude/Map/keys.dhall b/dhall-lang/Prelude/Map/keys.dhall --- a/dhall-lang/Prelude/Map/keys.dhall +++ b/dhall-lang/Prelude/Map/keys.dhall @@ -1,6 +1,4 @@ -{- -Get all of the keys of a `Map` as a `List` --} +--| Get all of the keys of a `Map` as a `List` let Map = ./Type sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed ? ./Type diff --git a/dhall-lang/Prelude/Map/map.dhall b/dhall-lang/Prelude/Map/map.dhall --- a/dhall-lang/Prelude/Map/map.dhall +++ b/dhall-lang/Prelude/Map/map.dhall @@ -1,6 +1,4 @@ -{- -Transform a `Map` by applying a function to each value --} +--| Transform a `Map` by applying a function to each value let Map = ./Type sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed ? ./Type diff --git a/dhall-lang/Prelude/Map/values.dhall b/dhall-lang/Prelude/Map/values.dhall --- a/dhall-lang/Prelude/Map/values.dhall +++ b/dhall-lang/Prelude/Map/values.dhall @@ -1,6 +1,4 @@ -{- -Get all of the values of a `Map` as a `List` --} +--| Get all of the values of a `Map` as a `List` let Map = ./Type sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed ? ./Type diff --git a/dhall-lang/Prelude/Monoid.dhall b/dhall-lang/Prelude/Monoid.dhall --- a/dhall-lang/Prelude/Monoid.dhall +++ b/dhall-lang/Prelude/Monoid.dhall @@ -1,4 +1,4 @@ -{- +{-| Any function `f` that is a `Monoid` must satisfy the following law: ``` diff --git a/dhall-lang/Prelude/Natural/build.dhall b/dhall-lang/Prelude/Natural/build.dhall --- a/dhall-lang/Prelude/Natural/build.dhall +++ b/dhall-lang/Prelude/Natural/build.dhall @@ -1,6 +1,4 @@ -{- -`build` is the inverse of `fold` --} +--| `build` is the inverse of `fold` let build : ( ∀(natural : Type) → ∀(succ : natural → natural) → diff --git a/dhall-lang/Prelude/Natural/enumerate.dhall b/dhall-lang/Prelude/Natural/enumerate.dhall --- a/dhall-lang/Prelude/Natural/enumerate.dhall +++ b/dhall-lang/Prelude/Natural/enumerate.dhall @@ -1,4 +1,4 @@ -{- +{-| Generate a list of numbers from `0` up to but not including the specified number -} diff --git a/dhall-lang/Prelude/Natural/equal.dhall b/dhall-lang/Prelude/Natural/equal.dhall --- a/dhall-lang/Prelude/Natural/equal.dhall +++ b/dhall-lang/Prelude/Natural/equal.dhall @@ -1,6 +1,4 @@ -{- -`equal` checks if two Naturals are equal. --} +--| `equal` checks if two Naturals are equal. let lessThanEqual = ./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 ? ./lessThanEqual diff --git a/dhall-lang/Prelude/Natural/even.dhall b/dhall-lang/Prelude/Natural/even.dhall --- a/dhall-lang/Prelude/Natural/even.dhall +++ b/dhall-lang/Prelude/Natural/even.dhall @@ -1,6 +1,4 @@ -{- -Returns `True` if a number if even and returns `False` otherwise --} +--| Returns `True` if a number if even and returns `False` otherwise let even : Natural → Bool = Natural/even diff --git a/dhall-lang/Prelude/Natural/fold.dhall b/dhall-lang/Prelude/Natural/fold.dhall --- a/dhall-lang/Prelude/Natural/fold.dhall +++ b/dhall-lang/Prelude/Natural/fold.dhall @@ -1,4 +1,4 @@ -{- +{-| `fold` is the primitive function for consuming `Natural` numbers If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just diff --git a/dhall-lang/Prelude/Natural/greaterThan.dhall b/dhall-lang/Prelude/Natural/greaterThan.dhall --- a/dhall-lang/Prelude/Natural/greaterThan.dhall +++ b/dhall-lang/Prelude/Natural/greaterThan.dhall @@ -1,6 +1,4 @@ -{- -`greaterThan` checks if one Natural is strictly greater than another. --} +--| `greaterThan` checks if one Natural is strictly greater than another. let lessThan = ./lessThan sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c ? ./lessThan diff --git a/dhall-lang/Prelude/Natural/greaterThanEqual.dhall b/dhall-lang/Prelude/Natural/greaterThanEqual.dhall --- a/dhall-lang/Prelude/Natural/greaterThanEqual.dhall +++ b/dhall-lang/Prelude/Natural/greaterThanEqual.dhall @@ -1,4 +1,4 @@ -{- +{-| `greaterThanEqual` checks if one Natural is greater than or equal to another. -} let lessThanEqual = diff --git a/dhall-lang/Prelude/Natural/isZero.dhall b/dhall-lang/Prelude/Natural/isZero.dhall --- a/dhall-lang/Prelude/Natural/isZero.dhall +++ b/dhall-lang/Prelude/Natural/isZero.dhall @@ -1,6 +1,4 @@ -{- -Returns `True` if a number is `0` and returns `False` otherwise --} +--| Returns `True` if a number is `0` and returns `False` otherwise let isZero : Natural → Bool = Natural/isZero diff --git a/dhall-lang/Prelude/Natural/lessThan.dhall b/dhall-lang/Prelude/Natural/lessThan.dhall --- a/dhall-lang/Prelude/Natural/lessThan.dhall +++ b/dhall-lang/Prelude/Natural/lessThan.dhall @@ -1,6 +1,4 @@ -{- -`lessThan` checks if one Natural is strictly less than another. --} +--| `lessThan` checks if one Natural is strictly less than another. let greaterThanEqual = ./greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4 ? ./greaterThanEqual diff --git a/dhall-lang/Prelude/Natural/lessThanEqual.dhall b/dhall-lang/Prelude/Natural/lessThanEqual.dhall --- a/dhall-lang/Prelude/Natural/lessThanEqual.dhall +++ b/dhall-lang/Prelude/Natural/lessThanEqual.dhall @@ -1,6 +1,4 @@ -{- -`lessThanEqual` checks if one Natural is less than or equal to another. --} +--| `lessThanEqual` checks if one Natural is less than or equal to another. let lessThanEqual : Natural → Natural → Bool = λ(x : Natural) → λ(y : Natural) → Natural/isZero (Natural/subtract y x) diff --git a/dhall-lang/Prelude/Natural/listMax.dhall b/dhall-lang/Prelude/Natural/listMax.dhall --- a/dhall-lang/Prelude/Natural/listMax.dhall +++ b/dhall-lang/Prelude/Natural/listMax.dhall @@ -1,4 +1,4 @@ -{- +{-| `listMax` returns the largest element of a `List` or `None Natural` if the `List` is empty -} diff --git a/dhall-lang/Prelude/Natural/listMin.dhall b/dhall-lang/Prelude/Natural/listMin.dhall --- a/dhall-lang/Prelude/Natural/listMin.dhall +++ b/dhall-lang/Prelude/Natural/listMin.dhall @@ -1,4 +1,4 @@ -{- +{-| `listMin` returns the smallest element of a `List` or `None Natural` if the `List` is empty -} diff --git a/dhall-lang/Prelude/Natural/max.dhall b/dhall-lang/Prelude/Natural/max.dhall --- a/dhall-lang/Prelude/Natural/max.dhall +++ b/dhall-lang/Prelude/Natural/max.dhall @@ -1,6 +1,4 @@ -{- -`max a b` returns the larger of `a` or `b` --} +--| `max a b` returns the larger of `a` or `b` let lessThanEqual = ./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 ? ./lessThanEqual diff --git a/dhall-lang/Prelude/Natural/min.dhall b/dhall-lang/Prelude/Natural/min.dhall --- a/dhall-lang/Prelude/Natural/min.dhall +++ b/dhall-lang/Prelude/Natural/min.dhall @@ -1,6 +1,4 @@ -{- -`min a b` returns the smaller of `a` or `b` --} +--| `min a b` returns the smaller of `a` or `b` let lessThanEqual = ./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 ? ./lessThanEqual diff --git a/dhall-lang/Prelude/Natural/odd.dhall b/dhall-lang/Prelude/Natural/odd.dhall --- a/dhall-lang/Prelude/Natural/odd.dhall +++ b/dhall-lang/Prelude/Natural/odd.dhall @@ -1,6 +1,4 @@ -{- -Returns `True` if a number is odd and returns `False` otherwise --} +--| Returns `True` if a number is odd and returns `False` otherwise let odd : Natural → Bool = Natural/odd diff --git a/dhall-lang/Prelude/Natural/product.dhall b/dhall-lang/Prelude/Natural/product.dhall --- a/dhall-lang/Prelude/Natural/product.dhall +++ b/dhall-lang/Prelude/Natural/product.dhall @@ -1,6 +1,4 @@ -{- -Multiply all the numbers in a `List` --} +--| Multiply all the numbers in a `List` let product : List Natural → Natural = λ(xs : List Natural) → diff --git a/dhall-lang/Prelude/Natural/show.dhall b/dhall-lang/Prelude/Natural/show.dhall --- a/dhall-lang/Prelude/Natural/show.dhall +++ b/dhall-lang/Prelude/Natural/show.dhall @@ -1,4 +1,4 @@ -{- +{-| Render a `Natural` number as `Text` using the same representation as Dhall source code (i.e. a decimal number) -} diff --git a/dhall-lang/Prelude/Natural/sort.dhall b/dhall-lang/Prelude/Natural/sort.dhall --- a/dhall-lang/Prelude/Natural/sort.dhall +++ b/dhall-lang/Prelude/Natural/sort.dhall @@ -1,6 +1,4 @@ -{- -`sort` sorts a `List` of `Natural`s in ascending order --} +--| `sort` sorts a `List` of `Natural`s in ascending order let greaterThanEqual = ./greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4 ? ./greaterThanEqual diff --git a/dhall-lang/Prelude/Natural/subtract.dhall b/dhall-lang/Prelude/Natural/subtract.dhall --- a/dhall-lang/Prelude/Natural/subtract.dhall +++ b/dhall-lang/Prelude/Natural/subtract.dhall @@ -1,6 +1,4 @@ -{- -`subtract m n` computes `n - m`, truncating to `0` if `m > n` --} +--| `subtract m n` computes `n - m`, truncating to `0` if `m > n` let subtract : Natural → Natural → Natural = Natural/subtract diff --git a/dhall-lang/Prelude/Natural/sum.dhall b/dhall-lang/Prelude/Natural/sum.dhall --- a/dhall-lang/Prelude/Natural/sum.dhall +++ b/dhall-lang/Prelude/Natural/sum.dhall @@ -1,6 +1,4 @@ -{- -Add all the numbers in a `List` --} +--| Add all the numbers in a `List` let sum : List Natural → Natural = λ(xs : List Natural) → diff --git a/dhall-lang/Prelude/Natural/toDouble.dhall b/dhall-lang/Prelude/Natural/toDouble.dhall --- a/dhall-lang/Prelude/Natural/toDouble.dhall +++ b/dhall-lang/Prelude/Natural/toDouble.dhall @@ -1,6 +1,4 @@ -{- -Convert a `Natural` number to the corresponding `Double` --} +--| Convert a `Natural` number to the corresponding `Double` let toDouble : Natural → Double = λ(n : Natural) → Integer/toDouble (Natural/toInteger n) diff --git a/dhall-lang/Prelude/Natural/toInteger.dhall b/dhall-lang/Prelude/Natural/toInteger.dhall --- a/dhall-lang/Prelude/Natural/toInteger.dhall +++ b/dhall-lang/Prelude/Natural/toInteger.dhall @@ -1,6 +1,4 @@ -{- -Convert a `Natural` number to the corresponding `Integer` --} +--| Convert a `Natural` number to the corresponding `Integer` let toInteger : Natural → Integer = Natural/toInteger diff --git a/dhall-lang/Prelude/Optional/all.dhall b/dhall-lang/Prelude/Optional/all.dhall --- a/dhall-lang/Prelude/Optional/all.dhall +++ b/dhall-lang/Prelude/Optional/all.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `False` if the supplied function returns `False` for a present element and `True` otherwise: -} diff --git a/dhall-lang/Prelude/Optional/any.dhall b/dhall-lang/Prelude/Optional/any.dhall --- a/dhall-lang/Prelude/Optional/any.dhall +++ b/dhall-lang/Prelude/Optional/any.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `True` if the supplied function returns `True` for a present element and `False` otherwise -} diff --git a/dhall-lang/Prelude/Optional/build.dhall b/dhall-lang/Prelude/Optional/build.dhall --- a/dhall-lang/Prelude/Optional/build.dhall +++ b/dhall-lang/Prelude/Optional/build.dhall @@ -1,6 +1,4 @@ -{- -`build` is the inverse of `fold` --} +--| `build` is the inverse of `fold` let build : ∀(a : Type) → ( ∀(optional : Type) → diff --git a/dhall-lang/Prelude/Optional/concat.dhall b/dhall-lang/Prelude/Optional/concat.dhall --- a/dhall-lang/Prelude/Optional/concat.dhall +++ b/dhall-lang/Prelude/Optional/concat.dhall @@ -1,6 +1,4 @@ -{- -Flatten two `Optional` layers into a single `Optional` layer --} +--| Flatten two `Optional` layers into a single `Optional` layer let concat : ∀(a : Type) → Optional (Optional a) → Optional a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/default.dhall b/dhall-lang/Prelude/Optional/default.dhall --- a/dhall-lang/Prelude/Optional/default.dhall +++ b/dhall-lang/Prelude/Optional/default.dhall @@ -1,6 +1,4 @@ -{- -Unpack an `Optional`, returning the default when it's `None`. --} +--| Unpack an `Optional`, returning the default when it's `None`. let default : ∀(a : Type) → a → Optional a → a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/filter.dhall b/dhall-lang/Prelude/Optional/filter.dhall --- a/dhall-lang/Prelude/Optional/filter.dhall +++ b/dhall-lang/Prelude/Optional/filter.dhall @@ -1,6 +1,4 @@ -{- -Only keep an `Optional` element if the supplied function returns `True` --} +--| Only keep an `Optional` element if the supplied function returns `True` let filter : ∀(a : Type) → (a → Bool) → Optional a → Optional a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/fold.dhall b/dhall-lang/Prelude/Optional/fold.dhall --- a/dhall-lang/Prelude/Optional/fold.dhall +++ b/dhall-lang/Prelude/Optional/fold.dhall @@ -1,6 +1,4 @@ -{- -`fold` is the primitive function for consuming `Optional` values --} +--| `fold` is the primitive function for consuming `Optional` values let fold : ∀(a : Type) → Optional a → diff --git a/dhall-lang/Prelude/Optional/head.dhall b/dhall-lang/Prelude/Optional/head.dhall --- a/dhall-lang/Prelude/Optional/head.dhall +++ b/dhall-lang/Prelude/Optional/head.dhall @@ -1,6 +1,4 @@ -{- -Returns the first non-empty `Optional` value in a `List` --} +--| Returns the first non-empty `Optional` value in a `List` let head : ∀(a : Type) → List (Optional a) → Optional a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/last.dhall b/dhall-lang/Prelude/Optional/last.dhall --- a/dhall-lang/Prelude/Optional/last.dhall +++ b/dhall-lang/Prelude/Optional/last.dhall @@ -1,6 +1,4 @@ -{- -Returns the last non-empty `Optional` value in a `List` --} +--| Returns the last non-empty `Optional` value in a `List` let last : ∀(a : Type) → List (Optional a) → Optional a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/length.dhall b/dhall-lang/Prelude/Optional/length.dhall --- a/dhall-lang/Prelude/Optional/length.dhall +++ b/dhall-lang/Prelude/Optional/length.dhall @@ -1,4 +1,4 @@ -{- +{-| Returns `1` if the `Optional` value is present and `0` if the value is absent -} let length diff --git a/dhall-lang/Prelude/Optional/map.dhall b/dhall-lang/Prelude/Optional/map.dhall --- a/dhall-lang/Prelude/Optional/map.dhall +++ b/dhall-lang/Prelude/Optional/map.dhall @@ -1,6 +1,4 @@ -{- -Transform an `Optional` value with a function --} +--| Transform an `Optional` value with a function let map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/null.dhall b/dhall-lang/Prelude/Optional/null.dhall --- a/dhall-lang/Prelude/Optional/null.dhall +++ b/dhall-lang/Prelude/Optional/null.dhall @@ -1,6 +1,4 @@ -{- -Returns `True` if the `Optional` value is absent and `False` if present --} +--| Returns `True` if the `Optional` value is absent and `False` if present let null : ∀(a : Type) → Optional a → Bool = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/toList.dhall b/dhall-lang/Prelude/Optional/toList.dhall --- a/dhall-lang/Prelude/Optional/toList.dhall +++ b/dhall-lang/Prelude/Optional/toList.dhall @@ -1,6 +1,4 @@ -{- -Convert an `Optional` value into the equivalent `List` --} +--| Convert an `Optional` value into the equivalent `List` let toList : ∀(a : Type) → Optional a → List a = λ(a : Type) → diff --git a/dhall-lang/Prelude/Optional/unzip.dhall b/dhall-lang/Prelude/Optional/unzip.dhall --- a/dhall-lang/Prelude/Optional/unzip.dhall +++ b/dhall-lang/Prelude/Optional/unzip.dhall @@ -1,6 +1,4 @@ -{- -Unzip an `Optional` value into two separate `Optional` values --} +--| Unzip an `Optional` value into two separate `Optional` values let unzip : ∀(a : Type) → ∀(b : Type) → diff --git a/dhall-lang/Prelude/Text/concat.dhall b/dhall-lang/Prelude/Text/concat.dhall --- a/dhall-lang/Prelude/Text/concat.dhall +++ b/dhall-lang/Prelude/Text/concat.dhall @@ -1,6 +1,4 @@ -{- -Concatenate all the `Text` values in a `List` --} +--| Concatenate all the `Text` values in a `List` let concat : List Text → Text = λ(xs : List Text) → diff --git a/dhall-lang/Prelude/Text/concatMap.dhall b/dhall-lang/Prelude/Text/concatMap.dhall --- a/dhall-lang/Prelude/Text/concatMap.dhall +++ b/dhall-lang/Prelude/Text/concatMap.dhall @@ -1,6 +1,4 @@ -{- -Transform each value in a `List` into `Text` and concatenate the result --} +--| Transform each value in a `List` into `Text` and concatenate the result let concatMap : ∀(a : Type) → (a → Text) → List a → Text = λ(a : Type) → diff --git a/dhall-lang/Prelude/Text/concatMapSep.dhall b/dhall-lang/Prelude/Text/concatMapSep.dhall --- a/dhall-lang/Prelude/Text/concatMapSep.dhall +++ b/dhall-lang/Prelude/Text/concatMapSep.dhall @@ -1,4 +1,4 @@ -{- +{-| Transform each value in a `List` to `Text` and then concatenate them with a separator in between each value -} diff --git a/dhall-lang/Prelude/Text/concatSep.dhall b/dhall-lang/Prelude/Text/concatSep.dhall --- a/dhall-lang/Prelude/Text/concatSep.dhall +++ b/dhall-lang/Prelude/Text/concatSep.dhall @@ -1,6 +1,4 @@ -{- -Concatenate a `List` of `Text` values with a separator in between each value --} +--| Concatenate a `List` of `Text` values with a separator in between each value let Status = < Empty | NonEmpty : Text > let concatSep diff --git a/dhall-lang/Prelude/Text/default.dhall b/dhall-lang/Prelude/Text/default.dhall --- a/dhall-lang/Prelude/Text/default.dhall +++ b/dhall-lang/Prelude/Text/default.dhall @@ -1,6 +1,4 @@ -{- -Unwrap an `Optional` `Text` value, defaulting `None` to `""` --} +--| Unwrap an `Optional` `Text` value, defaulting `None` to `""` let default : Optional Text → Text = λ(o : Optional Text) → merge { Some = λ(t : Text) → t, None = "" } o diff --git a/dhall-lang/Prelude/Text/defaultMap.dhall b/dhall-lang/Prelude/Text/defaultMap.dhall --- a/dhall-lang/Prelude/Text/defaultMap.dhall +++ b/dhall-lang/Prelude/Text/defaultMap.dhall @@ -1,6 +1,4 @@ -{- -Transform the value in an `Optional` into `Text`, defaulting `None` to `""` --} +--| Transform the value in an `Optional` into `Text`, defaulting `None` to `""` let defaultMap : ∀(a : Type) → (a → Text) → Optional a → Text = λ(a : Type) → diff --git a/dhall-lang/Prelude/Text/replicate.dhall b/dhall-lang/Prelude/Text/replicate.dhall --- a/dhall-lang/Prelude/Text/replicate.dhall +++ b/dhall-lang/Prelude/Text/replicate.dhall @@ -1,6 +1,4 @@ -{- -Build a Text by copying the given Text the specified number of times --} +--| Build a Text by copying the given Text the specified number of times let concat = ./concat sha256:731265b0288e8a905ecff95c97333ee2db614c39d69f1514cb8eed9259745fc0 diff --git a/dhall-lang/Prelude/Text/spaces.dhall b/dhall-lang/Prelude/Text/spaces.dhall --- a/dhall-lang/Prelude/Text/spaces.dhall +++ b/dhall-lang/Prelude/Text/spaces.dhall @@ -1,8 +1,8 @@ -{- +{-| Return a Text with the number of spaces specified. -This function is particularly helpful when trying to generate Text where whitespace -is significant, i.e. with nested indentation. +This function is particularly helpful when trying to generate Text where +whitespace is significant, i.e. with nested indentation. -} let replicate = diff --git a/dhall-lang/Prelude/XML/Type.dhall b/dhall-lang/Prelude/XML/Type.dhall --- a/dhall-lang/Prelude/XML/Type.dhall +++ b/dhall-lang/Prelude/XML/Type.dhall @@ -1,12 +1,13 @@ -{- Dhall encoding of an arbitrary XML element +{-| +Dhall encoding of an arbitrary XML element - For example, the following XML element: +For example, the following XML element: ``` baz ``` - ... corresponds to the following Dhall expression: +... corresponds to the following Dhall expression: ``` diff --git a/dhall-lang/Prelude/XML/attribute.dhall b/dhall-lang/Prelude/XML/attribute.dhall --- a/dhall-lang/Prelude/XML/attribute.dhall +++ b/dhall-lang/Prelude/XML/attribute.dhall @@ -1,4 +1,4 @@ -{- Builds a key-value record with a Text key and value. -} +--| Builds a key-value record with a Text key and value. let attribute : Text → Text → { mapKey : Text, mapValue : Text } diff --git a/dhall-lang/Prelude/XML/element.dhall b/dhall-lang/Prelude/XML/element.dhall --- a/dhall-lang/Prelude/XML/element.dhall +++ b/dhall-lang/Prelude/XML/element.dhall @@ -1,4 +1,5 @@ -{- Create an XML element value. +{-| +Create an XML element value. ``` let XML = ./package.dhall diff --git a/dhall-lang/Prelude/XML/emptyAttributes.dhall b/dhall-lang/Prelude/XML/emptyAttributes.dhall --- a/dhall-lang/Prelude/XML/emptyAttributes.dhall +++ b/dhall-lang/Prelude/XML/emptyAttributes.dhall @@ -1,3 +1,3 @@ -{- Create an empty XML attribute List. -} +--| Create an empty XML attribute List. [] : List { mapKey : Text, mapValue : Text } diff --git a/dhall-lang/Prelude/XML/leaf.dhall b/dhall-lang/Prelude/XML/leaf.dhall --- a/dhall-lang/Prelude/XML/leaf.dhall +++ b/dhall-lang/Prelude/XML/leaf.dhall @@ -1,4 +1,5 @@ -{- Create an XML element value without child elements. +{-| +Create an XML element value without child elements. ``` let XML = ./package.dhall diff --git a/dhall-lang/Prelude/XML/render.dhall b/dhall-lang/Prelude/XML/render.dhall --- a/dhall-lang/Prelude/XML/render.dhall +++ b/dhall-lang/Prelude/XML/render.dhall @@ -1,11 +1,12 @@ -{- Render an `XML` value as `Text` +{-| +Render an `XML` value as `Text` - *WARNING:* rendering does not include any XML injection mitigations, - therefore it should not be used to process arbitrary strings into - element attributes or element data. +*WARNING:* rendering does not include any XML injection mitigations, +therefore it should not be used to process arbitrary strings into +element attributes or element data. - For indentation and schema validation, see the `xmllint` utility - bundled with libxml2. +For indentation and schema validation, see the `xmllint` utility +bundled with libxml2. ``` let XML = ./package.dhall diff --git a/dhall-lang/Prelude/XML/text.dhall b/dhall-lang/Prelude/XML/text.dhall --- a/dhall-lang/Prelude/XML/text.dhall +++ b/dhall-lang/Prelude/XML/text.dhall @@ -1,4 +1,5 @@ -{- Create a Text value to be inserted into an XML element as content. +{-| +Create a Text value to be inserted into an XML element as content. ``` let XML = ./package.dhall diff --git a/dhall-lang/tests/normalization/success/unit/WithDesugarA.dhall b/dhall-lang/tests/normalization/success/unit/WithDesugarA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/unit/WithDesugarA.dhall @@ -0,0 +1,4 @@ +{- This test verifies that an implementation desugars `with` correctly by + leaving `x` abstract +-} +\(x: { a : { b : { c : {} } }}) -> x with a.b.c = 42 diff --git a/dhall-lang/tests/normalization/success/unit/WithDesugarB.dhall b/dhall-lang/tests/normalization/success/unit/WithDesugarB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/unit/WithDesugarB.dhall @@ -0,0 +1,1 @@ +λ(x : { a : { b : { c : {} } } }) → x ⫽ { a = x.a ⫽ { b = x.a.b ⫽ { c = 42 } } } diff --git a/dhall-lang/tests/normalization/success/unit/WithUnderscoreA.dhall b/dhall-lang/tests/normalization/success/unit/WithUnderscoreA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/unit/WithUnderscoreA.dhall @@ -0,0 +1,5 @@ +{- This test checks that an implementation doesn't mistakenly implement the + optimization suggested by the standard without the requisite shift + judgment +-} +let _ = 1 in {=} with a = _ diff --git a/dhall-lang/tests/normalization/success/unit/WithUnderscoreB.dhall b/dhall-lang/tests/normalization/success/unit/WithUnderscoreB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/unit/WithUnderscoreB.dhall @@ -0,0 +1,1 @@ +{ a = 1 } diff --git a/dhall-lang/tests/parser/success/unit/WithA.dhall b/dhall-lang/tests/parser/success/unit/WithA.dhall --- a/dhall-lang/tests/parser/success/unit/WithA.dhall +++ b/dhall-lang/tests/parser/success/unit/WithA.dhall @@ -1,6 +1,1 @@ -{- The purpose of this test is to verify that an implementation correctly - desugars the base case of a non-nested update. Specifically, an - implementation should not use an intermediate `let` when desugaring this - base case. --} { a = 1 } with a = 2 diff --git a/dhall-lang/tests/parser/success/unit/WithB.dhallb b/dhall-lang/tests/parser/success/unit/WithB.dhallb --- a/dhall-lang/tests/parser/success/unit/WithB.dhallb +++ b/dhall-lang/tests/parser/success/unit/WithB.dhallb @@ -1,1 +1,1 @@ -„ ‚¡aa‚‚¡aa‚ +„‚¡aa‚aa‚ diff --git a/dhall-lang/tests/parser/success/unit/WithMultipleA.dhall b/dhall-lang/tests/parser/success/unit/WithMultipleA.dhall --- a/dhall-lang/tests/parser/success/unit/WithMultipleA.dhall +++ b/dhall-lang/tests/parser/success/unit/WithMultipleA.dhall @@ -1,8 +1,4 @@ -{- This test ensures that `with` is purely syntactic sugar, meaning that it is - desugared before encoding and therefore is encoded as the desugared expression - in the CBOR encoding. - - This test also ensures that implementations desugar the code exactly as - specified (e.g. using an intermediate `let` binding) +{- This test verifies that an implementation correctly encodes chained + `with` expressions in a left-associative way. -} { a.b = 1, c.d = 2 } with a.b = 3 with c.e = 4 diff --git a/dhall-lang/tests/parser/success/unit/WithMultipleB.dhallb b/dhall-lang/tests/parser/success/unit/WithMultipleB.dhallb --- a/dhall-lang/tests/parser/success/unit/WithMultipleB.dhallb +++ b/dhall-lang/tests/parser/success/unit/WithMultipleB.dhallb @@ -1,1 +1,1 @@ -„ „ ‚¢aa‚¡ab‚ac‚¡ad‚‚¡aa„ ƒ ‚¢aa‚¡ab‚ac‚¡ad‚aa‚¡ab‚‚¡ac„ ƒ „ ‚¢aa‚¡ab‚ac‚¡ad‚‚¡aa„ ƒ ‚¢aa‚¡ab‚ac‚¡ad‚aa‚¡ab‚ac‚¡ae‚ +„„‚¢aa‚¡ab‚ac‚¡ad‚‚aaab‚‚acae‚ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb --- a/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb +++ b/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb @@ -1,1 +1,1 @@ -„ „ ‚¡aaƒö‚‚¡aaƒö‚‚¡aaƒö‚ +„„‚¡aaƒö‚aaƒö‚aaƒö‚ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb Binary files a/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb and b/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb Binary files a/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb and b/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb differ diff --git a/dhall-lang/tests/type-inference/success/unit/WithNestedA.dhall b/dhall-lang/tests/type-inference/success/unit/WithNestedA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/WithNestedA.dhall @@ -0,0 +1,4 @@ +{- This test illustrates that the `with` keyword is permitted to override + existing fields nested within a child record +-} +{ a = { p = 2, q = "hi" }, b = 5.6 } with a.p = True diff --git a/dhall-lang/tests/type-inference/success/unit/WithNestedB.dhall b/dhall-lang/tests/type-inference/success/unit/WithNestedB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/WithNestedB.dhall @@ -0,0 +1,1 @@ +{ a : { p : Bool, q : Text }, b : Double } diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.34.0 +Version: 1.35.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 8.4.3, GHC == 8.6.1 @@ -455,6 +455,12 @@ Default: True Manual: True +Flag use-http-client-tls + Description: Use http-client-tls for resolving HTTP imports by default + (requires with-http to be enabled) + Default: True + Manual: True + Flag cross Description: Disable TemplateHaskell to make cross-compiling easier Default: False @@ -466,7 +472,7 @@ base >= 4.11.0.0 && < 5 , aeson >= 1.0.0.0 && < 1.6 , aeson-pretty < 0.9 , - ansi-terminal >= 0.6.3.1 && < 0.11, + ansi-terminal >= 0.6.3.1 && < 0.12, atomic-write >= 0.2.0.7 && < 0.3 , bytestring < 0.11, case-insensitive < 1.3 , @@ -486,12 +492,12 @@ haskeline >= 0.7.2.1 && < 0.9 , hashable >= 1.2 && < 1.4 , lens-family-core >= 1.0.0 && < 2.2 , - megaparsec >= 7 && < 8.1 , + megaparsec >= 7 && < 9.1 , memory >= 0.14 && < 0.16, mmorph < 1.2 , mtl >= 2.2.1 && < 2.3 , network-uri >= 2.6 && < 2.7 , - optparse-applicative >= 0.14.0.0 && < 0.16, + optparse-applicative >= 0.14.0.0 && < 0.17, parsers >= 0.12.4 && < 0.13, parser-combinators , prettyprinter >= 1.5.1 && < 1.8 , @@ -513,6 +519,9 @@ if flag(with-http) CPP-Options: -DWITH_HTTP + if flag(use-http-client-tls) + CPP-Options: + -DUSE_HTTP_CLIENT_TLS if impl(ghcjs) Hs-Source-Dirs: ghcjs-src Build-Depends: @@ -525,8 +534,10 @@ if flag(with-http) Build-Depends: http-types >= 0.7.0 && < 0.13, - http-client >= 0.5.0 && < 0.8 , - http-client-tls >= 0.2.0 && < 0.4 + http-client >= 0.5.0 && < 0.8 + if flag(use-http-client-tls) + Build-Depends: + http-client-tls >= 0.2.0 && < 0.4 Other-Extensions: BangPatterns @@ -660,7 +671,6 @@ QuickCheck >= 2.10 && < 2.15, quickcheck-instances >= 0.3.12 && < 0.4 , scientific , - semigroups , serialise , special-values < 0.2 , spoon < 0.4 , @@ -668,6 +678,7 @@ tasty-expected-failure < 0.13, tasty-hunit >= 0.10 && < 0.11, tasty-quickcheck >= 0.9.2 && < 0.11, + tasty-silver < 3.2 , template-haskell , text >= 0.11.1.0 && < 1.3 , transformers , @@ -703,12 +714,11 @@ dhall , directory , gauge >= 0.2.3 && < 0.3, - serialise , text >= 0.11.1.0 && < 1.3 Default-Language: Haskell2010 Other-Extensions: TypeApplications - ghc-options: -rtsopts + ghc-options: -rtsopts -Wall Benchmark deep-nested-large-record Type: exitcode-stdio-1.0 @@ -720,3 +730,4 @@ dhall , gauge >= 0.2.3 && < 0.3 Default-Language: Haskell2010 + ghc-options: -Wall diff --git a/doctest/Main.hs b/doctest/Main.hs --- a/doctest/Main.hs +++ b/doctest/Main.hs @@ -33,6 +33,7 @@ Test.DocTest.doctest [ "-DWITH_HTTP" + , "-DUSE_HTTP_CLIENT_TLS" , "--fast" , prefix "ghc-src" diff --git a/ghc-src/Dhall/Crypto.hs b/ghc-src/Dhall/Crypto.hs --- a/ghc-src/Dhall/Crypto.hs +++ b/ghc-src/Dhall/Crypto.hs @@ -9,6 +9,7 @@ SHA256Digest(..) , sha256DigestFromByteString , sha256Hash + , toString ) where import Control.DeepSeq (NFData) @@ -26,7 +27,7 @@ deriving (Eq, Generic, Ord, NFData, ByteArrayAccess) instance Show SHA256Digest where - show (SHA256Digest bytes) = ByteString.Char8.unpack $ convertToBase Base16 bytes + show = toString {-| Attempt to interpret a `ByteString` as a `SHA256Digest`, returning `Nothing` if the conversion fails @@ -41,3 +42,7 @@ sha256Hash bytes = SHA256Digest $ convert h where h = Crypto.Hash.hash bytes :: Crypto.Hash.Digest SHA256 + +-- | 'String' representation of a 'SHA256Digest' +toString :: SHA256Digest -> String +toString (SHA256Digest bytes) = ByteString.Char8.unpack $ convertToBase Base16 bytes diff --git a/ghc-src/Dhall/Import/HTTP.hs b/ghc-src/Dhall/Import/HTTP.hs --- a/ghc-src/Dhall/Import/HTTP.hs +++ b/ghc-src/Dhall/Import/HTTP.hs @@ -25,7 +25,6 @@ import Network.HTTP.Client ( HttpException (..) , HttpExceptionContent (..) - , Manager ) import qualified Control.Exception @@ -37,7 +36,6 @@ import qualified Data.Text.Lazy.Encoding import qualified Dhall.Util import qualified Network.HTTP.Client as HTTP -import qualified Network.HTTP.Client.TLS as HTTP import qualified Network.HTTP.Types mkPrettyHttpException :: String -> HttpException -> PrettyHttpException @@ -147,14 +145,11 @@ newManager :: StateT Status IO Manager newManager = do - let settings = HTTP.tlsManagerSettings - { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro (30 * 1000 * 1000) } -- 30 seconds - Status { _manager = oldManager, ..} <- State.get case oldManager of Nothing -> do - manager <- liftIO (HTTP.newManager settings) + manager <- liftIO _newManager State.put (Status { _manager = Just manager , ..}) diff --git a/ghc-src/Dhall/Import/Manager.hs b/ghc-src/Dhall/Import/Manager.hs --- a/ghc-src/Dhall/Import/Manager.hs +++ b/ghc-src/Dhall/Import/Manager.hs @@ -1,14 +1,33 @@ -{-| Both the GHC and GHCJS implementations of "Dhall.Import.Manager" export a - `Manager` type suitable for use within the "Dhall.Import" module +{-# LANGUAGE CPP #-} - For the GHC implementation the `Manager` type is a real `Manager` from the - @http-client@ package. For the GHCJS implementation the `Manager` type is - a synonym for @`Data.Void.Void`@ since GHCJS does not use a `Manager` for - HTTP requests. +{-| Both the GHC and GHCJS implementations of 'Dhall.Import.Manager.Manager' + export a `Dhall.Import.Manager.Manager` type suitable for use within the + "Dhall.Import" module + + For the GHC implementation the `Dhall.Import.Manager` type is a real + `Network.HTTP.Client.Manager` from the @http-client@ package. For the + GHCJS implementation the `Dhall.Import.Manager.Manager` type is + a synonym for @`Data.Void.Void`@ since GHCJS does not use a + `Network.HTTP.Client.Manager` for HTTP requests. -} module Dhall.Import.Manager ( -- * Manager Manager + , defaultNewManager ) where -import Network.HTTP.Client (Manager) +import Network.HTTP.Client (Manager, newManager) +import qualified Network.HTTP.Client as HTTP + +#ifdef USE_HTTP_CLIENT_TLS +import Network.HTTP.Client.TLS (tlsManagerSettings) +#endif + +defaultNewManager :: IO Manager +defaultNewManager = newManager +#ifdef USE_HTTP_CLIENT_TLS + tlsManagerSettings +#else + HTTP.defaultManagerSettings +#endif + { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro (30 * 1000 * 1000) } -- 30 seconds diff --git a/ghcjs-src/Dhall/Import/HTTP.hs b/ghcjs-src/Dhall/Import/HTTP.hs --- a/ghcjs-src/Dhall/Import/HTTP.hs +++ b/ghcjs-src/Dhall/Import/HTTP.hs @@ -2,29 +2,18 @@ module Dhall.Import.HTTP ( fetchFromHttpUrl - , Manager ) where import Control.Monad.IO.Class (MonadIO (..)) import Control.Monad.Trans.State.Strict (StateT) import Data.ByteString (ByteString) import Data.CaseInsensitive (CI) -import Data.Void (Void) import Dhall.Core (URL (..)) -import Dhall.Import.Types +import Dhall.Import.Types (Status) import Dhall.URL (renderURL) import qualified Data.Text as Text import qualified JavaScript.XHR - - -{-| The GHCJS implementation does not require a `Manager` - - The purpose of this synonym is so that "Dhall.Import.Types" can import a - `Manager` type from "Dhall.Import.HTTP" that does the correct thing for - both the GHC and GHCJS implementations --} -type Manager = Void fetchFromHttpUrl :: URL diff --git a/ghcjs-src/Dhall/Import/Manager.hs b/ghcjs-src/Dhall/Import/Manager.hs --- a/ghcjs-src/Dhall/Import/Manager.hs +++ b/ghcjs-src/Dhall/Import/Manager.hs @@ -1,17 +1,26 @@ -{-| Both the GHC and GHCJS implementations of "Dhall.Import.Manager" export a - `Manager` type suitable for use within the "Dhall.Import" module +{-| Both the GHC and GHCJS implementations of `Dhall.Import.Manager.Manager` + export a `Dhall.Import.Manager.Manager` type suitable for use within the + "Dhall.Import" module - For the GHC implementation the `Manager` type is a real `Manager` from the - @http-client@ package. For the GHCJS implementation the `Manager` type is - a synonym for @`Data.Void.Void`@ since GHCJS does not use a `Manager` for - HTTP requests. + For the GHC implementation the `Dhall.Import.Manager.Manager` type is a real + `Network.HTTP.Client.Manager` from the @http-client@ package. For the GHCJS + implementation the `Dhall.Import.Manager.Manager` type is a synonym for + @`Data.Void.Void`@ since GHCJS does not use a + `Network.HTTP.Client.Manager` for HTTP requests. -} module Dhall.Import.Manager ( -- * Manager Manager + , defaultNewManager ) where -import Data.Void (Void) +{-| The GHCJS implementation does not require a `Network.HTTP.Client.Manager` --- | GHCJS does not use a `Manager` -type Manager = Void + The purpose of this synonym is so that "Dhall.Import.Types" can import a + `Dhall.Import.Manager.Manager` type from "Dhall.Import.HTTP" that does the + correct thing for both the GHC and GHCJS implementations +-} +type Manager = () + +defaultNewManager :: IO Manager +defaultNewManager = pure () diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -13,9 +13,11 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} {-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining how to use the language, the compiler, and this library @@ -35,11 +37,12 @@ , startingContext , substitutions , normalizer + , newManager , defaultInputSettings , InputSettings , defaultEvaluateSettings , EvaluateSettings - , HasEvaluateSettings + , HasEvaluateSettings(..) , detailed -- * Decoders @@ -72,6 +75,16 @@ , bool , natural , integer + , word + , word8 + , word16 + , word32 + , word64 + , int + , int8 + , int16 + , int32 + , int64 , scientific , double , lazyText @@ -98,7 +111,7 @@ , union , constructor , GenericFromDhall(..) - + , GenericFromDhallUnion(..) , ToDhall(..) , Inject , inject @@ -121,6 +134,7 @@ , rawInput , (>$<) , (>*<) + , Result -- * Re-exports , Natural @@ -154,13 +168,15 @@ import Data.Typeable (Proxy (..), Typeable) import Data.Vector (Vector) import Data.Void (Void) -import Data.Word (Word16, Word32, Word64, Word8) +import Data.Word (Word8, Word16, Word32, Word64) +import Data.Int (Int8, Int16, Int32, Int64) import Dhall.Import (Imported (..)) import Dhall.Parser (Src (..)) import Dhall.Syntax ( Chunks (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , RecordField (..) , Var (..) ) @@ -245,7 +261,7 @@ Failure e -> fmap ExpectedTypeError e Success expected' -> DhallErrors $ pure $ TypeMismatch $ InvalidDecoder expected' actual --- | Turn a `Text` message into an extraction failure +-- | Turn a `Data.Text.Text` message into an extraction failure extractError :: Text -> Extractor s a b extractError = Failure . DhallErrors . pure . ExtractError @@ -310,12 +326,17 @@ instance (Pretty s, Pretty a, Typeable s, Typeable a) => Exception (ExtractError s a) -{-| Every `Decoder` must obey the contract that if an expression's type matches the - the `expected` type then the `extract` function must not fail with a type error. - If not, then this value is returned. +{-| Every `Decoder` must obey the contract that if an expression's type matches + the `expected` type then the `extract` function must not fail with a type + error. However, decoding may still fail for other reasons (such as the + decoder for `Data.Map.Set`s rejecting a Dhall @List@ with duplicate + elements). - This value indicates that an invalid `Decoder` was provided to the `input` - function + This error type is used to indicate an internal error in the implementation + of a `Decoder` where the expected type matched the Dhall expression, but the + expression supplied to the extraction function did not match the expected + type. If this happens that means that the `Decoder` itself needs to be + fixed. -} data InvalidDecoder s a = InvalidDecoder { invalidDecoderExpected :: Expr s a @@ -366,6 +387,7 @@ , _evaluateSettings = defaultEvaluateSettings } + -- | Access the directory to resolve imports relative to. -- -- @since 1.16 @@ -391,6 +413,7 @@ { _substitutions :: Dhall.Substitution.Substitutions Src Void , _startingContext :: Dhall.Context.Context (Expr Src Void) , _normalizer :: Maybe (Core.ReifiedNormalizer Void) + , _newManager :: IO Dhall.Import.Manager } -- | Default evaluation settings: no extra entries in the initial @@ -402,6 +425,7 @@ { _substitutions = Dhall.Substitution.empty , _startingContext = Dhall.Context.empty , _normalizer = Nothing + , _newManager = Dhall.Import.defaultNewManager } -- | Access the starting context used for evaluation and type-checking. @@ -440,6 +464,18 @@ => LensLike' f EvaluateSettings (Maybe (Core.ReifiedNormalizer Void)) l k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s)) +-- | Access the HTTP manager initializer. +-- +-- @since 1.36 +newManager + :: (Functor f, HasEvaluateSettings s) + => LensLike' f s (IO Dhall.Import.Manager) +newManager = evaluateSettings . l + where + l :: (Functor f) + => LensLike' f EvaluateSettings (IO Dhall.Import.Manager) + l k s = fmap (\x -> s { _newManager = x }) (k (_newManager s)) + -- | @since 1.16 class HasEvaluateSettings s where evaluateSettings @@ -603,7 +639,7 @@ . Lens.Family.set Dhall.Import.normalizer _normalizer . Lens.Family.set Dhall.Import.startingContext _startingContext - let status = transform (Dhall.Import.emptyStatus _rootDirectory) + let status = transform (Dhall.Import.emptyStatusWithManager _newManager _rootDirectory) expr' <- State.evalStateT (Dhall.Import.loadWith expr) status @@ -616,7 +652,7 @@ -- The intended use case is to allow easy extraction of Dhall values for -- making the function `Core.normalizeWith` easier to use. -- --- For other use cases, use `input` from `Dhall` module. It will give you +-- For other use cases, use `input` from "Dhall" module. It will give you -- a much better user experience. rawInput :: Alternative f @@ -771,7 +807,7 @@ } deriving (Functor) -{-| Decode a `Bool` +{-| Decode a `Prelude.Bool` >>> input bool "True" True @@ -784,7 +820,7 @@ expected = pure Bool -{-| Decode a `Natural` +{-| Decode a `Prelude.Natural` >>> input natural "42" 42 @@ -797,7 +833,7 @@ expected = pure Natural -{-| Decode an `Integer` +{-| Decode an `Prelude.Integer` >>> input integer "+42" 42 @@ -810,7 +846,114 @@ expected = pure Integer +wordHelper :: forall a . (Bounded a, Integral a) => Text -> Decoder a +wordHelper name = Decoder {..} + where + extract (NaturalLit n) + | toInteger n <= toInteger (maxBound @a) = + pure (fromIntegral n) + | otherwise = + extractError ("Decoded " <> name <> " is out of bounds: " <> Data.Text.pack (show n)) + extract expr = + typeError expected expr + + expected = pure Natural + +{-| Decode a `Word` from a Dhall @Natural@ + +>>> input word "42" +42 +-} +word :: Decoder Word +word = wordHelper "Word" + +{-| Decode a `Word8` from a Dhall @Natural@ + +>>> input word8 "42" +42 +-} +word8 :: Decoder Word8 +word8 = wordHelper "Word8" + +{-| Decode a `Word16` from a Dhall @Natural@ + +>>> input word16 "42" +42 +-} +word16 :: Decoder Word16 +word16 = wordHelper "Word16" + +{-| Decode a `Word32` from a Dhall @Natural@ + +>>> input word32 "42" +42 +-} +word32 :: Decoder Word32 +word32 = wordHelper "Word32" + +{-| Decode a `Word64` from a Dhall @Natural@ + +>>> input word64 "42" +42 +-} +word64 :: Decoder Word64 +word64 = wordHelper "Word64" + +intHelper :: forall a . (Bounded a, Integral a) => Text -> Decoder a +intHelper name = Decoder {..} + where + extract (IntegerLit n) + | toInteger (minBound @a) <= n && n <= toInteger (maxBound @a) = + pure (fromIntegral n) + | otherwise = + extractError ("Decoded " <> name <> " is out of bounds: " <> Data.Text.pack (show n)) + extract expr = + typeError expected expr + + expected = pure Integer + +{-| Decode an `Int` from a Dhall @Integer@ + +>>> input int "-42" +-42 +-} +int :: Decoder Int +int = intHelper "Int" + +{-| Decode an `Int8` from a Dhall @Integer@ + +>>> input int8 "-42" +-42 +-} +int8 :: Decoder Int8 +int8 = intHelper "Int8" + +{-| Decode an `Int16` from a Dhall @Integer@ + +>>> input int16 "-42" +-42 +-} +int16 :: Decoder Int16 +int16 = intHelper "Int16" + +{-| Decode an `Int32` from a Dhall @Integer@ + +>>> input int32 "-42" +-42 +-} +int32 :: Decoder Int32 +int32 = intHelper "Int32" + +{-| Decode an `Int64` from a Dhall @Integer@ + +>>> input int64 "-42" +-42 +-} +int64 :: Decoder Int64 +int64 = intHelper "Int64" + {-| Decode a `Scientific` +r >>> input scientific "1e100" 1.0e100 @@ -818,7 +961,7 @@ scientific :: Decoder Scientific scientific = fmap Data.Scientific.fromFloatDigits double -{-| Decode a `Double` +{-| Decode a `Prelude.Double` >>> input double "42.0" 42.0 @@ -831,7 +974,7 @@ expected = pure Double -{-| Decode lazy `Text` +{-| Decode lazy `Data.Text.Text` >>> input lazyText "\"Test\"" "Test" @@ -839,7 +982,7 @@ lazyText :: Decoder Data.Text.Lazy.Text lazyText = fmap Data.Text.Lazy.fromStrict strictText -{-| Decode strict `Text` +{-| Decode strict `Data.Text.Text` >>> input strictText "\"Test\"" "Test" @@ -933,7 +1076,7 @@ expectedOut = Pi "_" declared <$> expectedIn -{-| Decode a `Set` from a `List` +{-| Decode a `Data.Set.Set` from a `List` >>> input (setIgnoringDuplicates natural) "[1, 2, 3]" fromList [1,2,3] @@ -947,7 +1090,7 @@ setIgnoringDuplicates :: (Ord a) => Decoder a -> Decoder (Data.Set.Set a) setIgnoringDuplicates = fmap Data.Set.fromList . list -{-| Decode a `HashSet` from a `List` +{-| Decode a `Data.HashSet.HashSet` from a `List` >>> input (hashSetIgnoringDuplicates natural) "[1, 2, 3]" fromList [1,2,3] @@ -963,7 +1106,7 @@ -> Decoder (Data.HashSet.HashSet a) hashSetIgnoringDuplicates = fmap Data.HashSet.fromList . list -{-| Decode a `Set` from a `List` with distinct elements +{-| Decode a `Data.Set.Set` from a `List` with distinct elements >>> input (setFromDistinctList natural) "[1, 2, 3]" fromList [1,2,3] @@ -992,7 +1135,7 @@ setFromDistinctList :: (Ord a, Show a) => Decoder a -> Decoder (Data.Set.Set a) setFromDistinctList = setHelper Data.Set.size Data.Set.fromList -{-| Decode a `HashSet` from a `List` with distinct elements +{-| Decode a `Data.HashSet.HashSet` from a `List` with distinct elements >>> input (hashSetFromDistinctList natural) "[1, 2, 3]" fromList [1,2,3] @@ -1201,9 +1344,39 @@ instance FromDhall Natural where autoWith _ = natural +instance FromDhall Word where + autoWith _ = word + +instance FromDhall Word8 where + autoWith _ = word8 + +instance FromDhall Word16 where + autoWith _ = word16 + +instance FromDhall Word32 where + autoWith _ = word32 + +instance FromDhall Word64 where + autoWith _ = word64 + instance FromDhall Integer where autoWith _ = integer +instance FromDhall Int where + autoWith _ = int + +instance FromDhall Int8 where + autoWith _ = int8 + +instance FromDhall Int16 where + autoWith _ = int16 + +instance FromDhall Int32 where + autoWith _ = int32 + +instance FromDhall Int64 where + autoWith _ = int64 + instance FromDhall Scientific where autoWith _ = scientific @@ -1361,10 +1534,12 @@ where die = typeError expected expr0 - extract0 (Lam x _ expr) = extract1 (rename x "result" expr) + extract0 (Lam (FunctionBinding { functionBindingVariable = x }) expr) = + extract1 (rename x "result" expr) extract0 _ = die - extract1 (Lam y _ expr) = extract2 (rename y "Make" expr) + extract1 (Lam (FunctionBinding { functionBindingVariable = y }) expr) = + extract2 (rename y "Make" expr) extract1 _ = die extract2 expr = fmap resultToFix (Dhall.extract (autoWith inputNormalizer) expr) @@ -1496,9 +1671,9 @@ :: Text -> Expr Src Void -> (Text, Maybe (Expr Src Void)) -unsafeExpectUnionLit _ (Field (Union _) k) = +unsafeExpectUnionLit _ (Field (Union _) (Core.fieldSelectionLabel -> k)) = (k, Nothing) -unsafeExpectUnionLit _ (App (Field (Union _) k) v) = +unsafeExpectUnionLit _ (App (Field (Union _) (Core.fieldSelectionLabel -> k)) v) = (k, Just v) unsafeExpectUnionLit name expression = Core.internalError @@ -1523,13 +1698,16 @@ _ -> Just e extractUnionConstructor :: Expr s a -> Maybe (Text, Expr s a, Dhall.Map.Map Text (Maybe (Expr s a))) -extractUnionConstructor (App (Field (Union kts) fld) e) = +extractUnionConstructor (App (Field (Union kts) (Core.fieldSelectionLabel -> fld)) e) = return (fld, e, Dhall.Map.delete fld kts) -extractUnionConstructor (Field (Union kts) fld) = +extractUnionConstructor (Field (Union kts) (Core.fieldSelectionLabel -> fld)) = return (fld, RecordLit mempty, Dhall.Map.delete fld kts) extractUnionConstructor _ = empty +{-| This is the underlying class that powers the `FromDhall` class's support + for automatically deriving a generic implementation for a union type +-} class GenericFromDhallUnion t f where genericUnionAutoWithNormalizer :: Proxy t -> InputNormalizer -> InterpretOptions -> UnionDecoder (f a) @@ -2130,16 +2308,16 @@ embed (L1 (M1 l)) = case notEmptyRecordLit (embedL l) of Nothing -> - Field declared keyL + Field declared $ Core.makeFieldSelection keyL Just valL -> - App (Field declared keyL) valL + App (Field declared $ Core.makeFieldSelection keyL) valL embed (R1 (M1 r)) = case notEmptyRecordLit (embedR r) of Nothing -> - Field declared keyR + Field declared $ Core.makeFieldSelection keyR Just valR -> - App (Field declared keyR) valR + App (Field declared $ Core.makeFieldSelection keyR) valR declared = Union @@ -2166,15 +2344,15 @@ where embed (L1 l) = case maybeValL of - Nothing -> Field declared keyL - Just valL -> App (Field declared keyL) valL + Nothing -> Field declared $ Core.makeFieldSelection keyL + Just valL -> App (Field declared $ Core.makeFieldSelection keyL) valL where (keyL, maybeValL) = unsafeExpectUnionLit "genericToDhallWithNormalizer (:+:)" (embedL l) embed (R1 (M1 r)) = case notEmptyRecordLit (embedR r) of - Nothing -> Field declared keyR - Just valR -> App (Field declared keyR) valR + Nothing -> Field declared $ Core.makeFieldSelection keyR + Just valR -> App (Field declared $ Core.makeFieldSelection keyR) valR nR :: M1 i c h a nR = undefined @@ -2193,12 +2371,12 @@ where embed (L1 (M1 l)) = case notEmptyRecordLit (embedL l) of - Nothing -> Field declared keyL - Just valL -> App (Field declared keyL) valL + Nothing -> Field declared $ Core.makeFieldSelection keyL + Just valL -> App (Field declared $ Core.makeFieldSelection keyL) valL embed (R1 r) = case maybeValR of - Nothing -> Field declared keyR - Just valR -> App (Field declared keyR) valR + Nothing -> Field declared $ Core.makeFieldSelection keyR + Just valR -> App (Field declared $ Core.makeFieldSelection keyR) valR where (keyR, maybeValR) = unsafeExpectUnionLit "genericToDhallWithNormalizer (:+:)" (embedR r) @@ -2220,15 +2398,15 @@ where embed (L1 l) = case maybeValL of - Nothing -> Field declared keyL - Just valL -> App (Field declared keyL) valL + Nothing -> Field declared $ Core.makeFieldSelection keyL + Just valL -> App (Field declared $ Core.makeFieldSelection keyL) valL where (keyL, maybeValL) = unsafeExpectUnionLit "genericToDhallWithNormalizer (:+:)" (embedL l) embed (R1 r) = case maybeValR of - Nothing -> Field declared keyR - Just valR -> App (Field declared keyR) valR + Nothing -> Field declared $ Core.makeFieldSelection keyR + Just valR -> App (Field declared $ Core.makeFieldSelection keyR) valR where (keyR, maybeValR) = unsafeExpectUnionLit "genericToDhallWithNormalizer (:+:)" (embedR r) @@ -2679,8 +2857,8 @@ { embed = \x -> let (name, y) = embedF x in case notEmptyRecordLit y of - Nothing -> Field (Union fields') name - Just val -> App (Field (Union fields') name) val + Nothing -> Field (Union fields') $ Core.makeFieldSelection name + Just val -> App (Field (Union fields') $ Core.makeFieldSelection name) val , declared = Union fields' } diff --git a/src/Dhall/Binary.hs b/src/Dhall/Binary.hs --- a/src/Dhall/Binary.hs +++ b/src/Dhall/Binary.hs @@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -39,6 +40,7 @@ , Expr (..) , File (..) , FilePrefix (..) + , FunctionBinding (..) , Import (..) , ImportHashed (..) , ImportMode (..) @@ -66,6 +68,8 @@ import qualified Data.ByteString import qualified Data.ByteString.Lazy import qualified Data.ByteString.Short +import qualified Data.Foldable as Foldable +import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Sequence import qualified Dhall.Crypto import qualified Dhall.Map @@ -93,7 +97,7 @@ -- ^ Version "1.0.0" deriving (Enum, Bounded) --- | Render a `StandardVersion` as `Text` +-- | Render a `StandardVersion` as `Data.Text.Text` renderStandardVersion :: StandardVersion -> Text renderStandardVersion NoVersion = "none" renderStandardVersion V_1_0_0 = "1.0.0" @@ -256,7 +260,7 @@ b <- go - return (Lam "_" _A b) + return (Lam (Syntax.makeFunctionBinding "_" _A) b) 4 -> do x <- Decoding.decodeString @@ -269,7 +273,7 @@ b <- go - return (Lam x _A b) + return (Lam (Syntax.makeFunctionBinding x _A) b) _ -> die ("Incorrect number of tokens used to encode a λ expression: " <> show len) @@ -391,7 +395,7 @@ x <- Decoding.decodeString - return (Field t x) + return (Field t (Syntax.makeFieldSelection x)) 10 -> do t <- go @@ -579,6 +583,23 @@ return (ListLit (Just _T) empty) + 29 -> do + l <- go + + n <- Decoding.decodeListLen + + ks₀ <- replicateDecoder n Decoding.decodeString + + ks₁ <- case NonEmpty.nonEmpty ks₀ of + Nothing -> + die "0 field labels in decoded with expression" + Just ks₁ -> + return ks₁ + + r <- go + + return (With l ks₁ r) + _ -> die ("Unexpected tag: " <> show tag) @@ -706,13 +727,13 @@ where (function, arguments) = unApply a - Lam "_" _A b -> + Lam (FunctionBinding { functionBindingVariable = "_", functionBindingAnnotation = _A }) b -> encodeList3 (Encoding.encodeInt 1) (go _A) (go b) - Lam x _A b -> + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b -> encodeList4 (Encoding.encodeInt 1) (Encoding.encodeString x) @@ -819,7 +840,7 @@ (Encoding.encodeInt 8) (encodeMapWith (go. recordFieldValue) xts) - Field t x -> + Field t (Syntax.fieldSelectionLabel -> x) -> encodeList3 (Encoding.encodeInt 9) (go t) @@ -939,8 +960,12 @@ (go t) (go _T) - a@With{} -> - go (Syntax.desugarWith a) + With l ks r -> + encodeList4 + (Encoding.encodeInt 29) + (go l) + (encodeList (fmap Encoding.encodeString ks)) + (go r) Note _ b -> go b @@ -974,11 +999,12 @@ encodeList4 a b c d = Encoding.encodeListLen 4 <> a <> b <> c <> d {-# INLINE encodeList4 #-} -encodeListN :: Int -> [ Encoding ] -> Encoding -encodeListN len xs = Encoding.encodeListLen (fromIntegral len) <> mconcat xs +encodeListN :: Foldable f => Int -> f Encoding -> Encoding +encodeListN len xs = + Encoding.encodeListLen (fromIntegral len) <> Foldable.fold xs {-# INLINE encodeListN #-} -encodeList :: [ Encoding ] -> Encoding +encodeList :: Foldable f => f Encoding -> Encoding encodeList xs = encodeListN (length xs) xs {-# INLINE encodeList #-} @@ -1179,7 +1205,7 @@ encodeExpression :: Serialise (Expr Void a) => Expr Void a -> ByteString encodeExpression = Serialise.serialise --- | Decode a Dhall expression from a CBOR `Term` +-- | Decode a Dhall expression from a CBOR `Codec.CBOR.Term.Term` decodeExpression :: Serialise (Expr s a) => ByteString -> Either DecodingFailure (Expr s a) decodeExpression bytes = diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs --- a/src/Dhall/Context.hs +++ b/src/Dhall/Context.hs @@ -15,8 +15,8 @@ import Data.Text (Text) import Prelude hiding (lookup) -{-| A @(Context a)@ associates `Text` labels with values of type @a@. Each - `Text` label can correspond to multiple values of type @a@ +{-| A @(Context a)@ associates `Data.Text.Text` labels with values of type @a@. + Each `Data.Text.Text` label can correspond to multiple values of type @a@ The `Context` is used for type-checking when @(a = Expr X)@ diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -27,6 +27,10 @@ , PreferAnnotation(..) , RecordField(..) , makeRecordField + , FunctionBinding(..) + , makeFunctionBinding + , FieldSelection (..) + , makeFieldSelection , Expr(..) -- * Normalization @@ -55,6 +59,7 @@ , chunkExprs , bindingExprs , recordFieldExprs + , functionBindingExprs -- * Let-blocks , multiLet @@ -94,7 +99,7 @@ pretty = pretty_ {-# INLINE pretty #-} -{-| Escape a `Text` literal using Dhall's escaping rules +{-| Escape a `Data.Text.Text` literal using Dhall's escaping rules Note that the result does not include surrounding quotes -} @@ -106,7 +111,7 @@ {-| Utility used to implement the @--censor@ flag, by: * Replacing all `Src` text with spaces - * Replacing all `Text` literals inside type errors with spaces + * Replacing all `Dhall.Syntax.Text` literals inside type errors with spaces -} censorExpression :: Expr Src a -> Expr Src a censorExpression (TextLit chunks) = TextLit (censorChunks chunks) @@ -120,7 +125,9 @@ xys' = [ (censorText x, censorExpression y) | (x, y) <- xys ] --- | Utility used to censor `Text` by replacing all characters with a space +{-| Utility used to censor `Data.Text.Text` by replacing all characters with a + space +-} censorText :: Text -> Text censorText = Data.Text.map (\_ -> ' ') diff --git a/src/Dhall/Deriving.hs b/src/Dhall/Deriving.hs --- a/src/Dhall/Deriving.hs +++ b/src/Dhall/Deriving.hs @@ -58,7 +58,7 @@ , TrainCase -- * Type-level versions of SingletonConstructors - , ToSingletonConstructors + , ToSingletonConstructors(..) , Bare , Wrapped , Smart @@ -402,7 +402,7 @@ Second, we defined the @Name@ type in Haskell as a newtype over @Text@, with a @getName@ field for unwrapping. In Dhall, however, @Name@ is a synonym of -'Text', which is why 'input' above was expecting a record. +'Data.Text.Text', which is why 'Dhall.input' above was expecting a record. The 'Dhall.Bare' option for 'singletonConstructors' is a perfect fit here: it translates Haskell singleton constructors into the Dhall version of the nested type, without wrapping it into a record. diff --git a/src/Dhall/Diff.hs b/src/Dhall/Diff.hs --- a/src/Dhall/Diff.hs +++ b/src/Dhall/Diff.hs @@ -1,5 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} {-| This module provides functionality for concisely displaying the difference between two expressions @@ -32,6 +33,7 @@ , Const (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , RecordField (..) , Var (..) ) @@ -645,7 +647,9 @@ diff l@(Lam {}) r@(Lam {}) = enclosed' " " (rarrow <> " ") (docs l r) where - docs (Lam aL bL cL) (Lam aR bR cR) = + docs + (Lam (FunctionBinding { functionBindingVariable = aL, functionBindingAnnotation = bL }) cL) + (Lam (FunctionBinding { functionBindingVariable = aR, functionBindingAnnotation = bR }) cR) = Data.List.NonEmpty.cons (align doc) (docs cL cR) where doc = lambda @@ -1061,7 +1065,7 @@ diffSelectorExpression l@(Field {}) r@(Field {}) = enclosed' " " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r)) where - docs (Field aL bL) (Field aR bR) = + docs (Field aL (Syntax.fieldSelectionLabel -> bL)) (Field aR (Syntax.fieldSelectionLabel -> bR)) = Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR) docs (Project aL (Left bL)) (Project aR (Left bR)) = Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR) @@ -1076,7 +1080,7 @@ diffSelectorExpression l@(Project {}) r@(Project {}) = enclosed' " " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r)) where - docs (Field aL bL) (Field aR bR) = + docs (Field aL (Syntax.fieldSelectionLabel -> bL)) (Field aR (Syntax.fieldSelectionLabel ->bR)) = Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR) docs (Project aL (Left bL)) (Project aR (Left bR)) = Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR) diff --git a/src/Dhall/DirectoryTree.hs b/src/Dhall/DirectoryTree.hs --- a/src/Dhall/DirectoryTree.hs +++ b/src/Dhall/DirectoryTree.hs @@ -137,8 +137,8 @@ unexpectedExpression = expression {- | This error indicates that you supplied an invalid Dhall expression to the - `directoryTree` function. The Dhall expression could not be translated to - a directory tree. + `toDirectoryTree` function. The Dhall expression could not be translated + to a directory tree. -} newtype FilesystemError = FilesystemError { unexpectedExpression :: Expr Void Void } diff --git a/src/Dhall/Eval.hs b/src/Dhall/Eval.hs --- a/src/Dhall/Eval.hs +++ b/src/Dhall/Eval.hs @@ -50,14 +50,14 @@ , textShow ) where -import Data.Foldable (foldr', toList) -import Data.Sequence (Seq, ViewL (..), ViewR (..)) -import Data.Text (Text) -import Data.Void (Void) -import Dhall.Map (Map) -import Dhall.Set (Set) -import GHC.Natural (Natural) -import Prelude hiding (succ) +import Data.Foldable (foldr', toList) +import Data.Sequence (Seq, ViewL (..), ViewR (..)) +import Data.Text (Text) +import Data.Void (Void) +import Dhall.Map (Map) +import Dhall.Set (Set) +import GHC.Natural (Natural) +import Prelude hiding (succ) import Dhall.Syntax ( Binding (..) @@ -65,6 +65,7 @@ , Const (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -389,7 +390,7 @@ VConst k Var v -> vVar env v - Lam x a t -> + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t -> VLam (eval env a) (Closure x env t) Pi x a b -> VPi (eval env a) (Closure x env b) @@ -676,7 +677,10 @@ Prefer _ t u -> vPrefer env (eval env t) (eval env u) RecordCompletion t u -> - eval env (Annot (Prefer PreferFromCompletion (Field t "default") u) (Field t "Type")) + eval env (Annot (Prefer PreferFromCompletion (Field t def) u) (Field t typ)) + where + def = Syntax.makeFieldSelection "default" + typ = Syntax.makeFieldSelection "Type" Merge x y ma -> case (eval env x, eval env y, fmap (eval env) ma) of (VRecordLit m, VInject _ k mt, _) @@ -707,7 +711,7 @@ in VListLit Nothing s (x', ma') -> VToMap x' ma' - Field t k -> + Field t (Syntax.fieldSelectionLabel -> k) -> vField (eval env t) k Project t (Left ks) -> vProjectByFields env (eval env t) (Dhall.Set.sort ks) @@ -984,10 +988,15 @@ VApp t u -> quote env t `qApp` u VLam a (freshClosure -> (x, v, t)) -> - Lam x (quote env a) (quoteBind x (instantiate t v)) + Lam + (Syntax.makeFunctionBinding x (quote env a)) + (quoteBind x (instantiate t v)) VHLam i t -> case i of - Typed (fresh -> (x, v)) a -> Lam x (quote env a) (quoteBind x (t v)) + Typed (fresh -> (x, v)) a -> + Lam + (Syntax.makeFunctionBinding x (quote env a)) + (quoteBind x (t v)) Prim -> quote env (t VPrimVar) NaturalSubtractZero -> App NaturalSubtract (NaturalLit 0) @@ -1102,7 +1111,7 @@ VToMap t ma -> ToMap (quote env t) (fmap (quote env) ma) VField t k -> - Field (quote env t) k + Field (quote env t) $ Syntax.makeFieldSelection k VProject t p -> Project (quote env t) (fmap (quote env) p) VAssert t -> @@ -1110,9 +1119,9 @@ VEquivalent t u -> Equivalent (quote env t) (quote env u) VInject m k Nothing -> - Field (Union (fmap (fmap (quote env)) m)) k + Field (Union (fmap (fmap (quote env)) m)) $ Syntax.makeFieldSelection k VInject m k (Just t) -> - Field (Union (fmap (fmap (quote env)) m)) k `qApp` t + Field (Union (fmap (fmap (quote env)) m)) (Syntax.makeFieldSelection k) `qApp` t VEmbed a -> Embed a VPrimVar -> @@ -1165,8 +1174,8 @@ Const k Var (V x i) -> goVar e0 x i - Lam x t u -> - Lam "_" (go t) (goBind x u) + Lam (FunctionBinding src0 x src1 src2 t) u -> + Lam (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u) Pi x a b -> Pi "_" (go a) (goBind x b) App t u -> @@ -1303,4 +1312,4 @@ go = goEnv e0 goBind x = goEnv (Bind e0 x) goChunks (Chunks ts x) = Chunks (fmap (fmap go) ts) x - goRecordField (RecordField s0 e) = RecordField s0 (go e) + goRecordField (RecordField s0 e s1 s2) = RecordField s0 (go e) s1 s2 diff --git a/src/Dhall/Freeze.hs b/src/Dhall/Freeze.hs --- a/src/Dhall/Freeze.hs +++ b/src/Dhall/Freeze.hs @@ -8,9 +8,13 @@ module Dhall.Freeze ( -- * Freeze freeze + , freezeWithManager , freezeExpression + , freezeExpressionWithManager , freezeImport + , freezeImportWithManager , freezeRemoteImport + , freezeRemoteImportWithManager -- * Types , Scope(..) @@ -57,7 +61,15 @@ -- ^ Current working directory -> Import -> IO Import -freezeImport directory import_ = do +freezeImport = freezeImportWithManager Dhall.Import.defaultNewManager + +-- | See 'freezeImport'. +freezeImportWithManager + :: IO Dhall.Import.Manager + -> FilePath + -> Import + -> IO Import +freezeImportWithManager newManager directory import_ = do let unprotectedImport = import_ { importHashed = @@ -66,7 +78,7 @@ } } - let status = Dhall.Import.emptyStatus directory + let status = Dhall.Import.emptyStatusWithManager newManager directory expression <- State.evalStateT (Dhall.Import.loadWith (Embed unprotectedImport)) status @@ -93,9 +105,17 @@ -- ^ Current working directory -> Import -> IO Import -freezeRemoteImport directory import_ = +freezeRemoteImport = freezeRemoteImportWithManager Dhall.Import.defaultNewManager + +-- | See 'freezeRemoteImport'. +freezeRemoteImportWithManager + :: IO Dhall.Import.Manager + -> FilePath + -> Import + -> IO Import +freezeRemoteImportWithManager newManager directory import_ = case importType (importHashed import_) of - Remote {} -> freezeImport directory import_ + Remote {} -> freezeImportWithManager newManager directory import_ _ -> return import_ -- | Specifies which imports to freeze @@ -125,7 +145,19 @@ -> CharacterSet -> Censor -> IO () -freeze outputMode input0 scope intent characterSet censor = go input0 +freeze = freezeWithManager Dhall.Import.defaultNewManager + +-- | See 'freeze'. +freezeWithManager + :: IO Dhall.Import.Manager + -> OutputMode + -> PossiblyTransitiveInput + -> Scope + -> Intent + -> CharacterSet + -> Censor + -> IO () +freezeWithManager newManager outputMode input0 scope intent characterSet censor = go input0 where go input = do let directory = case input of @@ -134,7 +166,7 @@ PossiblyTransitiveInputFile file _ -> System.FilePath.takeDirectory file - let status = Dhall.Import.emptyStatus directory + let status = Dhall.Import.emptyStatusWithManager newManager directory (originalText, transitivity) <- case input of PossiblyTransitiveInputFile file transitivity -> do @@ -160,7 +192,7 @@ NonTransitive -> return () - frozenExpression <- freezeExpression directory scope intent parsedExpression + frozenExpression <- freezeExpressionWithManager newManager directory scope intent parsedExpression let doc = Pretty.pretty header <> Dhall.Pretty.prettyCharacterSet characterSet frozenExpression @@ -213,13 +245,23 @@ -> Intent -> Expr s Import -> IO (Expr s Import) -freezeExpression directory scope intent expression = do +freezeExpression = freezeExpressionWithManager Dhall.Import.defaultNewManager + +-- | See 'freezeExpression'. +freezeExpressionWithManager + :: IO Dhall.Import.Manager + -> FilePath + -> Scope + -> Intent + -> Expr s Import + -> IO (Expr s Import) +freezeExpressionWithManager newManager directory scope intent expression = do let freezeScope = case scope of - AllImports -> freezeImport - OnlyRemoteImports -> freezeRemoteImport + AllImports -> freezeImportWithManager + OnlyRemoteImports -> freezeRemoteImportWithManager - let freezeFunction = freezeScope directory + let freezeFunction = freezeScope newManager directory let cache -- This case is necessary because `transformOf` is a bottom-up diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -6,6 +6,8 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} + {-# OPTIONS_GHC -Wall #-} {-| Dhall lets you import external expressions located either in local files or @@ -101,7 +103,9 @@ module Dhall.Import ( -- * Import load + , loadWithManager , loadRelativeTo + , loadRelativeToWithManager , loadWith , localToPath , hashExpression @@ -109,6 +113,8 @@ , writeExpressionToSemanticCache , warnAboutMissingCaches , assertNoImports + , Manager + , defaultNewManager , Status(..) , SemanticCacheMode(..) , Chained @@ -116,6 +122,7 @@ , chainedFromLocalHere , chainedChangeMode , emptyStatus + , emptyStatusWithManager , stack , cache , Depends(..) @@ -128,6 +135,7 @@ , chainImport , dependencyToFile , ImportSemantics + , HTTPHeader , Cycle(..) , ReferentiallyOpaque(..) , Imported(..) @@ -170,9 +178,9 @@ , ImportHashed (..) , ImportMode (..) , ImportType (..) - , RecordField (..) , URL (..) , bindingExprs + , functionBindingExprs , recordFieldExprs ) @@ -343,6 +351,7 @@ throwMissingImport :: (MonadCatch m, Exception e) => e -> m a throwMissingImport e = throwM (MissingImports [toException e]) +-- | HTTP headers type HTTPHeader = (CI ByteString, ByteString) -- | Exception thrown when a HTTP url is imported but dhall was built without @@ -496,9 +505,9 @@ return (Chained (canonicalize (parent <> child))) -- | Load an import, resulting in a fully resolved, type-checked and normalised --- expression. @loadImport@ handles the 'hot' cache in @Status@ and defers to --- `loadImportWithSemanticCache` for imports that aren't in the @Status@ cache --- already. +-- expression. @loadImport@ handles the \"hot\" cache in @Status@ and defers +-- to @loadImportWithSemanticCache@ for imports that aren't in the @Status@ +-- cache already. loadImport :: Chained -> StateT Status IO ImportSemantics loadImport import_ = do Status {..} <- State.get @@ -511,7 +520,7 @@ return importSemantics -- | Load an import from the 'semantic cache'. Defers to --- `loadImportWithSemisemanticCache` for imports that aren't frozen (and +-- @loadImportWithSemisemanticCache@ for imports that aren't frozen (and -- therefore not cached semantically), as well as those that aren't cached yet. loadImportWithSemanticCache :: Chained -> StateT Status IO ImportSemantics loadImportWithSemanticCache @@ -688,15 +697,15 @@ -- importSemantics is alpha-beta-normal by construction! let importSemantics = case importType of - Missing -> Field locationType "Missing" + Missing -> Field locationType $ Core.makeFieldSelection "Missing" local@(Local _ _) -> - App (Field locationType "Local") + App (Field locationType $ Core.makeFieldSelection "Local") (TextLit (Chunks [] (Core.pretty local))) remote_@(Remote _) -> - App (Field locationType "Remote") + App (Field locationType $ Core.makeFieldSelection "Remote") (TextLit (Chunks [] (Core.pretty remote_))) Env env -> - App (Field locationType "Environment") + App (Field locationType $ Core.makeFieldSelection "Environment") (TextLit (Chunks [] (Core.pretty env))) return (ImportSemantics {..}) @@ -778,7 +787,7 @@ toHeader :: Expr s a -> Maybe HTTPHeader toHeader (RecordLit m) = do - (RecordField _ (TextLit (Chunks [] keyText)), RecordField _ (TextLit (Chunks [] valueText))) + (Core.recordFieldValue -> TextLit (Chunks [] keyText), Core.recordFieldValue -> TextLit (Chunks [] valueText)) <- lookupHeader <|> lookupMapKey let keyBytes = Data.Text.Encoding.encodeUtf8 keyText let valueBytes = Data.Text.Encoding.encodeUtf8 valueText @@ -1012,8 +1021,12 @@ -- | Default starting `Status`, importing relative to the given directory. emptyStatus :: FilePath -> Status -emptyStatus = emptyStatusWith fetchRemote +emptyStatus = emptyStatusWithManager defaultNewManager +-- | See 'emptyStatus'. +emptyStatusWithManager :: IO Manager -> FilePath -> Status +emptyStatusWithManager newManager = emptyStatusWith newManager fetchRemote + {-| Generalized version of `load` You can configure the desired behavior through the initial `Status` that you @@ -1074,12 +1087,18 @@ Let a b -> Let <$> bindingExprs loadWith a <*> loadWith b Record m -> Record <$> traverse (recordFieldExprs loadWith) m RecordLit m -> RecordLit <$> traverse (recordFieldExprs loadWith) m + Lam a b -> Lam <$> functionBindingExprs loadWith a <*> loadWith b + Field a b -> Field <$> loadWith a <*> pure b expression -> Syntax.unsafeSubExpressions loadWith expression -- | Resolve all imports within an expression load :: Expr Src Import -> IO (Expr Src Void) -load = loadRelativeTo "." UseSemanticCache +load = loadWithManager defaultNewManager +-- | See 'load'. +loadWithManager :: IO Manager -> Expr Src Import -> IO (Expr Src Void) +loadWithManager newManager = loadRelativeToWithManager newManager "." UseSemanticCache + printWarning :: (MonadIO m) => String -> m () printWarning message = do let warning = @@ -1092,10 +1111,19 @@ -- | Resolve all imports within an expression, importing relative to the given -- directory. loadRelativeTo :: FilePath -> SemanticCacheMode -> Expr Src Import -> IO (Expr Src Void) -loadRelativeTo rootDirectory semanticCacheMode expression = +loadRelativeTo = loadRelativeToWithManager defaultNewManager + +-- | See 'loadRelativeTo'. +loadRelativeToWithManager + :: IO Manager + -> FilePath + -> SemanticCacheMode + -> Expr Src Import + -> IO (Expr Src Void) +loadRelativeToWithManager newManager rootDirectory semanticCacheMode expression = State.evalStateT (loadWith expression) - (emptyStatus rootDirectory) { _semanticCacheMode = semanticCacheMode } + (emptyStatusWithManager newManager rootDirectory) { _semanticCacheMode = semanticCacheMode } encodeExpression :: StandardVersion diff --git a/src/Dhall/Import/Types.hs b/src/Dhall/Import/Types.hs --- a/src/Dhall/Import/Types.hs +++ b/src/Dhall/Import/Types.hs @@ -31,7 +31,7 @@ import System.FilePath (isRelative, splitDirectories) #ifdef WITH_HTTP -import Dhall.Import.Manager (Manager) +import qualified Dhall.Import.Manager #endif import qualified Data.Text @@ -39,8 +39,8 @@ import qualified Dhall.Map as Map import qualified Dhall.Substitution --- | A fully 'chained' import, i.e. if it contains a relative path that path is --- relative to the current directory. If it is a remote import with headers +-- | A fully \"chained\" import, i.e. if it contains a relative path that path +-- is relative to the current directory. If it is a remote import with headers -- those are well-typed (either of type `List { header : Text, value Text}` or -- `List { mapKey : Text, mapValue Text})` and in normal form. These -- invariants are preserved by the API exposed by @Dhall.Import@. @@ -67,6 +67,24 @@ -} data SemanticCacheMode = IgnoreSemanticCache | UseSemanticCache deriving (Eq) +-- | Shared state for HTTP requests +type Manager = +#ifdef WITH_HTTP + Dhall.Import.Manager.Manager +#else + () +#endif + +-- | The default HTTP 'Manager' +defaultNewManager :: IO Manager +defaultNewManager = +#ifdef WITH_HTTP + Dhall.Import.Manager.defaultNewManager +#else + pure () +#endif + + -- | State threaded throughout the import process data Status = Status { _stack :: NonEmpty Chained @@ -81,12 +99,10 @@ -- ^ Cache of imported expressions with their node id in order to avoid -- importing the same expression twice with different values -#ifdef WITH_HTTP + , _newManager :: IO Manager , _manager :: Maybe Manager -#else - , _manager :: Maybe Void -#endif - -- ^ Used to cache the `Manager` when making multiple requests + -- ^ Used to cache the `Dhall.Import.Manager.Manager` when making multiple + -- requests , _remote :: URL -> StateT Status IO Data.Text.Text -- ^ The remote resolver, fetches the content at the given URL. @@ -100,10 +116,10 @@ , _semanticCacheMode :: SemanticCacheMode } --- | Initial `Status`, parameterised over the remote resolver, importing --- relative to the given directory. -emptyStatusWith :: (URL -> StateT Status IO Data.Text.Text) -> FilePath -> Status -emptyStatusWith _remote rootDirectory = Status {..} +-- | Initial `Status`, parameterised over the HTTP 'Manager' and the remote resolver, +-- importing relative to the given directory. +emptyStatusWith :: IO Manager -> (URL -> StateT Status IO Data.Text.Text) -> FilePath -> Status +emptyStatusWith _newManager _remote rootDirectory = Status {..} where _stack = pure (Chained rootImport) @@ -171,11 +187,9 @@ {-| This exception indicates that there was an internal error in Dhall's import-related logic - the `expected` type then the `extract` function must succeed. If not, then - this exception is thrown - This exception indicates that an invalid `Type` was provided to the `input` - function + This exception indicates that an invalid `Dhall.Syntax.Type` was provided to + the `Dhall.input` function -} data InternalError = InternalError deriving (Typeable) @@ -202,11 +216,12 @@ instance Exception InternalError --- | Wrapper around `HttpException`s with a prettier `Show` instance. +-- | Wrapper around `Network.HTTP.Client.HttpException`s with a prettier `Show` +-- instance -- -- In order to keep the library API constant even when the @with-http@ Cabal -- flag is disabled the pretty error message is pre-rendered and the real --- 'HttpExcepion' is stored in a 'Dynamic' +-- 'Network.HTTP.Client.HttpException' is stored in a 'Dynamic' data PrettyHttpException = PrettyHttpException String Dynamic deriving (Typeable) diff --git a/src/Dhall/Lint.hs b/src/Dhall/Lint.hs --- a/src/Dhall/Lint.hs +++ b/src/Dhall/Lint.hs @@ -68,7 +68,7 @@ Just (Core.shift (-1) (V a 0) d) removeUnusedBindings _ = Nothing --- | Fix `Let` bindings that the user probably meant to be `assert`s +-- | Fix `Let` bindings that the user probably meant to be @assert@s fixAssert :: Expr s a -> Maybe (Expr s a) fixAssert (Let (Binding { value = v@(Core.shallowDenote -> Equivalent {}), ..}) body) = Just (Let (Binding { value = Assert v, .. }) body) diff --git a/src/Dhall/Main.hs b/src/Dhall/Main.hs --- a/src/Dhall/Main.hs +++ b/src/Dhall/Main.hs @@ -12,6 +12,7 @@ ( -- * Options Options(..) , Mode(..) + , ResolveMode(..) , parseOptions , parserInfoOptions @@ -161,15 +162,19 @@ } | Encode { file :: Input, json :: Bool } | Decode { file :: Input, json :: Bool, quiet :: Bool } - | Text { file :: Input } + | Text { file :: Input, output :: Output } | DirectoryTree { file :: Input, path :: FilePath } | Schemas { file :: Input, outputMode :: OutputMode, schemas :: Text } | SyntaxTree { file :: Input, noted :: Bool } +-- | This specifies how to resolve transitive dependencies data ResolveMode = Dot + -- ^ Generate a DOT file for @graphviz@ | ListTransitiveDependencies + -- ^ List all transitive dependencies as text, one per line | ListImmediateDependencies + -- ^ List immediate dependencies as text, one per line -- | Groups of subcommands data Group @@ -250,7 +255,7 @@ Generate "text" "Render a Dhall expression that evaluates to a Text literal" - (Text <$> parseFile) + (Text <$> parseFile <*> parseOutput) <|> subcommand Generate "to-directory-tree" @@ -902,7 +907,10 @@ case normalizedExpression of Dhall.Core.TextLit (Dhall.Core.Chunks [] text) -> - Data.Text.IO.putStr text + let write = case output of + StandardOutput -> Data.Text.IO.putStr + OutputFile file_ -> Data.Text.IO.writeFile file_ + in write text _ -> do let invalidDecoderExpected :: Expr Void Void invalidDecoderExpected = Dhall.Core.Text diff --git a/src/Dhall/Map.hs b/src/Dhall/Map.hs --- a/src/Dhall/Map.hs +++ b/src/Dhall/Map.hs @@ -356,7 +356,7 @@ ks' = filterKeys (\k -> Data.Map.member k m') ks {-# INLINABLE filter #-} -{-| Restrict a 'Map' to only those keys found in a @"Data.Set".'Set'@. +{-| Restrict a 'Map' to only those keys found in a @"Data.Set".'Data.Set.Set'@. >>> restrictKeys (fromList [("A",1),("B",2)]) (Data.Set.fromList ["A"]) fromList [("A",1)] @@ -369,7 +369,7 @@ ks' = filterKeys (\k -> Data.Set.member k s) ks {-# INLINABLE restrictKeys #-} -{-| Remove all keys in a @"Data.Set".'Set'@ from a 'Map' +{-| Remove all keys in a @"Data.Set".'Data.Set.Set'@ from a 'Map' >>> withoutKeys (fromList [("A",1),("B",2)]) (Data.Set.fromList ["A"]) fromList [("B",2)] @@ -679,7 +679,7 @@ elems (Map m (Original ks)) = fmap (\k -> m Data.Map.! k) ks {-# INLINABLE elems #-} -{-| Return the @"Data.Set".'Set'@ of the keys +{-| Return the @"Data.Set".'Data.Set.Set'@ of the keys >>> keysSet (fromList [("B",1),("A",2)]) fromList ["A","B"] diff --git a/src/Dhall/Normalize.hs b/src/Dhall/Normalize.hs --- a/src/Dhall/Normalize.hs +++ b/src/Dhall/Normalize.hs @@ -1,6 +1,8 @@ {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} module Dhall.Normalize ( alphaNormalize @@ -12,7 +14,7 @@ , ReifiedNormalizer (..) , judgmentallyEqual , subst - , shift + , Syntax.shift , isNormalized , isNormalizedWith , freeIn @@ -31,6 +33,8 @@ , Chunks (..) , DhallDouble (..) , Expr (..) + , FieldSelection (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -55,115 +59,28 @@ judgmentallyEqual = Eval.judgmentallyEqual {-# INLINE judgmentallyEqual #-} -{-| `shift` is used by both normalization and type-checking to avoid variable - capture by shifting variable indices - - For example, suppose that you were to normalize the following expression: - -> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x - - If you were to substitute @y@ with @x@ without shifting any variable - indices, then you would get the following incorrect result: - -> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form - - In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in - order to avoid being misinterpreted as the @x@ bound by the innermost - lambda. If we perform that `shift` then we get the correct result: - -> λ(a : Type) → λ(x : a) → λ(x : a) → x@1 - - As a more worked example, suppose that you were to normalize the following - expression: - -> λ(a : Type) -> → λ(f : a → a → a) -> → λ(x : a) -> → λ(x : a) -> → (λ(x : a) → f x x@1) x@1 - - The correct normalized result would be: - -> λ(a : Type) -> → λ(f : a → a → a) -> → λ(x : a) -> → λ(x : a) -> → f x@1 x - - The above example illustrates how we need to both increase and decrease - variable indices as part of substitution: - - * We need to increase the index of the outer @x\@1@ to @x\@2@ before we - substitute it into the body of the innermost lambda expression in order - to avoid variable capture. This substitution changes the body of the - lambda expression to @(f x\@2 x\@1)@ - - * We then remove the innermost lambda and therefore decrease the indices of - both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one - less @x@ variable is now bound within that scope - - Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to - the indices of all variables named @x@ whose indices are greater than - @(n + m)@, where @m@ is the number of bound variables of the same name - within that scope - - In practice, @d@ is always @1@ or @-1@ because we either: - - * increment variables by @1@ to avoid variable capture during substitution - * decrement variables by @1@ when deleting lambdas after substitution - - @n@ starts off at @0@ when substitution begins and increments every time we - descend into a lambda or let expression that binds a variable of the same - name in order to avoid shifting the bound variables by mistake. --} -shift :: Int -> Var -> Expr s a -> Expr s a -shift d (V x n) (Var (V x' n')) = Var (V x' n'') - where - n'' = if x == x' && n <= n' then n' + d else n' -shift d (V x n) (Lam x' _A b) = Lam x' _A' b' - where - _A' = shift d (V x n ) _A - b' = shift d (V x n') b - where - n' = if x == x' then n + 1 else n -shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B' - where - _A' = shift d (V x n ) _A - _B' = shift d (V x n') _B - where - n' = if x == x' then n + 1 else n -shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) = - Let (Binding src0 f src1 mt' src2 r') e' - where - e' = shift d (V x n') e - where - n' = if x == f then n + 1 else n - - mt' = fmap (fmap (shift d (V x n))) mt - r' = shift d (V x n) r -shift d v expression = Lens.over Syntax.subExpressions (shift d v) expression - {-| Substitute all occurrences of a variable with an expression > subst x C B ~ B[x := C] -} subst :: Var -> Expr s a -> Expr s a -> Expr s a subst _ _ (Const a) = Const a -subst (V x n) e (Lam y _A b) = Lam y _A' b' +subst (V x n) e (Lam (FunctionBinding src0 y src1 src2 _A) b) = + Lam (FunctionBinding src0 y src1 src2 _A') b' where - _A' = subst (V x n ) e _A - b' = subst (V x n') (shift 1 (V y 0) e) b + _A' = subst (V x n ) e _A + b' = subst (V x n') (Syntax.shift 1 (V y 0) e) b n' = if x == y then n + 1 else n subst (V x n) e (Pi y _A _B) = Pi y _A' _B' where - _A' = subst (V x n ) e _A - _B' = subst (V x n') (shift 1 (V y 0) e) _B + _A' = subst (V x n ) e _A + _B' = subst (V x n') (Syntax.shift 1 (V y 0) e) _B n' = if x == y then n + 1 else n subst v e (Var v') = if v == v' then e else Var v' subst (V x n) e (Let (Binding src0 f src1 mt src2 r) b) = Let (Binding src0 f src1 mt' src2 r') b' where - b' = subst (V x n') (shift 1 (V f 0) e) b + b' = subst (V x n') (Syntax.shift 1 (V f 0) e) b where n' = if x == f then n + 1 else n @@ -196,8 +113,9 @@ {-| α-normalize an expression by renaming all bound variables to @\"_\"@ and using De Bruijn indices to distinguish them ->>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x")))) -Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1))))) +>>> mfb = Syntax.makeFunctionBinding +>>> alphaNormalize (Lam (mfb "a" (Const Type)) (Lam (mfb "b" (Const Type)) (Lam (mfb "x" "a") (Lam (mfb "y" "b") "x")))) +Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1))))) α-normalization does not affect free variables: @@ -225,7 +143,7 @@ {-| Reduce an expression to its normal form, performing beta reduction and applying any custom definitions. - `normalizeWith` is designed to be used with function `typeWith`. The `typeWith` + `normalizeWith` is designed to be used with function `Dhall.TypeCheck.typeWith`. The `Dhall.TypeCheck.typeWith` function allows typing of Dhall functions in a custom typing context whereas `normalizeWith` allows evaluating Dhall expressions in a custom context. @@ -253,10 +171,11 @@ :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a) normalizeWithM ctx e0 = loop (Syntax.denote e0) where - loop e = case e of + loop = \case Const k -> pure (Const k) Var v -> pure (Var v) - Lam x _A b -> Lam x <$> _A' <*> b' + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b -> + Lam <$> (Syntax.makeFunctionBinding x <$> _A') <*> b' where _A' = loop _A b' = loop b @@ -272,11 +191,11 @@ f' <- loop f a' <- loop a case f' of - Lam x _A b₀ -> do + Lam (FunctionBinding _ x _ _ _A) b₀ -> do - let a₂ = shift 1 (V x 0) a' + let a₂ = Syntax.shift 1 (V x 0) a' let b₁ = subst (V x 0) a₂ b₀ - let b₂ = shift (-1) (V x 0) b₁ + let b₂ = Syntax.shift (-1) (V x 0) b₁ loop b₂ _ -> @@ -299,7 +218,7 @@ lazyLoop !n = App succ' (lazyLoop (n - 1)) App NaturalBuild g -> loop (App (App (App g Natural) succ) zero) where - succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1)) + succ = Lam (Syntax.makeFunctionBinding "n" Natural) (NaturalPlus "n" (NaturalLit 1)) zero = NaturalLit 0 App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0)) @@ -336,14 +255,14 @@ pure (TextLit (Chunks [] (Data.Text.pack (show n)))) App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil) where - _A₁ = shift 1 "a" _A₀ + _A₁ = Syntax.shift 1 "a" _A₀ list = App List _A₀ cons = - Lam "a" _A₀ - (Lam "as" - (App List _A₁) + Lam (Syntax.makeFunctionBinding "a" _A₀) + (Lam + (Syntax.makeFunctionBinding "as" (App List _A₁)) (ListAppend (ListLit Nothing (pure "a")) "as") ) @@ -405,9 +324,9 @@ Just app' -> loop app' Let (Binding _ f _ _ _ r) b -> loop b'' where - r' = shift 1 (V f 0) r + r' = Syntax.shift 1 (V f 0) r b' = subst (V f 0) r' b - b'' = shift (-1) (V f 0) b' + b'' = Syntax.shift (-1) (V f 0) b' Annot x _ -> loop x Bool -> pure Bool BoolLit b -> pure (BoolLit b) @@ -528,11 +447,11 @@ None -> pure None Record kts -> Record . Dhall.Map.sort <$> kts' where - f (RecordField s0 expr) = RecordField s0 <$> loop expr + f (RecordField s0 expr s1 s2) = (\e -> RecordField s0 e s1 s2) <$> loop expr kts' = traverse f kts RecordLit kvs -> RecordLit . Dhall.Map.sort <$> kvs' where - f (RecordField s0 expr) = RecordField s0 <$> loop expr + f (RecordField s0 expr s1 s2) = (\e -> RecordField s0 e s1 s2) <$> loop expr kvs' = traverse f kvs Union kts -> Union . Dhall.Map.sort <$> kts' where @@ -546,7 +465,7 @@ decide (RecordLit m) (RecordLit n) = RecordLit (Dhall.Map.unionWith f m n) where - f (RecordField _ expr) (RecordField _ expr') = + f (RecordField _ expr _ _) (RecordField _ expr' _ _) = Syntax.makeRecordField $ decide expr expr' decide l r = Combine mk l r @@ -559,7 +478,7 @@ decide (Record m) (Record n) = Record (Dhall.Map.unionWith f m n) where - f (RecordField _ expr) (RecordField _ expr') = + f (RecordField _ expr _ _) (RecordField _ expr' _ _) = Syntax.makeRecordField $ decide expr expr' decide l r = CombineTypes l r @@ -576,14 +495,17 @@ decide l r = Prefer PreferFromSource l r RecordCompletion x y -> - loop (Annot (Prefer PreferFromCompletion (Field x "default") y) (Field x "Type")) + loop (Annot (Prefer PreferFromCompletion (Field x def) y) (Field x typ)) + where + def = Syntax.makeFieldSelection "default" + typ = Syntax.makeFieldSelection "Type" Merge x y t -> do x' <- loop x y' <- loop y case x' of RecordLit kvsX -> case y' of - Field (Union ktsY) kY -> + Field (Union ktsY) (Syntax.fieldSelectionLabel -> kY) -> case Dhall.Map.lookup kY ktsY of Just Nothing -> case recordFieldValue <$> Dhall.Map.lookup kY kvsX of @@ -591,7 +513,7 @@ Nothing -> Merge x' y' <$> t' _ -> Merge x' y' <$> t' - App (Field (Union ktsY) kY) vY -> + App (Field (Union ktsY) (Syntax.fieldSelectionLabel -> kY)) vY -> case Dhall.Map.lookup kY ktsY of Just (Just _) -> case recordFieldValue <$> Dhall.Map.lookup kY kvsX of @@ -635,7 +557,7 @@ return (ListLit listType keyValues) _ -> return (ToMap x' t') - Field r x -> do + Field r k@FieldSelection{fieldSelectionLabel = x} -> do let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v) r' <- loop r @@ -643,21 +565,21 @@ RecordLit kvs -> case Dhall.Map.lookup x kvs of Just v -> pure $ recordFieldValue v - Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure x - Project r_ _ -> loop (Field r_ x) + Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure k + Project r_ _ -> loop (Field r_ k) Prefer _ (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of - Just v -> pure (Field (Prefer PreferFromSource (singletonRecordLit v) r_) x) - Nothing -> loop (Field r_ x) + Just v -> pure (Field (Prefer PreferFromSource (singletonRecordLit v) r_) k) + Nothing -> loop (Field r_ k) Prefer _ l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of Just v -> pure $ recordFieldValue v - Nothing -> loop (Field l x) + Nothing -> loop (Field l k) Combine m (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of - Just v -> pure (Field (Combine m (singletonRecordLit v) r_) x) - Nothing -> loop (Field r_ x) + Just v -> pure (Field (Combine m (singletonRecordLit v) r_) k) + Nothing -> loop (Field r_ k) Combine m l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of - Just v -> pure (Field (Combine m l (singletonRecordLit v)) x) - Nothing -> loop (Field l x) - _ -> pure (Field r' x) + Just v -> pure (Field (Combine m l (singletonRecordLit v)) k) + Nothing -> loop (Field l k) + _ -> pure (Field r' k) Project x (Left fields)-> do x' <- loop x let fieldsSet = Dhall.Set.toSet fields @@ -732,10 +654,11 @@ loop e = case e of Const _ -> True Var _ -> True - Lam _ a b -> loop a && loop b + Lam (FunctionBinding Nothing _ Nothing Nothing a) b -> loop a && loop b + Lam _ _ -> False Pi _ a b -> loop a && loop b App f a -> loop f && loop a && case App f a of - App (Lam _ _ _) _ -> False + App (Lam _ _) _ -> False App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False App NaturalBuild _ -> False App NaturalIsZero (NaturalLit _) -> False @@ -852,8 +775,14 @@ Optional -> True Some a -> loop a None -> True - Record kts -> Dhall.Map.isSorted kts && all (loop . recordFieldValue) kts - RecordLit kvs -> Dhall.Map.isSorted kvs && all (loop . recordFieldValue) kvs + Record kts -> Dhall.Map.isSorted kts && all decide kts + where + decide (RecordField Nothing exp' Nothing Nothing) = loop exp' + decide _ = False + RecordLit kvs -> Dhall.Map.isSorted kvs && all decide kvs + where + decide (RecordField Nothing exp' Nothing Nothing) = loop exp' + decide _ = False Union kts -> Dhall.Map.isSorted kts && all (all loop) kts Combine _ x y -> loop x && loop y && decide x y where @@ -885,7 +814,7 @@ ToMap x t -> case x of RecordLit _ -> False _ -> loop x && all loop t - Field r k -> case r of + Field r (FieldSelection Nothing k Nothing) -> case r of RecordLit _ -> False Project _ _ -> False Prefer _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r @@ -893,6 +822,7 @@ Combine _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r Combine _ _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r _ -> loop r + Field _ _ -> False Project r p -> loop r && case p of Left s -> case r of @@ -916,7 +846,7 @@ True >>> "x" `freeIn` "y" False ->>> "x" `freeIn` Lam "x" (Const Type) "x" +>>> "x" `freeIn` Lam (Syntax.makeFunctionBinding "x" (Const Type)) "x" False -} freeIn :: Eq a => Var -> Expr s a -> Bool diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -76,7 +76,7 @@ instance Exception ParseError --- | Parse an expression from `Text` containing a Dhall program +-- | Parse an expression from `Data.Text.Text` containing a Dhall program exprFromText :: String -- ^ User-friendly name describing the input expression, -- used in parsing error messages diff --git a/src/Dhall/Parser/Combinators.hs b/src/Dhall/Parser/Combinators.hs --- a/src/Dhall/Parser/Combinators.hs +++ b/src/Dhall/Parser/Combinators.hs @@ -63,7 +63,7 @@ <> Pretty.renderString (Dhall.Pretty.layout (pretty source)) --- | Doesn't force the 'Text' part +-- | Doesn't force the 'Data.Text.Text' part laxSrcEq :: Src -> Src -> Bool laxSrcEq (Src p q _) (Src p' q' _) = eq p p' && eq q q' where diff --git a/src/Dhall/Parser/Expression.hs b/src/Dhall/Parser/Expression.hs --- a/src/Dhall/Parser/Expression.hs +++ b/src/Dhall/Parser/Expression.hs @@ -18,6 +18,7 @@ import Text.Parser.Combinators (choice, try, ()) import qualified Control.Monad +import qualified Control.Monad.Combinators as Combinators import qualified Control.Monad.Combinators.NonEmpty as Combinators.NonEmpty import qualified Data.ByteArray.Encoding import qualified Data.ByteString @@ -33,13 +34,6 @@ import Dhall.Parser.Combinators import Dhall.Parser.Token --- | Get the current source position -getSourcePos :: Text.Megaparsec.MonadParsec e s m => - m Text.Megaparsec.SourcePos -getSourcePos = - Text.Megaparsec.getSourcePos -{-# INLINE getSourcePos #-} - -- | Get the current source offset (in tokens) getOffset :: Text.Megaparsec.MonadParsec e s m => m Int getOffset = Text.Megaparsec.stateOffset <$> Text.Megaparsec.getParserState @@ -57,17 +51,17 @@ -} src :: Parser a -> Parser Src src parser = do - before <- getSourcePos + before <- Text.Megaparsec.getSourcePos (tokens, _) <- Text.Megaparsec.match parser - after <- getSourcePos + after <- Text.Megaparsec.getSourcePos return (Src before after tokens) -- | Same as `src`, except also return the parsed value srcAnd :: Parser a -> Parser (Src, a) srcAnd parser = do - before <- getSourcePos + before <- Text.Megaparsec.getSourcePos (tokens, x) <- Text.Megaparsec.match parser - after <- getSourcePos + after <- Text.Megaparsec.getSourcePos return (Src before after tokens, x) {-| Wrap a `Parser` to still match the same text, but to wrap the resulting @@ -75,9 +69,9 @@ -} noted :: Parser (Expr Src a) -> Parser (Expr Src a) noted parser = do - before <- getSourcePos + before <- Text.Megaparsec.getSourcePos (tokens, e) <- Text.Megaparsec.match parser - after <- getSourcePos + after <- Text.Megaparsec.getSourcePos let src₀ = Src before after tokens case e of Note src₁ _ | laxSrcEq src₀ src₁ -> return e @@ -137,11 +131,11 @@ _lambda whitespace _openParens - whitespace + src0 <- src whitespace a <- label - whitespace + src1 <- src whitespace _colon - nonemptyWhitespace + src2 <- src nonemptyWhitespace b <- expression whitespace _closeParens @@ -149,7 +143,7 @@ _arrow whitespace c <- expression - return (Lam a b c) + return (Lam (FunctionBinding (Just src0) a (Just src1) (Just src2) b) c) alternative1 = do try (_if *> nonemptyWhitespace) @@ -443,18 +437,29 @@ selectorExpression = noted (do a <- primitiveExpression - let recordType = _openParens *> whitespace *> expression <* whitespace <* _closeParens + let recordType = whitespace *> _openParens *> whitespace *> expression <* whitespace <* _closeParens let field x e = Field e x let projectBySet xs e = Project e (Left xs) let projectByExpression xs e = Project e (Right xs) + let fieldSelection = do + src0 <- src whitespace + l <- anyLabel + pos <- Text.Megaparsec.getSourcePos + + -- FIXME: Suffix whitespace can't be parsed given our limitation + -- about whitespace treatment, but for @dhall-docs@ this + -- is enough + let src1 = Src pos pos "" + return (FieldSelection (Just src0) l (Just src1)) + let alternatives = - fmap field anyLabel - <|> fmap projectBySet labels + fmap field fieldSelection + <|> fmap projectBySet (whitespace *> labels) <|> fmap projectByExpression recordType - b <- Text.Megaparsec.many (try (whitespace *> _dot *> whitespace *> alternatives)) + b <- Text.Megaparsec.many (try (whitespace *> _dot *> alternatives)) return (foldl' (\e k -> k e) a b) ) primitiveExpression = @@ -786,12 +791,15 @@ nonEmptyRecordTypeOrLiteral firstSrc0 = do let nonEmptyRecordType = do - a <- try (anyLabelOrSome <* whitespace <* _colon) - nonemptyWhitespace + (firstKeySrc1, a) <- try $ do + a <- anyLabelOrSome + s <- src whitespace + _colon + return (s, a) - b <- expression + firstKeySrc2 <- src nonemptyWhitespace - whitespace + b <- expression e <- Text.Megaparsec.many $ do (src0', c) <- try $ do @@ -800,48 +808,60 @@ c <- anyLabelOrSome return (src0', c) - whitespace + src1 <- src whitespace _colon - nonemptyWhitespace + src2 <- src nonemptyWhitespace d <- expression whitespace - return (c, RecordField (Just src0') d) + return (c, RecordField (Just src0') d (Just src1) (Just src2)) _ <- optional (whitespace *> _comma) whitespace - m <- toMap ((a, RecordField (Just firstSrc0) b) : e) + m <- toMap ((a, RecordField (Just firstSrc0) b (Just firstKeySrc1) (Just firstKeySrc2)) : e) return (Record m) let keysValue maybeSrc = do - src0 <- case maybeSrc of + firstSrc0' <- case maybeSrc of Just src0 -> return src0 Nothing -> src whitespace - keys <- Combinators.NonEmpty.sepBy1 anyLabelOrSome (try (whitespace *> _dot) *> whitespace) + firstLabel <- anyLabelOrSome + firstSrc1 <- src whitespace + let parseLabelWithWhsp = try $ do + _dot + src0 <- src whitespace + l <- anyLabelOrSome + src1 <- src whitespace + return (src0, l, src1) + + restKeys <- Combinators.many parseLabelWithWhsp + let keys = (firstSrc0', firstLabel, firstSrc1) :| restKeys + let normalRecordEntry = do - try (whitespace *> _equal) + try _equal - whitespace + lastSrc2 <- src whitespace value <- expression - let cons key (key', values@(RecordField s0 _)) = - (key, RecordField s0 $ RecordLit [ (key', values) ]) + let cons (s0, key, s1) (key', values) = + (key, RecordField (Just s0) (RecordLit [ (key', values) ]) (Just s1) Nothing) - let nil = (NonEmpty.last keys, RecordField (Just src0) value) + let (lastSrc0, lastLabel, lastSrc1) = NonEmpty.last keys + let nil = (lastLabel, RecordField (Just lastSrc0) value (Just lastSrc1) (Just lastSrc2)) return (foldr cons nil (NonEmpty.init keys)) let punnedEntry = case keys of - x :| [] -> return (x, RecordField (Just src0) $ Var (V x 0)) + (s0, x, s1) :| [] -> return (x, RecordField (Just s0) (Var (V x 0)) (Just s1) Nothing) _ -> empty (normalRecordEntry <|> punnedEntry) <* whitespace diff --git a/src/Dhall/Parser/Token.hs b/src/Dhall/Parser/Token.hs --- a/src/Dhall/Parser/Token.hs +++ b/src/Dhall/Parser/Token.hs @@ -185,7 +185,7 @@ let negative = fmap (\_ -> negate) (char '-') positive <|> negative ) "sign" -{-| Parse a `Double` literal +{-| Parse a `Dhall.Syntax.Double` literal This corresponds to the @double-literal@ rule from the official grammar -} @@ -257,7 +257,7 @@ a <- text "Infinity" >> return (1.0/0.0) return (sign a) ) "literal" -{-| Parse an `Integer` literal +{-| Parse an `Dhall.Syntax.Integer` literal This corresponds to the @integer-literal@ rule from the official grammar -} @@ -267,7 +267,7 @@ a <- naturalLiteral return (sign (fromIntegral a)) ) "literal" -{-| Parse a `Natural` literal +{-| Parse a `Dhall.Syntax.Natural` literal This corresponds to the @natural-literal@ rule from the official grammar -} @@ -552,7 +552,7 @@ || ('\x23' <= c && c <= '\x2E') || ('\x30' <= c && c <= '\x10FFFF') -{-| The `pathComponent` function uses this type to distinguish whether to parse +{-| The @pathComponent@ function uses this type to distinguish whether to parse a URL path component or a file path component -} data ComponentType = URLComponent | FileComponent diff --git a/src/Dhall/Pretty/Internal.hs b/src/Dhall/Pretty/Internal.hs --- a/src/Dhall/Pretty/Internal.hs +++ b/src/Dhall/Pretty/Internal.hs @@ -1,6 +1,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall #-} @@ -16,6 +17,7 @@ , CharacterSet(..) , prettyCharacterSet + , prettyImportExpression , prettyVar , pretty_ @@ -77,6 +79,7 @@ import qualified Data.HashSet import qualified Data.List import qualified Data.List.NonEmpty as NonEmpty +import qualified Data.Maybe import qualified Data.Set import qualified Data.Text as Text import qualified Data.Text.Prettyprint.Doc as Pretty @@ -157,18 +160,29 @@ -> Doc Ann renderSrc strip (Just (Src {..})) | not (Text.all isWhitespace srcText) = - Pretty.align (Pretty.concatWith f newLines <> suffix) + renderComment (strip srcText) +renderSrc _ _ = + mempty + +{-| Render a comment. + + Any preprocessing, such as whitespace stripping, needs to be handled by the + caller, see e.g. 'renderSrc'. + + See the documentation for 'renderSrc' for examples. +-} +renderComment :: Text -> Doc Ann +renderComment text = + Pretty.align (Pretty.concatWith f newLines <> suffix) where horizontalSpace c = c == ' ' || c == '\t' - strippedText = strip srcText - suffix = - if Text.null strippedText || Text.last strippedText == '\n' + if Text.null text || Text.last text == '\n' then mempty else " " - oldLines = Text.splitOn "\n" strippedText + oldLines = Text.splitOn "\n" text spacePrefix = Text.takeWhile horizontalSpace @@ -197,9 +211,27 @@ in Pretty.pretty l0 : map perLine ls f x y = x <> Pretty.hardline <> y -renderSrc _ _ = - mempty +{-| This is a variant of 'renderSrc' with the following differences: + + * The 'srcText' is stripped of all whitespace at the start and the end. + * When the stripped 'srcText' is empty, the result is 'Nothing'. +-} +renderSrcMaybe :: Maybe Src -> Maybe (Doc Ann) +renderSrcMaybe (Just Src{..}) = + case Text.dropAround isWhitespace srcText of + "" -> Nothing + t -> Just (renderComment t) +renderSrcMaybe _ = Nothing + +{-| @ + 'containsComment' mSrc ≡ 'Data.Maybe.isJust' ('renderSrcMaybe' mSrc) + @ +-} +containsComment :: Maybe Src -> Bool +containsComment Nothing = False +containsComment (Just Src{..}) = not (Text.all isWhitespace srcText) + -- Annotation helpers keyword, syntax, label, literal, builtin, operator :: Doc Ann -> Doc Ann keyword = Pretty.annotate Keyword @@ -452,10 +484,31 @@ prettyAnyLabel :: Text -> Doc Ann prettyAnyLabel = prettyLabelShared True -prettyAnyLabels :: Foldable list => list Text -> Doc Ann -prettyAnyLabels = - mconcat . Pretty.punctuate dot . fmap prettyAnyLabel . toList +prettyAnyLabels :: Foldable list => list (Maybe Src, Text, Maybe Src) -> Doc Ann +prettyAnyLabels keys = Pretty.group (Pretty.flatAlt long short) + where + short = (mconcat . Pretty.punctuate dot . map prettyKey . toList) keys + long = + case map prettyKey (toList keys) of + [] -> mempty + [doc] -> doc + doc:docs -> + Pretty.align + . mconcat + . Pretty.punctuate (Pretty.hardline <> ". ") + $ Pretty.indent 2 doc : docs + + prettyKey (mSrc0, key, mSrc1) = + Pretty.align + . mconcat + . Pretty.punctuate Pretty.hardline + . Data.Maybe.catMaybes + $ [ renderSrcMaybe mSrc0 + , Just (prettyAnyLabel key) + , renderSrcMaybe mSrc1 + ] + prettyLabels :: Set Text -> Doc Ann prettyLabels a | Data.Set.null (Dhall.Set.toSet a) = @@ -530,13 +583,33 @@ This means the structure of parsed let-blocks is preserved. -} prettyCharacterSet :: Pretty a => CharacterSet -> Expr Src a -> Doc Ann -prettyCharacterSet characterSet expression = - Pretty.group (prettyExpression expression) +prettyCharacterSet characterSet = prettyCompleteExpression where - prettyExpression a0@(Lam _ _ _) = + PrettyPrinters{..} = prettyPrinters characterSet + +-- Mainly used by the `Pretty` instance for `Import` +prettyImportExpression :: Pretty a => Expr Src a -> Doc Ann +prettyImportExpression = prettyImportExpression_ + where + PrettyPrinters{..} = prettyPrinters Unicode + +data PrettyPrinters a = PrettyPrinters + { prettyCompleteExpression :: Expr Src a -> Doc Ann + , prettyImportExpression_ :: Expr Src a -> Doc Ann + } + +prettyPrinters :: Pretty a => CharacterSet -> PrettyPrinters a +prettyPrinters characterSet = + PrettyPrinters{..} + where + prettyCompleteExpression expression = + Pretty.group (prettyExpression expression) + + prettyExpression a0@(Lam _ _) = arrows characterSet (docs a0) where - docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c + docs (Lam (FunctionBinding { functionBindingVariable = a, functionBindingAnnotation = b }) c) = + Pretty.group (Pretty.flatAlt long short) : docs c where long = (lambda characterSet <> space) <> Pretty.align @@ -703,7 +776,7 @@ <> Pretty.align (keyword "with" <> " " <> update) (update, _) = - prettyKeyValue prettyAnyLabels prettyOperatorExpression equals (b, c) + prettyKeyValue prettyOperatorExpression equals (makeKeyValue b c) prettyExpression (Assert a) = Pretty.group (Pretty.flatAlt long short) where @@ -730,18 +803,18 @@ Pretty.align ( keyword "merge" <> Pretty.hardline - <> Pretty.indent 2 (prettyImportExpression a) + <> Pretty.indent 2 (prettyImportExpression_ a) <> Pretty.hardline - <> Pretty.indent 2 (prettyImportExpression b) + <> Pretty.indent 2 (prettyImportExpression_ b) <> Pretty.hardline <> colon <> space <> prettyApplicationExpression c ) short = keyword "merge" <> space - <> prettyImportExpression a + <> prettyImportExpression_ a <> " " - <> prettyImportExpression b + <> prettyImportExpression_ b <> space <> colon <> space <> prettyApplicationExpression c prettyAnnotatedExpression (ToMap a (Just b)) = @@ -751,14 +824,14 @@ Pretty.align ( keyword "toMap" <> Pretty.hardline - <> Pretty.indent 2 (prettyImportExpression a) + <> Pretty.indent 2 (prettyImportExpression_ a) <> Pretty.hardline <> colon <> space <> prettyApplicationExpression b ) short = keyword "toMap" <> space - <> prettyImportExpression a + <> prettyImportExpression_ a <> space <> colon <> space <> prettyApplicationExpression b prettyAnnotatedExpression a0@(Annot _ _) = @@ -1076,27 +1149,27 @@ e | Note _ b <- e -> go args b | null args -> - prettyImportExpression e -- just a performance optimization + prettyImportExpression_ e -- just a performance optimization | Just doc <- preserveSource e -> app doc args | otherwise -> - app (prettyImportExpression e) args + app (prettyImportExpression_ e) args app f args = enclose' "" "" " " "" ( duplicate f - : map (fmap (Pretty.indent 2) . duplicate . prettyImportExpression) args + : map (fmap (Pretty.indent 2) . duplicate . prettyImportExpression_) args ) - prettyImportExpression :: Pretty a => Expr Src a -> Doc Ann - prettyImportExpression (Embed a) = + prettyImportExpression_ :: Pretty a => Expr Src a -> Doc Ann + prettyImportExpression_ (Embed a) = Pretty.pretty a - prettyImportExpression a + prettyImportExpression_ a | Just doc <- preserveSource a = doc | Note _ b <- a = - prettyImportExpression b + prettyImportExpression_ b | otherwise = prettyCompletionExpression a @@ -1107,7 +1180,7 @@ Pretty.align ( prettySelectorExpression a <> doubleColon - <> prettyCompletionLit 0 (recordFieldValue <$> kvs) + <> prettyCompletionLit 0 kvs ) _ -> prettySelectorExpression a <> doubleColon @@ -1121,7 +1194,7 @@ prettySelectorExpression a prettySelectorExpression :: Pretty a => Expr Src a -> Doc Ann - prettySelectorExpression (Field a b) = + prettySelectorExpression (Field a (Dhall.Syntax.fieldSelectionLabel -> b)) = prettySelectorExpression a <> dot <> prettyAnyLabel b prettySelectorExpression (Project a (Left b)) = prettySelectorExpression a <> dot <> prettyLabels b @@ -1216,9 +1289,9 @@ prettyPrimitiveExpression (TextLit a) = prettyChunks a prettyPrimitiveExpression (Record a) = - prettyRecord $ recordFieldValue <$> a + prettyRecord a prettyPrimitiveExpression (RecordLit a) = - prettyRecordLit $ recordFieldValue <$> a + prettyRecordLit a prettyPrimitiveExpression (Union a) = prettyUnion a prettyPrimitiveExpression (ListLit Nothing b) = @@ -1239,115 +1312,141 @@ prettyKeyValue :: Pretty a - => (k -> Doc Ann) - -> (Expr Src a -> Doc Ann) + => (Expr Src a -> Doc Ann) -> Doc Ann - -> (k, Expr Src a) + -> KeyValue Src a -> (Doc Ann, Doc Ann) - prettyKeyValue prettyKey prettyValue separator (key, val) = + prettyKeyValue prettyValue separator (KeyValue key mSrc val) = duplicate (Pretty.group (Pretty.flatAlt long short)) where completion _T r = - " " - <> prettySelectorExpression _T + prettySelectorExpression _T <> doubleColon <> case shallowDenote r of RecordLit kvs -> - prettyCompletionLit 2 $ recordFieldValue <$> kvs + prettyCompletionLit 2 kvs _ -> prettySelectorExpression r - short = prettyKey key + short = prettyAnyLabels key <> " " <> separator <> " " + <> case renderSrcMaybe mSrc of + Nothing -> mempty + Just doc -> doc <> Pretty.hardline <> prettyValue val - long = - prettyKey key - <> " " + long = Pretty.align + ( prettyAnyLabels key + <> preSeparator + ) <> separator - <> case shallowDenote val of - Some val' -> - " " <> builtin "Some" - <> case shallowDenote val' of - RecordCompletion _T r -> - completion _T r + <> case renderSrcMaybe mSrc of + Just doc -> + preComment + <> Pretty.align + ( doc + <> Pretty.hardline + <> prettyValue val + ) + Nothing -> + case shallowDenote val of + Some val' -> + " " + <> builtin "Some" + <> case shallowDenote val' of + RecordCompletion _T r -> + " " + <> completion _T r - RecordLit _ -> - Pretty.hardline - <> " " - <> prettyImportExpression val' + RecordLit _ -> + Pretty.hardline + <> " " + <> prettyImportExpression_ val' - ListLit _ xs - | not (null xs) -> - Pretty.hardline - <> " " - <> prettyImportExpression val' + ListLit _ xs + | not (null xs) -> + Pretty.hardline + <> " " + <> prettyImportExpression_ val' - _ -> Pretty.hardline - <> " " - <> prettyImportExpression val' + _ -> Pretty.hardline + <> " " + <> prettyImportExpression_ val' - ToMap val' Nothing -> - " " <> keyword "toMap" - <> case shallowDenote val' of - RecordCompletion _T r -> - completion _T r - _ -> Pretty.hardline - <> " " - <> prettyImportExpression val' + ToMap val' Nothing -> + " " + <> keyword "toMap" + <> case shallowDenote val' of + RecordCompletion _T r -> + completion _T r + _ -> Pretty.hardline + <> " " + <> prettyImportExpression_ val' - RecordCompletion _T r -> - completion _T r + RecordCompletion _T r -> + " " <> completion _T r - RecordLit _ -> - Pretty.hardline - <> " " - <> prettyValue val + RecordLit _ -> + Pretty.hardline + <> " " + <> prettyValue val - ListLit _ xs - | not (null xs) -> - Pretty.hardline - <> " " - <> prettyValue val + ListLit _ xs + | not (null xs) -> + Pretty.hardline + <> " " + <> prettyValue val - _ -> - Pretty.hardline - <> " " - <> prettyValue val + _ -> + Pretty.group + ( Pretty.flatAlt (Pretty.hardline <> " ") " " + <> prettyValue val + ) + where + (preSeparator, preComment) = + case key of + (_, _, mSrc2) :| [] | not (containsComment mSrc2) -> + (" ", Pretty.hardline <> " ") + _ -> + (Pretty.hardline, " ") - prettyRecord :: Pretty a => Map Text (Expr Src a) -> Doc Ann + + prettyRecord :: Pretty a => Map Text (RecordField Src a) -> Doc Ann prettyRecord = braces - . map (prettyKeyValue prettyAnyLabel prettyExpression colon) + . map (prettyKeyValue prettyExpression colon . adapt) . Map.toList + where + adapt (key, RecordField mSrc0 val mSrc1 mSrc2) = KeyValue (pure (mSrc0, key, mSrc1)) mSrc2 val - prettyRecordLit :: Pretty a => Map Text (Expr Src a) -> Doc Ann + prettyRecordLit :: Pretty a => Map Text (RecordField Src a) -> Doc Ann prettyRecordLit = prettyRecordLike braces - prettyCompletionLit :: Pretty a => Int -> Map Text (Expr Src a) -> Doc Ann + prettyCompletionLit :: Pretty a => Int -> Map Text (RecordField Src a) -> Doc Ann prettyCompletionLit = prettyRecordLike . hangingBraces prettyRecordLike braceStyle a | Data.Foldable.null a = lbrace <> equals <> rbrace | otherwise = - braceStyle (map prettyRecordEntry (Map.toList consolidated)) + braceStyle (map prettyRecordEntry consolidated) where consolidated = consolidateRecordLiteral a - prettyRecordEntry (keys, value) = + prettyRecordEntry kv@(KeyValue keys mSrc2 val) = case keys of - key :| [] - | Var (V key' 0) <- Dhall.Syntax.shallowDenote value - , key == key' -> - duplicate (prettyAnyLabel key) + (mSrc0, key, mSrc1) :| [] + | Var (V key' 0) <- Dhall.Syntax.shallowDenote val + , key == key' + , not (containsComment mSrc2) -> + duplicate (prettyAnyLabels [(mSrc0, key, mSrc1)]) _ -> - prettyKeyValue prettyAnyLabels prettyExpression equals (keys, value) + prettyKeyValue prettyExpression equals kv prettyAlternative (key, Just val) = - prettyKeyValue prettyAnyLabel prettyExpression colon (key, val) + prettyKeyValue prettyExpression colon (makeKeyValue (pure key) val) prettyAlternative (key, Nothing) = duplicate (prettyAnyLabel key) @@ -1479,7 +1578,8 @@ toChunk (t0, t1) = (t0, TextLit (Chunks [] t1)) --- | Split `Text` on a predicate, preserving all parts of the original string. +-- | Split `Data.Text.Text` on a predicate, preserving all parts of the original +-- string. -- -- >>> splitOnPredicate (== 'x') "" -- ([],"") @@ -1513,27 +1613,35 @@ pretty_ :: Pretty a => a -> Text pretty_ = prettyToStrictText +data KeyValue s a = KeyValue + { _keyValueKeys :: NonEmpty (Maybe s, Text, Maybe s) + , _keyValueSrc :: Maybe s + , _keyValueValue :: Expr s a + } + +makeKeyValue :: NonEmpty Text -> Expr s a -> KeyValue s a +makeKeyValue keys expr = KeyValue (adapt <$> keys) Nothing expr + where + adapt key = (Nothing, key, Nothing) + {- This utility function converts - `{ x = { y = { z = 1 } } }` to `{ x.y.z. = 1 }` + `{ x = { y = { z = 1 } } }` to `{ x.y.z = 1 }` -} consolidateRecordLiteral - :: Map Text (Expr s a) -> Map (NonEmpty Text) (Expr s a) -consolidateRecordLiteral = Map.fromList . fmap adapt . Map.toList + :: Map Text (RecordField Src a) -> [KeyValue Src a] +consolidateRecordLiteral = map adapt . Map.toList where - adapt :: (Text, Expr s a) -> (NonEmpty Text, Expr s a) - adapt (key, expression) = - case shallowDenote expression of - RecordLit m -> - case fmap adapt (Map.toList $ recordFieldValue <$> m) of - [ (keys, expression') ] -> - (NonEmpty.cons key keys, expression') - _ -> - (pure key, RecordLit m) - _ -> - (pure key, expression) + adapt :: (Text, RecordField Src a) -> KeyValue Src a + adapt (key, RecordField mSrc0 val mSrc1 mSrc2) + | not (containsComment mSrc2) + , RecordLit m <- shallowDenote val + , [ KeyValue keys mSrc2' val' ] <- map adapt (Map.toList m) = + KeyValue (NonEmpty.cons (mSrc0, key, mSrc1) keys) mSrc2' val' + | otherwise = + KeyValue (pure (mSrc0, key, mSrc1)) mSrc2 val --- | Escape a `Text` literal using Dhall's escaping rules for single-quoted --- @Text@ +-- | Escape a `Data.Text.Text` literal using Dhall's escaping rules for +-- single-quoted @Text@ escapeSingleQuotedText :: Text -> Text escapeSingleQuotedText inputText = outputText where @@ -1541,7 +1649,7 @@ substitute before after = Text.intercalate after . Text.splitOn before -{-| Escape a `Text` literal using Dhall's escaping rules +{-| Escape a `Data.Text.Text` literal using Dhall's escaping rules Note that the result does not include surrounding quotes -} diff --git a/src/Dhall/Pretty/Internal.hs-boot b/src/Dhall/Pretty/Internal.hs-boot --- a/src/Dhall/Pretty/Internal.hs-boot +++ b/src/Dhall/Pretty/Internal.hs-boot @@ -2,6 +2,7 @@ import Data.Text (Text) import Data.Text.Prettyprint.Doc (Pretty, Doc) +import Dhall.Src (Src) import {-# SOURCE #-} Dhall.Syntax @@ -14,3 +15,5 @@ prettyExpr :: Pretty a => Expr s a -> Doc Ann prettyEnvironmentVariable :: Text -> Doc ann + +prettyImportExpression :: Pretty a => Expr Src a -> Doc Ann diff --git a/src/Dhall/Schemas.hs b/src/Dhall/Schemas.hs --- a/src/Dhall/Schemas.hs +++ b/src/Dhall/Schemas.hs @@ -185,7 +185,7 @@ let defaultedRecord = RecordLit defaultedKeyValues - return (RecordCompletion (Field "schemas" name) defaultedRecord) + return (RecordCompletion (Field "schemas" $ Core.makeFieldSelection name) defaultedRecord) schemasRewrite subExpression = subExpression diff --git a/src/Dhall/Set.hs b/src/Dhall/Set.hs --- a/src/Dhall/Set.hs +++ b/src/Dhall/Set.hs @@ -75,33 +75,35 @@ toSeq :: Set a -> Seq a toSeq (Set _ xs) = xs --- | Convert a `Set` to a list, preserving the original order of the elements +{-| Convert a `Dhall.Set.Set` to a list, preserving the original order of the + elements +-} toList :: Set a -> [a] toList (Set _ xs) = Data.Foldable.toList xs --- | Convert a `Set` to a list of ascending elements +-- | Convert a `Dhall.Set.Set` to a list of ascending elements toAscList :: Set a -> [a] toAscList (Set s _) = Data.Set.toAscList s --- | Convert a list to a `Set`, remembering the element order +-- | Convert a list to a `Dhall.Set.Set`, remembering the element order fromList :: Ord a => [a] -> Set a fromList = foldl' (flip append) empty -- O(n log n) time complexity, O(n) space complexity. -- Implementing it this way is a little silly, but is faster than (nub xs). -- n.b. toList . fromList = id, only if the list elements are unique --- | Convert a @"Data.Set".`Data.Set.Set`@ to a sorted `Set` +-- | Convert a @"Data.Set".`Data.Set.Set`@ to a sorted `Dhall.Set.Set` fromSet :: Data.Set.Set a -> Set a fromSet s = Set s (Data.Sequence.fromList (Data.Set.elems s)) --- | Append an element to the end of a `Set` +-- | Append an element to the end of a `Dhall.Set.Set` append :: Ord a => a -> Set a -> Set a append x os@(Set s xs) | Data.Set.member x s = os | otherwise = Set (Data.Set.insert x s) (xs |> x) -- O(log n) time complexity. --- | The empty `Set` +-- | The empty `Dhall.Set.Set` empty :: Set a empty = Set Data.Set.empty Data.Sequence.empty diff --git a/src/Dhall/Syntax.hs b/src/Dhall/Syntax.hs --- a/src/Dhall/Syntax.hs +++ b/src/Dhall/Syntax.hs @@ -6,6 +6,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} @@ -29,6 +30,10 @@ , Expr(..) , RecordField(..) , makeRecordField + , FunctionBinding(..) + , makeFunctionBinding + , FieldSelection(..) + , makeFieldSelection -- ** 'Let'-blocks , MultiLet(..) @@ -41,6 +46,7 @@ , chunkExprs , bindingExprs , recordFieldExprs + , functionBindingExprs -- ** Handling 'Note's , denote @@ -63,7 +69,7 @@ , reservedIdentifiers , reservedKeywords - -- * `Text` manipulation + -- * `Data.Text.Text` manipulation , toDoubleQuoted , longestSharedWhitespacePrefix , linesLiteral @@ -74,6 +80,9 @@ -- * Utilities , internalError + -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a + -- module cycle + , shift ) where import Control.DeepSeq (NFData) @@ -139,7 +148,7 @@ {-| Label for a bound variable - The `Text` field is the variable's name (i.e. \"@x@\"). + The `Data.Text.Text` field is the variable's name (i.e. \"@x@\"). The `Int` field disambiguates variables with the same name if there are multiple bound variables of the same name in scope. Zero refers to the @@ -166,7 +175,7 @@ > v │ > λ(x : Type) → λ(y : Type) → λ(x : Type) → x - Zero indices are omitted when pretty-printing `Var`s and non-zero indices + Zero indices are omitted when pretty-printing @Var@s and non-zero indices appear as a numeric suffix. -} data Var = V Text !Int @@ -285,41 +294,136 @@ For example, -> { {- A -} x : T } +> { {- A -} x {- B -} : {- C -} T } ... or -> { {- A -} x = T } +> { {- A -} x {- B -} = {- C -} T } will be instantiated as follows: -* @recordFieldSrc@ corresponds to the @A@ comment. -* @field@ is @"T"@ +* @recordFieldSrc0@ corresponds to the @A@ comment. +* @recordFieldValue@ is @"T"@ +* @recordFieldSrc1@ corresponds to the @B@ comment. +* @recordFieldSrc2@ corresponds to the @C@ comment. Although the @A@ comment isn't annotating the @"T"@ Record Field, -this is the best place to keep these comments +this is the best place to keep these comments. + +Note that @recordFieldSrc2@ is always 'Nothing' when the 'RecordField' is for +a punned entry, because there is no @=@ sign. For example, + +> { {- A -} x {- B -} } + +will be instantiated as follows: + +* @recordFieldSrc0@ corresponds to the @A@ comment. +* @recordFieldValue@ corresponds to @(Var "x")@ +* @recordFieldSrc1@ corresponds to the @B@ comment. +* @recordFieldSrc2@ will be 'Nothing' + +The labels involved in a record using dot-syntax like in this example: + +> { {- A -} a {- B -} . {- C -} b {- D -} . {- E -} c {- F -} = {- G -} e } + +will be instantiated as follows: + +* For both the @a@ and @b@ field, @recordfieldSrc2@ is 'Nothing' +* For the @a@ field: + * @recordFieldSrc0@ corresponds to the @A@ comment + * @recordFieldSrc1@ corresponds to the @B@ comment +* For the @b@ field: + * @recordFieldSrc0@ corresponds to the @C@ comment + * @recordFieldSrc1@ corresponds to the @D@ comment +* For the @c@ field: + * @recordFieldSrc0@ corresponds to the @E@ comment + * @recordFieldSrc1@ corresponds to the @F@ comment + * @recordFieldSrc2@ corresponds to the @G@ comment + +That is, for every label except the last one the semantics of @recordFieldSrc0@ +and @recordFieldSrc1@ are the same from a regular record label but +@recordFieldSrc2@ is always 'Nothing'. For the last keyword, all srcs are 'Just' -} data RecordField s a = RecordField - { recordFieldSrc :: Maybe s + { recordFieldSrc0 :: Maybe s , recordFieldValue :: Expr s a + , recordFieldSrc1 :: Maybe s + , recordFieldSrc2 :: Maybe s } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) -- | Construct a 'RecordField' with no src information makeRecordField :: Expr s a -> RecordField s a -makeRecordField = RecordField Nothing +makeRecordField e = RecordField Nothing e Nothing Nothing instance Bifunctor RecordField where - first k (RecordField s0 value) = - RecordField (k <$> s0) (first k value) + first k (RecordField s0 value s1 s2) = + RecordField (k <$> s0) (first k value) (k <$> s1) (k <$> s2) second = fmap +{-| Record the label of a function or a function-type expression + +For example, + +> λ({- A -} a {- B -} : {- C -} T) -> e + +will be instantiated as follows: +* @functionBindingSrc0@ corresponds to the @A@ comment +* @functionBindingVariable@ is @a@ +* @functionBindingSrc1@ corresponds to the @B@ comment +* @functionBindingSrc2@ corresponds to the @C@ comment +* @functionBindingAnnotation@ is @T@ +-} +data FunctionBinding s a = FunctionBinding + { functionBindingSrc0 :: Maybe s + , functionBindingVariable :: Text + , functionBindingSrc1 :: Maybe s + , functionBindingSrc2 :: Maybe s + , functionBindingAnnotation :: Expr s a + } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) + +-- | Smart constructor for 'FunctionBinding' with no src information +makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a +makeFunctionBinding l t = FunctionBinding Nothing l Nothing Nothing t + +instance Bifunctor FunctionBinding where + first k (FunctionBinding src0 label src1 src2 type_) = + FunctionBinding (k <$> src0) label (k <$> src1) (k <$> src2) (first k type_) + + second = fmap + +{-| Record the field on a selector-expression + +For example, + +> e . {- A -} x {- B -} + +will be instantiated as follows: +* @fieldSelectionSrc0@ corresponds to the @A@ comment +* @fieldSelectionLabel@ corresponds to @x@ +* @fieldSelectionSrc1@ corresponds to the @B@ comment + +Given our limitation that not all expressions recover their whitespaces, the +purpose of @fieldSelectionSrc1@ is to save the 'Text.Megaparsec.SourcePos' where +the @fieldSelectionLabel@ ends, but we /still/ use a 'Maybe Src' (@s = 'Src'@) +to be consistent with similar data types such as 'Binding', for example. +-} +data FieldSelection s = FieldSelection + { fieldSelectionSrc0 :: Maybe s + , fieldSelectionLabel :: !Text + , fieldSelectionSrc1 :: Maybe s + } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) + +-- | Smart constructor for 'FieldSelection' with no src information +makeFieldSelection :: Text -> FieldSelection s +makeFieldSelection t = FieldSelection Nothing t Nothing + {-| Syntax tree for expressions The @s@ type parameter is used to track the presence or absence of `Src` spans: - * If @s = `Src`@ then the code may contains `Src` spans (either in a `Noted` + * If @s = `Src`@ then the code may contains `Src` spans (either in a `Note` constructor or inline within another constructor, like `Let`) * If @s = `Void`@ then the code has no `Src` spans @@ -334,8 +438,8 @@ -- | > Var (V x 0) ~ x -- > Var (V x n) ~ x@n | Var Var - -- | > Lam x A b ~ λ(x : A) -> b - | Lam Text (Expr s a) (Expr s a) + -- | > Lam (FunctionBinding _ "x" _ _ A) b ~ λ(x : A) -> b + | Lam (FunctionBinding s a) (Expr s a) -- | > Pi "_" A B ~ A -> B -- > Pi x A B ~ ∀(x : A) -> B | Pi Text (Expr s a) (Expr s a) @@ -499,8 +603,8 @@ -- | > ToMap x (Just t) ~ toMap x : t -- > ToMap x Nothing ~ toMap x | ToMap (Expr s a) (Maybe (Expr s a)) - -- | > Field e x ~ e.x - | Field (Expr s a) Text + -- | > Field e (FieldSelection _ x _) ~ e.x + | Field (Expr s a) (FieldSelection s) -- | > Project e (Left xs) ~ e.{ xs } -- > Project e (Right t) ~ e.(t) | Project (Expr s a) (Either (Set Text) (Expr s a)) @@ -543,6 +647,8 @@ fmap f (Note s e1) = Note s (fmap f e1) fmap f (Record a) = Record $ fmap f <$> a fmap f (RecordLit a) = RecordLit $ fmap f <$> a + fmap f (Lam fb e) = Lam (f <$> fb) (f <$> e) + fmap f (Field a b) = Field (f <$> a) b fmap f expression = Lens.over unsafeSubExpressions (fmap f) expression {-# INLINABLE fmap #-} @@ -555,18 +661,24 @@ return = pure expression >>= k = case expression of - Embed a -> k a - Let a b -> Let (adaptBinding a) (b >>= k) - Note a b -> Note a (b >>= k) - Record a -> Record $ bindRecordKeyValues <$> a + Embed a -> k a + Let a b -> Let (adaptBinding a) (b >>= k) + Note a b -> Note a (b >>= k) + Record a -> Record $ bindRecordKeyValues <$> a RecordLit a -> RecordLit $ bindRecordKeyValues <$> a + Lam a b -> Lam (adaptFunctionBinding a) (b >>= k) + Field a b -> Field (a >>= k) b _ -> Lens.over unsafeSubExpressions (>>= k) expression where - bindRecordKeyValues (RecordField s0 e) = RecordField s0 (e >>= k) + bindRecordKeyValues (RecordField s0 e s1 s2) = + RecordField s0 (e >>= k) s1 s2 adaptBinding (Binding src0 c src1 d src2 e) = Binding src0 c src1 (fmap adaptBindingAnnotation d) src2 (e >>= k) + adaptFunctionBinding (FunctionBinding src0 label src1 src2 type_) = + FunctionBinding src0 label src1 src2 (type_ >>= k) + adaptBindingAnnotation (src3, f) = (src3, f >>= k) instance Bifunctor Expr where @@ -575,6 +687,8 @@ first k (Let a b ) = Let (first k a) (first k b) first k (Record a ) = Record $ first k <$> a first k (RecordLit a) = RecordLit $ first k <$> a + first k (Lam a b ) = Lam (first k a) (first k b) + first k (Field a b ) = Field (first k a) (k <$> b) first k expression = Lens.over unsafeSubExpressions (first k) expression second = fmap @@ -644,6 +758,8 @@ subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b subExpressions f (Record a) = Record <$> traverse (recordFieldExprs f) a subExpressions f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a +subExpressions f (Lam fb e) = Lam <$> functionBindingExprs f fb <*> f e +subExpressions f (Field a b) = Field <$> f a <*> pure b subExpressions f expression = unsafeSubExpressions f expression {-# INLINABLE subExpressions #-} @@ -658,7 +774,6 @@ :: Applicative f => (Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b) unsafeSubExpressions _ (Const c) = pure (Const c) unsafeSubExpressions _ (Var v) = pure (Var v) -unsafeSubExpressions f (Lam a b c) = Lam a <$> f b <*> f c unsafeSubExpressions f (Pi a b c) = Pi a <$> f b <*> f c unsafeSubExpressions f (App a b) = App <$> f a <*> f b unsafeSubExpressions f (Annot a b) = Annot <$> f a <*> f b @@ -720,7 +835,6 @@ unsafeSubExpressions f (RecordCompletion a b) = RecordCompletion <$> f a <*> f b unsafeSubExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t unsafeSubExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t -unsafeSubExpressions f (Field a b) = Field <$> f a <*> pure b unsafeSubExpressions f (Project a b) = Project <$> f a <*> traverse f b unsafeSubExpressions f (Assert a) = Assert <$> f a unsafeSubExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b @@ -731,6 +845,8 @@ unsafeSubExpressions _ (Embed {}) = unhandledConstructor "Embed" unsafeSubExpressions _ (Record {}) = unhandledConstructor "Record" unsafeSubExpressions _ (RecordLit {}) = unhandledConstructor "RecordLit" +unsafeSubExpressions _ (Lam {}) = unhandledConstructor "Lam" +unsafeSubExpressions _ (Field {}) = unhandledConstructor "Field" {-# INLINABLE unsafeSubExpressions #-} unhandledConstructor :: Text -> a @@ -763,11 +879,27 @@ :: Applicative f => (Expr s a -> f (Expr s b)) -> RecordField s a -> f (RecordField s b) -recordFieldExprs f (RecordField s0 e) = +recordFieldExprs f (RecordField s0 e s1 s2) = RecordField <$> pure s0 <*> f e + <*> pure s1 + <*> pure s2 +{-| Traverse over the immediate 'Expr' children in a 'FunctionBinding'. +-} +functionBindingExprs + :: Applicative f + => (Expr s a -> f (Expr s b)) + -> FunctionBinding s a -> f (FunctionBinding s b) +functionBindingExprs f (FunctionBinding s0 label s1 s2 type_) = + FunctionBinding + <$> pure s0 + <*> pure label + <*> pure s1 + <*> pure s2 + <*> f type_ + -- | A traversal over the immediate sub-expressions in 'Chunks'. chunkExprs :: Applicative f @@ -856,7 +988,8 @@ <> queryDoc <> foldMap prettyHeaders headers where - prettyHeaders h = " using " <> Pretty.pretty h + prettyHeaders h = + " using " <> Pretty.unAnnotate (prettyImportExpression h) File {..} = path @@ -990,14 +1123,19 @@ Combine _ b c -> Combine Nothing (denote b) (denote c) Record a -> Record $ denoteRecordField <$> a RecordLit a -> RecordLit $ denoteRecordField <$> a + Lam a b -> Lam (denoteFunctionBinding a) (denote b) + Field a (FieldSelection _ b _) -> Field (denote a) (FieldSelection Nothing b Nothing) expression -> Lens.over unsafeSubExpressions denote expression where - denoteRecordField (RecordField _ e) = RecordField Nothing (denote e) + denoteRecordField (RecordField _ e _ _) = RecordField Nothing (denote e) Nothing Nothing denoteBinding (Binding _ c _ d _ e) = Binding Nothing c Nothing (fmap denoteBindingAnnotation d) Nothing (denote e) denoteBindingAnnotation (_, f) = (Nothing, denote f) + denoteFunctionBinding (FunctionBinding _ l _ _ t) = + FunctionBinding Nothing l Nothing Nothing (denote t) + -- | The \"opposite\" of `denote`, like @first absurd@ but faster renote :: Expr Void a -> Expr s a renote = unsafeCoerce @@ -1012,7 +1150,7 @@ shallowDenote (Note _ e) = shallowDenote e shallowDenote e = e --- | The set of reserved keywords according to the `keyword` rule in the grammar +-- | The set of reserved keywords according to the @keyword@ rule in the grammar reservedKeywords :: HashSet Text reservedKeywords = Data.HashSet.fromList @@ -1170,17 +1308,114 @@ indent = Data.Text.length longestSharedPrefix +{-| `shift` is used by both normalization and type-checking to avoid variable + capture by shifting variable indices + + For example, suppose that you were to normalize the following expression: + +> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x + + If you were to substitute @y@ with @x@ without shifting any variable + indices, then you would get the following incorrect result: + +> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form + + In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in + order to avoid being misinterpreted as the @x@ bound by the innermost + lambda. If we perform that `shift` then we get the correct result: + +> λ(a : Type) → λ(x : a) → λ(x : a) → x@1 + + As a more worked example, suppose that you were to normalize the following + expression: + +> λ(a : Type) +> → λ(f : a → a → a) +> → λ(x : a) +> → λ(x : a) +> → (λ(x : a) → f x x@1) x@1 + + The correct normalized result would be: + +> λ(a : Type) +> → λ(f : a → a → a) +> → λ(x : a) +> → λ(x : a) +> → f x@1 x + + The above example illustrates how we need to both increase and decrease + variable indices as part of substitution: + + * We need to increase the index of the outer @x\@1@ to @x\@2@ before we + substitute it into the body of the innermost lambda expression in order + to avoid variable capture. This substitution changes the body of the + lambda expression to @(f x\@2 x\@1)@ + + * We then remove the innermost lambda and therefore decrease the indices of + both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one + less @x@ variable is now bound within that scope + + Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to + the indices of all variables named @x@ whose indices are greater than + @(n + m)@, where @m@ is the number of bound variables of the same name + within that scope + + In practice, @d@ is always @1@ or @-1@ because we either: + + * increment variables by @1@ to avoid variable capture during substitution + * decrement variables by @1@ when deleting lambdas after substitution + + @n@ starts off at @0@ when substitution begins and increments every time we + descend into a lambda or let expression that binds a variable of the same + name in order to avoid shifting the bound variables by mistake. +-} +shift :: Int -> Var -> Expr s a -> Expr s a +shift d (V x n) (Var (V x' n')) = Var (V x' n'') + where + n'' = if x == x' && n <= n' then n' + d else n' +shift d (V x n) (Lam (FunctionBinding src0 x' src1 src2 _A) b) = + Lam (FunctionBinding src0 x' src1 src2 _A') b' + where + _A' = shift d (V x n ) _A + b' = shift d (V x n') b + where + n' = if x == x' then n + 1 else n +shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B' + where + _A' = shift d (V x n ) _A + _B' = shift d (V x n') _B + where + n' = if x == x' then n + 1 else n +shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) = + Let (Binding src0 f src1 mt' src2 r') e' + where + e' = shift d (V x n') e + where + n' = if x == f then n + 1 else n + + mt' = fmap (fmap (shift d (V x n))) mt + r' = shift d (V x n) r +shift d v expression = Lens.over subExpressions (shift d v) expression + -- | Desugar all @with@ expressions desugarWith :: Expr s a -> Expr s a desugarWith = Optics.rewriteOf subExpressions rewrite where rewrite e@(With record (key :| []) value) = - Just (Prefer (PreferFromWith e) record (RecordLit [ (key, makeRecordField value) ])) + Just + (Prefer + (PreferFromWith e) + record + (RecordLit [ (key, makeRecordField value) ]) + ) rewrite e@(With record (key0 :| key1 : keys) value) = Just - (Prefer (PreferFromWith e) record - (RecordLit - [ (key0, makeRecordField $ With (Field record key0) (key1 :| keys) value) ] + (Let + (makeBinding "_" record) + (Prefer (PreferFromWith e) "_" + (RecordLit + [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ] + ) ) ) rewrite _ = Nothing diff --git a/src/Dhall/TH.hs b/src/Dhall/TH.hs --- a/src/Dhall/TH.hs +++ b/src/Dhall/TH.hs @@ -58,8 +58,8 @@ > < This : Natural | Other : ../Other/Type.dhall > - ... rather than duplicating the AST manually in a Haskell `Type`, you can - do: + ... rather than duplicating the AST manually in a Haskell `Dhall.Type`, you + can do: > Dhall.Type > (\case @@ -363,7 +363,7 @@ -- -- By default, the generated types only derive `GHC.Generics.Generic`, -- `Dhall.FromDhall`, and `Dhall.ToDhall`. To add any desired instances (such --- as `Eq`\/`Ord`\/`Show`), you can use the `StandaloneDeriving` language +-- as `Eq`\/`Ord`\/`Show`), you can use the @StandaloneDeriving@ language -- extension, like this: -- -- > {-# LANGUAGE DeriveAnyClass #-} diff --git a/src/Dhall/Tags.hs b/src/Dhall/Tags.hs --- a/src/Dhall/Tags.hs +++ b/src/Dhall/Tags.hs @@ -111,11 +111,11 @@ _ -> mempty {-| Used to update tag position and to build tag from term. - After getTagsFromExpr line and column in line are in `LineColumn` for each tag. + After getTagsFromExpr line and column in line are in @LineColumn@ for each tag. And tagPattern is not added. Emacs use tag pattern to check if tag is on line. It compares line from start with tag pattern and in case they are the same, relocate user. - fixPosAndDefinition change position to line and byte offset (`LineOffset`) and + fixPosAndDefinition change position to line and byte offset (@LineOffset@) and add tag pattern. For example, for Dhall string: >>> let dhallSource = "let foo = \"bar\"\nlet baz = \"qux\"" @@ -161,7 +161,7 @@ lengthInBytes = BS.length . encodeUtf8 {-| get information about term from map of lines - In most cases, `LineColumn` after `getTagsFromExpr` points to byte before term. + In most cases, @LineColumn@ after `getTagsFromExpr` points to byte before term. It's better to have term in term pattern, so this function finds and updates line number and byte offset and generate pattern. -} diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -148,8 +148,8 @@ -- >>> input auto "True" :: IO Bool -- True -- --- The `input` function can decode any value if we specify the value's expected --- `Type`: +-- The `Dhall.input` function can decode any value if we specify the value's +-- expected `Dhall.Type`: -- -- > input -- > :: Type a -- Expected type @@ -180,7 +180,7 @@ -- You can see what types `auto` supports \"out-of-the-box\" by browsing the -- instances for the `FromDhall` class. For example, the following instance -- says that we can directly decode any Dhall expression that evaluates to a --- @Bool@ into a Haskell `Bool`: +-- @Bool@ into a Haskell `Prelude.Bool`: -- -- > instance FromDhall Bool -- @@ -198,8 +198,8 @@ -- >>> input auto "[True, False]" :: IO (Vector Bool) -- [True,False] -- --- We could also specify what type to decode by providing an explicit `Type` --- instead of using `auto` with a type annotation: +-- We could also specify what type to decode by providing an explicit +-- `Dhall.Type` instead of using `auto` with a type annotation: -- -- >>> input (vector bool) "[True, False]" -- [True,False] @@ -253,7 +253,7 @@ -- ... -- -- The interpreter complains because the string @\"1\"@ cannot be decoded into a --- Haskell value of type `Bool`. This part of the type error: +-- Haskell value of type `Prelude.Bool`. This part of the type error: -- -- > - Bool -- > + Natural @@ -594,7 +594,7 @@ -- using the @dhall@ command. -- -- You can convert a record to a list of key-value pairs (a.k.a. a \"Map\") by --- using the `toMap` keyword. For example: +-- using the @toMap@ keyword. For example: -- -- > $ dhall <<< 'toMap { foo = 1, bar = 2 }' -- > [ { mapKey = "bar", mapValue = 2 }, { mapKey = "foo", mapValue = 1 } ] @@ -614,14 +614,17 @@ -- > [ n && True, n && False, n || True, n || False ] -- -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB) --- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into that --- sort of thing): +-- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into +-- that sort of thing): -- -- > $ -- ./makeBools.dhall -- > λ(n : Bool) → -- > [ n && True, n && False, n || True, n || False ] -- > -- +-- We'll be sticking to ASCII for the remainder of the tutorial, though, while +-- still pointing out Unicode equivalents as we go. +-- -- You can read this as a function of one argument named @n@ that has type -- @Bool@. This function returns a @List@ of @Bool@s. Each element of the -- @List@ depends on the input argument named @n@. @@ -644,7 +647,7 @@ -- Thanks to currying, this instance works for functions of multiple simple -- arguments: -- --- >>> dhallAnd <- input auto "λ(x : Bool) → λ(y : Bool) → x && y" :: IO (Bool -> Bool -> Bool) +-- >>> dhallAnd <- input auto "\\(x : Bool) -> \\(y : Bool) -> x && y" :: IO (Bool -> Bool -> Bool) -- >>> dhallAnd True False -- False -- @@ -666,7 +669,7 @@ -- > deriving (Generic, ToDhall) -- > -- > main = do --- > f <- input auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" +-- > f <- input auto "\\(r : { foo : Bool, bar : Bool }) -> r.foo && r.bar" -- > print (f (Example0 { foo = True, bar = False }) :: Bool) -- > print (f (Example0 { foo = True, bar = True }) :: Bool) -- @@ -686,6 +689,12 @@ -- > $ dhall --annotate <<< './makeBools.dhall' -- > (λ(n : Bool) → [ n, False, True, n ]) : ∀(n : Bool) → List Bool -- +-- The @dhall@ command emits Unicode output by default, but you can switch to +-- ASCII output using the @--ascii@ flag: +-- +-- > $ dhall --annotate --ascii <<< './makeBools.dhall' +-- > (\(n : Bool) -> [ n, False, True, n ]) : forall (n : Bool) -> List Bool +-- -- The @--annotate@ flag adds a type signature to the output to let us know -- what type the interpreter inferred for our expression. The type signature -- is @∀(n : Bool) → List Bool@ which says that @makeBools@ is a function of one @@ -693,16 +702,16 @@ -- @Bool@s. The @∀@ (U+2200) symbol is shorthand for the ASCII @forall@ -- keyword: -- --- > ∀(x : a) → b -- This type ... +-- > ∀(x : a) → b -- This type ... -- > --- > forall (x : a) → b -- ... is the same as this type +-- > forall (x : a) -> b -- ... is the same as this type -- -- ... and Dhall's @forall@ keyword behaves the same way as Haskell's @forall@ -- keyword for input values that are @Type@s: -- --- > forall (x : Type) → b -- This Dhall type ... +-- > forall (x : Type) -> b -- This Dhall type ... -- --- > forall x . b -- ... is the same as this Haskell type +-- > forall x . b -- ... is the same as this Haskell type -- -- The part where Dhall differs from Haskell is that you can also use -- @∀@/@forall@ to give names to non-@Type@ arguments (such as the first @@ -734,7 +743,7 @@ -- Remember that file paths are synonymous with their contents, so the above -- code is exactly equivalent to: -- --- > $ dhall <<< '(λ(n : Bool) → [n && True, n && False, n || True, n || False]) True' +-- > $ dhall <<< '(\(n : Bool) -> [n && True, n && False, n || True, n || False]) True' -- > [True, False, True, True] -- -- When you apply an anonymous function to an argument, you substitute the @@ -742,9 +751,9 @@ -- -- > Bound variable -- > ⇩ --- > (λ(n : Bool) → ...) True --- > ⇧ --- > Function argument +-- > (\(n : Bool) -> ...) True +-- > ⇧ +-- > Function argument -- -- So in our above example, we would replace all occurrences of @n@ with @True@, -- like this: @@ -767,7 +776,7 @@ -- __Exercise__: Create a file named @getFoo@ that is a function of the following -- type: -- --- > ∀(r : { foo : Bool, bar : Text }) → Bool +-- > forall (r : { foo : Bool, bar : Text }) -> Bool -- -- This function should take a single input argument named @r@ that is a record -- with two fields. The function should return the value of the @foo@ field. @@ -878,7 +887,7 @@ -- ... but fails with a type error if either shared field is not a record: -- -- > $ dhall --- > { foo = 1, bar = "ABC" } ∧ { foo = True } +-- > { foo = 1, bar = "ABC" } /\ { foo = True } -- > -- > Use "dhall --explain" for detailed errors -- > @@ -894,7 +903,7 @@ -- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53): -- -- > $ dhall --- > { foo : Natural } ⩓ { bar : Text } +-- > { foo : Natural } //\\ { bar : Text } -- > -- > { foo : Natural, bar : Text } -- @@ -902,7 +911,7 @@ -- operator descends recursively into record types: -- -- > $ dhall --- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural } +-- > { foo : { bar : Text } } //\\ { foo : { baz : Bool }, qux : Natural } -- > -- > { foo : { bar : Text, baz : Bool }, qux : Natural } @@ -941,7 +950,7 @@ -- function: -- -- > $ dhall --- > let twice = λ(x : Text) → x ++ x in twice "ha" +-- > let twice = \(x : Text) -> x ++ x in twice "ha" -- > -- > "haha" -- @@ -1092,10 +1101,10 @@ -- would write: -- -- > $ cat > process < λ(union : < Left : Natural | Right : Bool >) --- > → let handlers = +-- > \(union : < Left : Natural | Right : Bool >) -> +-- > let handlers = -- > { Left = Natural/even -- Natural/even is a built-in function --- > , Right = λ(b : Bool) → b +-- > , Right = \(b : Bool) -> b -- > } -- > in merge handlers union -- > EOF @@ -1125,14 +1134,14 @@ -- -- So, for example: -- --- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Left 3) +-- > merge { Left = Natural/even, Right = \(b : Bool) -> b } (< Left : Natural | Right : Bool >.Left 3) -- > = Natural/even 3 -- > = False -- -- ... and similarly: -- --- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Right True) --- > = (λ(b : Bool) → b) True +-- > merge { Left = Natural/even, Right = \(b : Bool) -> b } (< Left : Natural | Right : Bool >.Right True) +-- > = (\(b : Bool) -> b) True -- > = True -- -- Notice that each handler has to return the same type of result (@Bool@ in @@ -1165,13 +1174,13 @@ -- ... and when you @merge@ an empty alternative the correspond handler takes no -- argument: -- --- > λ(x : < Empty | Person : { name : Text, age : Natural } >) --- > → merge --- > { Empty = "Unknown" -- Note the absence of a `λ` +-- > \(x : < Empty | Person : { name : Text, age : Natural } >) -> +-- > merge +-- > { Empty = "Unknown" -- Note the absence of an anonymous function -- > --- > , Person = --- > λ(person : { name : Text, age : Natural }) --- > → "Name: ${person.name}, Age: ${Natural/show person.age}" +-- > , Person = +-- > \(person : { name : Text, age : Natural }) -> +-- > "Name: ${person.name}, Age: ${Natural/show person.age}" -- > } -- > x -- @@ -1203,14 +1212,14 @@ -- -- The equivalent function in Dhall is: -- --- > λ(a : Type) → λ(x : a) → x +-- > \(a : Type) -> \(x : a) -> x -- -- Notice how this function takes two arguments instead of one. The first -- argument is the type of the second argument. -- -- Let's illustrate how this works by actually using the above function: -- --- > $ echo "λ(a : Type) → λ(x : a) → x" > id +-- > $ echo "\\(a : Type) -> \\(x : a) -> x" > id -- -- Let's ask the interpreter for the type of this function: -- the first line: @@ -1280,7 +1289,7 @@ -- argument type then that means that the name of the argument is @"_"@. This -- is true even for user-defined functions: -- --- > $ dhall type <<< 'λ(_ : Text) → 1' +-- > $ dhall type <<< '\\(_ : Text) -> 1' -- > Text → Natural -- -- The type @Text → Natural@ is the same as @∀(_ : Text) → Natural@ @@ -1313,8 +1322,8 @@ -- complex example: -- -- > $ dhall --- > let List/map = https://prelude.dhall-lang.org/List/map --- > in λ(f : Natural → Natural) → List/map Natural Natural f [1, 2, 3] +-- > let List/map = https://prelude.dhall-lang.org/List/map +-- > in \(f : Natural → Natural) -> List/map Natural Natural f [1, 2, 3] -- > -- > λ(f : Natural → Natural) → [f 1, f 2, f 3] -- @@ -1348,8 +1357,8 @@ -- code. For example, we can add some tests to our @not@ function like this: -- -- > let not --- > : Bool → Bool --- > = λ(b : Bool) → b == False +-- > : Bool -> Bool +-- > = \(b : Bool) -> b == False -- > -- > let example0 = assert : not False === True -- > @@ -1366,8 +1375,8 @@ -- > -- ./test.dhall -- > -- > let not --- > : Bool → Bool --- > = λ(b : Bool) → b == False +-- > : Bool -> Bool +-- > = \(b : Bool) -> b == False -- > -- > let example0 = assert : not False === True -- > @@ -1528,7 +1537,7 @@ -- From Dhall's point of view, the hash is the true address and the file path -- is just a suggestion for how to obtain the import if it's not already cached. -- --- You can disable the cache by setting `XDG_CACHE_HOME` to `/var/empty` (an +-- You can disable the cache by setting @XDG_CACHE_HOME@ to `/var/empty` (an -- empty and unwritable directory), like this: -- -- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo' @@ -1620,8 +1629,8 @@ -- $rawText -- -- Sometimes you want to import the contents of a raw text file as a Dhall --- value of type `Text`. For example, one of the fields of a record might be --- the contents of a software license: +-- value of type `Dhall.Syntax.Text`. For example, one of the fields of a +-- record might be the contents of a software license: -- -- > { package = "dhall" -- > , author = "Gabriel Gonzalez" @@ -1684,30 +1693,30 @@ -- ... and run the expression through the formatter: -- -- > $ dhall format < ./unformatted --- > λ(a : Type) --- > → λ(kvss : List (List { index : Natural, value : a })) --- > → List/build +-- > λ(a : Type) → +-- > λ(kvss : List (List { index : Natural, value : a })) → +-- > List/build -- > { index : Natural, value : a } --- > ( λ(list : Type) --- > → λ(cons : { index : Natural, value : a } → list → list) --- > → λ(nil : list) --- > → ( List/fold +-- > ( λ(list : Type) → +-- > λ(cons : { index : Natural, value : a } → list → list) → +-- > λ(nil : list) → +-- > ( List/fold -- > (List { index : Natural, value : a }) -- > kvss -- > { count : Natural, diff : Natural → list } --- > ( λ(kvs : List { index : Natural, value : a }) --- > → λ(y : { count : Natural, diff : Natural → list }) --- > → { count = +-- > ( λ(kvs : List { index : Natural, value : a }) → +-- > λ(y : { count : Natural, diff : Natural → list }) → +-- > { count = -- > y.count + List/length { index : Natural, value : a } kvs -- > , diff = --- > λ(n : Natural) --- > → List/fold +-- > λ(n : Natural) → +-- > List/fold -- > { index : Natural, value : a } -- > kvs -- > list --- > ( λ(kvOld : { index : Natural, value : a }) --- > → λ(z : list) --- > → cons +-- > ( λ(kvOld : { index : Natural, value : a }) → +-- > λ(z : list) → +-- > cons -- > { index = kvOld.index + n, value = kvOld.value } -- > z -- > ) @@ -1880,7 +1889,7 @@ -- new built-in functions. This section contains a simple Haskell recipe to add -- a new @Natural/equal@ built-in function of type: -- --- > Natural/equal : Natural → Natural → Bool +-- > Natural/equal : Natural -> Natural -> Bool -- -- To do so, we: -- @@ -2030,10 +2039,10 @@ -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- --- > $ $ dhall <<< 'https://prelude.dhall-lang.org/Bool/not as Text' +-- > $ dhall <<< 'https://prelude.dhall-lang.org/Bool/not as Text' -- > '' -- > {- --- > Flip the value of a `Bool` +-- > Flip the value of a Bool -- > -} -- > let not : Bool → Bool = λ(b : Bool) → b == False -- > @@ -2237,10 +2246,10 @@ -- convenience: -- -- > $ dhall --- > let Prelude = https://prelude.dhall-lang.org/package.dhall +-- > let Prelude = https://prelude.dhall-lang.org/package.dhall -- > --- > in λ(x : Text) --- > → Prelude.List.length Text (Prelude.List.replicate 10 Text x) +-- > in \(x : Text) -> +-- > Prelude.List.length Text (Prelude.List.replicate 10 Text x) -- > -- > ∀(x : Text) → Natural -- > diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall #-} @@ -56,6 +57,7 @@ , Chunks (..) , Const (..) , Expr (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -184,19 +186,19 @@ fresh :: Ctx a -> Text -> Val a fresh Ctx{..} x = VVar x (Eval.countNames x (Eval.envNames values)) -{-| `typeWithA` is implemented internally in terms of `infer` in order to speed +{-| `typeWithA` is implemented internally in terms of @infer@ in order to speed up equivalence checking. - Specifically, we extend the `Context` to become a `Ctx`, which can store + Specifically, we extend the `Context` to become a @Ctx@, which can store the entire contents of a `let` expression (i.e. the type *and* the value - of the bound variable). By storing this extra information in the `Ctx` we + of the bound variable). By storing this extra information in the @Ctx@ we no longer need to substitute `let` expressions at all (which is very expensive!). However, this means that we need to use `Dhall.Eval.conv` to perform equivalence checking instead of `Dhall.Core.judgmentallyEqual` since - only `judgmentallyEqual` is unable to use the information stored in the - extended context for accurate equivalence checking. + only `Dhall.Core.judgmentallyEqual` is unable to use the information stored + in the extended context for accurate equivalence checking. -} infer :: forall a s @@ -227,7 +229,7 @@ go types n0 - Lam x _A b -> do + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b -> do tA' <- loop ctx _A case tA' of @@ -732,7 +734,7 @@ return (VOptional _A') Record xTs -> do - let process x (RecordField _ _T) = do + let process x (RecordField {recordFieldValue = _T}) = do tT' <- lift (loop ctx _T) case tT' of @@ -907,9 +909,12 @@ | not (Dhall.Map.member "Type" xLs') -> die (InvalidRecordCompletion "Type" l) | otherwise - -> loop ctx (Annot (Prefer PreferFromCompletion (Field l "default") r) (Field l "Type")) + -> loop ctx (Annot (Prefer PreferFromCompletion (Field l def) r) (Field l typ)) _ -> die (CompletionSchemaMustBeARecord l (quote names _L')) + where + def = Syntax.makeFieldSelection "default" + typ = Syntax.makeFieldSelection "Type" Merge t u mT₁ -> do _T' <- loop ctx t @@ -1112,7 +1117,7 @@ die (MapTypeMismatch (quote names (mapType _T')) _T₁'') - Field e x -> do + Field e (Syntax.fieldSelectionLabel -> x) -> do _E' <- loop ctx e let _E'' = quote names _E' @@ -4504,7 +4509,7 @@ _ -> mempty {-| Wrap a type error in this exception type to censor source code and - `Text` literals from the error message + `Dhall.Syntax.Text` literals from the error message -} data Censored = CensoredDetailed (DetailedTypeError Src X) diff --git a/src/Dhall/Version.hs b/src/Dhall/Version.hs --- a/src/Dhall/Version.hs +++ b/src/Dhall/Version.hs @@ -8,7 +8,7 @@ import qualified Data.Version as V import qualified Paths_dhall as P --- | The current `Version` of the Haskell implementation +-- | The current `V.Version` of the Haskell implementation dhallVersion :: V.Version dhallVersion = P.version diff --git a/tests/Dhall/Test/Dhall.hs b/tests/Dhall/Test/Dhall.hs --- a/tests/Dhall/Test/Dhall.hs +++ b/tests/Dhall/Test/Dhall.hs @@ -13,23 +13,25 @@ module Dhall.Test.Dhall where -import Control.Exception (SomeException, try) -import Data.Fix (Fix (..)) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Maybe (isJust) -import Data.Scientific (Scientific) -import Data.Sequence (Seq) -import Data.Text (Text) -import Data.Vector (Vector) -import Data.Void (Void) -import Dhall (FromDhall, ToDhall) -import Dhall.Core (Expr (..)) -import GHC.Generics (Generic, Rep) -import Numeric.Natural (Natural) -import System.Timeout (timeout) +import Control.Exception (SomeException, try) +import Data.Fix (Fix (..)) +import Data.Functor.Classes (Eq1(..), Show1(..)) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Maybe (isJust) +import Data.Scientific (Scientific) +import Data.Sequence (Seq) +import Data.Text (Text) +import Data.Vector (Vector) +import Data.Void (Void) +import Dhall (FromDhall, ToDhall) +import Dhall.Core (Expr (..)) +import GHC.Generics (Generic, Rep) +import Numeric.Natural (Natural) +import System.Timeout (timeout) import Test.Tasty import Test.Tasty.HUnit +import qualified Data.Functor.Classes as Classes import qualified Data.Text.Lazy import qualified Dhall import qualified Dhall.Core @@ -43,6 +45,17 @@ | MulF expr expr deriving (Eq, Functor, Generic, FromDhall, Show) +instance Eq1 ExprF where + liftEq _ (LitF aL) (LitF aR) = aL == aR + liftEq eq (AddF aL bL) (AddF aR bR) = (aL `eq` aR) && (bL `eq` bR) + liftEq eq (MulF aL bL) (MulF aR bR) = (aL `eq` aR) && (bL `eq` bR) + liftEq _ _ _ = False + +instance Show1 ExprF where + liftShowsPrec _ _ d (LitF a) = showsPrec d a + liftShowsPrec sp _ d (AddF a b) = Classes.showsBinaryWith sp sp "AddF" d a b + liftShowsPrec sp _ d (MulF a b) = Classes.showsBinaryWith sp sp "MulF" d a b + tests :: TestTree tests = testGroup "Input" @@ -116,9 +129,10 @@ let exampleEncoder :: Dhall.Encoder () exampleEncoder = Dhall.unionEncoder (Dhall.encodeConstructor "A") - Dhall.embed exampleEncoder () @=? Field (Union (Dhall.Map.singleton "A" Nothing)) "A" + let a = Dhall.Core.makeFieldSelection "A" + Dhall.embed exampleEncoder () @=? Field (Union (Dhall.Map.singleton "A" Nothing)) a -data RecursiveType a = RecursiveType (RecursiveType a) +newtype RecursiveType a = RecursiveType (RecursiveType a) deriving Generic instance FromDhall (RecursiveType a) diff --git a/tests/Dhall/Test/Format.hs b/tests/Dhall/Test/Format.hs --- a/tests/Dhall/Test/Format.hs +++ b/tests/Dhall/Test/Format.hs @@ -17,7 +17,7 @@ import qualified Dhall.Pretty as Pretty import qualified Dhall.Test.Util as Test.Util import qualified Test.Tasty as Tasty -import qualified Test.Tasty.HUnit as Tasty.HUnit +import qualified Test.Tasty.Silver as Tasty.Silver import qualified Turtle getTests :: IO TestTree @@ -55,22 +55,14 @@ formatTest :: CharacterSet -> Text -> TestTree formatTest characterSet prefix = - Tasty.HUnit.testCase (Text.unpack prefix) $ do - let inputFile = Text.unpack (prefix <> "A.dhall") - let outputFile = Text.unpack (prefix <> "B.dhall") - - inputText <- Text.IO.readFile inputFile - - headerAndExpr <- Core.throws (Parser.exprAndHeaderFromText mempty inputText) + let inputFile = Text.unpack (prefix <> "A.dhall") + outputFile = Text.unpack (prefix <> "B.dhall") - let actualText = format characterSet headerAndExpr - expectedText <- Text.IO.readFile outputFile + action = do + inputText <- Text.IO.readFile inputFile - let message = - "The formatted expression did not match the expected output\n" - <> "Expected:\n\n" <> Text.unpack expectedText <> "\n\n" - <> "Actual:\n\n" <> Text.unpack actualText <> "\n\n" - <> "Expected (show): " <> show expectedText <> "\n" - <> "Actual (show): " <> show actualText <> "\n" + headerAndExpr <- Core.throws (Parser.exprAndHeaderFromText mempty inputText) - Tasty.HUnit.assertBool message (actualText == expectedText) + return (format characterSet headerAndExpr) + in + Tasty.Silver.goldenVsAction (Text.unpack prefix) outputFile action id diff --git a/tests/Dhall/Test/Import.hs b/tests/Dhall/Test/Import.hs --- a/tests/Dhall/Test/Import.hs +++ b/tests/Dhall/Test/Import.hs @@ -36,6 +36,12 @@ -- -- URL: https://test.dhall-lang.org/Bool/package.dhall importDirectory "success/headerForwardingA.dhall" + , importDirectory "success/unit/RemoteAsTextA.dhall" + , importDirectory "success/unit/SimpleRemoteA.dhall" + , importDirectory "success/unit/asLocation/RemoteChain1A.dhall" + , importDirectory "success/unit/asLocation/RemoteChain2A.dhall" + , importDirectory "success/unit/asLocation/RemoteChain3A.dhall" + , importDirectory "success/unit/asLocation/RemoteChainMissingA.dhall" ] successTests <- Test.Util.discover (Turtle.chars <> "A.dhall") successTest (do diff --git a/tests/Dhall/Test/QuickCheck.hs b/tests/Dhall/Test/QuickCheck.hs --- a/tests/Dhall/Test/QuickCheck.hs +++ b/tests/Dhall/Test/QuickCheck.hs @@ -37,8 +37,10 @@ , DhallDouble (..) , Directory (..) , Expr (..) + , FieldSelection (..) , File (..) , FilePrefix (..) + , FunctionBinding (..) , Import (..) , ImportHashed (..) , ImportMode (..) @@ -60,7 +62,7 @@ import Dhall.Src (Src (..)) import Dhall.Test.Format (format) import Dhall.TypeCheck (TypeError, Typer) -import Generic.Random ((:+) (..), W, Weights, (%), ConstrGen(..)) +import Generic.Random ((:+) (..), ConstrGen (..), W, Weights, (%)) import Test.QuickCheck ( Arbitrary (..) , Gen @@ -277,11 +279,22 @@ ] instance (Arbitrary s, Arbitrary a) => Arbitrary (RecordField s a) where - arbitrary = - lift1 Dhall.Core.makeRecordField + arbitrary = lift4 RecordField shrink = genericShrink +instance (Arbitrary s, Arbitrary a) => Arbitrary (FunctionBinding s a) where + arbitrary = do + l <- label + type_ <- arbitrary + return $ FunctionBinding Nothing l Nothing Nothing type_ + + shrink = genericShrink + +instance Arbitrary s => Arbitrary (FieldSelection s) where + arbitrary = FieldSelection <$> pure Nothing <*> label <*> pure Nothing + shrink = genericShrink + instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where arbitrary = Test.QuickCheck.suchThat @@ -292,17 +305,17 @@ standardizedExpression where customGens - :: ConstrGen "Lam" 0 Text + :: ConstrGen "Lam" 0 (FunctionBinding s a) :+ ConstrGen "Pi" 0 Text - :+ ConstrGen "Field" 1 Text + :+ ConstrGen "Field" 1 (FieldSelection s) :+ ConstrGen "Project" 1 (Either (Set Text) (Expr s a)) :+ Gen Integer -- Generates all Integer fields in Expr :+ Gen Text -- Generates all Text fields in Expr :+ () customGens = - ConstrGen label - :+ ConstrGen label + ConstrGen arbitrary :+ ConstrGen label + :+ ConstrGen arbitrary :+ ConstrGen projection :+ integer -- 'Lam's and 'Pi's are encoded differently when the binding is @@ -445,7 +458,10 @@ arbitrary = do lift2 Src <*> whitespace - shrink _ = [] + shrink (Src start end text) = + (Src <$> shrink start <*> pure end <*> pure text) + ++ (Src <$> pure start <*> shrink end <*> pure text) + ++ (Src <$> pure start <*> pure end <*> shrinkWhitespace text) instance Arbitrary SourcePos where arbitrary = lift3 SourcePos @@ -603,10 +619,15 @@ Nothing -> Test.QuickCheck.discard Just v -> v where + denotedExpression :: Expr Void Import + denotedExpression = Dhall.Core.denote expression + maybeProp = do nf <- Control.Spoon.spoon (Dhall.Core.normalize expression) isNormalized <- Control.Spoon.spoon (Dhall.Core.isNormalized expression) - return $ isNormalized === (nf == expression) + -- Dhall.Core.isNormalized ignores 'Note's and other annotations. + -- So we do the same when checking the result of 'normalize'. + return $ isNormalized === (nf == denotedExpression) normalizeWithMIsConsistentWithNormalize :: Expr () Import -> Property normalizeWithMIsConsistentWithNormalize expression = diff --git a/tests/format/dottedFieldsCommentsA.dhall b/tests/format/dottedFieldsCommentsA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/dottedFieldsCommentsA.dhall @@ -0,0 +1,17 @@ +{ {- A -} + a + -- B + . -- C + b + . c + {- D -} + . d = + -- E + x +, {- F -} + e + {- G -} + . f = + {- H -} + { g = y } +} diff --git a/tests/format/dottedFieldsCommentsB.dhall b/tests/format/dottedFieldsCommentsB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/dottedFieldsCommentsB.dhall @@ -0,0 +1,17 @@ +{ {- A -} + a + -- B + . -- C + b + . c + {- D -} + . d + = -- E + x +, {- F -} + e + {- G -} + . f + = {- H -} + { g = y } +} diff --git a/tests/format/punCommentsA.dhall b/tests/format/punCommentsA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/punCommentsA.dhall @@ -0,0 +1,7 @@ +{ {- A -} + x + {- B -} +, y = + {- C -} + y +} diff --git a/tests/format/punCommentsB.dhall b/tests/format/punCommentsB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/punCommentsB.dhall @@ -0,0 +1,7 @@ +{ {- A -} + x + {- B -} +, y = + {- C -} + y +} diff --git a/tests/format/recordLitComments0A.dhall b/tests/format/recordLitComments0A.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitComments0A.dhall @@ -0,0 +1,6 @@ +{ {- A -} + x + {- B -} + = {- C -} + T +} diff --git a/tests/format/recordLitComments0B.dhall b/tests/format/recordLitComments0B.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitComments0B.dhall @@ -0,0 +1,6 @@ +{ {- A -} + x + {- B -} + = {- C -} + T +} diff --git a/tests/format/recordLitComments1A.dhall b/tests/format/recordLitComments1A.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitComments1A.dhall @@ -0,0 +1,4 @@ +{ +--| a comment for y +y = 42 +} diff --git a/tests/format/recordLitComments1B.dhall b/tests/format/recordLitComments1B.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitComments1B.dhall @@ -0,0 +1,3 @@ +{ --| a comment for y + y = 42 +} diff --git a/tests/format/recordLitMultilineBlockCommentsA.dhall b/tests/format/recordLitMultilineBlockCommentsA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitMultilineBlockCommentsA.dhall @@ -0,0 +1,9 @@ +{ {- A + A -} + x + {- B + B -} + = {- C + C -} + y +} diff --git a/tests/format/recordLitMultilineBlockCommentsB.dhall b/tests/format/recordLitMultilineBlockCommentsB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordLitMultilineBlockCommentsB.dhall @@ -0,0 +1,9 @@ +{ {- A + A -} + x + {- B + B -} + = {- C + C -} + y +} diff --git a/tests/format/recordTypeCommentsA.dhall b/tests/format/recordTypeCommentsA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordTypeCommentsA.dhall @@ -0,0 +1,6 @@ +{ {- A -} + a + {- B -} + : {- C -} + A +} diff --git a/tests/format/recordTypeCommentsB.dhall b/tests/format/recordTypeCommentsB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/recordTypeCommentsB.dhall @@ -0,0 +1,6 @@ +{ {- A -} + a + {- B -} + : {- C -} + A +} diff --git a/tests/format/usingToMapA.dhall b/tests/format/usingToMapA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/usingToMapA.dhall @@ -0,0 +1,1 @@ +https://httpbin.org/headers using (toMap { TOKEN = "AAAA" }) as Text diff --git a/tests/format/usingToMapB.dhall b/tests/format/usingToMapB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/usingToMapB.dhall @@ -0,0 +1,1 @@ +https://httpbin.org/headers using (toMap { TOKEN = "AAAA" }) as Text