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