dhall 1.13.1 → 1.14.0
raw patch · 198 files changed
+1228/−1125 lines, 198 filesdep +doctestdep ~basedep ~insert-ordered-containersdep ~tastyPVP ok
version bump matches the API change (PVP)
Dependencies added: doctest
Dependency ranges changed: base, insert-ordered-containers, tasty
API changes (from Hackage documentation)
- Dhall.Core: Homeless :: HasHome
- Dhall.Core: Path :: PathHashed -> PathMode -> Path
- Dhall.Core: PathHashed :: Maybe (Digest SHA256) -> PathType -> PathHashed
- Dhall.Core: [pathHashed] :: Path -> PathHashed
- Dhall.Core: [pathMode] :: Path -> PathMode
- Dhall.Core: [pathType] :: PathHashed -> PathType
- Dhall.Core: data HasHome
- Dhall.Core: data Path
- Dhall.Core: data PathHashed
- Dhall.Core: data PathMode
- Dhall.Core: data PathType
- Dhall.Core: instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Path
- Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.Path
- Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.PathHashed
- Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.PathType
- Dhall.Core: instance GHC.Classes.Eq Dhall.Core.HasHome
- Dhall.Core: instance GHC.Classes.Eq Dhall.Core.Path
- Dhall.Core: instance GHC.Classes.Eq Dhall.Core.PathHashed
- Dhall.Core: instance GHC.Classes.Eq Dhall.Core.PathMode
- Dhall.Core: instance GHC.Classes.Eq Dhall.Core.PathType
- Dhall.Core: instance GHC.Classes.Ord Dhall.Core.HasHome
- Dhall.Core: instance GHC.Classes.Ord Dhall.Core.Path
- Dhall.Core: instance GHC.Classes.Ord Dhall.Core.PathHashed
- Dhall.Core: instance GHC.Classes.Ord Dhall.Core.PathMode
- Dhall.Core: instance GHC.Classes.Ord Dhall.Core.PathType
- Dhall.Core: instance GHC.Show.Show Dhall.Core.HasHome
- Dhall.Core: instance GHC.Show.Show Dhall.Core.Path
- Dhall.Core: instance GHC.Show.Show Dhall.Core.PathHashed
- Dhall.Core: instance GHC.Show.Show Dhall.Core.PathMode
- Dhall.Core: instance GHC.Show.Show Dhall.Core.PathType
- Dhall.Import: exprFromPath :: Path -> StateT Status IO (Expr Src Path)
+ Dhall.Core: Absolute :: FilePrefix
+ Dhall.Core: Directory :: [Text] -> Directory
+ Dhall.Core: Here :: FilePrefix
+ Dhall.Core: Import :: ImportHashed -> ImportMode -> Import
+ Dhall.Core: ImportHashed :: Maybe (Digest SHA256) -> ImportType -> ImportHashed
+ Dhall.Core: Local :: FilePrefix -> File -> ImportType
+ Dhall.Core: Parent :: FilePrefix
+ Dhall.Core: [components] :: Directory -> [Text]
+ Dhall.Core: [directory] :: File -> Directory
+ Dhall.Core: [file] :: File -> Text
+ Dhall.Core: [importHashed] :: Import -> ImportHashed
+ Dhall.Core: [importMode] :: Import -> ImportMode
+ Dhall.Core: [importType] :: ImportHashed -> ImportType
+ Dhall.Core: data File
+ Dhall.Core: data FilePrefix
+ Dhall.Core: data Import
+ Dhall.Core: data ImportHashed
+ Dhall.Core: data ImportMode
+ Dhall.Core: data ImportType
+ Dhall.Core: instance Data.Semigroup.Semigroup Dhall.Core.Directory
+ Dhall.Core: instance Data.Semigroup.Semigroup Dhall.Core.File
+ Dhall.Core: instance Data.Semigroup.Semigroup Dhall.Core.Import
+ Dhall.Core: instance Data.Semigroup.Semigroup Dhall.Core.ImportHashed
+ Dhall.Core: instance Data.Semigroup.Semigroup Dhall.Core.ImportType
+ Dhall.Core: instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Import
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.Directory
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.File
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.FilePrefix
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.Import
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.ImportHashed
+ Dhall.Core: instance Formatting.Buildable.Buildable Dhall.Core.ImportType
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.Directory
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.File
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.FilePrefix
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.Import
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.ImportHashed
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.ImportMode
+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.ImportType
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.Directory
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.File
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.FilePrefix
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.Import
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.ImportHashed
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.ImportMode
+ Dhall.Core: instance GHC.Classes.Ord Dhall.Core.ImportType
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.Directory
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.File
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.FilePrefix
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.Import
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.ImportHashed
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.ImportMode
+ Dhall.Core: instance GHC.Show.Show Dhall.Core.ImportType
+ Dhall.Core: newtype Directory
+ Dhall.Core: type Path = Import
+ Dhall.Import: exprFromImport :: Import -> StateT Status IO (Expr Src Import)
+ Dhall.Import: instance Dhall.Import.Canonicalize Dhall.Core.Directory
+ Dhall.Import: instance Dhall.Import.Canonicalize Dhall.Core.File
+ Dhall.Import: instance Dhall.Import.Canonicalize Dhall.Core.Import
+ Dhall.Import: instance Dhall.Import.Canonicalize Dhall.Core.ImportHashed
+ Dhall.Import: instance Dhall.Import.Canonicalize Dhall.Core.ImportType
- Dhall.Core: Code :: PathMode
+ Dhall.Core: Code :: ImportMode
- Dhall.Core: Env :: Text -> PathType
+ Dhall.Core: Env :: Text -> ImportType
- Dhall.Core: File :: HasHome -> FilePath -> PathType
+ Dhall.Core: File :: Directory -> Text -> File
- Dhall.Core: Home :: HasHome
+ Dhall.Core: Home :: FilePrefix
- Dhall.Core: RawText :: PathMode
+ Dhall.Core: RawText :: ImportMode
- Dhall.Core: URL :: Text -> (Maybe PathHashed) -> PathType
+ Dhall.Core: URL :: Text -> File -> Text -> (Maybe ImportHashed) -> ImportType
- Dhall.Core: [hash] :: PathHashed -> Maybe (Digest SHA256)
+ Dhall.Core: [hash] :: ImportHashed -> Maybe (Digest SHA256)
- Dhall.Import: Cycle :: Path -> Cycle
+ Dhall.Import: Cycle :: Import -> Cycle
- Dhall.Import: Imported :: [Path] -> e -> Imported e
+ Dhall.Import: Imported :: [Import] -> e -> Imported e
- Dhall.Import: ReferentiallyOpaque :: Path -> ReferentiallyOpaque
+ Dhall.Import: ReferentiallyOpaque :: Import -> ReferentiallyOpaque
- Dhall.Import: Status :: [Path] -> Map Path (Expr Src X) -> Maybe Manager -> Status
+ Dhall.Import: Status :: [Import] -> Map Import (Expr Src X) -> Maybe Manager -> Status
- Dhall.Import: [_cache] :: Status -> Map Path (Expr Src X)
+ Dhall.Import: [_cache] :: Status -> Map Import (Expr Src X)
- Dhall.Import: [_stack] :: Status -> [Path]
+ Dhall.Import: [_stack] :: Status -> [Import]
- Dhall.Import: [cyclicImport] :: Cycle -> Path
+ Dhall.Import: [cyclicImport] :: Cycle -> Import
- Dhall.Import: [importStack] :: Imported e -> [Path]
+ Dhall.Import: [importStack] :: Imported e -> [Import]
- Dhall.Import: [opaqueImport] :: ReferentiallyOpaque -> Path
+ Dhall.Import: [opaqueImport] :: ReferentiallyOpaque -> Import
- Dhall.Import: load :: Expr Src Path -> IO (Expr Src X)
+ Dhall.Import: load :: Expr Src Import -> IO (Expr Src X)
- Dhall.Import: loadWith :: MonadCatch m => (Path -> StateT Status m (Expr Src Path)) -> Context (Expr Src X) -> Expr Src Path -> m (Expr Src X)
+ Dhall.Import: loadWith :: MonadCatch m => (Import -> StateT Status m (Expr Src Import)) -> Context (Expr Src X) -> Normalizer X -> Expr Src Import -> m (Expr Src X)
- Dhall.Import: loadWithContext :: Context (Expr Src X) -> Expr Src Path -> IO (Expr Src X)
+ Dhall.Import: loadWithContext :: Context (Expr Src X) -> Normalizer X -> Expr Src Import -> IO (Expr Src X)
- Dhall.Parser: expr :: Parser (Expr Src Path)
+ Dhall.Parser: expr :: Parser (Expr Src Import)
- Dhall.Parser: exprAndHeaderFromText :: String -> Text -> Either ParseError (Text, Expr Src Path)
+ Dhall.Parser: exprAndHeaderFromText :: String -> Text -> Either ParseError (Text, Expr Src Import)
- Dhall.Parser: exprFromText :: String -> Text -> Either ParseError (Expr Src Path)
+ Dhall.Parser: exprFromText :: String -> Text -> Either ParseError (Expr Src Import)
Files
- CHANGELOG.md +34/−0
- Prelude/Bool/fold +2/−2
- Prelude/Integer/show +3/−2
- Prelude/List/all +1/−1
- Prelude/List/any +1/−1
- Prelude/List/concat +7/−7
- Prelude/List/concatMap +2/−2
- Prelude/List/filter +4/−4
- Prelude/List/fold +7/−7
- Prelude/List/generate +3/−3
- Prelude/List/head +2/−2
- Prelude/List/indexed +3/−3
- Prelude/List/iterate +3/−3
- Prelude/List/last +2/−2
- Prelude/List/length +2/−2
- Prelude/List/map +1/−1
- Prelude/List/null +2/−2
- Prelude/List/replicate +2/−2
- Prelude/List/reverse +2/−2
- Prelude/List/shifted +20/−20
- Prelude/Natural/build +2/−2
- Prelude/Natural/enumerate +3/−3
- Prelude/Natural/even +2/−2
- Prelude/Natural/fold +5/−5
- Prelude/Natural/isZero +3/−3
- Prelude/Natural/odd +2/−2
- Prelude/Natural/product +3/−3
- Prelude/Natural/show +3/−3
- Prelude/Natural/sum +3/−3
- Prelude/Natural/toInteger +2/−2
- Prelude/Optional/all +1/−1
- Prelude/Optional/any +1/−1
- Prelude/Optional/build +6/−6
- Prelude/Optional/concat +6/−6
- Prelude/Optional/filter +3/−3
- Prelude/Optional/fold +2/−2
- Prelude/Optional/head +10/−10
- Prelude/Optional/last +10/−10
- Prelude/Optional/length +4/−4
- Prelude/Optional/map +1/−1
- Prelude/Optional/null +2/−2
- Prelude/Optional/toList +2/−2
- Prelude/Text/concatMap +2/−2
- Prelude/Text/concatMapSep +2/−2
- dhall.cabal +13/−4
- dhall/Main.hs +3/−3
- doctest/Main.hs +6/−0
- src/Dhall.hs +22/−19
- src/Dhall/Core.hs +137/−53
- src/Dhall/Import.hs +245/−318
- src/Dhall/Parser.hs +84/−73
- src/Dhall/Pretty/Internal.hs +8/−6
- src/Dhall/Tutorial.hs +228/−205
- src/Dhall/TypeCheck.hs +102/−101
- tests/Normalization.hs +4/−4
- tests/Tutorial.hs +1/−1
- tests/TypeCheck.hs +3/−0
- tests/normalization/examples/Bool/fold/0A.dhall +1/−1
- tests/normalization/examples/Bool/fold/1A.dhall +1/−1
- tests/normalization/examples/Integer/show/1A.dhall +1/−1
- tests/normalization/examples/Integer/show/1B.dhall +1/−1
- tests/normalization/examples/List/all/0A.dhall +1/−1
- tests/normalization/examples/List/any/0A.dhall +1/−1
- tests/normalization/examples/List/concat/0A.dhall +1/−1
- tests/normalization/examples/List/concat/1A.dhall +4/−4
- tests/normalization/examples/List/concat/1B.dhall +1/−1
- tests/normalization/examples/List/concatMap/0A.dhall +1/−1
- tests/normalization/examples/List/concatMap/0B.dhall +1/−1
- tests/normalization/examples/List/filter/0A.dhall +1/−1
- tests/normalization/examples/List/filter/0B.dhall +1/−1
- tests/normalization/examples/List/filter/1A.dhall +1/−1
- tests/normalization/examples/List/filter/1B.dhall +1/−1
- tests/normalization/examples/List/fold/0A.dhall +2/−2
- tests/normalization/examples/List/fold/0B.dhall +1/−1
- tests/normalization/examples/List/fold/1A.dhall +1/−1
- tests/normalization/examples/List/fold/1B.dhall +1/−1
- tests/normalization/examples/List/fold/2A.dhall +1/−1
- tests/normalization/examples/List/fold/2B.dhall +1/−1
- tests/normalization/examples/List/generate/0A.dhall +1/−1
- tests/normalization/examples/List/generate/1A.dhall +1/−1
- tests/normalization/examples/List/head/0A.dhall +1/−1
- tests/normalization/examples/List/head/0B.dhall +1/−1
- tests/normalization/examples/List/head/1A.dhall +1/−1
- tests/normalization/examples/List/head/1B.dhall +1/−1
- tests/normalization/examples/List/iterate/0A.dhall +1/−1
- tests/normalization/examples/List/iterate/0B.dhall +1/−1
- tests/normalization/examples/List/iterate/1A.dhall +1/−1
- tests/normalization/examples/List/last/0A.dhall +1/−1
- tests/normalization/examples/List/last/0B.dhall +1/−1
- tests/normalization/examples/List/last/1A.dhall +1/−1
- tests/normalization/examples/List/last/1B.dhall +1/−1
- tests/normalization/examples/List/length/0A.dhall +1/−1
- tests/normalization/examples/List/length/0B.dhall +1/−1
- tests/normalization/examples/List/length/1A.dhall +1/−1
- tests/normalization/examples/List/length/1B.dhall +1/−1
- tests/normalization/examples/List/map/0A.dhall +1/−1
- tests/normalization/examples/List/null/0A.dhall +1/−1
- tests/normalization/examples/List/null/1A.dhall +1/−1
- tests/normalization/examples/List/replicate/0A.dhall +1/−1
- tests/normalization/examples/List/replicate/1A.dhall +1/−1
- tests/normalization/examples/List/replicate/1B.dhall +1/−1
- tests/normalization/examples/List/reverse/0A.dhall +1/−1
- tests/normalization/examples/List/reverse/1A.dhall +1/−1
- tests/normalization/examples/List/reverse/1B.dhall +1/−1
- tests/normalization/examples/List/shifted/0A.dhall +9/−9
- tests/normalization/examples/List/shifted/0B.dhall +9/−9
- tests/normalization/examples/Natural/build/0B.dhall +1/−1
- tests/normalization/examples/Natural/build/1B.dhall +1/−1
- tests/normalization/examples/Natural/enumerate/0A.dhall +1/−1
- tests/normalization/examples/Natural/enumerate/0B.dhall +1/−1
- tests/normalization/examples/Natural/enumerate/1A.dhall +1/−1
- tests/normalization/examples/Natural/even/0A.dhall +1/−1
- tests/normalization/examples/Natural/even/1A.dhall +1/−1
- tests/normalization/examples/Natural/fold/0A.dhall +1/−1
- tests/normalization/examples/Natural/fold/0B.dhall +1/−1
- tests/normalization/examples/Natural/fold/1A.dhall +1/−1
- tests/normalization/examples/Natural/fold/1B.dhall +1/−1
- tests/normalization/examples/Natural/fold/2A.dhall +1/−1
- tests/normalization/examples/Natural/isZero/0A.dhall +1/−1
- tests/normalization/examples/Natural/isZero/1A.dhall +1/−1
- tests/normalization/examples/Natural/odd/0A.dhall +1/−1
- tests/normalization/examples/Natural/odd/1A.dhall +1/−1
- tests/normalization/examples/Natural/product/0A.dhall +1/−1
- tests/normalization/examples/Natural/product/0B.dhall +1/−1
- tests/normalization/examples/Natural/product/1B.dhall +1/−1
- tests/normalization/examples/Natural/show/0A.dhall +1/−1
- tests/normalization/examples/Natural/show/0B.dhall +1/−1
- tests/normalization/examples/Natural/show/1A.dhall +1/−1
- tests/normalization/examples/Natural/show/1B.dhall +1/−1
- tests/normalization/examples/Natural/sum/0A.dhall +1/−1
- tests/normalization/examples/Natural/sum/0B.dhall +1/−1
- tests/normalization/examples/Natural/sum/1B.dhall +1/−1
- tests/normalization/examples/Natural/toInteger/0A.dhall +1/−1
- tests/normalization/examples/Natural/toInteger/0B.dhall +1/−1
- tests/normalization/examples/Natural/toInteger/1A.dhall +1/−1
- tests/normalization/examples/Natural/toInteger/1B.dhall +1/−1
- tests/normalization/examples/Optional/all/0A.dhall +1/−1
- tests/normalization/examples/Optional/any/0A.dhall +1/−1
- tests/normalization/examples/Optional/build/0A.dhall +2/−2
- tests/normalization/examples/Optional/build/0B.dhall +1/−1
- tests/normalization/examples/Optional/build/1A.dhall +2/−2
- tests/normalization/examples/Optional/build/1B.dhall +1/−1
- tests/normalization/examples/Optional/concat/0A.dhall +1/−1
- tests/normalization/examples/Optional/concat/0B.dhall +1/−1
- tests/normalization/examples/Optional/concat/1A.dhall +1/−1
- tests/normalization/examples/Optional/concat/1B.dhall +1/−1
- tests/normalization/examples/Optional/concat/2A.dhall +1/−1
- tests/normalization/examples/Optional/concat/2B.dhall +1/−1
- tests/normalization/examples/Optional/filter/0A.dhall +1/−1
- tests/normalization/examples/Optional/filter/0B.dhall +1/−1
- tests/normalization/examples/Optional/filter/1A.dhall +1/−1
- tests/normalization/examples/Optional/fold/0A.dhall +1/−1
- tests/normalization/examples/Optional/fold/1A.dhall +1/−1
- tests/normalization/examples/Optional/head/0A.dhall +4/−4
- tests/normalization/examples/Optional/head/0B.dhall +1/−1
- tests/normalization/examples/Optional/head/1A.dhall +2/−2
- tests/normalization/examples/Optional/head/1B.dhall +1/−1
- tests/normalization/examples/Optional/last/0A.dhall +4/−4
- tests/normalization/examples/Optional/last/0B.dhall +1/−1
- tests/normalization/examples/Optional/last/1A.dhall +2/−2
- tests/normalization/examples/Optional/last/1B.dhall +1/−1
- tests/normalization/examples/Optional/last/2A.dhall +1/−1
- tests/normalization/examples/Optional/last/2B.dhall +1/−1
- tests/normalization/examples/Optional/length/0A.dhall +1/−1
- tests/normalization/examples/Optional/length/0B.dhall +1/−1
- tests/normalization/examples/Optional/length/1A.dhall +1/−1
- tests/normalization/examples/Optional/length/1B.dhall +1/−1
- tests/normalization/examples/Optional/map/0A.dhall +1/−1
- tests/normalization/examples/Optional/null/0A.dhall +1/−1
- tests/normalization/examples/Optional/null/1A.dhall +1/−1
- tests/normalization/examples/Optional/toList/0A.dhall +1/−1
- tests/normalization/examples/Optional/toList/1A.dhall +1/−1
- tests/normalization/examples/Optional/toList/1B.dhall +1/−1
- tests/normalization/examples/Text/concatMap/0A.dhall +1/−1
- tests/normalization/examples/Text/concatMap/1A.dhall +1/−1
- tests/normalization/examples/Text/concatMapSep/0A.dhall +1/−1
- tests/normalization/examples/Text/concatMapSep/1A.dhall +1/−1
- tests/normalization/integerShowA.dhall +2/−2
- tests/normalization/integerShowB.dhall +1/−1
- tests/normalization/naturalPlusA.dhall +1/−1
- tests/normalization/naturalPlusB.dhall +1/−1
- tests/normalization/naturalShowA.dhall +1/−1
- tests/normalization/naturalShowB.dhall +1/−1
- tests/normalization/naturalToIntegerA.dhall +1/−1
- tests/normalization/naturalToIntegerB.dhall +1/−1
- tests/normalization/optionalBuildA.dhall +2/−2
- tests/normalization/optionalBuildB.dhall +2/−2
- tests/normalization/optionalFoldA.dhall +1/−1
- tests/normalization/optionalFoldB.dhall +1/−1
- tests/parser/urls.dhall +6/−6
- tests/regression/issue216b.dhall +2/−10
- tests/tutorial/unions0A.dhall +1/−1
- tests/tutorial/unions2A.dhall +2/−2
- tests/tutorial/unions2B.dhall +2/−2
- tests/tutorial/unions3A.dhall +2/−2
- tests/tutorial/unions3B.dhall +2/−2
- tests/typecheck/mergeEquivalenceA.dhall +6/−0
- tests/typecheck/mergeEquivalenceB.dhall +1/−0
CHANGELOG.md view
@@ -1,3 +1,37 @@+1.14.0++* BREAKING CHANGE TO THE LANGUAGE: Switch grammar of `Natural` and `Integer`+ * `Natural` number literals are now unsigned and `Integer` literals always+ require a sign+ * This is a **VERY** disruptive change to most Dhall code in the wild but+ was unanimously agreed upon here:+ https://github.com/dhall-lang/dhall-lang/issues/138+ * See also: https://github.com/dhall-lang/dhall-haskell/pull/381+* BREAKING CHANGE TO THE LANGUAGE: Drop support for importing directories+ * Importing `dir/` used to resolve to `dir/@`, which is no longer supported+ * See: https://github.com/dhall-lang/dhall-haskell/pull/384+* BREAKING CHANGE TO THE LANGUAGE: Change to the grammar for imports+ * File path components can no longer contain `#` or `?` characters+ * URL imports must now contain at least one path component+ * URL path components must match the grammar for file path components+ * See: https://github.com/dhall-lang/dhall-haskell/pull/390+* BREAKING CHANGE TO THE API: Rename `Path{,Mode,Hashed,Type}` to+ `Import{,Mode,Hashed,Type}`+ * In practice this change is not breaking for the most common use cases+ since this also provides a `Path` type synonym for backwards compatibility+ * See: https://github.com/dhall-lang/dhall-haskell/pull/376+* BUG FIX: Fix α-equivalence bug when type-checking `merge`+ * `merge` expressions would sometimes reject valid code due to a+ type-checking bug+ * See: https://github.com/dhall-lang/dhall-haskell/pull/394+* Improve import caching+ * See: https://github.com/dhall-lang/dhall-haskell/pull/388+ * See: https://github.com/dhall-lang/dhall-haskell/pull/392+* Increase upper bound on `tasty`+ * See: https://github.com/dhall-lang/dhall-haskell/pull/382+* Fix lower bound on `insert-ordered-containers`+ * See: https://github.com/dhall-lang/dhall-haskell/pull/377+ 1.13.1 * Increase upper bound on `ansi-terminal` and `megaparsec`
Prelude/Bool/fold view
@@ -4,9 +4,9 @@ Examples: ```-./fold True Integer 0 1 = 0+./fold True Natural 0 1 = 0 -./fold False Integer 0 1 = 1+./fold False Natural 0 1 = 1 ``` -} let fold
Prelude/Integer/show view
@@ -1,13 +1,14 @@ {- Render an `Integer` as `Text` using the same representation as Dhall source-code (i.e. a decimal number with a leading `-` sign if negative)+code (i.e. a decimal number with a leading `-` sign if negative and a leading+`+` sign if non-negative) Examples: ``` ./show -3 = "-3" -./show 0 = "0"+./show +0 = "+0" ``` -} let show : Integer → Text = Integer/show in show
Prelude/List/all view
@@ -5,7 +5,7 @@ Examples: ```-./all Natural Natural/even [ +2, +3, +5 ] = False+./all Natural Natural/even [ 2, 3, 5 ] = False ./all Natural Natural/even ([] : List Natural) = True ```
Prelude/List/any view
@@ -5,7 +5,7 @@ Examples: ```-./any Natural Natural/even [ +2, +3, +5 ] = True+./any Natural Natural/even [ 2, 3, 5 ] = True ./any Natural Natural/even ([] : List Natural) = False ```
Prelude/List/concat view
@@ -4,22 +4,22 @@ Examples: ```-./concat Integer+./concat Natural [ [0, 1, 2] , [3, 4] , [5, 6, 7, 8] ] = [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] -./concat Integer-( [ [] : List Integer- , [] : List Integer- , [] : List Integer+./concat Natural+( [ [] : List Natural+ , [] : List Natural+ , [] : List Natural ] )-= [] : List Integer+= [] : List Natural -./concat Integer ([] : List (List Integer)) = [] : List Integer+./concat Natural ([] : List (List Natural)) = [] : List Natural ``` -} let concat
Prelude/List/concatMap view
@@ -5,8 +5,8 @@ Examples: ```-./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]-= [ +2, +2, +3, +3, +5, +5 ]+./concatMap Natural Natural (λ(n : Natural) → [n, n]) [2, 3, 5]+= [ 2, 2, 3, 3, 5, 5 ] ./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural) = [] : List Natural
Prelude/List/filter view
@@ -4,11 +4,11 @@ Examples: ```-./filter Natural Natural/even [+2, +3, +5]-= [ +2 ]+./filter Natural Natural/even [ 2, 3, 5 ]+= [ 2 ] -./filter Natural Natural/odd [+2, +3, +5]-= [ +3, +5 ]+./filter Natural Natural/odd [ 2, 3, 5 ]+= [ 3, 5 ] ``` -} let filter
Prelude/List/fold view
@@ -9,29 +9,29 @@ ``` ./fold Natural- [ +2, +3, +5 ]+ [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y)- +0-= +10+ 0+= 10 λ(nil : Natural) → ./fold Natural- [ +2, +3, +5 ]+ [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) nil-= λ(nil : Natural) → +2 + +3 + +5 + nil+= λ(nil : Natural) → 2 + 3 + 5 + nil λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list)-→ ./fold Natural [ +2, +3, +5 ] list cons nil+→ ./fold Natural [ 2, 3, 5 ] list cons nil = λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list)-→ cons +2 (cons +3 (cons +5 nil))+→ cons 2 (cons 3 (cons 5 nil)) ``` -} let fold
Prelude/List/generate view
@@ -1,13 +1,13 @@ {--Build a list by calling the supplied function on all `Natural` numbers from `+0`+Build a list by calling the supplied function on all `Natural` numbers from `0` up to but not including the supplied `Natural` number Examples: ```-./generate +5 Bool Natural/even = [ True, False, True, False, True ]+./generate 5 Bool Natural/even = [ True, False, True, False, True ] -./generate +0 Bool Natural/even = [] : List Bool+./generate 0 Bool Natural/even = [] : List Bool ``` -} let generate
Prelude/List/head view
@@ -4,9 +4,9 @@ Examples: ```-./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer+./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural -./head Integer ([] : List Integer) = [] : Optional Integer+./head Natural ([] : List Natural) = [] : Optional Natural ``` -} let head : ∀(a : Type) → List a → Optional a = List/head in head
Prelude/List/indexed view
@@ -5,9 +5,9 @@ ``` ./indexed Bool [ True, False, True ]-= [ { index = +0, value = True }- , { index = +1, value = False }- , { index = +2, value = True }+= [ { index = 0, value = True }+ , { index = 1, value = False }+ , { index = 2, value = True } ] : List { index : Natural, value : Bool } ./indexed Bool ([] : List Bool)
Prelude/List/iterate view
@@ -5,10 +5,10 @@ Examples: ```-./iterate +10 Natural (λ(x : Natural) → x * +2) +1-= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]+./iterate 10 Natural (λ(x : Natural) → x * 2) 1+= [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ] -./iterate +0 Natural (λ(x : Natural) → x * +2) +1+./iterate 0 Natural (λ(x : Natural) → x * 2) 1 = [] : List Natural ``` -}
Prelude/List/last view
@@ -4,9 +4,9 @@ Examples: ```-./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer+./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural -./last Integer ([] : List Integer) = [] : Optional Integer+./last Natural ([] : List Natural) = [] : Optional Natural ``` -} let last : ∀(a : Type) → List a → Optional a = List/last in last
Prelude/List/length view
@@ -4,9 +4,9 @@ Examples: ```-./length Integer [ 0, 1, 2 ] = +3+./length Natural [ 0, 1, 2 ] = 3 -./length Integer ([] : List Integer) = +0+./length Natural ([] : List Natural) = 0 ``` -} let length : ∀(a : Type) → List a → Natural = List/length in length
Prelude/List/map view
@@ -4,7 +4,7 @@ Examples: ```-./map Natural Bool Natural/even [ +2, +3, +5 ]+./map Natural Bool Natural/even [ 2, 3, 5 ] = [ True, False, False ] ./map Natural Bool Natural/even ([] : List Natural)
Prelude/List/null view
@@ -4,9 +4,9 @@ Examples: ```-./null Integer [ 0, 1, 2 ] = False+./null Natural [ 0, 1, 2 ] = False -./null Integer ([] : List Integer) = True+./null Natural ([] : List Natural) = True ``` -} let null
Prelude/List/replicate view
@@ -4,9 +4,9 @@ Examples: ```-./replicate +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]+./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] -./replicate +0 Integer 1 = [] : List Integer+./replicate 0 Natural 1 = [] : List Natural ``` -} let replicate
Prelude/List/reverse view
@@ -4,9 +4,9 @@ Examples: ```-./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer+./reverse Natural [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Natural -./reverse Integer ([] : List Integer) = [] : List Integer+./reverse Natural ([] : List Natural) = [] : List Natural ``` -} let reverse : ∀(a : Type) → List a → List a = List/reverse in reverse
Prelude/List/shifted view
@@ -7,28 +7,28 @@ ``` ./shifted Bool-[ [ { index = +0, value = True }- , { index = +1, value = True }- , { index = +2, value = True }+[ [ { index = 0, value = True }+ , { index = 1, value = True }+ , { index = 2, value = True } ]-, [ { index = +0, value = False }- , { index = +1, value = False }+, [ { index = 0, value = False }+ , { index = 1, value = False } ]-, [ { index = +0, value = True }- , { index = +1, value = True }- , { index = +2, value = True }- , { index = +3, value = True }+, [ { index = 0, value = True }+ , { index = 1, value = True }+ , { index = 2, value = True }+ , { index = 3, value = True } ] ]-= [ { index = +0, value = True }- , { index = +1, value = True }- , { index = +2, value = True }- , { index = +3, value = False }- , { index = +4, value = False }- , { index = +5, value = True }- , { index = +6, value = True }- , { index = +7, value = True }- , { index = +8, value = True }+= [ { index = 0, value = True }+ , { index = 1, value = True }+ , { index = 2, value = True }+ , { index = 3, value = False }+ , { index = 4, value = False }+ , { index = 5, value = True }+ , { index = 6, value = True }+ , { index = 7, value = True }+ , { index = 8, value = True } ] ./shifted Bool ([] : List (List { index : Natural, value : Bool }))@@ -79,9 +79,9 @@ (y.diff (n + length)) } )- { count = +0, diff = λ(_ : Natural) → nil }+ { count = 0, diff = λ(_ : Natural) → nil } - in result.diff +0+ in result.diff 0 ) in shifted
Prelude/Natural/build view
@@ -10,7 +10,7 @@ → λ(zero : natural) → succ (succ (succ zero)) )-= +3+= 3 ./build ( λ(natural : Type)@@ -18,7 +18,7 @@ → λ(zero : natural) → zero )-= +0+= 0 ``` -} let build
Prelude/Natural/enumerate view
@@ -1,13 +1,13 @@ {--Generate a list of numbers from `+0` up to but not including the specified+Generate a list of numbers from `0` up to but not including the specified number Examples: ```-./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]+./enumerate 10 = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ] -./enumerate +0 = [] : List Natural+./enumerate 0 = [] : List Natural ``` -} let enumerate
Prelude/Natural/even view
@@ -4,9 +4,9 @@ Examples: ```-./even +3 = False+./even 3 = False -./even +0 = True+./even 0 = True ``` -} let even : Natural → Bool = Natural/even in even
Prelude/Natural/fold view
@@ -1,21 +1,21 @@ {- `fold` is the primitive function for consuming `Natural` numbers -If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just+If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just replaces each `succ` and `zero` with something else Examples: ```-./fold +3 Natural (λ(x : Natural) → +5 * x) +1 = +125+./fold 3 Natural (λ(x : Natural) → 5 * x) 1 = 125 -λ(zero : Natural) → ./fold +3 Natural (λ(x : Natural) → +5 * x) zero-= λ(zero : Natural) → +5 * +5 * +5 * zero+λ(zero : Natural) → ./fold 3 Natural (λ(x : Natural) → 5 * x) zero+= λ(zero : Natural) → 5 * 5 * 5 * zero λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural)-→ ./fold +3 natural succ zero+→ ./fold 3 natural succ zero = λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural)
Prelude/Natural/isZero view
@@ -1,12 +1,12 @@ {--Returns `True` if a number is `+0` and returns `False` otherwise+Returns `True` if a number is `0` and returns `False` otherwise Examples: ```-./isZero +2 = False+./isZero 2 = False -./isZero +0 = True+./isZero 0 = True ``` -} let isZero : Natural → Bool = Natural/isZero in isZero
Prelude/Natural/odd view
@@ -4,9 +4,9 @@ Examples: ```-./odd +3 = True+./odd 3 = True -./odd +0 = False+./odd 0 = False ``` -} let odd : Natural → Bool = Natural/odd in odd
Prelude/Natural/product view
@@ -4,9 +4,9 @@ Examples: ```-./product [ +2, +3, +5 ] = +30+./product [ 2, 3, 5 ] = 30 -./product ([] : List Natural) = +1+./product ([] : List Natural) = 1 ``` -} let product@@ -17,6 +17,6 @@ xs Natural (λ(l : Natural) → λ(r : Natural) → l * r)- +1+ 1 in product
Prelude/Natural/show view
@@ -1,13 +1,13 @@ {- Render a `Natural` number as `Text` using the same representation as Dhall-source code (i.e. a decimal number with a leading `+` sign)+source code (i.e. a decimal number) Examples: ```-./show +3 = "+3"+./show 3 = "3" -./show +0 = "+0"+./show 0 = "0" ``` -} let show : Natural → Text = Natural/show in show
Prelude/Natural/sum view
@@ -4,9 +4,9 @@ Examples: ```-./sum [ +2, +3, +5 ] = +10+./sum [ 2, 3, 5 ] = 10 -./sum ([] : List Natural) = +0+./sum ([] : List Natural) = 0 ``` -} let sum@@ -17,6 +17,6 @@ xs Natural (λ(l : Natural) → λ(r : Natural) → l + r)- +0+ 0 in sum
Prelude/Natural/toInteger view
@@ -4,9 +4,9 @@ Examples: ```-./toInteger +3 = 3+./toInteger 3 = +3 -./toInteger +0 = 0+./toInteger 0 = +0 ``` -} let toInteger : Natural → Integer = Natural/toInteger in toInteger
Prelude/Optional/all view
@@ -5,7 +5,7 @@ Examples: ```-./all Natural Natural/even ([ +3 ] : Optional Natural) = False+./all Natural Natural/even ([ 3 ] : Optional Natural) = False ./all Natural Natural/even ([] : Optional Natural) = True ```
Prelude/Optional/any view
@@ -5,7 +5,7 @@ Examples: ```-./any Natural Natural/even ([ +2 ] : Optional Natural) = True+./any Natural Natural/even ([ 2 ] : Optional Natural) = True ./any Natural Natural/even ([] : Optional Natural) = False ```
Prelude/Optional/build view
@@ -5,22 +5,22 @@ ``` ./build-Integer+Natural ( λ(optional : Type)-→ λ(just : Integer → optional)+→ λ(just : Natural → optional) → λ(nothing : optional) → just 1 )-= [ 1 ] : Optional Integer+= [ 1 ] : Optional Natural ./build-Integer+Natural ( λ(optional : Type)-→ λ(just : Integer → optional)+→ λ(just : Natural → optional) → λ(nothing : optional) → nothing )-= [] : Optional Integer+= [] : Optional Natural ``` -} let build
Prelude/Optional/concat view
@@ -4,14 +4,14 @@ Examples: ```-./concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer))-= [ 1 ] : Optional Integer+./concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural))+= [ 1 ] : Optional Natural -./concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))-= [] : Optional Integer+./concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural))+= [] : Optional Natural -./concat Integer ([] : Optional (Optional Integer))-= [] : Optional Integer+./concat Natural ([] : Optional (Optional Natural))+= [] : Optional Natural ``` -} let concat
Prelude/Optional/filter view
@@ -4,10 +4,10 @@ Examples: ```-./filter Natural Natural/even ([ +2 ] : Optional Natural)-= [ +2 ] : Optional Natural+./filter Natural Natural/even ([ 2 ] : Optional Natural)+= [ 2 ] : Optional Natural -./filter Natural Natural/odd ([ +2 ] : Optional Natural)+./filter Natural Natural/odd ([ 2 ] : Optional Natural) = [] : Optional Natural ``` -}
Prelude/Optional/fold view
@@ -4,9 +4,9 @@ Examples: ```-./fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2+./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2 -./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0+./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0 ``` -} let fold
Prelude/Optional/head view
@@ -5,20 +5,20 @@ ``` ./head-Integer-[ [ ] : Optional Integer-, [ 1 ] : Optional Integer-, [ 2 ] : Optional Integer+Natural+[ [ ] : Optional Natural+, [ 1 ] : Optional Natural+, [ 2 ] : Optional Natural ]-= [ 1 ] : Optional Integer+= [ 1 ] : Optional Natural ./head-Integer-[ [] : Optional Integer, [] : Optional Integer ]-= [] : Optional Integer+Natural+[ [] : Optional Natural, [] : Optional Natural ]+= [] : Optional Natural -./head Integer ([] : List (Optional Integer))-= [] : Optional Integer+./head Natural ([] : List (Optional Natural))+= [] : Optional Natural ``` -} let head
Prelude/Optional/last view
@@ -5,20 +5,20 @@ ``` ./last-Integer-[ [ ] : Optional Integer-, [ 1 ] : Optional Integer-, [ 2 ] : Optional Integer+Natural+[ [ ] : Optional Natural+, [ 1 ] : Optional Natural+, [ 2 ] : Optional Natural ]-= [ 2 ] : Optional Integer+= [ 2 ] : Optional Natural ./last-Integer-[ [] : Optional Integer, [] : Optional Integer ]-= [] : Optional Integer+Natural+[ [] : Optional Natural, [] : Optional Natural ]+= [] : Optional Natural -./last Integer ([] : List (Optional Integer))-= [] : Optional Integer+./last Natural ([] : List (Optional Natural))+= [] : Optional Natural ``` -} let last
Prelude/Optional/length view
@@ -1,18 +1,18 @@ {--Returns `+1` if the `Optional` value is present and `+0` if the value is absent+Returns `1` if the `Optional` value is present and `0` if the value is absent Examples: ```-./length Integer ([ 2 ] : Optional Integer) = +1+./length Natural ([ 2 ] : Optional Natural) = 1 -./length Integer ([] : Optional Integer) = +0+./length Natural ([] : Optional Natural) = 0 ``` -} let length : ∀(a : Type) → Optional a → Natural = λ(a : Type) → λ(xs : Optional a)- → Optional/fold a xs Natural (λ(_ : a) → +1) +0+ → Optional/fold a xs Natural (λ(_ : a) → 1) 0 in length
Prelude/Optional/map view
@@ -4,7 +4,7 @@ Examples: ```-./map Natural Bool Natural/even ([ +3 ] : Optional Natural)+./map Natural Bool Natural/even ([ 3 ] : Optional Natural) = [ False ] : Optional Bool ./map Natural Bool Natural/even ([] : Optional Natural)
Prelude/Optional/null view
@@ -4,9 +4,9 @@ Examples: ```-./null Integer ([ 2 ] : Optional Integer) = False+./null Natural ([ 2 ] : Optional Natural) = False -./null Integer ([] : Optional Integer) = True+./null Natural ([] : Optional Natural) = True ``` -} let null
Prelude/Optional/toList view
@@ -4,9 +4,9 @@ Examples: ```-./toList Integer ([ 1 ] : Optional Integer) = [ 1 ]+./toList Natural ([ 1 ] : Optional Natural) = [ 1 ] -./toList Integer ([] : Optional Integer) = [] : List Integer+./toList Natural ([] : Optional Natural) = [] : List Natural ``` -} let toList
Prelude/Text/concatMap view
@@ -4,10 +4,10 @@ Examples: ```-./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ]+./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ] = "0 1 2 " -./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer)+./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural) = "" ``` -}
Prelude/Text/concatMapSep view
@@ -5,9 +5,9 @@ Examples: ```-./concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] = "0, 1, 2"+./concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] = "0, 1, 2" -./concatMapSep ", " Integer Integer/show ([] : List Integer) = ""+./concatMapSep ", " Natural Natural/show ([] : List Natural) = "" ``` -} let concatMapSep
dhall.cabal view
@@ -1,5 +1,5 @@ Name: dhall-Version: 1.13.1+Version: 1.14.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1@@ -168,7 +168,7 @@ formatting >= 6.3 && < 6.4 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 ,- insert-ordered-containers >= 0.1.0.1 && < 0.3 ,+ insert-ordered-containers >= 0.2.1.0 && < 0.3 , lens-family-core >= 1.0.0 && < 1.3 , megaparsec >= 6.1.1 && < 6.6 , memory >= 0.14 && < 0.15,@@ -258,7 +258,7 @@ Other-Modules: Paths_dhall -Test-Suite test+Test-Suite tasty Type: exitcode-stdio-1.0 Hs-Source-Dirs: tests Main-Is: Tests.hs@@ -277,7 +277,16 @@ dhall , insert-ordered-containers , prettyprinter ,- tasty >= 0.11.2 && < 1.1 ,+ tasty >= 0.11.2 && < 1.2 , tasty-hunit >= 0.9.2 && < 0.11, text >= 0.11.1.0 && < 1.3 , vector >= 0.11.0.0 && < 0.13++Test-Suite doctest+ Type: exitcode-stdio-1.0+ Hs-Source-Dirs: doctest+ Main-Is: Main.hs+ GHC-Options: -Wall+ Build-Depends:+ base ,+ doctest >= 0.7.0 && < 0.16
dhall/Main.hs view
@@ -11,7 +11,7 @@ import Data.Text.Prettyprint.Doc (Pretty) import Data.Typeable (Typeable) import Data.Version (showVersion)-import Dhall.Core (Expr, Path)+import Dhall.Core (Expr, Import) import Dhall.Import (Imported(..), load) import Dhall.Parser (Src) import Dhall.Pretty (annToAnsiStyle, prettyExpr)@@ -94,13 +94,13 @@ throws (Left e) = Control.Exception.throwIO e throws (Right a) = return a -getExpression :: IO (Expr Src Path)+getExpression :: IO (Expr Src Import) getExpression = do inText <- Data.Text.Lazy.IO.getContents throws (Dhall.Parser.exprFromText "(stdin)" inText) -assertNoImports :: Expr Src Path -> IO (Expr Src X)+assertNoImports :: Expr Src Import -> IO (Expr Src X) assertNoImports expression = throws (traverse (\_ -> Left ImportResolutionDisabled) expression)
+ doctest/Main.hs view
@@ -0,0 +1,6 @@+module Main where++import qualified Test.DocTest++main :: IO ()+main = Test.DocTest.doctest [ "-isrc", "src/Dhall.hs" ]
src/Dhall.hs view
@@ -104,6 +104,9 @@ import qualified Dhall.Parser import qualified Dhall.TypeCheck +-- $setup+-- >>> :set -XOverloadedStrings+ throws :: Exception e => Either e a -> IO a throws (Left e) = Control.Exception.throwIO e throws (Right r) = return r@@ -133,7 +136,7 @@ The first argument determines the type of value that you decode: ->>> input integer "2"+>>> input integer "+2" 2 >>> input (vector double) "[1.0, 2.0]" [1.0,2.0]@@ -169,7 +172,7 @@ -- ^ The decoded value in Haskell inputWith (Type {..}) ctx n txt = do expr <- throws (Dhall.Parser.exprFromText "(input)" txt)- expr' <- Dhall.Import.loadWithContext ctx expr+ expr' <- Dhall.Import.loadWithContext ctx n expr let suffix = ( Data.Text.Lazy.Builder.toLazyText . build@@ -235,13 +238,13 @@ > > > ┌─────────────┐-> │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type+> │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type > └─────────────┘ checker accepts the annotation > >-> ┌────────────────────────┐-> │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type-> └────────────────────────┘ checker accepts the annotation+> ┌───────────────────────┐+> │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type+> └───────────────────────┘ checker accepts the annotation > > > ┌────────────────────┐@@ -362,7 +365,7 @@ {-| Decode a `Natural` ->>> input natural "+42"+>>> input natural "42" 42 -} natural :: Type Natural@@ -375,7 +378,7 @@ {-| Decode an `Integer` ->>> input integer "42"+>>> input integer "+42" 42 -} integer :: Type Integer@@ -430,7 +433,7 @@ {-| Decode a `Maybe` ->>> input (maybe integer) "[1] : Optional Integer"+>>> input (maybe natural) "[1] : Optional Natural" Just 1 -} maybe :: Type a -> Type (Maybe a)@@ -443,8 +446,8 @@ {-| Decode a `Seq` -->>> input (sequence integer) "[1, 2, 3]"-[1,2,3]+>>> input (sequence natural) "[1, 2, 3]"+fromList [1,2,3] -} sequence :: Type a -> Type (Seq a) sequence (Type extractIn expectedIn) = Type extractOut expectedOut@@ -456,7 +459,7 @@ {-| Decode a list ->>> input (list integer) "[1, 2, 3]"+>>> input (list natural) "[1, 2, 3]" [1,2,3] -} list :: Type a -> Type [a]@@ -464,7 +467,7 @@ {-| Decode a `Vector` ->>> input (vector integer) "[1, 2, 3]"+>>> input (vector natural) "[1, 2, 3]" [1,2,3] -} vector :: Type a -> Type (Vector a)@@ -472,8 +475,8 @@ {-| Decode `()` from an empty record. ->>> input unit "{=}"-()+>>> input unit "{=}" -- GHC doesn't print the result if it is @()@+ -} unit :: Type () unit = Type extractOut expectedOut@@ -495,8 +498,8 @@ {-| Given a pair of `Type`s, decode a tuple-record into their pairing. ->>> input (pair natural bool) "{ _1 = +42, _2 = False }"-(42, False)+>>> input (pair natural bool) "{ _1 = 42, _2 = False }"+(42,False) -} pair :: Type a -> Type b -> Type (a, b) pair l r = Type extractOut expectedOut@@ -517,7 +520,7 @@ {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input` ->>> input auto "[1, 2, 3]" :: IO (Vector Integer)+>>> input auto "[1, 2, 3]" :: IO (Vector Natural) [1,2,3] This class auto-generates a default implementation for records that@@ -1077,7 +1080,7 @@ > , description = > "A configuration language guaranteed to terminate" > , stars =-> +289+> 289 > } Our parser has type 'Type' @Project@, but we can't build that out of any
src/Dhall/Core.hs view
@@ -18,11 +18,14 @@ module Dhall.Core ( -- * Syntax Const(..)- , HasHome(..)- , PathType(..)- , PathHashed(..)- , PathMode(..)- , Path(..)+ , Directory(..)+ , File(..)+ , FilePrefix(..)+ , Import(..)+ , ImportHashed(..)+ , ImportMode(..)+ , ImportType(..)+ , Path , Var(..) , Chunks(..) , Expr(..)@@ -79,9 +82,8 @@ import qualified Data.Sequence import qualified Data.Set import qualified Data.Text-import qualified Data.Text.Lazy as Text-import qualified Data.Text.Lazy.Builder as Builder-import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Text.Prettyprint.Doc as Pretty {-| Constants for a pure type system @@ -105,64 +107,145 @@ instance Buildable Const where build = buildConst --- | Whether or not a path is relative to the user's home directory-data HasHome = Home | Homeless deriving (Eq, Ord, Show)+{-| Internal representation of a directory that stores the path components in+ reverse order --- | The type of path to import (i.e. local vs. remote vs. environment)-data PathType- = File HasHome FilePath+ In other words, the directory @/foo/bar/baz@ is encoded as+ @Directory { components = [ "baz", "bar", "foo" ] }@+-}+newtype Directory = Directory { components :: [Text] }+ deriving (Eq, Ord, Show)++instance Semigroup Directory where+ Directory components₀ <> Directory components₁ =+ Directory (components₁ <> components₀)++instance Buildable Directory where+ build (Directory {..}) =+ foldMap buildComponent (reverse components)+ where+ buildComponent text = "/" <> build text++{-| A `File` is a `directory` followed by one additional path component+ representing the `file` name+-}+data File = File+ { directory :: Directory+ , file :: Text+ } deriving (Eq, Ord, Show)++instance Buildable File where+ build (File {..}) = build directory <> "/" <> build file++instance Semigroup File where+ File directory₀ _ <> File directory₁ file =+ File (directory₀ <> directory₁) file++data FilePrefix+ = Absolute+ -- ^ Absolute path+ | Here+ -- ^ Path relative to @.@+ | Parent+ -- ^ Path relative to @..@+ | Home+ -- ^ Path relative to @~@+ deriving (Eq, Ord, Show)++instance Buildable FilePrefix where+ build Absolute = ""+ build Here = "."+ build Parent = ".."+ build Home = "~"++-- | The type of import (i.e. local vs. remote vs. environment)+data ImportType+ = Local FilePrefix File -- ^ Local path- | URL Text (Maybe PathHashed)- -- ^ URL of remote resource and optional headers stored in a path+ | URL Text File Text (Maybe ImportHashed)+ -- ^ URL of remote resource and optional headers stored in an import | Env Text -- ^ Environment variable deriving (Eq, Ord, Show) -instance Buildable PathType where- build (File Home file)- = "~/" <> build (Text.pack file)- build (File Homeless file)- | Text.isPrefixOf "./" txt- || Text.isPrefixOf "/" txt- || Text.isPrefixOf "../" txt- = build txt <> " "- | otherwise- = "./" <> build txt <> " "+parent :: File+parent = File { directory = Directory { components = [ ".." ] }, file = "" }++instance Semigroup ImportType where+ Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁)++ URL prefix file₀ suffix headers <> Local Here file₁ =+ URL prefix (file₀ <> file₁) suffix headers++ Local prefix file₀ <> Local Parent file₁ =+ Local prefix (file₀ <> parent <> file₁)++ URL prefix file₀ suffix headers <> Local Parent file₁ =+ URL prefix (file₀ <> parent <> file₁) suffix headers++ _ <> import₁ =+ import₁++instance Buildable ImportType where+ build (Local prefix file) =+ build prefix <> build file <> " "++ build (URL prefix file suffix headers) =+ build prefix+ <> build file+ <> build suffix+ <> foldMap buildHeaders headers+ <> " " where- txt = Text.pack file- build (URL str Nothing ) = build str <> " "- build (URL str (Just headers)) = build str <> " using " <> build headers <> " "- build (Env env) = "env:" <> build env+ buildHeaders h = " using " <> build h --- | How to interpret the path's contents (i.e. as Dhall code or raw text)-data PathMode = Code | RawText deriving (Eq, Ord, Show)+ build (Env env) =+ "env:" <> build env <> " " --- | A `PathType` extended with an optional hash for semantic integrity checks-data PathHashed = PathHashed- { hash :: Maybe (Crypto.Hash.Digest SHA256)- , pathType :: PathType+-- | How to interpret the import's contents (i.e. as Dhall code or raw text)+data ImportMode = Code | RawText deriving (Eq, Ord, Show)++-- | A `ImportType` extended with an optional hash for semantic integrity checks+data ImportHashed = ImportHashed+ { hash :: Maybe (Crypto.Hash.Digest SHA256)+ , importType :: ImportType } deriving (Eq, Ord, Show) -instance Buildable PathHashed where- build (PathHashed Nothing p) = build p- build (PathHashed (Just h) p) = build p <> "sha256:" <> build (show h) <> " "+instance Semigroup ImportHashed where+ ImportHashed _ importType₀ <> ImportHashed hash importType₁ =+ ImportHashed hash (importType₀ <> importType₁) --- | Path to an external resource-data Path = Path- { pathHashed :: PathHashed- , pathMode :: PathMode+instance Buildable ImportHashed where+ build (ImportHashed Nothing p) =+ build p+ build (ImportHashed (Just h) p) =+ build p <> "sha256:" <> build (show h) <> " "++-- | Reference to an external resource+data Import = Import+ { importHashed :: ImportHashed+ , importMode :: ImportMode } deriving (Eq, Ord, Show) -instance Buildable Path where- build (Path {..}) = build pathHashed <> suffix+instance Semigroup Import where+ Import importHashed₀ _ <> Import importHashed₁ code =+ Import (importHashed₀ <> importHashed₁) code++instance Buildable Import where+ build (Import {..}) = build importHashed <> suffix where- suffix = case pathMode of+ suffix = case importMode of RawText -> "as Text" Code -> "" -instance Pretty Path where- pretty path = Pretty.pretty (Builder.toLazyText (build path))+instance Pretty Import where+ pretty import_ = Pretty.pretty (Builder.toLazyText (build import_)) +-- | Type synonym for `Import`, provided for backwards compatibility+type Path = Import++{-# DEPRECATED Path "Use Dhall.Core.Import instead" #-}+ {-| Label for a bound variable The `Text` field is the variable's name (i.e. \"@x@\").@@ -239,7 +322,7 @@ | BoolIf (Expr s a) (Expr s a) (Expr s a) -- | > Natural ~ Natural | Natural- -- | > NaturalLit n ~ +n+ -- | > NaturalLit n ~ n | NaturalLit Natural -- | > NaturalFold ~ Natural/fold | NaturalFold@@ -261,7 +344,7 @@ | NaturalTimes (Expr s a) (Expr s a) -- | > Integer ~ Integer | Integer- -- | > IntegerLit n ~ n+ -- | > IntegerLit n ~ ±n | IntegerLit Integer -- | > IntegerShow ~ Integer/show | IntegerShow@@ -332,7 +415,7 @@ | Project (Expr s a) (Set Text) -- | > Note s x ~ e | Note s (Expr s a)- -- | > Embed path ~ path+ -- | > Embed import ~ import | Embed a deriving (Functor, Foldable, Traversable, Show, Eq) @@ -1302,9 +1385,10 @@ App NaturalOdd (NaturalLit n) -> BoolLit (odd n) App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n) App NaturalShow (NaturalLit n) ->- TextLit (Chunks [] ("+" <> buildNatural n))- App IntegerShow (IntegerLit n) ->- TextLit (Chunks [] (buildNumber n))+ TextLit (Chunks [] (buildNatural n))+ App IntegerShow (IntegerLit n)+ | 0 <= n -> TextLit (Chunks [] ("+" <> buildNumber n))+ | otherwise -> TextLit (Chunks [] (buildNumber n)) App DoubleShow (DoubleLit n) -> TextLit (Chunks [] (buildScientific n)) App (App OptionalBuild _A₀) g ->
src/Dhall/Import.hs view
@@ -1,7 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall #-} @@ -58,10 +60,6 @@ > http://example.com/id - You can also reuse directory names as expressions. If you provide a path- to a local or remote directory then the compiler will look for a file named- @\@@ within that directory and use that file to represent the directory.- You can also import expressions stored within environment variables using @env:NAME@, where @NAME@ is the name of the environment variable. For example:@@ -74,7 +72,7 @@ > > { bar = "Hi", baz = λ(x : Bool) → x == False, foo = 1 } - If you wish to import the raw contents of a path as @Text@ then add+ If you wish to import the raw contents of an impoert as @Text@ then add @as Text@ to the end of the import: > $ dhall <<< "http://example.com as Text"@@ -101,7 +99,7 @@ module Dhall.Import ( -- * Import- exprFromPath+ exprFromImport , load , loadWith , loadWithContext@@ -118,17 +116,16 @@ ) where import Control.Applicative (empty)-import Control.Exception- (Exception, IOException, SomeException, onException, throwIO)+import Control.Exception (Exception, SomeException, throwIO) import Control.Monad (join) import Control.Monad.Catch (throwM, MonadCatch(catch)) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Crypto.Hash (SHA256)-import Data.ByteString.Lazy (ByteString) import Data.CaseInsensitive (CI)+import Data.List.NonEmpty (NonEmpty(..)) import Data.Map (Map)-import Data.Monoid ((<>))+import Data.Semigroup (sconcat, (<>)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) #if MIN_VERSION_base(4,8,0)@@ -141,11 +138,13 @@ import Dhall.Core ( Expr(..) , Chunks(..)- , HasHome(..)- , PathHashed(..)- , PathMode(..)- , PathType(..)- , Path(..)+ , Directory(..)+ , File(..)+ , FilePrefix(..)+ , ImportHashed(..)+ , ImportType(..)+ , ImportMode(..)+ , Import(..) ) import Dhall.Parser (Parser(..), ParseError(..), Src(..)) import Dhall.TypeCheck (X(..))@@ -167,7 +166,6 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.Map.Strict as Map import qualified Data.Text.Encoding-import qualified Data.Text.IO import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Encoding@@ -190,14 +188,15 @@ -- | An import failed because of a cycle in the import graph newtype Cycle = Cycle- { cyclicImport :: Path -- ^ The offending cyclic import+ { cyclicImport :: Import -- ^ The offending cyclic import } deriving (Typeable) instance Exception Cycle instance Show Cycle where- show (Cycle path) = "\nCyclic import: " ++ builderToString (build path)+ show (Cycle import_) =+ "\nCyclic import: " ++ builderToString (build import_) {-| Dhall tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will@@ -226,33 +225,33 @@ All other imports are defined to be non-local -} newtype ReferentiallyOpaque = ReferentiallyOpaque- { opaqueImport :: Path -- ^ The offending opaque import+ { opaqueImport :: Import -- ^ The offending opaque import } deriving (Typeable) instance Exception ReferentiallyOpaque instance Show ReferentiallyOpaque where- show (ReferentiallyOpaque path) =- "\nReferentially opaque import: " ++ builderToString (build path)+ show (ReferentiallyOpaque import_) =+ "\nReferentially opaque import: " ++ builderToString (build import_) -- | Extend another exception with the current import stack data Imported e = Imported- { importStack :: [Path] -- ^ Imports resolved so far, in reverse order- , nested :: e -- ^ The nested exception+ { importStack :: [Import] -- ^ Imports resolved so far, in reverse order+ , nested :: e -- ^ The nested exception } deriving (Typeable) instance Exception e => Exception (Imported e) instance Show e => Show (Imported e) where- show (Imported paths e) =- (case paths of [] -> ""; _ -> "\n")- ++ unlines (map indent paths')+ show (Imported imports e) =+ (case imports of [] -> ""; _ -> "\n")+ ++ unlines (map indent imports') ++ show e where- indent (n, path) =- take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)- -- Canonicalize all paths- paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths)))+ indent (n, import_) =+ take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build import_)+ -- Canonicalize all imports+ imports' = zip [0..] (drop 1 (reverse (canonicalizeAll imports))) -- | Newtype used to wrap `HttpException`s with a prettier `Show` instance newtype PrettyHttpException = PrettyHttpException HttpException@@ -328,10 +327,10 @@ -- | State threaded throughout the import process data Status = Status- { _stack :: [Path]- -- ^ Stack of `Path`s that we've imported along the way to get to the+ { _stack :: [Import]+ -- ^ Stack of `Import`s that we've imported along the way to get to the -- current point- , _cache :: Map Path (Expr Src X)+ , _cache :: Map Import (Expr Src X) -- ^ Cache of imported expressions in order to avoid importing the same -- expression twice with different values , _manager :: Maybe Manager@@ -342,13 +341,13 @@ emptyStatus :: Status emptyStatus = Status [] Map.empty Nothing -canonicalizeAll :: [Path] -> [Path]-canonicalizeAll = map canonicalizePath . List.tails+canonicalizeAll :: [Import] -> [Import]+canonicalizeAll = map canonicalizeImport . List.tails -stack :: Functor f => LensLike' f Status [Path]+stack :: Functor f => LensLike' f Status [Import] stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) -cache :: Functor f => LensLike' f Status (Map Path (Expr Src X))+cache :: Functor f => LensLike' f Status (Map Import (Expr Src X)) cache k s = fmap (\x -> s { _cache = x }) (k (_cache s)) manager :: Functor f => LensLike' f Status (Maybe Manager)@@ -370,107 +369,62 @@ zoom manager (State.put (Just m)) return m -{-| This function computes the current path by taking the last absolute path- (either an absolute `FilePath` or `URL`) and combining it with all following- relative paths+{-|+> canonicalize (canonicalize x) = canonicalize x+-}+class Canonicalize path where+ canonicalize :: path -> path - For example, if the file `./foo/bar` imports `./baz`, that will resolve to- `./foo/baz`. Relative imports are relative to a file's parent directory.- This also works for URLs, too.+instance Canonicalize Directory where+ canonicalize (Directory []) = Directory [] - This code is full of all sorts of edge cases so it wouldn't surprise me at- all if you find something broken in here. Most of the ugliness is due to:+ canonicalize (Directory ("." : components₀)) =+ canonicalize (Directory components₀) - * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only- if you navigate to any downstream relative paths- * Removing spurious @.@s and @..@s from the path+ canonicalize (Directory (".." : components₀)) =+ case canonicalize (Directory components₀) of+ Directory [] -> Directory [ ".." ]+ Directory (_ : components₁) -> Directory components₁ - Also, there are way too many `reverse`s in the URL-handling code For now I- don't mind, but if were to really do this correctly we'd store the URLs as- `Text` for O(1) access to the end of the string. The only reason we use- `String` at all is for consistency with the @http-client@ library.--}-canonicalize :: [PathType] -> PathType-canonicalize [] = File Homeless "."-canonicalize (File hasHome0 file0:paths0) =- if FilePath.isRelative file0 && hasHome0 == Homeless- then go file0 paths0- else File hasHome0 (FilePath.normalise file0)- where- go currPath [] = File Homeless (FilePath.normalise currPath)- go currPath (Env _ :_ ) = File Homeless (FilePath.normalise currPath)- go currPath (URL url0 headers:rest ) = combine prefix suffix+ canonicalize (Directory (component : components₀)) =+ Directory (component : components₁) where- headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers-- prefix = parentURL (removeAtFromURL url0)+ Directory components₁ = canonicalize (Directory components₀) - suffix = FilePath.normalise currPath+instance Canonicalize File where+ canonicalize (File { directory, .. }) =+ File { directory = canonicalize directory, .. } - -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still- -- need to manually handle @.@/@..@'s at the beginning of the path- combine url path = case List.stripPrefix "../" path of- Just path' -> combine url' path'- where- url' = parentURL (removeAtFromURL url)- Nothing -> case List.stripPrefix "./" path of- Just path' -> combine url path'- Nothing ->- -- This `last` is safe because the lexer constrains all- -- URLs to be non-empty. I couldn't find a simple and safe- -- equivalent in the `text` API- case Text.last url of- '/' -> URL (url <> path') headers'- _ -> URL (url <> "/" <> path') headers'- where- path' = Text.pack path- go currPath (File hasHome file:paths) =- if FilePath.isRelative file && hasHome == Homeless- then go file' paths- else File hasHome (FilePath.normalise file')- where- file' = FilePath.takeDirectory (removeAtFromFilename file) </> currPath-canonicalize (URL path headers:rest) = URL path headers'- where- headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers-canonicalize (Env env :_ ) = Env env+instance Canonicalize ImportType where+ canonicalize (Local prefix file) =+ Local prefix (canonicalize file) -onPathType :: (PathType -> PathType) -> PathHashed -> PathHashed-onPathType f (PathHashed a b) = PathHashed a (f b)+ canonicalize (URL prefix file suffix header) =+ URL prefix (canonicalize file) suffix header -canonicalizePath :: [Path] -> Path-canonicalizePath [] =- Path- { pathMode = Code- , pathHashed = PathHashed- { hash = Nothing- , pathType = canonicalize []- }- }-canonicalizePath (path:paths) =- Path- { pathMode = pathMode path- , pathHashed = (pathHashed path)- { hash = hash (pathHashed path)- , pathType =- canonicalize (map (pathType . pathHashed) (path:paths))- }- }+ canonicalize (Env name) =+ Env name -parentURL :: Text -> Text-parentURL = Text.dropWhileEnd (/= '/')+instance Canonicalize ImportHashed where+ canonicalize (ImportHashed hash importType) =+ ImportHashed hash (canonicalize importType) -removeAtFromURL:: Text -> Text-removeAtFromURL url- | Text.isSuffixOf "/@" url = Text.dropEnd 2 url- | Text.isSuffixOf "/" url = Text.dropEnd 1 url- | otherwise = url+instance Canonicalize Import where+ canonicalize (Import importHashed importMode) =+ Import (canonicalize importHashed) importMode -removeAtFromFilename :: FilePath -> FilePath-removeAtFromFilename fp =- if FilePath.takeFileName fp == "@"- then FilePath.takeDirectory fp- else fp+canonicalizeImport :: [Import] -> Import+canonicalizeImport imports =+ canonicalize (sconcat (defaultImport :| reverse imports))+ where+ defaultImport =+ Import+ { importMode = Code+ , importHashed = ImportHashed+ { hash = Nothing+ , importType = Local Here (File (Directory []) ".")+ }+ } toHeaders :: Expr s a@@ -549,262 +503,235 @@ <> "\n" <> "↳ " <> show actualHash <> "\n" --- | Parse an expression from a `Path` containing a Dhall program-exprFromPath :: Path -> StateT Status IO (Expr Src Path)-exprFromPath (Path {..}) = case pathType of- File hasHome file -> liftIO (do- path <- case hasHome of- Home -> do- home <- System.Directory.getHomeDirectory- return (home </> file)- Homeless -> do- return file+-- | Parse an expression from a `Import` containing a Dhall program+exprFromImport :: Import -> StateT Status IO (Expr Src Import)+exprFromImport (Import {..}) = do+ let ImportHashed {..} = importHashed - case pathMode of- Code -> do- exists <- System.Directory.doesFileExist path- if exists- then return ()- else throwIO (MissingFile path)+ (path, text) <- case importType of+ Local prefix (File {..}) -> liftIO $ do+ let Directory {..} = directory - -- Unfortunately, GHC throws an `InappropriateType` exception- -- when trying to read a directory, but does not export the- -- exception, so I must resort to a more heavy-handed `catch`- let handler :: IOException -> IO Text- handler e = do- -- If the fallback fails, reuse the original exception- -- to avoid user confusion- Data.Text.Lazy.IO.readFile (path </> "@")- `onException` throwIO e+ prefixPath <- case prefix of+ Home -> do+ System.Directory.getHomeDirectory - text <- Data.Text.Lazy.IO.readFile path `catch` handler- case Text.Megaparsec.parse parser path text of- Left errInfo -> do- throwIO (ParseError errInfo text)- Right expr -> do- return expr- RawText -> do- text <- Data.Text.IO.readFile path- return (TextLit (Chunks [] (build text))) )- URL url headerPath -> do- m <- needManager- request <- liftIO (HTTP.parseUrlThrow (Text.unpack url))+ Absolute -> do+ return "/" - let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString)-#if MIN_VERSION_http_client(0,5,0)- handler err@(HttpExceptionRequest _ (StatusCodeException _ _)) = do-#else- handler err@(StatusCodeException _ _ _) = do-#endif- let request' = request { HTTP.path = HTTP.path request <> "/@" }- -- If the fallback fails, reuse the original exception to avoid- -- user confusion- HTTP.httpLbs request' m `onException` throwIO (PrettyHttpException err)- handler err = throwIO (PrettyHttpException err)+ Parent -> do+ pwd <- System.Directory.getCurrentDirectory+ return (FilePath.takeDirectory pwd) - requestWithHeaders <- case headerPath of- Nothing -> return request- Just path -> do- expr <- loadStaticIO Dhall.Context.empty (Path path Code)- let expected :: Expr Src X- expected =- App List- ( Record- ( Data.HashMap.Strict.InsOrd.fromList- [("header", Text), ("value", Text)]+ Here -> do+ System.Directory.getCurrentDirectory++ let cs = map Text.unpack (file : components)++ let cons component dir = dir </> component++ let path = foldr cons prefixPath cs++ exists <- System.Directory.doesFileExist path++ if exists+ then return ()+ else throwIO (MissingFile path)++ text <- Data.Text.Lazy.IO.readFile path++ return (path, text)++ URL prefix file suffix maybeHeaders -> do+ m <- needManager++ let fileText = Builder.toLazyText (build file)+ let url = Text.unpack (prefix <> fileText <> suffix)++ request <- liftIO (HTTP.parseUrlThrow url)++ requestWithHeaders <- case maybeHeaders of+ Nothing -> return request+ Just importHashed_ -> do+ expr <- loadStaticIO Dhall.Context.empty+ (const Nothing)+ (Import importHashed_ Code)+ let expected :: Expr Src X+ expected =+ App List+ ( Record+ ( Data.HashMap.Strict.InsOrd.fromList+ [("header", Text), ("value", Text)]+ ) )- )- let suffix =- ( Builder.toLazyText- . build- ) expected- let annot = case expr of- Note (Src begin end bytes) _ ->- Note (Src begin end bytes') (Annot expr expected)- where- bytes' = bytes <> " : " <> suffix- _ ->- Annot expr expected- case Dhall.TypeCheck.typeOf annot of- Left err -> liftIO (throwIO err)- Right _ -> return ()- let expr' = Dhall.Core.normalize expr- headers <- case toHeaders expr' of- Just headers -> do- return headers- Nothing -> do- liftIO (throwIO InternalError)- let requestWithHeaders = request- { HTTP.requestHeaders = headers- }- return requestWithHeaders- response <- liftIO (HTTP.httpLbs requestWithHeaders m `catch` handler)+ let suffix_ =+ ( Builder.toLazyText+ . build+ ) expected+ let annot = case expr of+ Note (Src begin end bytes) _ ->+ Note (Src begin end bytes') (Annot expr expected)+ where+ bytes' = bytes <> " : " <> suffix_+ _ ->+ Annot expr expected - let bytes = HTTP.responseBody response+ case Dhall.TypeCheck.typeOf annot of+ Left err -> liftIO (throwIO err)+ Right _ -> return () - text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of- Left err -> liftIO (throwIO err)- Right text -> return text+ let expr' = Dhall.Core.normalize expr - case pathMode of- Code ->- case Text.Megaparsec.parse parser (Text.unpack url) text of- Left err -> do- -- Also try the fallback in case of a parse error, since- -- the parse error might signify that this URL points to- -- a directory list- let err' = ParseError err text+ headers <- case toHeaders expr' of+ Just headers -> do+ return headers+ Nothing -> do+ liftIO (throwIO InternalError) - request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url))+ let requestWithHeaders = request+ { HTTP.requestHeaders = headers+ } - let request'' =- request'- { HTTP.path = HTTP.path request' <> "/@" }- response' <- liftIO (HTTP.httpLbs request'' m `onException` throwIO err' )+ return requestWithHeaders - let bytes' = HTTP.responseBody response'+ response <- liftIO (HTTP.httpLbs requestWithHeaders m) - text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of- Left _ -> liftIO (throwIO err')- Right text' -> return text'+ let bytes = HTTP.responseBody response - case Text.Megaparsec.parse parser (Text.unpack url) text' of- Left _ -> liftIO (throwIO err')- Right expr -> return expr- Right expr -> return expr- RawText -> do- return (TextLit (Chunks [] (build text)))- Env env -> liftIO (do- x <- System.Environment.lookupEnv (Text.unpack env)- case x of- Just str -> do- let text = Text.pack str- case pathMode of- Code ->- case Text.Megaparsec.parse parser (Text.unpack env) text of- Left errInfo -> do- throwIO (ParseError errInfo text)- Right expr -> do- return expr- RawText -> return (TextLit (Chunks [] (build str)))- Nothing -> throwIO (MissingEnvironmentVariable env) )- where- PathHashed {..} = pathHashed+ case Data.Text.Lazy.Encoding.decodeUtf8' bytes of+ Left err -> liftIO (throwIO err)+ Right text -> return (url, text) - parser = unParser (do- Text.Parser.Token.whiteSpace- r <- Dhall.Parser.expr- Text.Parser.Combinators.eof- return r )+ Env env -> liftIO $ do+ x <- System.Environment.lookupEnv (Text.unpack env)+ case x of+ Just string -> return (Text.unpack env, Text.pack string)+ Nothing -> throwIO (MissingEnvironmentVariable env) -{-| Load a `Path` as a \"dynamic\" expression (without resolving any imports)+ case importMode of+ Code -> do+ let parser = unParser $ do+ Text.Parser.Token.whiteSpace+ r <- Dhall.Parser.expr+ Text.Parser.Combinators.eof+ return r - This also returns the true final path (i.e. explicit "/@" at the end for- directories)+ case Text.Megaparsec.parse parser path text of+ Left errInfo -> do+ liftIO (throwIO (ParseError errInfo text))+ Right expr -> do+ return expr++ RawText -> do+ return (TextLit (Chunks [] (build text)))++{-| Load an `Import` as a \"dynamic\" expression (without resolving any imports) -} loadDynamic :: forall m . MonadCatch m- => (Path -> StateT Status m (Expr Src Path))- -> Path- -> StateT Status m (Expr Src Path)-loadDynamic from_path p = do- paths <- zoom stack State.get+ => (Import -> StateT Status m (Expr Src Import))+ -> Import+ -> StateT Status m (Expr Src Import)+loadDynamic from_import import_ = do+ imports <- zoom stack State.get - let handler :: SomeException -> StateT Status m (Expr Src Path)- handler e = throwM (Imported (p:paths) e)+ let handler :: SomeException -> StateT Status m (Expr Src Import)+ handler e = throwM (Imported (import_:imports) e) - from_path (canonicalizePath (p:paths)) `catch` handler+ from_import (canonicalizeImport (import_:imports)) `catch` handler loadStaticIO :: Dhall.Context.Context (Expr Src X)- -> Path+ -> Dhall.Core.Normalizer X+ -> Import -> StateT Status IO (Expr Src X)-loadStaticIO = loadStaticWith exprFromPath+loadStaticIO = loadStaticWith exprFromImport --- | Resolve all imports within an expression using a custom typing context and Path--- resolving callback in arbitrary `MonadCatch` monad.+-- | Resolve all imports within an expression using a custom typing context and+-- `Import`-resolving callback in arbitrary `MonadCatch` monad. loadWith :: MonadCatch m- => (Path -> StateT Status m (Expr Src Path))+ => (Import -> StateT Status m (Expr Src Import)) -> Dhall.Context.Context (Expr Src X)- -> Expr Src Path+ -> Dhall.Core.Normalizer X+ -> Expr Src Import -> m (Expr Src X)-loadWith from_path ctx = evalStatus (loadStaticWith from_path ctx)+loadWith from_import ctx n = evalStatus (loadStaticWith from_import ctx n) -- | Resolve all imports within an expression using a custom typing context. -- -- @load = loadWithContext Dhall.Context.empty@ loadWithContext :: Dhall.Context.Context (Expr Src X)- -> Expr Src Path+ -> Dhall.Core.Normalizer X+ -> Expr Src Import -> IO (Expr Src X)-loadWithContext ctx = evalStatus (loadStaticIO ctx)+loadWithContext ctx n = evalStatus (loadStaticIO ctx n) loadStaticWith :: MonadCatch m- => (Path -> StateT Status m (Expr Src Path))+ => (Import -> StateT Status m (Expr Src Import)) -> Dhall.Context.Context (Expr Src X)- -> Path+ -> Dhall.Core.Normalizer X+ -> Import -> StateT Status m (Expr Src X)-loadStaticWith from_path ctx path = do- paths <- zoom stack State.get+loadStaticWith from_import ctx n import_ = do+ imports <- zoom stack State.get - let local (Path (PathHashed _ (URL _ _ )) _) = False- local (Path (PathHashed _ (File _ _)) _) = True- local (Path (PathHashed _ (Env _ )) _) = True+ let local (Import (ImportHashed _ (URL {})) _) = False+ local (Import (ImportHashed _ (Local {})) _) = True+ local (Import (ImportHashed _ (Env {})) _) = True - let parent = canonicalizePath paths- let here = canonicalizePath (path:paths)+ let parent = canonicalizeImport imports+ let here = canonicalizeImport (import_:imports) if local here && not (local parent)- then throwM (Imported paths (ReferentiallyOpaque path))+ then throwM (Imported imports (ReferentiallyOpaque import_)) else return () - (expr, cached) <- if here `elem` canonicalizeAll paths- then throwM (Imported paths (Cycle path))+ expr <- if here `elem` canonicalizeAll imports+ then throwM (Imported imports (Cycle import_)) else do m <- zoom cache State.get case Map.lookup here m of- Just expr -> return (expr, True)+ Just expr -> return expr Nothing -> do- expr' <- loadDynamic from_path path+ expr' <- loadDynamic from_import import_ expr'' <- case traverse (\_ -> Nothing) expr' of -- No imports left- Just expr -> do- zoom cache (State.put $! Map.insert here expr m)- return expr+ Just expr -> return expr -- Some imports left, so recurse Nothing -> do- let paths' = path:paths- zoom stack (State.put paths')- expr'' <- fmap join (traverse (loadStaticWith from_path ctx)+ let imports' = import_:imports+ zoom stack (State.put imports')+ expr'' <- fmap join (traverse (loadStaticWith from_import ctx n) expr')- zoom stack (State.put paths)+ zoom stack (State.put imports) return expr''- return (expr'', False)-- -- Type-check expressions here for three separate reasons:- --- -- * to verify that they are closed- -- * to catch type errors as early in the import process as possible- -- * to avoid normalizing ill-typed expressions that need to be hashed- --- -- There is no need to check expressions that have been cached, since they- -- have already been checked- if cached- then return ()- else case Dhall.TypeCheck.typeWith ctx expr of- Left err -> throwM (Imported (path:paths) err)- Right _ -> return ()+ -- Type-check expressions here for three separate reasons:+ --+ -- * to verify that they are closed+ -- * to catch type errors as early in the import process+ -- as possible+ -- * to avoid normalizing ill-typed expressions that need+ -- to be hashed+ --+ -- There is no need to check expressions that have been+ -- cached, since they have already been checked+ expr''' <- case Dhall.TypeCheck.typeWith ctx expr'' of+ Left err -> throwM (Imported (import_:imports) err)+ Right _ -> return (Dhall.Core.normalizeWith n expr'')+ zoom cache (State.put $! Map.insert here expr''' m)+ return expr''' - case hash (pathHashed path) of+ case hash (importHashed import_) of Nothing -> do return () Just expectedHash -> do let actualHash = hashExpression expr if expectedHash == actualHash then return ()- else throwM (HashMismatch {..})+ else throwM (Imported (import_:imports) (HashMismatch {..})) return expr @@ -814,8 +741,8 @@ evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) emptyStatus -- | Resolve all imports within an expression-load :: Expr Src Path -> IO (Expr Src X)-load = loadWithContext Dhall.Context.empty+load :: Expr Src Import -> IO (Expr Src X)+load = loadWithContext Dhall.Context.empty (const Nothing) -- | Hash a fully resolved expression hashExpression :: Expr s X -> (Crypto.Hash.Digest SHA256)
src/Dhall/Parser.hs view
@@ -50,6 +50,7 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet import qualified Data.List+import qualified Data.List.NonEmpty import qualified Data.Sequence import qualified Data.Set import qualified Data.Text@@ -748,11 +749,15 @@ return (sign a) ) <?> "double literal" integerLiteral :: Parser Integer-integerLiteral = Text.Parser.Token.integer <?> "integer literal"+integerLiteral = (do+ let positive = fmap (\_ -> id ) (Text.Parser.Char.char '+')+ let negative = fmap (\_ -> negate) (Text.Parser.Char.char '-')+ sign <- positive <|> negative+ a <- Text.Parser.Token.natural+ return (sign a) ) <?> "integer literal" naturalLiteral :: Parser Natural naturalLiteral = (do- _ <- Text.Parser.Char.char '+' a <- Text.Parser.Token.natural return (fromIntegral a) ) <?> "natural literal" @@ -767,75 +772,87 @@ n <- indexed <|> pure 0 return (V x n) -headPathCharacter :: Char -> Bool-headPathCharacter c =- ('\x21' <= c && c <= '\x27')+pathCharacter :: Char -> Bool+pathCharacter c =+ ('\x21' <= c && c <= '\x22')+ || ('\x24' <= c && c <= '\x27') || ('\x2A' <= c && c <= '\x2B') || ('\x2D' <= c && c <= '\x2E') || ('\x30' <= c && c <= '\x3B') || c == '\x3D'- || ('\x3F' <= c && c <= '\x5A')+ || ('\x40' <= c && c <= '\x5A') || ('\x5E' <= c && c <= '\x7A') || c == '\x7C' || c == '\x7E' -pathCharacter :: Char -> Bool-pathCharacter c =- headPathCharacter c- || c == '\\'- || c == '/'+pathComponent :: Parser Text+pathComponent = do+ _ <- "/" :: Parser Builder+ string <- some (Text.Parser.Char.satisfy pathCharacter) -fileRaw :: Parser PathType-fileRaw =+ return (Data.Text.Lazy.pack string)++file_ :: Parser File+file_ = do+ path <- Data.List.NonEmpty.some1 pathComponent++ let directory = Directory (reverse (Data.List.NonEmpty.init path))+ let file = Data.List.NonEmpty.last path++ return (File {..})++localRaw :: Parser ImportType+localRaw = choice- [ try absolutePath- , relativePath- , parentPath+ [ parentPath+ , herePath , homePath+ , try absolutePath ] where- absolutePath = do- _ <- Text.Parser.Char.char '/'- a <- Text.Parser.Char.satisfy headPathCharacter- bs <- many (Text.Parser.Char.satisfy pathCharacter)- let filepath = '/':a:bs- return (File Homeless filepath)+ parentPath = do+ _ <- ".." :: Parser Builder+ file <- file_ - relativePath = do- _ <- Text.Parser.Char.text "./"- as <- many (Text.Parser.Char.satisfy pathCharacter)- let filepath = "./" <> as- return (File Homeless filepath)+ return (Local Parent file) - parentPath = do- _ <- Text.Parser.Char.text "../"- as <- many (Text.Parser.Char.satisfy pathCharacter)- let filepath = "../" <> as- return (File Homeless filepath)+ herePath = do+ _ <- "." :: Parser Builder+ file <- file_ + return (Local Here file)+ homePath = do- _ <- Text.Parser.Char.text "~/"- as <- many (Text.Parser.Char.satisfy pathCharacter)- return (File Home as)+ _ <- "~" :: Parser Builder+ file <- file_ -file :: Parser PathType-file = do- a <- fileRaw+ return (Local Home file)++ absolutePath = do+ file <- file_++ return (Local Absolute file)++local :: Parser ImportType+local = do+ a <- localRaw whitespace return a scheme :: Parser Builder scheme = "http" <> option "s" -httpRaw :: Parser Builder-httpRaw =- scheme- <> "://"- <> authority- <> pathAbempty- <> option ("?" <> query)- <> option ("#" <> fragment)+httpRaw :: Parser (Text, File, Text)+httpRaw = do+ prefix <- scheme <> "://" <> authority+ file <- file_+ suffix <- option ("?" <> query) <> option ("#" <> fragment) + let prefixText = Data.Text.Lazy.Builder.toLazyText prefix+ let suffixText = Data.Text.Lazy.Builder.toLazyText suffix++ return (prefixText, file, suffixText)+ authority :: Parser Builder authority = option (try (userinfo <> "@")) <> host <> option (":" <> port) @@ -942,12 +959,6 @@ where predicate c = unreserved c || subDelims c -pathAbempty :: Parser Builder-pathAbempty = star ("/" <> segment)--segment :: Parser Builder-segment = star pchar- pchar :: Parser Builder pchar = satisfy predicate <|> pctEncoded where@@ -973,16 +984,16 @@ subDelims :: Char -> Bool subDelims c = c `elem` ("!$&'()*+,;=" :: String) -http :: Parser PathType+http :: Parser ImportType http = do- a <- httpRaw+ (prefix, path, suffix) <- httpRaw whitespace- b <- optional (do+ headers <- optional (do _using- pathHashed_ )- return (URL (Data.Text.Lazy.Builder.toLazyText a) b)+ importHashed_ )+ return (URL prefix path suffix headers) -env :: Parser PathType+env :: Parser ImportType env = do _ <- Text.Parser.Char.text "env:" a <- (alternative0 <|> alternative1)@@ -1546,7 +1557,7 @@ snoc m (k, v) = Data.HashMap.Strict.InsOrd.insertWith combine k v m -- | Parser for a top-level Dhall expression-expr :: Parser (Expr Src Path)+expr :: Parser (Expr Src Import) expr = exprA import_ -- | Parser for a top-level Dhall expression. The expression is parameterized@@ -1554,16 +1565,16 @@ exprA :: Parser a -> Parser (Expr Src a) exprA = completeExpression -pathType_ :: Parser PathType-pathType_ = choice [ file, http, env ]+importType_ :: Parser ImportType+importType_ = choice [ local, http, env ] -pathHashed_ :: Parser PathHashed-pathHashed_ = do- pathType <- pathType_- hash <- optional pathHash_- return (PathHashed {..})+importHashed_ :: Parser ImportHashed+importHashed_ = do+ importType <- importType_+ hash <- optional importHash_+ return (ImportHashed {..}) where- pathHash_ = do+ importHash_ = do _ <- Text.Parser.Char.text "sha256:" builder <- count 64 (satisfy hexdig <?> "hex digit") whitespace@@ -1577,11 +1588,11 @@ Nothing -> fail "Invalid sha256 hash" Just h -> pure h -import_ :: Parser Path+import_ :: Parser Import import_ = (do- pathHashed <- pathHashed_- pathMode <- alternative <|> pure Code- return (Path {..}) ) <?> "import"+ importHashed <- importHashed_+ importMode <- alternative <|> pure Code+ return (Import {..}) ) <?> "import" where alternative = do _as@@ -1601,7 +1612,7 @@ instance Exception ParseError -- | Parse an expression from `Text` containing a Dhall program-exprFromText :: String -> Text -> Either ParseError (Expr Src Path)+exprFromText :: String -> Text -> Either ParseError (Expr Src Import) exprFromText delta text = fmap snd (exprAndHeaderFromText delta text) {-| Like `exprFromText` but also returns the leading comments and whitespace@@ -1619,7 +1630,7 @@ exprAndHeaderFromText :: String -> Text- -> Either ParseError (Text, Expr Src Path)+ -> Either ParseError (Text, Expr Src Import) exprAndHeaderFromText delta text = case result of Left errInfo -> Left (ParseError { unwrap = errInfo, input = text }) Right (txt, r) -> Right (Data.Text.Lazy.dropWhileEnd (/= '\n') txt, r)
src/Dhall/Pretty/Internal.hs view
@@ -736,10 +736,11 @@ builtin "True" prettyExprF (BoolLit False) = builtin "False"-prettyExprF (IntegerLit a) =- prettyNumber a+prettyExprF (IntegerLit a)+ | 0 <= a = literal "+" <> prettyNumber a+ | otherwise = prettyNumber a prettyExprF (NaturalLit a) =- literal "+" <> prettyNatural a+ prettyNatural a prettyExprF (DoubleLit a) = prettyScientific a prettyExprF (TextLit a) =@@ -1094,10 +1095,11 @@ "True" buildExprF (BoolLit False) = "False"-buildExprF (IntegerLit a) =- buildNumber a+buildExprF (IntegerLit a)+ | 0 <= a = "+" <> buildNumber a+ | otherwise = buildNumber a buildExprF (NaturalLit a) =- "+" <> buildNatural a+ buildNatural a buildExprF (DoubleLit a) = buildScientific a buildExprF (TextLit a) =
src/Dhall/Tutorial.hs view
@@ -189,7 +189,7 @@ -- > -- > import Dhall -- > --- > data Example = Example { foo :: Integer, bar :: Vector Double }+-- > data Example = Example { foo :: Natural, bar :: Vector Double } -- > deriving (Generic, Show) -- > -- > instance Interpret Example@@ -275,7 +275,7 @@ -- > -- > import Dhall -- > --- > data Person = Person { age :: Integer, name :: Text }+-- > data Person = Person { age :: Natural, name :: Text } -- > deriving (Generic, Show) -- > -- > instance Interpret Person@@ -304,16 +304,25 @@ -- Suppose that we try to decode a value of the wrong type, like this: -- -- > >>> input auto "1" :: IO Bool--- > *** Exception: +-- > *** Exception: -- > Error: Expression doesn't match annotation -- > +-- > - Bool+-- > + Natural+-- > -- > 1 : Bool -- > -- > (input):1:1 -- -- The interpreter complains because the string @\"1\"@ cannot be decoded into a--- Haskell value of type `Bool`.+-- Haskell value of type `Bool`. This part of the type error: --+-- > - Bool+-- > + Natural+--+-- ... means that the expected type was @Bool@ but the inferred type of the+-- expression @1@ was @Natural@.+-- -- The code excerpt from the above error message has two components: -- -- * the expression being type checked (i.e. @1@)@@ -406,7 +415,7 @@ -- -- ... then the interpreter will reject the import: ----- > >>> input auto "./file1" :: IO Integer+-- > >>> input auto "./file1" :: IO Natural -- > *** Exception: -- > ↳ ./file1 -- > ↳ ./file2@@ -438,7 +447,7 @@ -- You can also import Dhall expressions from environment variables, too: -- -- > >>> System.Environment.setEnv "FOO" "1"--- > >>> input auto "env:FOO" :: IO Integer+-- > >>> input auto "env:FOO" :: IO Natural -- > 1 -- -- You can import types, too. For example, we can change our @./bar@ file to:@@ -474,12 +483,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: ----- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not> -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: ----- > >>> input auto "https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > >>> input auto "https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess@@ -494,31 +503,35 @@ -- required for empty lists but optional for non-empty lists. You will get a -- type error if you provide an empty list without a type annotation: ----- > >>> input auto "[]" :: IO (Vector Integer)--- > *** Exception: --- > Error: Empty lists need a type annotation--- > --- > []+-- > >>> input auto "[]" :: IO (Vector Natural)+-- > *** Exception:+-- > Error: Invalid input -- > --- > (input):1:1--- > >>> input auto "[] : List Integer" :: IO (Vector Integer)--- > []+-- > (input):1:3:+-- > |+-- > 1 | []+-- > | ^+-- > unexpected end of input+-- > expecting ':' or whitespace -- -- Also, list elements must all have the same type. You will get an error if -- you try to store elements of different types in a list: ----- > >>> input auto "[1, True, 3]" :: IO (Vector Integer)--- > *** Exception: --- > Error: List elements should have the same type+-- > >>> input auto "[1, True, 3]" :: IO (Vector Natural)+-- > *** Exception:+-- > Error: List elements should all have the same type -- > --- > [1, True, 3]+-- > - Natural+-- > + Bool -- > --- > (input):1:1+-- > True+-- > +-- > (input):1:5 -- -- __Exercise:__ What is the shortest @./config@ file that you can decode using -- this command: ----- > >>> input auto "./config" :: IO (Vector (Vector Integer))+-- > >>> input auto "./config" :: IO (Vector (Vector Natural)) -- $optional0 --@@ -527,19 +540,19 @@ -- -- For example, these are valid @Optional@ values: ----- > [1] : Optional Integer+-- > [1] : Optional Natural -- >--- > [] : Optional Integer+-- > [] : Optional Natural -- -- ... but this is /not/ valid: ----- > [1, 2] : Optional Integer -- NOT valid+-- > [1, 2] : Optional Natural -- NOT valid -- -- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes: ----- > >>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)+-- > >>> input auto "[1] : Optional Natural" :: IO (Maybe Natural) -- > Just 1--- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer)+-- > >>> input auto "[] : Optional Natural" :: IO (Maybe Natural) -- > Nothing -- -- You cannot omit the type annotation for @Optional@ values. The type@@ -548,7 +561,7 @@ -- __Exercise:__ What is the shortest possible @./config@ file that you can decode -- like this: ----- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))+-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Natural))) -- > ??? -- -- __Exercise:__ Try to decode an @Optional@ value with more than one element and@@ -569,7 +582,7 @@ -- record literal has the following record type: -- -- > { foo : Bool--- > , bar : Integer+-- > , bar : Natural -- > , baz : Double -- > } --@@ -612,7 +625,7 @@ -- > $ dhall -- > { x = 1, y = True, z = "ABC" }.{ x, y } -- > <Ctrl-D>--- > { x : Integer, y : Bool }+-- > { x : Natural, y : Bool } -- > -- > { x = 1, y = True } --@@ -714,7 +727,7 @@ -- > <Ctrl-D> -- > ∀(n : Bool) → List Bool -- > --- > λ(n : Bool) → [n && True, n && False, n || True, n || False]+-- > λ(n : Bool) → [ n, False, True, n ] -- -- The first line says that @makeBools@ is a function of one argument named @n@ -- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@@@ -737,10 +750,15 @@ -- -- The second line of Dhall's output is our program's normal form: ----- > λ(n : Bool) → [n && True, n && False, n || True, n || False]+-- > λ(n : Bool) → [ n, False, True, n ] ----- ... which in this case happens to be identical to our original program.+-- ... and the interpreter was able to simplify our expression by noting that: --+-- * @n && True = n@+-- * @n && False = False@+-- * @n || True = True@+-- * @n || False = n@+-- -- To apply a function to an argument you separate the function and argument by -- whitespace (just like Haskell): --@@ -847,7 +865,7 @@ -- > $ dhall -- > let name = "John Doe" -- > in let age = 21--- > in "My name is ${name} and my age is ${Integer/show age}"+-- > in "My name is ${name} and my age is ${Natural/show age}" -- > <Ctrl-D> -- > Text -- >@@ -875,13 +893,13 @@ -- > $ dhall -- > { foo = 1, bar = "ABC" } // { baz = True } -- > <Ctrl-D>--- > { bar : Text, baz : Bool, foo : Integer }+-- > { bar : Text, baz : Bool, foo : Natural } -- > -- > { bar = "ABC", baz = True, foo = 1 } -- > $ dhall -- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode -- > <Ctrl-D>--- > { bar : Bool, foo : Integer }+-- > { bar : Bool, foo : Natural } -- > -- > { bar = True, foo = 1 } --@@ -926,9 +944,9 @@ -- operator descends recursively into record types: -- -- > $ dhall--- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }+-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural } -- > <Ctrl-D>--- > { foo : { bar : Text, baz : Bool }, qux : Integer }+-- > { foo : { bar : Text, baz : Bool }, qux : Natural } -- $let --@@ -983,10 +1001,14 @@ -- > $ dhall -- > let twice (x : Text) = x ++ x in twice "ha" -- > <Ctrl-D>--- > (stdin):1:11: error: expected: ":",--- > "="--- > let twice (x : Text) = x ++ x in twice "ha" --- > ^+-- > Error: Invalid input+-- > +-- > (stdin):1:11:+-- > |+-- > 1 | let twice (x : Text) = x ++ x in twice "ha"+-- > | ^+-- > unexpected '('+-- > expecting ':', '=', or the rest of label -- -- The error message says that Dhall expected either a @(:)@ (i.e. the beginning -- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a@@ -995,7 +1017,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall--- > let not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not+-- > let not = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > in not True -- > <Ctrl-D> -- > Bool@@ -1048,7 +1070,7 @@ -- remaining alternatives. For example, both of the following union literals -- have the same type, which is the above union type: ----- > < Left = +0 | Right : Bool >+-- > < Left = 0 | Right : Bool > -- -- > < Right = True | Left : Natural > --@@ -1070,7 +1092,7 @@ -- Now our @./process@ function can handle both alternatives: -- -- > $ dhall--- > ./process < Left = +3 | Right : Bool >+-- > ./process < Left = 3 | Right : Bool > -- > <Ctrl-D> -- > Bool -- > @@ -1100,8 +1122,8 @@ -- -- So, for example: ----- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool--- > = Natural/even +3 : Bool+-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = 3 | Right : Bool > : Bool+-- > = Natural/even 3 : Bool -- > = False -- -- ... and similarly:@@ -1135,8 +1157,8 @@ -- > in let Person = -- > λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > -- > in [ Empty--- > , Person { name = "John", age = +23 }--- > , Person { name = "Amy" , age = +25 }+-- > , Person { name = "John", age = 23 }+-- > , Person { name = "Amy" , age = 25 } -- > , Empty -- > ] --@@ -1145,8 +1167,8 @@ -- -- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > -- > in [ MyType.Empty {=}--- > , MyType.Person { name = "John", age = +23 }--- > , MyType.Person { name = "Amy" , age = +25 }+-- > , MyType.Person { name = "John", age = 23 }+-- > , MyType.Person { name = "Amy" , age = 25 } -- > ] -- -- The @constructors@ keyword takes a union type argument and returns a record@@ -1186,7 +1208,7 @@ -- __Exercise__: Create a list of the following type with at least one element -- per alternative: ----- > List < Left : Integer | Right : Double >+-- > List < Left : Natural | Right : Double > -- $polymorphic --@@ -1236,15 +1258,15 @@ -- argument). The result also has type @a@.\" -- -- This means that the type of the second argument changes depending on what--- type we provide for the first argument. When we apply @./id@ to @Integer@, we--- create a function that expects an @Integer@ argument:+-- type we provide for the first argument. When we apply @./id@ to @Natural@,+-- we create a function that expects an @Natural@ argument: -- -- > $ dhall--- > ./id Integer+-- > ./id Natural -- > <Ctrl-D>--- > ∀(x : Integer) → Integer+-- > ∀(x : Natural) → Natural -- > --- > λ(x : Integer) → x+-- > λ(x : Natural) → x -- -- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a -- @Bool@ argument:@@ -1260,9 +1282,9 @@ -- that they both work on their respective types: -- -- > $ dhall--- > ./id Integer 4+-- > ./id Natural 4 -- > <Ctrl-D>--- > Integer+-- > Natural -- > -- > 4 --@@ -1317,11 +1339,11 @@ -- > $ dhall -- > λ(_ : Text) → 1 -- > <Ctrl-D>--- > Text → Integer+-- > Text → Natural -- > -- > λ(_ : Text) → 1 ----- The type @(Text → Integer)@ is the same as @(∀(_ : Text) → Integer)@+-- The type @(Text → Natural)@ is the same as @(∀(_ : Text) → Natural)@ -- -- __Exercise__ : Translate Haskell's `flip` function to Dhall @@ -1339,11 +1361,11 @@ -- applied. For example, the following program is an anonymous function: -- -- > $ dhall--- > \(n : Bool) -> +10 * +10+-- > \(n : Bool) -> 10 * 10 -- > <Ctrl-D> -- > ∀(n : Bool) → Natural -- > --- > λ(n : Bool) → +100+-- > λ(n : Bool) → 100 -- -- ... and even though the function is still missing the first argument named -- @n@ the compiler is smart enough to evaluate the body of the anonymous@@ -1353,12 +1375,12 @@ -- complex example: -- -- > $ dhall--- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map--- > in λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3]+-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map+-- > in λ(f : Natural → Natural) → Prelude/List/map Natural Natural f [1, 2, 3] -- > <Ctrl-D>--- > ∀(f : Integer → Integer) → List Integer+-- > ∀(f : Natural → Natural) → List Natural -- > --- > λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer+-- > λ(f : Natural → Natural) → [f 1, f 2, f 3] : List Natural -- -- Dhall can apply our function to each element of the list even before we specify -- which function to apply.@@ -1368,21 +1390,21 @@ -- an @Optional@ value: -- -- > $ dhall--- > List/head Integer ([] : List Integer)+-- > List/head Natural ([] : List Natural) -- > <Ctrl-D>--- > Optional Integer+-- > Optional Natural -- > --- > [] : Optional Integer+-- > [] : Optional Natural -- -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: ----- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate>+-- <https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate> -- -- Test what the following Dhall expression normalizes to: ----- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate--- > in replicate +10+-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate+-- > in replicate 10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by -- finding an input expression that crashes or loops forever (and file a bug@@ -1461,7 +1483,7 @@ -- imported Dhall value and reject the import if there is a hash mismatch: -- -- > $ dhall <<< './foo'--- > Integer+-- > Natural -- > -- > 1 --@@ -1477,7 +1499,7 @@ -- changes to whitespace or comments: -- -- > $ dhall <<< './foo' # This still succeeds--- > Integer+-- > Natural -- > -- > 1 --@@ -1592,7 +1614,7 @@ -- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a -- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value } -- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count = --- > +0, diff = λ(_ : Natural) → nil }).diff +0)+-- > 0, diff = λ(_ : Natural) → nil }).diff 0) -- -- ... and run the expression through the @dhall-format@ executable: --@@ -1624,25 +1646,25 @@ -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > )--- > { count = +0, diff = λ(_ : Natural) → nil }+-- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff--- > +0+-- > 0 -- > ) -- -- The executable formats expressions without resolving, type-checking, or -- normalizing them: -- -- > $ dhall-format--- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))+-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate +-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D> -- > let replicate =--- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate +-- > https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate -- > -- > in replicate--- > +5--- > (List (List Integer))--- > (replicate +5 (List Integer) (replicate +5 Integer 1))+-- > 5+-- > (List (List Natural))+-- > (replicate 5 (List Natural) (replicate 5 Natural 1)) -- -- You can also use the formatter to modify files in place using the -- @--inplace@ flag (i.e. for formatting source code):@@ -1676,9 +1698,9 @@ -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > )--- > { count = +0, diff = λ(_ : Natural) → nil }+-- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff--- > +0+-- > 0 -- > ) -- -- Carefully note that the code formatter does not preserve all comments.@@ -1700,48 +1722,48 @@ -- multi-line expressions, too: -- -- > $ dhall--- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))+-- > let replicate = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/replicate +-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D>--- > List (List (List Integer))+-- > List (List (List Natural)) -- > --- > [ [ [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer+-- > [ [ [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ]--- > : List (List Integer)--- > , [ [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer+-- > : List (List Natural)+-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ]--- > : List (List Integer)--- > , [ [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer+-- > : List (List Natural)+-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ]--- > : List (List Integer)--- > , [ [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer+-- > : List (List Natural)+-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ]--- > : List (List Integer)--- > , [ [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer--- > , [ 1, 1, 1, 1, 1 ] : List Integer+-- > : List (List Natural)+-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural+-- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ]--- > : List (List Integer)+-- > : List (List Natural) -- > ]--- > : List (List (List Integer))+-- > : List (List (List Natural)) -- $builtins --@@ -1782,18 +1804,19 @@ -- -- First, Dhall only supports addition and multiplication on @Natural@ numbers -- (i.e. non-negative integers), which are not the same type of number as--- @Integer@s (which can be negative). A @Natural@ number is a number prefixed--- with the @+@ symbol. If you try to add or multiply two @Integer@s (without--- the @+@ prefix) you will get a type error:+-- @Integer@s (which can be negative). An @Integer@ number is a number prefixed+-- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading+-- sign. If you try to add or multiply two @Integer@s you will get a type+-- error: -- -- > $ dhall--- > 2 + 2+-- > +2 + +2 -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: ❰+❱ only works on ❰Natural❱s -- > --- > 2 + 2+-- > +2 + +2 -- > -- > (stdin):1:1 --@@ -1983,7 +2006,7 @@ -- > $ dhall -- > if True then 3 else 5 -- > <Ctrl-D>--- > Integer+-- > Natural -- > -- > 3 --@@ -2005,11 +2028,12 @@ -- $natural ----- @Natural@ literals are numbers prefixed by a @+@ sign, like this:+-- @Natural@ literals are non-negative numbers without any leading sign, like+-- this: ----- > +4 : Natural+-- > 4 : Natural ----- If you omit the @+@ sign then you get an @Integer@ literal, which is a+-- If you add a @+@ or @-@ sign then you get an @Integer@ literal, which is a -- different type of value -- $plus@@ -2017,11 +2041,11 @@ -- Example: -- -- > $ dhall--- > +2 + +3+-- > 2 + 3 -- > <Ctrl-D> -- > Natural -- > --- > +5+-- > 5 -- -- Type: --@@ -2033,20 +2057,20 @@ -- -- > (x + y) + z = x + (y + z) -- >--- > x + +0 = x+-- > x + 0 = x -- >--- > +0 + x = x+-- > 0 + x = x -- $times -- -- Example: -- -- > $ dhall--- > +2 * +3+-- > 2 * 3 -- > <Ctrl-D> -- > Natural -- > --- > +6+-- > 6 -- -- Type: --@@ -2058,24 +2082,24 @@ -- -- > (x * y) * z = x * (y * z) -- >--- > x * +1 = x+-- > x * 1 = x -- >--- > +1 * x = x+-- > 1 * x = x -- > -- > (x + y) * z = (x * z) + (y * z) -- > -- > x * (y + z) = (x * y) + (x * z) -- >--- > x * +0 = +0+-- > x * 0 = 0 -- >--- > +0 * x = +0+-- > 0 * x = 0 -- $even -- -- Example: -- -- > $ dhall--- > Natural/even +6+-- > Natural/even 6 -- > <Ctrl-D> -- > Bool -- > @@ -2090,18 +2114,18 @@ -- -- > Natural/even (x + y) = Natural/even x == Natural/even y -- >--- > Natural/even +0 = True+-- > Natural/even 0 = True -- > -- > Natural/even (x * y) = Natural/even x || Natural/even y -- >--- > Natural/even +1 = False+-- > Natural/even 1 = False -- $odd -- -- Example: -- -- > $ dhall--- > Natural/odd +6+-- > Natural/odd 6 -- > <Ctrl-D> -- > Bool -- > @@ -2116,18 +2140,18 @@ -- -- > Natural/odd (x + y) = Natural/odd x != Natural/odd y -- >--- > Natural/odd +0 = False+-- > Natural/odd 0 = False -- > -- > Natural/odd (x * y) = Natural/odd x && Natural/odd y -- >--- > Natural/odd +1 = True+-- > Natural/odd 1 = True -- $isZero -- -- Example: -- -- > $ dhall--- > Natural/isZero +6+-- > Natural/isZero 6 -- > <Ctrl-D> -- > Bool -- > @@ -2142,18 +2166,18 @@ -- -- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y -- >--- > Natural/isZero +0 = True+-- > Natural/isZero 0 = True -- > -- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y -- >--- > Natural/isZero +1 = False+-- > Natural/isZero 1 = False -- $naturalFold -- -- Example: -- -- > $ dhall--- > Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome"+-- > Natural/fold 40 Text (λ(t : Text) → t ++ "!") "You're welcome" -- > <Ctrl-D> -- > Text -- > @@ -2168,11 +2192,11 @@ -- -- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z) -- > --- > Natural/fold +0 n s z = z+-- > Natural/fold 0 n s z = z -- > -- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s) -- > --- > Natural/fold +1 n s = s+-- > Natural/fold 1 n s = s -- $naturalBuild --@@ -2183,7 +2207,7 @@ -- > <Ctrl-D> -- > Natural -- > --- > +2+-- > 2 -- -- Type: --@@ -2198,14 +2222,13 @@ -- $integer ----- @Integer@ literals are either prefixed with a @-@ sign (if they are negative)--- or no sign (if they are positive), like this:+-- @Integer@ literals are prefixed with a @+@ (if they are non-negative) or a+-- @-@ sign (if they are negative), like this: ----- > 3 : Integer+-- > +3 : Integer -- > -2 : Integer ----- If you prefix them with a @+@ sign then they are @Natural@ literals and not--- @Integer@s+-- If you omit the sign then they are @Natural@ literals and not @Integer@s -- -- There are no built-in operations on @Integer@s. For all practical purposes -- they are opaque values within the Dhall language@@ -2266,7 +2289,7 @@ -- -- Also, every empty @List@ must end with a mandatory type annotation, for example: ----- > [] : List Integer+-- > [] : List Natural -- -- The built-in operations on @List@s are: @@ -2277,7 +2300,7 @@ -- > $ dhall -- > [1, 2, 3] # [4, 5, 6] -- > <Ctrl-D>--- > List Integer+-- > List Natural -- > -- > [1, 2, 3, 4, 5, 6] --@@ -2313,7 +2336,7 @@ -- -- Rules: ----- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat -- > -- > List/fold a (Prelude/List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)@@ -2327,11 +2350,11 @@ -- Example: -- -- > $ dhall--- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))+-- > List/build Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil))) -- > <Ctrl-D>--- > List Integer+-- > List Natural -- > --- > [1, 2, 3] : List Integer+-- > [1, 2, 3] : List Natural -- -- Type: --@@ -2349,11 +2372,11 @@ -- Example: -- -- > $ dhall--- > List/length Integer [1, 2, 3]+-- > List/length Natural [1, 2, 3] -- > <Ctrl-D> -- > Natural -- > --- > +3+-- > 3 -- -- Type: --@@ -2362,18 +2385,18 @@ -- -- Rules: ----- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0+-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + 1) 0 -- $listHead -- -- Example: -- -- > $ dhall--- > List/head Integer [1, 2, 3]+-- > List/head Natural [1, 2, 3] -- > <Ctrl-D>--- > Optional Integer+-- > Optional Natural -- > --- > [1] : Optional Integer+-- > [1] : Optional Natural -- -- Type: --@@ -2382,10 +2405,10 @@ -- -- Rules: ----- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/head--- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap--- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map+-- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Optional/head+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap+-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/head a (Prelude/List/concat a xss) = -- > Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss)@@ -2400,11 +2423,11 @@ -- Example: -- -- > $ dhall--- > List/last Integer [1, 2, 3]+-- > List/last Natural [1, 2, 3] -- > <Ctrl-D>--- > Optional Integer+-- > Optional Natural -- > --- > [1] : Optional Integer+-- > [1] : Optional Natural -- -- Type: --@@ -2413,10 +2436,10 @@ -- -- Rules: ----- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/last--- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap--- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map+-- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Optional/last+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap+-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/last a (Prelude/List/concat a xss) = -- > Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss)@@ -2435,7 +2458,7 @@ -- > <Ctrl-D> -- > List { index : Natural, value : Text } -- > --- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text }+-- > [{ index = 0, value = "ABC" }, { index = 1, value = "DEF" }, { index = 2, value = "GHI" }] : List { index : Natural, value : Text } -- -- Type: --@@ -2444,9 +2467,9 @@ -- -- Rules: ----- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/shifted--- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat--- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map+-- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/shifted+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat+-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map -- > -- > List/indexed a (Prelude/List/concat a xss) = -- > Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)@@ -2456,11 +2479,11 @@ -- Example: -- -- > $ dhall--- > List/reverse Integer [1, 2, 3]+-- > List/reverse Natural [1, 2, 3] -- > <Ctrl-D>--- > List Integer+-- > List Natural -- > --- > [3, 2, 1] : List Integer+-- > [3, 2, 1] : List Natural -- -- Type: --@@ -2469,9 +2492,9 @@ -- -- Rules: ----- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map--- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap+-- > let Prelude/List/map = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/map+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/List/concatMap -- > -- > List/reverse a (Prelude/List/concat a xss) -- > = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss))@@ -2529,7 +2552,7 @@ -- -- ... which currenty redirects to: ----- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude>+-- <https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude> -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a@@ -2540,12 +2563,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: ----- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not> -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents ----- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not+-- > $ curl https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2578,7 +2601,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall--- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not True+-- > https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not True -- > <Ctrl-D> -- > Bool -- > @@ -2587,7 +2610,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall--- > let Bool/not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not+-- > let Bool/not = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Bool/not -- > in Bool/not True -- > <Ctrl-D> -- > Bool@@ -2598,16 +2621,16 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: ----- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Natural/even+-- > $ curl https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > -- > Examples: -- > -- > ```--- > ./even +3 = False+-- > ./even 3 = False -- > --- > ./even +0 = True+-- > ./even 0 = True -- > ``` -- > -} -- > let even : Natural → Bool@@ -2619,7 +2642,7 @@ -- using local relative paths instead of URLs. For example, you can use @wget@, -- like this: ----- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/+-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool@@ -2683,12 +2706,12 @@ -- locally like this: -- -- > $ ipfs mount--- > $ cd /ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude+-- > $ cd /ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: ----- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude>+-- <https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial@@ -2697,14 +2720,14 @@ -- convenience: -- -- > $ dhall--- > let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall+-- > let Prelude = https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/package.dhall -- > -- > in λ(x : Text)--- > → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x)+-- > → Prelude.`List`.length Text (Prelude.`List`.replicate 10 Text x) -- > <Ctrl-D> -- > ∀(x : Text) → Natural -- >--- > λ(x : Text) → +10+-- > λ(x : Text) → 10 -- -- The organization of the package mirrors the layout of the Prelude, meaning -- that every directory is stored as a record whose children are the fields of@@ -2712,7 +2735,7 @@ -- -- __Exercise__: Browse the Prelude by running: ----- > $ dhall <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'+-- > $ dhall <<< 'https://ipfs.io/ipfs/QmV5MMfZehF4Z1EC4hK1s4yjE81kZV5hxypcuqfh9qcDMB/Prelude/package.dhall' -- $conclusion --
src/Dhall/TypeCheck.hs view
@@ -629,13 +629,14 @@ Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of- Pi _ tY' t' -> do+ Pi y tY' t' -> do if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))- if Dhall.Core.judgmentallyEqual t t'+ let t'' = Dhall.Core.shift (-1) (V y 0) t'+ if Dhall.Core.judgmentallyEqual t t'' then return ()- else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'))+ else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t@@ -661,20 +662,21 @@ (kX, t) <- case Data.HashMap.Strict.InsOrd.toList ktsX of [] -> Left (TypeError ctx e MissingMergeType)- (kX, Pi _ _ t):_ -> return (kX, t)+ (kX, Pi y _ t):_ -> return (kX, Dhall.Core.shift (-1) (V y 0) t) (kX, tX ):_ -> Left (TypeError ctx e (HandlerNotAFunction kX tX)) let process (kY, tY) = do case Data.HashMap.Strict.InsOrd.lookup kY ktsX of Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of- Pi _ tY' t' -> do+ Pi y tY' t' -> do if Dhall.Core.judgmentallyEqual tY tY' then return () else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))- if Dhall.Core.judgmentallyEqual t t'+ let t'' = Dhall.Core.shift (-1) (V y 0) t'+ if Dhall.Core.judgmentallyEqual t t'' then return ()- else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'))+ else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t@@ -915,9 +917,9 @@ \● You tried to define a recursive value, like this: \n\ \ \n\ \ \n\- \ ┌─────────────────────┐ \n\- \ │ let x = x + +1 in x │ \n\- \ └─────────────────────┘ \n\+ \ ┌────────────────────┐ \n\+ \ │ let x = x + 1 in x │ \n\+ \ └────────────────────┘ \n\ \ ⇧ \n\ \ Recursive definitions are not allowed \n\ \ \n\@@ -961,7 +963,7 @@ \ \n\ \ \n\ \ ┌────────────────┐ \n\- \ │ Bool → Integer │ This is the type of a function that accepts an anonymous\n\+ \ │ Bool → Natural │ This is the type of a function that accepts an anonymous\n\ \ └────────────────┘ input term that has type ❰Bool❱ \n\ \ ⇧ \n\ \ This is the type of the input term \n\@@ -1028,8 +1030,8 @@ \ \n\ \ \n\ \ ┌────────────────┐ \n\- \ │ Bool → Integer │ This is the type of a function that returns an output \n\- \ └────────────────┘ term that has type ❰Int❱ \n\+ \ │ Bool → Natural │ This is the type of a function that returns an output \n\+ \ └────────────────┘ term that has type ❰Natural❱ \n\ \ ⇧ \n\ \ This is the type of the output term \n\ \ \n\@@ -1167,13 +1169,13 @@ \ \n\ \ \n\ \ ┌─────────────┐ \n\- \ │ 1 : Integer │ ❰1❱ is not a function because ❰Integer❱ is not the type of \n\+ \ │ 1 : Natural │ ❰1❱ is not a function because ❰Natural❱ is not the type of \n\ \ └─────────────┘ a function \n\ \ \n\ \ \n\- \ ┌────────────────────────┐ \n\- \ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ is not a function because \n\- \ └────────────────────────┘ ❰Bool❱ is not the type of a function \n\+ \ ┌───────────────────────┐ \n\+ \ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ is not a function because \n\+ \ └───────────────────────┘ ❰Bool❱ is not the type of a function \n\ \ \n\ \ \n\ \ ┌──────────────────┐ \n\@@ -1183,7 +1185,7 @@ \ \n\ \Some common reasons why you might get this error: \n\ \ \n\- \● You tried to add two ❰Integer❱s without a space around the ❰+❱, like this: \n\+ \● You tried to add two ❰Natural❱s without a space around the ❰+❱, like this: \n\ \ \n\ \ \n\ \ ┌─────┐ \n\@@ -1202,21 +1204,17 @@ \ \n\ \ \n\ \ This is because the ❰+❱ symbol has two meanings: you use ❰+❱ to add two \n\- \ numbers, but you also can prefix ❰Integer❱ literals with a ❰+❱ to turn them \n\- \ into ❰Natural❱ literals (like ❰+2❱) \n\+ \ numbers, but you also can prefix ❰Natural❱ literals with a ❰+❱ to turn them \n\+ \ into ❰Integer❱ literals (like ❰+2❱) \n\ \ \n\- \ To fix the code, you need to put spaces around the ❰+❱ and also prefix each \n\- \ ❰2❱ with a ❰+❱, like this: \n\+ \ To fix the code, you need to put spaces around the ❰+❱, like this: \n\ \ \n\ \ \n\- \ ┌─────────┐ \n\- \ │ +2 + +2 │ \n\- \ └─────────┘ \n\+ \ ┌───────┐ \n\+ \ │ 2 + 2 │ \n\+ \ └───────┘ \n\ \ \n\ \ \n\- \ You can only add ❰Natural❱ numbers, which is why you must also change each \n\- \ ❰2❱ to ❰+2❱ \n\- \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ \ \n\ \You tried to use the following expression as a function: \n\@@ -1280,9 +1278,9 @@ \ └────────────────────────┘ of argument that the anonymous function accepts \n\ \ \n\ \ \n\- \ ┌─────────────────┐ \n\- \ │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of \n\- \ └─────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\+ \ ┌────────────────┐ \n\+ \ │ Natural/even 2 │ ❰2❱ has type ❰Natural❱, which matches the type of \n\+ \ └────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\@@ -1316,7 +1314,7 @@ \ \n\ \ \n\ \ ┌────────┐ \n\- \ │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an \n\+ \ │ List 1 │ ❰1❱ has type ❰Natural❱, but the ❰List❱ function expects an \n\ \ └────────┘ argument that has kind ❰Type❱ \n\ \ \n\ \ \n\@@ -1330,17 +1328,17 @@ \ └───────────────────────┘ \n\ \ ⇧ \n\ \ ❰List/head❱ is missing the first argument, \n\- \ which should be: ❰Integer❱ \n\+ \ which should be: ❰Natural❱ \n\ \ \n\ \ \n\ \● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ \n\ \ \n\ \ \n\- \ ┌────────────────┐ \n\- \ │ Natural/even 2 │ \n\- \ └────────────────┘ \n\+ \ ┌─────────────────┐ \n\+ \ │ Natural/even +2 │ \n\+ \ └─────────────────┘ \n\ \ ⇧ \n\- \ This should be ❰+2❱ \n\+ \ This should be ❰2❱ \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\@@ -1388,13 +1386,13 @@ \ \n\ \ \n\ \ ┌─────────────┐ \n\- \ │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type \n\+ \ │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type \n\ \ └─────────────┘ checker accepts the annotation \n\ \ \n\ \ \n\- \ ┌────────────────────────┐ \n\- \ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type \n\- \ └────────────────────────┘ checker accepts the annotation \n\+ \ ┌───────────────────────┐ \n\+ \ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type \n\+ \ └───────────────────────┘ checker accepts the annotation \n\ \ \n\ \ \n\ \ ┌────────────────────┐ \n\@@ -1587,7 +1585,7 @@ \ \n\ \ \n\ \ ┌────────────────────┐ \n\- \ │ 1 : Integer : Type │ ❰1❱ is a term with a type (❰Integer❱) of kind ❰Type❱\n\+ \ │ 1 : Natural : Type │ ❰1❱ is a term with a type (❰Natural❱) of kind ❰Type❱\n\ \ └────────────────────┘ \n\ \ ⇧ \n\ \ term \n\@@ -1674,7 +1672,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────┐ \n\- \ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱ \n\+ \ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Natural❱ \n\ \ └──────────────────────────────────┘ \n\ \ \n\ \ \n\@@ -1688,7 +1686,7 @@ \However, the following expression is " <> _NOT <> " valid: \n\ \ \n\ \ \n\- \ This branch has type ❰Integer❱ \n\+ \ This branch has type ❰Natural❱ \n\ \ ⇩ \n\ \ ┌────────────────────────┐ \n\ \ │ if True then 0 │ \n\@@ -1734,14 +1732,15 @@ \ \n\ \ \n\ \ ┌──────────────────────────┐ \n\- \ │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s \n\+ \ │ [1, 2, 3] : List Natural │ A ❰List❱ of three ❰Natural❱ numbers \n\ \ └──────────────────────────┘ \n\ \ ⇧ \n\- \ The type of the ❰List❱'s elements, which are ❰Integer❱s \n\+ \ The type of the ❰List❱'s elements, which are ❰Natural❱ \n\+ \ numbers \n\ \ \n\ \ \n\ \ ┌───────────────────┐ \n\- \ │ [] : List Integer │ An empty ❰List❱ \n\+ \ │ [] : List Natural │ An empty ❰List❱ \n\ \ └───────────────────┘ \n\ \ ⇧ \n\ \ You must specify the type when the ❰List❱ is empty \n\@@ -1755,7 +1754,7 @@ \ │ ... : List 1 │ \n\ \ └──────────────┘ \n\ \ ⇧ \n\- \ This is an ❰Integer❱ and not a ❰Type❱ \n\+ \ This is a ❰Natural❱ number and not a ❰Type❱ \n\ \ \n\ \ \n\ \ ┌─────────────────┐ \n\@@ -1784,7 +1783,7 @@ \ \n\ \ \n\ \ ┌───────────┐ \n\- \ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Integer❱\n\+ \ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Natural❱\n\ \ └───────────┘ \n\ \ \n\ \ \n\@@ -1792,7 +1791,7 @@ \ \n\ \ \n\ \ ┌───────────────────┐ \n\- \ │ [] : List Integer │ This type annotation is mandatory \n\+ \ │ [] : List Natural │ This type annotation is mandatory \n\ \ └───────────────────┘ \n\ \ \n\ \ \n\@@ -1812,7 +1811,7 @@ \ \n\ \ \n\ \ ┌───────────┐ \n\- \ │ [1, 2, 3] │ Every element in this ❰List❱ is an ❰Integer❱ \n\+ \ │ [1, 2, 3] │ Every element in this ❰List❱ is a ❰Natural❱ number \n\ \ └───────────┘ \n\ \ \n\ \ \n\@@ -1851,7 +1850,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────┐ \n\- \ │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱ \n\+ \ │ [1, 2, 3] : List Natural │ Every element in this ❰List❱ is an ❰Natural❱ \n\ \ └──────────────────────────┘ \n\ \ \n\ \ \n\@@ -1859,7 +1858,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────┐ \n\- \ │ [1, \"ABC\", 3] : List Integer │ The second element is not an ❰Integer❱ \n\+ \ │ [1, \"ABC\", 3] : List Natural │ The second element is not an ❰Natural❱ \n\ \ └──────────────────────────────┘ \n\ \ \n\ \ \n\@@ -1885,14 +1884,15 @@ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\- \ │ [1] : Optional Integer │ An optional element that's present \n\+ \ │ [1] : Optional Natural │ An optional element that's present \n\ \ └────────────────────────┘ \n\ \ ⇧ \n\- \ The type of the ❰Optional❱ element, which is an ❰Integer❱ \n\+ \ The type of the ❰Optional❱ element, which is an ❰Natural❱ \n\+ \ number \n\ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\- \ │ [] : Optional Integer │ An optional element that's absent \n\+ \ │ [] : Optional Natural │ An optional element that's absent \n\ \ └────────────────────────┘ \n\ \ ⇧ \n\ \ You still specify the type even when the element is absent \n\@@ -1906,7 +1906,7 @@ \ │ ... : Optional 1 │ \n\ \ └──────────────────┘ \n\ \ ⇧ \n\- \ This is an ❰Integer❱ and not a ❰Type❱ \n\+ \ This is a ❰Natural❱ number and not a ❰Type❱ \n\ \ \n\ \ \n\ \ ┌─────────────────────┐ \n\@@ -1939,15 +1939,15 @@ \ \n\ \ \n\ \ ┌────────────────────────┐ \n\- \ │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type \n\- \ └────────────────────────┘ \n\+ \ │ [1] : Optional Natural │ ❰1❱ is a ❰Natural❱ number, which matches the \n\+ \ └────────────────────────┘ number \n\ \ \n\ \ \n\ \... but this is " <> _NOT <> " a valid ❰Optional❱ value: \n\ \ \n\ \ \n\ \ ┌────────────────────────────┐ \n\- \ │ [\"ABC\"] : Optional Integer │ ❰\"ABC\"❱ is not an ❰Integer❱ \n\+ \ │ [\"ABC\"] : Optional Natural │ ❰\"ABC\"❱ is not a ❰Natural❱ number \n\ \ └────────────────────────────┘ \n\ \ \n\ \ \n\@@ -1977,7 +1977,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────┐ \n\- \ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\+ \ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\ \ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\ \ \n\ \ \n\@@ -1990,10 +1990,11 @@ \ \n\ \ \n\ \ ┌────────────────────────────┐ \n\- \ │ { foo : Integer, bar : 1 } │ Invalid record type \n\+ \ │ { foo : Natural, bar : 1 } │ Invalid record type \n\ \ └────────────────────────────┘ \n\ \ ⇧ \n\- \ ❰1❱ is an ❰Integer❱ and not a ❰Type❱ or ❰Kind❱ \n\+ \ ❰1❱ is a ❰Natural❱ number and not a ❰Type❱ or \n\+ \ ❰Kind❱ \n\ \ \n\ \ \n\ \You provided a record type with a field named: \n\@@ -2019,7 +2020,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────┐ \n\- \ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\+ \ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\ \ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\ \ \n\ \ \n\@@ -2034,7 +2035,7 @@ \ This is a ❰Type❱ annotation \n\ \ ⇩ \n\ \ ┌───────────────────────────────┐ \n\- \ │ { foo : Integer, bar : Type } │ Invalid record type \n\+ \ │ { foo : Natural, bar : Type } │ Invalid record type \n\ \ └───────────────────────────────┘ \n\ \ ⇧ \n\ \ ... but this is a ❰Kind❱ annotation \n\@@ -2086,7 +2087,7 @@ \ \n\ \ \n\ \ ┌───────────────────────────────┐ \n\- \ │ { foo = Integer, bar = Text } │ Every field is a type \n\+ \ │ { foo = Natural, bar = Text } │ Every field is a type \n\ \ └───────────────────────────────┘ \n\ \ \n\ \ \n\@@ -2311,7 +2312,7 @@ \For example, the following expression is " <> _NOT <> " valid: \n\ \ \n\ \ \n\- \ These elements have type ❰Integer❱ \n\+ \ These elements have type ❰Natural❱ \n\ \ ⇩ \n\ \ ┌───────────────────────────┐ \n\ \ │ [1, 2, 3] # [True, False] │ Invalid: the element types don't match \n\@@ -2594,7 +2595,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2649,7 +2650,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2689,7 +2690,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2702,11 +2703,11 @@ \ \n\ \ \n\ \ ┌───────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing\n\- \ │ in let handlers = │ \n\+ \ │ let union = < Left = 2 > │ The ❰Right❱ alternative is \n\+ \ │ in let handlers = │ missing \n\ \ │ { Left = Natural/even │ \n\- \ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used\n\- \ │ } │ \n\+ \ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't \n\+ \ │ } │ used \n\ \ │ in merge handlers union : Bool │ \n\ \ └───────────────────────────────────────┘ \n\ \ \n\@@ -2729,7 +2730,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2745,7 +2746,7 @@ \ ⇩ \n\ \ ┌─────────────────────────────────────────────────┐ \n\ \ │ let handlers = { Left = Natural/even } │ \n\- \ │ in let union = < Left = +2 | Right : Bool > │ \n\+ \ │ in let union = < Left = 2 | Right : Bool > │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────┘ \n\ \ \n\@@ -2770,7 +2771,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2802,7 +2803,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2830,7 +2831,7 @@ \ ⇩ \n\ \ ┌──────────────────────────────────────────────────────────────────────┐ \n\ \ │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │ \n\- \ │ in let union = < Left = +2 | Right : Bool > │ \n\+ \ │ in let union = < Left = 2 | Right : Bool > │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └──────────────────────────────────────────────────────────────────────┘ \n\ \ \n\@@ -2864,7 +2865,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2891,7 +2892,7 @@ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Text │ \n\ \ └──────────────────────────────────────────────────────────────────────┘ \n\@@ -2928,7 +2929,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -2948,7 +2949,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = │ \n\ \ │ { Left = λ(x : Natural) → x │ This outputs ❰Natural❱ \n\ \ │ , Right = λ(x : Bool ) → x │ This outputs ❰Bool❱ \n\@@ -2982,7 +2983,7 @@ \ \n\ \ \n\ \ ┌─────────────────────────────────────────────────────────────────────┐ \n\- \ │ let union = < Left = +2 | Right : Bool > │ \n\+ \ │ let union = < Left = 2 | Right : Bool > │ \n\ \ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\ \ │ in merge handlers union : Bool │ \n\ \ └─────────────────────────────────────────────────────────────────────┘ \n\@@ -3197,9 +3198,9 @@ \ └────────────────────────────┘ \n\ \ \n\ \ \n\- \ ┌───────────────────────────────────────────────────────────────────┐ \n\- \ │ λ(age : Natural) → \"Age: ${Integer/show (Natural/toInteger age)}\" │ \n\- \ └───────────────────────────────────────────────────────────────────┘ \n\+ \ ┌───────────────────────────────────────────────┐ \n\+ \ │ λ(age : Natural) → \"Age: ${Natural/show age}\" │ \n\+ \ └───────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ \Some common reasons why you might get this error: \n\@@ -3341,9 +3342,9 @@ \Similarly, this is " <> _NOT <> " legal code: \n\ \ \n\ \ \n\- \ ┌────────────────────────────────────────────────────┐ \n\- \ │ λ(Vector : Natural → Type → Type) → Vector +0 Text │ \n\- \ └────────────────────────────────────────────────────┘ \n\+ \ ┌───────────────────────────────────────────────────┐ \n\+ \ │ λ(Vector : Natural → Type → Type) → Vector 0 Text │ \n\+ \ └───────────────────────────────────────────────────┘ \n\ \ ⇧ \n\ \ Invalid dependent type \n\ \ \n\@@ -3401,9 +3402,9 @@ \For example, this is a valid use of ❰" <> txt2 <> "❱: \n\ \ \n\ \ \n\- \ ┌─────────┐ \n\- \ │ +3 " <> txt2 <> " +5 │ \n\- \ └─────────┘ \n\+ \ ┌───────┐ \n\+ \ │ 3 " <> txt2 <> " 5 │ \n\+ \ └───────┘ \n\ \ \n\ \ \n\ \Some common reasons why you might get this error: \n\@@ -3422,18 +3423,18 @@ \● You might have mistakenly used an ❰Integer❱ literal, which is " <> _NOT <> " allowed:\n\ \ \n\ \ \n\- \ ┌───────┐ \n\- \ │ 2 " <> txt2 <> " 2 │ Not valid \n\- \ └───────┘ \n\+ \ ┌─────────┐ \n\+ \ │ +2 " <> txt2 <> " +2 │ Not valid \n\+ \ └─────────┘ \n\ \ \n\ \ \n\- \ You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱ \n\- \ literals, like this: \n\+ \ You need to remove the leading ❰+❱ to transform them into ❰Natural❱ literals, \n\+ \ like this: \n\ \ \n\ \ \n\- \ ┌─────────┐ \n\- \ │ +2 " <> txt2 <> " +2 │ Valid \n\- \ └─────────┘ \n\+ \ ┌───────┐ \n\+ \ │ 2 " <> txt2 <> " 2 │ Valid \n\+ \ └───────┘ \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\
tests/Normalization.hs view
@@ -203,8 +203,8 @@ valCtx e = case e of (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> Just (NaturalLit (min x y)) _ -> Nothing- e <- codeWith tyCtx "min (min +11 +12) +8 + +1" - assertNormalizesToWith valCtx e "+9"+ e <- codeWith tyCtx "min (min 11 12) 8 + 1" + assertNormalizesToWith valCtx e "9" nestedReduction :: TestTree nestedReduction = testCase "doubleReduction" $ do@@ -219,8 +219,8 @@ (App (Var (V "fiveorless" 0)) (NaturalLit x)) -> Just (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2))) _ -> Nothing- e <- codeWith tyCtx "wurble +6"- assertNormalizesToWith valCtx e "+5"+ e <- codeWith tyCtx "wurble 6"+ assertNormalizesToWith valCtx e "5" should :: Text -> Text -> TestTree should name basename =
tests/Tutorial.hs view
@@ -44,7 +44,7 @@ e <- Util.code " let name = \"John Doe\" \n\ \in let age = 21 \n\- \in \"My name is ${name} and my age is ${Integer/show age}\"\n"+ \in \"My name is ${name} and my age is ${Natural/show age}\"\n" Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" ) _Interpolation_1 :: TestTree
tests/TypeCheck.hs view
@@ -40,6 +40,9 @@ , should "allow anonymous functions in types to be judgmentally equal" "anonymousFunctionsInTypes"+ , should+ "correctly handle α-equivalent merge alternatives"+ "mergeEquivalence" ] should :: Text -> Text -> TestTree
tests/normalization/examples/Bool/fold/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Bool/fold True Integer 0 1+../../../../../Prelude/Bool/fold True Natural 0 1
tests/normalization/examples/Bool/fold/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Bool/fold False Integer 0 1+../../../../../Prelude/Bool/fold False Natural 0 1
tests/normalization/examples/Integer/show/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Integer/show 0+../../../../../Prelude/Integer/show +0
tests/normalization/examples/Integer/show/1B.dhall view
@@ -1,1 +1,1 @@-"0"+"+0"
tests/normalization/examples/List/all/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/all Natural Natural/even [ +2, +3, +5 ]+../../../../../Prelude/List/all Natural Natural/even [ 2, 3, 5 ]
tests/normalization/examples/List/any/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/any Natural Natural/even [ +2, +3, +5 ]+../../../../../Prelude/List/any Natural Natural/even [ 2, 3, 5 ]
tests/normalization/examples/List/concat/0A.dhall view
@@ -1,4 +1,4 @@-../../../../../Prelude/List/concat Integer+../../../../../Prelude/List/concat Natural [ [ 0, 1, 2 ] , [ 3, 4 ] , [ 5, 6, 7, 8 ]
tests/normalization/examples/List/concat/1A.dhall view
@@ -1,5 +1,5 @@-../../../../../Prelude/List/concat Integer-[ [] : List Integer-, [] : List Integer-, [] : List Integer+../../../../../Prelude/List/concat Natural+[ [] : List Natural+, [] : List Natural+, [] : List Natural ]
tests/normalization/examples/List/concat/1B.dhall view
@@ -1,1 +1,1 @@-[] : List Integer+[] : List Natural
tests/normalization/examples/List/concatMap/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ +2, +3, +5 ]+../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ]
tests/normalization/examples/List/concatMap/0B.dhall view
@@ -1,1 +1,1 @@-[ +2, +2, +3, +3, +5, +5 ]+[ 2, 2, 3, 3, 5, 5 ]
tests/normalization/examples/List/filter/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/filter Natural Natural/even [ +2, +3, +5 ]+../../../../../Prelude/List/filter Natural Natural/even [ 2, 3, 5 ]
tests/normalization/examples/List/filter/0B.dhall view
@@ -1,1 +1,1 @@-[ +2 ]+[ 2 ]
tests/normalization/examples/List/filter/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/filter Natural Natural/odd [ +2, +3, +5 ]+../../../../../Prelude/List/filter Natural Natural/odd [ 2, 3, 5 ]
tests/normalization/examples/List/filter/1B.dhall view
@@ -1,1 +1,1 @@-[ +3, +5 ]+[ 3, 5 ]
tests/normalization/examples/List/fold/0A.dhall view
@@ -1,6 +1,6 @@ ../../../../../Prelude/List/fold Natural-[ +2, +3, +5 ]+[ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y)-+0+0
tests/normalization/examples/List/fold/0B.dhall view
@@ -1,1 +1,1 @@-+10+10
tests/normalization/examples/List/fold/1A.dhall view
@@ -1,7 +1,7 @@ λ(nil : Natural) → ../../../../../Prelude/List/fold Natural- [ +2, +3, +5 ]+ [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) nil
tests/normalization/examples/List/fold/1B.dhall view
@@ -1,1 +1,1 @@-λ(nil : Natural) → +2 + +3 + +5 + nil+λ(nil : Natural) → 2 + 3 + 5 + nil
tests/normalization/examples/List/fold/2A.dhall view
@@ -1,4 +1,4 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list)-→ ../../../../../Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil+→ ../../../../../Prelude/List/fold Natural [ 2, 3, 5 ] list cons nil
tests/normalization/examples/List/fold/2B.dhall view
@@ -1,4 +1,4 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list)-→ cons +2 (cons +3 (cons +5 nil))+→ cons 2 (cons 3 (cons 5 nil))
tests/normalization/examples/List/generate/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/generate +5 Bool Natural/even+../../../../../Prelude/List/generate 5 Bool Natural/even
tests/normalization/examples/List/generate/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/generate +0 Bool Natural/even+../../../../../Prelude/List/generate 0 Bool Natural/even
tests/normalization/examples/List/head/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/head Integer [ 0, 1, 2 ]+../../../../../Prelude/List/head Natural [ 0, 1, 2 ]
tests/normalization/examples/List/head/0B.dhall view
@@ -1,1 +1,1 @@-[ 0 ] : Optional Integer+[ 0 ] : Optional Natural
tests/normalization/examples/List/head/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/head Integer ([] : List Integer)+../../../../../Prelude/List/head Natural ([] : List Natural)
tests/normalization/examples/List/head/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/List/iterate/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1+../../../../../Prelude/List/iterate 10 Natural (λ(x : Natural) → x * 2) 1
tests/normalization/examples/List/iterate/0B.dhall view
@@ -1,1 +1,1 @@-[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]+[ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
tests/normalization/examples/List/iterate/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1+../../../../../Prelude/List/iterate 0 Natural (λ(x : Natural) → x * 2) 1
tests/normalization/examples/List/last/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/last Integer [ 0, 1, 2 ]+../../../../../Prelude/List/last Natural [ 0, 1, 2 ]
tests/normalization/examples/List/last/0B.dhall view
@@ -1,1 +1,1 @@-[ 2 ] : Optional Integer+[ 2 ] : Optional Natural
tests/normalization/examples/List/last/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/last Integer ([] : List Integer)+../../../../../Prelude/List/last Natural ([] : List Natural)
tests/normalization/examples/List/last/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/List/length/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/length Integer [ 0, 1, 2 ]+../../../../../Prelude/List/length Natural [ 0, 1, 2 ]
tests/normalization/examples/List/length/0B.dhall view
@@ -1,1 +1,1 @@-+3+3
tests/normalization/examples/List/length/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/length Integer ([] : List Integer)+../../../../../Prelude/List/length Natural ([] : List Natural)
tests/normalization/examples/List/length/1B.dhall view
@@ -1,1 +1,1 @@-+0+0
tests/normalization/examples/List/map/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ]+../../../../../Prelude/List/map Natural Bool Natural/even [ 2, 3, 5 ]
tests/normalization/examples/List/null/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/null Integer [ 0, 1, 2 ]+../../../../../Prelude/List/null Natural [ 0, 1, 2 ]
tests/normalization/examples/List/null/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/null Integer ([] : List Integer)+../../../../../Prelude/List/null Natural ([] : List Natural)
tests/normalization/examples/List/replicate/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/replicate +9 Integer 1+../../../../../Prelude/List/replicate 9 Natural 1
tests/normalization/examples/List/replicate/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/replicate +0 Integer 1+../../../../../Prelude/List/replicate 0 Natural 1
tests/normalization/examples/List/replicate/1B.dhall view
@@ -1,1 +1,1 @@-[] : List Integer+[] : List Natural
tests/normalization/examples/List/reverse/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/reverse Integer [ 0, 1, 2 ]+../../../../../Prelude/List/reverse Natural [ 0, 1, 2 ]
tests/normalization/examples/List/reverse/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/List/reverse Integer ([] : List Integer)+../../../../../Prelude/List/reverse Natural ([] : List Natural)
tests/normalization/examples/List/reverse/1B.dhall view
@@ -1,1 +1,1 @@-[] : List Integer+[] : List Natural
tests/normalization/examples/List/shifted/0A.dhall view
@@ -1,15 +1,15 @@ ../../../../../Prelude/List/shifted Bool-[ [ { index = +0, value = True }- , { index = +1, value = True }- , { index = +2, value = False }+[ [ { index = 0, value = True }+ , { index = 1, value = True }+ , { index = 2, value = False } ]-, [ { index = +0, value = False }- , { index = +1, value = False }+, [ { index = 0, value = False }+ , { index = 1, value = False } ]-, [ { index = +0, value = True }- , { index = +1, value = True }- , { index = +2, value = True }- , { index = +3, value = True }+, [ { index = 0, value = True }+ , { index = 1, value = True }+ , { index = 2, value = True }+ , { index = 3, value = True } ] ]
tests/normalization/examples/List/shifted/0B.dhall view
@@ -1,10 +1,10 @@-[ { index = +0, value = True }-, { index = +1, value = True }-, { index = +2, value = False }-, { index = +3, value = False }-, { index = +4, value = False }-, { index = +5, value = True }-, { index = +6, value = True }-, { index = +7, value = True }-, { index = +8, value = True }+[ { index = 0, value = True }+, { index = 1, value = True }+, { index = 2, value = False }+, { index = 3, value = False }+, { index = 4, value = False }+, { index = 5, value = True }+, { index = 6, value = True }+, { index = 7, value = True }+, { index = 8, value = True } ]
tests/normalization/examples/Natural/build/0B.dhall view
@@ -1,1 +1,1 @@-+3+3
tests/normalization/examples/Natural/build/1B.dhall view
@@ -1,1 +1,1 @@-+0+0
tests/normalization/examples/Natural/enumerate/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/enumerate +10+../../../../../Prelude/Natural/enumerate 10
tests/normalization/examples/Natural/enumerate/0B.dhall view
@@ -1,1 +1,1 @@-[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]+[ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
tests/normalization/examples/Natural/enumerate/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/enumerate +0+../../../../../Prelude/Natural/enumerate 0
tests/normalization/examples/Natural/even/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/even +3+../../../../../Prelude/Natural/even 3
tests/normalization/examples/Natural/even/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/even +0+../../../../../Prelude/Natural/even 0
tests/normalization/examples/Natural/fold/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1+../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) 1
tests/normalization/examples/Natural/fold/0B.dhall view
@@ -1,1 +1,1 @@-+125+125
tests/normalization/examples/Natural/fold/1A.dhall view
@@ -1,1 +1,1 @@-λ(zero : Natural) → ../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero+λ(zero : Natural) → ../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) zero
tests/normalization/examples/Natural/fold/1B.dhall view
@@ -1,1 +1,1 @@-λ(zero : Natural) → +5 * +5 * +5 * zero+λ(zero : Natural) → 5 * 5 * 5 * zero
tests/normalization/examples/Natural/fold/2A.dhall view
@@ -1,4 +1,4 @@ λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural)-→ ../../../../../Prelude/Natural/fold +3 natural succ zero+→ ../../../../../Prelude/Natural/fold 3 natural succ zero
tests/normalization/examples/Natural/isZero/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/isZero +2+../../../../../Prelude/Natural/isZero 2
tests/normalization/examples/Natural/isZero/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/isZero +0+../../../../../Prelude/Natural/isZero 0
tests/normalization/examples/Natural/odd/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/odd +3+../../../../../Prelude/Natural/odd 3
tests/normalization/examples/Natural/odd/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/odd +0+../../../../../Prelude/Natural/odd 0
tests/normalization/examples/Natural/product/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/product [ +2, +3, +5 ]+../../../../../Prelude/Natural/product [ 2, 3, 5 ]
tests/normalization/examples/Natural/product/0B.dhall view
@@ -1,1 +1,1 @@-+30+30
tests/normalization/examples/Natural/product/1B.dhall view
@@ -1,1 +1,1 @@-+1+1
tests/normalization/examples/Natural/show/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/show +3+../../../../../Prelude/Natural/show 3
tests/normalization/examples/Natural/show/0B.dhall view
@@ -1,1 +1,1 @@-"+3"+"3"
tests/normalization/examples/Natural/show/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/show +0+../../../../../Prelude/Natural/show 0
tests/normalization/examples/Natural/show/1B.dhall view
@@ -1,1 +1,1 @@-"+0"+"0"
tests/normalization/examples/Natural/sum/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/sum [ +2, +3, +5 ]+../../../../../Prelude/Natural/sum [ 2, 3, 5 ]
tests/normalization/examples/Natural/sum/0B.dhall view
@@ -1,1 +1,1 @@-+10+10
tests/normalization/examples/Natural/sum/1B.dhall view
@@ -1,1 +1,1 @@-+0+0
tests/normalization/examples/Natural/toInteger/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/toInteger +3+../../../../../Prelude/Natural/toInteger 3
tests/normalization/examples/Natural/toInteger/0B.dhall view
@@ -1,1 +1,1 @@-3++3
tests/normalization/examples/Natural/toInteger/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Natural/toInteger +0+../../../../../Prelude/Natural/toInteger 0
tests/normalization/examples/Natural/toInteger/1B.dhall view
@@ -1,1 +1,1 @@-0++0
tests/normalization/examples/Optional/all/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural)+../../../../../Prelude/Optional/all Natural Natural/even ([ 3 ] : Optional Natural)
tests/normalization/examples/Optional/any/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural)+../../../../../Prelude/Optional/any Natural Natural/even ([ 2 ] : Optional Natural)
tests/normalization/examples/Optional/build/0A.dhall view
@@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/build-Integer+Natural ( λ(optional : Type)-→ λ(just : Integer → optional)+→ λ(just : Natural → optional) → λ(nothing : optional) → just 1 )
tests/normalization/examples/Optional/build/0B.dhall view
@@ -1,1 +1,1 @@-[ 1 ] : Optional Integer+[ 1 ] : Optional Natural
tests/normalization/examples/Optional/build/1A.dhall view
@@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/build-Integer+Natural ( λ(optional : Type)-→ λ(just : Integer → optional)+→ λ(just : Natural → optional) → λ(nothing : optional) → nothing )
tests/normalization/examples/Optional/build/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/concat/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer))+../../../../../Prelude/Optional/concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural))
tests/normalization/examples/Optional/concat/0B.dhall view
@@ -1,1 +1,1 @@-[ 1 ] : Optional Integer+[ 1 ] : Optional Natural
tests/normalization/examples/Optional/concat/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))+../../../../../Prelude/Optional/concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural))
tests/normalization/examples/Optional/concat/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/concat/2A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ]: Optional (Optional Integer))+../../../../../Prelude/Optional/concat Natural ([ [] : Optional Natural ]: Optional (Optional Natural))
tests/normalization/examples/Optional/concat/2B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/filter/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural)+../../../../../Prelude/Optional/filter Natural Natural/even ([ 2 ] : Optional Natural)
tests/normalization/examples/Optional/filter/0B.dhall view
@@ -1,1 +1,1 @@-[ +2 ] : Optional Natural+[ 2 ] : Optional Natural
tests/normalization/examples/Optional/filter/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural)+../../../../../Prelude/Optional/filter Natural Natural/odd ([ 2 ] : Optional Natural)
tests/normalization/examples/Optional/fold/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0+../../../../../Prelude/Optional/fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0
tests/normalization/examples/Optional/fold/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0+../../../../../Prelude/Optional/fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0
tests/normalization/examples/Optional/head/0A.dhall view
@@ -1,6 +1,6 @@ ../../../../../Prelude/Optional/head-Integer-[ [] : Optional Integer-, [ 1 ] : Optional Integer-, [ 2 ] : Optional Integer+Natural+[ [] : Optional Natural+, [ 1 ] : Optional Natural+, [ 2 ] : Optional Natural ]
tests/normalization/examples/Optional/head/0B.dhall view
@@ -1,1 +1,1 @@-[ 1 ] : Optional Integer+[ 1 ] : Optional Natural
tests/normalization/examples/Optional/head/1A.dhall view
@@ -1,3 +1,3 @@ ../../../../../Prelude/Optional/head-Integer-[ [] : Optional Integer, [] : Optional Integer ]+Natural+[ [] : Optional Natural, [] : Optional Natural ]
tests/normalization/examples/Optional/head/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/last/0A.dhall view
@@ -1,7 +1,7 @@ ../../../../../Prelude/Optional/last-Integer-( [ [] : Optional Integer- , [ 1 ] : Optional Integer- , [ 2 ] : Optional Integer+Natural+( [ [] : Optional Natural+ , [ 1 ] : Optional Natural+ , [ 2 ] : Optional Natural ] )
tests/normalization/examples/Optional/last/0B.dhall view
@@ -1,1 +1,1 @@-[ 2 ] : Optional Integer+[ 2 ] : Optional Natural
tests/normalization/examples/Optional/last/1A.dhall view
@@ -1,3 +1,3 @@ ../../../../../Prelude/Optional/last-Integer-[ [] : Optional Integer, [] : Optional Integer ]+Natural+[ [] : Optional Natural, [] : Optional Natural ]
tests/normalization/examples/Optional/last/1B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/last/2A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/last Integer ([] : List (Optional Integer))+../../../../../Prelude/Optional/last Natural ([] : List (Optional Natural))
tests/normalization/examples/Optional/last/2B.dhall view
@@ -1,1 +1,1 @@-[] : Optional Integer+[] : Optional Natural
tests/normalization/examples/Optional/length/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/length Integer ([ 2 ] : Optional Integer)+../../../../../Prelude/Optional/length Natural ([ 2 ] : Optional Natural)
tests/normalization/examples/Optional/length/0B.dhall view
@@ -1,1 +1,1 @@-+1+1
tests/normalization/examples/Optional/length/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/length Integer ([] : Optional Integer)+../../../../../Prelude/Optional/length Natural ([] : Optional Natural)
tests/normalization/examples/Optional/length/1B.dhall view
@@ -1,1 +1,1 @@-+0+0
tests/normalization/examples/Optional/map/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/map Natural Bool Natural/even ([ +3 ] : Optional Natural)+../../../../../Prelude/Optional/map Natural Bool Natural/even ([ 3 ] : Optional Natural)
tests/normalization/examples/Optional/null/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/null Integer ([ 2 ] : Optional Integer)+../../../../../Prelude/Optional/null Natural ([ 2 ] : Optional Natural)
tests/normalization/examples/Optional/null/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/null Integer ([] : Optional Integer)+../../../../../Prelude/Optional/null Natural ([] : Optional Natural)
tests/normalization/examples/Optional/toList/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/toList Integer ([ 1 ] : Optional Integer)+../../../../../Prelude/Optional/toList Natural ([ 1 ] : Optional Natural)
tests/normalization/examples/Optional/toList/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Optional/toList Integer ([] : Optional Integer)+../../../../../Prelude/Optional/toList Natural ([] : Optional Natural)
tests/normalization/examples/Optional/toList/1B.dhall view
@@ -1,1 +1,1 @@-[] : List Integer+[] : List Natural
tests/normalization/examples/Text/concatMap/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ]+../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ]
tests/normalization/examples/Text/concatMap/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer)+../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural)
tests/normalization/examples/Text/concatMapSep/0A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show [ 0, 1, 2 ]+../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show [ 0, 1, 2 ]
tests/normalization/examples/Text/concatMapSep/1A.dhall view
@@ -1,1 +1,1 @@-../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show ([] : List Integer)+../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show ([] : List Natural)
tests/normalization/integerShowA.dhall view
@@ -1,4 +1,4 @@-{ example0 = Integer/show 1337+{ example0 = Integer/show +1337 , example1 = Integer/show -42-, example2 = Integer/show 0+, example2 = Integer/show +0 }
tests/normalization/integerShowB.dhall view
@@ -1,1 +1,1 @@-{ example0 = "1337", example1 = "-42", example2 = "0" }+{ example0 = "+1337", example1 = "-42", example2 = "+0" }
tests/normalization/naturalPlusA.dhall view
@@ -1,1 +1,1 @@-+1 + +2+1 + 2
tests/normalization/naturalPlusB.dhall view
@@ -1,1 +1,1 @@-+3+3
tests/normalization/naturalShowA.dhall view
@@ -1,1 +1,1 @@-Natural/show +42+Natural/show 42
tests/normalization/naturalShowB.dhall view
@@ -1,1 +1,1 @@-"+42"+"42"
tests/normalization/naturalToIntegerA.dhall view
@@ -1,1 +1,1 @@-Natural/toInteger +1+Natural/toInteger 1
tests/normalization/naturalToIntegerB.dhall view
@@ -1,1 +1,1 @@-1++1
tests/normalization/optionalBuildA.dhall view
@@ -4,12 +4,12 @@ ( λ(optional : Type) → λ(just : Natural → optional) → λ(nothing : optional)- → just +1+ → just 1 ) , example1 = Optional/build Integer- (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 1)+ (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 +1) , example2 = λ(id : ∀(a : Type) → a → a) → Optional/build
tests/normalization/optionalBuildB.dhall view
@@ -1,7 +1,7 @@ { example0 =- [ +1 ] : Optional Natural+ [ 1 ] : Optional Natural , example1 =- [ 1 ] : Optional Integer+ [ +1 ] : Optional Integer , example2 = λ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool) , example3 =
tests/normalization/optionalFoldA.dhall view
@@ -1,6 +1,6 @@ let f = λ(o : Optional Text)- → Optional/fold Text o Natural (λ(j : Text) → +1) +2+ → Optional/fold Text o Natural (λ(j : Text) → 1) 2 in { example0 = f ([ "foo" ] : Optional Text) , example1 = f ([] : Optional Text)
tests/normalization/optionalFoldB.dhall view
@@ -1,1 +1,1 @@-{ example0 = +1, example1 = +2 }+{ example0 = 1, example1 = 2 }
tests/parser/urls.dhall view
@@ -1,11 +1,11 @@-[ http://example.com+[ http://example.com/someFile.dhall , https://john:doe@example.com:8080/foo/bar?qux=0#xyzzy-, http://prelude.dhall-lang.org/+, http://prelude.dhall-lang.org/package.dhall , https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude-, https://127.0.0.1-, https://[::]-, https://[2001:0db8:85a3:0000:0000:8a2e:0370:7334]+, https://127.0.0.1/index.dhall+, https://[::]/index.dhall+, https://[2001:0db8:85a3:0000:0000:8a2e:0370:7334]/tutorial.dhall -- Yes, this is legal-, https://-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:/-._~%2C!$&'()*+,;=:@?/-._~%2C!$&'()*+,;=:@/?#/-._~%2C!$&'()*+,;=:@/?+, https://-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:/foo?/-._~%2C!$&'()*+,;=:@/?#/-._~%2C!$&'()*+,;=:@/? ]
tests/regression/issue216b.dhall view
@@ -1,10 +1,2 @@- let GitHubProject : Type = { owner : Text, repo : Text }--in let gitHubProject =- λ(github : GitHubProject)- → let gitHubRoot =- "https://github.com/${github.owner}/${github.repo}"- - in { bugReports = "${gitHubRoot}/issues" }--in gitHubProject+ λ(github : { owner : Text, repo : Text })+→ { bugReports = "https://github.com/${github.owner}/${github.repo}/issues" }
tests/tutorial/unions0A.dhall view
@@ -1,1 +1,1 @@-./process.dhall < Left = +3 | Right : Bool >+./process.dhall < Left = 3 | Right : Bool >
tests/tutorial/unions2A.dhall view
@@ -2,7 +2,7 @@ in let Person = λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > in [ Empty- , Person { name = "John", age = +23 }- , Person { name = "Amy" , age = +25 }+ , Person { name = "John", age = 23 }+ , Person { name = "Amy" , age = 25 } , Empty ]
tests/tutorial/unions2B.dhall view
@@ -1,5 +1,5 @@ [ < Empty = {=} | Person : { age : Natural, name : Text } >-, < Person = { age = +23, name = "John" } | Empty : {} >-, < Person = { age = +25, name = "Amy" } | Empty : {} >+, < Person = { age = 23, name = "John" } | Empty : {} >+, < Person = { age = 25, name = "Amy" } | Empty : {} > , < Empty = {=} | Person : { age : Natural, name : Text } > ]
tests/tutorial/unions3A.dhall view
@@ -1,5 +1,5 @@ let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > in [ MyType.Empty {=}- , MyType.Person { name = "John", age = +23 }- , MyType.Person { name = "Amy" , age = +25 }+ , MyType.Person { name = "John", age = 23 }+ , MyType.Person { name = "Amy" , age = 25 } ]
tests/tutorial/unions3B.dhall view
@@ -1,4 +1,4 @@ [ < Empty = {=} | Person : { age : Natural, name : Text } >-, < Person = { age = +23, name = "John" } | Empty : {} >-, < Person = { age = +25, name = "Amy" } | Empty : {} >+, < Person = { age = 23, name = "John" } | Empty : {} >+, < Person = { age = 25, name = "Amy" } | Empty : {} > ]
+ tests/typecheck/mergeEquivalenceA.dhall view
@@ -0,0 +1,6 @@+ let Foo = < Bar : {} | Baz : {} >++in λ(a : Type)+ → λ(f : {} → a)+ → λ(ts : Foo)+ → merge { Bar = λ(a : {}) → f a, Baz = f } ts
+ tests/typecheck/mergeEquivalenceB.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → ∀(f : {} → a) → ∀(ts : < Bar : {} | Baz : {} >) → a