diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,33 @@ +1.4.0 + +* BREAKING CHANGE TO THE LANGUAGE AND API: You can now supply custom headers for + URL imports with the new `using` keyword + * This is a breaking change to the language because this adds a new reserved + `using` keyword + * This is a breaking change to the API because this adds a new field to the + `URL` constructor to store optional custom headers +* BUG FIX: `:` is no longer a disallowed path character + * This was breaking URL imports with a port +* BUG FIX: If you import a home-anchored path (i.e. `~/foo`) and that imports a + relative path (like `./bar`), then the canonical path of the relative import + should be home-anchored (i.e. `~/bar`). However, there was a bug that made + lose the home anchor (i.e. `./foo/bar`), which this release fixes + likely fail due to no longer being home-anchored (i.e. `./foob +* Add support for string interpolation +* `merge` no longer requires a type annotation if you are merging at least one + alternative +* Expanded Prelude + * `./Prelude/Optional/all` + * `./Prelude/Optional/any` + * `./Prelude/Optional/filter` + * `./Prelude/Optional/length` + * `./Prelude/Optional/null` + * `./Prelude/Text/concatMap` + * `./Prelude/Text/concatMapSep` + * `./Prelude/Text/concatSep` +* Rearrange detailed error messages to put summary information at the bottom of + the message + 1.3.0 * BREAKING CHANGE TO THE API: Add support for new primitives, specifically: diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.3.0 +Version: 1.4.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.10.2, GHC == 8.0.1 @@ -83,6 +83,7 @@ base >= 4.8.0.0 && < 5 , ansi-wl-pprint < 0.7 , bytestring < 0.11, + case-insensitive < 1.3 , charset < 0.4 , containers >= 0.5.0.0 && < 0.6 , http-client >= 0.4.30 && < 0.6 , @@ -95,7 +96,7 @@ text >= 0.11.1.0 && < 1.3 , text-format < 0.4 , transformers >= 0.2.0.0 && < 0.6 , - trifecta >= 1.6 && < 1.7 , + trifecta >= 1.6 && < 1.8 , unordered-containers >= 0.1.3.0 && < 0.3 , vector >= 0.11.0.0 && < 0.13 Exposed-Modules: @@ -115,7 +116,7 @@ base >= 4 && < 5 , dhall , optparse-generic >= 1.1.1 && < 1.2, - trifecta >= 1.6 && < 1.7, + trifecta >= 1.6 && < 1.8, text >= 0.11.1.0 && < 1.3 GHC-Options: -Wall Other-Modules: diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -100,8 +100,8 @@ data PathType = File HasHome FilePath -- ^ Local path - | URL Text - -- ^ Remote resource + | URL Text (Maybe PathType) + -- ^ URL of emote resource and optional headers stored in a path | Env Text -- ^ Environment variable deriving (Eq, Ord, Show) @@ -120,8 +120,9 @@ = "./" <> build txt <> " " where txt = Text.fromStrict (either id id (Filesystem.toText file)) - build (URL str ) = build str <> " " - build (Env env ) = "env:" <> build env + build (URL str Nothing ) = build str <> " " + build (URL str (Just headers)) = build str <> " using " <> build headers <> " " + build (Env env) = "env:" <> build env -- | How to interpret the path's contents (i.e. as Dhall code or raw text) data PathMode = Code | RawText deriving (Eq, Ord, Show) @@ -293,8 +294,9 @@ | Combine (Expr s a) (Expr s a) -- | > CombineRight x y ~ x ⫽ y | Prefer (Expr s a) (Expr s a) - -- | > Merge x y t ~ merge x y : t - | Merge (Expr s a) (Expr s a) (Expr s a) + -- | > Merge x y (Just t ) ~ merge x y : t + -- | > Merge x y Nothing ~ merge x y + | Merge (Expr s a) (Expr s a) (Maybe (Expr s a)) -- | > Field e x ~ e.x | Field (Expr s a) Text -- | > Note s x ~ e @@ -364,7 +366,7 @@ UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c) Combine a b >>= k = Combine (a >>= k) (b >>= k) Prefer a b >>= k = Prefer (a >>= k) (b >>= k) - Merge a b c >>= k = Merge (a >>= k) (b >>= k) (c >>= k) + Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c) Field a b >>= k = Field (a >>= k) b Note a b >>= k = Note a (b >>= k) Embed a >>= k = k a @@ -423,7 +425,7 @@ first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c) first k (Combine a b ) = Combine (first k a) (first k b) first k (Prefer a b ) = Prefer (first k a) (first k b) - first k (Merge a b c ) = Merge (first k a) (first k b) (first k c) + first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c) first k (Field a b ) = Field (first k a) b first k (Note a b ) = Note (k a) (first k b) first _ (Embed a ) = Embed a @@ -530,8 +532,10 @@ "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a buildExprB (OptionalLit a b) = "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a -buildExprB (Merge a b c) = +buildExprB (Merge a b (Just c)) = "merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c +buildExprB (Merge a b Nothing) = + "merge " <> buildExprE a <> " " <> buildExprE b buildExprB (Note _ b) = buildExprB b buildExprB a = @@ -972,9 +976,9 @@ b' = shift d v b shift d v (Merge a b c) = Merge a' b' c' where - a' = shift d v a - b' = shift d v b - c' = shift d v c + a' = shift d v a + b' = shift d v b + c' = fmap (shift d v) c shift d v (Field a b) = Field a' b where a' = shift d v a @@ -1103,9 +1107,9 @@ b' = subst x e b subst x e (Merge a b c) = Merge a' b' c' where - a' = subst x e a - b' = subst x e b - c' = subst x e c + a' = subst x e a + b' = subst x e b + c' = fmap (subst x e) c subst x e (Field a b) = Field a' b where a' = subst x e a @@ -1419,9 +1423,9 @@ _ -> Merge x' y' t' _ -> Merge x' y' t' where - x' = normalize x - y' = normalize y - t' = normalize t + x' = normalize x + y' = normalize y + t' = fmap normalize t Field r x -> case normalize r of RecordLit kvs -> @@ -1612,7 +1616,7 @@ RecordLit _ -> False _ -> True _ -> True - Merge x y t -> isNormalized x && isNormalized y && isNormalized t && + Merge x y t -> isNormalized x && isNormalized y && any isNormalized t && case x of RecordLit kvsX -> case y of @@ -1674,6 +1678,7 @@ (len, _, mv) <- f cons nil return (Data.Vector.Mutable.slice 0 len mv) )) +-- | The set of reserved identifiers for the Dhall language reservedIdentifiers :: HashSet String reservedIdentifiers = Data.HashSet.fromList @@ -1690,6 +1695,7 @@ , "then" , "else" , "as" + , "using" , "Natural" , "Natural/fold" , "Natural/build" diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -1,6 +1,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall #-} @@ -109,6 +110,7 @@ , MissingFile(..) ) where +import Control.Applicative (empty) import Control.Exception (Exception, IOException, SomeException, catch, onException, throwIO) import Control.Lens (Lens', zoom) @@ -116,6 +118,7 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Data.ByteString.Lazy (ByteString) +import Data.CaseInsensitive (CI) import Data.Map.Strict (Map) import Data.Monoid ((<>)) import Data.Text.Buildable (build) @@ -129,7 +132,7 @@ import Filesystem.Path ((), FilePath) import Dhall.Core (Expr(..), HasHome(..), PathMode(..), PathType(..), Path(..)) -import Dhall.Parser (Parser(..), ParseError(..), Src) +import Dhall.Parser (Parser(..), ParseError(..), Src(..)) import Dhall.TypeCheck (X(..)) #if MIN_VERSION_http_client(0,5,0) import Network.HTTP.Client @@ -142,16 +145,23 @@ import Text.Trifecta.Delta (Delta(..)) import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.ByteString import qualified Data.ByteString.Lazy +import qualified Data.CaseInsensitive import qualified Data.List as List import qualified Data.Map.Strict as Map +import qualified Data.Text +import qualified Data.Text.Encoding import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Encoding +import qualified Data.Vector +import qualified Dhall.Core import qualified Dhall.Parser import qualified Dhall.TypeCheck import qualified Filesystem import qualified Filesystem.Path.CurrentOS +import qualified NeatInterpolation import qualified Network.HTTP.Client as HTTP import qualified Network.HTTP.Client.TLS as HTTP import qualified Filesystem.Path.CurrentOS as Filesystem @@ -360,10 +370,12 @@ then go file0 paths0 else File hasHome0 (clean file0) where - go currPath [] = File hasHome0 (clean currPath) - go currPath (Env _ :_ ) = File hasHome0 (clean currPath) - go currPath (URL url0:_ ) = combine prefix suffix + go currPath [] = File Homeless (clean currPath) + go currPath (Env _ :_ ) = File Homeless (clean currPath) + go currPath (URL url0 headers:rest ) = combine prefix suffix where + headers' = fmap (\h -> canonicalize (h:rest)) headers + prefix = parentURL (removeAtFromURL url0) suffix = clean currPath @@ -381,8 +393,8 @@ -- 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') - _ -> URL (url <> "/" <> path') + '/' -> URL (url <> path') headers' + _ -> URL (url <> "/" <> path') headers' where path' = Text.fromStrict (case Filesystem.toText path of Left txt -> txt @@ -390,11 +402,13 @@ go currPath (File hasHome file:paths) = if Filesystem.relative file && hasHome == Homeless then go file' paths - else File hasHome0 (clean file') + else File hasHome (clean file') where file' = Filesystem.parent (removeAtFromFile file) currPath -canonicalize (URL path:_) = URL path -canonicalize (Env env :_) = Env env +canonicalize (URL path headers:rest) = URL path headers' + where + headers' = fmap (\h -> canonicalize (h:rest)) headers +canonicalize (Env env :_ ) = Env env canonicalizePath :: [Path] -> Path canonicalizePath [] = @@ -431,6 +445,62 @@ Nothing -> p Just p' -> p' +toHeaders + :: Expr s a + -> Maybe [(CI Data.ByteString.ByteString, Data.ByteString.ByteString)] +toHeaders (ListLit _ hs) = do + hs' <- mapM toHeader hs + return (Data.Vector.toList hs') +toHeaders _ = do + empty + +toHeader + :: Expr s a + -> Maybe (CI Data.ByteString.ByteString, Data.ByteString.ByteString) +toHeader (RecordLit m) = do + TextLit keyBuilder <- Map.lookup "header" m + TextLit valueBuilder <- Map.lookup "value" m + let keyText = Text.toStrict (Builder.toLazyText keyBuilder ) + let valueText = Text.toStrict (Builder.toLazyText valueBuilder) + let keyBytes = Data.Text.Encoding.encodeUtf8 keyText + let valueBytes = Data.Text.Encoding.encodeUtf8 valueText + return (Data.CaseInsensitive.mk keyBytes, valueBytes) +toHeader _ = do + empty + + +{-| This exception indicates that there was an internal error in Dhall's + import-related logic + the `expected` type then the `extract` function must succeed. If not, then + this exception is thrown + + This exception indicates that an invalid `Type` was provided to the `input` + function +-} +data InternalError = InternalError deriving (Typeable) + +_ERROR :: Data.Text.Text +_ERROR = "\ESC[1;31mError\ESC[0m" + +instance Show InternalError where + show InternalError = Data.Text.unpack [NeatInterpolation.text| +$_ERROR: Compiler bug + +Explanation: This error message means that there is a bug in the Dhall compiler. +You didn't do anything wrong, but if you would like to see this problem fixed +then you should report the bug at: + +https://github.com/Gabriel439/Haskell-Dhall-Library/issues + +Please include the following text in your bug report: + +``` +Header extraction failed even though the header type-checked +``` +|] + +instance Exception InternalError + -- | Parse an expression from a `Path` containing a Dhall program exprFromPath :: Manager -> Path -> IO (Expr Src Path) exprFromPath m (Path {..}) = case pathType of @@ -474,7 +544,7 @@ RawText -> do text <- Filesystem.readTextFile path return (TextLit (build text)) - URL url -> do + URL url headerPath -> do request <- HTTP.parseUrlThrow (Text.unpack url) let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) @@ -488,8 +558,45 @@ -- user confusion HTTP.httpLbs request' m `onException` throwIO (PrettyHttpException err) handler err = throwIO (PrettyHttpException err) - response <- HTTP.httpLbs request m `catch` handler + requestWithHeaders <- case headerPath of + Nothing -> return request + Just path -> do + expr <- load (Embed (Path path Code)) + let expected :: Expr Src X + expected = + App List + ( Record + ( Map.fromList + [("header", Text), ("value", Text)] + ) + ) + let suffix = + ( Data.ByteString.Lazy.toStrict + . Data.Text.Lazy.Encoding.encodeUtf8 + . 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 -> Control.Exception.throwIO err + Right _ -> return () + let expr' = Dhall.Core.normalize expr + headers <- case toHeaders expr' of + Just headers -> return headers + Nothing -> Control.Exception.throwIO InternalError + let requestWithHeaders = request + { HTTP.requestHeaders = headers + } + return requestWithHeaders + response <- HTTP.httpLbs requestWithHeaders m `catch` handler + let bytes = HTTP.responseBody response text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of @@ -570,14 +677,15 @@ loadStatic path = do paths <- zoom stack State.get - let local (Path (URL url ) _) = case HTTP.parseUrlThrow (Text.unpack url) of - Nothing -> False - Just request -> case HTTP.host request of - "127.0.0.1" -> True - "localhost" -> True - _ -> False - local (Path (File _ _) _) = True - local (Path (Env _ ) _) = True + let local (Path (URL url _) _) = + case HTTP.parseUrlThrow (Text.unpack url) of + Nothing -> False + Just request -> case HTTP.host request of + "127.0.0.1" -> True + "localhost" -> True + _ -> False + local (Path (File _ _ ) _) = True + local (Path (Env _ ) _) = True let parent = canonicalizePath paths let here = canonicalizePath (path:paths) diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -28,7 +28,6 @@ import Data.Sequence (ViewL(..)) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) -import Data.Text.Lazy.Builder (Builder) import Data.Typeable (Typeable) import Data.Vector (Vector) import Dhall.Core @@ -164,60 +163,169 @@ as <- sepBy p sep return (a:as) -stringLiteral :: Parser Builder -stringLiteral = Text.Parser.Token.stringLiteral <|> doubleSingleQuoteString +stringLiteral :: Show a => Parser a -> Parser (Expr Src a) +stringLiteral embedded = + Text.Parser.Token.token + ( doubleQuoteLiteral embedded + <|> doubleSingleQuoteString embedded + ) -doubleSingleQuoteString :: Parser Builder -doubleSingleQuoteString = do - builder <- Text.Parser.Token.token p0 - return (process builder) +doubleQuoteLiteral :: Show a => Parser a -> Parser (Expr Src a) +doubleQuoteLiteral embedded = do + _ <- Text.Parser.Char.char '"' + go where - process = - Data.Text.Lazy.Builder.fromLazyText - . Data.Text.Lazy.unlines - . trim - . Data.Text.Lazy.lines - . Data.Text.Lazy.Builder.toLazyText + go = go0 <|> go1 <|> go2 <|> go3 - trim lines_ = map (Data.Text.Lazy.drop shortestIndent) lines_ - where - isEmpty = Data.Text.Lazy.all Data.Char.isSpace + go0 = do + _ <- Text.Parser.Char.char '"' + return (TextLit mempty) - nonEmptyLines = filter (not . isEmpty) lines_ + go1 = do + _ <- Text.Parser.Char.text "${" + Text.Parser.Token.whiteSpace + a <- exprA embedded + _ <- Text.Parser.Char.char '}' + b <- go + return (TextAppend a b) - indentLength line = + go2 = do + _ <- Text.Parser.Char.text "''${" + b <- go + let e = case b of + TextLit cs -> + TextLit ("${" <> cs) + TextAppend (TextLit cs) d -> + TextAppend (TextLit ("${" <> cs)) d + _ -> + TextAppend (TextLit "${") b + return e + + go3 = do + a <- Text.Parser.Token.characterChar + b <- go + let e = case b of + TextLit cs -> + TextLit (build a <> cs) + TextAppend (TextLit cs) d -> + TextAppend (TextLit (build a <> cs)) d + _ -> + TextAppend (TextLit (build a)) b + return e + +doubleSingleQuoteString :: Show a => Parser a -> Parser (Expr Src a) +doubleSingleQuoteString embedded = do + expr0 <- Text.Parser.Token.token p0 + + let builder0 = concatFragments expr0 + let text0 = Data.Text.Lazy.Builder.toLazyText builder0 + let lines0 = Data.Text.Lazy.lines text0 + let isEmpty = Data.Text.Lazy.all Data.Char.isSpace + let nonEmptyLines = filter (not . isEmpty) lines0 + + let indentLength line = Data.Text.Lazy.length (Data.Text.Lazy.takeWhile Data.Char.isSpace line) - shortestIndent = case nonEmptyLines of + let shortestIndent = case nonEmptyLines of [] -> 0 _ -> minimum (map indentLength nonEmptyLines) + -- The purpose of this complicated `trim0`/`trim1` is to ensure that we + -- strip leading whitespace without stripping whitespace after variable + -- interpolation + let trim0 = + build + . Data.Text.Lazy.intercalate "\n" + . map (Data.Text.Lazy.drop shortestIndent) + . Data.Text.Lazy.splitOn "\n" + . Data.Text.Lazy.Builder.toLazyText + + let trim1 builder = build (Data.Text.Lazy.intercalate "\n" lines_) + where + text = Data.Text.Lazy.Builder.toLazyText builder + + lines_ = case Data.Text.Lazy.splitOn "\n" text of + [] -> [] + l:ls -> l:map (Data.Text.Lazy.drop shortestIndent) ls + + let process trim (TextAppend (TextLit t) e) = + TextAppend (TextLit (trim t)) (process trim1 e) + process _ (TextAppend e0 e1) = + TextAppend e0 (process trim1 e1) + process trim (TextLit t) = + TextLit (trim t) + process _ e = + e + + return (process trim0 expr0) + where + -- This treats variable interpolation as breaking leading whitespace for the + -- purposes of computing the shortest leading whitespace. The "${VAR}" + -- could really be any text that breaks whitespace + concatFragments (TextAppend (TextLit t) e) = t <> concatFragments e + concatFragments (TextAppend _ e) = "${VAR}" <> concatFragments e + concatFragments (TextLit t) = t + concatFragments _ = mempty + p0 = do _ <- Text.Parser.Char.string "''" p1 - p1 = p2 <|> p3 <|> p4 <|> p5 + p1 = p2 + <|> p3 + <|> p4 + <|> p5 (Text.Parser.Char.char '\'') + <|> p6 + <|> p5 Text.Parser.Char.anyChar p2 = do _ <- Text.Parser.Char.text "'''" s1 <- p1 - return ("''" <> s1) + let s4 = case s1 of + TextLit s2 -> + TextLit ("''" <> s2) + TextAppend (TextLit s2) s3 -> + TextAppend (TextLit ("''" <> s2)) s3 + _ -> + TextAppend (TextLit "''") s1 + return s4 p3 = do - _ <- Text.Parser.Char.text "''" - return "" + _ <- Text.Parser.Char.text "''${" + s1 <- p1 + let s4 = case s1 of + TextLit s2 -> + TextLit ("${" <> s2) + TextAppend (TextLit s2) s3 -> + TextAppend (TextLit ("${" <> s2)) s3 + _ -> + TextAppend (TextLit "${") s1 + return s4 p4 = do - s0 <- Text.Parser.Char.text "'" - s1 <- p1 - return (Data.Text.Lazy.Builder.fromText s0 <> s1) + _ <- Text.Parser.Char.text "''" + return (TextLit mempty) - p5 = do - s0 <- some (Text.Trifecta.satisfy (/= '\'')) + p5 parser = do + s0 <- parser s1 <- p1 - return (Data.Text.Lazy.Builder.fromString s0 <> s1) + let s4 = case s1 of + TextLit s2 -> + TextLit (build s0 <> s2) + TextAppend (TextLit s2) s3 -> + TextAppend (TextLit (build s0 <> s2)) s3 + _ -> TextAppend (TextLit (build s0)) s1 + return s4 + p6 = do + _ <- Text.Parser.Char.text "${" + Text.Parser.Token.whiteSpace + s1 <- exprA embedded + _ <- Text.Parser.Char.char '}' + s3 <- p1 + return (TextAppend s1 s3) + lambda :: Parser () lambda = symbol "\\" <|> symbol "λ" @@ -323,8 +431,9 @@ reserve "merge" a <- exprE embedded b <- exprE embedded - symbol ":" - c <- exprD embedded + c <- optional (do + symbol ":" + exprD embedded ) return (Merge a b c) exprB1 = do @@ -584,9 +693,7 @@ a <- Text.Parser.Token.double return (DoubleLit (sign a)) - exprStringLiteral = do - a <- stringLiteral - return (TextLit a) + exprStringLiteral = stringLiteral embedded exprRecordType = record embedded "record type" @@ -731,8 +838,7 @@ import_ :: Parser Path import_ = do - pathType <- file <|> url <|> env - Text.Parser.Token.whiteSpace + pathType <- pathType_ let rawText = do _ <- reserve "as" _ <- reserve "Text" @@ -740,6 +846,9 @@ pathMode <- rawText <|> pure Code return (Path {..}) +pathType_ :: Parser PathType +pathType_ = file <|> url <|> env + pathChar :: Char -> Bool pathChar c = not @@ -748,7 +857,7 @@ ) disallowedPathChars :: CharSet -disallowedPathChars = Data.CharSet.fromList "()[]{}<>:" +disallowedPathChars = Data.CharSet.fromList "()[]{}<>" file :: Parser PathType file = try (token file0) @@ -763,22 +872,26 @@ '\\':_ -> empty -- So that "/\" parses as the operator and not a path '/' :_ -> empty -- So that "//" parses as the operator and not a path _ -> return () + Text.Parser.Token.whiteSpace return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) file1 = do a <- Text.Parser.Char.string "./" b <- many (Text.Parser.Char.satisfy pathChar) + Text.Parser.Token.whiteSpace return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) file2 = do a <- Text.Parser.Char.string "../" b <- many (Text.Parser.Char.satisfy pathChar) + Text.Parser.Token.whiteSpace return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b))) file3 = do _ <- Text.Parser.Char.string "~" _ <- some (Text.Parser.Char.string "/") b <- many (Text.Parser.Char.satisfy pathChar) + Text.Parser.Token.whiteSpace return (File Home (Filesystem.Path.CurrentOS.decodeString b)) url :: Parser PathType @@ -788,17 +901,28 @@ url0 = do a <- Text.Parser.Char.string "https://" b <- many (Text.Parser.Char.satisfy pathChar) - return (URL (Data.Text.Lazy.pack (a <> b))) + Text.Parser.Token.whiteSpace + c <- optional (do + _ <- Text.Parser.Char.string "using" + Text.Parser.Token.whiteSpace + pathType_ ) + return (URL (Data.Text.Lazy.pack (a <> b)) c) url1 = do a <- Text.Parser.Char.string "http://" b <- many (Text.Parser.Char.satisfy pathChar) - return (URL (Data.Text.Lazy.pack (a <> b))) + Text.Parser.Token.whiteSpace + c <- optional (do + _ <- Text.Parser.Char.string "using" + Text.Parser.Token.whiteSpace + pathType_ ) + return (URL (Data.Text.Lazy.pack (a <> b)) c) env :: Parser PathType env = do _ <- Text.Parser.Char.string "env:" a <- many (Text.Parser.Char.satisfy pathChar) + Text.Parser.Token.whiteSpace return (Env (Data.Text.Lazy.pack a)) -- | A parsing error diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -44,6 +44,9 @@ -- * Total -- $total + -- * Headers + -- $headers + -- * Built-in functions -- $builtins @@ -456,12 +459,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: -- --- +-- -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- --- > >>> input auto "https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool +-- > >>> input auto "https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess @@ -762,7 +765,28 @@ -- minimal indentation of the string as a whole (disregarding the indentation -- of empty lines).\" -- --- Unlike Nix-style strings, you cannot interpolate variables into the string. +-- You can also interpolate expressions into strings using @${...}@ syntax. For +-- example: +-- +-- > $ dhall +-- > let name = "John Doe" +-- > in let age = 21 +-- > in "My name is ${name} and my age is ${Integer/show age}" +-- > +-- > Text +-- > +-- > "My name is John Doe and my age is 21" +-- +-- Note that you can only interpolate expressions of type @Text@ +-- +-- If you need to insert a @"${"@ into a string without interpolation then use +-- @"''${"@ (same as Nix) +-- +-- > '' +-- > for file in *; do +-- > echo "Found ''${file}" +-- > done +-- > '' -- $combine -- @@ -904,7 +928,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall --- > let not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not +-- > let not = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not -- > in not True -- > -- > Bool @@ -1015,6 +1039,11 @@ -- Notice that each handler has to return the same type of result (@Bool@ in -- this case) which must also match the declared result type of the @merge@. -- +-- You can also omit the type annotation when merging a union with one or more +-- alternatives, like this: +-- +-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > +-- -- __Exercise__: Create a list of the following type with at least one element -- per alternative: -- @@ -1185,7 +1214,7 @@ -- complex example: -- -- > $ dhall --- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map +-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map -- > in λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3] -- > -- > ∀(f : Integer → Integer) → List Integer @@ -1209,17 +1238,61 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- --- +-- -- -- Test what the following Dhall expression normalizes to: -- --- > let replicate = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate +-- > let replicate = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/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 -- report if you succeed) +-- $headers +-- +-- Sometimes you would like to provide additional request headers when importing +-- Dhall expressions from URLs. For example, you might want to provide an +-- authorization header or specify the expected content type. +-- +-- Dhall URL imports let you add or modify request headers with the @using@ +-- keyword: +-- +-- > https://example.com using ./headers +-- +-- ... where you can replace @./headers@ with any import that points to a Dhall +-- expression of the following type: +-- +-- > List { header : Text, value : Text } +-- +-- For example, if you needed to specify the content type correctly in order to +-- download the file, then your @./headers@ file might look like this: +-- +-- > $ cat headers +-- > [ { header = "Accept", value = "application/dhall" } ] +-- +-- ... or if you needed to provide an authorization token to access a private +-- GitHub repository, then your headers could look like this: +-- +-- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN}" } ] +-- +-- This would read your GitHub API token from the @GITHUB_TOKEN@ environment +-- variable and supply that token in the authorization header. +-- +-- You cannot inline the headers within the same file as the URL. You must +-- provide them as a separate import. That means that this is /not/ legal code: +-- +-- > http://example.com using [ { header = "Accept", value = "application/dhall" } ] -- NOT legal +-- +-- Dhall will forward imports if you import an expression from a URL that +-- contains a relative import. For example, if you import an expression like +-- this: +-- +-- > http://example.com using ./headers +-- +-- ... and @http:\/\/example.com@ contains a relative import of @./foo@ then +-- Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. + -- $builtins -- -- Dhall is a restricted programming language that only supports simple built-in @@ -1763,7 +1836,7 @@ -- -- Rules: -- --- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat +-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat -- > -- > List/fold a (List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) @@ -1832,10 +1905,10 @@ -- -- Rules: -- --- > let Optional/head = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/head --- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap --- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map +-- > let Optional/head = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Optional/head +-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map -- > -- > List/head a (List/concat a xss) = -- > Optional/head a (List/map (List a) (Optional a) (List/head a) xss) @@ -1863,10 +1936,10 @@ -- -- Rules: -- --- > let Optional/last = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/last --- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap --- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map +-- > let Optional/last = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Optional/last +-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map -- > -- > List/last a (List/concat a xss) = -- > Optional/last a (List/map (List a) (Optional a) (List/last a) xss) @@ -1894,9 +1967,9 @@ -- -- Rules: -- --- > let List/shifted = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/shifted --- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat --- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map +-- > let List/shifted = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/shifted +-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat +-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map -- > -- > List/indexed a (List/concat a xss) = -- > List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) @@ -1919,9 +1992,9 @@ -- -- Rules: -- --- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map --- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat --- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap +-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map +-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat +-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap -- > -- > List/reverse a (List/concat a xss) -- > = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss)) @@ -1975,7 +2048,7 @@ -- -- There is also a Prelude available at: -- --- +-- -- -- 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 @@ -1986,12 +2059,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: -- --- +-- -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- --- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not +-- > $ curl https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2024,7 +2097,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall --- > https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not True +-- > https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not True -- > -- > Bool -- > @@ -2033,7 +2106,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall --- > let Bool/not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not +-- > let Bool/not = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not -- > in Bool/not True -- > -- > Bool @@ -2044,7 +2117,7 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- --- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Natural/even +-- > $ curl https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > @@ -2065,7 +2138,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/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/ +-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool @@ -2129,12 +2202,12 @@ -- locally like this: -- -- > $ ipfs mount --- > $ cd /ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude +-- > $ cd /ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- --- +-- -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -532,7 +532,7 @@ Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) return (Record (Data.Map.union ktsY ktsX)) -typeWith ctx e@(Merge kvsX kvsY t) = do +typeWith ctx e@(Merge kvsX kvsY (Just t)) = do tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) ktsX <- case tKvsX of Record kts -> return kts @@ -563,10 +563,49 @@ else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) if propEqual t t' then return () - else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t')) + else Left (TypeError ctx e (InvalidHandlerOutputType kY t t')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.Map.toList ktsY) return t +typeWith ctx e@(Merge kvsX kvsY Nothing) = do + tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) + let ksX = Data.Map.keysSet ktsX + + tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) + ktsY <- case tKvsY of + Union kts -> return kts + _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) + let ksY = Data.Map.keysSet ktsY + + let diffX = Data.Set.difference ksX ksY + let diffY = Data.Set.difference ksY ksX + + if Data.Set.null diffX + then return () + else Left (TypeError ctx e (UnusedHandler diffX)) + + (kX, t) <- case Data.Map.assocs ktsX of + [] -> Left (TypeError ctx e MissingMergeType) + (kX, Pi _ _ t):_ -> return (kX, t) + (kX, tX ):_ -> Left (TypeError ctx e (HandlerNotAFunction kX tX)) + let process (kY, tY) = do + case Data.Map.lookup kY ktsX of + Nothing -> Left (TypeError ctx e (MissingHandler diffY)) + Just tX -> + case tX of + Pi _ tY' t' -> do + if propEqual tY tY' + then return () + else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) + if propEqual t t' + then return () + else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t')) + _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) + mapM_ process (Data.Map.toList ktsY) + return t typeWith ctx e@(Field r x ) = do t <- fmap Dhall.Core.normalize (typeWith ctx r) case t of @@ -632,7 +671,9 @@ | UnusedHandler (Set Text) | MissingHandler (Set Text) | HandlerInputTypeMismatch Text (Expr s X) (Expr s X) - | HandlerOutputTypeMismatch Text (Expr s X) (Expr s X) + | HandlerOutputTypeMismatch Text (Expr s X) Text (Expr s X) + | InvalidHandlerOutputType Text (Expr s X) (Expr s X) + | MissingMergeType | HandlerNotAFunction Text (Expr s X) | NotARecord Text (Expr s X) (Expr s X) | MissingField Text (Expr s X) @@ -906,12 +947,6 @@ This is not a type or kind -You specified that your function outputs a: - -↳ $txt - -... which is neither a type nor a kind: - Some common reasons why you might get this error: ● You use ❰∀❱ instead of ❰λ❱ by mistake, like this: @@ -922,6 +957,15 @@ └────────────────┘ ⇧ Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function + + +──────────────────────────────────────────────────────────────────────────────── + +You specified that your function outputs a: + +↳ $txt + +... which is neither a type nor a kind: |] where txt = Text.toStrict (Dhall.Core.pretty expr) @@ -1018,16 +1062,6 @@ └──────────────────┘ the type of a function -You tried to use the following expression as a function: - -↳ $txt0 - -... but this expression's type is: - -↳ $txt1 - -... which is not a function type - Some common reasons why you might get this error: ● You tried to add two ❰Integer❱s without a space around the ❰+❱, like this: @@ -1037,14 +1071,17 @@ │ 2+2 │ └─────┘ + The above code is parsed as: + ┌────────┐ │ 2 (+2) │ └────────┘ ⇧ The compiler thinks that this ❰2❱ is a function whose argument is ❰+2❱ + This is because the ❰+❱ symbol has two meanings: you use ❰+❱ to add two numbers, but you also can prefix ❰Integer❱ literals with a ❰+❱ to turn them into ❰Natural❱ literals (like ❰+2❱) @@ -1052,12 +1089,26 @@ To fix the code, you need to put spaces around the ❰+❱ and also prefix each ❰2❱ with a ❰+❱, like this: + ┌─────────┐ │ +2 + +2 │ └─────────┘ + You can only add ❰Natural❱ numbers, which is why you must also change each ❰2❱ to ❰+2❱ + +──────────────────────────────────────────────────────────────────────────────── + +You tried to use the following expression as a function: + +↳ $txt0 + +... but this expression's type is: + +↳ $txt1 + +... which is not a function type |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -1150,22 +1201,6 @@ └────────┘ argument that has kind ❰Type❱ -You tried to invoke the following function: - -↳ $txt0 - -... which expects an argument of type or kind: - -↳ $txt1 - -... on the following argument: - -↳ $txt2 - -... which has a different type or kind: - -↳ $txt3 - Some common reasons why you might get this error: ● You omit a function argument by mistake: @@ -1181,11 +1216,31 @@ ● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ + ┌────────────────┐ │ Natural/even 2 │ └────────────────┘ ⇧ This should be ❰+2❱ + + +──────────────────────────────────────────────────────────────────────────────── + +You tried to invoke the following function: + +↳ $txt0 + +... which expects an argument of type or kind: + +↳ $txt1 + +... on the following argument: + +↳ $txt2 + +... which has a different type or kind: + +↳ $txt3 |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -1248,18 +1303,6 @@ └─────────────┘ -You or the interpreter annotated this expression: - -↳ $txt0 - -... with this type or kind: - -↳ $txt1 - -... but the inferred type or kind of the expression is actually: - -↳ $txt2 - Some common reasons why you might get this error: ● The Haskell Dhall interpreter implicitly inserts a top-level annotation @@ -1283,6 +1326,20 @@ ... and then type-checking will fail + +──────────────────────────────────────────────────────────────────────────────── + +You or the interpreter annotated this expression: + +↳ $txt0 + +... with this type or kind: + +↳ $txt1 + +... but the inferred type or kind of the expression is actually: + +↳ $txt2 |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -1365,6 +1422,17 @@ └────────────────────────────┘ +Some common reasons why you might get this error: + +● You might be used to other programming languages that accept predicates other + than ❰Bool❱ + + For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat + them as equivalent to ❰False❱. However, the Dhall language does not permit + this + +──────────────────────────────────────────────────────────────────────────────── + Your ❰if❱ expression begins with the following predicate: ↳ $txt0 @@ -1374,15 +1442,6 @@ ↳ $txt1 ... but the predicate must instead have type ❰Bool❱ - -Some common reasons why you might get this error: - -● You might be used to other programming languages that accept predicates other - than ❰Bool❱ - - For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat - them as equivalent to ❰False❱. However, the Dhall language does not permit - this |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -1608,7 +1667,7 @@ prettyTypeMessage MissingListType = do ErrorMessages {..} where - short = "Empty lists need a type annotation" + short = "An empty list requires a type annotation" long = Builder.fromText [NeatInterpolation.text| @@ -1857,12 +1916,6 @@ └───────────────────────────┘ -Your ❰Optional❱ value had this many elements: - -↳ $txt0 - -... when an ❰Optional❱ value can only have at most one element - Some common reasons why you might get this error: ● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this: @@ -1873,6 +1926,15 @@ └────────────────────────────────────────────────────┘ ⇧ This should be ❰List❱ instead + + +──────────────────────────────────────────────────────────────────────────────── + +Your ❰Optional❱ value had this many elements: + +↳ $txt0 + +... when an ❰Optional❱ value can only have at most one element |] where txt0 = Text.toStrict (Dhall.Core.pretty n) @@ -2003,26 +2065,30 @@ This is a kind and not a term -You provided a union literal with an alternative named: - -↳ $txt0 - -... whose value is: - -↳ $txt1 - -... which is not a term - Some common reasons why you might get this error: ● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one alternative: + ┌────────────────────┐ │ < Example = Text > │ └────────────────────┘ ⇧ This could be ❰:❱ instead + + +──────────────────────────────────────────────────────────────────────────────── + +You provided a union literal with an alternative named: + +↳ $txt0 + +... whose value is: + +↳ $txt1 + +... which is not a term |] where txt0 = Text.toStrict (Dhall.Core.pretty k ) @@ -2064,14 +2130,6 @@ This is a kind and not a type -You provided a union type with an alternative named: - -↳ $txt0 - -... annotated with the following expression which is not a type: - -↳ $txt1 - Some common reasons why you might get this error: ● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one @@ -2082,6 +2140,17 @@ └─────────────────┘ ⇧ This could be ❰=❱ instead + + +──────────────────────────────────────────────────────────────────────────────── + +You provided a union type with an alternative named: + +↳ $txt0 + +... annotated with the following expression which is not a type: + +↳ $txt1 |] where txt0 = Text.toStrict (Dhall.Core.pretty k ) @@ -2203,12 +2272,6 @@ └───────────────────────────────────────────┘ -You combined two records that share the following field: - -↳ $txt0 - -... which is not allowed - Some common reasons why you might get this error: ● You tried to use ❰∧❱ to update a field's value, like this: @@ -2222,6 +2285,14 @@ Field updates are intentionally not allowed as the Dhall language discourages patch-oriented programming + +──────────────────────────────────────────────────────────────────────────────── + +You combined two records that share the following field: + +↳ $txt0 + +... which is not allowed |] where txt0 = Text.toStrict k @@ -2256,14 +2327,6 @@ Invalid: ❰handler❱ isn't a record -You provided the following handler: - -↳ $txt0 - -... which is not a record, but is actually a value of type: - -↳ $txt1 - Some common reasons why you might get this error: ● You accidentally provide an empty record type instead of an empty record when @@ -2275,6 +2338,17 @@ └──────────────────────────────────────────┘ ⇧ This should be ❰{=}❱ instead + + +──────────────────────────────────────────────────────────────────────────────── + +You provided the following handler: + +↳ $txt0 + +... which is not a record, but is actually a value of type: + +↳ $txt1 |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -2406,6 +2480,38 @@ where txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks)) +prettyTypeMessage MissingMergeType = + ErrorMessages {..} + where + short = "An empty ❰merge❱ requires a type annotation" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: A ❰merge❱ does not require a type annotation if the union has at +least one alternative, like this + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union │ + └─────────────────────────────────────────────────────────────────────┘ + + +However, you must provide a type annotation when merging an empty union: + + + ┌────────────────────────────────┐ + │ λ(a : <>) → merge {=} a : Bool │ + └────────────────────────────────┘ + ⇧ + This can be any type + + +You can provide any type at all as the annotation, since merging an empty +union can produce any type of output +|] + prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) = ErrorMessages {..} where @@ -2468,7 +2574,7 @@ txt1 = Text.toStrict (Dhall.Core.pretty expr1) txt2 = Text.toStrict (Dhall.Core.pretty expr2) -prettyTypeMessage (HandlerOutputTypeMismatch expr0 expr1 expr2) = +prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) = ErrorMessages {..} where short = "Wrong handler output type" @@ -2507,8 +2613,8 @@ ┌──────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ │ in merge handlers union : Text │ └──────────────────────────────────────────────────────────────────────┘ ⇧ @@ -2532,6 +2638,62 @@ txt1 = Text.toStrict (Dhall.Core.pretty expr1) txt2 = Text.toStrict (Dhall.Core.pretty expr2) +prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) = + ErrorMessages {..} + where + short = "Handlers should have the same output type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union │ + └─────────────────────────────────────────────────────────────────────┘ + + +... as long as the output type of each handler function is the same: + + + ┌───────────────────────────────────────────────────────────┐ + │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │ + └───────────────────────────────────────────────────────────┘ + ⇧ ⇧ + These output types both match + + +For example, the following expression is $_NOT valid: + + + ┌─────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = │ + │ { Left = λ(x : Natural) → x │ This outputs ❰Natural❱ + │ , Right = λ(x : Bool ) → x │ This outputs ❰Bool❱ + │ } │ + │ in merge handlers union │ + └─────────────────────────────────────────────────┘ + ⇧ + Invalid: The handlers in this record don't have matching outputs + + +The handler for the ❰$txt0❱ alternative has this output type: + +↳ $txt1 + +... but the handler for the ❰$txt2❱ alternative has this output type instead: + +↳ $txt3 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty key0 ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + txt2 = Text.toStrict (Dhall.Core.pretty key1 ) + txt3 = Text.toStrict (Dhall.Core.pretty expr1) prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..} where short = "Handler is not a function" @@ -2606,18 +2768,6 @@ Invalid: Not a record -You tried to access a field named: - -↳ $txt0 - -... on the following expression which is not a record: - -↳ $txt1 - -... but is actually an expression of type: - -↳ $txt2 - Some common reasons why you might get this error: ● You accidentally try to access a field of a union instead of a record, like @@ -2629,6 +2779,21 @@ └─────────────────┘ ⇧ This is a union, not a record + + +──────────────────────────────────────────────────────────────────────────────── + +You tried to access a field named: + +↳ $txt0 + +... on the following expression which is not a record: + +↳ $txt1 + +... but is actually an expression of type: + +↳ $txt2 |] where txt0 = Text.toStrict (Dhall.Core.pretty k ) @@ -2704,24 +2869,28 @@ └────────────────┘ -You provided this argument: - -↳ $txt0 - -... which does not have type ❰Text❱ but instead has type: - -↳ $txt1 - Some common reasons why you might get this error: ● You might have thought that ❰++❱ was the operator to combine two lists: + ┌────────────────────────┐ │ [1, 2, 3] ++ [4, 5, 6] │ Not valid └────────────────────────┘ + The Dhall programming language does not provide a built-in operator for combining two lists + +──────────────────────────────────────────────────────────────────────────────── + +You provided this argument: + +↳ $txt0 + +... which does not have type ❰Text❱ but instead has type: + +↳ $txt1 |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) @@ -2916,14 +3085,6 @@ └─────────┘ -You provided this argument: - -↳ $txt0 - -... which does not have type ❰Natural❱ but instead has type: - -↳ $txt1 - Some common reasons why you might get this error: ● You might have tried to use an ❰Integer❱, which is $_NOT allowed: @@ -2952,6 +3113,17 @@ ┌─────────┐ │ +2 $txt2 +2 │ Valid └─────────┘ + + +──────────────────────────────────────────────────────────────────────────────── + +You provided this argument: + +↳ $txt0 + +... which does not have type ❰Natural❱ but instead has type: + +↳ $txt1 |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0) diff --git a/tests/Examples.hs b/tests/Examples.hs --- a/tests/Examples.hs +++ b/tests/Examples.hs @@ -195,7 +195,15 @@ ] ] , Test.Tasty.testGroup "Optional" - [ Test.Tasty.testGroup "build" + [ Test.Tasty.testGroup "all" + [ _Optional_all_0 + , _Optional_all_1 + ] + , Test.Tasty.testGroup "any" + [ _Optional_any_0 + , _Optional_any_1 + ] + , Test.Tasty.testGroup "build" [ _Optional_build_0 , _Optional_build_1 ] @@ -204,6 +212,10 @@ , _Optional_concat_1 , _Optional_concat_2 ] + , Test.Tasty.testGroup "filter" + [ _Optional_filter_0 + , _Optional_filter_1 + ] , Test.Tasty.testGroup "fold" [ _Optional_fold_0 , _Optional_fold_1 @@ -218,6 +230,14 @@ , _Optional_last_1 , _Optional_last_2 ] + , Test.Tasty.testGroup "length" + [ _Optional_length_0 + , _Optional_length_1 + ] + , Test.Tasty.testGroup "null" + [ _Optional_null_0 + , _Optional_null_1 + ] , Test.Tasty.testGroup "map" [ _Optional_map_0 , _Optional_map_1 @@ -236,6 +256,18 @@ [ _Text_concat_0 , _Text_concat_1 ] + , Test.Tasty.testGroup "concatMap" + [ _Text_concatMap_0 + , _Text_concatMap_1 + ] + , Test.Tasty.testGroup "concatMapSep" + [ _Text_concatMapSep_0 + , _Text_concatMapSep_1 + ] + , Test.Tasty.testGroup "concatSep" + [ _Text_concatSep_0 + , _Text_concatSep_1 + ] ] ] @@ -961,6 +993,34 @@ |] Util.assertNormalizesTo e "0" ) +_Optional_all_0 :: TestTree +_Optional_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/all Natural Natural/even ([+3] : Optional Natural) +|] + Util.assertNormalizesTo e "False" ) + +_Optional_all_1 :: TestTree +_Optional_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/all Natural Natural/even ([] : Optional Natural) +|] + Util.assertNormalizesTo e "True" ) + +_Optional_any_0 :: TestTree +_Optional_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/any Natural Natural/even ([+2] : Optional Natural) +|] + Util.assertNormalizesTo e "True" ) + +_Optional_any_1 :: TestTree +_Optional_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/any Natural Natural/even ([] : Optional Natural) +|] + Util.assertNormalizesTo e "False" ) + _Optional_build_0 :: TestTree _Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code [NeatInterpolation.text| @@ -1008,6 +1068,20 @@ |] Util.assertNormalizesTo e "[] : Optional Integer" ) +_Optional_filter_0 :: TestTree +_Optional_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/filter Natural Natural/even ([+2] : Optional Natural) +|] + Util.assertNormalizesTo e "[+2] : Optional Natural" ) + +_Optional_filter_1 :: TestTree +_Optional_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/filter Natural Natural/odd ([+2] : Optional Natural) +|] + Util.assertNormalizesTo e "[] : Optional Natural" ) + _Optional_fold_0 :: TestTree _Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code [NeatInterpolation.text| @@ -1083,6 +1157,20 @@ |] Util.assertNormalizesTo e "[False] : Optional Bool" ) +_Optional_length_0 :: TestTree +_Optional_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/length Integer ([2] : Optional Integer) +|] + Util.assertNormalizesTo e "+1" ) + +_Optional_length_1 :: TestTree +_Optional_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/length Integer ([] : Optional Integer) +|] + Util.assertNormalizesTo e "+0" ) + _Optional_map_1 :: TestTree _Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do e <- Util.code [NeatInterpolation.text| @@ -1090,6 +1178,20 @@ |] Util.assertNormalizesTo e "[] : Optional Bool" ) +_Optional_null_0 :: TestTree +_Optional_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/null Integer ([2] : Optional Integer) +|] + Util.assertNormalizesTo e "False" ) + +_Optional_null_1 :: TestTree +_Optional_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Optional/null Integer ([] : Optional Integer) +|] + Util.assertNormalizesTo e "True" ) + _Optional_toList_0 :: TestTree _Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do e <- Util.code [NeatInterpolation.text| @@ -1132,5 +1234,47 @@ _Text_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do e <- Util.code [NeatInterpolation.text| ./Prelude/Text/concat ([] : List Text) +|] + Util.assertNormalizesTo e "\"\"" ) + +_Text_concatMap_0 :: TestTree +_Text_concatMap_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text//concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [0, 1, 2] +|] + Util.assertNormalizesTo e "\"0 1 2 \"" ) + +_Text_concatMap_1 :: TestTree +_Text_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer) +|] + Util.assertNormalizesTo e "\"\"" ) + +_Text_concatMapSep_0 :: TestTree +_Text_concatMapSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concatMapSep ", " Integer Integer/show [0, 1, 2] +|] + Util.assertNormalizesTo e "\"0, 1, 2\"" ) + +_Text_concatMapSep_1 :: TestTree +_Text_concatMapSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concatMapSep ", " Integer Integer/show ([] : List Integer) +|] + Util.assertNormalizesTo e "\"\"" ) + +_Text_concatSep_0 :: TestTree +_Text_concatSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concatSep ", " ["ABC", "DEF", "GHI"] +|] + Util.assertNormalizesTo e "\"ABC, DEF, GHI\"" ) + +_Text_concatSep_1 :: TestTree +_Text_concatSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code [NeatInterpolation.text| +./Prelude/Text/concatSep ", " ([] : List Text) |] Util.assertNormalizesTo e "\"\"" ) diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -2,6 +2,7 @@ import Normalization (normalizationTests) import Examples (exampleTests) +import Tutorial (tutorialTests) import Test.Tasty allTests :: TestTree @@ -9,6 +10,7 @@ testGroup "Dhall Tests" [ normalizationTests , exampleTests + , tutorialTests ] main :: IO ()