dhall 1.3.0 → 1.4.0
raw patch · 9 files changed
+898/−238 lines, 9 filesdep +case-insensitivedep ~trifectaPVP ok
version bump matches the API change (PVP)
Dependencies added: case-insensitive
Dependency ranges changed: trifecta
API changes (from Hackage documentation)
+ Dhall.Import: instance GHC.Exception.Exception Dhall.Import.InternalError
+ Dhall.Import: instance GHC.Show.Show Dhall.Import.InternalError
+ Dhall.TypeCheck: InvalidHandlerOutputType :: Text -> (Expr s X) -> (Expr s X) -> TypeMessage s
+ Dhall.TypeCheck: MissingMergeType :: TypeMessage s
- Dhall.Core: Merge :: (Expr s a) -> (Expr s a) -> (Expr s a) -> Expr s a
+ Dhall.Core: Merge :: (Expr s a) -> (Expr s a) -> (Maybe (Expr s a)) -> Expr s a
- Dhall.Core: URL :: Text -> PathType
+ Dhall.Core: URL :: Text -> (Maybe PathType) -> PathType
- Dhall.TypeCheck: HandlerOutputTypeMismatch :: Text -> (Expr s X) -> (Expr s X) -> TypeMessage s
+ Dhall.TypeCheck: HandlerOutputTypeMismatch :: Text -> (Expr s X) -> Text -> (Expr s X) -> TypeMessage s
Files
- CHANGELOG.md +30/−0
- dhall.cabal +4/−3
- src/Dhall/Core.hs +25/−19
- src/Dhall/Import.hs +127/−19
- src/Dhall/Parser.hs +163/−39
- src/Dhall/Tutorial.hs +104/−31
- src/Dhall/TypeCheck.hs +298/−126
- tests/Examples.hs +145/−1
- tests/Tests.hs +2/−0
CHANGELOG.md view
@@ -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:
dhall.cabal view
@@ -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:
src/Dhall/Core.hs view
@@ -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"
src/Dhall/Import.hs view
@@ -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)
src/Dhall/Parser.hs view
@@ -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
src/Dhall/Tutorial.hs view
@@ -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: ----- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not> -- -- 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}"+-- > <Ctrl-D>+-- > 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 -- > <Ctrl-D> -- > 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] -- > <Ctrl-D> -- > ∀(f : Integer → Integer) → List Integer@@ -1209,17 +1238,61 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: ----- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate>+-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/replicate> -- -- 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: ----- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude>+-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/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@@ -1986,12 +2059,12 @@ -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: ----- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not> -- -- 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 -- > <Ctrl-D> -- > 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 -- > <Ctrl-D> -- > 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: ----- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude>+-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial
src/Dhall/TypeCheck.hs view
@@ -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)
tests/Examples.hs view
@@ -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 "\"\"" )
tests/Tests.hs view
@@ -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 ()