diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,41 @@ +1.32.0 + +* [Supports version 16.0.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v16.0.0) + * BREAKING CHANGE: Change the precedence of `with` and `===` + * The precedence change to `with` means that some old expressions that + were valid now require explicit parentheses + * BREAKING CHANGE: Use RFC7049bis encoding for `Double`s + * This is a breaking change because the hashes of expressions with small + `Double` literals will change now + * Add support for unions mixing terms and types + * For example, `< A : Bool | B : Type >` is legal now + * You can now write `someRecord with a.b.c = x` to update a nested + fields + * [Add support for record puns](https://github.com/dhall-lang/dhall-haskell/pull/1710) + * You can now write `{ x, y }` as a shorthand for `{ x = x, y = y }` +* DEPRECATION: [Deprecate `Dhall.Parser.exprA`](https://github.com/dhall-lang/dhall-haskell/pull/1740) + * `Dhall.Parser` module will eventually drop support for parsing custom + import types + * This is necessary in order to fix several parsing bugs and improve + parsing error messages +* BUG FIX: [GHC Generics instance for `:+:` now uses `union`](https://github.com/dhall-lang/dhall-haskell/pull/1725) + * This fixes a few subtle bugs in how Dhall unions are marshalled into + Haskell types, and also improves the error messages +* Formatting improvements + * [Change formatting of `if` expressions](https://github.com/dhall-lang/dhall-haskell/pull/1767) + * [Change formatting for functions and their types](https://github.com/dhall-lang/dhall-haskell/pull/1759) + * [Prefer puns when formatting record completions](https://github.com/dhall-lang/dhall-haskell/pull/1736) +* [Convert union alternatives to directory tree](https://github.com/dhall-lang/dhall-haskell/pull/1757) + * `dhall to-directory-tree` now supports unions which are automatically + unwrapped +* [Fix `dhall freeze --cache` to better handle protected imports](https://github.com/dhall-lang/dhall-haskell/pull/1772) + * `dhall freeze --cache` will now also update imports that already have + integrity checks +* [Don't normalized partially saturated `{List,Natural}/fold`](https://github.com/dhall-lang/dhall-haskell/pull/1742) + * The behavior now matches the standard. Previously, the Haskell + implementation was not standards-compliant because it would normalize + these partially saturated built-ins + 1.31.1 * BUG FIX: [Allow whitespace after record pun entry](https://github.com/dhall-lang/dhall-haskell/pull/1733) diff --git a/dhall-lang/Prelude/List/index b/dhall-lang/Prelude/List/index new file mode 100644 --- /dev/null +++ b/dhall-lang/Prelude/List/index @@ -0,0 +1,19 @@ +{- +Retrieve an element from a `List` using its 0-based index +-} +let drop = + ./drop sha256:af983ba3ead494dd72beed05c0f3a17c36a4244adedf7ced502c6512196ed0cf + ? ./drop + +let index + : Natural → ∀(a : Type) → List a → Optional a + = λ(n : Natural) → λ(a : Type) → λ(xs : List a) → List/head a (drop n a xs) + +let property = + λ(n : Natural) → λ(a : Type) → assert : index n a ([] : List a) ≡ None a + +let example0 = assert : index 1 Natural [ 2, 3, 5 ] ≡ Some 3 + +let example1 = assert : index 1 Natural ([] : List Natural) ≡ None Natural + +in index diff --git a/dhall-lang/Prelude/List/package.dhall b/dhall-lang/Prelude/List/package.dhall --- a/dhall-lang/Prelude/List/package.dhall +++ b/dhall-lang/Prelude/List/package.dhall @@ -34,6 +34,9 @@ , head = ./head sha256:0d2e65ba0aea908377e46d22020dc3ad970284f4ee4eb8e6b8c51e53038c0026 ? ./head +, index = + ./index sha256:e657b55ecae4d899465c3032cb1a64c6aa6dc2aa3034204f3c15ce5c96c03e63 + ? ./index , indexed = ./indexed sha256:58bb44457fa81adf26f5123c1b2e8bef0c5aa22dac5fa5ebdfb7da84563b027f ? ./indexed @@ -70,4 +73,7 @@ , unzip = ./unzip sha256:4d6003e9e683a289fe33f4c90f958eb1e08ea0bbb474210fcd90d1885c9660e9 ? ./unzip +, zip = + ./zip sha256:7be343f42cddb7e3b5884611ae5c8731e76e52b22d7bb45420cae7c9a82be0ca + ? ./zip } diff --git a/dhall-lang/Prelude/List/zip b/dhall-lang/Prelude/List/zip new file mode 100644 --- /dev/null +++ b/dhall-lang/Prelude/List/zip @@ -0,0 +1,49 @@ +{- +Zip two `List` into a single `List` + +Resulting `List` will have the length of the shortest of its arguments. +-} +let List/drop = + ./drop sha256:af983ba3ead494dd72beed05c0f3a17c36a4244adedf7ced502c6512196ed0cf + +let zip + : ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b } + = λ(a : Type) + → λ(xa : List a) + → λ(b : Type) + → λ(xb : List b) + → let Carry = { acc : List { _1 : a, _2 : b }, context : List b } + + let cons = + λ(elem : a) + → λ(prev : Carry) + → let nextAcc = + merge + { Some = + λ(bb : b) → [ { _1 = elem, _2 = bb } ] # prev.acc + , None = prev.acc + } + (List/head b prev.context) + + in { acc = nextAcc, context = List/drop 1 b prev.context } + + let nil = { acc = [] : List { _1 : a, _2 : b }, context = xb } + + let result = List/fold a xa Carry cons nil + + in result.acc + +let example0 = + assert + : zip Text [ "ABC", "DEF", "GHI" ] Bool [ True, False, True ] + ≡ [ { _1 = "ABC", _2 = True } + , { _1 = "DEF", _2 = False } + , { _1 = "GHI", _2 = True } + ] + +let example1 = + assert + : zip Text [ "ABC" ] Bool ([] : List Bool) + ≡ ([] : List { _1 : Text, _2 : Bool }) + +in zip diff --git a/dhall-lang/Prelude/Text/package.dhall b/dhall-lang/Prelude/Text/package.dhall --- a/dhall-lang/Prelude/Text/package.dhall +++ b/dhall-lang/Prelude/Text/package.dhall @@ -16,7 +16,13 @@ , defaultMap = ./defaultMap sha256:3a3fa1264f6198800c27483cb144de2c5366484876d60b9c739a710ce0288588 ? ./defaultMap +, replicate = + ./replicate sha256:1b398b1d464b3a6c7264a690ac3cacb443b5683b43348c859d68e7c2cb925c4f + ? ./replicate , show = ./show sha256:c9dc5de3e5f32872dbda57166804865e5e80785abe358ff61f1d8ac45f1f4784 ? ./show +, spaces = + ./spaces sha256:fccfd4f26601e006bf6a79ca948dbd37c676cdd0db439554447320293d23b3dc + ? ./spaces } diff --git a/dhall-lang/Prelude/Text/replicate b/dhall-lang/Prelude/Text/replicate new file mode 100644 --- /dev/null +++ b/dhall-lang/Prelude/Text/replicate @@ -0,0 +1,21 @@ +{- +Build a Text by copying the given Text the specified number of times +-} + +let concat = + ./concat sha256:731265b0288e8a905ecff95c97333ee2db614c39d69f1514cb8eed9259745fc0 + ? ./concat + +let List/replicate = + ../List/replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347 + ? ../List/replicate + +let replicate + : Natural → Text → Text + = λ(num : Natural) → λ(text : Text) → concat (List/replicate num Text text) + +let example0 = assert : replicate 3 "foo" ≡ "foofoofoo" + +let property = λ(text : Text) → assert : replicate 0 text ≡ "" + +in replicate diff --git a/dhall-lang/Prelude/Text/spaces b/dhall-lang/Prelude/Text/spaces new file mode 100644 --- /dev/null +++ b/dhall-lang/Prelude/Text/spaces @@ -0,0 +1,20 @@ +{- +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. +-} + +let replicate = + ./replicate sha256:1b398b1d464b3a6c7264a690ac3cacb443b5683b43348c859d68e7c2cb925c4f + ? ./replicate + +let spaces + : Natural → Text + = λ(a : Natural) → replicate a " " + +let example0 = assert : spaces 1 ≡ " " + +let example1 = assert : spaces 0 ≡ "" + +in spaces diff --git a/dhall-lang/Prelude/package.dhall b/dhall-lang/Prelude/package.dhall --- a/dhall-lang/Prelude/package.dhall +++ b/dhall-lang/Prelude/package.dhall @@ -11,7 +11,7 @@ ./Integer/package.dhall sha256:d1a572ca3a764781496847e4921d7d9a881c18ffcfac6ae28d0e5299066938a0 ? ./Integer/package.dhall , List = - ./List/package.dhall sha256:67899380860ce07a2d5d9530dc502800f2c11c73c2d64e8c827f4920b5473887 + ./List/package.dhall sha256:10b6d87a09a77bfc1fdef554b7e62abb1b1f0a9267776d834f598ab240ef526c ? ./List/package.dhall , Location = ./Location/package.dhall sha256:0eb4e4a60814018009c720f6820aaa13cf9491eb1b09afb7b832039c6ee4d470 @@ -32,7 +32,7 @@ ./JSON/package.dhall sha256:1b02c5ff4710f90ee3f8dc1a2565f1b52b45e5317e2df4775307e2ba0cadcf21 ? ./JSON/package.dhall , Text = - ./Text/package.dhall sha256:3a5e3acde76fe5f90bd296e6c9d2e43e6ae81c56f804029b39352d2f1664b769 + ./Text/package.dhall sha256:819a967038fbf6f28cc289fa2651e42835f70b326210c86e51acf48f46f913d8 ? ./Text/package.dhall , XML = ./XML/package.dhall sha256:137e7b106b2e9743970e5d37b21a165f2e40f56ab593a4dd10605c9acd686fc6 diff --git a/dhall-lang/tests/import/data/file with spaces.txt b/dhall-lang/tests/import/data/file with spaces.txt new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/data/file with spaces.txt @@ -0,0 +1,1 @@ +True diff --git a/dhall-lang/tests/import/data/poisonedCache.dhall b/dhall-lang/tests/import/data/poisonedCache.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/data/poisonedCache.dhall @@ -0,0 +1,4 @@ +{- This file has a poisoned cache entry. We want to + ensure we ignore cache entries which don't match + the hash -} +"Correct benign content" diff --git a/dhall-lang/tests/import/success/unit/FilenameWithSpacesA.dhall b/dhall-lang/tests/import/success/unit/FilenameWithSpacesA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/FilenameWithSpacesA.dhall @@ -0,0 +1,1 @@ +../../data/"file with spaces.txt" diff --git a/dhall-lang/tests/import/success/unit/FilenameWithSpacesB.dhall b/dhall-lang/tests/import/success/unit/FilenameWithSpacesB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/FilenameWithSpacesB.dhall @@ -0,0 +1,1 @@ +True diff --git a/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheA.dhall b/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheA.dhall @@ -0,0 +1,1 @@ +../../data/poisonedCache.dhall sha256:618f785ce8f3930a9144398f576f0a992544b51212bc9108c31b4e670dc6ed21 diff --git a/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheB.dhall b/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/IgnorePoisonedCacheB.dhall @@ -0,0 +1,1 @@ +"Correct benign content" diff --git a/dhall-lang/tests/import/success/unit/QuotedPathA.dhall b/dhall-lang/tests/import/success/unit/QuotedPathA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/QuotedPathA.dhall @@ -0,0 +1,1 @@ +../".."/"data"/"example.txt" as Text diff --git a/dhall-lang/tests/import/success/unit/QuotedPathB.dhall b/dhall-lang/tests/import/success/unit/QuotedPathB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/import/success/unit/QuotedPathB.dhall @@ -0,0 +1,3 @@ +'' +Hello, world! +'' diff --git a/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsA.dhall b/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsA.dhall @@ -0,0 +1,16 @@ +{- The Haskell implementation was incorrectly normalizing partially + saturated `Natural/fold` and `List/fold` built-ins even though the standard + requires built-ins to be fully saturated before normalization. + + For example, the Haskell implementation was normalizing `Natural/fold 0` to: + + λ(natural : Type) + → λ(succ : natural → natural) + → λ(zero : natural) + → zero + + ... when the correct result should have been `Natural/fold 0` (no change) +-} +{ example0 = Natural/fold 0 +, example1 = List/fold Bool [ True ] +} diff --git a/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsB.dhall b/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/normalization/success/regression/UnsaturatedBuiltinsB.dhall @@ -0,0 +1,3 @@ +{ example0 = Natural/fold 0 +, example1 = List/fold Bool [ True ] +} diff --git a/dhall-lang/tests/parser/failure/unit/WithPrecedence1.dhall b/dhall-lang/tests/parser/failure/unit/WithPrecedence1.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/failure/unit/WithPrecedence1.dhall @@ -0,0 +1,1 @@ +{ x = 0 } // { y = 1 } with x = 1 diff --git a/dhall-lang/tests/parser/failure/unit/WithPrecedence2.dhall b/dhall-lang/tests/parser/failure/unit/WithPrecedence2.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/failure/unit/WithPrecedence2.dhall @@ -0,0 +1,1 @@ +foo { x = 0 } with x = 1 diff --git a/dhall-lang/tests/parser/failure/unit/WithPrecedence3.dhall b/dhall-lang/tests/parser/failure/unit/WithPrecedence3.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/failure/unit/WithPrecedence3.dhall @@ -0,0 +1,1 @@ +{ x = 0 } with x = 1 : T diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit16bitA.dhall b/dhall-lang/tests/parser/success/unit/DoubleLit16bitA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/DoubleLit16bitA.dhall @@ -0,0 +1,1 @@ +5.5 diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit16bitB.dhallb b/dhall-lang/tests/parser/success/unit/DoubleLit16bitB.dhallb new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/DoubleLit16bitB.dhallb @@ -0,0 +1,1 @@ +ùE€ diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit32bitA.dhall b/dhall-lang/tests/parser/success/unit/DoubleLit32bitA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/DoubleLit32bitA.dhall @@ -0,0 +1,1 @@ +5555.5 diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit32bitB.dhallb b/dhall-lang/tests/parser/success/unit/DoubleLit32bitB.dhallb new file mode 100644 Binary files /dev/null and b/dhall-lang/tests/parser/success/unit/DoubleLit32bitB.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit64bitA.dhall b/dhall-lang/tests/parser/success/unit/DoubleLit64bitA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/DoubleLit64bitA.dhall @@ -0,0 +1,1 @@ +55555555555.5 diff --git a/dhall-lang/tests/parser/success/unit/DoubleLit64bitB.dhallb b/dhall-lang/tests/parser/success/unit/DoubleLit64bitB.dhallb new file mode 100644 Binary files /dev/null and b/dhall-lang/tests/parser/success/unit/DoubleLit64bitB.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/DoubleLitExponentNoDotB.dhallb b/dhall-lang/tests/parser/success/unit/DoubleLitExponentNoDotB.dhallb Binary files a/dhall-lang/tests/parser/success/unit/DoubleLitExponentNoDotB.dhallb and b/dhall-lang/tests/parser/success/unit/DoubleLitExponentNoDotB.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/DoubleLitSecretelyIntB.dhallb b/dhall-lang/tests/parser/success/unit/DoubleLitSecretelyIntB.dhallb Binary files a/dhall-lang/tests/parser/success/unit/DoubleLitSecretelyIntB.dhallb and b/dhall-lang/tests/parser/success/unit/DoubleLitSecretelyIntB.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence1A.dhall b/dhall-lang/tests/parser/success/unit/WithPrecedence1A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/WithPrecedence1A.dhall @@ -0,0 +1,13 @@ +{- The purpose of this test is to illustrate that function application has + higher precedence than `with` so that chained with expressions parse + correctly + + The following expression should parse as: + + ({ a = Some 1 } with a = Some 2) with a = Some 3 + + ... and not parse as: + + { a = Some 1 } with a = (Some 2 with a = Some 3) +-} +{ a = Some 1 } with a = Some 2 with a = Some 3 diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/WithPrecedence1B.dhallb @@ -0,0 +1,1 @@ +„ „ ‚¡aaƒö‚‚¡aaƒö‚‚¡aaƒö‚ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence2A.dhall b/dhall-lang/tests/parser/success/unit/WithPrecedence2A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/WithPrecedence2A.dhall @@ -0,0 +1,1 @@ +{ x = 0 } with x = 1 + 1 diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb new file mode 100644 Binary files /dev/null and b/dhall-lang/tests/parser/success/unit/WithPrecedence2B.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence3A.dhall b/dhall-lang/tests/parser/success/unit/WithPrecedence3A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/WithPrecedence3A.dhall @@ -0,0 +1,1 @@ +foo::{ x = 0 } with x = 1 diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb new file mode 100644 Binary files /dev/null and b/dhall-lang/tests/parser/success/unit/WithPrecedence3B.dhallb differ diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedenceA.dhall b/dhall-lang/tests/parser/success/unit/WithPrecedenceA.dhall deleted file mode 100644 --- a/dhall-lang/tests/parser/success/unit/WithPrecedenceA.dhall +++ /dev/null @@ -1,13 +0,0 @@ -{- The purpose of this test is to illustrate that function application has - higher precedence than `with` so that chained with expressions parse - correctly - - The following expression should parse as: - - ({ a = Some 1 } with a = Some 2) with a = Some 3 - - ... and not parse as: - - { a = Some 1 } with a = (Some 2 with a = Some 3) --} -{ a = Some 1 } with a = Some 2 with a = Some 3 diff --git a/dhall-lang/tests/parser/success/unit/WithPrecedenceB.dhallb b/dhall-lang/tests/parser/success/unit/WithPrecedenceB.dhallb deleted file mode 100644 --- a/dhall-lang/tests/parser/success/unit/WithPrecedenceB.dhallb +++ /dev/null @@ -1,1 +0,0 @@ -„ „ ‚¡aaƒö‚‚¡aaƒö‚‚¡aaƒö‚ diff --git a/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceA.dhall b/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceA.dhall @@ -0,0 +1,1 @@ +2 + 3 * 4 === 4 * 3 + 2 diff --git a/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceB.dhallb b/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceB.dhallb new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/parser/success/unit/operators/PrecedenceEquivalenceB.dhallb @@ -0,0 +1,1 @@ +„ „‚„‚‚„„‚‚‚ diff --git a/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/0B.hash b/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/0B.hash --- a/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/0B.hash +++ b/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/0B.hash @@ -1,1 +1,1 @@ -sha256:17bf67209e1b636613b9f97ca5f2b8a59fab70eaab65a029be19129ec5f444ad +sha256:3c97d2d6c7d01c1c324e6e0a7fcf3b756ff56cf1bf398c4945f04898ae9325a7 diff --git a/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/1B.hash b/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/1B.hash --- a/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/1B.hash +++ b/dhall-lang/tests/semantic-hash/success/prelude/Integer/toDouble/1B.hash @@ -1,1 +1,1 @@ -sha256:d4b8848ff8a5d403469e4107f4a0cfdc42197bb3a9fcd2fa477b65dd252ce770 +sha256:fe5c1f8c6cc72fc9aeb61e3b0c5217bf62d2427bcfa678aeefeaa9d04cb9627c diff --git a/dhall-lang/tests/semantic-hash/success/prelude/Natural/toDouble/0B.hash b/dhall-lang/tests/semantic-hash/success/prelude/Natural/toDouble/0B.hash --- a/dhall-lang/tests/semantic-hash/success/prelude/Natural/toDouble/0B.hash +++ b/dhall-lang/tests/semantic-hash/success/prelude/Natural/toDouble/0B.hash @@ -1,1 +1,1 @@ -sha256:e894ad5c9620a9932e7025f1148823d20abada43ec7f6e50cbd89751a7ba638f +sha256:45b03fd4a48720ca71d4d12967cdde317c918d7c0295845cf9628784a124108d diff --git a/dhall-lang/tests/type-inference/failure/mixedUnions.dhall b/dhall-lang/tests/type-inference/failure/mixedUnions.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/failure/mixedUnions.dhall +++ /dev/null @@ -1,1 +0,0 @@ -< Left : Natural | Right : Type > diff --git a/dhall-lang/tests/type-inference/success/CacheImportsA.dhall b/dhall-lang/tests/type-inference/success/CacheImportsA.dhall --- a/dhall-lang/tests/type-inference/success/CacheImportsA.dhall +++ b/dhall-lang/tests/type-inference/success/CacheImportsA.dhall @@ -1,6 +1,11 @@ {- - This URL returns (probably) a different result for each request. This test - ensures that import results for a given URL are correctly cached within an - execution of dhall. + This URL returns (probably) a different result for each request. This test + ensures that import results for a given URL are correctly cached within an + execution of dhall. -} -let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text in 0 +let _ = + assert + : https://test.dhall-lang.org/random-string as Text + ≡ https://test.dhall-lang.org/random-string as Text + +in 0 diff --git a/dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall b/dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall --- a/dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall +++ b/dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall @@ -1,5 +1,10 @@ {- - This URL returns (probably) a different result for each request. This test - ensures that import locations are canonicalized before being cached. + This URL returns (probably) a different result for each request. This test + ensures that import locations are canonicalized before being cached. -} -let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/../csrng/csrng.php?min=0&max=1000 as Text in 0 +let _ = + assert + : https://test.dhall-lang.org/random-string as Text + ≡ https://test.dhall-lang.org/foo/../random-string as Text + +in 0 diff --git a/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsA.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsA.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Bool, y : Type } diff --git a/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsB.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/RecordTypeMixedKindsB.dhall +++ /dev/null @@ -1,1 +0,0 @@ -Kind diff --git a/dhall-lang/tests/type-inference/success/preludeB.dhall b/dhall-lang/tests/type-inference/success/preludeB.dhall --- a/dhall-lang/tests/type-inference/success/preludeB.dhall +++ b/dhall-lang/tests/type-inference/success/preludeB.dhall @@ -307,6 +307,7 @@ → list , generate : ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a , head : ∀(a : Type) → List a → Optional a + , index : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → Optional a , indexed : ∀(a : Type) → List a → List { index : Natural, value : a } , iterate : ∀(n : Natural) → ∀(a : Type) → ∀(f : a → a) → ∀(x : a) → List a , last : ∀(a : Type) → List a → Optional a @@ -330,6 +331,12 @@ → ∀(b : Type) → ∀(xs : List { _1 : a, _2 : b }) → { _1 : List a, _2 : List b } + , zip : + ∀(a : Type) + → ∀(xa : List a) + → ∀(b : Type) + → ∀(xb : List b) + → List { _1 : a, _2 : b } } , Location : { Type : Type } , Map : @@ -448,7 +455,9 @@ , concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text , default : ∀(o : Optional Text) → Text , defaultMap : ∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text + , replicate : ∀(num : Natural) → ∀(text : Text) → Text , show : Text → Text + , spaces : ∀(a : Natural) → Text } , XML : { Type : Type diff --git a/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2A.dhall b/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2A.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2A.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x = Type, y = {} } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2B.dhall b/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2B.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordMixedKinds2B.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Kind, y : Type } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsA.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsA.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x = {=}, y = Bool } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsB.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordMixedKindsB.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : {}, y : Type } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2A.dhall b/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2A.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2A.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Kind, y : Type } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2B.dhall b/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2B.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds2B.dhall +++ /dev/null @@ -1,1 +0,0 @@ -Sort diff --git a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3A.dhall b/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3A.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3A.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Kind, y : Bool } diff --git a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3B.dhall b/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3B.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecordTypeMixedKinds3B.dhall +++ /dev/null @@ -1,1 +0,0 @@ -Sort diff --git a/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsA.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsA.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x = True } ∧ { y = Bool } diff --git a/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsB.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RecursiveRecordMergeMixedKindsB.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Bool, y : Type } diff --git a/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsA.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsA.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x = {=} } ⫽ { x = Bool } diff --git a/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsB.dhall deleted file mode 100644 --- a/dhall-lang/tests/type-inference/success/simple/RightBiasedRecordMergeMixedKindsB.dhall +++ /dev/null @@ -1,1 +0,0 @@ -{ x : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/AssertSimpleA.dhall b/dhall-lang/tests/type-inference/success/unit/AssertSimpleA.dhall --- a/dhall-lang/tests/type-inference/success/unit/AssertSimpleA.dhall +++ b/dhall-lang/tests/type-inference/success/unit/AssertSimpleA.dhall @@ -1,1 +1,1 @@ -assert : (1 + 1) === 2 +assert : 1 + 1 === 2 diff --git a/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2A.dhall b/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2A.dhall @@ -0,0 +1,1 @@ +{ x = Type, y = {} } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2B.dhall b/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordMixedKinds2B.dhall @@ -0,0 +1,1 @@ +{ x : Kind, y : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsA.dhall @@ -0,0 +1,1 @@ +{ x = {=}, y = Bool } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordMixedKindsB.dhall @@ -0,0 +1,1 @@ +{ x : {}, y : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2A.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2A.dhall @@ -0,0 +1,1 @@ +{ x : Kind, y : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2B.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds2B.dhall @@ -0,0 +1,1 @@ +Sort diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3A.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3A.dhall @@ -0,0 +1,1 @@ +{ x : Kind, y : Bool } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3B.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKinds3B.dhall @@ -0,0 +1,1 @@ +Sort diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsA.dhall @@ -0,0 +1,1 @@ +{ x : Bool, y : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecordTypeMixedKindsB.dhall @@ -0,0 +1,1 @@ +Kind diff --git a/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsA.dhall @@ -0,0 +1,1 @@ +{ x = True } ∧ { y = Bool } diff --git a/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RecursiveRecordMergeMixedKindsB.dhall @@ -0,0 +1,1 @@ +{ x : Bool, y : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsA.dhall b/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsA.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsA.dhall @@ -0,0 +1,1 @@ +{ x = {=} } ⫽ { x = Bool } diff --git a/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsB.dhall b/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsB.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/RightBiasedRecordMergeMixedKindsB.dhall @@ -0,0 +1,1 @@ +{ x : Type } diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1A.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1A.dhall @@ -0,0 +1,1 @@ +< x : Kind | y : Type > diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1B.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds1B.dhall @@ -0,0 +1,1 @@ +Sort diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2A.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2A.dhall @@ -0,0 +1,1 @@ +< x : Kind | y : Bool > diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2B.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds2B.dhall @@ -0,0 +1,1 @@ +Sort diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3A.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3A.dhall @@ -0,0 +1,1 @@ +< x : Bool | y : Type > diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3B.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds3B.dhall @@ -0,0 +1,1 @@ +Kind diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4A.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4A.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4A.dhall @@ -0,0 +1,1 @@ +< x : Bool | y | z : Type > diff --git a/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4B.dhall b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4B.dhall new file mode 100644 --- /dev/null +++ b/dhall-lang/tests/type-inference/success/unit/UnionTypeMixedKinds4B.dhall @@ -0,0 +1,1 @@ +Kind diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.31.1 +Version: 1.32.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.1 @@ -97,6 +97,7 @@ dhall-lang/Prelude/List/fold dhall-lang/Prelude/List/generate dhall-lang/Prelude/List/head + dhall-lang/Prelude/List/index dhall-lang/Prelude/List/indexed dhall-lang/Prelude/List/iterate dhall-lang/Prelude/List/last @@ -110,6 +111,7 @@ dhall-lang/Prelude/List/shifted dhall-lang/Prelude/List/take dhall-lang/Prelude/List/unzip + dhall-lang/Prelude/List/zip dhall-lang/Prelude/Location/Type dhall-lang/Prelude/Location/package.dhall dhall-lang/Prelude/Map/Entry @@ -167,7 +169,9 @@ dhall-lang/Prelude/Text/default dhall-lang/Prelude/Text/defaultMap dhall-lang/Prelude/Text/package.dhall + dhall-lang/Prelude/Text/replicate dhall-lang/Prelude/Text/show + dhall-lang/Prelude/Text/spaces dhall-lang/Prelude/XML/Type dhall-lang/Prelude/XML/attribute dhall-lang/Prelude/XML/element @@ -416,6 +420,7 @@ tests/diff/*.dhall tests/diff/*.txt tests/format/*.dhall + tests/freeze/*.dhall tests/lint/success/*.dhall tests/recursive/*.dhall tests/regression/*.dhall @@ -460,6 +465,7 @@ either >= 5 && < 5.1, exceptions >= 0.8.3 && < 0.11, filepath >= 1.4 && < 1.5 , + half >= 0.2.2.3 && < 0.4 , haskeline >= 0.7.2.1 && < 0.9 , hashable >= 1.2 && < 1.4 , lens-family-core >= 1.0.0 && < 2.2 , @@ -606,6 +612,7 @@ Dhall.Test.Diff Dhall.Test.Tags Dhall.Test.Format + Dhall.Test.Freeze Dhall.Test.Import Dhall.Test.Lint Dhall.Test.Normalization diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -51,6 +51,7 @@ , Interpret , InvalidDecoder(..) , ExtractErrors(..) + , ExtractError(..) , Extractor , MonadicExtractor , typeError @@ -129,7 +130,7 @@ import Control.Monad.Trans.State.Strict import Control.Monad (guard) import Data.Coerce (coerce) -import Data.Either.Validation (Validation(..), ealt, eitherToValidation, validationToEither) +import Data.Either.Validation (Validation(..), eitherToValidation, validationToEither) import Data.Fix (Fix(..)) import Data.Functor.Contravariant (Contravariant(..), (>$<), Op(..)) import Data.Functor.Contravariant.Divisible (Divisible(..), divided) @@ -147,7 +148,7 @@ import Data.Vector (Vector) import Data.Void (Void) import Data.Word (Word8, Word16, Word32, Word64) -import Dhall.Syntax (Expr(..), Chunks(..), DhallDouble(..)) +import Dhall.Syntax (Expr(..), Chunks(..), DhallDouble(..), Var(..)) import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..)) import Dhall.TypeCheck (DetailedTypeError(..), TypeError) @@ -1307,12 +1308,22 @@ "result" ) - extract_ expression0 = go0 (Dhall.Core.alphaNormalize expression0) + extract_ expression0 = extract0 expression0 where - go0 (Lam _ _ (Lam _ _ expression1)) = - fmap resultToFix (extract (autoWith inputNormalizer) expression1) - go0 _ = typeError expected_ expression0 + die = typeError expected_ expression0 + extract0 (Lam x _ expression) = extract1 (rename x "result" expression) + extract0 _ = die + + extract1 (Lam y _ expression) = extract2 (rename y "Make" expression) + extract1 _ = die + + extract2 expression = fmap resultToFix (extract (autoWith inputNormalizer) expression) + + rename a b expression + | a /= b = Dhall.Core.subst (V a 0) (Var (V b 0)) (Dhall.Core.shift 1 (V b 0) expression) + | otherwise = expression + {-| `genericAuto` is the default implementation for `auto` if you derive `FromDhall`. The difference is that you can use `genericAuto` without having to explicitly provide a `FromDhall` instance for a type as long as @@ -1464,96 +1475,27 @@ extractUnionConstructor _ = empty -instance (Constructor c1, Constructor c2, GenericFromDhall f1, GenericFromDhall f2) => GenericFromDhall (M1 C c1 f1 :+: M1 C c2 f2) where - genericAutoWithNormalizer inputNormalizer options@(InterpretOptions {..}) = pure (Decoder {..}) - where - nL :: M1 i c1 f1 a - nL = undefined - - nR :: M1 i c2 f2 a - nR = undefined - - nameL = constructorModifier (Data.Text.pack (conName nL)) - nameR = constructorModifier (Data.Text.pack (conName nR)) - - extract e0 = do - case extractUnionConstructor e0 of - Just (name, e1, _) -> - if - | name == nameL -> fmap (L1 . M1) (extractL e1) - | name == nameR -> fmap (R1 . M1) (extractR e1) - | otherwise -> typeError expected e0 - _ -> typeError expected e0 - - expected = - Union - (Dhall.Map.fromList - [ (nameL, notEmptyRecord expectedL) - , (nameR, notEmptyRecord expectedR) - ] - ) - - Decoder extractL expectedL = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - Decoder extractR expectedR = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - -instance (Constructor c, GenericFromDhall (f :+: g), GenericFromDhall h) => GenericFromDhall ((f :+: g) :+: M1 C c h) where - genericAutoWithNormalizer inputNormalizer options@(InterpretOptions {..}) = pure (Decoder {..}) - where - n :: M1 i c h a - n = undefined - - name = constructorModifier (Data.Text.pack (conName n)) - - extract u = case extractUnionConstructor u of - Just (name', e, _) -> - if - | name == name' -> fmap (R1 . M1) (extractR e) - | otherwise -> fmap L1 (extractL u) - Nothing -> typeError expected u - - expected = - Union (Dhall.Map.insert name (notEmptyRecord expectedR) ktsL) - - Decoder extractL expectedL = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - Decoder extractR expectedR = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - - ktsL = unsafeExpectUnion "genericAutoWithNormalizer (:+:)" expectedL - -instance (Constructor c, GenericFromDhall f, GenericFromDhall (g :+: h)) => GenericFromDhall (M1 C c f :+: (g :+: h)) where - genericAutoWithNormalizer inputNormalizer options@(InterpretOptions {..}) = pure (Decoder {..}) - where - n :: M1 i c f a - n = undefined - - name = constructorModifier (Data.Text.pack (conName n)) - - extract u = case extractUnionConstructor u of - Just (name', e, _) -> - if - | name == name' -> fmap (L1 . M1) (extractL e) - | otherwise -> fmap R1 (extractR u) - _ -> typeError expected u - - expected = - Union (Dhall.Map.insert name (notEmptyRecord expectedL) ktsR) - - Decoder extractL expectedL = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - Decoder extractR expectedR = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - - ktsR = unsafeExpectUnion "genericAutoWithNormalizer (:+:)" expectedR +class GenericFromDhallUnion f where + genericUnionAutoWithNormalizer :: InputNormalizer -> InterpretOptions -> UnionDecoder (f a) -instance (GenericFromDhall (f :+: g), GenericFromDhall (h :+: i)) => GenericFromDhall ((f :+: g) :+: (h :+: i)) where - genericAutoWithNormalizer inputNormalizer options = pure (Decoder {..}) - where - extract e = fmap L1 (extractL e) `ealt` fmap R1 (extractR e) +instance (GenericFromDhallUnion f1, GenericFromDhallUnion f2) => GenericFromDhallUnion (f1 :+: f2) where + genericUnionAutoWithNormalizer inputNormalizer options = + (<>) + (L1 <$> genericUnionAutoWithNormalizer inputNormalizer options) + (R1 <$> genericUnionAutoWithNormalizer inputNormalizer options) - expected = Union (Dhall.Map.union ktsL ktsR) +instance (Constructor c1, GenericFromDhall f1) => GenericFromDhallUnion (M1 C c1 f1) where + genericUnionAutoWithNormalizer inputNormalizer options@(InterpretOptions {..}) = + constructor name (evalState (genericAutoWithNormalizer inputNormalizer options) 1) + where + n :: M1 C c1 f1 a + n = undefined - Decoder extractL expectedL = evalState (genericAutoWithNormalizer inputNormalizer options) 1 - Decoder extractR expectedR = evalState (genericAutoWithNormalizer inputNormalizer options) 1 + name = constructorModifier (Data.Text.pack (conName n)) - ktsL = unsafeExpectUnion "genericAutoWithNormalizer (:+:)" expectedL - ktsR = unsafeExpectUnion "genericAutoWithNormalizer (:+:)" expectedR +instance GenericFromDhallUnion (f :+: g) => GenericFromDhall (f :+: g) where + genericAutoWithNormalizer inputNormalizer options = + pure (union (genericUnionAutoWithNormalizer inputNormalizer options)) instance GenericFromDhall f => GenericFromDhall (M1 C c f) where genericAutoWithNormalizer inputNormalizer options = do diff --git a/src/Dhall/Binary.hs b/src/Dhall/Binary.hs --- a/src/Dhall/Binary.hs +++ b/src/Dhall/Binary.hs @@ -55,6 +55,7 @@ import Data.Text (Text) import Data.Void (Void, absurd) import GHC.Float (double2Float, float2Double) +import Numeric.Half (fromHalf, toHalf) import qualified Codec.CBOR.Decoding as Decoding import qualified Codec.CBOR.Encoding as Encoding @@ -875,11 +876,11 @@ where n32 = double2Float n64 - useFloat = n64 == float2Double n32 + n16 = toHalf n32 - useHalf = n64 == 0.0 || n64 == infinity || n64 == -infinity + useFloat = n64 == float2Double n32 - infinity = 1/0 :: Double + useHalf = n64 == (float2Double $ fromHalf n16) -- Fast path for the common case of an uninterpolated string TextLit (Chunks [] z) -> diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -72,7 +72,6 @@ import Control.Exception (Exception) import Control.Monad.IO.Class (MonadIO(..)) -import Data.Semigroup (Semigroup(..)) import Data.Text (Text) import Data.Text.Prettyprint.Doc (Pretty) import Dhall.Normalize @@ -92,29 +91,6 @@ pretty :: Pretty a => a -> Text pretty = pretty_ {-# INLINE pretty #-} - -_ERROR :: String -_ERROR = "\ESC[1;31mError\ESC[0m" - -{-| Utility function used to throw internal errors that should never happen - (in theory) but that are not enforced by the type system --} -internalError :: Data.Text.Text -> forall b . b -internalError text = error (unlines - [ _ERROR <> ": Compiler bug " - , " " - , "Explanation: This error message means that there is a bug in the Dhall compiler." - , "You didn't do anything wrong, but if you would like to see this problem fixed " - , "then you should report the bug at: " - , " " - , "https://github.com/dhall-lang/dhall-haskell/issues " - , " " - , "Please include the following text in your bug report: " - , " " - , "``` " - , Data.Text.unpack text <> " " - , "``` " - ] ) {-| Escape a `Text` literal using Dhall's escaping rules diff --git a/src/Dhall/DirectoryTree.hs b/src/Dhall/DirectoryTree.hs --- a/src/Dhall/DirectoryTree.hs +++ b/src/Dhall/DirectoryTree.hs @@ -104,6 +104,9 @@ Some value -> do toDirectoryTree path value + App (Field (Union _) _) value -> do + toDirectoryTree path value + App None _ -> do return () @@ -149,7 +152,9 @@ \Explanation: Only a subset of Dhall expressions can be converted to a directory \n\ \tree. Specifically, record literals or maps can be converted to directories, \n\ \❰Text❱ literals can be converted to files, and ❰Optional❱ values are included if\n\ - \❰Some❱ and omitted if ❰None❱. No other type of value can be translated to a \n\ + \❰Some❱ and omitted if ❰None❱. Values of union types can also be converted if \n\ + \they are an alternative which has a non-nullary constructor whose argument is of\n\ + \an otherwise convertible type. No other type of value can be translated to a \n\ \directory tree. \n\ \ \n\ \For example, this is a valid expression that can be translated to a directory \n\ diff --git a/src/Dhall/Eval.hs b/src/Dhall/Eval.hs --- a/src/Dhall/Eval.hs +++ b/src/Dhall/Eval.hs @@ -452,19 +452,27 @@ NaturalLit n -> VNaturalLit n NaturalFold -> - VPrim $ \case - VNaturalLit n -> - VHLam (Typed "natural" (VConst Type)) $ \natural -> - VHLam (Typed "succ" (natural ~> natural)) $ \succ -> - VHLam (Typed "zero" natural) $ \zero -> - let go !acc 0 = acc - go acc m = go (vApp succ acc) (m - 1) - in go zero (fromIntegral n :: Integer) - n -> - VPrim $ \natural -> - VPrim $ \succ -> - VPrim $ \zero -> - VNaturalFold n natural succ zero + VPrim $ \n -> + VPrim $ \natural -> + VPrim $ \succ -> + VPrim $ \zero -> + let inert = VNaturalFold n natural succ zero + in case zero of + VPrimVar -> inert + _ -> case succ of + VPrimVar -> inert + _ -> case natural of + VPrimVar -> inert + _ -> case n of + VNaturalLit n' -> + -- Use an `Integer` for the loop, due to the + -- following issue: + -- + -- https://github.com/ghcjs/ghcjs/issues/782 + let go !acc 0 = acc + go acc m = go (vApp succ acc) (m - 1) + in go zero (fromIntegral n' :: Integer) + _ -> inert NaturalBuild -> VPrim $ \case VPrimVar -> @@ -495,7 +503,12 @@ x@(VNaturalLit m) -> VPrim $ \case VNaturalLit n - | n >= m -> VNaturalLit (subtract m n) + | n >= m -> + -- Use an `Integer` for the subtraction, due to the + -- following issue: + -- + -- https://github.com/ghcjs/ghcjs/issues/782 + VNaturalLit (fromIntegral (subtract (fromIntegral m :: Integer) (fromIntegral n :: Integer))) | otherwise -> VNaturalLit 0 y -> VNaturalSubtract x y x -> @@ -580,17 +593,23 @@ ListFold -> VPrim $ \a -> - VPrim $ \case - VListLit _ as -> - VHLam (Typed "list" (VConst Type)) $ \list -> - VHLam (Typed "cons" (a ~> list ~> list) ) $ \cons -> - VHLam (Typed "nil" list) $ \nil -> - foldr' (\x b -> cons `vApp` x `vApp` b) nil as - as -> - VPrim $ \t -> - VPrim $ \c -> - VPrim $ \n -> - VListFold a as t c n + VPrim $ \as -> + VPrim $ \list -> + VPrim $ \cons -> + VPrim $ \nil -> + let inert = VListFold a as list cons nil + in case nil of + VPrimVar -> inert + _ -> case cons of + VPrimVar -> inert + _ -> case list of + VPrimVar -> inert + _ -> case a of + VPrimVar -> inert + _ -> case as of + VListLit _ as' -> + foldr' (\x b -> cons `vApp` x `vApp` b) nil as' + _ -> inert ListLength -> VPrim $ \ a -> VPrim $ \case diff --git a/src/Dhall/Freeze.hs b/src/Dhall/Freeze.hs --- a/src/Dhall/Freeze.hs +++ b/src/Dhall/Freeze.hs @@ -7,6 +7,7 @@ module Dhall.Freeze ( -- * Freeze freeze + , freezeExpression , freezeImport , freezeRemoteImport @@ -150,56 +151,7 @@ StandardInput -> "." InputFile file -> System.FilePath.takeDirectory file - let freezeScope = - case scope of - AllImports -> freezeImport - OnlyRemoteImports -> freezeRemoteImport - - let freezeFunction = freezeScope directory - - let cache - (ImportAlt - (Core.shallowDenote -> Embed - (Import { importHashed = ImportHashed { hash = Just _expectedHash } }) - ) - import_@(Core.shallowDenote -> ImportAlt - (Embed - (Import { importHashed = ImportHashed { hash = Just _actualHash } }) - ) - _ - ) - ) = do - {- Here we could actually compare the `_expectedHash` and - `_actualHash` to see if they differ, but we choose not to do - so and instead automatically accept the `_actualHash`. This - is done for the same reason that the `freeze*` functions - ignore hash mismatches: the user intention when using `dhall - freeze` is to update the hash, which they expect to possibly - change. - -} - return import_ - cache - (Embed import_@(Import { importHashed = ImportHashed { hash = Nothing } })) = do - frozenImport <- freezeFunction import_ - - {- The two imports can be the same if the import is local and - `freezeFunction` only freezes remote imports - -} - if frozenImport /= import_ - then return (ImportAlt (Embed frozenImport) (Embed import_)) - else return (Embed import_) - cache expression = do - return expression - - let rewrite expression = - case intent of - Secure -> - traverse freezeFunction expression - Cache -> - Dhall.Optics.transformMOf - Core.subExpressions - cache - expression + let rewrite = freezeExpression directory scope intent case outputMode of Write -> do @@ -217,7 +169,7 @@ let name = case input of InputFile file -> file - StandardInput -> "(stdin)" + StandardInput -> "(input)" (Header header, parsedExpression) <- do Core.throws (first Parser.censor (Parser.exprAndHeaderFromText name originalText)) @@ -240,3 +192,99 @@ let modified = "frozen" Exception.throwIO CheckFailed{..} + +{-| Slightly more pure version of the `freeze` function + + This still requires `IO` to freeze the import, but now the input and output + expression are passed in explicitly +-} +freezeExpression + :: FilePath + -- ^ Starting directory + -> Scope + -> Intent + -> Expr s Import + -> IO (Expr s Import) +freezeExpression directory scope intent expression = do + let freezeScope = + case scope of + AllImports -> freezeImport + OnlyRemoteImports -> freezeRemoteImport + + let freezeFunction = freezeScope directory + + let cache + -- This case is necessary because `transformOf` is a bottom-up + -- rewrite rule. Without this rule, if you were to transform a + -- file that already has a cached expression, like this: + -- + -- someImport sha256:… ? someImport + -- + -- ... then you would get: + -- + -- (someImport sha256:… ? someImport) + -- ? (someImport sha256:… ? someImport) + -- + -- ... and this rule fixes that by collapsing that back to: + -- + -- (someImport sha256:… ? someImport) + (ImportAlt + (Core.shallowDenote -> ImportAlt + (Core.shallowDenote -> Embed + Import{ importHashed = ImportHashed{ hash = Just _expectedHash } } + ) + (Core.shallowDenote -> Embed + Import{ importHashed = ImportHashed{ hash = Nothing } } + ) + ) + import_@(Core.shallowDenote -> ImportAlt + (Core.shallowDenote -> Embed + Import{ importHashed = ImportHashed{ hash = Just _actualHash } } + ) + (Core.shallowDenote -> Embed + Import{ importHashed = ImportHashed{ hash = Nothing } } + ) + ) + ) = do + {- Here we could actually compare the `_expectedHash` and + `_actualHash` to see if they differ, but we choose not to do + so and instead automatically accept the `_actualHash`. This + is done for the same reason that the `freeze*` functions + ignore hash mismatches: the user intention when using `dhall + freeze` is to update the hash, which they expect to possibly + change. + -} + return import_ + cache + (Embed import_@(Import { importHashed = ImportHashed { hash = Nothing } })) = do + frozenImport <- freezeFunction import_ + + {- The two imports can be the same if the import is local and + `freezeFunction` only freezes remote imports by default + -} + if frozenImport /= import_ + then return (ImportAlt (Embed frozenImport) (Embed import_)) + else return (Embed import_) + cache + (Embed import_@(Import { importHashed = ImportHashed { hash = Just _ } })) = do + -- Regenerate the integrity check, just in case it's wrong + frozenImport <- freezeFunction import_ + + -- `dhall freeze --cache` also works the other way around, adding an + -- unprotected fallback import to imports that are already + -- protected + let thawedImport = import_ + { importHashed = (importHashed import_) + { hash = Nothing + } + } + + return (ImportAlt (Embed frozenImport) (Embed thawedImport)) + cache expression_ = do + return expression_ + + case intent of + Secure -> + traverse freezeFunction expression + Cache -> + Dhall.Optics.transformMOf Core.subExpressions cache expression diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -138,7 +138,7 @@ , HashMismatch(..) ) where -import Control.Applicative (Alternative(..)) +import Control.Applicative (Alternative(..), liftA2) import Control.Exception (Exception, SomeException, IOException, toException) import Control.Monad (when) import Control.Monad.Catch (throwM, MonadCatch(catch), handle) @@ -164,10 +164,8 @@ , ImportType(..) , ImportMode(..) , Import(..) - , PreferAnnotation(..) , URL(..) , bindingExprs - , chunkExprs ) #ifdef WITH_HTTP import Dhall.Import.HTTP @@ -197,6 +195,7 @@ import qualified Dhall.Parser import qualified Dhall.Pretty.Internal import qualified Dhall.Substitution +import qualified Dhall.Syntax as Syntax import qualified Dhall.TypeCheck import qualified System.AtomicWrite.Writer.ByteString.Binary as AtomicWrite.Binary import qualified System.Environment @@ -730,13 +729,13 @@ toHeader :: Expr s a -> Maybe HTTPHeader toHeader (RecordLit m) = do - TextLit (Chunks [] keyText ) <- - Dhall.Map.lookup "header" m <|> Dhall.Map.lookup "mapKey" m - TextLit (Chunks [] valueText) <- - Dhall.Map.lookup "value" m <|> Dhall.Map.lookup "mapValue" m + (TextLit (Chunks [] keyText), TextLit (Chunks [] valueText)) <- lookupHeader <|> lookupMapKey let keyBytes = Data.Text.Encoding.encodeUtf8 keyText let valueBytes = Data.Text.Encoding.encodeUtf8 valueText return (Data.CaseInsensitive.mk keyBytes, valueBytes) + where + lookupHeader = liftA2 (,) (Dhall.Map.lookup "header" m) (Dhall.Map.lookup "value" m) + lookupMapKey = liftA2 (,) (Dhall.Map.lookup "mapKey" m) (Dhall.Map.lookup "mapValue" m) toHeader _ = do empty @@ -1022,83 +1021,12 @@ where text₂ = text₀ <> " ? " <> text₁ - Const a -> pure (Const a) - Var a -> pure (Var a) - Lam a b c -> Lam <$> pure a <*> loadWith b <*> loadWith c - Pi a b c -> Pi <$> pure a <*> loadWith b <*> loadWith c - App a b -> App <$> loadWith a <*> loadWith b - Let a b -> Let <$> bindingExprs loadWith a <*> loadWith b - Annot a b -> Annot <$> loadWith a <*> loadWith b - Bool -> pure Bool - BoolLit a -> pure (BoolLit a) - BoolAnd a b -> BoolAnd <$> loadWith a <*> loadWith b - BoolOr a b -> BoolOr <$> loadWith a <*> loadWith b - BoolEQ a b -> BoolEQ <$> loadWith a <*> loadWith b - BoolNE a b -> BoolNE <$> loadWith a <*> loadWith b - BoolIf a b c -> BoolIf <$> loadWith a <*> loadWith b <*> loadWith c - Natural -> pure Natural - NaturalLit a -> pure (NaturalLit a) - NaturalFold -> pure NaturalFold - NaturalBuild -> pure NaturalBuild - NaturalIsZero -> pure NaturalIsZero - NaturalEven -> pure NaturalEven - NaturalOdd -> pure NaturalOdd - NaturalToInteger -> pure NaturalToInteger - NaturalShow -> pure NaturalShow - NaturalSubtract -> pure NaturalSubtract - NaturalPlus a b -> NaturalPlus <$> loadWith a <*> loadWith b - NaturalTimes a b -> NaturalTimes <$> loadWith a <*> loadWith b - Integer -> pure Integer - IntegerLit a -> pure (IntegerLit a) - IntegerClamp -> pure IntegerClamp - IntegerNegate -> pure IntegerNegate - IntegerShow -> pure IntegerShow - IntegerToDouble -> pure IntegerToDouble - Double -> pure Double - DoubleLit a -> pure (DoubleLit a) - DoubleShow -> pure DoubleShow - Text -> pure Text - TextLit chunks -> TextLit <$> chunkExprs loadWith chunks - TextAppend a b -> TextAppend <$> loadWith a <*> loadWith b - TextShow -> pure TextShow - List -> pure List - ListLit a b -> ListLit <$> mapM loadWith a <*> mapM loadWith b - ListAppend a b -> ListAppend <$> loadWith a <*> loadWith b - ListBuild -> pure ListBuild - ListFold -> pure ListFold - ListLength -> pure ListLength - ListHead -> pure ListHead - ListLast -> pure ListLast - ListIndexed -> pure ListIndexed - ListReverse -> pure ListReverse - Optional -> pure Optional - None -> pure None - Some a -> Some <$> loadWith a - OptionalFold -> pure OptionalFold - OptionalBuild -> pure OptionalBuild - Record a -> Record <$> mapM loadWith a - RecordLit a -> RecordLit <$> mapM loadWith a - Union a -> Union <$> mapM (mapM loadWith) a - Combine m a b -> Combine m <$> loadWith a <*> loadWith b - CombineTypes a b -> CombineTypes <$> loadWith a <*> loadWith b - Prefer a b c -> Prefer <$> a' <*> loadWith b <*> loadWith c - where - a' = case a of - PreferFromSource -> pure PreferFromSource - PreferFromWith e -> PreferFromWith <$> loadWith e - PreferFromCompletion -> pure PreferFromCompletion - RecordCompletion a b -> RecordCompletion <$> loadWith a <*> loadWith b - Merge a b c -> Merge <$> loadWith a <*> loadWith b <*> mapM loadWith c - ToMap a b -> ToMap <$> loadWith a <*> mapM loadWith b - Field a b -> Field <$> loadWith a <*> pure b - Project a b -> Project <$> loadWith a <*> mapM loadWith b - Assert a -> Assert <$> loadWith a - Equivalent a b -> Equivalent <$> loadWith a <*> loadWith b - With a b c -> With <$> loadWith a <*> pure b <*> loadWith c Note a b -> do let handler e = throwM (SourcedException a (e :: MissingImports)) (Note <$> pure a <*> loadWith b) `catch` handler + Let a b -> Let <$> bindingExprs loadWith a <*> loadWith b + expression -> Syntax.unsafeSubExpressions loadWith expression -- | Resolve all imports within an expression load :: Expr Src Import -> IO (Expr Src Void) diff --git a/src/Dhall/Lint.hs b/src/Dhall/Lint.hs --- a/src/Dhall/Lint.hs +++ b/src/Dhall/Lint.hs @@ -16,12 +16,14 @@ , removeLetInLet , replaceOptionalBuildFold , replaceSaturatedOptionalFold + , useToMap ) where import Control.Applicative ((<|>)) import Dhall.Syntax ( Binding(..) + , Chunks(..) , Const(..) , Directory(..) , Expr(..) @@ -34,8 +36,10 @@ , subExpressions ) +import qualified Data.Foldable as Foldable import qualified Data.List.NonEmpty as NonEmpty import qualified Dhall.Core as Core +import qualified Dhall.Map as Map import qualified Dhall.Optics import qualified Lens.Family @@ -188,4 +192,52 @@ none ) = Just (Merge (RecordLit [ ("Some", some), ("None", none) ]) o Nothing) replaceSaturatedOptionalFold _ = + Nothing + +-- | This replaces a record of key-value pairs with the equivalent use of +-- @toMap@ +-- +-- This is currently not used by @dhall lint@ because this would sort @Map@ +-- keys, which is not necessarily a behavior-preserving change, but is still +-- made available as a convenient rewrite rule. For example, +-- @{json,yaml}-to-dhall@ use this rewrite to simplify their output. +useToMap :: Expr s a -> Maybe (Expr s a) +useToMap + (ListLit + t@(Just + (Core.shallowDenote -> App + (Core.shallowDenote -> List) + (Core.shallowDenote -> Record + (Map.sort -> + [ ("mapKey", Core.shallowDenote -> Text) + , ("mapValue", _) + ] + ) + ) + ) + ) + [] + ) = + Just (ToMap (RecordLit []) t) +useToMap (ListLit _ keyValues) + | not (null keyValues) + , Just keyValues' <- traverse convert keyValues = + Just + (ToMap + (RecordLit (Map.fromList (Foldable.toList keyValues'))) + Nothing + ) + where + convert keyValue = + case Core.shallowDenote keyValue of + RecordLit + (Map.sort -> + [ ("mapKey" , (Core.shallowDenote -> TextLit (Chunks [] key))) + , ("mapValue", value) + ] + ) -> + Just (key, value) + _ -> + Nothing +useToMap _ = Nothing diff --git a/src/Dhall/Main.hs b/src/Dhall/Main.hs --- a/src/Dhall/Main.hs +++ b/src/Dhall/Main.hs @@ -218,17 +218,17 @@ Manipulate "format" "Standard code formatter for the Dhall language" - (Format <$> parseInplace <*> parseCheck) + (Format <$> parseInplace <*> parseCheck "formatted") <|> subcommand Manipulate "freeze" "Add integrity checks to remote import statements of an expression" - (Freeze <$> parseInplace <*> parseAllFlag <*> parseCacheFlag <*> parseCheck) + (Freeze <$> parseInplace <*> parseAllFlag <*> parseCacheFlag <*> parseCheck "frozen") <|> subcommand Manipulate "lint" "Improve Dhall code by using newer language features and removing dead code" - (Lint <$> parseInplace <*> parseCheck) + (Lint <$> parseInplace <*> parseCheck "linted") <|> subcommand Generate "text" @@ -452,7 +452,7 @@ <> Options.Applicative.help "Add fallback unprotected imports when using integrity checks purely for caching purposes" ) - parseCheck = fmap adapt switch + parseCheck processed = fmap adapt switch where adapt True = Check adapt False = Write @@ -460,7 +460,7 @@ switch = Options.Applicative.switch ( Options.Applicative.long "check" - <> Options.Applicative.help "Only check if the input is formatted" + <> Options.Applicative.help ("Only check if the input is " <> processed) ) parseDirectoryTreeOutput = @@ -761,7 +761,7 @@ let name = case input of InputFile file -> file - StandardInput -> "(stdin)" + StandardInput -> "(input)" (Header header, expression) <- do Dhall.Core.throws (first Parser.censor (Parser.exprAndHeaderFromText name originalText)) diff --git a/src/Dhall/Normalize.hs b/src/Dhall/Normalize.hs --- a/src/Dhall/Normalize.hs +++ b/src/Dhall/Normalize.hs @@ -44,6 +44,7 @@ import qualified Dhall.Map import qualified Dhall.Set import qualified Dhall.Syntax as Syntax +import qualified Lens.Family as Lens {-| Returns `True` if two expressions are α-equivalent and β-equivalent and `False` otherwise @@ -117,7 +118,6 @@ name in order to avoid shifting the bound variables by mistake. -} shift :: Int -> Var -> Expr s a -> Expr s a -shift _ _ (Const a) = Const 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' @@ -133,10 +133,6 @@ _B' = shift d (V x n') _B where n' = if x == x' then n + 1 else n -shift d v (App f a) = App f' a' - where - f' = shift d v f - a' = shift d v a shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) = Let (Binding src0 f src1 mt' src2 r') e' where @@ -146,154 +142,7 @@ mt' = fmap (fmap (shift d (V x n))) mt r' = shift d (V x n) r -shift d v (Annot a b) = Annot a' b' - where - a' = shift d v a - b' = shift d v b -shift _ _ Bool = Bool -shift _ _ (BoolLit a) = BoolLit a -shift d v (BoolAnd a b) = BoolAnd a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (BoolOr a b) = BoolOr a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (BoolEQ a b) = BoolEQ a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (BoolNE a b) = BoolNE a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (BoolIf a b c) = BoolIf a' b' c' - where - a' = shift d v a - b' = shift d v b - c' = shift d v c -shift _ _ Natural = Natural -shift _ _ (NaturalLit a) = NaturalLit a -shift _ _ NaturalFold = NaturalFold -shift _ _ NaturalBuild = NaturalBuild -shift _ _ NaturalIsZero = NaturalIsZero -shift _ _ NaturalEven = NaturalEven -shift _ _ NaturalOdd = NaturalOdd -shift _ _ NaturalToInteger = NaturalToInteger -shift _ _ NaturalShow = NaturalShow -shift _ _ NaturalSubtract = NaturalSubtract -shift d v (NaturalPlus a b) = NaturalPlus a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (NaturalTimes a b) = NaturalTimes a' b' - where - a' = shift d v a - b' = shift d v b -shift _ _ Integer = Integer -shift _ _ (IntegerLit a) = IntegerLit a -shift _ _ IntegerClamp = IntegerClamp -shift _ _ IntegerNegate = IntegerNegate -shift _ _ IntegerShow = IntegerShow -shift _ _ IntegerToDouble = IntegerToDouble -shift _ _ Double = Double -shift _ _ (DoubleLit a) = DoubleLit a -shift _ _ DoubleShow = DoubleShow -shift _ _ Text = Text -shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b) - where - a' = fmap (fmap (shift d v)) a -shift d v (TextAppend a b) = TextAppend a' b' - where - a' = shift d v a - b' = shift d v b -shift _ _ TextShow = TextShow -shift _ _ List = List -shift d v (ListLit a b) = ListLit a' b' - where - a' = fmap (shift d v) a - b' = fmap (shift d v) b -shift _ _ ListBuild = ListBuild -shift d v (ListAppend a b) = ListAppend a' b' - where - a' = shift d v a - b' = shift d v b -shift _ _ ListFold = ListFold -shift _ _ ListLength = ListLength -shift _ _ ListHead = ListHead -shift _ _ ListLast = ListLast -shift _ _ ListIndexed = ListIndexed -shift _ _ ListReverse = ListReverse -shift _ _ Optional = Optional -shift d v (Some a) = Some a' - where - a' = shift d v a -shift _ _ None = None -shift _ _ OptionalFold = OptionalFold -shift _ _ OptionalBuild = OptionalBuild -shift d v (Record a) = Record a' - where - a' = fmap (shift d v) a -shift d v (RecordLit a) = RecordLit a' - where - a' = fmap (shift d v) a -shift d v (Union a) = Union a' - where - a' = fmap (fmap (shift d v)) a -shift d v (Combine a b c) = Combine a b' c' - where - b' = shift d v b - c' = shift d v c -shift d v (CombineTypes a b) = CombineTypes a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (Prefer a b c) = Prefer a b' c' - where - b' = shift d v b - c' = shift d v c -shift d v (RecordCompletion a b) = RecordCompletion a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (Merge a b c) = Merge a' b' c' - where - a' = shift d v a - b' = shift d v b - c' = fmap (shift d v) c -shift d v (ToMap a b) = ToMap a' b' - where - a' = shift d v a - b' = fmap (shift d v) b -shift d v (Field a b) = Field a' b - where - a' = shift d v a -shift d v (Assert a) = Assert a' - where - a' = shift d v a -shift d v (Equivalent a b) = Equivalent a' b' - where - a' = shift d v a - b' = shift d v b -shift d v (Project a b) = Project a' b' - where - a' = shift d v a - b' = fmap (shift d v) b -shift d v (With a b c) = With a' b c' - where - a' = shift d v a - c' = shift d v c -shift d v (Note a b) = Note a b' - where - b' = shift d v b -shift d v (ImportAlt a b) = ImportAlt a' b' - where - a' = shift d v a - b' = shift d v b --- The Dhall compiler enforces that all embedded values are closed expressions --- and `shift` does nothing to a closed expression -shift _ _ (Embed p) = Embed p +shift d v expression = Lens.over Syntax.subExpressions (shift d v) expression {-| Substitute all occurrences of a variable with an expression @@ -311,10 +160,6 @@ _A' = subst (V x n ) e _A _B' = subst (V x n') (shift 1 (V y 0) e) _B n' = if x == y then n + 1 else n -subst v e (App f a) = App f' a' - where - f' = subst v e f - a' = subst v e a 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' @@ -325,154 +170,7 @@ mt' = fmap (fmap (subst (V x n) e)) mt r' = subst (V x n) e r -subst x e (Annot a b) = Annot a' b' - where - a' = subst x e a - b' = subst x e b -subst _ _ Bool = Bool -subst _ _ (BoolLit a) = BoolLit a -subst x e (BoolAnd a b) = BoolAnd a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (BoolOr a b) = BoolOr a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (BoolEQ a b) = BoolEQ a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (BoolNE a b) = BoolNE a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (BoolIf a b c) = BoolIf a' b' c' - where - a' = subst x e a - b' = subst x e b - c' = subst x e c -subst _ _ Natural = Natural -subst _ _ (NaturalLit a) = NaturalLit a -subst _ _ NaturalFold = NaturalFold -subst _ _ NaturalBuild = NaturalBuild -subst _ _ NaturalIsZero = NaturalIsZero -subst _ _ NaturalEven = NaturalEven -subst _ _ NaturalOdd = NaturalOdd -subst _ _ NaturalToInteger = NaturalToInteger -subst _ _ NaturalShow = NaturalShow -subst _ _ NaturalSubtract = NaturalSubtract -subst x e (NaturalPlus a b) = NaturalPlus a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (NaturalTimes a b) = NaturalTimes a' b' - where - a' = subst x e a - b' = subst x e b -subst _ _ Integer = Integer -subst _ _ (IntegerLit a) = IntegerLit a -subst _ _ IntegerClamp = IntegerClamp -subst _ _ IntegerNegate = IntegerNegate -subst _ _ IntegerShow = IntegerShow -subst _ _ IntegerToDouble = IntegerToDouble -subst _ _ Double = Double -subst _ _ (DoubleLit a) = DoubleLit a -subst _ _ DoubleShow = DoubleShow -subst _ _ Text = Text -subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b) - where - a' = fmap (fmap (subst x e)) a -subst x e (TextAppend a b) = TextAppend a' b' - where - a' = subst x e a - b' = subst x e b -subst _ _ TextShow = TextShow -subst _ _ List = List -subst x e (ListLit a b) = ListLit a' b' - where - a' = fmap (subst x e) a - b' = fmap (subst x e) b -subst x e (ListAppend a b) = ListAppend a' b' - where - a' = subst x e a - b' = subst x e b -subst _ _ ListBuild = ListBuild -subst _ _ ListFold = ListFold -subst _ _ ListLength = ListLength -subst _ _ ListHead = ListHead -subst _ _ ListLast = ListLast -subst _ _ ListIndexed = ListIndexed -subst _ _ ListReverse = ListReverse -subst _ _ Optional = Optional -subst x e (Some a) = Some a' - where - a' = subst x e a -subst _ _ None = None -subst _ _ OptionalFold = OptionalFold -subst _ _ OptionalBuild = OptionalBuild -subst x e (Record kts) = Record kts' - where - kts' = fmap (subst x e) kts -subst x e (RecordLit kvs) = RecordLit kvs' - where - kvs' = fmap (subst x e) kvs -subst x e (Union kts) = Union kts' - where - kts' = fmap (fmap (subst x e)) kts -subst x e (Combine a b c) = Combine a b' c' - where - b' = subst x e b - c' = subst x e c -subst x e (CombineTypes a b) = CombineTypes a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (Prefer a b c) = Prefer a b' c' - where - b' = subst x e b - c' = subst x e c -subst x e (RecordCompletion a b) = RecordCompletion a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (Merge a b c) = Merge a' b' c' - where - a' = subst x e a - b' = subst x e b - c' = fmap (subst x e) c -subst x e (ToMap a b) = ToMap a' b' - where - a' = subst x e a - b' = fmap (subst x e) b -subst x e (Field a b) = Field a' b - where - a' = subst x e a -subst x e (Project a b) = Project a' b' - where - a' = subst x e a - b' = fmap (subst x e) b -subst x e (Assert a) = Assert a' - where - a' = subst x e a -subst x e (Equivalent a b) = Equivalent a' b' - where - a' = subst x e a - b' = subst x e b -subst x e (With a b c) = With a' b c' - where - a' = subst x e a - c' = subst x e c -subst x e (Note a b) = Note a b' - where - b' = subst x e b -subst x e (ImportAlt a b) = ImportAlt a' b' - where - a' = subst x e a - b' = subst x e b --- The Dhall compiler enforces that all embedded values are closed expressions --- and `subst` does nothing to a closed expression -subst _ _ (Embed p) = Embed p +subst x e expression = Lens.over Syntax.subExpressions (subst x e) expression {-| This function is used to determine whether folds like @Natural/fold@ or @List/fold@ should be lazy or strict in their accumulator based on the type @@ -584,24 +282,14 @@ loop b₂ _ -> do case App f' a' of - App NaturalFold (NaturalLit n) -> do - let natural = Var (V "natural" 0) - let go 0 x = x - go n' x = go (n'-1) (App (Var (V "succ" 0)) x) - let n' = go n (Var (V "zero" 0)) - pure - (Lam "natural" - (Const Type) - (Lam "succ" - (Pi "_" natural natural) - (Lam "zero" - natural - n'))) - App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do t' <- loop t if boundedType t' then strict else lazy where + -- Use an `Integer` for the loop, due to the following + -- issue: + -- + -- https://github.com/ghcjs/ghcjs/issues/782 strict = strictLoop (fromIntegral n0 :: Integer) lazy = loop ( lazyLoop (fromIntegral n0 :: Integer)) @@ -622,8 +310,14 @@ App NaturalShow (NaturalLit n) -> pure (TextLit (Chunks [] (Data.Text.pack (show n)))) App (App NaturalSubtract (NaturalLit x)) (NaturalLit y) - | y >= x -> pure (NaturalLit (subtract x y)) - | otherwise -> pure (NaturalLit 0) + -- Use an `Integer` for the subtraction, due to the + -- following issue: + -- + -- https://github.com/ghcjs/ghcjs/issues/782 + | y >= x -> + pure (NaturalLit (fromIntegral (subtract (fromIntegral x :: Integer) (fromIntegral y :: Integer)))) + | otherwise -> + pure (NaturalLit 0) App (App NaturalSubtract (NaturalLit 0)) y -> pure y App (App NaturalSubtract _) (NaturalLit 0) -> pure (NaturalLit 0) App (App NaturalSubtract x) y | Eval.judgmentallyEqual x y -> pure (NaturalLit 0) @@ -663,20 +357,6 @@ ) nil = ListLit (Just (App List _A₀)) empty - App (App ListFold t) (ListLit _ xs) -> do - t' <- loop t - let list = Var (V "list" 0) - let lam term = - Lam "list" (Const Type) - (Lam "cons" (Pi "_" t' (Pi "_" list list)) - (Lam "nil" list term)) - term <- foldrM - (\x acc -> do - x' <- loop x - pure (App (App (Var (V "cons" 0)) x') acc)) - (Var (V "nil" 0)) - xs - pure (lam term) App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do t' <- loop t if boundedType t' then strict else lazy @@ -1075,7 +755,6 @@ App f a -> loop f && loop a && case App f a of App (Lam _ _ _) _ -> False App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False - App NaturalFold (NaturalLit _) -> False App NaturalBuild _ -> False App NaturalIsZero (NaturalLit _) -> False App NaturalEven (NaturalLit _) -> False @@ -1093,7 +772,7 @@ App DoubleShow (DoubleLit _) -> False App (App OptionalBuild _) _ -> False App (App ListBuild _) _ -> False - App (App ListFold _) (ListLit _ _) -> False + App (App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _) _ -> False App (App ListLength _) (ListLit _ _) -> False App (App ListHead _) (ListLit _ _) -> False App (App ListLast _) (ListLit _ _) -> False diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -46,6 +46,7 @@ -- over any parseable type, allowing the language to be extended as needed. exprA :: Parser a -> Parser (Expr Src a) exprA = completeExpression +{-# DEPRECATED exprA "Support for parsing custom imports will be dropped in a future release" #-} -- | A parsing error data ParseError = ParseError { 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 @@ -233,8 +233,13 @@ return (Assert a) alternative5 = do - a <- operatorExpression + a0 <- applicationExpression + let (parseFirstOperatorExpression, parseOperatorExpression) = + operatorExpression (pure a0) + + a <- parseFirstOperatorExpression + let alternative4A = do _arrow whitespace @@ -255,14 +260,63 @@ return (ToMap c (Just b)) _ -> return (Annot a b) - alternative4A <|> alternative4B <|> pure a + let alternative4C = do + case shallowDenote a of + Equivalent{} -> empty + ImportAlt{} -> empty + BoolOr{} -> empty + NaturalPlus{} -> empty + TextAppend{} -> empty + ListAppend{} -> empty + BoolAnd{} -> empty + Combine{} -> empty + Prefer{} -> empty + CombineTypes{} -> empty + NaturalTimes{} -> empty + BoolEQ{} -> empty + BoolNE{} -> empty + App{} -> empty + _ -> return () - operatorExpression = - foldr makeOperatorExpression withExpression operatorParsers + bs <- many (do + try (whitespace *> _with *> nonemptyWhitespace) - makeOperatorExpression operatorParser subExpression = + keys <- Combinators.NonEmpty.sepBy1 anyLabel (try (whitespace *> _dot) *> whitespace) + + whitespace + + _equal + + whitespace + + value <- parseOperatorExpression + + return (\e -> With e keys value) ) + + return (foldl (\e f -> f e) a0 bs) + + alternative4A <|> alternative4B <|> alternative4C <|> pure a + + -- The firstApplicationExpression argument is necessary in order to + -- left-factor the parsers for function types and @with@ expressions to + -- minimize backtracking + -- + -- For a longer explanation, see: + -- + -- https://github.com/dhall-lang/dhall-haskell/pull/1770#discussion_r419022486 + operatorExpression firstApplicationExpression = + foldr cons nil operatorParsers + where + cons operatorParser (p0, p) = + ( makeOperatorExpression p0 operatorParser p + , makeOperatorExpression p operatorParser p + ) + + nil = (firstApplicationExpression, applicationExpression) + + makeOperatorExpression firstSubExpression operatorParser subExpression = noted (do - a <- subExpression + a <- firstSubExpression whitespace @@ -278,7 +332,8 @@ operatorParsers :: [Parser (Expr s a -> Expr s a -> Expr s a)] operatorParsers = - [ ImportAlt <$ _importAlt <* nonemptyWhitespace + [ Equivalent <$ _equivalent <* whitespace + , ImportAlt <$ _importAlt <* nonemptyWhitespace , BoolOr <$ _or <* whitespace , NaturalPlus <$ _plus <* nonemptyWhitespace , TextAppend <$ _textAppend <* whitespace @@ -288,30 +343,10 @@ , Prefer PreferFromSource <$ _prefer <* whitespace , CombineTypes <$ _combineTypes <* whitespace , NaturalTimes <$ _times <* whitespace - , BoolEQ <$ _doubleEqual <* whitespace + -- Make sure that `==` is not actually the prefix of `===` + , BoolEQ <$ try (_doubleEqual <* Text.Megaparsec.notFollowedBy (char '=')) <* whitespace , BoolNE <$ _notEqual <* whitespace - , Equivalent <$ _equivalent <* whitespace ] - - withExpression = noted (do - a <- applicationExpression - - bs <- many (do - try (nonemptyWhitespace *> _with *> nonemptyWhitespace) - - keys <- Combinators.NonEmpty.sepBy1 anyLabel (try (whitespace *> _dot) *> whitespace) - - whitespace - - _equal - - whitespace - - value <- applicationExpression - - return (\e -> With e keys value) ) - - return (foldl (\e f -> f e) a bs) ) applicationExpression = do let alternative0 = do 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 @@ -307,21 +307,34 @@ combineLong x y = x <> y <> Pretty.hardline +unsnoc :: [a] -> Maybe ([a], a) +unsnoc [] = Nothing +unsnoc (x0 : xs0) = Just (go id x0 xs0) + where + go diffXs x [] = (diffXs [], x) + go diffXs x (y : ys) = go (diffXs . (x:)) y ys + -- | Pretty-print anonymous functions and function types -arrows :: CharacterSet -> [(Doc Ann, Doc Ann)] -> Doc Ann -arrows ASCII = - enclose' - "" - " " - (" " <> rarrow ASCII <> " ") - (rarrow ASCII <> " ") -arrows Unicode = - enclose' - "" - " " - (" " <> rarrow Unicode <> " ") - (rarrow Unicode <> " ") +arrows :: CharacterSet -> [ Doc Ann ] -> Doc Ann +arrows characterSet docs = Pretty.group (Pretty.flatAlt long short) + where + long = Pretty.align (mconcat (Data.List.intersperse Pretty.hardline docs')) + where + docs' = case unsnoc docs of + Nothing -> docs + Just (init_, last_) -> init' ++ [ last' ] + where + appendArrow doc = doc <> space <> rarrow characterSet + + init' = map appendArrow init_ + + last' = space <> space <> last_ + + short = mconcat (Data.List.intersperse separator docs) + where + separator = space <> rarrow characterSet <> space + combine :: CharacterSet -> Text combine ASCII = "/\\" combine Unicode = "∧" @@ -521,7 +534,7 @@ Pretty.group (prettyExpression expression) where prettyExpression a0@(Lam _ _ _) = - arrows characterSet (fmap duplicate (docs a0)) + arrows characterSet (docs a0) where docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c where @@ -552,10 +565,10 @@ Pretty.group (Pretty.flatAlt long short) where prefixesLong = - " " + "" : cycle - [ Pretty.hardline <> keyword "then" <> " " - , Pretty.hardline <> keyword "else" <> " " + [ keyword "then" <> " " + , keyword "else" <> " " ] prefixesShort = @@ -565,25 +578,29 @@ , space <> keyword "else" <> space ] - longLines = zipWith (<>) prefixesLong (docsLong a0) + longLines = zipWith (<>) prefixesLong (docsLong True a0) long = Pretty.align (mconcat (Data.List.intersperse Pretty.hardline longLines)) short = mconcat (zipWith (<>) prefixesShort (docsShort a0)) - docsLong (BoolIf a b c) = - docLong ++ docsLong c + docsLong initial (BoolIf a b c) = + docLong ++ docsLong False c where + padding + | initial = " " + | otherwise = mempty + docLong = - [ keyword "if" <> " " <> prettyExpression a + [ keyword "if" <> padding <> " " <> prettyExpression a , prettyExpression b ] - docsLong c + docsLong initial c | Just doc <- preserveSource c = [ doc ] | Note _ d <- c = - docsLong d + docsLong initial d | otherwise = [ prettyExpression c ] @@ -647,7 +664,7 @@ , keyword "in" <> " " <> prettyExpression b ) prettyExpression a0@(Pi _ _ _) = - arrows characterSet (fmap duplicate (docs a0)) + arrows characterSet (docs a0) where docs (Pi "_" b c) = prettyOperatorExpression b : docs c docs (Pi a b c) = Pretty.group (Pretty.flatAlt long short) : docs c @@ -675,6 +692,18 @@ docs d | otherwise = [ prettyExpression c ] + prettyExpression (With a b c) = + prettyExpression a + <> Pretty.flatAlt long short + where + short = " " <> keyword "with" <> " " <> update + + long = Pretty.hardline + <> " " + <> Pretty.align (keyword "with" <> " " <> update) + + (update, _) = + prettyKeyValue prettyAnyLabels prettyOperatorExpression equals (b, c) prettyExpression (Assert a) = Pretty.group (Pretty.flatAlt long short) where @@ -761,7 +790,7 @@ prettyOperatorExpression a prettyOperatorExpression :: Pretty a => Expr Src a -> Doc Ann - prettyOperatorExpression = prettyImportAltExpression + prettyOperatorExpression = prettyEquivalentExpression prettyOperator :: Text -> [Doc Ann] -> Doc Ann prettyOperator op docs = @@ -776,6 +805,26 @@ spacer = if Text.length op == 1 then " " else " " + prettyEquivalentExpression :: Pretty a => Expr Src a -> Doc Ann + prettyEquivalentExpression a0@(Equivalent _ _) = + prettyOperator (equivalent characterSet) (docs a0) + where + docs (Equivalent a b) = prettyImportAltExpression b : docs a + docs a + | Just doc <- preserveSource a = + [ doc ] + | Note _ b <- a = + docs b + | otherwise = + [ prettyImportAltExpression a ] + prettyEquivalentExpression a + | Just doc <- preserveSource a = + doc + | Note _ b <- a = + prettyEquivalentExpression b + | otherwise = + prettyImportAltExpression a + prettyImportAltExpression :: Pretty a => Expr Src a -> Doc Ann prettyImportAltExpression a0@(ImportAlt _ _) = prettyOperator "?" (docs a0) @@ -1000,60 +1049,20 @@ prettyNotEqualExpression a0@(BoolNE _ _) = prettyOperator "!=" (docs a0) where - docs (BoolNE a b) = prettyEquivalentExpression b : docs a + docs (BoolNE a b) = prettyApplicationExpression b : docs a docs a | Just doc <- preserveSource a = [ doc ] | Note _ b <- a = docs b | otherwise = - [ prettyEquivalentExpression a ] + [ prettyApplicationExpression a ] prettyNotEqualExpression a | Just doc <- preserveSource a = doc | Note _ b <- a = prettyNotEqualExpression b | otherwise = - prettyEquivalentExpression a - - prettyEquivalentExpression :: Pretty a => Expr Src a -> Doc Ann - prettyEquivalentExpression a0@(Equivalent _ _) = - prettyOperator (equivalent characterSet) (docs a0) - where - docs (Equivalent a b) = prettyApplicationExpression b : docs a - docs a - | Just doc <- preserveSource a = - [ doc ] - | Note _ b <- a = - docs b - | otherwise = - [ prettyApplicationExpression a ] - prettyEquivalentExpression a - | Just doc <- preserveSource a = - doc - | Note _ b <- a = - prettyEquivalentExpression b - | otherwise = - prettyWithExpression a - - prettyWithExpression :: Pretty a => Expr Src a -> Doc Ann - prettyWithExpression (With a b c) = - prettyWithExpression a - <> Pretty.flatAlt long short - where - short = " " <> keyword "with" <> " " <> update - - long = Pretty.hardline - <> " " - <> Pretty.align (keyword "with" <> " " <> update) - - (update, _ ) = prettyKeyValue prettyAnyLabels equals (b, c) - prettyWithExpression a - | Just doc <- preserveSource a = - doc - | Note _ b <- a = - prettyWithExpression b - | otherwise = prettyApplicationExpression a prettyApplicationExpression :: Pretty a => Expr Src a -> Doc Ann @@ -1235,10 +1244,11 @@ prettyKeyValue :: Pretty a => (k -> Doc Ann) + -> (Expr Src a -> Doc Ann) -> Doc Ann -> (k, Expr Src a) -> (Doc Ann, Doc Ann) - prettyKeyValue prettyKey separator (key, val) = + prettyKeyValue prettyKey prettyValue separator (key, val) = duplicate (Pretty.group (Pretty.flatAlt long short)) where completion _T r = @@ -1255,7 +1265,7 @@ <> " " <> separator <> " " - <> prettyExpression val + <> prettyValue val long = prettyKey key @@ -1277,7 +1287,7 @@ | not (null xs) -> Pretty.hardline <> " " - <> prettyExpression val' + <> prettyImportExpression val' _ -> Pretty.hardline <> " " @@ -1298,29 +1308,36 @@ RecordLit _ -> Pretty.hardline <> " " - <> prettyExpression val + <> prettyValue val ListLit _ xs | not (null xs) -> Pretty.hardline <> " " - <> prettyExpression val + <> prettyValue val _ -> Pretty.hardline <> " " - <> prettyExpression val + <> prettyValue val prettyRecord :: Pretty a => Map Text (Expr Src a) -> Doc Ann prettyRecord = - braces . map (prettyKeyValue prettyAnyLabel colon) . Map.toList + braces + . map (prettyKeyValue prettyAnyLabel prettyExpression colon) + . Map.toList prettyRecordLit :: Pretty a => Map Text (Expr Src a) -> Doc Ann - prettyRecordLit a + prettyRecordLit = prettyRecordLike braces + + prettyCompletionLit :: Pretty a => Int -> Map Text (Expr Src a) -> Doc Ann + prettyCompletionLit = prettyRecordLike . hangingBraces + + prettyRecordLike braceStyle a | Data.Foldable.null a = lbrace <> equals <> rbrace | otherwise = - braces (map prettyRecordEntry (Map.toList consolidated)) + braceStyle (map prettyRecordEntry (Map.toList consolidated)) where consolidated = consolidateRecordLiteral a @@ -1331,22 +1348,12 @@ , key == key' -> duplicate (prettyAnyLabel key) _ -> - prettyKeyValue prettyAnyLabels equals (keys, value) - - prettyCompletionLit - :: Pretty a => Int -> Map Text (Expr Src a) -> Doc Ann - prettyCompletionLit n a - | Data.Foldable.null a = - lbrace <> equals <> rbrace - | otherwise = - hangingBraces n (map prettyRecordEntry (Map.toList consolidated)) - where - consolidated = consolidateRecordLiteral a - - prettyRecordEntry = prettyKeyValue prettyAnyLabels equals + prettyKeyValue prettyAnyLabels prettyExpression equals (keys, value) - prettyAlternative (key, Just val) = prettyKeyValue prettyAnyLabel colon (key, val) - prettyAlternative (key, Nothing ) = duplicate (prettyAnyLabel key) + prettyAlternative (key, Just val) = + prettyKeyValue prettyAnyLabel prettyExpression colon (key, val) + prettyAlternative (key, Nothing) = + duplicate (prettyAnyLabel key) prettyUnion :: Pretty a => Map Text (Maybe (Expr Src a)) -> Doc Ann prettyUnion = diff --git a/src/Dhall/Repl.hs b/src/Dhall/Repl.hs --- a/src/Dhall/Repl.hs +++ b/src/Dhall/Repl.hs @@ -130,7 +130,7 @@ :: MonadIO m => String -> m ( Dhall.Expr Dhall.Src Void) parseAndLoad src = do parsed <- - case Dhall.exprFromText "(stdin)" (Text.pack src <> "\n") of + case Dhall.exprFromText "(input)" (Text.pack src <> "\n") of Left e -> liftIO ( throwIO e ) @@ -222,7 +222,7 @@ addBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => [String] -> m () addBinding (k : "=" : srcs) = do - varName <- case Megaparsec.parse (unParser Parser.Token.label) "(stdin)" (Text.pack k) of + varName <- case Megaparsec.parse (unParser Parser.Token.label) "(input)" (Text.pack k) of Left _ -> Fail.fail "Invalid variable name" Right varName -> return varName diff --git a/src/Dhall/Set.hs b/src/Dhall/Set.hs --- a/src/Dhall/Set.hs +++ b/src/Dhall/Set.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveLift #-} -- | This module only exports ways of constructing a Set, -- retrieving List, Set, and Seq representations of the same data, @@ -36,14 +37,13 @@ import qualified Data.Set import qualified Data.Sequence import qualified Data.Foldable -import qualified Language.Haskell.TH.Syntax as Syntax {-| This is a variation on @"Data.Set".`Data.Set.Set`@ that remembers the original order of elements. This ensures that ordering is not lost when formatting Dhall code -} data Set a = Set (Data.Set.Set a) (Seq a) - deriving (Generic, Show, Data, NFData) + deriving (Generic, Show, Data, NFData, Lift) -- Invariant: In @Set set seq@, @toAscList set == sort (toList seq)@. instance Eq a => Eq (Set a) where @@ -53,9 +53,6 @@ instance Ord a => Ord (Set a) where compare (Set _ x) (Set _ y) = compare x y {-# INLINABLE compare #-} - -instance (Data a, Lift a, Ord a) => Lift (Set a) where - lift = Syntax.liftData instance Foldable Set where foldMap f (Set _ x) = foldMap f x diff --git a/src/Dhall/Src.hs b/src/Dhall/Src.hs --- a/src/Dhall/Src.hs +++ b/src/Dhall/Src.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} @@ -18,7 +19,7 @@ import Data.Text.Prettyprint.Doc (Pretty (..)) import GHC.Generics (Generic) import Instances.TH.Lift () -import Language.Haskell.TH.Syntax (Lift, lift) +import Language.Haskell.TH.Syntax (Lift(..)) import Text.Megaparsec (SourcePos (SourcePos), mkPos, unPos) import {-# SOURCE #-} qualified Dhall.Util @@ -36,8 +37,13 @@ instance Lift Src where +#if MIN_VERSION_template_haskell(2,16,0) + liftTyped (Src (SourcePos a b c) (SourcePos d e f) g) = + [|| Src (SourcePos a (mkPos b') (mkPos c')) (SourcePos d (mkPos e') (mkPos f')) g ||] +#else lift (Src (SourcePos a b c) (SourcePos d e f) g) = [| Src (SourcePos a (mkPos b') (mkPos c')) (SourcePos d (mkPos e') (mkPos f')) g |] +#endif where b' = unPos b c' = unPos c diff --git a/src/Dhall/Syntax.hs b/src/Dhall/Syntax.hs --- a/src/Dhall/Syntax.hs +++ b/src/Dhall/Syntax.hs @@ -37,6 +37,7 @@ -- ** Optics , subExpressions + , unsafeSubExpressions , chunkExprs , bindingExprs @@ -68,6 +69,9 @@ -- * Desugaring , desugarWith + + -- * Utilities + , internalError ) where import Control.DeepSeq (NFData) @@ -102,6 +106,7 @@ import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Dhall.Crypto import qualified Dhall.Optics as Optics +import qualified Lens.Family as Lens import qualified Network.URI as URI {-| Constants for a pure type system @@ -493,77 +498,10 @@ -- implementation with this pragma below to allow GHC to, possibly, -- inline the implementation for performance improvements. instance Functor (Expr s) where - fmap _ (Const c) = Const c - fmap _ (Var v) = Var v - fmap f (Lam v e1 e2) = Lam v (fmap f e1) (fmap f e2) - fmap f (Pi v e1 e2) = Pi v (fmap f e1) (fmap f e2) - fmap f (App e1 e2) = App (fmap f e1) (fmap f e2) + fmap f (Embed a) = Embed (f a) fmap f (Let b e2) = Let (fmap f b) (fmap f e2) - fmap f (Annot e1 e2) = Annot (fmap f e1) (fmap f e2) - fmap _ Bool = Bool - fmap _ (BoolLit b) = BoolLit b - fmap f (BoolAnd e1 e2) = BoolAnd (fmap f e1) (fmap f e2) - fmap f (BoolOr e1 e2) = BoolOr (fmap f e1) (fmap f e2) - fmap f (BoolEQ e1 e2) = BoolEQ (fmap f e1) (fmap f e2) - fmap f (BoolNE e1 e2) = BoolNE (fmap f e1) (fmap f e2) - fmap f (BoolIf e1 e2 e3) = BoolIf (fmap f e1) (fmap f e2) (fmap f e3) - fmap _ Natural = Natural - fmap _ (NaturalLit n) = NaturalLit n - fmap _ NaturalFold = NaturalFold - fmap _ NaturalBuild = NaturalBuild - fmap _ NaturalIsZero = NaturalIsZero - fmap _ NaturalEven = NaturalEven - fmap _ NaturalOdd = NaturalOdd - fmap _ NaturalToInteger = NaturalToInteger - fmap _ NaturalShow = NaturalShow - fmap _ NaturalSubtract = NaturalSubtract - fmap f (NaturalPlus e1 e2) = NaturalPlus (fmap f e1) (fmap f e2) - fmap f (NaturalTimes e1 e2) = NaturalTimes (fmap f e1) (fmap f e2) - fmap _ Integer = Integer - fmap _ (IntegerLit i) = IntegerLit i - fmap _ IntegerClamp = IntegerClamp - fmap _ IntegerNegate = IntegerNegate - fmap _ IntegerShow = IntegerShow - fmap _ IntegerToDouble = IntegerToDouble - fmap _ Double = Double - fmap _ (DoubleLit d) = DoubleLit d - fmap _ DoubleShow = DoubleShow - fmap _ Text = Text - fmap f (TextLit cs) = TextLit (fmap f cs) - fmap f (TextAppend e1 e2) = TextAppend (fmap f e1) (fmap f e2) - fmap _ TextShow = TextShow - fmap _ List = List - fmap f (ListLit maybeE seqE) = ListLit (fmap (fmap f) maybeE) (fmap (fmap f) seqE) - fmap f (ListAppend e1 e2) = ListAppend (fmap f e1) (fmap f e2) - fmap _ ListBuild = ListBuild - fmap _ ListFold = ListFold - fmap _ ListLength = ListLength - fmap _ ListHead = ListHead - fmap _ ListLast = ListLast - fmap _ ListIndexed = ListIndexed - fmap _ ListReverse = ListReverse - fmap _ Optional = Optional - fmap f (Some e) = Some (fmap f e) - fmap _ None = None - fmap _ OptionalFold = OptionalFold - fmap _ OptionalBuild = OptionalBuild - fmap f (Record r) = Record (fmap (fmap f) r) - fmap f (RecordLit r) = RecordLit (fmap (fmap f) r) - fmap f (Union u) = Union (fmap (fmap (fmap f)) u) - fmap f (Combine m e1 e2) = Combine m (fmap f e1) (fmap f e2) - fmap f (CombineTypes e1 e2) = CombineTypes (fmap f e1) (fmap f e2) - fmap f (Prefer a e1 e2) = Prefer (fmap f a) (fmap f e1) (fmap f e2) - fmap f (RecordCompletion e1 e2) = RecordCompletion (fmap f e1) (fmap f e2) - fmap f (Merge e1 e2 maybeE) = Merge (fmap f e1) (fmap f e2) (fmap (fmap f) maybeE) - fmap f (ToMap e maybeE) = ToMap (fmap f e) (fmap (fmap f) maybeE) - fmap f (Field e1 v) = Field (fmap f e1) v - fmap f (Project e1 vs) = Project (fmap f e1) (fmap (fmap f) vs) - fmap f (Assert t) = Assert (fmap f t) - fmap f (Equivalent e1 e2) = Equivalent (fmap f e1) (fmap f e2) - fmap f (With e k v) = With (fmap f e) k (fmap f v) fmap f (Note s e1) = Note s (fmap f e1) - fmap f (ImportAlt e1 e2) = ImportAlt (fmap f e1) (fmap f e2) - fmap f (Embed a) = Embed (f a) + fmap f expression = Lens.over unsafeSubExpressions (fmap f) expression {-# INLINABLE fmap #-} instance Applicative (Expr s) where @@ -574,160 +512,21 @@ instance Monad (Expr s) where return = pure - Const a >>= _ = Const a - Var a >>= _ = Var a - Lam a b c >>= k = Lam a (b >>= k) (c >>= k) - Pi a b c >>= k = Pi a (b >>= k) (c >>= k) - App a b >>= k = App (a >>= k) (b >>= k) - Let a b >>= k = Let (adapt0 a) (b >>= k) + Embed a >>= k = k a + Let a b >>= k = Let (adapt0 a) (b >>= k) where adapt0 (Binding src0 c src1 d src2 e) = Binding src0 c src1 (fmap adapt1 d) src2 (e >>= k) adapt1 (src3, f) = (src3, f >>= k) - Annot a b >>= k = Annot (a >>= k) (b >>= k) - Bool >>= _ = Bool - BoolLit a >>= _ = BoolLit a - BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k) - BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k) - BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k) - BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k) - BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k) - Natural >>= _ = Natural - NaturalLit a >>= _ = NaturalLit a - NaturalFold >>= _ = NaturalFold - NaturalBuild >>= _ = NaturalBuild - NaturalIsZero >>= _ = NaturalIsZero - NaturalEven >>= _ = NaturalEven - NaturalOdd >>= _ = NaturalOdd - NaturalToInteger >>= _ = NaturalToInteger - NaturalShow >>= _ = NaturalShow - NaturalSubtract >>= _ = NaturalSubtract - NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k) - NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k) - Integer >>= _ = Integer - IntegerLit a >>= _ = IntegerLit a - IntegerClamp >>= _ = IntegerClamp - IntegerNegate >>= _ = IntegerNegate - IntegerShow >>= _ = IntegerShow - IntegerToDouble >>= _ = IntegerToDouble - Double >>= _ = Double - DoubleLit a >>= _ = DoubleLit a - DoubleShow >>= _ = DoubleShow - Text >>= _ = Text - TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b) - TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k) - TextShow >>= _ = TextShow - List >>= _ = List - ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b) - ListAppend a b >>= k = ListAppend (a >>= k) (b >>= k) - ListBuild >>= _ = ListBuild - ListFold >>= _ = ListFold - ListLength >>= _ = ListLength - ListHead >>= _ = ListHead - ListLast >>= _ = ListLast - ListIndexed >>= _ = ListIndexed - ListReverse >>= _ = ListReverse - Optional >>= _ = Optional - Some a >>= k = Some (a >>= k) - None >>= _ = None - OptionalFold >>= _ = OptionalFold - OptionalBuild >>= _ = OptionalBuild - Record a >>= k = Record (fmap (>>= k) a) - RecordLit a >>= k = RecordLit (fmap (>>= k) a) - Union a >>= k = Union (fmap (fmap (>>= k)) a) - Combine a b c >>= k = Combine a (b >>= k) (c >>= k) - CombineTypes a b >>= k = CombineTypes (a >>= k) (b >>= k) - Prefer a b c >>= k = Prefer a' (b >>= k) (c >>= k) - where - a' = case a of - PreferFromSource -> PreferFromSource - PreferFromWith e -> PreferFromWith (e >>= k) - PreferFromCompletion -> PreferFromCompletion - RecordCompletion a b >>= k = RecordCompletion (a >>= k) (b >>= k) - Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c) - ToMap a b >>= k = ToMap (a >>= k) (fmap (>>= k) b) - Field a b >>= k = Field (a >>= k) b - Project a b >>= k = Project (a >>= k) (fmap (>>= k) b) - Assert a >>= k = Assert (a >>= k) - Equivalent a b >>= k = Equivalent (a >>= k) (b >>= k) - With a b c >>= k = With (a >>= k) b (c >>= k) - Note a b >>= k = Note a (b >>= k) - ImportAlt a b >>= k = ImportAlt (a >>= k) (b >>= k) - Embed a >>= k = k a + Note a b >>= k = Note a (b >>= k) + expression >>= k = Lens.over unsafeSubExpressions (>>= k) expression instance Bifunctor Expr where - first _ (Const a ) = Const a - first _ (Var a ) = Var a - first k (Lam a b c ) = Lam a (first k b) (first k c) - first k (Pi a b c ) = Pi a (first k b) (first k c) - first k (App a b ) = App (first k a) (first k b) - first k (Let a b ) = Let (first k a) (first k b) - first k (Annot a b ) = Annot (first k a) (first k b) - first _ Bool = Bool - first _ (BoolLit a ) = BoolLit a - first k (BoolAnd a b ) = BoolAnd (first k a) (first k b) - first k (BoolOr a b ) = BoolOr (first k a) (first k b) - first k (BoolEQ a b ) = BoolEQ (first k a) (first k b) - first k (BoolNE a b ) = BoolNE (first k a) (first k b) - first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c) - first _ Natural = Natural - first _ (NaturalLit a ) = NaturalLit a - first _ NaturalFold = NaturalFold - first _ NaturalBuild = NaturalBuild - first _ NaturalIsZero = NaturalIsZero - first _ NaturalEven = NaturalEven - first _ NaturalOdd = NaturalOdd - first _ NaturalToInteger = NaturalToInteger - first _ NaturalShow = NaturalShow - first _ NaturalSubtract = NaturalSubtract - first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b) - first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b) - first _ Integer = Integer - first _ (IntegerLit a ) = IntegerLit a - first _ IntegerClamp = IntegerClamp - first _ IntegerNegate = IntegerNegate - first _ IntegerShow = IntegerShow - first _ IntegerToDouble = IntegerToDouble - first _ Double = Double - first _ (DoubleLit a ) = DoubleLit a - first _ DoubleShow = DoubleShow - first _ Text = Text - first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b) - first k (TextAppend a b ) = TextAppend (first k a) (first k b) - first _ TextShow = TextShow - first _ List = List - first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b) - first k (ListAppend a b ) = ListAppend (first k a) (first k b) - first _ ListBuild = ListBuild - first _ ListFold = ListFold - first _ ListLength = ListLength - first _ ListHead = ListHead - first _ ListLast = ListLast - first _ ListIndexed = ListIndexed - first _ ListReverse = ListReverse - first _ Optional = Optional - first k (Some a ) = Some (first k a) - first _ None = None - first _ OptionalFold = OptionalFold - first _ OptionalBuild = OptionalBuild - first k (Record a ) = Record (fmap (first k) a) - first k (RecordLit a ) = RecordLit (fmap (first k) a) - first k (Union a ) = Union (fmap (fmap (first k)) a) - first k (Combine a b c ) = Combine a (first k b) (first k c) - first k (CombineTypes a b ) = CombineTypes (first k a) (first k b) - first k (Prefer a b c ) = Prefer (first k a) (first k b) (first k c) - first k (RecordCompletion a b) = RecordCompletion (first k a) (first k b) - first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c) - first k (ToMap a b ) = ToMap (first k a) (fmap (first k) b) - first k (Field a b ) = Field (first k a) b - first k (Assert a ) = Assert (first k a) - first k (Equivalent a b ) = Equivalent (first k a) (first k b) - first k (Project a b ) = Project (first k a) (fmap (first k) b) - first k (With a b c ) = With (first k a) b (first k c) - first k (Note a b ) = Note (k a) (first k b) - first k (ImportAlt a b ) = ImportAlt (first k a) (first k b) - first _ (Embed a ) = Embed a + first k (Note a b ) = Note (k a) (first k b) + first _ (Embed a ) = Embed a + first k (Let a b ) = Let (first k a) (first k b) + first k expression = Lens.over unsafeSubExpressions (first k) expression second = fmap @@ -789,80 +588,110 @@ data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a) -- | A traversal over the immediate sub-expressions of an expression. -subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a) -subExpressions _ (Const c) = pure (Const c) -subExpressions _ (Var v) = pure (Var v) -subExpressions f (Lam a b c) = Lam a <$> f b <*> f c -subExpressions f (Pi a b c) = Pi a <$> f b <*> f c -subExpressions f (App a b) = App <$> f a <*> f b +subExpressions + :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a) +subExpressions _ (Embed a) = pure (Embed a) +subExpressions f (Note a b) = Note a <$> f b subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b -subExpressions f (Annot a b) = Annot <$> f a <*> f b -subExpressions _ Bool = pure Bool -subExpressions _ (BoolLit b) = pure (BoolLit b) -subExpressions f (BoolAnd a b) = BoolAnd <$> f a <*> f b -subExpressions f (BoolOr a b) = BoolOr <$> f a <*> f b -subExpressions f (BoolEQ a b) = BoolEQ <$> f a <*> f b -subExpressions f (BoolNE a b) = BoolNE <$> f a <*> f b -subExpressions f (BoolIf a b c) = BoolIf <$> f a <*> f b <*> f c -subExpressions _ Natural = pure Natural -subExpressions _ (NaturalLit n) = pure (NaturalLit n) -subExpressions _ NaturalFold = pure NaturalFold -subExpressions _ NaturalBuild = pure NaturalBuild -subExpressions _ NaturalIsZero = pure NaturalIsZero -subExpressions _ NaturalEven = pure NaturalEven -subExpressions _ NaturalOdd = pure NaturalOdd -subExpressions _ NaturalToInteger = pure NaturalToInteger -subExpressions _ NaturalShow = pure NaturalShow -subExpressions _ NaturalSubtract = pure NaturalSubtract -subExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b -subExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b -subExpressions _ Integer = pure Integer -subExpressions _ (IntegerLit n) = pure (IntegerLit n) -subExpressions _ IntegerClamp = pure IntegerClamp -subExpressions _ IntegerNegate = pure IntegerNegate -subExpressions _ IntegerShow = pure IntegerShow -subExpressions _ IntegerToDouble = pure IntegerToDouble -subExpressions _ Double = pure Double -subExpressions _ (DoubleLit n) = pure (DoubleLit n) -subExpressions _ DoubleShow = pure DoubleShow -subExpressions _ Text = pure Text -subExpressions f (TextLit chunks) = +subExpressions f expression = unsafeSubExpressions f expression +{-# INLINABLE subExpressions #-} + +{-| An internal utility used to implement transformations that require changing + one of the type variables of the `Expr` type + + This utility only works because the implementation is partial, not + handling the `Let`, `Note`, or `Embed` cases, which need to be handled by + the caller. +-} +unsafeSubExpressions + :: 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 +unsafeSubExpressions _ Bool = pure Bool +unsafeSubExpressions _ (BoolLit b) = pure (BoolLit b) +unsafeSubExpressions f (BoolAnd a b) = BoolAnd <$> f a <*> f b +unsafeSubExpressions f (BoolOr a b) = BoolOr <$> f a <*> f b +unsafeSubExpressions f (BoolEQ a b) = BoolEQ <$> f a <*> f b +unsafeSubExpressions f (BoolNE a b) = BoolNE <$> f a <*> f b +unsafeSubExpressions f (BoolIf a b c) = BoolIf <$> f a <*> f b <*> f c +unsafeSubExpressions _ Natural = pure Natural +unsafeSubExpressions _ (NaturalLit n) = pure (NaturalLit n) +unsafeSubExpressions _ NaturalFold = pure NaturalFold +unsafeSubExpressions _ NaturalBuild = pure NaturalBuild +unsafeSubExpressions _ NaturalIsZero = pure NaturalIsZero +unsafeSubExpressions _ NaturalEven = pure NaturalEven +unsafeSubExpressions _ NaturalOdd = pure NaturalOdd +unsafeSubExpressions _ NaturalToInteger = pure NaturalToInteger +unsafeSubExpressions _ NaturalShow = pure NaturalShow +unsafeSubExpressions _ NaturalSubtract = pure NaturalSubtract +unsafeSubExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b +unsafeSubExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b +unsafeSubExpressions _ Integer = pure Integer +unsafeSubExpressions _ (IntegerLit n) = pure (IntegerLit n) +unsafeSubExpressions _ IntegerClamp = pure IntegerClamp +unsafeSubExpressions _ IntegerNegate = pure IntegerNegate +unsafeSubExpressions _ IntegerShow = pure IntegerShow +unsafeSubExpressions _ IntegerToDouble = pure IntegerToDouble +unsafeSubExpressions _ Double = pure Double +unsafeSubExpressions _ (DoubleLit n) = pure (DoubleLit n) +unsafeSubExpressions _ DoubleShow = pure DoubleShow +unsafeSubExpressions _ Text = pure Text +unsafeSubExpressions f (TextLit chunks) = TextLit <$> chunkExprs f chunks -subExpressions f (TextAppend a b) = TextAppend <$> f a <*> f b -subExpressions _ TextShow = pure TextShow -subExpressions _ List = pure List -subExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b -subExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b -subExpressions _ ListBuild = pure ListBuild -subExpressions _ ListFold = pure ListFold -subExpressions _ ListLength = pure ListLength -subExpressions _ ListHead = pure ListHead -subExpressions _ ListLast = pure ListLast -subExpressions _ ListIndexed = pure ListIndexed -subExpressions _ ListReverse = pure ListReverse -subExpressions _ Optional = pure Optional -subExpressions f (Some a) = Some <$> f a -subExpressions _ None = pure None -subExpressions _ OptionalFold = pure OptionalFold -subExpressions _ OptionalBuild = pure OptionalBuild -subExpressions f (Record a) = Record <$> traverse f a -subExpressions f ( RecordLit a ) = RecordLit <$> traverse f a -subExpressions f (Union a) = Union <$> traverse (traverse f) a -subExpressions f (Combine a b c) = Combine a <$> f b <*> f c -subExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b -subExpressions f (Prefer a b c) = Prefer <$> pure a <*> f b <*> f c -subExpressions f (RecordCompletion a b) = RecordCompletion <$> f a <*> f b -subExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t -subExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t -subExpressions f (Field a b) = Field <$> f a <*> pure b -subExpressions f (Project a b) = Project <$> f a <*> traverse f b -subExpressions f (Assert a) = Assert <$> f a -subExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b -subExpressions f (With a b c) = With <$> f a <*> pure b <*> f c -subExpressions f (Note a b) = Note a <$> f b -subExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r -subExpressions _ (Embed a) = pure (Embed a) +unsafeSubExpressions f (TextAppend a b) = TextAppend <$> f a <*> f b +unsafeSubExpressions _ TextShow = pure TextShow +unsafeSubExpressions _ List = pure List +unsafeSubExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b +unsafeSubExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b +unsafeSubExpressions _ ListBuild = pure ListBuild +unsafeSubExpressions _ ListFold = pure ListFold +unsafeSubExpressions _ ListLength = pure ListLength +unsafeSubExpressions _ ListHead = pure ListHead +unsafeSubExpressions _ ListLast = pure ListLast +unsafeSubExpressions _ ListIndexed = pure ListIndexed +unsafeSubExpressions _ ListReverse = pure ListReverse +unsafeSubExpressions _ Optional = pure Optional +unsafeSubExpressions f (Some a) = Some <$> f a +unsafeSubExpressions _ None = pure None +unsafeSubExpressions _ OptionalFold = pure OptionalFold +unsafeSubExpressions _ OptionalBuild = pure OptionalBuild +unsafeSubExpressions f (Record a) = Record <$> traverse f a +unsafeSubExpressions f ( RecordLit a ) = RecordLit <$> traverse f a +unsafeSubExpressions f (Union a) = Union <$> traverse (traverse f) a +unsafeSubExpressions f (Combine a b c) = Combine a <$> f b <*> f c +unsafeSubExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b +unsafeSubExpressions f (Prefer a b c) = Prefer <$> a' <*> f b <*> f c + where + a' = case a of + PreferFromSource -> pure PreferFromSource + PreferFromWith d -> PreferFromWith <$> f d + PreferFromCompletion -> pure PreferFromCompletion +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 +unsafeSubExpressions f (With a b c) = With <$> f a <*> pure b <*> f c +unsafeSubExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r +unsafeSubExpressions _ (Let {}) = unhandledConstructor "Let" +unsafeSubExpressions _ (Note {}) = unhandledConstructor "Note" +unsafeSubExpressions _ (Embed {}) = unhandledConstructor "Embed" +{-# INLINABLE unsafeSubExpressions #-} +unhandledConstructor :: Text -> a +unhandledConstructor constructor = + internalError + ( "Dhall.Syntax.unsafeSubExpressions: Unhandled " + <> constructor + <> " construtor" + ) + {-| Traverse over the immediate 'Expr' children in a 'Binding'. -} bindingExprs @@ -877,6 +706,7 @@ <*> traverse (traverse f) t <*> pure s2 <*> f v +{-# INLINABLE bindingExprs #-} -- | A traversal over the immediate sub-expressions in 'Chunks'. chunkExprs @@ -885,6 +715,7 @@ -> Chunks s a -> f (Chunks t b) chunkExprs f (Chunks chunks final) = flip Chunks final <$> traverse (traverse f) chunks +{-# INLINABLE chunkExprs #-} {-| Internal representation of a directory that stores the path components in reverse order @@ -1092,87 +923,16 @@ -- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`) denote :: Expr s a -> Expr t a -denote (Note _ b ) = denote b -denote (Const a ) = Const a -denote (Var a ) = Var a -denote (Lam a b c ) = Lam a (denote b) (denote c) -denote (Pi a b c ) = Pi a (denote b) (denote c) -denote (App a b ) = App (denote a) (denote b) -denote (Let a b ) = Let (adapt0 a) (denote b) +denote (Note _ b ) = denote b +denote (Let a b ) = Let (adapt0 a) (denote b) where adapt0 (Binding _ c _ d _ e) = Binding Nothing c Nothing (fmap adapt1 d) Nothing (denote e) adapt1 (_, f) = (Nothing, denote f) -denote (Annot a b ) = Annot (denote a) (denote b) -denote Bool = Bool -denote (BoolLit a ) = BoolLit a -denote (BoolAnd a b ) = BoolAnd (denote a) (denote b) -denote (BoolOr a b ) = BoolOr (denote a) (denote b) -denote (BoolEQ a b ) = BoolEQ (denote a) (denote b) -denote (BoolNE a b ) = BoolNE (denote a) (denote b) -denote (BoolIf a b c ) = BoolIf (denote a) (denote b) (denote c) -denote Natural = Natural -denote (NaturalLit a ) = NaturalLit a -denote NaturalFold = NaturalFold -denote NaturalBuild = NaturalBuild -denote NaturalIsZero = NaturalIsZero -denote NaturalEven = NaturalEven -denote NaturalOdd = NaturalOdd -denote NaturalToInteger = NaturalToInteger -denote NaturalShow = NaturalShow -denote NaturalSubtract = NaturalSubtract -denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b) -denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b) -denote Integer = Integer -denote (IntegerLit a ) = IntegerLit a -denote IntegerClamp = IntegerClamp -denote IntegerNegate = IntegerNegate -denote IntegerShow = IntegerShow -denote IntegerToDouble = IntegerToDouble -denote Double = Double -denote (DoubleLit a ) = DoubleLit a -denote DoubleShow = DoubleShow -denote Text = Text -denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b) -denote (TextAppend a b ) = TextAppend (denote a) (denote b) -denote TextShow = TextShow -denote List = List -denote (ListLit a b ) = ListLit (fmap denote a) (fmap denote b) -denote (ListAppend a b ) = ListAppend (denote a) (denote b) -denote ListBuild = ListBuild -denote ListFold = ListFold -denote ListLength = ListLength -denote ListHead = ListHead -denote ListLast = ListLast -denote ListIndexed = ListIndexed -denote ListReverse = ListReverse -denote Optional = Optional -denote (Some a ) = Some (denote a) -denote None = None -denote OptionalFold = OptionalFold -denote OptionalBuild = OptionalBuild -denote (Record a ) = Record (fmap denote a) -denote (RecordLit a ) = RecordLit (fmap denote a) -denote (Union a ) = Union (fmap (fmap denote) a) -denote (Combine _ b c ) = Combine Nothing (denote b) (denote c) -denote (CombineTypes a b ) = CombineTypes (denote a) (denote b) -denote (Prefer a b c ) = Prefer a' (denote b) (denote c) - where - a' = case a of - PreferFromSource -> PreferFromSource - PreferFromWith e -> PreferFromWith (denote e) - PreferFromCompletion -> PreferFromCompletion -denote (RecordCompletion a b) = RecordCompletion (denote a) (denote b) -denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c) -denote (ToMap a b ) = ToMap (denote a) (fmap denote b) -denote (Field a b ) = Field (denote a) b -denote (Project a b ) = Project (denote a) (fmap denote b) -denote (Assert a ) = Assert (denote a) -denote (Equivalent a b ) = Equivalent (denote a) (denote b) -denote (With a b c ) = With (denote a) b (denote c) -denote (ImportAlt a b ) = ImportAlt (denote a) (denote b) -denote (Embed a ) = Embed a +denote (Embed a ) = Embed a +denote (Combine _ b c) = Combine Nothing (denote b) (denote c) +denote expression = Lens.over unsafeSubExpressions denote expression -- | The \"opposite\" of `denote`, like @first absurd@ but faster renote :: Expr Void a -> Expr s a @@ -1356,3 +1116,26 @@ ) ) rewrite _ = Nothing + +_ERROR :: String +_ERROR = "\ESC[1;31mError\ESC[0m" + +{-| Utility function used to throw internal errors that should never happen + (in theory) but that are not enforced by the type system +-} +internalError :: Data.Text.Text -> forall b . b +internalError text = error (unlines + [ _ERROR <> ": Compiler bug " + , " " + , "Explanation: This error message means that there is a bug in the Dhall compiler." + , "You didn't do anything wrong, but if you would like to see this problem fixed " + , "then you should report the bug at: " + , " " + , "https://github.com/dhall-lang/dhall-haskell/issues " + , " " + , "Please include the following text in your bug report: " + , " " + , "``` " + , Data.Text.unpack text <> " " + , "``` " + ] ) diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -874,7 +874,7 @@ -- > -- > { foo = 1, bar = "ABC" } ∧ { foo = True } -- > --- > (stdin):1:1 +-- > (input):1:1 -- -- __Exercise__: Combine any record with the empty record. What do you expect -- to happen? @@ -941,7 +941,7 @@ -- > -- > Error: Invalid input -- > --- > (stdin):1:11: +-- > (input):1:11: -- > | -- > 1 | let twice (x : Text) = x ++ x in twice "ha" -- > | ^ @@ -1381,7 +1381,7 @@ -- > -- > 1│ ./test.dhall -- > --- > (stdin):1:1 +-- > (input):1:1 -- -- You can compare expressions that contain variables, too, which is equivalent -- to symbolic reasoning: @@ -1410,7 +1410,7 @@ -- > -- > 1│ assert : Natural/even (n + n) === True -- > --- > (stdin):1:19 +-- > (input):1:19 -- -- Here the interpreter is not smart enough to simplify @Natural/even (n + n)@ -- to @True@ so the assertion fails. @@ -1849,7 +1849,7 @@ -- > -- > +2 + +2 -- > --- > (stdin):1:1 +-- > (input):1:1 -- -- In fact, there are no built-in functions for @Integer@s (or @Double@s) other -- than @Integer/show@ and @Double/show@. As far as the language is concerned @@ -1932,7 +1932,7 @@ -- > -- > Natural/equal -- > --- > (stdin):1:1 +-- > (input):1:1 -- -- You will need to either: -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -31,7 +31,7 @@ import Control.Exception (Exception) import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Writer.Strict (execWriterT, tell) -import Data.Monoid (Endo(..), First(..)) +import Data.Monoid (Endo(..)) import Data.List.NonEmpty (NonEmpty(..)) import Data.Semigroup (Max(..), Semigroup(..)) import Data.Sequence (Seq, ViewL(..)) @@ -55,7 +55,7 @@ , Var(..) ) -import qualified Data.Foldable +import qualified Data.Foldable as Foldable import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Map import qualified Data.Sequence @@ -86,8 +86,7 @@ {-# DEPRECATED X "Use Data.Void.Void instead" #-} traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f () -traverseWithIndex_ k xs = - Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs) +traverseWithIndex_ k xs = Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs) axiom :: Const -> Either (TypeError s a) Const axiom Type = return Kind @@ -781,36 +780,18 @@ return (VRecord xTs) Union xTs -> do - let nonEmpty x mT = First (fmap (\_T -> (x, _T)) mT) - - case getFirst (Dhall.Map.foldMapWithKey nonEmpty xTs) of - Nothing -> do - return (VConst Type) - - Just (x₀, _T₀) -> do - tT₀' <- loop ctx _T₀ - - c₀ <- case tT₀' of - VConst c₀ -> return c₀ - _ -> die (InvalidAlternativeType x₀ _T₀) - - let process _ Nothing = do - return () - - process x₁ (Just _T₁) = do - tT₁' <- loop ctx _T₁ - - c₁ <- case tT₁' of - VConst c₁ -> return c₁ - _ -> die (InvalidAlternativeType x₁ _T₁) + let process _ Nothing = do + return mempty - if c₀ == c₁ - then return () - else die (AlternativeAnnotationMismatch x₁ _T₁ c₁ x₀ _T₀ c₀) + process x₁ (Just _T₁) = do + tT₁' <- loop ctx _T₁ - Dhall.Map.unorderedTraverseWithKey_ process (Dhall.Map.delete x₀ xTs) + case tT₁' of + VConst c -> return (Max c) + _ -> die (InvalidAlternativeType x₁ _T₁) - return (VConst c₀) + Max c <- fmap Foldable.fold (Dhall.Map.unorderedTraverseWithKey process xTs) + return (VConst c) Combine mk l r -> do _L' <- loop ctx l @@ -901,7 +882,7 @@ let mL = Dhall.Map.toMap xLs₀' let mR = Dhall.Map.toMap xRs₀' - Data.Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) + Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) combineTypes [] xLs' xRs' @@ -1048,7 +1029,7 @@ (Data.Map.intersectionWithKey match (Dhall.Map.toMap yTs') (Dhall.Map.toMap yUs')) let checkMatched :: Data.Map.Map Text (Val a) -> Either (TypeError s a) (Maybe (Val a)) - checkMatched = fmap (fmap snd) . Data.Foldable.foldlM go Nothing . Data.Map.toList + checkMatched = fmap (fmap snd) . Foldable.foldlM go Nothing . Data.Map.toList where go Nothing (y₁, _T₁') = return (Just (y₁, _T₁')) @@ -1102,7 +1083,7 @@ VConst Type -> return () _ -> die (InvalidToMapRecordKind _E'' tE'') - Data.Foldable.traverse_ (loop ctx) mT₁ + Foldable.traverse_ (loop ctx) mT₁ let compareFieldTypes _T₀' Nothing = Just (Right _T₀') @@ -1342,7 +1323,6 @@ | IfBranchMustBeTerm Bool (Expr s a) (Expr s a) (Expr s a) | InvalidFieldType Text (Expr s a) | InvalidAlternativeType Text (Expr s a) - | AlternativeAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const | ListAppendMismatch (Expr s a) (Expr s a) | MustUpdateARecord (Expr s a) (Expr s a) (Expr s a) | MustCombineARecord Char (Expr s a) (Expr s a) @@ -2637,70 +2617,6 @@ txt0 = insert k txt1 = insert expr0 -prettyTypeMessage (AlternativeAnnotationMismatch k0 expr0 c0 k1 expr1 c1) = ErrorMessages {..} - where - short = "Alternative annotation mismatch" - - long = - "Explanation: Every union type annotates each alternative with a ❰Type❱ or a \n\ - \❰Kind❱, like this: \n\ - \ \n\ - \ \n\ - \ ┌───────────────────────────────────┐ \n\ - \ │ < Left : Natural | Right : Bool > │ Every alternative is annotated with a\n\ - \ └───────────────────────────────────┘ ❰Type❱ \n\ - \ \n\ - \ \n\ - \ ┌────────────────────────────────────┐ \n\ - \ │ < Foo : Type → Type | Bar : Type > │ Every alternative is annotated with \n\ - \ └────────────────────────────────────┘ a ❰Kind❱ \n\ - \ \n\ - \ \n\ - \ ┌────────────────┐ \n\ - \ │ < Baz : Kind > │ Every alternative is annotated with a ❰Sort❱ \n\ - \ └────────────────┘ \n\ - \ \n\ - \ \n\ - \However, you cannot have a union type that mixes ❰Type❱s, ❰Kind❱s, or ❰Sort❱s \n\ - \for the annotations: \n\ - \ \n\ - \ \n\ - \ This is a ❰Type❱ annotation \n\ - \ ⇩ \n\ - \ ┌───────────────────────────────┐ \n\ - \ │ { foo : Natural, bar : Type } │ Invalid union type \n\ - \ └───────────────────────────────┘ \n\ - \ ⇧ \n\ - \ ... but this is a ❰Kind❱ annotation \n\ - \ \n\ - \ \n\ - \You provided a union type with an alternative named: \n\ - \ \n\ - \" <> txt0 <> "\n\ - \ \n\ - \... annotated with the following expression: \n\ - \ \n\ - \" <> txt1 <> "\n\ - \ \n\ - \... which is a " <> level c0 <> " whereas another alternative named: \n\ - \ \n\ - \" <> txt2 <> "\n\ - \ \n\ - \... annotated with the following expression: \n\ - \ \n\ - \" <> txt3 <> "\n\ - \ \n\ - \... is a " <> level c1 <> ", which does not match \n" - where - txt0 = insert k0 - txt1 = insert expr0 - txt2 = insert k1 - txt3 = insert expr1 - - level Type = "❰Type❱" - level Kind = "❰Kind❱" - level Sort = "❰Sort❱" - prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..} where short = "You can only append ❰List❱s with matching element types\n" @@ -4676,8 +4592,6 @@ InvalidFieldType <$> pure a <*> f b InvalidAlternativeType a b -> InvalidAlternativeType <$> pure a <*> f b - AlternativeAnnotationMismatch a b c d e g -> - AlternativeAnnotationMismatch <$> pure a <*> f b <*> pure c <*> pure d <*> f e <*> pure g ListAppendMismatch a b -> ListAppendMismatch <$> f a <*> f b InvalidDuplicateField a b c -> @@ -4832,6 +4746,4 @@ toPath :: (Functor list, Foldable list) => list Text -> Text toPath ks = Text.intercalate "." - (Data.Foldable.toList - (fmap (Dhall.Pretty.Internal.escapeLabel True) ks) - ) + (Foldable.toList (fmap (Dhall.Pretty.Internal.escapeLabel True) ks)) diff --git a/src/Dhall/Util.hs b/src/Dhall/Util.hs --- a/src/Dhall/Util.hs +++ b/src/Dhall/Util.hs @@ -116,8 +116,8 @@ let name = case input of Input_ (InputFile file) -> file - Input_ StandardInput -> "(stdin)" - StdinText _ -> "(stdin)" + Input_ StandardInput -> "(input)" + StdinText _ -> "(input)" let result = parser name inText 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 @@ -18,10 +18,12 @@ import Control.Exception (SomeException, try) import Data.Fix (Fix(..)) +import Data.List.NonEmpty (NonEmpty (..)) import Data.Sequence (Seq) import Data.Scientific (Scientific) import Data.Text (Text) import Data.Vector (Vector) +import Data.Void (Void) import Dhall (ToDhall, FromDhall) import Dhall.Core (Expr(..)) import GHC.Generics (Generic, Rep) @@ -51,8 +53,9 @@ , shouldHaveWorkingGenericAuto , shouldHandleUnionsCorrectly , shouldTreatAConstructorStoringUnitAsEmptyAlternative - , shouldConvertDhallToHaskellCorrectly + , shouldConvertDhallToHaskellCorrectly , shouldConvertHaskellToDhallCorrectly + , shouldShowCorrectErrorForInvalidDecoderInUnion ] data MyType = MyType { foo :: String , bar :: Natural } @@ -415,3 +418,45 @@ Dhall.Core.pretty (Dhall.embed Dhall.inject haskellValue) expectedDhallCode @=? actualDhallCode + +-- https://github.com/dhall-lang/dhall-haskell/issues/1711 +data Issue1711 + = A Bad + | B + | C + | D + deriving (Generic, Show, FromDhall) + +newtype Bad = Bad Text + deriving (Show) + +issue1711Msg :: Text +issue1711Msg = "Issue 1711" + +instance FromDhall Bad where + autoWith _ = + Dhall.Decoder + (const (Dhall.extractError issue1711Msg)) + (Dhall.expected Dhall.strictText) + +type DhallExtractErrors = Dhall.ExtractErrors Dhall.Parser.Src Void + +-- https://github.com/dhall-lang/dhall-haskell/issues/1711 +shouldShowCorrectErrorForInvalidDecoderInUnion :: TestTree +shouldShowCorrectErrorForInvalidDecoderInUnion = + testCase "Correct error is thrown for invalid decoder in union" $ do + let value = "< B | D | C | A : Text >.A \"\"" + + inputEx :: Either DhallExtractErrors Issue1711 <- try (Dhall.input Dhall.auto value) + + let expectedMsg = issue1711Msg + + let assertMsg = "The exception message did not match the expected output" + + case inputEx of + Left (Dhall.ExtractErrors errs) -> case errs of + (err :| []) -> case err of + Dhall.TypeMismatch {} -> fail "The extraction using an invalid decoder failed with a type mismatch" + Dhall.ExtractError extractError -> assertEqual assertMsg expectedMsg extractError + _ -> fail "The extraction using an invalid decoder failed with multiple errors" + Right _ -> fail "The extraction using an invalid decoder succeeded" diff --git a/tests/Dhall/Test/Freeze.hs b/tests/Dhall/Test/Freeze.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Freeze.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Freeze where + +import Data.Text (Text) +import Dhall.Freeze (Intent(..), Scope(..)) +import Prelude hiding (FilePath) +import Test.Tasty (TestTree) +import Turtle (FilePath) + +import qualified Data.Text as Text +import qualified Data.Text.IO as Text.IO +import qualified Dhall.Core as Core +import qualified Dhall.Freeze as Freeze +import qualified Dhall.Parser as Parser +import qualified Dhall.Test.Util as Test.Util +import qualified Test.Tasty as Tasty +import qualified Test.Tasty.HUnit as Tasty.HUnit +import qualified Turtle + +freezeDirectory :: FilePath +freezeDirectory = "./tests/freeze" + +getTests :: IO TestTree +getTests = do + freezeTests <- Test.Util.discover (Turtle.chars <* "A.dhall") freezeTest (Turtle.lstree freezeDirectory) + + let testTree = Tasty.testGroup "freeze tests" [ freezeTests ] + + return testTree + +freezeTest :: Text -> TestTree +freezeTest prefix = do + 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 + + parsedInput <- Core.throws (Parser.exprFromText mempty inputText) + + actualExpression <- Freeze.freezeExpression (Turtle.encodeString freezeDirectory) AllImports Cache parsedInput + + let actualText = Core.pretty actualExpression <> "\n" + + expectedText <- Text.IO.readFile outputFile + + let message = "The linted expression did not match the expected output" + + Tasty.HUnit.assertEqual message expectedText actualText 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 @@ -81,7 +81,10 @@ State.evalStateT (Test.Util.loadWith actualExpr) (Import.emptyStatus directoryString) let runTest = do - if Turtle.filename (Turtle.fromText path) == "hashFromCacheA.dhall" + if Turtle.filename (Turtle.fromText path) `elem` + [ "hashFromCacheA.dhall" + , "unit/asLocation/HashA.dhall" + ] then do setCache _ <- load diff --git a/tests/Dhall/Test/Main.hs b/tests/Dhall/Test/Main.hs --- a/tests/Dhall/Test/Main.hs +++ b/tests/Dhall/Test/Main.hs @@ -7,6 +7,7 @@ import qualified Dhall.Test.Diff import qualified Dhall.Test.Tags import qualified Dhall.Test.Format +import qualified Dhall.Test.Freeze import qualified Dhall.Test.SemanticHash import qualified Dhall.Test.Import import qualified Dhall.Test.Lint @@ -43,6 +44,8 @@ semanticHashTests <- Dhall.Test.SemanticHash.getTests + freezeTests <- Dhall.Test.Freeze.getTests + let testTree = Test.Tasty.testGroup "Dhall Tests" [ normalizationTests @@ -54,6 +57,7 @@ , diffTests , semanticHashTests , tagsTests + , freezeTests , Dhall.Test.Regression.tests , Dhall.Test.Tutorial.tests , Dhall.Test.QuickCheck.tests diff --git a/tests/Dhall/Test/Normalization.hs b/tests/Dhall/Test/Normalization.hs --- a/tests/Dhall/Test/Normalization.hs +++ b/tests/Dhall/Test/Normalization.hs @@ -170,10 +170,14 @@ Tasty.HUnit.assertEqual message expectedNormalized actualNormalized betaNormalizationTest :: Text -> TestTree -betaNormalizationTest prefix = - Tasty.HUnit.testCase (Text.unpack prefix) $ do - let actualCode = Test.Util.toDhallPath (prefix <> "A.dhall") - let expectedCode = Test.Util.toDhallPath (prefix <> "B.dhall") +betaNormalizationTest prefix = do + let prefixString = Text.unpack prefix + + Tasty.HUnit.testCase prefixString $ do + let actualCode = Test.Util.toDhallPath (prefix <> "A.dhall") + + let expectedPath = prefixString <> "B.dhall" + expectedCode <- Text.IO.readFile expectedPath actualExpr <- throws (Parser.exprFromText mempty actualCode) diff --git a/tests/Dhall/Test/SemanticHash.hs b/tests/Dhall/Test/SemanticHash.hs --- a/tests/Dhall/Test/SemanticHash.hs +++ b/tests/Dhall/Test/SemanticHash.hs @@ -45,4 +45,4 @@ let message = "The hash did not match the expected hash." - Tasty.HUnit.assertEqual message actualHash expectedHash + Tasty.HUnit.assertEqual message expectedHash actualHash diff --git a/tests/format/concatSepB.dhall b/tests/format/concatSepB.dhall --- a/tests/format/concatSepB.dhall +++ b/tests/format/concatSepB.dhall @@ -5,20 +5,20 @@ let concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text - = λ(separator : Text) - → λ(elements : List Text) - → let status = + = λ(separator : Text) → + λ(elements : List Text) → + let status = List/fold Text elements Status - ( λ(element : Text) - → λ(status : Status) - → merge + ( λ(element : Text) → + λ(status : Status) → + merge { Empty = Status.NonEmpty element , NonEmpty = - λ(result : Text) - → Status.NonEmpty (element ++ separator ++ result) + λ(result : Text) → + Status.NonEmpty (element ++ separator ++ result) } status ) diff --git a/tests/format/ifThenElseB.dhall b/tests/format/ifThenElseB.dhall --- a/tests/format/ifThenElseB.dhall +++ b/tests/format/ifThenElseB.dhall @@ -1,13 +1,7 @@ - if True - +if True then if True then if True then 1 else 2 else if True then 3 else 4 - else if True - then if True then 5 else 6 - else if True - then 7 - else 8 diff --git a/tests/format/ipfsB.dhall b/tests/format/ipfsB.dhall --- a/tests/format/ipfsB.dhall +++ b/tests/format/ipfsB.dhall @@ -20,14 +20,14 @@ let gatewayPort = k8s.IntOrString.Int 8080 let toRule = - λ ( args - : { host : Text - , path : Text - , serviceName : Text - , servicePort : k8s.IntOrString - } - ) - → k8s.IngressRule::{ + λ ( args + : { host : Text + , path : Text + , serviceName : Text + , servicePort : k8s.IntOrString + } + ) → + k8s.IngressRule::{ , host = Some args.host , http = Some k8s.HTTPIngressRuleValue::{ , paths = @@ -86,12 +86,12 @@ } , k8s.Resource.StatefulSet k8s.StatefulSet::{ - , metadata = k8s.ObjectMeta::{ name = name, labels = toMap labels } + , metadata = k8s.ObjectMeta::{ name, labels = toMap labels } , spec = Some k8s.StatefulSetSpec::{ - , serviceName = serviceName + , serviceName , selector = k8s.LabelSelector::{ matchLabels = toMap matchLabels } , template = k8s.PodTemplateSpec::{ - , metadata = k8s.ObjectMeta::{ name = name, labels = toMap labels } + , metadata = k8s.ObjectMeta::{ name, labels = toMap labels } , spec = Some k8s.PodSpec::{ , securityContext = Some k8s.PodSecurityContext::{ , runAsUser = Some 1000 @@ -100,7 +100,7 @@ } , containers = [ k8s.Container::{ - , name = name + , name , image = Some "ipfs/go-ipfs:v0.4.22" , livenessProbe = k8s.Probe::{ , httpGet = Some k8s.HTTPGetAction::{ diff --git a/tests/format/issue1400-2B.dhall b/tests/format/issue1400-2B.dhall --- a/tests/format/issue1400-2B.dhall +++ b/tests/format/issue1400-2B.dhall @@ -1,7 +1,7 @@ let Tagged : Type → Type - = λ(a : Type) - → { field : Text + = λ(a : Type) → + { field : Text , nesting : ./Nesting sha256:6284802edd41d5d725aa1ec7687e614e21ad1be7e14dd10996bfa9625105c335 ? ./Nesting diff --git a/tests/format/issue183B.dhall b/tests/format/issue183B.dhall --- a/tests/format/issue183B.dhall +++ b/tests/format/issue183B.dhall @@ -1,9 +1,9 @@ let foo = 1 -in λ(bar : Integer) - → let exposePort = - λ(portSpec : { ext : Integer, int : Integer }) - → Integer/show portSpec.ext ++ ":" ++ Integer/show portSpec.int +in λ(bar : Integer) → + let exposePort = + λ(portSpec : { ext : Integer, int : Integer }) → + Integer/show portSpec.ext ++ ":" ++ Integer/show portSpec.int in let exposeSamePort = λ(port : Integer) → exposePort { ext = port, int = port } diff --git a/tests/format/recordCompletionA.dhall b/tests/format/recordCompletionA.dhall --- a/tests/format/recordCompletionA.dhall +++ b/tests/format/recordCompletionA.dhall @@ -22,4 +22,5 @@ , t = 1 } , field1 = T::{ a = 1 } +, field2 = T::{ a = a } } diff --git a/tests/format/recordCompletionB.dhall b/tests/format/recordCompletionB.dhall --- a/tests/format/recordCompletionB.dhall +++ b/tests/format/recordCompletionB.dhall @@ -21,4 +21,5 @@ , t = 1 } , field1 = T::{ a = 1 } +, field2 = T::{ a } } diff --git a/tests/format/unicodeB.dhall b/tests/format/unicodeB.dhall --- a/tests/format/unicodeB.dhall +++ b/tests/format/unicodeB.dhall @@ -1,5 +1,5 @@ - λ(isActive : Bool) -→ { barLeftEnd = Some "┨" +λ(isActive : Bool) → + { barLeftEnd = Some "┨" , barRightEnd = Some "┠" , separator = Some "┃" , alignment = diff --git a/tests/format/withPrecedenceA.dhall b/tests/format/withPrecedenceA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/withPrecedenceA.dhall @@ -0,0 +1,5 @@ +let Foo = + Bar + with default = (Bar.default ⫽ { bar = 0 }) + +in Foo diff --git a/tests/format/withPrecedenceB.dhall b/tests/format/withPrecedenceB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/withPrecedenceB.dhall @@ -0,0 +1,1 @@ +let Foo = Bar with default = Bar.default ⫽ { bar = 0 } in Foo diff --git a/tests/freeze/True.dhall b/tests/freeze/True.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/True.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/freeze/cachedA.dhall b/tests/freeze/cachedA.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/cachedA.dhall @@ -0,0 +1,2 @@ + ./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 +? ./True.dhall diff --git a/tests/freeze/cachedB.dhall b/tests/freeze/cachedB.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/cachedB.dhall @@ -0,0 +1,2 @@ + ./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 +? ./True.dhall diff --git a/tests/freeze/incorrectHashA.dhall b/tests/freeze/incorrectHashA.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/incorrectHashA.dhall @@ -0,0 +1,1 @@ +./True.dhall sha256:0000000000000000000000000000000000000000000000000000000000000000 diff --git a/tests/freeze/incorrectHashB.dhall b/tests/freeze/incorrectHashB.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/incorrectHashB.dhall @@ -0,0 +1,2 @@ + ./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 +? ./True.dhall diff --git a/tests/freeze/protectedA.dhall b/tests/freeze/protectedA.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/protectedA.dhall @@ -0,0 +1,1 @@ +./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 diff --git a/tests/freeze/protectedB.dhall b/tests/freeze/protectedB.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/protectedB.dhall @@ -0,0 +1,2 @@ + ./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 +? ./True.dhall diff --git a/tests/freeze/unprotectedA.dhall b/tests/freeze/unprotectedA.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/unprotectedA.dhall @@ -0,0 +1,1 @@ +./True.dhall diff --git a/tests/freeze/unprotectedB.dhall b/tests/freeze/unprotectedB.dhall new file mode 100644 --- /dev/null +++ b/tests/freeze/unprotectedB.dhall @@ -0,0 +1,2 @@ + ./True.dhall sha256:27abdeddfe8503496adeb623466caa47da5f63abd2bc6fa19f6cfcb73ecfed70 +? ./True.dhall diff --git a/tests/lint/success/assertB.dhall b/tests/lint/success/assertB.dhall --- a/tests/lint/success/assertB.dhall +++ b/tests/lint/success/assertB.dhall @@ -3,9 +3,9 @@ let assertIn1Lam = λ(n : Natural) → assert : Natural/subtract 0 n ≡ n let assertIn2Lams = - λ(m : Natural) - → λ(n : Natural) - → assert : Natural/subtract m m ≡ Natural/subtract n n + λ(m : Natural) → + λ(n : Natural) → + assert : Natural/subtract m m ≡ Natural/subtract n n let assertInLetInLam = λ(m : Natural) → let n = m + 0 in assert : m ≡ n diff --git a/tests/lint/success/multiletB.dhall b/tests/lint/success/multiletB.dhall --- a/tests/lint/success/multiletB.dhall +++ b/tests/lint/success/multiletB.dhall @@ -2,15 +2,15 @@ let Person : Type - = ∀(Person : Type) - → ∀(MakePerson : { children : List Person, name : Text } → Person) - → Person + = ∀(Person : Type) → + ∀(MakePerson : { children : List Person, name : Text } → Person) → + Person let example : Person - = λ(Person : Type) - → λ(MakePerson : { children : List Person, name : Text } → Person) - → MakePerson + = λ(Person : Type) → + λ(MakePerson : { children : List Person, name : Text } → Person) → + MakePerson { children = [ MakePerson { children = [] : List Person, name = "Mary" } , MakePerson { children = [] : List Person, name = "Jane" } @@ -22,11 +22,11 @@ : Person → List Text = let concat = http://prelude.dhall-lang.org/List/concat - in λ(x : Person) - → x + in λ(x : Person) → + x (List Text) - ( λ(p : { children : List (List Text), name : Text }) - → [ p.name ] # concat Text p.children + ( λ(p : { children : List (List Text), name : Text }) → + [ p.name ] # concat Text p.children ) let result diff --git a/tests/lint/success/optionalFoldBuildB.dhall b/tests/lint/success/optionalFoldBuildB.dhall --- a/tests/lint/success/optionalFoldBuildB.dhall +++ b/tests/lint/success/optionalFoldBuildB.dhall @@ -1,18 +1,18 @@ { example0 = - λ(a : Type) - → λ(o : Optional a) - → λ(optional : Type) - → λ(some : a → optional) - → λ(none : optional) - → merge { Some = some, None = none } o + λ(a : Type) → + λ(o : Optional a) → + λ(optional : Type) → + λ(some : a → optional) → + λ(none : optional) → + merge { Some = some, None = none } o , example1 = - λ(a : Type) - → λ ( build - : ∀(optional : Type) - → ∀(some : a → optional) - → ∀(none : optional) - → optional - ) - → build (Optional a) (λ(x : a) → Some x) (None a) + λ(a : Type) → + λ ( build + : ∀(optional : Type) → + ∀(some : a → optional) → + ∀(none : optional) → + optional + ) → + build (Optional a) (λ(x : a) → Some x) (None a) , example2 = merge { Some = Natural/even, None = False } (Some 1) } diff --git a/tests/regression/issue216a.dhall b/tests/regression/issue216a.dhall --- a/tests/regression/issue216a.dhall +++ b/tests/regression/issue216a.dhall @@ -1,5 +1,5 @@ let GitHubProject : Type = { owner : Text, repo : Text } in let gitHubProject = \( github : GitHubProject ) -> let gitHubRoot = "https://github.com/${github.owner}/${github.repo}" - in { bugReports = "${gitHubRoot}/issues" } + in { bugReports = "${gitHubRoot}/issues" } in gitHubProject diff --git a/tests/regression/issue216b.dhall b/tests/regression/issue216b.dhall --- a/tests/regression/issue216b.dhall +++ b/tests/regression/issue216b.dhall @@ -1,2 +1,2 @@ - λ(github : { owner : Text, repo : Text }) -→ { bugReports = "https://github.com/${github.owner}/${github.repo}/issues" } +λ(github : { owner : Text, repo : Text }) → + { bugReports = "https://github.com/${github.owner}/${github.repo}/issues" }