dhall 1.26.1 → 1.27.0

raw patch · 212 files changed

+8031/−6646 lines, 212 filesdep +hashabledep +special-valuesdep ~eitherdep ~unordered-containersbinary-addedPVP ok

version bump matches the API change (PVP)

Dependencies added: hashable, special-values

Dependency ranges changed: either, unordered-containers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +57/−1
• dhall-lang/Prelude/Bool/not +3/−1
• dhall-lang/Prelude/Bool/show +3/−1
• dhall-lang/Prelude/Double/show +3/−1
• dhall-lang/Prelude/Integer/show +3/−1
• dhall-lang/Prelude/Integer/toDouble +3/−1
• dhall-lang/Prelude/JSON/Nesting +5/−1
• dhall-lang/Prelude/JSON/Tagged +1/−2
• dhall-lang/Prelude/JSON/Type +6/−12
• dhall-lang/Prelude/JSON/array +6/−12
• dhall-lang/Prelude/JSON/bool +6/−12
• dhall-lang/Prelude/JSON/keyText +2/−14
• dhall-lang/Prelude/JSON/keyValue +2/−17
• dhall-lang/Prelude/JSON/null +6/−12
• dhall-lang/Prelude/JSON/number +6/−12
• dhall-lang/Prelude/JSON/object +6/−12
• dhall-lang/Prelude/JSON/render +4/−8
• dhall-lang/Prelude/JSON/string +6/−12
• dhall-lang/Prelude/List/default +15/−0
• dhall-lang/Prelude/List/empty +10/−0
• dhall-lang/Prelude/List/head +3/−1
• dhall-lang/Prelude/List/last +3/−1
• dhall-lang/Prelude/List/length +3/−1
• dhall-lang/Prelude/List/package.dhall +6/−0
• dhall-lang/Prelude/List/reverse +3/−1
• dhall-lang/Prelude/List/shifted +3/−6
• dhall-lang/Prelude/Location/Type +3/−6
• dhall-lang/Prelude/Map/empty +15/−0
• dhall-lang/Prelude/Map/keyText +15/−0
• dhall-lang/Prelude/Map/keyValue +17/−0
• dhall-lang/Prelude/Map/package.dhall +9/−0
• dhall-lang/Prelude/Monoid +5/−1
• dhall-lang/Prelude/Natural/even +3/−1
• dhall-lang/Prelude/Natural/isZero +3/−1
• dhall-lang/Prelude/Natural/odd +3/−1
• dhall-lang/Prelude/Natural/show +3/−1
• dhall-lang/Prelude/Natural/subtract +3/−1
• dhall-lang/Prelude/Natural/toInteger +3/−1
• dhall-lang/Prelude/Optional/default +15/−0
• dhall-lang/Prelude/Optional/package.dhall +3/−0
• dhall-lang/Prelude/Text/concatMapSep +1/−2
• dhall-lang/Prelude/Text/concatSep +1/−2
• dhall-lang/Prelude/Text/show +3/−1
• dhall-lang/Prelude/XML/Type +4/−8
• dhall-lang/Prelude/XML/element +10/−20
• dhall-lang/Prelude/XML/leaf +2/−4
• dhall-lang/Prelude/XML/render +4/−8
• dhall-lang/Prelude/XML/text +4/−8
• dhall-lang/Prelude/package.dhall +3/−3
• dhall-lang/tests/binary-decode/failure/unit/OperatorUnknownOpcode.dhallb binary
• dhall-lang/tests/binary-decode/success/unit/CompletionA.dhallb binary
• dhall-lang/tests/binary-decode/success/unit/CompletionB.dhall +1/−0
• dhall-lang/tests/import/data/importBoundary.dhall +3/−0
• dhall-lang/tests/import/failure/customHeadersUsingBoundVariable.dhall +15/−0
• dhall-lang/tests/import/failure/importBoundary.dhall +1/−0
• dhall-lang/tests/normalization/success/simple/completionA.dhall +10/−0
• dhall-lang/tests/normalization/success/simple/completionB.dhall +5/−0
• dhall-lang/tests/normalization/success/unit/CompletionA.dhall +1/−0
• dhall-lang/tests/normalization/success/unit/CompletionB.dhall +1/−0
• dhall-lang/tests/normalization/success/unit/RecursiveRecordTypeMergeDeepA.dhall +1/−0
• dhall-lang/tests/normalization/success/unit/RecursiveRecordTypeMergeDeepB.dhall +1/−0
• dhall-lang/tests/parser/failure/nonBase16Hash.dhall +1/−0
• dhall-lang/tests/parser/success/leadingSeparatorsA.dhall +10/−0
• dhall-lang/tests/parser/success/leadingSeparatorsB.dhallb +1/−0
• dhall-lang/tests/parser/success/lineCommentCRLFA.dhall +3/−0
• dhall-lang/tests/parser/success/lineCommentCRLFB.dhallb +1/−0
• dhall-lang/tests/parser/success/text/dollarSignA.dhall +1/−0
• dhall-lang/tests/parser/success/text/dollarSignB.dhallb +1/−0
• dhall-lang/tests/parser/success/unit/CompletionA.dhall +1/−0
• dhall-lang/tests/parser/success/unit/CompletionB.dhallb binary
• dhall-lang/tests/parser/success/unit/DoubleLitNegZeroA.dhall +1/−0
• dhall-lang/tests/parser/success/unit/DoubleLitNegZeroB.dhallb binary
• dhall-lang/tests/parser/success/unit/import/environmentVariablePosixA.dhall +1/−1
• dhall-lang/tests/parser/success/unit/import/environmentVariablePosixB.dhallb binary
• dhall-lang/tests/parser/success/unit/import/urls/ipv4upperoctetsA.dhall +1/−0
• dhall-lang/tests/parser/success/unit/import/urls/ipv4upperoctetsB.dhallb binary
• dhall-lang/tests/parser/success/unit/import/urls/ipv6verylongA.dhall +1/−0
• dhall-lang/tests/parser/success/unit/import/urls/ipv6verylongB.dhallb binary
• dhall-lang/tests/type-inference/data/importBoundary.dhall +0/−3
• dhall-lang/tests/type-inference/failure/customHeadersUsingBoundVariable.dhall +0/−15
• dhall-lang/tests/type-inference/failure/importBoundary.dhall +0/−1
• dhall-lang/tests/type-inference/success/preludeB.dhall +148/−274
• dhall-lang/tests/type-inference/success/simple/completionA.dhall +25/−0
• dhall-lang/tests/type-inference/success/simple/completionB.dhall +8/−0
• dhall-lang/tests/type-inference/success/simple/orderInsensitivityA.dhall +15/−0
• dhall-lang/tests/type-inference/success/simple/orderInsensitivityB.dhall +1/−0
• dhall-lang/tests/type-inference/success/simple/toMapEmptyNormalizeAnnotationA.dhall +3/−0
• dhall-lang/tests/type-inference/success/simple/toMapEmptyNormalizeAnnotationB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/CompletionA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/CompletionB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionApplicationNormalizeArgumentA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionApplicationNormalizeArgumentB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionApplicationNormalizeResultA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionApplicationNormalizeResultB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionNormalizeTypeAnnotationA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/FunctionNormalizeTypeAnnotationB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotation0A.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotation0B.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotation1A.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotation1B.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotationA.dhall +0/−1
• dhall-lang/tests/type-inference/success/unit/MergeOneWithAnnotationB.dhall +0/−1
• dhall-lang/tests/type-inference/success/unit/RecursiveRecordTypeMergeDeepA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/RecursiveRecordTypeMergeDeepB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/ToMapInferTypeFromRecordA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/ToMapInferTypeFromRecordB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/TypeAnnotationFunctionA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/TypeAnnotationFunctionB.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/TypeAnnotationNormalizeA.dhall +1/−0
• dhall-lang/tests/type-inference/success/unit/TypeAnnotationNormalizeB.dhall +1/−0
• dhall.cabal +16/−3
• doctest/Main.hs +2/−1
• ghc-src/Dhall/Crypto.hs +9/−0
• ghcjs-src/Dhall/Crypto.hs +9/−0
• src/Dhall.hs +597/−213
• src/Dhall/Binary.hs +34/−16
• src/Dhall/Binary.hs-boot +0/−10
• src/Dhall/Core.hs +1383/−2389
• src/Dhall/Core.hs-boot +0/−11
• src/Dhall/Diff.hs +20/−3
• src/Dhall/Eval.hs +53/−44
• src/Dhall/Eval.hs-boot +0/−8
• src/Dhall/Format.hs +4/−4
• src/Dhall/Freeze.hs +5/−5
• src/Dhall/Hash.hs +0/−37
• src/Dhall/Import.hs +18/−17
• src/Dhall/Import/Types.hs +23/−9
• src/Dhall/Lint.hs +17/−2
• src/Dhall/Main.hs +130/−28
• src/Dhall/Parser/Combinators.hs +1/−0
• src/Dhall/Parser/Expression.hs +99/−20
• src/Dhall/Parser/Token.hs +302/−2
• src/Dhall/Pretty/Internal.hs +126/−82
• src/Dhall/Pretty/Internal.hs-boot +1/−6
• src/Dhall/Repl.hs +10/−12
• src/Dhall/Set.hs +15/−4
• src/Dhall/Syntax.hs +1182/−0
• src/Dhall/Syntax.hs-boot +7/−0
• src/Dhall/Tags.hs +279/−0
• src/Dhall/Tutorial.hs +2172/−2983
• src/Dhall/TypeCheck.hs +182/−98
• src/Dhall/Util.hs +9/−5
• src/Dhall/Version.hs +5/−0
• tests/Dhall/Test/Dhall.hs +42/−44
• tests/Dhall/Test/Format.hs +7/−2
• tests/Dhall/Test/Lint.hs +3/−3
• tests/Dhall/Test/Main.hs +4/−0
• tests/Dhall/Test/Normalization.hs +7/−7
• tests/Dhall/Test/Parser.hs +12/−11
• tests/Dhall/Test/QuickCheck.hs +93/−7
• tests/Dhall/Test/Regression.hs +13/−4
• tests/Dhall/Test/Tags.hs +63/−0
• tests/Dhall/Test/Tutorial.hs +2/−2
• tests/Dhall/Test/TypeInference.hs +9/−21
• tests/Dhall/Test/Util.hs +16/−16
• tests/format/applicationMultilineA.dhall +30/−0
• tests/format/applicationMultilineB.dhall +30/−0
• tests/format/asciiB.dhall +0/−0
• tests/format/concatSepA.dhall +30/−0
• tests/format/concatSepB.dhall +33/−0
• tests/format/doubleRoundB.dhall +0/−0
• tests/format/emptyRecordB.dhall +0/−0
• tests/format/escapeNumericLabelB.dhall +0/−0
• tests/format/escapeSingleQuotedOpenInterpolationB.dhall +0/−0
• tests/format/fieldOrderB.dhall +0/−0
• tests/format/functionLikeA.dhall +6/−0
• tests/format/functionLikeB.dhall +6/−0
• tests/format/headerB.dhall +0/−0
• tests/format/ifThenElseB.dhall +0/−0
• tests/format/importAccessB.dhall +0/−0
• tests/format/importLines2A.dhall +0/−0
• tests/format/importLines2B.dhall +0/−0
• tests/format/importLinesB.dhall +0/−0
• tests/format/importSuffixB.dhall +0/−0
• tests/format/innerMultilineB.dhall +0/−0
• tests/format/issue1301B.dhall +0/−0
• tests/format/issue1413A.dhall +6/−0
• tests/format/issue1413B.dhall +6/−0
• tests/format/largeExponentB.dhall +0/−0
• tests/format/largeRecordB.dhall +9/−9
• tests/format/letB.dhall +0/−0
• tests/format/letCommentsB.dhall +0/−0
• tests/format/letLineCommentsAfterVariableA.dhall +10/−0
• tests/format/letLineCommentsAfterVariableB.dhall +12/−0
• tests/format/letLongCommentsB.dhall +0/−0
• tests/format/letNewlineCommentsB.dhall +0/−0
• tests/format/letShortCommentsB.dhall +7/−1
• tests/format/multilineB.dhall +0/−0
• tests/format/parentB.dhall +0/−0
• tests/format/projectionOrderB.dhall +0/−0
• tests/format/recordCompletionA.dhall +25/−0
• tests/format/recordCompletionB.dhall +25/−0
• tests/format/sha256PrintingB.dhall +0/−0
• tests/format/unicodeB.dhall +0/−0
• tests/format/urlsB.dhall +0/−0
• tests/lint/success/fixAssertA.dhall +1/−0
• tests/lint/success/fixAssertB.dhall +1/−0
• tests/tags/all.tags +61/−0
• tests/tags/let.dhall +4/−0
• tests/tags/let.tags +6/−0
• tests/tags/nonunicode.dhall +3/−0
• tests/tags/nonunicode.tags +5/−0
• tests/tags/record.dhall +35/−0
• tests/tags/record.tags +13/−0
• tests/tags/recordlit.dhall +14/−0
• tests/tags/recordlit.tags +10/−0
• tests/tags/simple.dhall +39/−0
• tests/tags/simple.tags +11/−0
• tests/tags/unicode.dhall +3/−0
• tests/tags/unicode.tags +5/−0
• tests/tags/union.dhall +4/−0
• tests/tags/union.tags +11/−0

@@ -1,3 +1,55 @@+1.27.0++* [Supports version 11.0.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v11.0.0)+* BREAKING CHANGE: Rename `Inject`/`Interpret` to `ToDhall`/`FromDhall`+    * This change `ConstraintKinds` to minimize disruption by keeping around+      `Inject`/`Interpret` as synonyms for `ToDhall`/`FromDhall`+    * In other words, constraints and derived instances using `Inject` or+      `Interpret` will still work+    * However, manual instances using `Inject` or `Interpret` won't work+      unless you rename them to `ToDhall`/`FromDhall` or enable the+      `TypeSynonymInstances` extension+* BREAKING CHANGE: Fix `Eq` instance for `Expr`s with special `Double`s+    * This fixes the `Eq` instance for `Expr`s to match the standard regarding+      `Double` comparisons+    * Specifically: `NaN == NaN` and `-0.0 /= 0.0`+    * This is a breaking change because the `DoubleLit` constructor of `Expr`+      now stores a `DhallDouble` instead of a `Double`+* BREAKING CHANGE: [Add `--file` option for `dhall hash`](https://github.com/dhall-lang/dhall-haskell/pull/1445)+    * This is a breaking change because it also removes the `Dhall.Hash` module,+      which wasn't really carrying its own weight+* [Add support for leading separators](https://github.com/dhall-lang/dhall-haskell/pull/1355)+    * See the [changelog for standard version 11.0.0](https://github.com/dhall-lang/dhall-lang/releases/tag/v11.0.0) for more details+* [Add record completion operator](https://github.com/dhall-lang/dhall-haskell/pull/1375)+    * See the [changelog for standard version 11.0.0](https://github.com/dhall-lang/dhall-lang/releases/tag/v11.0.0) for more details+* [Add `dhall tags` subcommand](https://github.com/dhall-lang/dhall-haskell/pull/1398)+    * This generates an ETags file from an input file or directory+* [Add `dhall lint` support for fixing malformed assertions](https://github.com/dhall-lang/dhall-haskell/pull/1353)+    * `dhall lint` now fixes `let example = foo === bar` to be+       `let example = assert : foo === bar`+* Normalize inferred types [#1337](https://github.com/dhall-lang/dhall-haskell/pull/1337)+* New `FromDhall`/`ToDhall` (previously `Interpret`/`Inject`) instances for:+    * [`Void`](https://github.com/dhall-lang/dhall-haskell/pull/1382)+    * `Map` [#1391](https://github.com/dhall-lang/dhall-haskell/pull/1391) / [#1412](https://github.com/dhall-lang/dhall-haskell/pull/1412)+    * [`HashMap`](https://github.com/dhall-lang/dhall-haskell/pull/1426)+    * [`Set` and `HashSet`](https://github.com/dhall-lang/dhall-haskell/pull/1405)+    * [`()`](https://github.com/dhall-lang/dhall-haskell/pull/1388)+* [Add `--output` option to `dhall`](https://github.com/dhall-lang/dhall-haskell/pull/1399)+* [Move syntax things from `Dhall.Core` to a new `Dhall.Syntax` module](https://github.com/dhall-lang/dhall-haskell/pull/1440)+    * This is not a breaking change.  `Dhall.Core` still re-exports the same+      API as before+* Performance improvements+    * [#1362](https://github.com/dhall-lang/dhall-haskell/pull/1362)+    * [#1366](https://github.com/dhall-lang/dhall-haskell/pull/1366)+    * [#1368](https://github.com/dhall-lang/dhall-haskell/pull/1368)+    * [#1397](https://github.com/dhall-lang/dhall-haskell/pull/1397)+    * [#1401](https://github.com/dhall-lang/dhall-haskell/pull/1401)+* Fixes and improvements to code formatting+    * [#1360](https://github.com/dhall-lang/dhall-haskell/pull/1360)+    * [#1372](https://github.com/dhall-lang/dhall-haskell/pull/1372)+    * [#1380](https://github.com/dhall-lang/dhall-haskell/pull/1380)+    * [#1415](https://github.com/dhall-lang/dhall-haskell/pull/1415)+ 1.26.1  * TECHNICALLY BREAKING CHANGES: [Simplify `⫽` within projection](https://github.com/dhall-lang/dhall-haskell/pull/1283) / [Simplify nested record projections](https://github.com/dhall-lang/dhall-haskell/pull/1307)@@ -40,6 +92,10 @@     * This fixes `dhall type` to more accurately follow the standard * [Initial changes for GHC 8.8 support](https://github.com/dhall-lang/dhall-haskell/pull/1324) * [Fix Haddock formatting for `dhallFromJSON`](https://github.com/dhall-lang/dhall-haskell/pull/1316)+* [Improved Windows caching support](https://github.com/dhall-lang/dhall-haskell/pull/1272)+    * `dhall` will now prefer the `%LOCALAPPDATA%` directory for caching if it is+      available+* [Warn about missing cache directories](https://github.com/dhall-lang/dhall-haskell/pull/1320)  1.26.0 @@ -104,7 +160,7 @@       newly-added utilities     * See also: [#1298](https://github.com/dhall-lang/dhall-haskell/pull/1298) * [New `:help` command for `dhall repl`](https://github.com/dhall-lang/dhall-haskell/pull/1237)-* [New `--no-cache` flag](https://github.com/dhall-lang/dhall-haskell/pull/1290)+* New `--no-cache` flag [#1290](https://github.com/dhall-lang/dhall-haskell/pull/1290) / [#1434](https://github.com/dhall-lang/dhall-haskell/pull/1434) / [#1436](https://github.com/dhall-lang/dhall-haskell/pull/1436)     * You can now disable use of the cache with this flag     * This comes in handy if you want to disable α-normalization for imports       protected by a semantic integrity check

@@ -1,7 +1,9 @@ {- Flip the value of a `Bool` -}-let not : Bool → Bool = λ(b : Bool) → b == False+let not+    : Bool → Bool+    = λ(b : Bool) → b == False  let example0 = assert : not True ≡ False 

@@ -2,7 +2,9 @@ Render a `Bool` as `Text` using the same representation as Dhall source code (i.e. beginning with a capital letter) -}-let show : Bool → Text = λ(b : Bool) → if b then "True" else "False"+let show+    : Bool → Text+    = λ(b : Bool) → if b then "True" else "False"  let example0 = assert : show True ≡ "True" 

@@ -2,7 +2,9 @@ Render a `Double` as `Text` using the same representation as Dhall source code (i.e. a decimal floating point number with a leading `-` sign if negative) -}-let show : Double → Text = Double/show+let show+    : Double → Text+    = Double/show  let example0 = assert : show -3.1 ≡ "-3.1" 

@@ -3,7 +3,9 @@ code (i.e. a decimal number with a leading `-` sign if negative and a leading `+` sign if non-negative) -}-let show : Integer → Text = Integer/show+let show+    : Integer → Text+    = Integer/show  let example0 = assert : show -3 ≡ "-3" 

@@ -1,7 +1,9 @@ {- Convert an `Integer` to the corresponding `Double` -}-let toDouble : Integer → Double = Integer/toDouble+let toDouble+    : Integer → Double+    = Integer/toDouble  let example0 = assert : toDouble -3 ≡ -3.0 

@@ -28,4 +28,8 @@ ```  -}-let Nesting : Type = < Inline | Nested : Text > in Nesting+let Nesting+    : Type+    = < Inline | Nested : Text >++in  Nesting

@@ -70,8 +70,7 @@         , nesting :               ./Nesting sha256:6284802edd41d5d725aa1ec7687e614e21ad1be7e14dd10996bfa9625105c335             ? ./Nesting-        , contents :-            a+        , contents : a         }  in  Tagged

@@ -57,18 +57,12 @@     : Type     =   ∀(JSON : Type)       → ∀ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → JSON

@@ -24,18 +24,12 @@     =   λ(x : List JSON)       → λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.array (List/map JSON@1 JSON (λ(j : JSON@1) → j JSON json) x)

@@ -19,18 +19,12 @@     =   λ(x : Bool)       → λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.bool x

@@ -1,14 +1,2 @@-{--Builds a key-value record such that a List of them will be converted to a-homogeneous record by dhall-to-json and dhall-to-yaml.--Both key and value are fixed to Text.-Take a look at `Record/keyValue` for a polymorphic version.--}-let keyText =-      λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }--let example0 =-      assert : keyText "foo" "bar" ≡ { mapKey = "foo", mapValue = "bar" }--in  keyText+  ../Map/keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc+? ../Map/keyText

@@ -1,17 +1,2 @@-{--Builds a key-value record such that a List of them will be converted to a-homogeneous record by dhall-to-json and dhall-to-yaml.--}-let keyValue =-        λ(v : Type)-      → λ(key : Text)-      → λ(value : v)-      → { mapKey = key, mapValue = value }--let example0 =-      assert : keyValue Natural "foo" 2 ≡ { mapKey = "foo", mapValue = 2 }--let example1 =-      assert : keyValue Text "bar" "baz" ≡ { mapKey = "bar", mapValue = "baz" }--in  keyValue+  ../Map/keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c+? ../Map/keyValue

@@ -14,18 +14,12 @@     : JSON     =   λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.null

@@ -19,18 +19,12 @@     =   λ(x : Double)       → λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.number x

@@ -30,18 +30,12 @@     =   λ(x : List { mapKey : Text, mapValue : JSON })       → λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.object

@@ -32,10 +32,8 @@     =   λ(j : JSON)       → j           Text-          { string =-              λ(x : Text) → Text/show x-          , number =-              λ(x : Double) → Double/show x+          { string = λ(x : Text) → Text/show x+          , number = λ(x : Double) → Double/show x           , object =                 λ(x : List { mapKey : Text, mapValue : Text })               → let body =@@ -53,10 +51,8 @@               → let body = Text/concatMapSep "," Text (λ(y : Text) → " ${y}") x                                  in  "[${body} ]"-          , bool =-              λ(x : Bool) → if x then "true" else "false"-          , null =-              "null"+          , bool = λ(x : Bool) → if x then "true" else "false"+          , null = "null"           }  in  render

@@ -19,18 +19,12 @@     =   λ(x : Text)       → λ(JSON : Type)       → λ ( json-          : { string :-                Text → JSON-            , number :-                Double → JSON-            , object :-                List { mapKey : Text, mapValue : JSON } → JSON-            , array :-                List JSON → JSON-            , bool :-                Bool → JSON-            , null :-                JSON+          : { string : Text → JSON+            , number : Double → JSON+            , object : List { mapKey : Text, mapValue : JSON } → JSON+            , array : List JSON → JSON+            , bool : Bool → JSON+            , null : JSON             }           )       → json.string x

@@ -0,0 +1,15 @@+{-+Unpack an `Optional` containing a `List`, defaulting to an empty list when the+`Optional` is `None`+-}+let default+    : ∀(a : Type) → Optional (List a) → List a+    =   λ(a : Type)+      → λ(o : Optional (List a))+      → Optional/fold (List a) o (List a) (λ(l : List a) → l) ([] : List a)++let example0 = assert : default Bool (None (List Bool)) ≡ ([] : List Bool)++let example1 = assert : default Bool (Some [ True ]) ≡ [ True ]++in  default

@@ -0,0 +1,10 @@+{-+An empty list of the given type+-}+let empty+    : ∀(a : Type) → List a+    = λ(a : Type) → [] : List a++let example0 = assert : empty Bool ≡ ([] : List Bool)++in  empty

@@ -1,7 +1,9 @@ {- Retrieve the first element of the list -}-let head : ∀(a : Type) → List a → Optional a = List/head+let head+    : ∀(a : Type) → List a → Optional a+    = List/head  let example0 = assert : head Natural [ 0, 1, 2 ] ≡ Some 0 

@@ -1,7 +1,9 @@ {- Retrieve the last element of the list -}-let last : ∀(a : Type) → List a → Optional a = List/last+let last+    : ∀(a : Type) → List a → Optional a+    = List/last  let example0 = assert : last Natural [ 0, 1, 2 ] ≡ Some 2 

@@ -1,7 +1,9 @@ {- Returns the number of elements in a list -}-let length : ∀(a : Type) → List a → Natural = List/length+let length+    : ∀(a : Type) → List a → Natural+    = List/length  let example0 = assert : length Natural [ 0, 1, 2 ] ≡ 3 

@@ -13,6 +13,12 @@ , concatMap =       ./concatMap sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64     ? ./concatMap+, default =+      ./default sha256:0ed2a04df6c1d55c08bcdbad82b30980af9ac40d2df7a1628f3663e3e8b4fe01+    ? ./default+, empty =+      ./empty sha256:b2f561f35098c457353723c93a22bd5de28d26ecc5370814bef9dfda421e0147+    ? ./empty , filter =       ./filter sha256:8ebfede5bbfe09675f246c33eb83964880ac615c4b1be8d856076fdbc4b26ba6     ? ./filter

@@ -1,7 +1,9 @@ {- Reverse a list -}-let reverse : ∀(a : Type) → List a → List a = List/reverse+let reverse+    : ∀(a : Type) → List a → List a+    = List/reverse  let example0 = assert : reverse Natural [ 0, 1, 2 ] ≡ [ 2, 1, 0 ] 

@@ -23,8 +23,7 @@                         → let length =                                 List/length { index : Natural, value : a } kvs                           -                          in  { count =-                                  y.count + length+                          in  { count = y.count + length                               , diff =                                     λ(n : Natural)                                   → List/fold@@ -36,10 +35,8 @@                                             )                                         → λ(z : list)                                         → let kvNew =-                                                { index =-                                                    kvOld.index + n-                                                , value =-                                                    kvOld.value+                                                { index = kvOld.index + n+                                                , value = kvOld.value                                                 }                                                                                      in  cons kvNew z

@@ -9,13 +9,10 @@       :   (   missing sha256:f428188ff9d77ea15bc2bcd0da3f8ed81b304e175b07ade42a3b0fb02941b2aa as Location             ? missing as Location           )-        ≡ < Environment :-              Text-          | Local :-              Text+        ≡ < Environment : Text+          | Local : Text           | Missing-          | Remote :-              Text+          | Remote : Text           >.Missing  in  Location

@@ -0,0 +1,15 @@+{-+An empty `Map` of the given key and value types+-}+let Map =+        ./Type sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed+      ? ./Type++let empty+    : ∀(k : Type) → ∀(v : Type) → Map k v+    = λ(k : Type) → λ(v : Type) → [] : Map k v++let example0 =+      assert : empty Text Bool ≡ ([] : List { mapKey : Text, mapValue : Bool })++in  empty

@@ -0,0 +1,15 @@+{-+Builds a key-value record such that a `List` of them will be converted to a+homogeneous record by dhall-to-json and dhall-to-yaml.++Both key and value are fixed to `Text`.++Take a look at `./keyValue` for a polymorphic version.+-}+let keyText =+      λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }++let example0 =+      assert : keyText "foo" "bar" ≡ { mapKey = "foo", mapValue = "bar" }++in  keyText

@@ -0,0 +1,17 @@+{-+Builds a key-value record such that a List of them will be converted to a+homogeneous record by dhall-to-json and dhall-to-yaml.+-}+let keyValue =+        λ(v : Type)+      → λ(key : Text)+      → λ(value : v)+      → { mapKey = key, mapValue = value }++let example0 =+      assert : keyValue Natural "foo" 2 ≡ { mapKey = "foo", mapValue = 2 }++let example1 =+      assert : keyValue Text "bar" "baz" ≡ { mapKey = "bar", mapValue = "baz" }++in  keyValue

@@ -4,6 +4,15 @@ , Entry =       ./Entry sha256:f334283bdd9cd88e6ea510ca914bc221fc2dab5fb424d24514b2e0df600d5346     ? ./Entry+, empty =+      ./empty sha256:4c612558b8bbe8f955550ed3fb295d57b1b864c85cd52615b52d0ee0e9682e52+    ? ./empty+, keyText =+      ./keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc+    ? ./keyText+, keyValue =+      ./keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c+    ? ./keyValue , keys =       ./keys sha256:d13ec34e6acf7c349d82272ef09a37c7bdf37f0dab489e9df47a1ff215d9f5e7     ? ./keys

@@ -36,4 +36,8 @@     : ./Monoid Text ``` -}-let Monoid : ∀(m : Type) → Type = λ(m : Type) → List m → m in Monoid+let Monoid+    : ∀(m : Type) → Type+    = λ(m : Type) → List m → m++in  Monoid

@@ -1,7 +1,9 @@ {- Returns `True` if a number if even and returns `False` otherwise -}-let even : Natural → Bool = Natural/even+let even+    : Natural → Bool+    = Natural/even  let example0 = assert : even 3 ≡ False 

@@ -1,7 +1,9 @@ {- Returns `True` if a number is `0` and returns `False` otherwise -}-let isZero : Natural → Bool = Natural/isZero+let isZero+    : Natural → Bool+    = Natural/isZero  let example0 = assert : isZero 2 ≡ False 

@@ -1,7 +1,9 @@ {- Returns `True` if a number is odd and returns `False` otherwise -}-let odd : Natural → Bool = Natural/odd+let odd+    : Natural → Bool+    = Natural/odd  let example0 = assert : odd 3 ≡ True 

@@ -2,7 +2,9 @@ Render a `Natural` number as `Text` using the same representation as Dhall source code (i.e. a decimal number) -}-let show : Natural → Text = Natural/show+let show+    : Natural → Text+    = Natural/show  let example0 = assert : show 3 ≡ "3" 

@@ -1,7 +1,9 @@ {- `subtract m n` computes `n - m`, truncating to `0` if `m > n` -}-let subtract : Natural → Natural → Natural = Natural/subtract+let subtract+    : Natural → Natural → Natural+    = Natural/subtract  let example0 = assert : subtract 1 2 ≡ 1 

@@ -1,7 +1,9 @@ {- Convert a `Natural` number to the corresponding `Integer` -}-let toInteger : Natural → Integer = Natural/toInteger+let toInteger+    : Natural → Integer+    = Natural/toInteger  let example0 = assert : toInteger 3 ≡ +3 

@@ -0,0 +1,15 @@+{-+Unpack an `Optional`, returning the default when it's `None`.+-}+let default+    : ∀(a : Type) → a → Optional a → a+    =   λ(a : Type)+      → λ(default : a)+      → λ(o : Optional a)+      → Optional/fold a o a (λ(x : a) → x) default++let example0 = assert : default Bool False (None Bool) ≡ False++let example1 = assert : default Bool False (Some True) ≡ True++in  default

@@ -10,6 +10,9 @@ , concat =       ./concat sha256:b49a3b7dc49eb83d150977caa5ae347be1cbbe14e3b6d0e07349bd2e5f707d69     ? ./concat+, default =+      ./default sha256:8f802473931b605422b545d7b81de20dbecb38f2ae63950c13f5381865a7f012+    ? ./default , filter =       ./filter sha256:b3d5e19a6cec592a76c12167a9e5e1e76649e776229d70a11c77b76cd29f617e     ? ./filter

@@ -18,8 +18,7 @@                 (   λ(x : a)                   → λ(status : Status)                   → merge-                      { Empty =-                          Status.NonEmpty (f x)+                      { Empty = Status.NonEmpty (f x)                       , NonEmpty =                             λ(result : Text)                           → Status.NonEmpty (f x ++ separator ++ result)

@@ -15,8 +15,7 @@                 (   λ(element : Text)                   → λ(status : Status)                   → merge-                      { Empty =-                          Status.NonEmpty element+                      { Empty = Status.NonEmpty element                       , NonEmpty =                             λ(result : Text)                           → Status.NonEmpty (element ++ separator ++ result)

@@ -2,7 +2,9 @@ Render a `Text` literal as its own representation as Dhall source code (i.e. a double-quoted string literal) -}-let show : Text → Text = Text/show+let show+    : Text → Text+    = Text/show  let example0 = assert : show "ABC" ≡ "\"ABC\"" 

@@ -48,15 +48,11 @@     : Type     =   ∀(XML : Type)       → ∀ ( xml-          : { text :-                Text → XML+          : { text : Text → XML             , element :-                  { attributes :-                      List { mapKey : Text, mapValue : Text }-                  , content :-                      List XML-                  , name :-                      Text+                  { attributes : List { mapKey : Text, mapValue : Text }+                  , content : List XML+                  , name : Text                   }                 → XML             }

@@ -28,12 +28,9 @@       ? ../List/map  let Args =-        { attributes :-            List { mapKey : Text, mapValue : Text }-        , name :-            Text-        , content :-            List XML+        { attributes : List { mapKey : Text, mapValue : Text }+        , name : Text+        , content : List XML         }       : Type @@ -42,26 +39,19 @@     =   λ(elem : Args)       → λ(XML : Type)       → λ ( xml-          : { text :-                Text → XML+          : { text : Text → XML             , element :-                  { attributes :-                      List { mapKey : Text, mapValue : Text }-                  , content :-                      List XML-                  , name :-                      Text+                  { attributes : List { mapKey : Text, mapValue : Text }+                  , content : List XML+                  , name : Text                   }                 → XML             }           )       → xml.element-          { attributes =-              elem.attributes-          , name =-              elem.name-          , content =-              List/map XML@1 XML (λ(x : XML@1) → x XML xml) elem.content+          { attributes = elem.attributes+          , name = elem.name+          , content = List/map XML@1 XML (λ(x : XML@1) → x XML xml) elem.content           }  in  element

@@ -21,10 +21,8 @@     :   { attributes : List { mapKey : Text, mapValue : Text }, name : Text }       → XML     =   λ ( elem-          : { attributes :-                List { mapKey : Text, mapValue : Text }-            , name :-                Text+          : { attributes : List { mapKey : Text, mapValue : Text }+            , name : Text             }           )       → element (elem ⫽ { content = [] : List XML })

@@ -43,16 +43,12 @@     =   λ(x : XML)       → x           Text-          { text =-              λ(d : Text) → d+          { text = λ(d : Text) → d           , element =                 λ ( elem-                  : { attributes :-                        List { mapKey : Text, mapValue : Text }-                    , content :-                        List Text-                    , name :-                        Text+                  : { attributes : List { mapKey : Text, mapValue : Text }+                    , content : List Text+                    , name : Text                     }                   )               → let attribs = Text/concatMap Attr renderAttr elem.attributes

@@ -23,15 +23,11 @@     =   λ(d : Text)       → λ(XML : Type)       → λ ( xml-          : { text :-                Text → XML+          : { text : Text → XML             , element :-                  { attributes :-                      List { mapKey : Text, mapValue : Text }-                  , content :-                      List XML-                  , name :-                      Text+                  { attributes : List { mapKey : Text, mapValue : Text }+                  , content : List XML+                  , name : Text                   }                 → XML             }

@@ -11,13 +11,13 @@       ./Integer/package.dhall sha256:eb464566d3192dd16ce915a9bd874aaaad612d5c69beb356e5b7d2e0c4949dcf     ? ./Integer/package.dhall , List =-      ./List/package.dhall sha256:108be3af5ebd465f7091039f2216c433e65ae5d25556a9a71786dd84d33ef49a+      ./List/package.dhall sha256:88ae09f29981480e62a39c925011b3246d716a80871440f071cf981efea1ad5e     ? ./List/package.dhall , Location =       ./Location/package.dhall sha256:0eb4e4a60814018009c720f6820aaa13cf9491eb1b09afb7b832039c6ee4d470     ? ./Location/package.dhall , Map =-      ./Map/package.dhall sha256:5e378b6da12f26b64f796f9c1b61d89bcc5a591f3a3dedcf85cb4637bbb8b618+      ./Map/package.dhall sha256:598e9c76103b2686fbbda6cc30078f9e60dd846d9eaf155d0149cf0ae06c21c5     ? ./Map/package.dhall , Monoid =       ./Monoid sha256:26fafa098600ef7a54ef9dba5ada416bbbdd21df1af306c052420c61553ad4af@@ -26,7 +26,7 @@       ./Natural/package.dhall sha256:4574df29e6bb82fd894c311f6c2ad9a22574756eb62f06d475aa8306d25006fc     ? ./Natural/package.dhall , Optional =-      ./Optional/package.dhall sha256:36a366af67a3c26cd5d196e095d3023f18953c5b5db3a03956fa554609e5442a+      ./Optional/package.dhall sha256:7608f2d38dabee8bfe6865b4adc11289059984220f422d2b023b15b3908f7a4c     ? ./Optional/package.dhall , JSON =       ./JSON/package.dhall sha256:0c3c40a63108f2e6ad59f23b789c18eb484d0e9aebc9416c5a4f338c6753084b

binary file changed (5 → 6 bytes)

binary file changed (absent → 11 bytes)

@@ -0,0 +1,1 @@+T::r

@@ -0,0 +1,3 @@+-- This file contains a free variable. This should be a type error, even if the variable+-- is in scope in the importing expression+x

@@ -0,0 +1,15 @@+{- This is a type error because the custom headers are type-checked with an+   empty context.  This is necessary because:++   * import resolution precedes β-normalization+   * we also don't want custom headers to leak program state anyway++   This should fail due to the `x` within the custom header being an unbound+   variable+-}++let x = "Bar"++in https://httpbin.org/headers+     using [ { mapKey = "Foo", mapValue = x } ]+     as Text

@@ -0,0 +1,1 @@+\(x: Bool) -> ../data/importBoundary.dhall

@@ -0,0 +1,10 @@+let Example =+      { Type = { name : Text, id : Optional Natural }+      , default = { name = "", id = None Natural }+      }++in  { example0 = Example::{=}+    , example1 = Example::{ name = "John Doe" }+    , example2 = Example::{ id = Some 0 }+    , example3 = Example::{ name = "Mary Jane", id = Some 0 }+    }

@@ -0,0 +1,5 @@+{ example0 = { id = None Natural, name = "" }+, example1 = { id = None Natural, name = "John Doe" }+, example2 = { id = Some 0, name = "" }+, example3 = { id = Some 0, name = "Mary Jane" }+}

@@ -0,0 +1,1 @@+{ default = {=}, Type = {} }::{=}

@@ -0,0 +1,1 @@+{=}

@@ -0,0 +1,1 @@+{ a : { b : { x : Bool } } } ⩓ { a : { b : { y : Bool } } }

@@ -0,0 +1,1 @@+{ a : { b : { x : Bool, y : Bool } } }

@@ -0,0 +1,1 @@+./foo sha256:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe1g

@@ -0,0 +1,10 @@+{ emptyRecordLiteral = { , = }+, emptyRecordType = { , }+, emptyList = [,] : List Natural+, emptyUnionType = < | >++, recordLiteral = { , x = 1, y = True }+, recordType = { , x : Natural, y : Bool }+, list = [ , 1, 2 ]+, unionType = < | x : Natural | y : Bool >+}

@@ -0,0 +1,1 @@+‚¨iemptyList‚gNaturalremptyRecordLiteral‚ oemptyRecordType‚ nemptyUnionType‚ dlist„ö‚‚mrecordLiteral‚¢ax‚ayõjrecordType‚¢axgNaturalaydBooliunionType‚¢axgNaturalaydBool

@@ -0,0 +1,3 @@+-- foo
+
+1

@@ -0,0 +1,1 @@+‚

@@ -0,0 +1,1 @@+"$"

@@ -0,0 +1,1 @@+‚a$

@@ -0,0 +1,1 @@+T::r

binary file changed (absent → 11 bytes)

@@ -0,0 +1,1 @@+-0.0

binary file changed (absent → 3 bytes)

@@ -1,2 +1,2 @@ -- Yes, this is legal-env:"\"\\\a\b\f\n\r\t\v"+env:"\"\\\a\b\f\n\r\t\v!<[~"

binary file changed (16 → 20 bytes)

@@ -0,0 +1,1 @@+https://200.249.250.255/index.dhall

binary file changed (absent → 36 bytes)

@@ -0,0 +1,1 @@+http://[AAAA:BBBB:CCCC:DDDD:EEEE:FFFF:0000::]/tutorial.dhall

binary file changed (absent → 63 bytes)

@@ -1,3 +0,0 @@--- This file contains a free variable. This should be a type error, even if the variable--- is in scope in the importing expression-x

@@ -1,15 +0,0 @@-{- This is a type error because the custom headers are type-checked with an-   empty context.  This is necessary because:--   * import resolution precedes β-normalization-   * we also don't want custom headers to leak program state anyway--   This should fail due to the `x` within the custom header being an unbound-   variable--}--let x = "Bar"--in https://httpbin.org/headers-     using [ { mapKey = "Foo", mapValue = x } ]-     as Text

@@ -1,1 +0,0 @@-\(x: Bool) -> ../data/importBoundary.dhall

@@ -1,23 +1,16 @@ { Bool :-    { and :-        ∀(xs : List Bool) → Bool+    { and : ∀(xs : List Bool) → Bool     , build :         ∀(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool-    , even :-        ∀(xs : List Bool) → Bool+    , even : ∀(xs : List Bool) → Bool     , fold :         ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool-    , not :-        ∀(b : Bool) → Bool-    , odd :-        ∀(xs : List Bool) → Bool-    , or :-        ∀(xs : List Bool) → Bool-    , show :-        ∀(b : Bool) → Text+    , not : ∀(b : Bool) → Bool+    , odd : ∀(xs : List Bool) → Bool+    , or : ∀(xs : List Bool) → Bool+    , show : ∀(b : Bool) → Text     }-, Double :-    { show : Double → Text }+, Double : { show : Double → Text } , Function :     { compose :           ∀(A : Type)@@ -28,32 +21,23 @@         → ∀(x : A)         → C     }-, Integer :-    { show : Integer → Text, toDouble : Integer → Double }+, Integer : { show : Integer → Text, toDouble : Integer → Double } , JSON :-    { Nesting :-        Type-    , Tagged :-        ∀(a : Type) → Type-    , Type :-        Type+    { Nesting : Type+    , Tagged : ∀(a : Type) → Type+    , Type : Type     , array :           ∀ ( x             : List                 (   ∀(JSON : Type)                   → ∀ ( json-                      : { array :-                            List JSON → JSON-                        , bool :-                            Bool → JSON-                        , null :-                            JSON-                        , number :-                            Double → JSON+                      : { array : List JSON → JSON+                        , bool : Bool → JSON+                        , null : JSON+                        , number : Double → JSON                         , object :                             List { mapKey : Text, mapValue : JSON } → JSON-                        , string :-                            Text → JSON+                        , string : Text → JSON                         }                       )                   → JSON@@ -61,18 +45,12 @@             )         → ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON@@ -80,18 +58,12 @@           ∀(x : Bool)         → ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON@@ -105,18 +77,12 @@     , null :           ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON@@ -124,41 +90,29 @@           ∀(x : Double)         → ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON     , object :           ∀ ( x             : List-                { mapKey :-                    Text+                { mapKey : Text                 , mapValue :                       ∀(JSON : Type)                     → ∀ ( json-                        : { array :-                              List JSON → JSON-                          , bool :-                              Bool → JSON-                          , null :-                              JSON-                          , number :-                              Double → JSON+                        : { array : List JSON → JSON+                          , bool : Bool → JSON+                          , null : JSON+                          , number : Double → JSON                           , object :                               List { mapKey : Text, mapValue : JSON } → JSON-                          , string :-                              Text → JSON+                          , string : Text → JSON                           }                         )                     → JSON@@ -166,18 +120,12 @@             )         → ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON@@ -185,18 +133,12 @@           ∀ ( j             :   ∀(JSON : Type)               → ∀ ( json-                  : { array :-                        List JSON → JSON-                    , bool :-                        Bool → JSON-                    , null :-                        JSON-                    , number :-                        Double → JSON-                    , object :-                        List { mapKey : Text, mapValue : JSON } → JSON-                    , string :-                        Text → JSON+                  : { array : List JSON → JSON+                    , bool : Bool → JSON+                    , null : JSON+                    , number : Double → JSON+                    , object : List { mapKey : Text, mapValue : JSON } → JSON+                    , string : Text → JSON                     }                   )               → JSON@@ -206,37 +148,29 @@           ∀(x : Text)         → ∀(JSON : Type)         → ∀ ( json-            : { array :-                  List JSON → JSON-              , bool :-                  Bool → JSON-              , null :-                  JSON-              , number :-                  Double → JSON-              , object :-                  List { mapKey : Text, mapValue : JSON } → JSON-              , string :-                  Text → JSON+            : { array : List JSON → JSON+              , bool : Bool → JSON+              , null : JSON+              , number : Double → JSON+              , object : List { mapKey : Text, mapValue : JSON } → JSON+              , string : Text → JSON               }             )         → JSON     } , List :-    { all :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool-    , any :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool+    { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool+    , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool     , build :           ∀(a : Type)         → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)         → List a-    , concat :-        ∀(a : Type) → ∀(xss : List (List a)) → List a+    , concat : ∀(a : Type) → ∀(xss : List (List a)) → List a     , concatMap :         ∀(a : Type) → ∀(b : Type) → ∀(f : a → List b) → ∀(xs : List a) → List b-    , filter :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a+    , default : ∀(a : Type) → ∀(o : Optional (List a)) → List a+    , empty : ∀(a : Type) → List a+    , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a     , fold :           ∀(a : Type)         → List a@@ -244,26 +178,16 @@         → ∀(cons : a → list → list)         → ∀(nil : list)         → list-    , generate :-        ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a-    , head :-        ∀(a : Type) → 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-    , length :-        ∀(a : Type) → List a → Natural-    , map :-        ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b-    , null :-        ∀(a : Type) → ∀(xs : List a) → Bool-    , replicate :-        ∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a-    , reverse :-        ∀(a : Type) → List a → List a+    , generate : ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a+    , head : ∀(a : Type) → 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+    , length : ∀(a : Type) → List a → Natural+    , map : ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b+    , null : ∀(a : Type) → ∀(xs : List a) → Bool+    , replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a+    , reverse : ∀(a : Type) → List a → List a     , shifted :           ∀(a : Type)         → ∀(kvss : List (List { index : Natural, value : a }))@@ -274,13 +198,18 @@         → ∀(xs : List { _1 : a, _2 : b })         → { _1 : List a, _2 : List b }     }-, Location :-    { Type : Type }+, Location : { Type : Type } , Map :-    { Entry :-        ∀(k : Type) → ∀(v : Type) → Type-    , Type :-        ∀(k : Type) → ∀(v : Type) → Type+    { Entry : ∀(k : Type) → ∀(v : Type) → Type+    , Type : ∀(k : Type) → ∀(v : Type) → Type+    , empty : ∀(k : Type) → ∀(v : Type) → List { mapKey : k, mapValue : v }+    , keyText :+        ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }+    , keyValue :+          ∀(v : Type)+        → ∀(key : Text)+        → ∀(value : v)+        → { mapKey : Text, mapValue : v }     , keys :           ∀(k : Type)         → ∀(v : Type)@@ -299,8 +228,7 @@         → ∀(xs : List { mapKey : k, mapValue : v })         → List v     }-, Monoid :-    ∀(m : Type) → Type+, Monoid : ∀(m : Type) → Type , Natural :     { build :           (   ∀(natural : Type)@@ -309,48 +237,31 @@             → natural           )         → Natural-    , enumerate :-        ∀(n : Natural) → List Natural-    , equal :-        ∀(a : Natural) → ∀(b : Natural) → Bool-    , even :-        Natural → Bool+    , enumerate : ∀(n : Natural) → List Natural+    , equal : ∀(a : Natural) → ∀(b : Natural) → Bool+    , even : Natural → Bool     , fold :           Natural         → ∀(natural : Type)         → ∀(succ : natural → natural)         → ∀(zero : natural)         → natural-    , greaterThan :-        ∀(x : Natural) → ∀(y : Natural) → Bool-    , greaterThanEqual :-        ∀(x : Natural) → ∀(y : Natural) → Bool-    , isZero :-        Natural → Bool-    , lessThan :-        ∀(x : Natural) → ∀(y : Natural) → Bool-    , lessThanEqual :-        ∀(x : Natural) → ∀(y : Natural) → Bool-    , odd :-        Natural → Bool-    , product :-        ∀(xs : List Natural) → Natural-    , show :-        Natural → Text-    , subtract :-        Natural → Natural → Natural-    , sum :-        ∀(xs : List Natural) → Natural-    , toDouble :-        ∀(n : Natural) → Double-    , toInteger :-        Natural → Integer+    , greaterThan : ∀(x : Natural) → ∀(y : Natural) → Bool+    , greaterThanEqual : ∀(x : Natural) → ∀(y : Natural) → Bool+    , isZero : Natural → Bool+    , lessThan : ∀(x : Natural) → ∀(y : Natural) → Bool+    , lessThanEqual : ∀(x : Natural) → ∀(y : Natural) → Bool+    , odd : Natural → Bool+    , product : ∀(xs : List Natural) → Natural+    , show : Natural → Text+    , subtract : Natural → Natural → Natural+    , sum : ∀(xs : List Natural) → Natural+    , toDouble : ∀(n : Natural) → Double+    , toInteger : Natural → Integer     } , Optional :-    { all :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool-    , any :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool+    { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool+    , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool     , build :           ∀(a : Type)         → (   ∀(optional : Type)@@ -359,10 +270,9 @@             → optional           )         → Optional a-    , concat :-        ∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a-    , filter :-        ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a+    , concat : ∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a+    , default : ∀(a : Type) → ∀(default : a) → ∀(o : Optional a) → a+    , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a     , fold :           ∀(a : Type)         → Optional a@@ -370,22 +280,17 @@         → ∀(just : a → optional)         → ∀(nothing : optional)         → optional-    , head :-        ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a-    , last :-        ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a-    , length :-        ∀(a : Type) → ∀(xs : Optional a) → Natural+    , head : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a+    , last : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a+    , length : ∀(a : Type) → ∀(xs : Optional a) → Natural     , map :           ∀(a : Type)         → ∀(b : Type)         → ∀(f : a → b)         → ∀(o : Optional a)         → Optional b-    , null :-        ∀(a : Type) → ∀(xs : Optional a) → Bool-    , toList :-        ∀(a : Type) → ∀(o : Optional a) → List a+    , null : ∀(a : Type) → ∀(xs : Optional a) → Bool+    , toList : ∀(a : Type) → ∀(o : Optional a) → List a     , unzip :           ∀(a : Type)         → ∀(b : Type)@@ -393,34 +298,26 @@         → { _1 : Optional a, _2 : Optional b }     } , Text :-    { concat :-        ∀(xs : List Text) → Text-    , concatMap :-        ∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text+    { concat : ∀(xs : List Text) → Text+    , concatMap : ∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text     , concatMapSep :           ∀(separator : Text)         → ∀(a : Type)         → ∀(f : a → Text)         → ∀(elements : List a)         → Text-    , concatSep :-        ∀(separator : Text) → ∀(elements : List Text) → Text-    , default :-        ∀(o : Optional Text) → Text-    , defaultMap :-        ∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text-    , show :-        Text → Text+    , concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text+    , default : ∀(o : Optional Text) → Text+    , defaultMap : ∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text+    , show : Text → Text     } , XML :-    { Type :-        Type+    { Type : Type     , attribute :         ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }     , element :           ∀ ( elem-            : { attributes :-                  List { mapKey : Text, mapValue : Text }+            : { attributes : List { mapKey : Text, mapValue : Text }               , content :                   List                     (   ∀(XML : Type)@@ -428,61 +325,46 @@                           : { element :                                   { attributes :                                       List { mapKey : Text, mapValue : Text }-                                  , content :-                                      List XML-                                  , name :-                                      Text+                                  , content : List XML+                                  , name : Text                                   }                                 → XML-                            , text :-                                Text → XML+                            , text : Text → XML                             }                           )                       → XML                     )-              , name :-                  Text+              , name : Text               }             )         → ∀(XML : Type)         → ∀ ( xml             : { element :-                    { attributes :-                        List { mapKey : Text, mapValue : Text }-                    , content :-                        List XML-                    , name :-                        Text+                    { attributes : List { mapKey : Text, mapValue : Text }+                    , content : List XML+                    , name : Text                     }                   → XML-              , text :-                  Text → XML+              , text : Text → XML               }             )         → XML-    , emptyAttributes :-        List { mapKey : Text, mapValue : Text }+    , emptyAttributes : List { mapKey : Text, mapValue : Text }     , leaf :           ∀ ( elem-            : { attributes :-                  List { mapKey : Text, mapValue : Text }-              , name :-                  Text+            : { attributes : List { mapKey : Text, mapValue : Text }+              , name : Text               }             )         → ∀(XML : Type)         → ∀ ( xml             : { element :-                    { attributes :-                        List { mapKey : Text, mapValue : Text }-                    , content :-                        List XML-                    , name :-                        Text+                    { attributes : List { mapKey : Text, mapValue : Text }+                    , content : List XML+                    , name : Text                     }                   → XML-              , text :-                  Text → XML+              , text : Text → XML               }             )         → XML@@ -491,16 +373,12 @@             :   ∀(XML : Type)               → ∀ ( xml                   : { element :-                          { attributes :-                              List { mapKey : Text, mapValue : Text }-                          , content :-                              List XML-                          , name :-                              Text+                          { attributes : List { mapKey : Text, mapValue : Text }+                          , content : List XML+                          , name : Text                           }                         → XML-                    , text :-                        Text → XML+                    , text : Text → XML                     }                   )               → XML@@ -511,16 +389,12 @@         → ∀(XML : Type)         → ∀ ( xml             : { element :-                    { attributes :-                        List { mapKey : Text, mapValue : Text }-                    , content :-                        List XML-                    , name :-                        Text+                    { attributes : List { mapKey : Text, mapValue : Text }+                    , content : List XML+                    , name : Text                     }                   → XML-              , text :-                  Text → XML+              , text : Text → XML               }             )         → XML

@@ -0,0 +1,25 @@+let Example =+      { Type = { name : Text, id : Optional Natural }+      , default = { name = "", id = None Natural }+      }++let ExtraFields = Example ∧ { extra = {=} }++let RequiredFields =+        { Type = { name : Text, id : Optional Natural }+        , default = { id = None Natural }+        }++let WrongDefaultType =+        { Type = { name : Text, id : Optional Natural }+        , default = { id = True }+        }++in  { example0 = Example::{=}+    , example1 = Example::{ name = "John Doe" }+    , example2 = Example::{ id = Some 0 }+    , example3 = Example::{ name = "Mary Jane", id = Some 0 }+    , example4 = ExtraFields::{=}+    , example5 = RequiredFields::{ name = "Jane Smith" }+    , example6 = WrongDefaultType::{ name = "Bob Roberts", id = Some 0 }+    }

@@ -0,0 +1,8 @@+{ example0 : { id : Optional Natural, name : Text }+, example1 : { id : Optional Natural, name : Text }+, example2 : { id : Optional Natural, name : Text }+, example3 : { id : Optional Natural, name : Text }+, example4 : { id : Optional Natural, name : Text }+, example5 : { id : Optional Natural, name : Text }+, example6 : { id : Optional Natural, name : Text }+}

@@ -0,0 +1,15 @@+{- This test caught a regression in the Haskell implementation's typechecker.++   The typechecker was not sorting the fields of a record type inferred from a+   projection, meaning that it inferred that the fully normalized type of+   the subexpression `{ bar = "", foo = "" }.{ foo, bar }` was+   `{ foo : Text, bar : Text }` when according to the standard the inferred type+   should have been `{ bar : Text, foo : Text }`.  On top of that the Haskell+   implementation was sensitive to field order, leading to a type mismatch+   when applying a function whose input type had the fields sorted.++   This test ensures that implementations correctly handle order-insensitivity+   when projecting fields and/or comparing types, just in case they are+   order-sensitive like the Haskell implementation.+-}+λ(f : { bar : Text, foo : Text } → Bool) → f { bar = "", foo = "" }.{ foo, bar }

@@ -0,0 +1,1 @@+∀(f : { bar : Text, foo : Text } → Bool) → Bool

@@ -0,0 +1,3 @@+toMap+  { x = Bool }.{}+: List { mapKey : { t = Text }.t, mapValue : { t = Double }.t }

@@ -0,0 +1,1 @@+List { mapKey : Text, mapValue : Double }

@@ -0,0 +1,1 @@+{ default = {=}, Type = {} }::{=}

@@ -0,0 +1,1 @@+{}

@@ -0,0 +1,1 @@+List/length (let x = 0 in Bool)

@@ -0,0 +1,1 @@+List Bool → Natural

@@ -0,0 +1,1 @@+(λ(g : Natural → Bool) → assert : g 0 ≡ g 0) Natural/even

@@ -0,0 +1,1 @@+True ≡ True

@@ -0,0 +1,1 @@+λ(x : { t = Bool }.t) → x

@@ -0,0 +1,1 @@+∀(x : Bool) → Bool

@@ -0,0 +1,1 @@+merge { x = λ(_ : Bool) → _ } (< x : Bool >.x True) : Bool

@@ -0,0 +1,1 @@+Bool

@@ -0,0 +1,1 @@+merge { x = λ(y : Bool) → y } < x >.x : (Bool → Bool)

@@ -0,0 +1,1 @@+∀(y : Bool) → Bool

@@ -1,1 +0,0 @@-merge { x = λ(_ : Bool) → _ } (< x : Bool >.x True) : Bool

@@ -1,1 +0,0 @@-Bool

@@ -0,0 +1,1 @@+{ a : { b : { x : Bool } } } ⩓ { a : { b : { y : Bool } } }

@@ -0,0 +1,1 @@+Type

@@ -0,0 +1,1 @@+toMap { x = λ(x : Bool) → x } : List { mapKey : Text, mapValue : Bool → Bool }

@@ -0,0 +1,1 @@+List { mapKey : Text, mapValue : ∀(x : Bool) → Bool }

@@ -0,0 +1,1 @@+(λ(x : Bool) → x) : Bool → Bool

@@ -0,0 +1,1 @@+∀(x : Bool) → Bool

@@ -0,0 +1,1 @@+True : { x = Bool }.x

@@ -0,0 +1,1 @@+Bool

@@ -1,5 +1,5 @@ Name: dhall-Version: 1.26.1+Version: 1.27.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 7.10.3, GHC == 8.4.3, GHC == 8.6.1@@ -61,6 +61,8 @@     dhall-lang/Prelude/List/build     dhall-lang/Prelude/List/concat     dhall-lang/Prelude/List/concatMap+    dhall-lang/Prelude/List/default+    dhall-lang/Prelude/List/empty     dhall-lang/Prelude/List/filter     dhall-lang/Prelude/List/fold     dhall-lang/Prelude/List/generate@@ -79,7 +81,10 @@     dhall-lang/Prelude/Location/package.dhall     dhall-lang/Prelude/Location/Type     dhall-lang/Prelude/Map/Entry+    dhall-lang/Prelude/Map/empty     dhall-lang/Prelude/Map/keys+    dhall-lang/Prelude/Map/keyText+    dhall-lang/Prelude/Map/keyValue     dhall-lang/Prelude/Map/map     dhall-lang/Prelude/Map/package.dhall     dhall-lang/Prelude/Map/Type@@ -107,6 +112,7 @@     dhall-lang/Prelude/Optional/any     dhall-lang/Prelude/Optional/build     dhall-lang/Prelude/Optional/concat+    dhall-lang/Prelude/Optional/default     dhall-lang/Prelude/Optional/filter     dhall-lang/Prelude/Optional/fold     dhall-lang/Prelude/Optional/head@@ -295,7 +301,6 @@     dhall-lang/tests/semantic-hash/success/simple/*.hash     dhall-lang/tests/semantic-hash/success/simplifications/*.dhall     dhall-lang/tests/semantic-hash/success/simplifications/*.hash-    dhall-lang/tests/type-inference/data/*.dhall     dhall-lang/tests/type-inference/failure/*.dhall     dhall-lang/tests/type-inference/success/*.dhall     dhall-lang/tests/type-inference/success/prelude/Bool/and/*.dhall@@ -366,6 +371,8 @@     tests/diff/*.txt     tests/recursive/*.dhall     tests/regression/*.dhall+    tests/tags/*.dhall+    tests/tags/*.tags     tests/tutorial/*.dhall  Source-Repository head@@ -404,6 +411,7 @@         exceptions                  >= 0.8.3    && < 0.11,         filepath                    >= 1.4      && < 1.5 ,         haskeline                   >= 0.7.2.1  && < 0.8 ,+        hashable                    >= 1.2      && < 1.3 ,         lens-family-core            >= 1.0.0    && < 2.1 ,         megaparsec                  >= 6.5.0    && < 7.1 ,         memory                      >= 0.14     && < 0.16,@@ -482,9 +490,9 @@         Dhall.Core,         Dhall.Crypto,         Dhall.Diff,+        Dhall.Tags,         Dhall.Format,         Dhall.Freeze,-        Dhall.Hash,         Dhall.Import,         Dhall.Lint,         Dhall.Main,@@ -509,6 +517,7 @@         Dhall.Parser.Combinators,         Dhall.URL,         Dhall.Import.Types,+        Dhall.Syntax,         Dhall.Eval,         Paths_dhall     Autogen-Modules:@@ -535,6 +544,7 @@     Other-Modules:         Dhall.Test.Dhall         Dhall.Test.Diff+        Dhall.Test.Tags         Dhall.Test.Format         Dhall.Test.Import         Dhall.Test.Lint@@ -555,6 +565,7 @@         deepseq                   >= 1.2.0.1  && < 1.5 ,         dhall                                          ,         directory                                      ,+        either                                         ,         filepath                                       ,         foldl                                    < 1.5 ,         generic-random            >= 1.3.0.0  && < 1.4 ,@@ -566,6 +577,7 @@         scientific                                     ,         semigroups                                     ,         serialise                                      ,+        special-values                           < 0.2 ,         spoon                                    < 0.4 ,         tasty                     >= 0.11.2   && < 1.3 ,         tasty-expected-failure                   < 0.12,@@ -574,6 +586,7 @@         text                      >= 0.11.1.0 && < 1.3 ,         transformers                                   ,         turtle                                   < 1.6 ,+        unordered-containers                           ,         vector                    >= 0.11.0.0 && < 0.13     if flag(with-http)       CPP-Options:

@@ -17,7 +17,7 @@     prefix <- System.Directory.makeAbsolute pwd      Test.Mockery.Directory.inTempDirectory $ do-        writeFile "makeBools" "λ(n : Bool) → [ n && True, n && False, n || True, n || False ]"+        writeFile "makeBools.dhall" "λ(n : Bool) → [ n && True, n && False, n || True, n || False ]"         writeFile "bool1" "True"         writeFile "bool2" "False"         writeFile "both" "./bool1 && ./bool2"@@ -32,4 +32,5 @@             , prefix </> "src/Dhall.hs"             , prefix </> "src/Dhall/Import.hs"             , prefix </> "src/Dhall/Tutorial.hs"+            , prefix </> "src/Dhall/Tags.hs"             ]

@@ -1,6 +1,10 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-| This module provides implementations of cryptographic utilities that only+    work for GHC (as opposed to GHCJS)+-}+ module Dhall.Crypto (       SHA256Digest(..)     , sha256DigestFromByteString@@ -17,17 +21,22 @@ import qualified Crypto.Hash import qualified Data.ByteString.Char8 as ByteString.Char8 +-- | A SHA256 digest newtype SHA256Digest = SHA256Digest { unSHA256Digest :: ByteString }   deriving (Eq, Generic, Ord, NFData, ByteArrayAccess)  instance Show SHA256Digest where   show (SHA256Digest bytes) = ByteString.Char8.unpack $ convertToBase Base16 bytes +{-| Attempt to interpret a `ByteString` as a `SHA256Digest`, returning+    `Nothing` if the conversion fails+-} sha256DigestFromByteString :: ByteString -> Maybe SHA256Digest sha256DigestFromByteString bytes = SHA256Digest . convert <$> mh   where     mh = Crypto.Hash.digestFromByteString bytes :: Maybe (Crypto.Hash.Digest SHA256) +-- | Hash a `ByteString` and return the hash as a `SHA256Digest` sha256Hash :: ByteString -> SHA256Digest sha256Hash bytes = SHA256Digest $ convert h   where

@@ -2,6 +2,10 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE JavaScriptFFI #-} +{-| This module provides implementations of cryptographic utilities that only+    work for GHCJS+-}+ module Dhall.Crypto (       SHA256Digest(..)     , sha256DigestFromByteString@@ -20,12 +24,16 @@ import qualified Data.ByteString.Char8  as ByteString.Char8 import qualified GHCJS.Buffer           as Buffer +-- | A SHA256 digest newtype SHA256Digest = SHA256Digest { unSHA256Digest :: ByteString }   deriving (Eq, Generic, Ord, NFData, ByteArrayAccess)  instance Show SHA256Digest where   show (SHA256Digest bytes) = ByteString.Char8.unpack $ convertToBase Base16 bytes +{-| Attempt to interpret a `ByteString` as a `SHA256Digest`, returning+    `Nothing` if the conversion fails+-} sha256DigestFromByteString :: ByteString -> Maybe SHA256Digest sha256DigestFromByteString bytes   | ByteString.length bytes == 32 = Just $ SHA256Digest bytes@@ -55,6 +63,7 @@ arrayBufferToByteString =   Buffer.toByteString 0 Nothing . Buffer.createFromArrayBuffer +-- | Hash a `ByteString` and return the hash as a `SHA256Digest` sha256Hash :: ByteString -> SHA256Digest sha256Hash bytes   | ByteString.length out == 32 = SHA256Digest out

@@ -46,7 +46,8 @@     , RecordType(..)     , UnionType(..)     , InputType(..)-    , Interpret(..)+    , FromDhall(..)+    , Interpret     , InvalidType(..)     , ExtractErrors(..)     , Extractor@@ -71,19 +72,28 @@     , sequence     , list     , vector+    , setFromDistinctList+    , setIgnoringDuplicates+    , hashSetFromDistinctList+    , hashSetIgnoringDuplicates+    , Dhall.map+    , hashMap+    , pairFromMapEntry     , unit+    , void     , string     , pair     , record     , field     , union     , constructor-    , GenericInterpret(..)-    , GenericInject(..)+    , GenericFromDhall(..)+    , GenericToDhall(..) -    , Inject(..)+    , ToDhall(..)+    , Inject     , inject-    , genericInject+    , genericToDhall     , RecordInputType(..)     , inputFieldWith     , inputField@@ -116,7 +126,10 @@ import Data.Fix (Fix(..)) import Data.Functor.Contravariant (Contravariant(..), (>$<), Op(..)) import Data.Functor.Contravariant.Divisible (Divisible(..), divided)+import Data.Hashable (Hashable) import Data.List.NonEmpty (NonEmpty (..))+import Data.HashMap.Strict (HashMap)+import Data.Map (Map) import Data.Monoid ((<>)) import Data.Scientific (Scientific) import Data.Semigroup (Semigroup)@@ -125,13 +138,14 @@ import Data.Text.Prettyprint.Doc (Pretty) import Data.Typeable (Typeable) import Data.Vector (Vector)+import Data.Void (Void) import Data.Word (Word8, Word16, Word32, Word64)-import Dhall.Core (Expr(..), Chunks(..))+import Dhall.Core (Expr(..), Chunks(..), DhallDouble(..)) import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..))-import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)+import Dhall.TypeCheck (DetailedTypeError(..), TypeError) import GHC.Generics-import Lens.Family (LensLike', set, view)+import Lens.Family (LensLike', view) import Numeric.Natural (Natural) import Prelude hiding (maybe, sequence) import System.FilePath (takeDirectory)@@ -142,16 +156,21 @@ import qualified Data.Foldable import qualified Data.Functor.Compose import qualified Data.Functor.Product+import qualified Data.HashMap.Strict as HashMap+import qualified Data.Map import qualified Data.Maybe+import qualified Data.List import qualified Data.List.NonEmpty import qualified Data.Semigroup import qualified Data.Scientific import qualified Data.Sequence import qualified Data.Set+import qualified Data.HashSet import qualified Data.Text import qualified Data.Text.IO import qualified Data.Text.Lazy import qualified Data.Vector+import qualified Data.Void import qualified Dhall.Context import qualified Dhall.Core import qualified Dhall.Import@@ -160,18 +179,32 @@ import qualified Dhall.Pretty.Internal import qualified Dhall.TypeCheck import qualified Dhall.Util+import qualified Lens.Family  -- $setup -- >>> :set -XOverloadedStrings -- >>> :set -XRecordWildCards+-- >>> import Data.Word (Word8, Word16, Word32, Word64)+-- >>> import Dhall.Pretty.Internal (prettyExpr) +{-| Useful synonym for the `Validation` type used when marshalling Dhall+    expressions+-} type Extractor s a = Validation (ExtractErrors s a)-type MonadicExtractor s a = Either (ExtractErrors s a) +{-| Useful synonym for the equivalent `Either` type used when marshalling Dhall+    code+-}+type MonadicExtractor s a = Either (ExtractErrors s a) +{-| Generate a type error during extraction by specifying the expected type+    and the actual type+-} typeError :: Expr s a -> Expr s a -> Extractor s a b-typeError expected actual = Failure . ExtractErrors . pure . TypeMismatch $ InvalidType expected actual+typeError expected actual =+    Failure . ExtractErrors . pure . TypeMismatch $ InvalidType expected actual +-- | Turn a `Text` message into an extraction failure extractError :: Text -> Extractor s a b extractError = Failure . ExtractErrors . pure . ExtractError @@ -185,6 +218,9 @@ fromMonadic :: MonadicExtractor s a b -> Extractor s a b fromMonadic = eitherToValidation +{-| One or more errors returned from extracting a Dhall expression to a+    Haskell expression+-} newtype ExtractErrors s a = ExtractErrors    { getErrors :: NonEmpty (ExtractError s a)    } deriving Semigroup@@ -298,8 +334,8 @@  -- | @since 1.16 data EvaluateSettings = EvaluateSettings-  { _startingContext :: Dhall.Context.Context (Expr Src X)-  , _normalizer      :: Maybe (Dhall.Core.ReifiedNormalizer X)+  { _startingContext :: Dhall.Context.Context (Expr Src Void)+  , _normalizer      :: Maybe (Dhall.Core.ReifiedNormalizer Void)   }  -- | Default evaluation settings: no extra entries in the initial@@ -317,11 +353,11 @@ -- @since 1.16 startingContext   :: (Functor f, HasEvaluateSettings s)-  => LensLike' f s (Dhall.Context.Context (Expr Src X))+  => LensLike' f s (Dhall.Context.Context (Expr Src Void)) startingContext = evaluateSettings . l   where     l :: (Functor f)-      => LensLike' f EvaluateSettings (Dhall.Context.Context (Expr Src X))+      => LensLike' f EvaluateSettings (Dhall.Context.Context (Expr Src Void))     l k s = fmap (\x -> s { _startingContext = x}) (k (_startingContext s))  -- | Access the custom normalizer.@@ -329,11 +365,11 @@ -- @since 1.16 normalizer   :: (Functor f, HasEvaluateSettings s)-  => LensLike' f s (Maybe (Dhall.Core.ReifiedNormalizer X))+  => LensLike' f s (Maybe (Dhall.Core.ReifiedNormalizer Void)) normalizer = evaluateSettings . l   where     l :: (Functor f)-      => LensLike' f EvaluateSettings (Maybe (Dhall.Core.ReifiedNormalizer X))+      => LensLike' f EvaluateSettings (Maybe (Dhall.Core.ReifiedNormalizer Void))     l k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s))  -- | @since 1.16@@ -398,8 +434,8 @@     let EvaluateSettings {..} = _evaluateSettings      let transform =-               set Dhall.Import.normalizer      _normalizer-            .  set Dhall.Import.startingContext _startingContext+               Lens.Family.set Dhall.Import.normalizer      _normalizer+            .  Lens.Family.set Dhall.Import.startingContext _startingContext      let status = transform (Dhall.Import.emptyStatus _rootDirectory) @@ -467,7 +503,7 @@ inputExpr     :: Text     -- ^ The Dhall program-    -> IO (Expr Src X)+    -> IO (Expr Src Void)     -- ^ The fully normalized AST inputExpr =   inputExprWithSettings defaultInputSettings@@ -482,7 +518,7 @@     :: InputSettings     -> Text     -- ^ The Dhall program-    -> IO (Expr Src X)+    -> IO (Expr Src Void)     -- ^ The fully normalized AST inputExprWithSettings settings txt = do     expr  <- Dhall.Core.throws (Dhall.Parser.exprFromText (view sourceName settings) txt)@@ -492,8 +528,8 @@     let EvaluateSettings {..} = _evaluateSettings      let transform =-               set Dhall.Import.normalizer      _normalizer-            .  set Dhall.Import.startingContext _startingContext+               Lens.Family.set Dhall.Import.normalizer      _normalizer+            .  Lens.Family.set Dhall.Import.startingContext _startingContext      let status = transform (Dhall.Import.emptyStatus _rootDirectory) @@ -512,7 +548,7 @@     :: Alternative f     => Type a     -- ^ The type of value to decode from Dhall to Haskell-    -> Expr s X+    -> Expr s Void     -- ^ a closed form Dhall program, which evaluates to the expected type     -> f a     -- ^ The decoded value in Haskell@@ -629,11 +665,11 @@ detailed =     Control.Exception.handle handler1 . Control.Exception.handle handler0   where-    handler0 :: Imported (TypeError Src X) -> IO a+    handler0 :: Imported (TypeError Src Void) -> IO a     handler0 (Imported ps e) =         Control.Exception.throwIO (Imported ps (DetailedTypeError e)) -    handler1 :: TypeError Src X -> IO a+    handler1 :: TypeError Src Void -> IO a     handler1 e = Control.Exception.throwIO (DetailedTypeError e)  {-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall@@ -654,9 +690,9 @@ > input :: Type a -> Text -> IO a -} data Type a = Type-    { extract  :: Expr Src X -> Extractor Src X a+    { extract  :: Expr Src Void -> Extractor Src Void a     -- ^ Extracts Haskell value from the Dhall expression-    , expected :: Expr Src X+    , expected :: Expr Src Void     -- ^ Dhall type of the Haskell value     }     deriving (Functor)@@ -716,8 +752,8 @@ double :: Type Double double = Type {..}   where-    extract (DoubleLit n) = pure n-    extract  expr            = typeError Double expr+    extract (DoubleLit (DhallDouble n)) = pure n+    extract  expr                       = typeError Double expr      expected = Double @@ -727,12 +763,7 @@ "Test" -} lazyText :: Type Data.Text.Lazy.Text-lazyText = Type {..}-  where-    extract (TextLit (Chunks [] t)) = pure (Data.Text.Lazy.fromStrict t)-    extract  expr = typeError Text expr--    expected = Text+lazyText = fmap Data.Text.Lazy.fromStrict strictText  {-| Decode strict `Text` @@ -740,8 +771,12 @@ "Test" -} strictText :: Type Text-strictText = fmap Data.Text.Lazy.toStrict lazyText+strictText = Type {..}+  where+    extract (TextLit (Chunks [] t)) = pure t+    extract  expr = typeError Text expr +    expected = Text {-| Decode a `Maybe`  >>> input (maybe natural) "Some 1"@@ -785,6 +820,176 @@ vector :: Type a -> Type (Vector a) vector = fmap Data.Vector.fromList . list +{-| Decode a `Set` from a `List`++>>> input (setIgnoringDuplicates natural) "[1, 2, 3]"+fromList [1,2,3]++Duplicate elements are ignored.++>>> input (setIgnoringDuplicates natural) "[1, 1, 3]"+fromList [1,3]++-}+setIgnoringDuplicates :: (Ord a) => Type a -> Type (Data.Set.Set a)+setIgnoringDuplicates = fmap Data.Set.fromList . list++{-| Decode a `HashSet` from a `List`++>>> input (hashSetIgnoringDuplicates natural) "[1, 2, 3]"+fromList [1,2,3]++Duplicate elements are ignored.++>>> input (hashSetIgnoringDuplicates natural) "[1, 1, 3]"+fromList [1,3]++-}+hashSetIgnoringDuplicates :: (Hashable a, Ord a)+                          => Type a+                          -> Type (Data.HashSet.HashSet a)+hashSetIgnoringDuplicates = fmap Data.HashSet.fromList . list++{-| Decode a `Set` from a `List` with distinct elements++>>> input (setFromDistinctList natural) "[1, 2, 3]"+fromList [1,2,3]++An error is thrown if the list contains duplicates.++> >>> input (setFromDistinctList natural) "[1, 1, 3]"+> *** Exception: Error: Failed extraction+>+> The expression type-checked successfully but the transformation to the target+> type failed with the following error:+>+> One duplicate element in the list: 1+>++> >>> input (setFromDistinctList natural) "[1, 1, 3, 3]"+> *** Exception: Error: Failed extraction+>+> The expression type-checked successfully but the transformation to the target+> type failed with the following error:+>+> 2 duplicates were found in the list, including 1+>++-}+setFromDistinctList :: (Ord a, Show a) => Type a -> Type (Data.Set.Set a)+setFromDistinctList = setHelper Data.Set.size Data.Set.fromList++{-| Decode a `HashSet` from a `List` with distinct elements++>>> input (hashSetFromDistinctList natural) "[1, 2, 3]"+fromList [1,2,3]++An error is thrown if the list contains duplicates.++> >>> input (hashSetFromDistinctList natural) "[1, 1, 3]"+> *** Exception: Error: Failed extraction+>+> The expression type-checked successfully but the transformation to the target+> type failed with the following error:+>+> One duplicate element in the list: 1+>++> >>> input (hashSetFromDistinctList natural) "[1, 1, 3, 3]"+> *** Exception: Error: Failed extraction+>+> The expression type-checked successfully but the transformation to the target+> type failed with the following error:+>+> 2 duplicates were found in the list, including 1+>++-}+hashSetFromDistinctList :: (Hashable a, Ord a, Show a)+                        => Type a+                        -> Type (Data.HashSet.HashSet a)+hashSetFromDistinctList = setHelper Data.HashSet.size Data.HashSet.fromList+++setHelper :: (Eq a, Foldable t, Show a)+          => (t a -> Int)+          -> ([a] -> t a)+          -> Type a+          -> Type (t a)+setHelper size toSet (Type extractIn expectedIn) = Type extractOut expectedOut+  where+    extractOut (ListLit _ es) = case traverse extractIn es of+        Success vSeq+            | sameSize               -> Success vSet+            | otherwise              -> extractError err+          where+            vList = Data.Foldable.toList vSeq+            vSet = toSet vList+            sameSize = size vSet == Data.Sequence.length vSeq+            duplicates = vList Data.List.\\ Data.Foldable.toList vSet+            err | length duplicates == 1 =+                     "One duplicate element in the list: "+                     <> (Data.Text.pack $ show $ head duplicates)+                | otherwise              = Data.Text.pack $ unwords+                     [ show $ length duplicates+                     , "duplicates were found in the list, including"+                     , show $ head duplicates+                     ]+        Failure f -> Failure f+    extractOut expr = typeError expectedOut expr++    expectedOut = App List expectedIn++{-| Decode a `Map` from a @toMap@ expression or generally a @Prelude.Map.Type@++>>> input (Dhall.map strictText bool) "toMap { a = True, b = False }"+fromList [("a",True),("b",False)]+>>> input (Dhall.map strictText bool) "[ { mapKey = \"foo\", mapValue = True } ]"+fromList [("foo",True)]++If there are duplicate @mapKey@s, later @mapValue@s take precedence:++>>> let expr = "[ { mapKey = 1, mapValue = True }, { mapKey = 1, mapValue = False } ]"+>>> input (Dhall.map natural bool) expr+fromList [(1,False)]++-}+map :: Ord k => Type k -> Type v -> Type (Map k v)+map k v = fmap Data.Map.fromList (list (pairFromMapEntry k v))++{-| Decode a `HashMap` from a @toMap@ expression or generally a @Prelude.Map.Type@++>>> input (Dhall.hashMap strictText bool) "toMap { a = True, b = False }"+fromList [("a",True),("b",False)]+>>> input (Dhall.hashMap strictText bool) "[ { mapKey = \"foo\", mapValue = True } ]"+fromList [("foo",True)]++If there are duplicate @mapKey@s, later @mapValue@s take precedence:++>>> let expr = "[ { mapKey = 1, mapValue = True }, { mapKey = 1, mapValue = False } ]"+>>> input (Dhall.hashMap natural bool) expr+fromList [(1,False)]++-}+hashMap :: (Eq k, Hashable k) => Type k -> Type v -> Type (HashMap k v)+hashMap k v = fmap HashMap.fromList (list (pairFromMapEntry k v))++{-| Decode a tuple from a @Prelude.Map.Entry@ record++>>> input (pairFromMapEntry strictText natural) "{ mapKey = \"foo\", mapValue = 3 }"+("foo",3)+-}+pairFromMapEntry :: Type k -> Type v -> Type (k, v)+pairFromMapEntry k v = Type extractOut expectedOut+  where+    extractOut (RecordLit kvs)+        | Just key <- Dhall.Map.lookup "mapKey" kvs+        , Just value <- Dhall.Map.lookup "mapValue" kvs+            = liftA2 (,) (extract k key) (extract v value)+    extractOut expr = typeError expectedOut expr++    expectedOut = Record (Dhall.Map.fromList [("mapKey", expected k), ("mapValue", expected v)])+ {-| Decode @()@ from an empty record.  >>> input unit "{=}"  -- GHC doesn't print the result if it is ()@@ -799,6 +1004,13 @@      expectedOut = Record mempty +{-| Decode 'Void' from an empty union.++Since @<>@ is uninhabited, @'input' 'void'@ will always fail.+-}+void :: Type Void+void = union mempty+ {-| Decode a `String`  >>> input string "\"ABC\""@@ -829,59 +1041,91 @@                 ]             ) -{-| Any value that implements `Interpret` can be automatically decoded based on+{-| Any value that implements `FromDhall` can be automatically decoded based on     the inferred return type of `input`  >>> input auto "[1, 2, 3]" :: IO (Vector Natural) [1,2,3]+>>> input auto "toMap { a = False, b = True }" :: IO (Map Text Bool)+fromList [("a",False),("b",True)]      This class auto-generates a default implementation for records that     implement `Generic`.  This does not auto-generate an instance for recursive     types. -}-class Interpret a where+class FromDhall a where     autoWith:: InterpretOptions -> Type a     default autoWith-        :: (Generic a, GenericInterpret (Rep a)) => InterpretOptions -> Type a+        :: (Generic a, GenericFromDhall (Rep a)) => InterpretOptions -> Type a     autoWith options = fmap GHC.Generics.to (evalState (genericAutoWith options) 1) -instance Interpret Bool where+{-| A compatibility alias for `FromDhall`++This will eventually be removed.+-}+type Interpret = FromDhall++instance FromDhall Void where+    autoWith _ = void++instance FromDhall () where+    autoWith _ = unit++instance FromDhall Bool where     autoWith _ = bool -instance Interpret Natural where+instance FromDhall Natural where     autoWith _ = natural -instance Interpret Integer where+instance FromDhall Integer where     autoWith _ = integer -instance Interpret Scientific where+instance FromDhall Scientific where     autoWith _ = scientific -instance Interpret Double where+instance FromDhall Double where     autoWith _ = double -instance {-# OVERLAPS #-} Interpret [Char] where+instance {-# OVERLAPS #-} FromDhall [Char] where     autoWith _ = string -instance Interpret Data.Text.Lazy.Text where+instance FromDhall Data.Text.Lazy.Text where     autoWith _ = lazyText -instance Interpret Text where+instance FromDhall Text where     autoWith _ = strictText -instance Interpret a => Interpret (Maybe a) where+instance FromDhall a => FromDhall (Maybe a) where     autoWith opts = maybe (autoWith opts) -instance Interpret a => Interpret (Seq a) where+instance FromDhall a => FromDhall (Seq a) where     autoWith opts = sequence (autoWith opts) -instance Interpret a => Interpret [a] where-    autoWith = fmap (fmap Data.Vector.toList) autoWith+instance FromDhall a => FromDhall [a] where+    autoWith opts = list (autoWith opts) -instance Interpret a => Interpret (Vector a) where+instance FromDhall a => FromDhall (Vector a) where     autoWith opts = vector (autoWith opts) -instance (Inject a, Interpret b) => Interpret (a -> b) where+{-| Note that this instance will throw errors in the presence of duplicates in+    the list. To ignore duplicates, use `setIgnoringDuplicates`.+-}+instance (FromDhall a, Ord a, Show a) => FromDhall (Data.Set.Set a) where+    autoWith opts = setFromDistinctList (autoWith opts)++{-| Note that this instance will throw errors in the presence of duplicates in+    the list. To ignore duplicates, use `hashSetIgnoringDuplicates`.+-}+instance (FromDhall a, Hashable a, Ord a, Show a) => FromDhall (Data.HashSet.HashSet a) where+    autoWith opts = hashSetFromDistinctList (autoWith opts)++instance (Ord k, FromDhall k, FromDhall v) => FromDhall (Map k v) where+    autoWith opts = Dhall.map (autoWith opts) (autoWith opts)++instance (Eq k, Hashable k, FromDhall k, FromDhall v) => FromDhall (HashMap k v) where+    autoWith opts = Dhall.hashMap (autoWith opts) (autoWith opts)++instance (ToDhall a, FromDhall b) => FromDhall (a -> b) where     autoWith opts = Type extractOut expectedOut       where         normalizer_ = Just (inputNormalizer opts)@@ -889,7 +1133,7 @@         -- ToDo         extractOut e = pure (\i -> case extractIn (Dhall.Core.normalizeWith normalizer_ (App e (embed i))) of             Success o  -> o-            Failure _e -> error "Interpret: You cannot decode a function if it does not have the correct type" )+            Failure _e -> error "FromDhall: You cannot decode a function if it does not have the correct type" )          expectedOut = Pi "_" declared expectedIn @@ -897,25 +1141,25 @@          Type extractIn expectedIn = autoWith opts -instance (Interpret a, Interpret b) => Interpret (a, b)+instance (FromDhall a, FromDhall b) => FromDhall (a, b)  {-| Use the default options for interpreting a configuration file  > auto = autoWith defaultInterpretOptions -}-auto :: Interpret a => Type a+auto :: FromDhall a => Type a auto = autoWith defaultInterpretOptions  {-| This type is exactly the same as `Data.Fix.Fix` except with a different-    `Interpret` instance.  This intermediate type simplies the implementation-    of the inner loop for the `Interpret` instance for `Fix`+    `FromDhall` instance.  This intermediate type simplies the implementation+    of the inner loop for the `FromDhall` instance for `Fix` -} newtype Result f = Result { _unResult :: f (Result f) }  resultToFix :: Functor f => Result f -> Fix f resultToFix (Result x) = Fix (fmap resultToFix x) -instance Interpret (f (Result f)) => Interpret (Result f) where+instance FromDhall (f (Result f)) => FromDhall (Result f) where     autoWith options = Type { expected = expected_, extract = extract_ }       where         expected_ = "result"@@ -939,30 +1183,30 @@ -- > {-# LANGUAGE StandaloneDeriving #-} -- > {-# LANGUAGE TypeFamilies       #-} -- > {-# LANGUAGE TemplateHaskell    #-}--- > +-- > -- > import Data.Fix (Fix(..)) -- > import Data.Text (Text)--- > import Dhall (Interpret)+-- > import Dhall (FromDhall) -- > import GHC.Generics (Generic) -- > import Numeric.Natural (Natural)--- > +-- > -- > import qualified Data.Fix                 as Fix -- > import qualified Data.Functor.Foldable    as Foldable -- > import qualified Data.Functor.Foldable.TH as TH -- > import qualified Dhall -- > import qualified NeatInterpolation--- > +-- > -- > data Expr -- >     = Lit Natural -- >     | Add Expr Expr -- >     | Mul Expr Expr -- >     deriving (Show)--- > +-- > -- > TH.makeBaseFunctor ''Expr--- > +-- > -- > deriving instance Generic (ExprF a)--- > deriving instance Interpret a => Interpret (ExprF a)--- > +-- > deriving instance FromDhall a => FromDhall (ExprF a)+-- > -- > example :: Text -- > example = [NeatInterpolation.text| -- >     \(Expr : Type)@@ -974,32 +1218,32 @@ -- >           | MulF : -- >               { _1 : Expr, _2 : Expr } -- >           >--- >     +-- > -- >     in      \(Fix : ExprF -> Expr) -- >         ->  let Lit = \(x : Natural) -> Fix (ExprF.LitF { _1 = x })--- >             +-- > -- >             let Add = -- >                       \(x : Expr) -- >                   ->  \(y : Expr) -- >                   ->  Fix (ExprF.AddF { _1 = x, _2 = y })--- >             +-- > -- >             let Mul = -- >                       \(x : Expr) -- >                   ->  \(y : Expr) -- >                   ->  Fix (ExprF.MulF { _1 = x, _2 = y })--- >             +-- > -- >             in  Add (Mul (Lit 3) (Lit 7)) (Add (Lit 1) (Lit 2)) -- > |]--- > +-- > -- > convert :: Fix ExprF -> Expr -- > convert = Fix.cata Foldable.embed--- > +-- > -- > main :: IO () -- > main = do -- >     x <- Dhall.input Dhall.auto example :: IO (Fix ExprF)--- > +-- > -- >     print (convert x :: Expr)-instance (Functor f, Interpret (f (Result f))) => Interpret (Fix f) where+instance (Functor f, FromDhall (f (Result f))) => FromDhall (Fix f) where     autoWith options = Type { expected = expected_, extract = extract_ }       where         expected_ =@@ -1015,15 +1259,15 @@             go0 _ = typeError expected_ expression0  {-| `genericAuto` is the default implementation for `auto` if you derive-    `Interpret`.  The difference is that you can use `genericAuto` without-    having to explicitly provide an `Interpret` instance for a type as long as+    `FromDhall`.  The difference is that you can use `genericAuto` without+    having to explicitly provide a `FromDhall` instance for a type as long as     the type derives `Generic` -}-genericAuto :: (Generic a, GenericInterpret (Rep a)) => Type a+genericAuto :: (Generic a, GenericFromDhall (Rep a)) => Type a genericAuto = fmap to (evalState (genericAutoWith defaultInterpretOptions) 1)  {-| Use these options to tweak how Dhall derives a generic implementation of-    `Interpret`+    `FromDhall` -} data InterpretOptions = InterpretOptions     { fieldModifier       :: Text -> Text@@ -1036,8 +1280,8 @@     -- ^ Specify how to handle constructors with only one field.  The default is     --   `Wrapped` for backwards compatibility but will eventually be changed to     --   `Smart`-    , inputNormalizer     :: Dhall.Core.ReifiedNormalizer X-    -- ^ This is only used by the `Interpret` instance for functions in order+    , inputNormalizer     :: Dhall.Core.ReifiedNormalizer Void+    -- ^ This is only used by the `FromDhall` instance for functions in order     --   to normalize the function input before marshaling the input into a     --   Dhall expression     }@@ -1082,18 +1326,18 @@           Dhall.Core.ReifiedNormalizer (const (pure Nothing))     } -{-| This is the underlying class that powers the `Interpret` class's support+{-| This is the underlying class that powers the `FromDhall` class's support     for automatically deriving a generic implementation -}-class GenericInterpret f where+class GenericFromDhall f where     genericAutoWith :: InterpretOptions -> State Int (Type (f a)) -instance GenericInterpret f => GenericInterpret (M1 D d f) where+instance GenericFromDhall f => GenericFromDhall (M1 D d f) where     genericAutoWith options = do         res <- genericAutoWith options         pure (fmap M1 res) -instance GenericInterpret V1 where+instance GenericFromDhall V1 where     genericAutoWith _ = pure Type {..}       where         extract expr = typeError expected expr@@ -1101,14 +1345,15 @@         expected = Union mempty  unsafeExpectUnion-    :: Text -> Expr Src X -> Dhall.Map.Map Text (Maybe (Expr Src X))+    :: Text -> Expr Src Void -> Dhall.Map.Map Text (Maybe (Expr Src Void)) unsafeExpectUnion _ (Union kts) =     kts unsafeExpectUnion name expression =     Dhall.Core.internalError         (name <> ": Unexpected constructor: " <> Dhall.Core.pretty expression) -unsafeExpectRecord :: Text -> Expr Src X -> Dhall.Map.Map Text (Expr Src X)+unsafeExpectRecord+    :: Text -> Expr Src Void -> Dhall.Map.Map Text (Expr Src Void) unsafeExpectRecord _ (Record kts) =     kts unsafeExpectRecord name expression =@@ -1117,8 +1362,8 @@  unsafeExpectUnionLit     :: Text-    -> Expr Src X-    -> (Text, Maybe (Expr Src X))+    -> Expr Src Void+    -> (Text, Maybe (Expr Src Void)) unsafeExpectUnionLit _ (Field (Union _) k) =     (k, Nothing) unsafeExpectUnionLit _ (App (Field (Union _) k) v) =@@ -1127,7 +1372,8 @@     Dhall.Core.internalError         (name <> ": Unexpected constructor: " <> Dhall.Core.pretty expression) -unsafeExpectRecordLit :: Text -> Expr Src X -> Dhall.Map.Map Text (Expr Src X)+unsafeExpectRecordLit+    :: Text -> Expr Src Void -> Dhall.Map.Map Text (Expr Src Void) unsafeExpectRecordLit _ (RecordLit kvs) =     kvs unsafeExpectRecordLit name expression =@@ -1152,7 +1398,7 @@ extractUnionConstructor _ =   empty -instance (Constructor c1, Constructor c2, GenericInterpret f1, GenericInterpret f2) => GenericInterpret (M1 C c1 f1 :+: M1 C c2 f2) where+instance (Constructor c1, Constructor c2, GenericFromDhall f1, GenericFromDhall f2) => GenericFromDhall (M1 C c1 f1 :+: M1 C c2 f2) where     genericAutoWith options@(InterpretOptions {..}) = pure (Type {..})       where         nL :: M1 i c1 f1 a@@ -1184,7 +1430,7 @@         Type extractL expectedL = evalState (genericAutoWith options) 1         Type extractR expectedR = evalState (genericAutoWith options) 1 -instance (Constructor c, GenericInterpret (f :+: g), GenericInterpret h) => GenericInterpret ((f :+: g) :+: M1 C c h) where+instance (Constructor c, GenericFromDhall (f :+: g), GenericFromDhall h) => GenericFromDhall ((f :+: g) :+: M1 C c h) where     genericAutoWith options@(InterpretOptions {..}) = pure (Type {..})       where         n :: M1 i c h a@@ -1207,7 +1453,7 @@          ktsL = unsafeExpectUnion "genericAutoWith (:+:)" expectedL -instance (Constructor c, GenericInterpret f, GenericInterpret (g :+: h)) => GenericInterpret (M1 C c f :+: (g :+: h)) where+instance (Constructor c, GenericFromDhall f, GenericFromDhall (g :+: h)) => GenericFromDhall (M1 C c f :+: (g :+: h)) where     genericAutoWith options@(InterpretOptions {..}) = pure (Type {..})       where         n :: M1 i c f a@@ -1230,7 +1476,7 @@          ktsR = unsafeExpectUnion "genericAutoWith (:+:)" expectedR -instance (GenericInterpret (f :+: g), GenericInterpret (h :+: i)) => GenericInterpret ((f :+: g) :+: (h :+: i)) where+instance (GenericFromDhall (f :+: g), GenericFromDhall (h :+: i)) => GenericFromDhall ((f :+: g) :+: (h :+: i)) where     genericAutoWith options = pure (Type {..})       where         extract e = fmap L1 (extractL e) `ealt` fmap R1 (extractR e)@@ -1243,12 +1489,12 @@         ktsL = unsafeExpectUnion "genericAutoWith (:+:)" expectedL         ktsR = unsafeExpectUnion "genericAutoWith (:+:)" expectedR -instance GenericInterpret f => GenericInterpret (M1 C c f) where+instance GenericFromDhall f => GenericFromDhall (M1 C c f) where     genericAutoWith options = do         res <- genericAutoWith options         pure (fmap M1 res) -instance GenericInterpret U1 where+instance GenericFromDhall U1 where     genericAutoWith _ = pure (Type {..})       where         extract _ = pure U1@@ -1262,7 +1508,7 @@              pure (Data.Text.pack ("_" ++ show i))     nn -> pure (Data.Text.pack nn) -instance (GenericInterpret (f :*: g), GenericInterpret (h :*: i)) => GenericInterpret ((f :*: g) :*: (h :*: i)) where+instance (GenericFromDhall (f :*: g), GenericFromDhall (h :*: i)) => GenericFromDhall ((f :*: g) :*: (h :*: i)) where     genericAutoWith options = do         Type extractL expectedL <- genericAutoWith options         Type extractR expectedR <- genericAutoWith options@@ -1277,7 +1523,7 @@          return (Type {..}) -instance (GenericInterpret (f :*: g), Selector s, Interpret a) => GenericInterpret ((f :*: g) :*: M1 S s (K1 i a)) where+instance (GenericFromDhall (f :*: g), Selector s, FromDhall a) => GenericFromDhall ((f :*: g) :*: M1 S s (K1 i a)) where     genericAutoWith options@InterpretOptions{..} = do         let nR :: M1 S s (K1 i a) r             nR = undefined@@ -1307,7 +1553,7 @@          return (Type {..}) -instance (Selector s, Interpret a, GenericInterpret (f :*: g)) => GenericInterpret (M1 S s (K1 i a) :*: (f :*: g)) where+instance (Selector s, FromDhall a, GenericFromDhall (f :*: g)) => GenericFromDhall (M1 S s (K1 i a) :*: (f :*: g)) where     genericAutoWith options@InterpretOptions{..} = do         let nL :: M1 S s (K1 i a) r             nL = undefined@@ -1337,7 +1583,7 @@          return (Type {..}) -instance (Selector s1, Selector s2, Interpret a1, Interpret a2) => GenericInterpret (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where+instance (Selector s1, Selector s2, FromDhall a1, FromDhall a2) => GenericFromDhall (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where     genericAutoWith options@InterpretOptions{..} = do         let nL :: M1 S s1 (K1 i1 a1) r             nL = undefined@@ -1374,7 +1620,7 @@          return (Type {..}) -instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where+instance (Selector s, FromDhall a) => GenericFromDhall (M1 S s (K1 i a)) where     genericAutoWith options@InterpretOptions{..} = do         let n :: M1 S s (K1 i a) r             n = undefined@@ -1420,9 +1666,9 @@     Haskell into Dhall -} data InputType a = InputType-    { embed    :: a -> Expr Src X+    { embed    :: a -> Expr Src Void     -- ^ Embeds a Haskell value as a Dhall expression-    , declared :: Expr Src X+    , declared :: Expr Src Void     -- ^ Dhall type of the Haskell value     } @@ -1431,53 +1677,66 @@       where         embed' x = embed (f x) -{-| This class is used by `Interpret` instance for functions:+{-| This class is used by `FromDhall` instance for functions: -> instance (Inject a, Interpret b) => Interpret (a -> b)+> instance (ToDhall a, FromDhall b) => FromDhall (a -> b)      You can convert Dhall functions with "simple" inputs (i.e. instances of this     class) into Haskell functions.  This works by:      * Marshaling the input to the Haskell function into a Dhall expression (i.e.-      @x :: Expr Src X@)-    * Applying the Dhall function (i.e. @f :: Expr Src X@) to the Dhall input+      @x :: Expr Src Void@)+    * Applying the Dhall function (i.e. @f :: Expr Src Void@) to the Dhall input       (i.e. @App f x@)     * Normalizing the syntax tree (i.e. @normalize (App f x)@)     * Marshaling the resulting Dhall expression back into a Haskell value -}-class Inject a where+class ToDhall a where     injectWith :: InterpretOptions -> InputType a     default injectWith-        :: (Generic a, GenericInject (Rep a)) => InterpretOptions -> InputType a+        :: (Generic a, GenericToDhall (Rep a)) => InterpretOptions -> InputType a     injectWith options-        = contramap GHC.Generics.from (evalState (genericInjectWith options) 1)+        = contramap GHC.Generics.from (evalState (genericToDhallWith options) 1) +{-| A compatibility alias for `ToDhall`++This will eventually be removed.+-}+type Inject = ToDhall+ {-| Use the default options for injecting a value -> inject = inject defaultInterpretOptions+> inject = injectWith defaultInterpretOptions -}-inject :: Inject a => InputType a+inject :: ToDhall a => InputType a inject = injectWith defaultInterpretOptions  {-| Use the default options for injecting a value, whose structure is determined generically. -This can be used when you want to use 'Inject' on types that you don't+This can be used when you want to use 'ToDhall' on types that you don't want to define orphan instances for. -}-genericInject-  :: (Generic a, GenericInject (Rep a)) => InputType a-genericInject-    = contramap GHC.Generics.from (evalState (genericInjectWith defaultInterpretOptions) 1)+genericToDhall+  :: (Generic a, GenericToDhall (Rep a)) => InputType a+genericToDhall+    = contramap GHC.Generics.from (evalState (genericToDhallWith defaultInterpretOptions) 1) -instance Inject Bool where+instance ToDhall Void where     injectWith _ = InputType {..}       where+        embed = Data.Void.absurd++        declared = Union mempty++instance ToDhall Bool where+    injectWith _ = InputType {..}+      where         embed = BoolLit          declared = Bool -instance Inject Data.Text.Lazy.Text where+instance ToDhall Data.Text.Lazy.Text where     injectWith _ = InputType {..}       where         embed text =@@ -1485,85 +1744,122 @@          declared = Text -instance Inject Text where+instance ToDhall Text where     injectWith _ = InputType {..}       where         embed text = TextLit (Chunks [] text)          declared = Text -instance {-# OVERLAPS #-} Inject String where+instance {-# OVERLAPS #-} ToDhall String where     injectWith options =         contramap Data.Text.pack (injectWith options :: InputType Text) -instance Inject Natural where+instance ToDhall Natural where     injectWith _ = InputType {..}       where         embed = NaturalLit          declared = Natural -instance Inject Integer where+instance ToDhall Integer where     injectWith _ = InputType {..}       where         embed = IntegerLit          declared = Integer -instance Inject Int where+instance ToDhall Int where     injectWith _ = InputType {..}       where         embed = IntegerLit . toInteger          declared = Integer -instance Inject Word8 where+{-|++>>> embed inject (12 :: Word)+NaturalLit 12+-}++instance ToDhall Word where     injectWith _ = InputType {..}       where-        embed = IntegerLit . toInteger+        embed = NaturalLit . fromIntegral -        declared = Integer+        declared = Natural -instance Inject Word16 where+{-|++>>> embed inject (12 :: Word8)+NaturalLit 12+-}++instance ToDhall Word8 where     injectWith _ = InputType {..}       where-        embed = IntegerLit . toInteger+        embed = NaturalLit . fromIntegral -        declared = Integer+        declared = Natural -instance Inject Word32 where+{-|++>>> embed inject (12 :: Word16)+NaturalLit 12+-}++instance ToDhall Word16 where     injectWith _ = InputType {..}       where-        embed = IntegerLit . toInteger+        embed = NaturalLit . fromIntegral -        declared = Integer+        declared = Natural -instance Inject Word64 where+{-|++>>> embed inject (12 :: Word32)+NaturalLit 12+-}++instance ToDhall Word32 where     injectWith _ = InputType {..}       where-        embed = IntegerLit . toInteger+        embed = NaturalLit . fromIntegral -        declared = Integer+        declared = Natural -instance Inject Double where+{-|++>>> embed inject (12 :: Word64)+NaturalLit 12+-}++instance ToDhall Word64 where     injectWith _ = InputType {..}       where-        embed = DoubleLit+        embed = NaturalLit . fromIntegral +        declared = Natural++instance ToDhall Double where+    injectWith _ = InputType {..}+      where+        embed = DoubleLit . DhallDouble+         declared = Double -instance Inject Scientific where+instance ToDhall Scientific where     injectWith options =         contramap Data.Scientific.toRealFloat (injectWith options :: InputType Double) -instance Inject () where+instance ToDhall () where     injectWith _ = InputType {..}       where         embed = const (RecordLit mempty)          declared = Record mempty -instance Inject a => Inject (Maybe a) where+instance ToDhall a => ToDhall (Maybe a) where     injectWith options = InputType embedOut declaredOut       where         embedOut (Just x ) = Some (embedIn x)@@ -1573,7 +1869,7 @@          declaredOut = App Optional declaredIn -instance Inject a => Inject (Seq a) where+instance ToDhall a => ToDhall (Seq a) where     injectWith options = InputType embedOut declaredOut       where         embedOut xs = ListLit listType (fmap embedIn xs)@@ -1586,35 +1882,108 @@          InputType embedIn declaredIn = injectWith options -instance Inject a => Inject [a] where+instance ToDhall a => ToDhall [a] where     injectWith = fmap (contramap Data.Sequence.fromList) injectWith -instance Inject a => Inject (Vector a) where+instance ToDhall a => ToDhall (Vector a) where     injectWith = fmap (contramap Data.Vector.toList) injectWith -instance Inject a => Inject (Data.Set.Set a) where-    injectWith = fmap (contramap Data.Set.toList) injectWith+{-| Note that the ouput list will be sorted -instance (Inject a, Inject b) => Inject (a, b)+>>> let x = Data.Set.fromList ["mom", "hi" :: Text]+>>> prettyExpr $ embed inject x+[ "hi", "mom" ] -{-| This is the underlying class that powers the `Interpret` class's support+-}+instance ToDhall a => ToDhall (Data.Set.Set a) where+    injectWith = fmap (contramap Data.Set.toAscList) injectWith++{-| Note that the ouput list may not be sorted++>>> let x = Data.HashSet.fromList ["hi", "mom" :: Text]+>>> prettyExpr $ embed inject x+[ "mom", "hi" ]++-}+instance ToDhall a => ToDhall (Data.HashSet.HashSet a) where+    injectWith = fmap (contramap Data.HashSet.toList) injectWith++instance (ToDhall a, ToDhall b) => ToDhall (a, b)++{-| Embed a `Data.Map` as a @Prelude.Map.Type@++>>> prettyExpr $ embed inject (Data.Map.fromList [(1 :: Natural, True)])+[ { mapKey = 1, mapValue = True } ]++>>> prettyExpr $ embed inject (Data.Map.fromList [] :: Data.Map.Map Natural Bool)+[] : List { mapKey : Natural, mapValue : Bool }++-}+instance (ToDhall k, ToDhall v) => ToDhall (Data.Map.Map k v) where+    injectWith options = InputType embedOut declaredOut+      where+        embedOut m = ListLit listType (mapEntries m)+          where+            listType+                | Data.Map.null m = Just declaredOut+                | otherwise       = Nothing++        declaredOut = App List (Record (Dhall.Map.fromList+                          [("mapKey", declaredK), ("mapValue", declaredV)]))++        mapEntries = Data.Sequence.fromList . fmap recordPair . Data.Map.toList+        recordPair (k, v) = RecordLit (Dhall.Map.fromList+                                [("mapKey", embedK k), ("mapValue", embedV v)])++        InputType embedK declaredK = injectWith options+        InputType embedV declaredV = injectWith options++{-| Embed a `Data.HashMap` as a @Prelude.Map.Type@++>>> prettyExpr $ embed inject (HashMap.fromList [(1 :: Natural, True)])+[ { mapKey = 1, mapValue = True } ]++>>> prettyExpr $ embed inject (HashMap.fromList [] :: HashMap Natural Bool)+[] : List { mapKey : Natural, mapValue : Bool }++-}+instance (ToDhall k, ToDhall v) => ToDhall (HashMap k v) where+    injectWith options = InputType embedOut declaredOut+      where+        embedOut m = ListLit listType (mapEntries m)+          where+            listType+                | HashMap.null m = Just declaredOut+                | otherwise       = Nothing++        declaredOut = App List (Record (Dhall.Map.fromList+                          [("mapKey", declaredK), ("mapValue", declaredV)]))++        mapEntries = Data.Sequence.fromList . fmap recordPair . HashMap.toList+        recordPair (k, v) = RecordLit (Dhall.Map.fromList+                                [("mapKey", embedK k), ("mapValue", embedV v)])++        InputType embedK declaredK = injectWith options+        InputType embedV declaredV = injectWith options++{-| This is the underlying class that powers the `FromDhall` class's support     for automatically deriving a generic implementation -}-class GenericInject f where-    genericInjectWith :: InterpretOptions -> State Int (InputType (f a))+class GenericToDhall f where+    genericToDhallWith :: InterpretOptions -> State Int (InputType (f a)) -instance GenericInject f => GenericInject (M1 D d f) where-    genericInjectWith options = do-        res <- genericInjectWith options+instance GenericToDhall f => GenericToDhall (M1 D d f) where+    genericToDhallWith options = do+        res <- genericToDhallWith options         pure (contramap unM1 res) -instance GenericInject f => GenericInject (M1 C c f) where-    genericInjectWith options = do-        res <- genericInjectWith options+instance GenericToDhall f => GenericToDhall (M1 C c f) where+    genericToDhallWith options = do+        res <- genericToDhallWith options         pure (contramap unM1 res) -instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where-    genericInjectWith options@InterpretOptions{..} = do+instance (Selector s, ToDhall a) => GenericToDhall (M1 S s (K1 i a)) where+    genericToDhallWith options@InterpretOptions{..} = do         let InputType { embed = embed', declared = declared' } =                 injectWith options @@ -1645,8 +2014,8 @@          return (InputType {..}) -instance (Constructor c1, Constructor c2, GenericInject f1, GenericInject f2) => GenericInject (M1 C c1 f1 :+: M1 C c2 f2) where-    genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})+instance (Constructor c1, Constructor c2, GenericToDhall f1, GenericToDhall f2) => GenericToDhall (M1 C c1 f1 :+: M1 C c2 f2) where+    genericToDhallWith options@(InterpretOptions {..}) = pure (InputType {..})       where         embed (L1 (M1 l)) =             case notEmptyRecordLit (embedL l) of@@ -1679,11 +2048,11 @@         keyL = constructorModifier (Data.Text.pack (conName nL))         keyR = constructorModifier (Data.Text.pack (conName nR)) -        InputType embedL declaredL = evalState (genericInjectWith options) 1-        InputType embedR declaredR = evalState (genericInjectWith options) 1+        InputType embedL declaredL = evalState (genericToDhallWith options) 1+        InputType embedR declaredR = evalState (genericToDhallWith options) 1 -instance (Constructor c, GenericInject (f :+: g), GenericInject h) => GenericInject ((f :+: g) :+: M1 C c h) where-    genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})+instance (Constructor c, GenericToDhall (f :+: g), GenericToDhall h) => GenericToDhall ((f :+: g) :+: M1 C c h) where+    genericToDhallWith options@(InterpretOptions {..}) = pure (InputType {..})       where         embed (L1 l) =             case maybeValL of@@ -1691,7 +2060,7 @@                 Just valL -> App (Field declared keyL) valL           where             (keyL, maybeValL) =-              unsafeExpectUnionLit "genericInjectWith (:+:)" (embedL l)+              unsafeExpectUnionLit "genericToDhallWith (:+:)" (embedL l)         embed (R1 (M1 r)) =             case notEmptyRecordLit (embedR r) of                 Nothing   -> Field declared keyR@@ -1704,13 +2073,13 @@          declared = Union (Dhall.Map.insert keyR (notEmptyRecord declaredR) ktsL) -        InputType embedL declaredL = evalState (genericInjectWith options) 1-        InputType embedR declaredR = evalState (genericInjectWith options) 1+        InputType embedL declaredL = evalState (genericToDhallWith options) 1+        InputType embedR declaredR = evalState (genericToDhallWith options) 1 -        ktsL = unsafeExpectUnion "genericInjectWith (:+:)" declaredL+        ktsL = unsafeExpectUnion "genericToDhallWith (:+:)" declaredL -instance (Constructor c, GenericInject f, GenericInject (g :+: h)) => GenericInject (M1 C c f :+: (g :+: h)) where-    genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})+instance (Constructor c, GenericToDhall f, GenericToDhall (g :+: h)) => GenericToDhall (M1 C c f :+: (g :+: h)) where+    genericToDhallWith options@(InterpretOptions {..}) = pure (InputType {..})       where         embed (L1 (M1 l)) =             case notEmptyRecordLit (embedL l) of@@ -1722,7 +2091,7 @@                 Just valR -> App (Field declared keyR) valR           where             (keyR, maybeValR) =-                unsafeExpectUnionLit "genericInjectWith (:+:)" (embedR r)+                unsafeExpectUnionLit "genericToDhallWith (:+:)" (embedR r)          nL :: M1 i c f a         nL = undefined@@ -1731,13 +2100,13 @@          declared = Union (Dhall.Map.insert keyL (notEmptyRecord declaredL) ktsR) -        InputType embedL declaredL = evalState (genericInjectWith options) 1-        InputType embedR declaredR = evalState (genericInjectWith options) 1+        InputType embedL declaredL = evalState (genericToDhallWith options) 1+        InputType embedR declaredR = evalState (genericToDhallWith options) 1 -        ktsR = unsafeExpectUnion "genericInjectWith (:+:)" declaredR+        ktsR = unsafeExpectUnion "genericToDhallWith (:+:)" declaredR -instance (GenericInject (f :+: g), GenericInject (h :+: i)) => GenericInject ((f :+: g) :+: (h :+: i)) where-    genericInjectWith options = pure (InputType {..})+instance (GenericToDhall (f :+: g), GenericToDhall (h :+: i)) => GenericToDhall ((f :+: g) :+: (h :+: i)) where+    genericToDhallWith options = pure (InputType {..})       where         embed (L1 l) =             case maybeValL of@@ -1745,52 +2114,52 @@                 Just valL -> App (Field declared keyL) valL           where             (keyL, maybeValL) =-                unsafeExpectUnionLit "genericInjectWith (:+:)" (embedL l)+                unsafeExpectUnionLit "genericToDhallWith (:+:)" (embedL l)         embed (R1 r) =             case maybeValR of                 Nothing   -> Field declared keyR                 Just valR -> App (Field declared keyR) valR           where             (keyR, maybeValR) =-                unsafeExpectUnionLit "genericInjectWith (:+:)" (embedR r)+                unsafeExpectUnionLit "genericToDhallWith (:+:)" (embedR r)          declared = Union (Dhall.Map.union ktsL ktsR) -        InputType embedL declaredL = evalState (genericInjectWith options) 1-        InputType embedR declaredR = evalState (genericInjectWith options) 1+        InputType embedL declaredL = evalState (genericToDhallWith options) 1+        InputType embedR declaredR = evalState (genericToDhallWith options) 1 -        ktsL = unsafeExpectUnion "genericInjectWith (:+:)" declaredL-        ktsR = unsafeExpectUnion "genericInjectWith (:+:)" declaredR+        ktsL = unsafeExpectUnion "genericToDhallWith (:+:)" declaredL+        ktsR = unsafeExpectUnion "genericToDhallWith (:+:)" declaredR -instance (GenericInject (f :*: g), GenericInject (h :*: i)) => GenericInject ((f :*: g) :*: (h :*: i)) where-    genericInjectWith options = do-        InputType embedL declaredL <- genericInjectWith options-        InputType embedR declaredR <- genericInjectWith options+instance (GenericToDhall (f :*: g), GenericToDhall (h :*: i)) => GenericToDhall ((f :*: g) :*: (h :*: i)) where+    genericToDhallWith options = do+        InputType embedL declaredL <- genericToDhallWith options+        InputType embedR declaredR <- genericToDhallWith options          let embed (l :*: r) =                 RecordLit (Dhall.Map.union mapL mapR)               where                 mapL =-                    unsafeExpectRecordLit "genericInjectWith (:*:)" (embedL l)+                    unsafeExpectRecordLit "genericToDhallWith (:*:)" (embedL l)                  mapR =-                    unsafeExpectRecordLit "genericInjectWith (:*:)" (embedR r)+                    unsafeExpectRecordLit "genericToDhallWith (:*:)" (embedR r)          let declared = Record (Dhall.Map.union mapL mapR)               where-                mapL = unsafeExpectRecord "genericInjectWith (:*:)" declaredL-                mapR = unsafeExpectRecord "genericInjectWith (:*:)" declaredR+                mapL = unsafeExpectRecord "genericToDhallWith (:*:)" declaredL+                mapR = unsafeExpectRecord "genericToDhallWith (:*:)" declaredR          pure (InputType {..}) -instance (GenericInject (f :*: g), Selector s, Inject a) => GenericInject ((f :*: g) :*: M1 S s (K1 i a)) where-    genericInjectWith options@InterpretOptions{..} = do+instance (GenericToDhall (f :*: g), Selector s, ToDhall a) => GenericToDhall ((f :*: g) :*: M1 S s (K1 i a)) where+    genericToDhallWith options@InterpretOptions{..} = do         let nR :: M1 S s (K1 i a) r             nR = undefined          nameR <- fmap fieldModifier (getSelName nR) -        InputType embedL declaredL <- genericInjectWith options+        InputType embedL declaredL <- genericToDhallWith options          let InputType embedR declaredR = injectWith options @@ -1798,16 +2167,16 @@                 RecordLit (Dhall.Map.insert nameR (embedR r) mapL)               where                 mapL =-                    unsafeExpectRecordLit "genericInjectWith (:*:)" (embedL l)+                    unsafeExpectRecordLit "genericToDhallWith (:*:)" (embedL l)          let declared = Record (Dhall.Map.insert nameR declaredR mapL)               where-                mapL = unsafeExpectRecord "genericInjectWith (:*:)" declaredL+                mapL = unsafeExpectRecord "genericToDhallWith (:*:)" declaredL          return (InputType {..}) -instance (Selector s, Inject a, GenericInject (f :*: g)) => GenericInject (M1 S s (K1 i a) :*: (f :*: g)) where-    genericInjectWith options@InterpretOptions{..} = do+instance (Selector s, ToDhall a, GenericToDhall (f :*: g)) => GenericToDhall (M1 S s (K1 i a) :*: (f :*: g)) where+    genericToDhallWith options@InterpretOptions{..} = do         let nL :: M1 S s (K1 i a) r             nL = undefined @@ -1815,22 +2184,22 @@          let InputType embedL declaredL = injectWith options -        InputType embedR declaredR <- genericInjectWith options+        InputType embedR declaredR <- genericToDhallWith options          let embed (M1 (K1 l) :*: r) =                 RecordLit (Dhall.Map.insert nameL (embedL l) mapR)               where                 mapR =-                    unsafeExpectRecordLit "genericInjectWith (:*:)" (embedR r)+                    unsafeExpectRecordLit "genericToDhallWith (:*:)" (embedR r)          let declared = Record (Dhall.Map.insert nameL declaredL mapR)               where-                mapR = unsafeExpectRecord "genericInjectWith (:*:)" declaredR+                mapR = unsafeExpectRecord "genericToDhallWith (:*:)" declaredR          return (InputType {..}) -instance (Selector s1, Selector s2, Inject a1, Inject a2) => GenericInject (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where-    genericInjectWith options@InterpretOptions{..} = do+instance (Selector s1, Selector s2, ToDhall a1, ToDhall a2) => GenericToDhall (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where+    genericToDhallWith options@InterpretOptions{..} = do         let nL :: M1 S s1 (K1 i1 a1) r             nL = undefined @@ -1857,8 +2226,8 @@          return (InputType {..}) -instance GenericInject U1 where-    genericInjectWith _ = pure (InputType {..})+instance GenericToDhall U1 where+    genericToDhallWith _ = pure (InputType {..})       where         embed _ = RecordLit mempty @@ -1909,12 +2278,12 @@         ( Control.Applicative.Const             ( Dhall.Map.Map                 Text-                ( Expr Src X )+                ( Expr Src Void )             )         )         ( Data.Functor.Compose.Compose-            ( (->) ( Expr Src X ) )-            (Extractor Src X)+            ( (->) ( Expr Src Void ) )+            (Extractor Src Void)         )         a     )@@ -2062,7 +2431,7 @@     adapt (Project{..}) = (projectName, (projectDescription, projectStars)) :} -    Or, since we are simply using the `Inject` instance to inject each field, we could write+    Or, since we are simply using the `ToDhall` instance to inject each field, we could write  >>> :{ injectProject :: InputType Project@@ -2084,6 +2453,7 @@  infixr 5 >*< +-- | Intermediate type used for building a `ToDhall` instance for a record newtype RecordInputType a   = RecordInputType (Dhall.Map.Map Text (InputType a)) @@ -2098,12 +2468,19 @@       ((contramap $ snd . f) <$> cInputTypeRecord)   conquer = RecordInputType mempty +{-| Specify how to encode one field of a record by supplying an explicit+    `InputType` for that field+-} inputFieldWith :: Text -> InputType a -> RecordInputType a inputFieldWith name inputType = RecordInputType $ Dhall.Map.singleton name inputType -inputField :: Inject a => Text -> RecordInputType a+{-| Specify how to encode one field of a record using the default `ToDhall`+    instance for that type+-}+inputField :: ToDhall a => Text -> RecordInputType a inputField name = inputFieldWith name inject +-- | Convert a `RecordInputType` into the equivalent `InputType` inputRecord :: RecordInputType a -> InputType a inputRecord (RecordInputType inputTypeRecord) = InputType makeRecordLit recordType   where@@ -2146,7 +2523,7 @@     adapt (Errored e) = Right (Right e) :} -    Or, since we are simply using the `Inject` instance to inject each branch, we could write+    Or, since we are simply using the `ToDhall` instance to inject each branch, we could write  >>> :{ injectStatus :: InputType Status@@ -2168,10 +2545,10 @@         ( Control.Applicative.Const             ( Dhall.Map.Map                 Text-                ( Expr Src X )+                ( Expr Src Void )             )         )-        ( Op (Text, Expr Src X) )+        ( Op (Text, Expr Src Void) )         a     )   deriving (Contravariant)@@ -2193,6 +2570,7 @@  infixr 5 >|< +-- | Convert a `UnionInputType` into the equivalent `InputType` inputUnion :: UnionInputType a -> InputType a inputUnion ( UnionInputType ( Data.Functor.Product.Pair ( Control.Applicative.Const fields ) ( Op embedF ) ) ) =     InputType@@ -2207,6 +2585,9 @@   where     fields' = fmap notEmptyRecord fields +{-| Specify how to encode an alternative by providing an explicit `InputType`+    for that alternative+-} inputConstructorWith     :: Text     -> InputType a@@ -2222,8 +2603,11 @@       ( Op ( (name,) . embed inputType )       ) +{-| Specify how to encode an alternative by using the default `ToDhall` instance+    for that type+-} inputConstructor-    :: Inject a+    :: ToDhall a     => Text     -> UnionInputType a inputConstructor name = inputConstructorWith name inject

@@ -31,6 +31,7 @@     , Chunks(..)     , Const(..)     , Directory(..)+    , DhallDouble(..)     , Expr(..)     , File(..)     , FilePrefix(..)@@ -59,7 +60,11 @@ import qualified Dhall.Map import qualified Dhall.Set --- | Supported version strings+{-| Supported version strings++    This exists primarily for backwards compatibility for expressions encoded+    before Dhall removed version tags from the binary encoding+-} data StandardVersion     = NoVersion     -- ^ No version string@@ -75,6 +80,7 @@     -- ^ Version "1.0.0"     deriving (Enum, Bounded) +-- | Render a `StandardVersion` as `Text` renderStandardVersion :: StandardVersion -> Text renderStandardVersion NoVersion = "none" renderStandardVersion V_1_0_0   = "1.0.0"@@ -263,6 +269,11 @@       where         l₁ = encode l₀         r₁ = encode r₀+    encode (RecordCompletion l₀ r₀) =+        TList [ TInt 3, TInt 13, l₁, r₁ ]+      where+        l₁ = encode l₀+        r₁ = encode r₀     encode (ListLit _T₀ xs₀)         | null xs₀  = TList [ TInt label, _T₁ ]         | otherwise = TList ([ TInt 4, TNull ] ++ xs₁)@@ -343,18 +354,8 @@         TList [ TInt 15, TInteger (fromIntegral n) ]     encode (IntegerLit n) =         TList [ TInt 16, TInteger n ]-    encode (DoubleLit n64)-        -- cborg always encodes NaN as "7e00"-        | isNaN n64 = THalf n32-        | useHalf   = THalf n32-        | useFloat  = TFloat n32-        | otherwise = TDouble n64-      where-        n32      = double2Float n64-        useFloat = n64 == float2Double n32-        -- the other three cases for Half-floats are 0.0 and the infinities-        useHalf  = or $ fmap (n64 ==) [0.0, infinity, -infinity]-        infinity = 1/0 :: Double+    encode (DoubleLit d) =+        encode d     encode (TextLit (Chunks xys₀ z₀)) =         TList ([ TInt 18 ] ++ xys₁ ++ [ z₁ ])       where@@ -472,6 +473,19 @@ instance ToTerm Void where     encode = absurd +instance ToTerm DhallDouble where+    encode (DhallDouble n64)+        -- cborg always encodes NaN as a half-precision float of value "7e00"+        | useHalf   = THalf n32+        | useFloat  = TFloat n32+        | otherwise = TDouble n64+      where+        n32      = double2Float n64+        useFloat = n64 == float2Double n32+        -- the other four cases for Half-floats are -0.0, 0.0 and the infinities+        useHalf  = n64 == 0.0 || n64 == infinity || n64 == -infinity+        infinity = 1/0 :: Double+ -- | Types that can be decoded from a CBOR `Term` class FromTerm a where     decode :: Term -> Maybe a@@ -593,6 +607,7 @@                 10 -> return CombineTypes                 11 -> return ImportAlt                 12 -> return Equivalent+                13 -> return RecordCompletion                 _  -> empty         return (op l₀ r₀)     decode (TList [ TInt 4, _T₁ ]) = do@@ -693,11 +708,11 @@     decode (TList [ TInt 16, TInteger n ]) = do         return (IntegerLit n)     decode (THalf n) = do-        return (DoubleLit (float2Double n))+        return (DoubleLit (DhallDouble (float2Double n)))     decode (TFloat n) = do-        return (DoubleLit (float2Double n))+        return (DoubleLit (DhallDouble (float2Double n)))     decode (TDouble n) = do-        return (DoubleLit n)+        return (DoubleLit (DhallDouble n))     decode (TList (TInt 18 : xs)) = do         let process (TString x : y₁ : zs) = do                 y₀ <- decode y₁@@ -932,6 +947,9 @@          decode taggedTerm +{-| This indicates that a given CBOR expression did not correspond to a valid+    Dhall expression+-} data DecodingFailure = CBORIsNotDhall Term     deriving (Eq) 

@@ -1,10 +0,0 @@-module Dhall.Binary where--import Codec.CBOR.Term (Term)--import {-# SOURCE #-} Dhall.Core--class ToTerm a where-    encode :: a -> Term--instance ToTerm a => ToTerm (Expr s a)

@@ -1,2390 +1,1384 @@ {-# LANGUAGE BangPatterns       #-}-{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveAnyClass     #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE DeriveTraversable  #-}-{-# LANGUAGE LambdaCase         #-}-{-# LANGUAGE OverloadedStrings  #-}-{-# LANGUAGE RankNTypes         #-}-{-# LANGUAGE RecordWildCards    #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE UnicodeSyntax      #-}-{-# OPTIONS_GHC -Wall #-}--{-| This module contains the core calculus for the Dhall language.--    Dhall is essentially a fork of the @morte@ compiler but with more built-in-    functionality, better error messages, and Haskell integration--}--module Dhall.Core (-    -- * Syntax-      Const(..)-    , Directory(..)-    , File(..)-    , FilePrefix(..)-    , Import(..)-    , ImportHashed(..)-    , ImportMode(..)-    , ImportType(..)-    , URL(..)-    , Scheme(..)-    , Var(..)-    , Chunks(..)-    , Expr(..)--    -- * Normalization-    , Eval.alphaNormalize-    , Eval.normalize-    , normalizeWith-    , normalizeWithM-    , Normalizer-    , NormalizerM-    , ReifiedNormalizer (..)-    , Eval.judgmentallyEqual-    , subst-    , shift-    , isNormalized-    , isNormalizedWith-    , denote-    , renote-    , shallowDenote-    , freeIn--    -- * Pretty-printing-    , pretty--    -- * Optics-    , subExpressions-    , chunkExprs-    , bindingExprs--    -- * Let-blocks-    , multiLet-    , wrapInLets-    , MultiLet(..)-    , Binding(..)-    , makeBinding--    -- * Miscellaneous-    , internalError-    , reservedIdentifiers-    , escapeText-    , pathCharacter-    , throws-    , textShow-    , censorExpression-    , censorText-    ) where--import Control.Applicative (empty)-import Control.DeepSeq (NFData)-import Control.Exception (Exception)-import Control.Monad.IO.Class (MonadIO(..))-import Data.Bifunctor (Bifunctor(..))-import Data.Data (Data)-import Data.Foldable-import Data.Functor.Identity (Identity(..))-import Data.HashSet (HashSet)-import Data.List.NonEmpty (NonEmpty(..))-import Data.String (IsString(..))-import Data.Semigroup (Semigroup(..))-import Data.Sequence (Seq, ViewL(..), ViewR(..))-import Data.Text (Text)-import Data.Text.Prettyprint.Doc (Doc, Pretty)-import Data.Traversable-import Data.Void (Void)-import Dhall.Map (Map)-import Dhall.Set (Set)-import Dhall.Src (Src(..))-import {-# SOURCE #-} Dhall.Pretty.Internal-import GHC.Generics (Generic)-import Instances.TH.Lift ()-import Language.Haskell.TH.Syntax (Lift)-import Lens.Family (over)-import Numeric.Natural (Natural)-import Prelude hiding (succ)-import Unsafe.Coerce (unsafeCoerce)--import qualified Control.Exception-import qualified Control.Monad-import qualified Data.Char-import {-# SOURCE #-} qualified Dhall.Eval  as Eval-import qualified Data.HashSet-import qualified Data.List.NonEmpty-import qualified Data.Sequence-import qualified Data.Set-import qualified Data.Text-import qualified Data.Text.Prettyprint.Doc  as Pretty-import qualified Dhall.Crypto-import qualified Dhall.Map-import qualified Dhall.Set-import qualified Network.URI                as URI-import qualified Text.Printf---{-| Constants for a pure type system--    The axioms are:--> ⊦ Type : Kind-> ⊦ Kind : Sort--    ... and the valid rule pairs are:--> ⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)-> ⊦ Kind ↝ Type : Type  -- Functions from types to terms (type-polymorphic functions)-> ⊦ Sort ↝ Type : Type  -- Functions from kinds to terms-> ⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type-level functions)-> ⊦ Sort ↝ Kind : Sort  -- Functions from kinds to types (kind-polymorphic functions)-> ⊦ Sort ↝ Sort : Sort  -- Functions from kinds to kinds (kind-level functions)--    Note that Dhall does not support functions from terms to types and therefore-    Dhall is not a dependently typed language--}-data Const = Type | Kind | Sort-    deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, NFData)--instance Lift Const--instance Pretty Const where-    pretty = Pretty.unAnnotate . prettyConst--{-| Internal representation of a directory that stores the path components in-    reverse order--    In other words, the directory @\/foo\/bar\/baz@ is encoded as-    @Directory { components = [ "baz", "bar", "foo" ] }@--}-newtype Directory = Directory { components :: [Text] }-    deriving (Eq, Generic, Ord, Show, NFData)--instance Semigroup Directory where-    Directory components₀ <> Directory components₁ =-        Directory (components₁ <> components₀)--instance Pretty Directory where-    pretty (Directory {..}) = foldMap prettyPathComponent (reverse components)--{-| A `File` is a `directory` followed by one additional path component-    representing the `file` name--}-data File = File-    { directory :: Directory-    , file      :: Text-    } deriving (Eq, Generic, Ord, Show, NFData)--instance Pretty File where-    pretty (File {..}) =-            Pretty.pretty directory-        <>  prettyPathComponent file--instance Semigroup File where-    File directory₀ _ <> File directory₁ file =-        File (directory₀ <> directory₁) file---- | The beginning of a file path which anchors subsequent path components-data FilePrefix-    = Absolute-    -- ^ Absolute path-    | Here-    -- ^ Path relative to @.@-    | Parent-    -- ^ Path relative to @..@-    | Home-    -- ^ Path relative to @~@-    deriving (Eq, Generic, Ord, Show, NFData)--instance Pretty FilePrefix where-    pretty Absolute = ""-    pretty Here     = "."-    pretty Parent   = ".."-    pretty Home     = "~"--data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)--data URL = URL-    { scheme    :: Scheme-    , authority :: Text-    , path      :: File-    , query     :: Maybe Text-    , headers   :: Maybe (Expr Src Import)-    } deriving (Eq, Generic, Ord, Show, NFData)--instance Pretty URL where-    pretty (URL {..}) =-            schemeDoc-        <>  "://"-        <>  Pretty.pretty authority-        <>  pathDoc-        <>  queryDoc-        <>  foldMap prettyHeaders headers-      where-        prettyHeaders h = " using " <> Pretty.pretty h--        File {..} = path--        Directory {..} = directory--        pathDoc =-                foldMap prettyURIComponent (reverse components)-            <>  prettyURIComponent file--        schemeDoc = case scheme of-            HTTP  -> "http"-            HTTPS -> "https"--        queryDoc = case query of-            Nothing -> ""-            Just q  -> "?" <> Pretty.pretty q---- | The type of import (i.e. local vs. remote vs. environment)-data ImportType-    = Local FilePrefix File-    -- ^ Local path-    | Remote URL-    -- ^ URL of remote resource and optional headers stored in an import-    | Env  Text-    -- ^ Environment variable-    | Missing-    deriving (Eq, Generic, Ord, Show, NFData)--parent :: File-parent = File { directory = Directory { components = [ ".." ] }, file = "" }--instance Semigroup ImportType where-    Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁)--    Remote (URL { path = path₀, ..}) <> Local Here path₁ =-        Remote (URL { path = path₀ <> path₁, ..})--    Local prefix file₀ <> Local Parent file₁ =-        Local prefix (file₀ <> parent <> file₁)--    Remote (URL { path = path₀, .. }) <> Local Parent path₁ =-        Remote (URL { path = path₀ <> parent <> path₁, .. })--    import₀ <> Remote (URL { headers = headers₀, .. }) =-        Remote (URL { headers = headers₁, .. })-      where-        importHashed₀ = Import (ImportHashed Nothing import₀) Code--        headers₁ = fmap (fmap (importHashed₀ <>)) headers₀--    _ <> import₁ =-        import₁--instance Pretty ImportType where-    pretty (Local prefix file) =-        Pretty.pretty prefix <> Pretty.pretty file--    pretty (Remote url) = Pretty.pretty url--    pretty (Env env) = "env:" <> Pretty.pretty env--    pretty Missing = "missing"---- | How to interpret the import's contents (i.e. as Dhall code or raw text)-data ImportMode = Code | RawText | Location-  deriving (Eq, Generic, Ord, Show, NFData)---- | A `ImportType` extended with an optional hash for semantic integrity checks-data ImportHashed = ImportHashed-    { hash       :: Maybe Dhall.Crypto.SHA256Digest-    , importType :: ImportType-    } deriving (Eq, Generic, Ord, Show, NFData)--instance Semigroup ImportHashed where-    ImportHashed _ importType₀ <> ImportHashed hash importType₁ =-        ImportHashed hash (importType₀ <> importType₁)--instance Pretty ImportHashed where-    pretty (ImportHashed  Nothing p) =-      Pretty.pretty p-    pretty (ImportHashed (Just h) p) =-      Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h)---- | Reference to an external resource-data Import = Import-    { importHashed :: ImportHashed-    , importMode   :: ImportMode-    } deriving (Eq, Generic, Ord, Show, NFData)--instance Semigroup Import where-    Import importHashed₀ _ <> Import importHashed₁ code =-        Import (importHashed₀ <> importHashed₁) code--instance Pretty Import where-    pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix-      where-        suffix :: Text-        suffix = case importMode of-            RawText  -> " as Text"-            Location -> " as Location"-            Code     -> ""--{-| Label for a bound variable--    The `Text` field is the variable's name (i.e. \"@x@\").--    The `Int` field disambiguates variables with the same name if there are-    multiple bound variables of the same name in scope.  Zero refers to the-    nearest bound variable and the index increases by one for each bound-    variable of the same name going outward.  The following diagram may help:-->                               ┌──refers to──┐->                               │             │->                               v             │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0->-> ┌─────────────────refers to─────────────────┐-> │                                           │-> v                                           │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1--    This `Int` behaves like a De Bruijn index in the special case where all-    variables have the same name.--    You can optionally omit the index if it is @0@:-->                               ┌─refers to─┐->                               │           │->                               v           │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x--    Zero indices are omitted when pretty-printing `Var`s and non-zero indices-    appear as a numeric suffix.--}-data Var = V Text !Int-    deriving (Data, Generic, Eq, Ord, Show, NFData)--instance Lift Var--instance IsString Var where-    fromString str = V (fromString str) 0--instance Pretty Var where-    pretty = Pretty.unAnnotate . prettyVar--{-| Syntax tree for expressions--    The @s@ type parameter is used to track the presence or absence of `Src`-    spans:--    * If @s = `Src`@ then the code may contains `Src` spans (either in a `Noted`-      constructor or inline within another constructor, like `Let`)-    * If @s = `Void`@ then the code has no `Src` spans--    The @a@ type parameter is used to track the presence or absence of imports--    * If @a = `Import`@ then the code may contain unresolved `Import`s-    * If @a = `Void`@ then the code has no `Import`s--}-data Expr s a-    -- | > Const c                                  ~  c-    = Const Const-    -- | > Var (V x 0)                              ~  x-    --   > Var (V x n)                              ~  x@n-    | Var Var-    -- | > Lam x     A b                            ~  λ(x : A) -> b-    | Lam Text (Expr s a) (Expr s a)-    -- | > Pi "_" A B                               ~        A  -> B-    --   > Pi x   A B                               ~  ∀(x : A) -> B-    | Pi  Text (Expr s a) (Expr s a)-    -- | > App f a                                  ~  f a-    | App (Expr s a) (Expr s a)-    -- | > Let (Binding _ x _  Nothing  _ r) e      ~  let x     = r in e-    --   > Let (Binding _ x _ (Just t ) _ r) e      ~  let x : t = r in e-    ---    -- The difference between-    ---    -- > let x = a    let y = b in e-    ---    -- and-    ---    -- > let x = a in let y = b in e-    ---    -- is only an additional 'Note' around @'Let' "y" …@ in the second-    -- example.-    ---    -- See 'MultiLet' for a representation of let-blocks that mirrors the-    -- source code more closely.-    | Let (Binding s a) (Expr s a)-    -- | > Annot x t                                ~  x : t-    | Annot (Expr s a) (Expr s a)-    -- | > Bool                                     ~  Bool-    | Bool-    -- | > BoolLit b                                ~  b-    | BoolLit Bool-    -- | > BoolAnd x y                              ~  x && y-    | BoolAnd (Expr s a) (Expr s a)-    -- | > BoolOr  x y                              ~  x || y-    | BoolOr  (Expr s a) (Expr s a)-    -- | > BoolEQ  x y                              ~  x == y-    | BoolEQ  (Expr s a) (Expr s a)-    -- | > BoolNE  x y                              ~  x != y-    | BoolNE  (Expr s a) (Expr s a)-    -- | > BoolIf x y z                             ~  if x then y else z-    | BoolIf (Expr s a) (Expr s a) (Expr s a)-    -- | > Natural                                  ~  Natural-    | Natural-    -- | > NaturalLit n                             ~  n-    | NaturalLit Natural-    -- | > NaturalFold                              ~  Natural/fold-    | NaturalFold-    -- | > NaturalBuild                             ~  Natural/build-    | NaturalBuild-    -- | > NaturalIsZero                            ~  Natural/isZero-    | NaturalIsZero-    -- | > NaturalEven                              ~  Natural/even-    | NaturalEven-    -- | > NaturalOdd                               ~  Natural/odd-    | NaturalOdd-    -- | > NaturalToInteger                         ~  Natural/toInteger-    | NaturalToInteger-    -- | > NaturalShow                              ~  Natural/show-    | NaturalShow-    -- | > NaturalSubtract                          ~  Natural/subtract-    | NaturalSubtract-    -- | > NaturalPlus x y                          ~  x + y-    | NaturalPlus (Expr s a) (Expr s a)-    -- | > NaturalTimes x y                         ~  x * y-    | NaturalTimes (Expr s a) (Expr s a)-    -- | > Integer                                  ~  Integer-    | Integer-    -- | > IntegerLit n                             ~  ±n-    | IntegerLit Integer-    -- | > IntegerShow                              ~  Integer/show-    | IntegerShow-    -- | > IntegerToDouble                          ~  Integer/toDouble-    | IntegerToDouble-    -- | > Double                                   ~  Double-    | Double-    -- | > DoubleLit n                              ~  n-    | DoubleLit Double-    -- | > DoubleShow                               ~  Double/show-    | DoubleShow-    -- | > Text                                     ~  Text-    | Text-    -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~  "t1${e1}t2${e2}t3"-    | TextLit (Chunks s a)-    -- | > TextAppend x y                           ~  x ++ y-    | TextAppend (Expr s a) (Expr s a)-    -- | > TextShow                                 ~  Text/show-    | TextShow-    -- | > List                                     ~  List-    | List-    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : t-    --   > ListLit  Nothing  [x, y, z]              ~  [x, y, z]-    | ListLit (Maybe (Expr s a)) (Seq (Expr s a))-    -- | > ListAppend x y                           ~  x # y-    | ListAppend (Expr s a) (Expr s a)-    -- | > ListBuild                                ~  List/build-    | ListBuild-    -- | > ListFold                                 ~  List/fold-    | ListFold-    -- | > ListLength                               ~  List/length-    | ListLength-    -- | > ListHead                                 ~  List/head-    | ListHead-    -- | > ListLast                                 ~  List/last-    | ListLast-    -- | > ListIndexed                              ~  List/indexed-    | ListIndexed-    -- | > ListReverse                              ~  List/reverse-    | ListReverse-    -- | > Optional                                 ~  Optional-    | Optional-    -- | > Some e                                   ~  Some e-    | Some (Expr s a)-    -- | > None                                     ~  None-    | None-    -- | > OptionalFold                             ~  Optional/fold-    | OptionalFold-    -- | > OptionalBuild                            ~  Optional/build-    | OptionalBuild-    -- | > Record       [(k1, t1), (k2, t2)]        ~  { k1 : t1, k2 : t1 }-    | Record    (Map Text (Expr s a))-    -- | > RecordLit    [(k1, v1), (k2, v2)]        ~  { k1 = v1, k2 = v2 }-    | RecordLit (Map Text (Expr s a))-    -- | > Union        [(k1, Just t1), (k2, Nothing)] ~  < k1 : t1 | k2 >-    | Union     (Map Text (Maybe (Expr s a)))-    -- | > Combine x y                              ~  x ∧ y-    | Combine (Expr s a) (Expr s a)-    -- | > CombineTypes x y                         ~  x ⩓ y-    | CombineTypes (Expr s a) (Expr s a)-    -- | > Prefer x y                               ~  x ⫽ y-    | Prefer (Expr s a) (Expr s a)-    -- | > Merge x y (Just t )                      ~  merge x y : t-    --   > Merge x y  Nothing                       ~  merge x y-    | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))-    -- | > ToMap x (Just t)                         ~  toMap x : t-    --   > ToMap x  Nothing                         ~  toMap x-    | ToMap (Expr s a) (Maybe (Expr s a))-    -- | > Field e x                                ~  e.x-    | Field (Expr s a) Text-    -- | > Project e (Left xs)                      ~  e.{ xs }-    -- | > Project e (Right t)                      ~  e.(t)-    | Project (Expr s a) (Either (Set Text) (Expr s a))-    -- | > Assert e                                 ~  assert : e-    | Assert (Expr s a)-    -- | > Equivalent x y                           ~  x ≡ y-    | Equivalent (Expr s a) (Expr s a)-    -- | > Note s x                                 ~  e-    | Note s (Expr s a)-    -- | > ImportAlt                                ~  e1 ? e2-    | ImportAlt (Expr s a) (Expr s a)-    -- | > Embed import                             ~  import-    | Embed a-    deriving (Foldable, Generic, Traversable, Show, Data, NFData)--- NB: If you add a constructor to Expr, please also update the Arbitrary--- instance in Dhall.Test.QuickCheck.---- | Note that this 'Eq' instance inherits `Double`'s defects, e.g.------ >>> nan = 0/0--- >>> DoubleLit nan == DoubleLit nan--- False-deriving instance (Eq s, Eq a) => Eq (Expr s a)---- | Note that this 'Eq' instance inherits `Double`'s defects, e.g.------ >>> nan = 0/0--- >>> DoubleLit nan <= DoubleLit nan--- False-deriving instance (Ord s, Ord a) => Ord (Expr s a)--instance (Lift s, Lift a, Data s, Data a) => Lift (Expr s a)---- This instance is hand-written due to the fact that deriving--- it does not give us an INLINABLE pragma. We annotate this fmap--- 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 (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 _ 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 e1 e2) = Combine (fmap f e1) (fmap f e2)-  fmap f (CombineTypes e1 e2) = CombineTypes (fmap f e1) (fmap f e2)-  fmap f (Prefer e1 e2) = Prefer (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 (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)-  {-# INLINABLE fmap #-}--instance Applicative (Expr s) where-    pure = Embed--    (<*>) = Control.Monad.ap--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)-      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-    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          >>= k = Combine (a >>= k) (b >>= k)-    CombineTypes a b     >>= k = CombineTypes (a >>= k) (b >>= k)-    Prefer a b           >>= k = Prefer (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)-    Note a b             >>= k = Note a (b >>= k)-    ImportAlt a b        >>= k = ImportAlt (a >>= k) (b >>= k)-    Embed a              >>= k = k a--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 _  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         ) = Combine (first k a) (first k b)-    first k (CombineTypes a b    ) = CombineTypes (first k a) (first k b)-    first k (Prefer a b          ) = Prefer (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 (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--    second = fmap--instance IsString (Expr s a) where-    fromString str = Var (fromString str)---- | The body of an interpolated @Text@ literal-data Chunks s a = Chunks [(Text, Expr s a)] Text-    deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)--instance (Lift s, Lift a, Data s, Data a) => Lift (Chunks s a)--instance Data.Semigroup.Semigroup (Chunks s a) where-    Chunks xysL zL <> Chunks         []    zR =-        Chunks xysL (zL <> zR)-    Chunks xysL zL <> Chunks ((x, y):xysR) zR =-        Chunks (xysL ++ (zL <> x, y):xysR) zR--instance Monoid (Chunks s a) where-    mempty = Chunks [] mempty--#if !(MIN_VERSION_base(4,11,0))-    mappend = (<>)-#endif--instance IsString (Chunks s a) where-    fromString str = Chunks [] (fromString str)--{-  There is a one-to-one correspondence between the builders in this section-    and the sub-parsers in "Dhall.Parser".  Each builder is named after the-    corresponding parser and the relationship between builders exactly matches-    the relationship between parsers.  This leads to the nice emergent property-    of automatically getting all the parentheses and precedences right.--    This approach has one major disadvantage: you can get an infinite loop if-    you add a new constructor to the syntax tree without adding a matching-    case the corresponding builder.--}---- | Generates a syntactically valid Dhall program-instance Pretty a => Pretty (Expr s a) where-    pretty = Pretty.unAnnotate . prettyExpr--{-| `shift` is used by both normalization and type-checking to avoid variable-    capture by shifting variable indices--    For example, suppose that you were to normalize the following expression:--> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x--    If you were to substitute @y@ with @x@ without shifting any variable-    indices, then you would get the following incorrect result:--> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form--    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in-    order to avoid being misinterpreted as the @x@ bound by the innermost-    lambda.  If we perform that `shift` then we get the correct result:--> λ(a : Type) → λ(x : a) → λ(x : a) → x@1--    As a more worked example, suppose that you were to normalize the following-    expression:-->     λ(a : Type)-> →   λ(f : a → a → a)-> →   λ(x : a)-> →   λ(x : a)-> →   (λ(x : a) → f x x@1) x@1--    The correct normalized result would be:-->     λ(a : Type)-> →   λ(f : a → a → a)-> →   λ(x : a)-> →   λ(x : a)-> →   f x@1 x--    The above example illustrates how we need to both increase and decrease-    variable indices as part of substitution:--    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we-      substitute it into the body of the innermost lambda expression in order-      to avoid variable capture.  This substitution changes the body of the-      lambda expression to @(f x\@2 x\@1)@--    * We then remove the innermost lambda and therefore decrease the indices of-      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one-      less @x@ variable is now bound within that scope--    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to-    the indices of all variables named @x@ whose indices are greater than-    @(n + m)@, where @m@ is the number of bound variables of the same name-    within that scope--    In practice, @d@ is always @1@ or @-1@ because we either:--    * increment variables by @1@ to avoid variable capture during substitution-    * decrement variables by @1@ when deleting lambdas after substitution--    @n@ starts off at @0@ when substitution begins and increments every time we-    descend into a lambda or let expression that binds a variable of the same-    name in order to avoid shifting the bound variables by mistake.--}-shift :: Int -> Var -> Expr s a -> Expr s a-shift _ _ (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'-shift d (V x n) (Lam x' _A b) = Lam x' _A' b'-  where-    _A' = shift d (V x n ) _A-    b'  = shift d (V x n') b-      where-        n' = if x == x' then n + 1 else n-shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'-  where-    _A' = shift d (V x n ) _A-    _B' = shift d (V x n') _B-      where-        n' = if x == x' then n + 1 else n-shift d v (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-    e' = shift d (V x n') e-      where-        n' = if x == f then n + 1 else n--    mt' = fmap (fmap (shift d (V x n))) mt-    r'  =             shift d (V x n)  r-shift d v (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 _ _ 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) = Combine a' b'-  where-    a' = shift d v a-    b' = shift d v b-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) = Prefer 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 (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--{-| Substitute all occurrences of a variable with an expression--> subst x C B  ~  B[x := C]--}-subst :: Var -> Expr s a -> Expr s a -> Expr s a-subst _ _ (Const a) = Const a-subst (V x n) e (Lam y _A b) = Lam y _A' b'-  where-    _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 x n) e (Pi y _A _B) = Pi y _A' _B'-  where-    _A' = subst (V x n )                  e  _A-    _B' = subst (V x n') (shift 1 (V y 0) e) _B-    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'-  where-    b' = subst (V x n') (shift 1 (V f 0) e) b-      where-        n' = if x == f then n + 1 else n--    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 _ _ 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) = Combine a' b'-  where-    a' = subst x e a-    b' = subst x e b-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) = Prefer 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 (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--{-| 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-    of the accumulator--    If this function returns `True`, then they will be strict in their-    accumulator since we can guarantee an upper bound on the amount of work to-    normalize the accumulator on each step of the loop.  If this function-    returns `False` then they will be lazy in their accumulator and only-    normalize the final result at the end of the fold--}-boundedType :: Expr s a -> Bool-boundedType Bool             = True-boundedType Natural          = True-boundedType Integer          = True-boundedType Double           = True-boundedType Text             = True-boundedType (App List _)     = False-boundedType (App Optional t) = boundedType t-boundedType (Record kvs)     = all boundedType kvs-boundedType (Union kvs)      = all (all boundedType) kvs-boundedType _                = False---- | 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)-  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  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 a b         ) = Combine (denote a) (denote b)-denote (CombineTypes a b    ) = CombineTypes (denote a) (denote b)-denote (Prefer a b          ) = Prefer (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 (ImportAlt a b       ) = ImportAlt (denote a) (denote b)-denote (Embed a             ) = Embed a---- | The \"opposite\" of `denote`, like @first absurd@ but faster-renote :: Expr Void a -> Expr s a-renote = unsafeCoerce-{-# INLINE renote #-}--shallowDenote :: Expr s a -> Expr s a-shallowDenote (Note _ e) = shallowDenote e-shallowDenote         e  = e--{-| Reduce an expression to its normal form, performing beta reduction and applying-    any custom definitions.--    `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`-    function allows typing of Dhall functions in a custom typing context whereas-    `normalizeWith` allows evaluating Dhall expressions in a custom context.--    To be more precise `normalizeWith` applies the given normalizer when it finds an-    application term that it cannot reduce by other means.--    Note that the context used in normalization will determine the properties of normalization.-    That is, if the functions in custom context are not total then the Dhall language, evaluated-    with those functions is not total either.--    `normalizeWith` can fail with an `error` if you normalize an ill-typed-    expression--}-normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a-normalizeWith (Just ctx) t = runIdentity (normalizeWithM (getReifiedNormalizer ctx) t)-normalizeWith _          t = Eval.normalize t--{-| This function generalizes `normalizeWith` by allowing the custom normalizer-    to use an arbitrary `Monad`--    `normalizeWithM` can fail with an `error` if you normalize an ill-typed-    expression--}-normalizeWithM-    :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)-normalizeWithM ctx e0 = loop (denote e0)- where- loop e =  case e of-    Const k -> pure (Const k)-    Var v -> pure (Var v)-    Lam x _A b -> Lam x <$> _A' <*> b'-      where-        _A' = loop _A-        b'  = loop b-    Pi x _A _B -> Pi x <$> _A' <*> _B'-      where-        _A' = loop _A-        _B' = loop _B-    App f a -> do-      res <- ctx (App f a)-      case res of-          Just e1 -> loop e1-          Nothing -> do-              f' <- loop f-              a' <- loop a-              case f' of-                Lam x _A b₀ -> do--                    let a₂ = shift 1 (V x 0) a'-                    let b₁ = subst (V x 0) a₂ b₀-                    let b₂ = shift (-1) (V x 0) b₁--                    loop b₂-                _ -> do-                  case App f' a' of-                    -- build/fold fusion for `List`-                    App (App ListBuild _) (App (App ListFold _) e') -> loop e'--                    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')))--                    -- build/fold fusion for `Natural`-                    App NaturalBuild (App NaturalFold e') -> loop e'--                    -- build/fold fusion for `Optional`-                    App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'--                    App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do-                      t' <- loop t-                      if boundedType t' then strict else lazy-                      where-                        strict =       strictLoop (fromIntegral n0 :: Integer)-                        lazy   = loop (  lazyLoop (fromIntegral n0 :: Integer))--                        strictLoop !0 = loop zero-                        strictLoop !n = App succ' <$> strictLoop (n - 1) >>= loop--                        lazyLoop !0 = zero-                        lazyLoop !n = App succ' (lazyLoop (n - 1))-                    App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)-                      where-                        succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1))--                        zero = NaturalLit 0-                    App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0))-                    App NaturalEven (NaturalLit n) -> pure (BoolLit (even n))-                    App NaturalOdd (NaturalLit n) -> pure (BoolLit (odd n))-                    App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n))-                    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)-                    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)-                    App IntegerShow (IntegerLit n)-                        | 0 <= n    -> pure (TextLit (Chunks [] ("+" <> Data.Text.pack (show n))))-                        | otherwise -> pure (TextLit (Chunks [] (Data.Text.pack (show n))))-                    -- `(read . show)` is used instead of `fromInteger` because `read` uses the correct rounding rule-                    App IntegerToDouble (IntegerLit n) -> pure (DoubleLit ((read . show) n))-                    App DoubleShow (DoubleLit n) ->-                        pure (TextLit (Chunks [] (Data.Text.pack (show n))))-                    App (App OptionalBuild _A₀) g ->-                        loop (App (App (App g optional) just) nothing)-                      where-                        optional = App Optional _A₀--                        just = Lam "a" _A₀ (Some "a")--                        nothing = App None _A₀-                    App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)-                      where-                        _A₁ = shift 1 "a" _A₀--                        list = App List _A₀--                        cons =-                            Lam "a" _A₀-                                (Lam "as"-                                    (App List _A₁)-                                    (ListAppend (ListLit Nothing (pure "a")) "as")-                                )--                        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-                      where-                        strict =       foldr strictCons strictNil xs-                        lazy   = loop (foldr   lazyCons   lazyNil xs)--                        strictNil = loop nil-                        lazyNil   =      nil--                        strictCons y ys = do-                          App (App cons y) <$> ys >>= loop-                        lazyCons   y ys =       App (App cons y) ys-                    App (App ListLength _) (ListLit _ ys) ->-                        pure (NaturalLit (fromIntegral (Data.Sequence.length ys)))-                    App (App ListHead t) (ListLit _ ys) -> loop o-                      where-                        o = case Data.Sequence.viewl ys of-                                y :< _ -> Some y-                                _      -> App None t-                    App (App ListLast t) (ListLit _ ys) -> loop o-                      where-                        o = case Data.Sequence.viewr ys of-                                _ :> y -> Some y-                                _      -> App None t-                    App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)-                      where-                        as₁ = Data.Sequence.mapWithIndex adapt as₀--                        _A₂ = Record (Dhall.Map.fromList kts)-                          where-                            kts = [ ("index", Natural)-                                  , ("value", _A₀)-                                  ]--                        t | null as₀  = Just (App List _A₂)-                          | otherwise = Nothing--                        adapt n a_ =-                            RecordLit (Dhall.Map.fromList kvs)-                          where-                            kvs = [ ("index", NaturalLit (fromIntegral n))-                                  , ("value", a_)-                                  ]-                    App (App ListReverse _) (ListLit t xs) ->-                        loop (ListLit t (Data.Sequence.reverse xs))--                    App (App OptionalFold t0) x0 -> do-                        t1 <- loop t0-                        let optional = Var (V "optional" 0)-                        let lam term = (Lam "optional"-                                           (Const Type)-                                           (Lam "some"-                                               (Pi "_" t1 optional)-                                               (Lam "none" optional term)))-                        x1 <- loop x0-                        pure $ case x1 of-                            App None _ -> lam (Var (V "none" 0))-                            Some x'    -> lam (App (Var (V "some" 0)) x')-                            _          -> App (App OptionalFold t1) x1--                    App TextShow (TextLit (Chunks [] oldText)) ->-                        loop (TextLit (Chunks [] newText))-                      where-                        newText = textShow oldText-                    _ -> do-                        res2 <- ctx (App f' a')-                        case res2 of-                            Nothing -> pure (App f' a')-                            Just app' -> loop app'-    Let (Binding _ f _ _ _ r) b -> loop b''-      where-        r'  = shift   1  (V f 0) r-        b'  = subst (V f 0) r' b-        b'' = shift (-1) (V f 0) b'-    Annot x _ -> loop x-    Bool -> pure Bool-    BoolLit b -> pure (BoolLit b)-    BoolAnd x y -> decide <$> loop x <*> loop y-      where-        decide (BoolLit True )  r              = r-        decide (BoolLit False)  _              = BoolLit False-        decide  l              (BoolLit True ) = l-        decide  _              (BoolLit False) = BoolLit False-        decide  l               r-            | Eval.judgmentallyEqual l r = l-            | otherwise                  = BoolAnd l r-    BoolOr x y -> decide <$> loop x <*> loop y-      where-        decide (BoolLit False)  r              = r-        decide (BoolLit True )  _              = BoolLit True-        decide  l              (BoolLit False) = l-        decide  _              (BoolLit True ) = BoolLit True-        decide  l               r-            | Eval.judgmentallyEqual l r = l-            | otherwise                  = BoolOr l r-    BoolEQ x y -> decide <$> loop x <*> loop y-      where-        decide (BoolLit True )  r              = r-        decide  l              (BoolLit True ) = l-        decide  l               r-            | Eval.judgmentallyEqual l r = BoolLit True-            | otherwise                  = BoolEQ l r-    BoolNE x y -> decide <$> loop x <*> loop y-      where-        decide (BoolLit False)  r              = r-        decide  l              (BoolLit False) = l-        decide  l               r-            | Eval.judgmentallyEqual l r = BoolLit False-            | otherwise                  = BoolNE l r-    BoolIf bool true false -> decide <$> loop bool <*> loop true <*> loop false-      where-        decide (BoolLit True )  l              _              = l-        decide (BoolLit False)  _              r              = r-        decide  b              (BoolLit True) (BoolLit False) = b-        decide  b               l              r-            | Eval.judgmentallyEqual l r = l-            | otherwise                  = BoolIf b l r-    Natural -> pure Natural-    NaturalLit n -> pure (NaturalLit n)-    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 x y -> decide <$> loop x <*> loop y-      where-        decide (NaturalLit 0)  r             = r-        decide  l             (NaturalLit 0) = l-        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n)-        decide  l              r             = NaturalPlus l r-    NaturalTimes x y -> decide <$> loop x <*> loop y-      where-        decide (NaturalLit 1)  r             = r-        decide  l             (NaturalLit 1) = l-        decide (NaturalLit 0)  _             = NaturalLit 0-        decide  _             (NaturalLit 0) = NaturalLit 0-        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n)-        decide  l              r             = NaturalTimes l r-    Integer -> pure Integer-    IntegerLit n -> pure (IntegerLit n)-    IntegerShow -> pure IntegerShow-    IntegerToDouble -> pure IntegerToDouble-    Double -> pure Double-    DoubleLit n -> pure (DoubleLit n)-    DoubleShow -> pure DoubleShow-    Text -> pure Text-    TextLit (Chunks xys z) -> do-        chunks' <- mconcat <$> chunks-        case chunks' of-            Chunks [("", x)] "" -> pure x-            c                   -> pure (TextLit c)-      where-        chunks =-          ((++ [Chunks [] z]) . concat) <$> traverse process xys--        process (x, y) = do-          y' <- loop y-          case y' of-            TextLit c -> pure [Chunks [] x, c]-            _         -> pure [Chunks [(x, y')] mempty]-    TextAppend x y -> loop (TextLit (Chunks [("", x), ("", y)] ""))-    TextShow -> pure TextShow-    List -> pure List-    ListLit t es-        | Data.Sequence.null es -> ListLit <$> t' <*> es'-        | otherwise             -> ListLit Nothing <$> es'-      where-        t'  = traverse loop t-        es' = traverse loop es-    ListAppend x y -> decide <$> loop x <*> loop y-      where-        decide (ListLit _ m)  r            | Data.Sequence.null m = r-        decide  l            (ListLit _ n) | Data.Sequence.null n = l-        decide (ListLit t m) (ListLit _ n)                        = ListLit t (m <> n)-        decide  l             r                                   = ListAppend l r-    ListBuild -> pure ListBuild-    ListFold -> pure ListFold-    ListLength -> pure ListLength-    ListHead -> pure ListHead-    ListLast -> pure ListLast-    ListIndexed -> pure ListIndexed-    ListReverse -> pure ListReverse-    Optional -> pure Optional-    Some a -> Some <$> a'-      where-        a' = loop a-    None -> pure None-    OptionalFold -> pure OptionalFold-    OptionalBuild -> pure OptionalBuild-    Record kts -> Record . Dhall.Map.sort <$> kts'-      where-        kts' = traverse loop kts-    RecordLit kvs -> RecordLit . Dhall.Map.sort <$> kvs'-      where-        kvs' = traverse loop kvs-    Union kts -> Union . Dhall.Map.sort <$> kts'-      where-        kts' = traverse (traverse loop) kts-    Combine x y -> decide <$> loop x <*> loop y-      where-        decide (RecordLit m) r | Data.Foldable.null m =-            r-        decide l (RecordLit n) | Data.Foldable.null n =-            l-        decide (RecordLit m) (RecordLit n) =-            RecordLit (Dhall.Map.unionWith decide m n)-        decide l r =-            Combine l r-    CombineTypes x y -> decide <$> loop x <*> loop y-      where-        decide (Record m) r | Data.Foldable.null m =-            r-        decide l (Record n) | Data.Foldable.null n =-            l-        decide (Record m) (Record n) =-            Record (Dhall.Map.unionWith decide m n)-        decide l r =-            CombineTypes l r-    Prefer x y -> decide <$> loop x <*> loop y-      where-        decide (RecordLit m) r | Data.Foldable.null m =-            r-        decide l (RecordLit n) | Data.Foldable.null n =-            l-        decide (RecordLit m) (RecordLit n) =-            RecordLit (Dhall.Map.union n m)-        decide l r | Eval.judgmentallyEqual l r =-            l-        decide l r =-            Prefer l r-    Merge x y t      -> do-        x' <- loop x-        y' <- loop y-        case x' of-            RecordLit kvsX ->-                case y' of-                    Field (Union ktsY) kY ->-                        case Dhall.Map.lookup kY ktsY of-                            Just Nothing ->-                                case Dhall.Map.lookup kY kvsX of-                                    Just vX -> return vX-                                    Nothing -> Merge x' y' <$> t'-                            _ ->-                                Merge x' y' <$> t'-                    App (Field (Union ktsY) kY) vY ->-                        case Dhall.Map.lookup kY ktsY of-                            Just (Just _) ->-                                case Dhall.Map.lookup kY kvsX of-                                    Just vX -> loop (App vX vY)-                                    Nothing -> Merge x' y' <$> t'-                            _ ->-                                Merge x' y' <$> t'-                    _ -> Merge x' y' <$> t'-            _ -> Merge x' y' <$> t'-      where-        t' = traverse loop t-    ToMap x t        -> do-        x' <- loop x-        t' <- traverse loop t-        case x' of-            RecordLit kvsX -> do-                let entry (key, value) =-                        RecordLit-                            (Dhall.Map.fromList-                                [ ("mapKey"  , TextLit (Chunks [] key))-                                , ("mapValue", value                  )-                                ]-                            )--                let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))--                let listType = case t' of-                        Just _ | null keyValues ->-                            t'-                        _ ->-                            Nothing--                return (ListLit listType keyValues)-            _ -> do-                return (ToMap x' t')-    Field r x        -> do-        let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)--        r' <- loop r-        case r' of-            RecordLit kvs ->-                case Dhall.Map.lookup x kvs of-                    Just v  -> pure v-                    Nothing -> Field <$> (RecordLit <$> traverse loop kvs) <*> pure x-            Project r_ _ -> loop (Field r_ x)-            Prefer (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of-                Just v -> pure (Field (Prefer (singletonRecordLit v) r_) x)-                Nothing -> loop (Field r_ x)-            Prefer l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of-                Just v -> pure v-                Nothing -> loop (Field l x)-            Combine (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of-                Just v -> pure (Field (Combine (singletonRecordLit v) r_) x)-                Nothing -> loop (Field r_ x)-            Combine l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of-                Just v -> pure (Field (Combine l (singletonRecordLit v)) x)-                Nothing -> loop (Field l x)-            _ -> pure (Field r' x)-    Project x (Left fields)-> do-        x' <- loop x-        let fieldsSet = Dhall.Set.toSet fields-        case x' of-            RecordLit kvs ->-                pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet))-            Project y _ ->-                loop (Project y (Left fields))-            Prefer l (RecordLit rKvs) -> do-                let rKs = Dhall.Map.keysSet rKvs-                let l' = Project l (Left (Dhall.Set.fromSet (Data.Set.difference fieldsSet rKs)))-                let r' = RecordLit (Dhall.Map.restrictKeys rKvs fieldsSet)-                loop (Prefer l' r')-            _ | null fields -> pure (RecordLit mempty)-              | otherwise   -> pure (Project x' (Left (Dhall.Set.sort fields)))-    Project r (Right e1) -> do-        e2 <- loop e1--        case e2 of-            Record kts -> do-                loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))-            _ -> do-                r' <- loop r-                pure (Project r' (Right e2))-    Assert t -> do-        t' <- loop t--        pure (Assert t')-    Equivalent l r -> do-        l' <- loop l-        r' <- loop r--        pure (Equivalent l' r')-    Note _ e' -> loop e'-    ImportAlt l _r -> loop l-    Embed a -> pure (Embed a)--textShow :: Text -> Text-textShow text = "\"" <> Data.Text.concatMap f text <> "\""-  where-    f '"'  = "\\\""-    f '$'  = "\\u0024"-    f '\\' = "\\\\"-    f '\b' = "\\b"-    f '\n' = "\\n"-    f '\r' = "\\r"-    f '\t' = "\\t"-    f '\f' = "\\f"-    f c | c <= '\x1F' = Data.Text.pack (Text.Printf.printf "\\u%04x" (Data.Char.ord c))-        | otherwise   = Data.Text.singleton c---- | Use this to wrap you embedded functions (see `normalizeWith`) to make them---   polymorphic enough to be used.-type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))--type Normalizer a = NormalizerM Identity a---- | A reified 'Normalizer', which can be stored in structures without--- running into impredicative polymorphism.-newtype ReifiedNormalizer a = ReifiedNormalizer-  { getReifiedNormalizer :: Normalizer a }---- | Check if an expression is in a normal form given a context of evaluation.---   Unlike `isNormalized`, this will fully normalize and traverse through the expression.------   It is much more efficient to use `isNormalized`.------  `isNormalizedWith` can fail with an `error` if you check an ill-typed---  expression-isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool-isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e---- | Quickly check if an expression is in normal form------ Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to--- @e == 'normalize' e@.------ Given an ill-typed expression, 'isNormalized' may fail with an error, or--- evaluate to either False or True!-isNormalized :: Eq a => Expr s a -> Bool-isNormalized e0 = loop (denote e0)-  where-    loop e = case e of-      Const _ -> True-      Var _ -> True-      Lam _ a b -> loop a && loop b-      Pi _ a b -> loop a && loop b-      App f a -> loop f && loop a && case App f a of-          App (Lam _ _ _) _ -> False--          -- build/fold fusion for `List`-          App (App ListBuild _) (App (App ListFold _) _) -> False--          -- build/fold fusion for `Natural`-          App NaturalBuild (App NaturalFold _) -> False--          -- build/fold fusion for `Optional`-          App (App OptionalBuild _) (App (App OptionalFold _) _) -> False--          App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False-          App NaturalFold (NaturalLit _) -> False-          App NaturalBuild _ -> False-          App NaturalIsZero (NaturalLit _) -> False-          App NaturalEven (NaturalLit _) -> False-          App NaturalOdd (NaturalLit _) -> False-          App NaturalShow (NaturalLit _) -> False-          App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False-          App (App NaturalSubtract (NaturalLit 0)) _ -> False-          App (App NaturalSubtract _) (NaturalLit 0) -> False-          App (App NaturalSubtract x) y -> not (Eval.judgmentallyEqual x y)-          App NaturalToInteger (NaturalLit _) -> False-          App IntegerShow (IntegerLit _) -> False-          App IntegerToDouble (IntegerLit _) -> False-          App DoubleShow (DoubleLit _) -> False-          App (App OptionalBuild _) _ -> False-          App (App ListBuild _) _ -> False-          App (App ListFold _) (ListLit _ _) -> False-          App (App ListLength _) (ListLit _ _) -> False-          App (App ListHead _) (ListLit _ _) -> False-          App (App ListLast _) (ListLit _ _) -> False-          App (App ListIndexed _) (ListLit _ _) -> False-          App (App ListReverse _) (ListLit _ _) -> False-          App (App OptionalFold _) (Some _) -> False-          App (App OptionalFold _) (App None _) -> False-          App TextShow (TextLit (Chunks [] _)) ->-              False-          _ -> True-      Let _ _ -> False-      Annot _ _ -> False-      Bool -> True-      BoolLit _ -> True-      BoolAnd x y -> loop x && loop y && decide x y-        where-          decide (BoolLit _)  _          = False-          decide  _          (BoolLit _) = False-          decide  l           r          = not (Eval.judgmentallyEqual l r)-      BoolOr x y -> loop x && loop y && decide x y-        where-          decide (BoolLit _)  _          = False-          decide  _          (BoolLit _) = False-          decide  l           r          = not (Eval.judgmentallyEqual l r)-      BoolEQ x y -> loop x && loop y && decide x y-        where-          decide (BoolLit True)  _             = False-          decide  _             (BoolLit True) = False-          decide  l              r             = not (Eval.judgmentallyEqual l r)-      BoolNE x y -> loop x && loop y && decide x y-        where-          decide (BoolLit False)  _               = False-          decide  _              (BoolLit False ) = False-          decide  l               r               = not (Eval.judgmentallyEqual l r)-      BoolIf x y z ->-          loop x && loop y && loop z && decide x y z-        where-          decide (BoolLit _)  _              _              = False-          decide  _          (BoolLit True) (BoolLit False) = False-          decide  _           l              r              = not (Eval.judgmentallyEqual l r)-      Natural -> True-      NaturalLit _ -> True-      NaturalFold -> True-      NaturalBuild -> True-      NaturalIsZero -> True-      NaturalEven -> True-      NaturalOdd -> True-      NaturalShow -> True-      NaturalSubtract -> True-      NaturalToInteger -> True-      NaturalPlus x y -> loop x && loop y && decide x y-        where-          decide (NaturalLit 0)  _             = False-          decide  _             (NaturalLit 0) = False-          decide (NaturalLit _) (NaturalLit _) = False-          decide  _              _             = True-      NaturalTimes x y -> loop x && loop y && decide x y-        where-          decide (NaturalLit 0)  _             = False-          decide  _             (NaturalLit 0) = False-          decide (NaturalLit 1)  _             = False-          decide  _             (NaturalLit 1) = False-          decide (NaturalLit _) (NaturalLit _) = False-          decide  _              _             = True-      Integer -> True-      IntegerLit _ -> True-      IntegerShow -> True-      IntegerToDouble -> True-      Double -> True-      DoubleLit _ -> True-      DoubleShow -> True-      Text -> True-      TextLit (Chunks [("", _)] "") -> False-      TextLit (Chunks xys _) -> all (all check) xys-        where-          check y = loop y && case y of-              TextLit _ -> False-              _         -> True-      TextAppend _ _ -> False-      TextShow -> True-      List -> True-      ListLit t es -> all loop t && all loop es-      ListAppend x y -> loop x && loop y && decide x y-        where-          decide (ListLit _ m)  _            | Data.Sequence.null m = False-          decide  _            (ListLit _ n) | Data.Sequence.null n = False-          decide (ListLit _ _) (ListLit _ _)                        = False-          decide  _             _                                   = True-      ListBuild -> True-      ListFold -> True-      ListLength -> True-      ListHead -> True-      ListLast -> True-      ListIndexed -> True-      ListReverse -> True-      Optional -> True-      Some a -> loop a-      None -> True-      OptionalFold -> True-      OptionalBuild -> True-      Record kts -> Dhall.Map.isSorted kts && all loop kts-      RecordLit kvs -> Dhall.Map.isSorted kvs && all loop kvs-      Union kts -> Dhall.Map.isSorted kts && all (all loop) kts-      Combine x y -> loop x && loop y && decide x y-        where-          decide (RecordLit m) _ | Data.Foldable.null m = False-          decide _ (RecordLit n) | Data.Foldable.null n = False-          decide (RecordLit _) (RecordLit _) = False-          decide  _ _ = True-      CombineTypes x y -> loop x && loop y && decide x y-        where-          decide (Record m) _ | Data.Foldable.null m = False-          decide _ (Record n) | Data.Foldable.null n = False-          decide (Record _) (Record _) = False-          decide  _ _ = True-      Prefer x y -> loop x && loop y && decide x y-        where-          decide (RecordLit m) _ | Data.Foldable.null m = False-          decide _ (RecordLit n) | Data.Foldable.null n = False-          decide (RecordLit _) (RecordLit _) = False-          decide l r = not (Eval.judgmentallyEqual l r)-      Merge x y t -> loop x && loop y && all loop t-      ToMap x t -> case x of-          RecordLit _ -> False-          _ -> loop x && all loop t-      Field r k -> case r of-          RecordLit _ -> False-          Project _ _ -> False-          Prefer (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r-          Prefer _ (RecordLit _) -> False-          Combine (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r-          Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r-          _ -> loop r-      Project r p -> loop r &&-          case p of-              Left s -> case r of-                  RecordLit _ -> False-                  Project _ _ -> False-                  Prefer _ (RecordLit _) -> False-                  _ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s-              Right e' -> case e' of-                  Record _ -> False-                  _ -> loop e'-      Assert t -> loop t-      Equivalent l r -> loop l && loop r-      Note _ e' -> loop e'-      ImportAlt _ _ -> False-      Embed _ -> True--{-| Detect if the given variable is free within the given expression-->>> "x" `freeIn` "x"-True->>> "x" `freeIn` "y"-False->>> "x" `freeIn` Lam "x" (Const Type) "x"-False--}-freeIn :: Eq a => Var -> Expr s a -> Bool-variable@(V var i) `freeIn` expression =-    Dhall.Core.subst variable (Var (V var (i + 1))) strippedExpression-      /= strippedExpression-  where-    denote' :: Expr t b -> Expr () b-    denote' = denote--    strippedExpression = denote' expression--_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 <> "                                                       "-    , "```                                                                             "-    ] )---- | The set of reserved identifiers for the Dhall language-reservedIdentifiers :: HashSet Text-reservedIdentifiers =-    Data.HashSet.fromList-        [ "let"-        , "in"-        , "Type"-        , "Kind"-        , "Sort"-        , "forall"-        , "Bool"-        , "True"-        , "False"-        , "merge"-        , "toMap"-        , "if"-        , "then"-        , "else"-        , "as"-        , "using"-        , "Natural"-        , "Natural/fold"-        , "Natural/build"-        , "Natural/isZero"-        , "Natural/even"-        , "Natural/odd"-        , "Natural/toInteger"-        , "Natural/show"-        , "Natural/subtract"-        , "Integer"-        , "Integer/show"-        , "Integer/toDouble"-        , "Double"-        , "Double/show"-        , "Text"-        , "Text/show"-        , "List"-        , "List/build"-        , "List/fold"-        , "List/length"-        , "List/head"-        , "List/last"-        , "List/indexed"-        , "List/reverse"-        , "Optional"-        , "Some"-        , "None"-        , "Optional/build"-        , "Optional/fold"-        , "NaN"-        , "Infinity"-        ]----- | 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 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 _ 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) =-    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) = Combine <$> f a <*> f b-subExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b-subExpressions f (Prefer a b) = Prefer <$> 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 (Note a b) = Note a <$> f b-subExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r-subExpressions _ (Embed a) = pure (Embed a)--{-| Utility used to implement the @--censor@ flag, by:--    * Replacing all `Src` text with spaces-    * Replacing all `Text` literals inside type errors with spaces--}-censorExpression :: Expr Src a -> Expr Src a-censorExpression (TextLit chunks) = TextLit (censorChunks chunks)-censorExpression (Note src     e) = Note (censorSrc src) (censorExpression e)-censorExpression  e               = over subExpressions censorExpression e--censorChunks :: Chunks Src a -> Chunks Src a-censorChunks (Chunks xys z) = Chunks xys' z'-  where-    z' = censorText z--    xys' = [ (censorText x, censorExpression y) | (x, y) <- xys ]---- | Utility used to censor `Text` by replacing all characters with a space-censorText :: Text -> Text-censorText = Data.Text.map (\_ -> ' ')--censorSrc :: Src -> Src-censorSrc (Src { srcText = oldText, .. }) = Src { srcText = newText, .. }-  where-    newText = censorText oldText---- | A traversal over the immediate sub-expressions in 'Chunks'.-chunkExprs-  :: Applicative f-  => (Expr s a -> f (Expr t b))-  -> Chunks s a -> f (Chunks t b)-chunkExprs f (Chunks chunks final) =-  flip Chunks final <$> traverse (traverse f) chunks--{-| Returns `True` if the given `Char` is valid within an unquoted path-    component--    This is exported for reuse within the @"Dhall.Parser.Token"@ module--}-pathCharacter :: Char -> Bool-pathCharacter c =-         '\x21' == c-    ||  ('\x24' <= c && c <= '\x27')-    ||  ('\x2A' <= c && c <= '\x2B')-    ||  ('\x2D' <= c && c <= '\x2E')-    ||  ('\x30' <= c && c <= '\x3B')-    ||  c == '\x3D'-    ||  ('\x40' <= c && c <= '\x5A')-    ||  ('\x5E' <= c && c <= '\x7A')-    ||  c == '\x7C'-    ||  c == '\x7E'--prettyPathComponent :: Text -> Doc ann-prettyPathComponent text-    | Data.Text.all pathCharacter text =-        "/" <> Pretty.pretty text-    | otherwise =-        "/\"" <> Pretty.pretty text <> "\""--prettyURIComponent :: Text -> Doc ann-prettyURIComponent text =-        Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text--{-| Convenience utility for converting `Either`-based exceptions to `IO`-based-    exceptions--}-throws :: (Exception e, MonadIO io) => Either e a -> io a-throws (Left  e) = liftIO (Control.Exception.throwIO e)-throws (Right r) = return r--{--Instead of converting explicitly between 'Expr's and 'MultiLet', it might-be nicer to use a pattern synonym:--> pattern MultiLet' :: NonEmpty (Binding s a) -> Expr s a -> Expr s a-> pattern MultiLet' as b <- (multiLetFromExpr -> Just (MultiLet as b)) where->   MultiLet' as b = wrapInLets as b->-> multiLetFromExpr :: Expr s a -> Maybe (MultiLet s a)-> multiLetFromExpr = \case->     Let x mA a b -> Just (multiLet x mA a b)->     _ -> Nothing--This works in principle, but GHC as of v8.8.1 doesn't handle it well:-https://gitlab.haskell.org/ghc/ghc/issues/17096--This should be fixed by GHC-8.10, so it might be worth revisiting then.--}--{-| Generate a 'MultiLet' from the contents of a 'Let'.--    In the resulting @'MultiLet' bs e@, @e@ is guaranteed not to be a 'Let',-    but it might be a @('Note' … ('Let' …))@.--    Given parser output, 'multiLet' consolidates @let@s that formed a-    let-block in the original source.--}-multiLet :: Binding s a -> Expr s a -> MultiLet s a-multiLet b0 = \case-    Let b1 e1 ->-        let MultiLet bs e = multiLet b1 e1-        in  MultiLet (Data.List.NonEmpty.cons b0 bs) e-    e -> MultiLet (b0 :| []) e--{-| Wrap let-'Binding's around an 'Expr'.--'wrapInLets' can be understood as an inverse for 'multiLet':--> let MultiLet bs e1 = multiLet b e0->-> wrapInLets bs e1 == Let b e0--}-wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a-wrapInLets bs e = foldr Let e bs--data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a)--{- | Record the binding part of a @let@ expression.--For example,-> let {- A -} x {- B -} : {- C -} Bool = {- D -} True in x-will be instantiated as follows:--* @bindingSrc0@ corresponds to the @A@ comment.-* @variable@ is @"x"@-* @bindingSrc1@ corresponds to the @B@ comment.-* @annotation@ is 'Just' a pair, corresponding to the @C@ comment and @Bool@.-* @bindingSrc2@ corresponds to the @D@ comment.-* @value@ corresponds to @True@.--}-data Binding s a = Binding-    { bindingSrc0 :: Maybe s-    , variable    :: Text-    , bindingSrc1 :: Maybe s-    , annotation  :: Maybe (Maybe s, Expr s a)-    , bindingSrc2 :: Maybe s-    , value       :: Expr s a-    } deriving (Data, Eq, Foldable, Functor, Generic, NFData, Ord, Show, Traversable)--instance Bifunctor Binding where-    first k (Binding src0 a src1 b src2 c) =-        Binding (fmap k src0) a (fmap k src1) (fmap adapt0 b) (fmap k src2) (first k c)-      where-        adapt0 (src3, d) = (fmap k src3, first k d)--    second = fmap--{-| Traverse over the immediate 'Expr' children in a 'Binding'.--}-bindingExprs-  :: (Applicative f)-  => (Expr s a -> f (Expr s b))-  -> Binding s a -> f (Binding s b)-bindingExprs f (Binding s0 n s1 t s2 v) =-  Binding-    <$> pure s0-    <*> pure n-    <*> pure s1-    <*> traverse (traverse f) t-    <*> pure s2-    <*> f v--{-| Construct a 'Binding' with no source information and no type annotation.--}-makeBinding :: Text -> Expr s a -> Binding s a-makeBinding name = Binding Nothing name Nothing Nothing Nothing+{-# LANGUAGE LambdaCase         #-}+{-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE RankNTypes         #-}+{-# LANGUAGE RecordWildCards    #-}++{-| This module contains the core calculus for the Dhall language.++    Dhall is essentially a fork of the @morte@ compiler but with more built-in+    functionality, better error messages, and Haskell integration+-}++module Dhall.Core (+    -- * Syntax+      Const(..)+    , Directory(..)+    , File(..)+    , FilePrefix(..)+    , Import(..)+    , ImportHashed(..)+    , ImportMode(..)+    , ImportType(..)+    , URL(..)+    , Scheme(..)+    , DhallDouble(..)+    , Var(..)+    , Binding(..)+    , makeBinding+    , Chunks(..)+    , Expr(..)++    -- * Normalization+    , alphaNormalize+    , normalize+    , normalizeWith+    , normalizeWithM+    , Normalizer+    , NormalizerM+    , ReifiedNormalizer (..)+    , judgmentallyEqual+    , subst+    , shift+    , isNormalized+    , isNormalizedWith+    , denote+    , renote+    , shallowDenote+    , freeIn++    -- * Pretty-printing+    , pretty++    -- * Optics+    , subExpressions+    , chunkExprs+    , bindingExprs++    -- * Let-blocks+    , multiLet+    , wrapInLets+    , MultiLet(..)++    -- * Miscellaneous+    , internalError+    , reservedIdentifiers+    , escapeText+    , pathCharacter+    , throws+    , Eval.textShow+    , censorExpression+    , censorText+    ) where++import Control.Applicative (empty)+import Control.Exception (Exception)+import Control.Monad.IO.Class (MonadIO(..))+import Data.Foldable+import Data.Functor.Identity (Identity(..))+import Data.Semigroup (Semigroup(..))+import Data.Sequence (ViewL(..), ViewR(..))+import Data.Text (Text)+import Data.Text.Prettyprint.Doc (Pretty)+import Data.Traversable+import Dhall.Src (Src(..))+import Dhall.Syntax+import Dhall.Pretty.Internal+import Instances.TH.Lift ()+import Lens.Family (over)+import Prelude hiding (succ)++import qualified Control.Exception+import qualified Dhall.Eval    as Eval+import qualified Data.Sequence+import qualified Data.Set+import qualified Data.Text+import qualified Dhall.Map+import qualified Dhall.Set++{-| Returns `True` if two expressions are α-equivalent and β-equivalent and+    `False` otherwise++    `judgmentallyEqual` can fail with an `error` if you compare ill-typed+    expressions+-}+judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool+judgmentallyEqual = Eval.judgmentallyEqual+{-# INLINE judgmentallyEqual #-}++{-| `shift` is used by both normalization and type-checking to avoid variable+    capture by shifting variable indices++    For example, suppose that you were to normalize the following expression:++> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x++    If you were to substitute @y@ with @x@ without shifting any variable+    indices, then you would get the following incorrect result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form++    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in+    order to avoid being misinterpreted as the @x@ bound by the innermost+    lambda.  If we perform that `shift` then we get the correct result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x@1++    As a more worked example, suppose that you were to normalize the following+    expression:++>     λ(a : Type)+> →   λ(f : a → a → a)+> →   λ(x : a)+> →   λ(x : a)+> →   (λ(x : a) → f x x@1) x@1++    The correct normalized result would be:++>     λ(a : Type)+> →   λ(f : a → a → a)+> →   λ(x : a)+> →   λ(x : a)+> →   f x@1 x++    The above example illustrates how we need to both increase and decrease+    variable indices as part of substitution:++    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we+      substitute it into the body of the innermost lambda expression in order+      to avoid variable capture.  This substitution changes the body of the+      lambda expression to @(f x\@2 x\@1)@++    * We then remove the innermost lambda and therefore decrease the indices of+      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one+      less @x@ variable is now bound within that scope++    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to+    the indices of all variables named @x@ whose indices are greater than+    @(n + m)@, where @m@ is the number of bound variables of the same name+    within that scope++    In practice, @d@ is always @1@ or @-1@ because we either:++    * increment variables by @1@ to avoid variable capture during substitution+    * decrement variables by @1@ when deleting lambdas after substitution++    @n@ starts off at @0@ when substitution begins and increments every time we+    descend into a lambda or let expression that binds a variable of the same+    name in order to avoid shifting the bound variables by mistake.+-}+shift :: Int -> Var -> Expr s a -> Expr s a+shift _ _ (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'+shift d (V x n) (Lam x' _A b) = Lam x' _A' b'+  where+    _A' = shift d (V x n ) _A+    b'  = shift d (V x n') b+      where+        n' = if x == x' then n + 1 else n+shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'+  where+    _A' = shift d (V x n ) _A+    _B' = shift d (V x n') _B+      where+        n' = if x == x' then n + 1 else n+shift d v (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+    e' = shift d (V x n') e+      where+        n' = if x == f then n + 1 else n++    mt' = fmap (fmap (shift d (V x n))) mt+    r'  =             shift d (V x n)  r+shift d v (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 _ _ 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) = Combine a' b'+  where+    a' = shift d v a+    b' = shift d v b+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) = Prefer a' b'+  where+    a' = shift d v a+    b' = shift d v b+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 (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++{-| Substitute all occurrences of a variable with an expression++> subst x C B  ~  B[x := C]+-}+subst :: Var -> Expr s a -> Expr s a -> Expr s a+subst _ _ (Const a) = Const a+subst (V x n) e (Lam y _A b) = Lam y _A' b'+  where+    _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 x n) e (Pi y _A _B) = Pi y _A' _B'+  where+    _A' = subst (V x n )                  e  _A+    _B' = subst (V x n') (shift 1 (V y 0) e) _B+    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'+  where+    b' = subst (V x n') (shift 1 (V f 0) e) b+      where+        n' = if x == f then n + 1 else n++    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 _ _ 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) = Combine a' b'+  where+    a' = subst x e a+    b' = subst x e b+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) = Prefer a' b'+  where+    a' = subst x e a+    b' = subst x e b+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 (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++{-| 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+    of the accumulator++    If this function returns `True`, then they will be strict in their+    accumulator since we can guarantee an upper bound on the amount of work to+    normalize the accumulator on each step of the loop.  If this function+    returns `False` then they will be lazy in their accumulator and only+    normalize the final result at the end of the fold+-}+boundedType :: Expr s a -> Bool+boundedType Bool             = True+boundedType Natural          = True+boundedType Integer          = True+boundedType Double           = True+boundedType Text             = True+boundedType (App List _)     = False+boundedType (App Optional t) = boundedType t+boundedType (Record kvs)     = all boundedType kvs+boundedType (Union kvs)      = all (all boundedType) kvs+boundedType _                = False++{-| α-normalize an expression by renaming all bound variables to @\"_\"@ and+    using De Bruijn indices to distinguish them++>>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x"))))+Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1)))))++    α-normalization does not affect free variables:++>>> alphaNormalize "x"+Var (V "x" 0)++-}+alphaNormalize :: Expr s a -> Expr s a+alphaNormalize = Eval.alphaNormalize+{-# INLINE alphaNormalize #-}++{-| Reduce an expression to its normal form, performing beta reduction++    `normalize` does not type-check the expression.  You may want to type-check+    expressions before normalizing them since normalization can convert an+    ill-typed expression into a well-typed expression.++    `normalize` can also fail with `error` if you normalize an ill-typed+    expression+-}+normalize :: Eq a => Expr s a -> Expr t a+normalize = Eval.normalize+{-# INLINE normalize #-}++{-| Reduce an expression to its normal form, performing beta reduction and applying+    any custom definitions.++    `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`+    function allows typing of Dhall functions in a custom typing context whereas+    `normalizeWith` allows evaluating Dhall expressions in a custom context.++    To be more precise `normalizeWith` applies the given normalizer when it finds an+    application term that it cannot reduce by other means.++    Note that the context used in normalization will determine the properties of normalization.+    That is, if the functions in custom context are not total then the Dhall language, evaluated+    with those functions is not total either.++    `normalizeWith` can fail with an `error` if you normalize an ill-typed+    expression+-}+normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a+normalizeWith (Just ctx) t = runIdentity (normalizeWithM (getReifiedNormalizer ctx) t)+normalizeWith _          t = Eval.normalize t++{-| This function generalizes `normalizeWith` by allowing the custom normalizer+    to use an arbitrary `Monad`++    `normalizeWithM` can fail with an `error` if you normalize an ill-typed+    expression+-}+normalizeWithM+    :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)+normalizeWithM ctx e0 = loop (denote e0)+ where+ loop e =  case e of+    Const k -> pure (Const k)+    Var v -> pure (Var v)+    Lam x _A b -> Lam x <$> _A' <*> b'+      where+        _A' = loop _A+        b'  = loop b+    Pi x _A _B -> Pi x <$> _A' <*> _B'+      where+        _A' = loop _A+        _B' = loop _B+    App f a -> do+      res <- ctx (App f a)+      case res of+          Just e1 -> loop e1+          Nothing -> do+              f' <- loop f+              a' <- loop a+              case f' of+                Lam x _A b₀ -> do++                    let a₂ = shift 1 (V x 0) a'+                    let b₁ = subst (V x 0) a₂ b₀+                    let b₂ = shift (-1) (V x 0) b₁++                    loop b₂+                _ -> do+                  case App f' a' of+                    -- build/fold fusion for `List`+                    App (App ListBuild _) (App (App ListFold _) e') -> loop e'++                    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')))++                    -- build/fold fusion for `Natural`+                    App NaturalBuild (App NaturalFold e') -> loop e'++                    -- build/fold fusion for `Optional`+                    App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'++                    App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do+                      t' <- loop t+                      if boundedType t' then strict else lazy+                      where+                        strict =       strictLoop (fromIntegral n0 :: Integer)+                        lazy   = loop (  lazyLoop (fromIntegral n0 :: Integer))++                        strictLoop !0 = loop zero+                        strictLoop !n = App succ' <$> strictLoop (n - 1) >>= loop++                        lazyLoop !0 = zero+                        lazyLoop !n = App succ' (lazyLoop (n - 1))+                    App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)+                      where+                        succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1))++                        zero = NaturalLit 0+                    App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0))+                    App NaturalEven (NaturalLit n) -> pure (BoolLit (even n))+                    App NaturalOdd (NaturalLit n) -> pure (BoolLit (odd n))+                    App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n))+                    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)+                    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)+                    App IntegerShow (IntegerLit n)+                        | 0 <= n    -> pure (TextLit (Chunks [] ("+" <> Data.Text.pack (show n))))+                        | otherwise -> pure (TextLit (Chunks [] (Data.Text.pack (show n))))+                    -- `(read . show)` is used instead of `fromInteger` because `read` uses+                    -- the correct rounding rule.+                    -- See https://gitlab.haskell.org/ghc/ghc/issues/17231.+                    App IntegerToDouble (IntegerLit n) -> pure (DoubleLit ((DhallDouble . read . show) n))+                    App DoubleShow (DoubleLit (DhallDouble n)) ->+                        pure (TextLit (Chunks [] (Data.Text.pack (show n))))+                    App (App OptionalBuild _A₀) g ->+                        loop (App (App (App g optional) just) nothing)+                      where+                        optional = App Optional _A₀++                        just = Lam "a" _A₀ (Some "a")++                        nothing = App None _A₀+                    App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)+                      where+                        _A₁ = shift 1 "a" _A₀++                        list = App List _A₀++                        cons =+                            Lam "a" _A₀+                                (Lam "as"+                                    (App List _A₁)+                                    (ListAppend (ListLit Nothing (pure "a")) "as")+                                )++                        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+                      where+                        strict =       foldr strictCons strictNil xs+                        lazy   = loop (foldr   lazyCons   lazyNil xs)++                        strictNil = loop nil+                        lazyNil   =      nil++                        strictCons y ys = do+                          App (App cons y) <$> ys >>= loop+                        lazyCons   y ys =       App (App cons y) ys+                    App (App ListLength _) (ListLit _ ys) ->+                        pure (NaturalLit (fromIntegral (Data.Sequence.length ys)))+                    App (App ListHead t) (ListLit _ ys) -> loop o+                      where+                        o = case Data.Sequence.viewl ys of+                                y :< _ -> Some y+                                _      -> App None t+                    App (App ListLast t) (ListLit _ ys) -> loop o+                      where+                        o = case Data.Sequence.viewr ys of+                                _ :> y -> Some y+                                _      -> App None t+                    App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)+                      where+                        as₁ = Data.Sequence.mapWithIndex adapt as₀++                        _A₂ = Record (Dhall.Map.fromList kts)+                          where+                            kts = [ ("index", Natural)+                                  , ("value", _A₀)+                                  ]++                        t | null as₀  = Just (App List _A₂)+                          | otherwise = Nothing++                        adapt n a_ =+                            RecordLit (Dhall.Map.fromList kvs)+                          where+                            kvs = [ ("index", NaturalLit (fromIntegral n))+                                  , ("value", a_)+                                  ]+                    App (App ListReverse _) (ListLit t xs) ->+                        loop (ListLit t (Data.Sequence.reverse xs))++                    App (App OptionalFold t0) x0 -> do+                        t1 <- loop t0+                        let optional = Var (V "optional" 0)+                        let lam term = (Lam "optional"+                                           (Const Type)+                                           (Lam "some"+                                               (Pi "_" t1 optional)+                                               (Lam "none" optional term)))+                        x1 <- loop x0+                        pure $ case x1 of+                            App None _ -> lam (Var (V "none" 0))+                            Some x'    -> lam (App (Var (V "some" 0)) x')+                            _          -> App (App OptionalFold t1) x1++                    App TextShow (TextLit (Chunks [] oldText)) ->+                        loop (TextLit (Chunks [] newText))+                      where+                        newText = Eval.textShow oldText+                    _ -> do+                        res2 <- ctx (App f' a')+                        case res2 of+                            Nothing -> pure (App f' a')+                            Just app' -> loop app'+    Let (Binding _ f _ _ _ r) b -> loop b''+      where+        r'  = shift   1  (V f 0) r+        b'  = subst (V f 0) r' b+        b'' = shift (-1) (V f 0) b'+    Annot x _ -> loop x+    Bool -> pure Bool+    BoolLit b -> pure (BoolLit b)+    BoolAnd x y -> decide <$> loop x <*> loop y+      where+        decide (BoolLit True )  r              = r+        decide (BoolLit False)  _              = BoolLit False+        decide  l              (BoolLit True ) = l+        decide  _              (BoolLit False) = BoolLit False+        decide  l               r+            | Eval.judgmentallyEqual l r = l+            | otherwise                  = BoolAnd l r+    BoolOr x y -> decide <$> loop x <*> loop y+      where+        decide (BoolLit False)  r              = r+        decide (BoolLit True )  _              = BoolLit True+        decide  l              (BoolLit False) = l+        decide  _              (BoolLit True ) = BoolLit True+        decide  l               r+            | Eval.judgmentallyEqual l r = l+            | otherwise                  = BoolOr l r+    BoolEQ x y -> decide <$> loop x <*> loop y+      where+        decide (BoolLit True )  r              = r+        decide  l              (BoolLit True ) = l+        decide  l               r+            | Eval.judgmentallyEqual l r = BoolLit True+            | otherwise                  = BoolEQ l r+    BoolNE x y -> decide <$> loop x <*> loop y+      where+        decide (BoolLit False)  r              = r+        decide  l              (BoolLit False) = l+        decide  l               r+            | Eval.judgmentallyEqual l r = BoolLit False+            | otherwise                  = BoolNE l r+    BoolIf bool true false -> decide <$> loop bool <*> loop true <*> loop false+      where+        decide (BoolLit True )  l              _              = l+        decide (BoolLit False)  _              r              = r+        decide  b              (BoolLit True) (BoolLit False) = b+        decide  b               l              r+            | Eval.judgmentallyEqual l r = l+            | otherwise                  = BoolIf b l r+    Natural -> pure Natural+    NaturalLit n -> pure (NaturalLit n)+    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 x y -> decide <$> loop x <*> loop y+      where+        decide (NaturalLit 0)  r             = r+        decide  l             (NaturalLit 0) = l+        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n)+        decide  l              r             = NaturalPlus l r+    NaturalTimes x y -> decide <$> loop x <*> loop y+      where+        decide (NaturalLit 1)  r             = r+        decide  l             (NaturalLit 1) = l+        decide (NaturalLit 0)  _             = NaturalLit 0+        decide  _             (NaturalLit 0) = NaturalLit 0+        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n)+        decide  l              r             = NaturalTimes l r+    Integer -> pure Integer+    IntegerLit n -> pure (IntegerLit n)+    IntegerShow -> pure IntegerShow+    IntegerToDouble -> pure IntegerToDouble+    Double -> pure Double+    DoubleLit n -> pure (DoubleLit n)+    DoubleShow -> pure DoubleShow+    Text -> pure Text+    TextLit (Chunks xys z) -> do+        chunks' <- mconcat <$> chunks+        case chunks' of+            Chunks [("", x)] "" -> pure x+            c                   -> pure (TextLit c)+      where+        chunks =+          ((++ [Chunks [] z]) . concat) <$> traverse process xys++        process (x, y) = do+          y' <- loop y+          case y' of+            TextLit c -> pure [Chunks [] x, c]+            _         -> pure [Chunks [(x, y')] mempty]+    TextAppend x y -> loop (TextLit (Chunks [("", x), ("", y)] ""))+    TextShow -> pure TextShow+    List -> pure List+    ListLit t es+        | Data.Sequence.null es -> ListLit <$> t' <*> pure Data.Sequence.empty+        | otherwise             -> ListLit Nothing <$> es'+      where+        t'  = traverse loop t+        es' = traverse loop es+    ListAppend x y -> decide <$> loop x <*> loop y+      where+        decide (ListLit _ m)  r            | Data.Sequence.null m = r+        decide  l            (ListLit _ n) | Data.Sequence.null n = l+        decide (ListLit t m) (ListLit _ n)                        = ListLit t (m <> n)+        decide  l             r                                   = ListAppend l r+    ListBuild -> pure ListBuild+    ListFold -> pure ListFold+    ListLength -> pure ListLength+    ListHead -> pure ListHead+    ListLast -> pure ListLast+    ListIndexed -> pure ListIndexed+    ListReverse -> pure ListReverse+    Optional -> pure Optional+    Some a -> Some <$> a'+      where+        a' = loop a+    None -> pure None+    OptionalFold -> pure OptionalFold+    OptionalBuild -> pure OptionalBuild+    Record kts -> Record . Dhall.Map.sort <$> kts'+      where+        kts' = traverse loop kts+    RecordLit kvs -> RecordLit . Dhall.Map.sort <$> kvs'+      where+        kvs' = traverse loop kvs+    Union kts -> Union . Dhall.Map.sort <$> kts'+      where+        kts' = traverse (traverse loop) kts+    Combine x y -> decide <$> loop x <*> loop y+      where+        decide (RecordLit m) r | Data.Foldable.null m =+            r+        decide l (RecordLit n) | Data.Foldable.null n =+            l+        decide (RecordLit m) (RecordLit n) =+            RecordLit (Dhall.Map.unionWith decide m n)+        decide l r =+            Combine l r+    CombineTypes x y -> decide <$> loop x <*> loop y+      where+        decide (Record m) r | Data.Foldable.null m =+            r+        decide l (Record n) | Data.Foldable.null n =+            l+        decide (Record m) (Record n) =+            Record (Dhall.Map.unionWith decide m n)+        decide l r =+            CombineTypes l r+    Prefer x y -> decide <$> loop x <*> loop y+      where+        decide (RecordLit m) r | Data.Foldable.null m =+            r+        decide l (RecordLit n) | Data.Foldable.null n =+            l+        decide (RecordLit m) (RecordLit n) =+            RecordLit (Dhall.Map.union n m)+        decide l r | Eval.judgmentallyEqual l r =+            l+        decide l r =+            Prefer l r+    RecordCompletion x y -> do+        loop (Annot (Prefer (Field x "default") y) (Field x "Type"))+    Merge x y t      -> do+        x' <- loop x+        y' <- loop y+        case x' of+            RecordLit kvsX ->+                case y' of+                    Field (Union ktsY) kY ->+                        case Dhall.Map.lookup kY ktsY of+                            Just Nothing ->+                                case Dhall.Map.lookup kY kvsX of+                                    Just vX -> return vX+                                    Nothing -> Merge x' y' <$> t'+                            _ ->+                                Merge x' y' <$> t'+                    App (Field (Union ktsY) kY) vY ->+                        case Dhall.Map.lookup kY ktsY of+                            Just (Just _) ->+                                case Dhall.Map.lookup kY kvsX of+                                    Just vX -> loop (App vX vY)+                                    Nothing -> Merge x' y' <$> t'+                            _ ->+                                Merge x' y' <$> t'+                    _ -> Merge x' y' <$> t'+            _ -> Merge x' y' <$> t'+      where+        t' = traverse loop t+    ToMap x t        -> do+        x' <- loop x+        t' <- traverse loop t+        case x' of+            RecordLit kvsX -> do+                let entry (key, value) =+                        RecordLit+                            (Dhall.Map.fromList+                                [ ("mapKey"  , TextLit (Chunks [] key))+                                , ("mapValue", value                  )+                                ]+                            )++                let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))++                let listType = case t' of+                        Just _ | null keyValues ->+                            t'+                        _ ->+                            Nothing++                return (ListLit listType keyValues)+            _ -> do+                return (ToMap x' t')+    Field r x        -> do+        let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)++        r' <- loop r+        case r' of+            RecordLit kvs ->+                case Dhall.Map.lookup x kvs of+                    Just v  -> pure v+                    Nothing -> Field <$> (RecordLit <$> traverse loop kvs) <*> pure x+            Project r_ _ -> loop (Field r_ x)+            Prefer (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of+                Just v -> pure (Field (Prefer (singletonRecordLit v) r_) x)+                Nothing -> loop (Field r_ x)+            Prefer l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of+                Just v -> pure v+                Nothing -> loop (Field l x)+            Combine (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of+                Just v -> pure (Field (Combine (singletonRecordLit v) r_) x)+                Nothing -> loop (Field r_ x)+            Combine l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of+                Just v -> pure (Field (Combine l (singletonRecordLit v)) x)+                Nothing -> loop (Field l x)+            _ -> pure (Field r' x)+    Project x (Left fields)-> do+        x' <- loop x+        let fieldsSet = Dhall.Set.toSet fields+        case x' of+            RecordLit kvs ->+                pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet))+            Project y _ ->+                loop (Project y (Left fields))+            Prefer l (RecordLit rKvs) -> do+                let rKs = Dhall.Map.keysSet rKvs+                let l' = Project l (Left (Dhall.Set.fromSet (Data.Set.difference fieldsSet rKs)))+                let r' = RecordLit (Dhall.Map.restrictKeys rKvs fieldsSet)+                loop (Prefer l' r')+            _ | null fields -> pure (RecordLit mempty)+              | otherwise   -> pure (Project x' (Left (Dhall.Set.sort fields)))+    Project r (Right e1) -> do+        e2 <- loop e1++        case e2 of+            Record kts -> do+                loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))+            _ -> do+                r' <- loop r+                pure (Project r' (Right e2))+    Assert t -> do+        t' <- loop t++        pure (Assert t')+    Equivalent l r -> do+        l' <- loop l+        r' <- loop r++        pure (Equivalent l' r')+    Note _ e' -> loop e'+    ImportAlt l _r -> loop l+    Embed a -> pure (Embed a)++-- | Use this to wrap you embedded functions (see `normalizeWith`) to make them+--   polymorphic enough to be used.+type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))++-- | An variation on `NormalizerM` for pure normalizers+type Normalizer a = NormalizerM Identity a++-- | A reified 'Normalizer', which can be stored in structures without+-- running into impredicative polymorphism.+newtype ReifiedNormalizer a = ReifiedNormalizer+  { getReifiedNormalizer :: Normalizer a }++-- | Check if an expression is in a normal form given a context of evaluation.+--   Unlike `isNormalized`, this will fully normalize and traverse through the expression.+--+--   It is much more efficient to use `isNormalized`.+--+--  `isNormalizedWith` can fail with an `error` if you check an ill-typed+--  expression+isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool+isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e++-- | Quickly check if an expression is in normal form+--+-- Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to+-- @e == 'normalize' e@.+--+-- Given an ill-typed expression, 'isNormalized' may fail with an error, or+-- evaluate to either False or True!+isNormalized :: Eq a => Expr s a -> Bool+isNormalized e0 = loop (denote e0)+  where+    loop e = case e of+      Const _ -> True+      Var _ -> True+      Lam _ a b -> loop a && loop b+      Pi _ a b -> loop a && loop b+      App f a -> loop f && loop a && case App f a of+          App (Lam _ _ _) _ -> False++          -- build/fold fusion for `List`+          App (App ListBuild _) (App (App ListFold _) _) -> False++          -- build/fold fusion for `Natural`+          App NaturalBuild (App NaturalFold _) -> False++          -- build/fold fusion for `Optional`+          App (App OptionalBuild _) (App (App OptionalFold _) _) -> False++          App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False+          App NaturalFold (NaturalLit _) -> False+          App NaturalBuild _ -> False+          App NaturalIsZero (NaturalLit _) -> False+          App NaturalEven (NaturalLit _) -> False+          App NaturalOdd (NaturalLit _) -> False+          App NaturalShow (NaturalLit _) -> False+          App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False+          App (App NaturalSubtract (NaturalLit 0)) _ -> False+          App (App NaturalSubtract _) (NaturalLit 0) -> False+          App (App NaturalSubtract x) y -> not (Eval.judgmentallyEqual x y)+          App NaturalToInteger (NaturalLit _) -> False+          App IntegerShow (IntegerLit _) -> False+          App IntegerToDouble (IntegerLit _) -> False+          App DoubleShow (DoubleLit _) -> False+          App (App OptionalBuild _) _ -> False+          App (App ListBuild _) _ -> False+          App (App ListFold _) (ListLit _ _) -> False+          App (App ListLength _) (ListLit _ _) -> False+          App (App ListHead _) (ListLit _ _) -> False+          App (App ListLast _) (ListLit _ _) -> False+          App (App ListIndexed _) (ListLit _ _) -> False+          App (App ListReverse _) (ListLit _ _) -> False+          App (App OptionalFold _) (Some _) -> False+          App (App OptionalFold _) (App None _) -> False+          App TextShow (TextLit (Chunks [] _)) ->+              False+          _ -> True+      Let _ _ -> False+      Annot _ _ -> False+      Bool -> True+      BoolLit _ -> True+      BoolAnd x y -> loop x && loop y && decide x y+        where+          decide (BoolLit _)  _          = False+          decide  _          (BoolLit _) = False+          decide  l           r          = not (Eval.judgmentallyEqual l r)+      BoolOr x y -> loop x && loop y && decide x y+        where+          decide (BoolLit _)  _          = False+          decide  _          (BoolLit _) = False+          decide  l           r          = not (Eval.judgmentallyEqual l r)+      BoolEQ x y -> loop x && loop y && decide x y+        where+          decide (BoolLit True)  _             = False+          decide  _             (BoolLit True) = False+          decide  l              r             = not (Eval.judgmentallyEqual l r)+      BoolNE x y -> loop x && loop y && decide x y+        where+          decide (BoolLit False)  _               = False+          decide  _              (BoolLit False ) = False+          decide  l               r               = not (Eval.judgmentallyEqual l r)+      BoolIf x y z ->+          loop x && loop y && loop z && decide x y z+        where+          decide (BoolLit _)  _              _              = False+          decide  _          (BoolLit True) (BoolLit False) = False+          decide  _           l              r              = not (Eval.judgmentallyEqual l r)+      Natural -> True+      NaturalLit _ -> True+      NaturalFold -> True+      NaturalBuild -> True+      NaturalIsZero -> True+      NaturalEven -> True+      NaturalOdd -> True+      NaturalShow -> True+      NaturalSubtract -> True+      NaturalToInteger -> True+      NaturalPlus x y -> loop x && loop y && decide x y+        where+          decide (NaturalLit 0)  _             = False+          decide  _             (NaturalLit 0) = False+          decide (NaturalLit _) (NaturalLit _) = False+          decide  _              _             = True+      NaturalTimes x y -> loop x && loop y && decide x y+        where+          decide (NaturalLit 0)  _             = False+          decide  _             (NaturalLit 0) = False+          decide (NaturalLit 1)  _             = False+          decide  _             (NaturalLit 1) = False+          decide (NaturalLit _) (NaturalLit _) = False+          decide  _              _             = True+      Integer -> True+      IntegerLit _ -> True+      IntegerShow -> True+      IntegerToDouble -> True+      Double -> True+      DoubleLit _ -> True+      DoubleShow -> True+      Text -> True+      TextLit (Chunks [("", _)] "") -> False+      TextLit (Chunks xys _) -> all (all check) xys+        where+          check y = loop y && case y of+              TextLit _ -> False+              _         -> True+      TextAppend _ _ -> False+      TextShow -> True+      List -> True+      ListLit t es -> all loop t && all loop es+      ListAppend x y -> loop x && loop y && decide x y+        where+          decide (ListLit _ m)  _            | Data.Sequence.null m = False+          decide  _            (ListLit _ n) | Data.Sequence.null n = False+          decide (ListLit _ _) (ListLit _ _)                        = False+          decide  _             _                                   = True+      ListBuild -> True+      ListFold -> True+      ListLength -> True+      ListHead -> True+      ListLast -> True+      ListIndexed -> True+      ListReverse -> True+      Optional -> True+      Some a -> loop a+      None -> True+      OptionalFold -> True+      OptionalBuild -> True+      Record kts -> Dhall.Map.isSorted kts && all loop kts+      RecordLit kvs -> Dhall.Map.isSorted kvs && all loop kvs+      Union kts -> Dhall.Map.isSorted kts && all (all loop) kts+      Combine x y -> loop x && loop y && decide x y+        where+          decide (RecordLit m) _ | Data.Foldable.null m = False+          decide _ (RecordLit n) | Data.Foldable.null n = False+          decide (RecordLit _) (RecordLit _) = False+          decide  _ _ = True+      CombineTypes x y -> loop x && loop y && decide x y+        where+          decide (Record m) _ | Data.Foldable.null m = False+          decide _ (Record n) | Data.Foldable.null n = False+          decide (Record _) (Record _) = False+          decide  _ _ = True+      Prefer x y -> loop x && loop y && decide x y+        where+          decide (RecordLit m) _ | Data.Foldable.null m = False+          decide _ (RecordLit n) | Data.Foldable.null n = False+          decide (RecordLit _) (RecordLit _) = False+          decide l r = not (Eval.judgmentallyEqual l r)+      RecordCompletion _ _ -> False+      Merge x y t -> loop x && loop y && all loop t+      ToMap x t -> case x of+          RecordLit _ -> False+          _ -> loop x && all loop t+      Field r k -> case r of+          RecordLit _ -> False+          Project _ _ -> False+          Prefer (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r+          Prefer _ (RecordLit _) -> False+          Combine (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r+          Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r+          _ -> loop r+      Project r p -> loop r &&+          case p of+              Left s -> case r of+                  RecordLit _ -> False+                  Project _ _ -> False+                  Prefer _ (RecordLit _) -> False+                  _ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s+              Right e' -> case e' of+                  Record _ -> False+                  _ -> loop e'+      Assert t -> loop t+      Equivalent l r -> loop l && loop r+      Note _ e' -> loop e'+      ImportAlt _ _ -> False+      Embed _ -> True++{-| Detect if the given variable is free within the given expression++>>> "x" `freeIn` "x"+True+>>> "x" `freeIn` "y"+False+>>> "x" `freeIn` Lam "x" (Const Type) "x"+False+-}+freeIn :: Eq a => Var -> Expr s a -> Bool+variable@(V var i) `freeIn` expression =+    Dhall.Core.subst variable (Var (V var (i + 1))) strippedExpression+      /= strippedExpression+  where+    denote' :: Expr t b -> Expr () b+    denote' = denote++    strippedExpression = denote' expression++-- | Pretty-print a value+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++    Note that the result does not include surrounding quotes+-}+escapeText :: Text -> Text+escapeText = escapeText_+{-# INLINE escapeText #-}+++{-| Utility used to implement the @--censor@ flag, by:++    * Replacing all `Src` text with spaces+    * Replacing all `Text` literals inside type errors with spaces+-}+censorExpression :: Expr Src a -> Expr Src a+censorExpression (TextLit chunks) = TextLit (censorChunks chunks)+censorExpression (Note src     e) = Note (censorSrc src) (censorExpression e)+censorExpression  e               = over subExpressions censorExpression e++censorChunks :: Chunks Src a -> Chunks Src a+censorChunks (Chunks xys z) = Chunks xys' z'+  where+    z' = censorText z++    xys' = [ (censorText x, censorExpression y) | (x, y) <- xys ]++-- | Utility used to censor `Text` by replacing all characters with a space+censorText :: Text -> Text+censorText = Data.Text.map (\_ -> ' ')++censorSrc :: Src -> Src+censorSrc (Src { srcText = oldText, .. }) = Src { srcText = newText, .. }+  where+    newText = censorText oldText++{-| Convenience utility for converting `Either`-based exceptions to `IO`-based+    exceptions+-}+throws :: (Exception e, MonadIO io) => Either e a -> io a+throws (Left  e) = liftIO (Control.Exception.throwIO e)+throws (Right r) = return r++{- $setup+>>> import qualified Codec.Serialise+>>> import qualified Dhall.Binary+>>> import Data.SpecialValues+>>> import Test.QuickCheck (Arbitrary(..), oneof, elements)+>>> :{+  instance Arbitrary DhallDouble where+    arbitrary = fmap DhallDouble (oneof [ arbitrary, elements specialValues ])+:}+-}