diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.0.1 +Version: 1.0.2 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.10.2, GHC == 8.0.1 @@ -29,12 +29,12 @@ Library Hs-Source-Dirs: src Build-Depends: - base >= 4 && < 5 , + base >= 4.8.0.0 && < 5 , ansi-wl-pprint < 0.7 , bytestring < 0.11, containers >= 0.5.0.0 && < 0.6 , - http-client >= 0.4.0 && < 0.5 , - http-client-tls >= 0.2.0 && < 0.3 , + http-client >= 0.4.30 && < 0.6 , + http-client-tls >= 0.2.0 && < 0.4 , microlens >= 0.2.0.0 && < 0.5 , microlens-mtl >= 0.1.3.1 && < 0.2 , neat-interpolation >= 0.3.2.1 && < 0.4 , diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -25,6 +25,7 @@ , normalize , subst , shift + , isNormalized -- * Pretty-printing , pretty @@ -49,7 +50,7 @@ import Data.Vector (Vector) import Filesystem.Path.CurrentOS (FilePath) import Numeric.Natural (Natural) -import Prelude hiding (FilePath) +import Prelude hiding (FilePath, succ) import qualified Control.Monad import qualified Data.Map @@ -1300,6 +1301,167 @@ e'' = bimap (\_ -> ()) (\_ -> ()) e text = "normalize (" <> Data.Text.pack (show e'') <> ")" + +-- | Quickly check if an expression is in normal form +isNormalized :: Expr s a -> Bool +isNormalized e = case shift 0 "_" e of -- `shift` is a hack to delete `Note` + Const _ -> True + Var _ -> True + Lam _ a b -> isNormalized a && isNormalized b + Pi _ a b -> isNormalized a && isNormalized b + App f a -> isNormalized f && isNormalized a && case App f a of + App (Lam _ _ _) _ -> False + + App (App ListBuild _) (App (App ListFold _) _) -> False + App (App ListFold _) (App (App ListBuild _) _) -> False + + -- fold/build fusion for `Natural` + App NaturalBuild (App NaturalFold _) -> False + App NaturalFold (App NaturalBuild _) -> False + + App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False + App NaturalBuild k0 -> isNormalized k0 && not (check0 k0) + where + check0 (Lam _ _ (Lam succ _ (Lam zero _ k))) = check1 succ zero k + check0 _ = False + + check1 succ zero (App (Var (V succ' n)) k) = + succ == succ' && n == (if succ == zero then 1 else 0) && check1 succ zero k + check1 _ zero (Var (V zero' 0)) = zero == zero' + check1 _ _ _ = False + App NaturalIsZero (NaturalLit _) -> False + App NaturalEven (NaturalLit _) -> False + App NaturalOdd (NaturalLit _) -> False + App (App ListBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0) + where + check0 (Lam _ _ (Lam cons _ (Lam nil _ k))) = check1 cons nil k + check0 _ = False + + check1 cons nil (App (Var (V cons' n)) k) = + cons == cons' && n == (if cons == nil then 1 else 0) && check1 cons nil k + check1 _ nil (Var (V nil' 0)) = nil == nil' + check1 _ _ _ = False + App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ -> + False + App (App ListLength _) (ListLit _ _) -> False + App (App ListHead _) (ListLit _ _) -> False + App (App ListLast _) (ListLit _ _) -> False + App (App ListIndexed _) (ListLit _ _) -> False + App (App ListReverse _) (ListLit _ _) -> False + App (App (App (App (App OptionalFold _) (OptionalLit _ _)) _) _) _ -> + False + _ -> True + Let _ _ _ _ -> False + Annot _ _ -> False + Bool -> True + BoolLit _ -> True + BoolAnd x y -> isNormalized x && isNormalized y && + case x of + BoolLit _ -> + case y of + BoolLit _ -> False + _ -> True + _ -> True + BoolOr x y -> isNormalized x && isNormalized y && + case x of + BoolLit _ -> + case y of + BoolLit _ -> False + _ -> True + _ -> True + BoolEQ x y -> isNormalized x && isNormalized y && + case x of + BoolLit _ -> + case y of + BoolLit _ -> False + _ -> True + _ -> True + BoolNE x y -> isNormalized x && isNormalized y && + case x of + BoolLit _ -> + case y of + BoolLit _ -> False + _ -> True + _ -> True + BoolIf b true false -> isNormalized b && case b of + BoolLit _ -> False + _ -> isNormalized true && isNormalized false + Natural -> True + NaturalLit _ -> True + NaturalFold -> True + NaturalBuild -> True + NaturalIsZero -> True + NaturalEven -> True + NaturalOdd -> True + NaturalPlus x y -> isNormalized x && isNormalized y && + case x of + NaturalLit _ -> + case y of + NaturalLit _ -> False + _ -> True + _ -> True + NaturalTimes x y -> isNormalized x && isNormalized y && + case x of + NaturalLit _ -> + case y of + NaturalLit _ -> False + _ -> True + _ -> True + Integer -> True + IntegerLit _ -> True + Double -> True + DoubleLit _ -> True + Text -> True + TextLit _ -> True + TextAppend x y -> isNormalized x && isNormalized y && + case x of + TextLit _ -> + case y of + TextLit _ -> False + _ -> True + _ -> True + List -> True + ListLit t es -> isNormalized t && all isNormalized es + ListBuild -> True + ListFold -> True + ListLength -> True + ListHead -> True + ListLast -> True + ListIndexed -> True + ListReverse -> True + Optional -> True + OptionalLit t es -> isNormalized t && all isNormalized es + OptionalFold -> True + Record kts -> all isNormalized kts + RecordLit kvs -> all isNormalized kvs + Union kts -> all isNormalized kts + UnionLit _ v kvs -> isNormalized v && all isNormalized kvs + Combine x0 y0 -> isNormalized x0 && isNormalized y0 && combine x0 y0 + where + combine x y = case x of + RecordLit _ -> case y of + RecordLit _ -> False + _ -> True + _ -> True + Merge x y t -> isNormalized x && isNormalized y && isNormalized t && + case x of + RecordLit kvsX -> + case y of + UnionLit kY _ _ -> + case Data.Map.lookup kY kvsX of + Just _ -> False + Nothing -> True + _ -> True + _ -> True + Field r x -> isNormalized r && + case r of + RecordLit kvs -> + case Data.Map.lookup x kvs of + Just _ -> False + Nothing -> True + _ -> True + Note _ e' -> isNormalized e' + Embed _ -> True {-| Utility function used to throw internal errors that should never happen (in theory) but that are not enforced by the type system diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -20,7 +20,7 @@ > ./id Bool True > > Bool - > + > > True Imported expressions may contain imports of their own, too, which will @@ -38,17 +38,17 @@ > $ dhall > ./foo > ^D - > ↳ ./foo - > ↳ ./bar - > - > Cyclic import: ./foo + > ↳ ./foo + > ↳ ./bar + > + > Cyclic import: ./foo You can also import expressions hosted on network endpoints. Just use the URL > http://host[:port]/path - The compiler expects the downloaded expressions to be in the same format + The compiler expects the downloaded expressions to be in the same format as local files, specifically UTF8-encoded source code text. For example, if our @id@ expression were hosted at @http://example.com/id@, @@ -95,7 +95,11 @@ import Dhall.Core (Expr, Path(..)) import Dhall.Parser (Parser(..), ParseError(..), Src) import Dhall.TypeCheck (X(..)) +#if MIN_VERSION_http_client(0,5,0) +import Network.HTTP.Client (HttpException(..), HttpExceptionContent(..), Manager) +#else import Network.HTTP.Client (HttpException(..), Manager) +#endif import Prelude hiding (FilePath) import Text.Trifecta (Result(..)) import Text.Trifecta.Delta (Delta(..)) @@ -191,7 +195,29 @@ instance Exception PrettyHttpException +#if MIN_VERSION_http_client(0,5,0) instance Show PrettyHttpException where + show (PrettyHttpException (InvalidUrlException _ r)) = + "\n" + <> "\ESC[1;31mError\ESC[0m: Invalid URL\n" + <> "\n" + <> "↳ " <> show r + show (PrettyHttpException (HttpExceptionRequest _ e)) = case e of + ConnectionFailure e' -> + "\n" + <> "\ESC[1;31mError\ESC[0m: Wrong host\n" + <> "\n" + <> "↳ " <> show e' + InvalidDestinationHost host -> + "\n" + <> "\ESC[1;31mError\ESC[0m: Invalid host name\n" + <> "\n" + <> "↳ " <> show host + ResponseTimeout -> + "\ESC[1;31mError\ESC[0m: The host took too long to respond\n" + e' -> "\n" <> show e' +#else +instance Show PrettyHttpException where show (PrettyHttpException e) = case e of FailedConnectionException2 _ _ _ e' -> "\n" @@ -206,7 +232,8 @@ ResponseTimeout -> "\ESC[1;31mError\ESC[0m: The host took too long to respond\n" e' -> "\n" - <> show e' + <> show e' +#endif -- | Exception thrown when an imported file is missing data MissingFile = MissingFile @@ -244,7 +271,11 @@ Just m -> return m Nothing -> do let settings = HTTP.tlsManagerSettings +#if MIN_VERSION_http_client(0,5,0) + { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro 1000000 } -- 1 second +#else { HTTP.managerResponseTimeout = Just 1000000 } -- 1 second +#endif m <- liftIO (HTTP.newManager settings) zoom manager (State.put (Just m)) return m @@ -291,7 +322,7 @@ url' = parentURL (removeAtFromURL url) Nothing -> case Filesystem.stripPrefix "." path of Just path' -> combine url path' - Nothing -> + Nothing -> -- This `last` is safe because the lexer constrains all -- URLs to be non-empty. I couldn't find a simple and safe -- equivalent in the `text` API @@ -372,7 +403,11 @@ request <- HTTP.parseUrlThrow (Text.unpack url) let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) - handler err@(HTTP.StatusCodeException _ _ _) = do +#if MIN_VERSION_http_client(0,5,0) + handler err@(HttpExceptionRequest _ (StatusCodeException _ _)) = do +#else + handler err@(StatusCodeException _ _ _) = do +#endif let request' = request { HTTP.path = HTTP.path request <> "/@" } -- If the fallback fails, reuse the original exception to avoid user -- confusion diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -26,6 +26,7 @@ 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 (Const(..), Expr(..), Path(..), Var(..)) @@ -50,6 +51,7 @@ import qualified Data.Sequence import qualified Data.Text import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding import qualified Data.Vector import qualified Dhall.Core @@ -187,6 +189,60 @@ _ <- Text.Parser.Token.symbol string return () +stringLiteral :: Parser Builder +stringLiteral = Text.Parser.Token.stringLiteral <|> doubleSingleQuoteString + +doubleSingleQuoteString :: Parser Builder +doubleSingleQuoteString = do + builder <- Text.Parser.Token.token p0 + return (process builder) + where + process = + Data.Text.Lazy.Builder.fromLazyText + . Data.Text.Lazy.unlines + . trim + . Data.Text.Lazy.lines + . Data.Text.Lazy.Builder.toLazyText + + trim lines_ = map (Data.Text.Lazy.drop shortestIndent) lines_ + where + isEmpty = Data.Text.Lazy.all Data.Char.isSpace + + nonEmptyLines = filter (not . isEmpty) lines_ + + indentLength line = + Data.Text.Lazy.length + (Data.Text.Lazy.takeWhile Data.Char.isSpace line) + + shortestIndent = case nonEmptyLines of + [] -> 0 + _ -> minimum (map indentLength nonEmptyLines) + + p0 = do + Text.Parser.Char.string "''" + p1 + + p1 = p2 <|> p3 <|> p4 <|> p5 + + p2 = do + Text.Parser.Char.text "'''" + s1 <- p1 + return ("''" <> s1) + + p3 = do + Text.Parser.Char.text "''" + return "" + + p4 = do + s0 <- Text.Parser.Char.text "'" + s1 <- p1 + return (Data.Text.Lazy.Builder.fromText s0 <> s1) + + p5 = do + s0 <- some (Text.Trifecta.satisfy (/= '\'')) + s1 <- p1 + return (Data.Text.Lazy.Builder.fromString s0 <> s1) + lambda :: Parser () lambda = symbol "\\" <|> symbol "λ" @@ -508,7 +564,7 @@ return (DoubleLit (sign a)) exprF27 = do - a <- Text.Parser.Token.stringLiteral + a <- stringLiteral return (TextLit a) exprF28 = record "record type" diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -26,6 +26,9 @@ -- * Functions -- $functions + -- * Strings + -- $strings + -- * Combine -- $combine @@ -62,7 +65,7 @@ -- *** @(==)@ -- $equal - -- *** @(/=)@ + -- *** @(!=)@ -- $unequal -- *** @if@\/@then@\/@else@ @@ -139,6 +142,9 @@ -- * Conclusion -- $conclusion + + -- * Frequently Asked Questions (FAQ) + -- $faq ) where import Data.Vector (Vector) @@ -251,7 +257,7 @@ -- > -- > import Dhall -- > --- > data Person = Person { age :: Natural, name :: Text } +-- > data Person = Person { age :: Integer, name :: Text } -- > deriving (Generic, Show) -- > -- > instance Interpret Person @@ -585,7 +591,7 @@ -- -- > $ cat > makeBools -- > \(n : Bool) -> --- > [ n && True, n && False, n || True, n || False ] : List Bool +-- > [ n && True, n && False, n || True, n || False ] : List Bool -- > -- -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB) @@ -594,12 +600,12 @@ -- -- > $ cat > makeBools -- > λ(n : Bool) → --- > [ n && True, n && False, n || True, n || False ] : List Bool +-- > [ n && True, n && False, n || True, n || False ] : List Bool -- > -- --- You can read either one as a function of one argument named @n@ that has type +-- You can read this as a function of one argument named @n@ that has type -- @Bool@. This function returns a @List@ of @Bool@s. Each element of the --- @List@ depends on the input argument. +-- @List@ depends on the input argument named @n@. -- -- The (ASCII) syntax for anonymous functions resembles the syntax for anonymous -- functions in Haskell. The only difference is that Dhall requires you to @@ -710,6 +716,41 @@ -- __Exercise__: Use the @dhall@ compiler to apply your function to a sample -- record +-- $strings +-- Dhall supports ordinary string literals with Haskell-style escaping rules: +-- +-- > dhall +-- > "Hello, \"world\"!" +-- > +-- > Text +-- > +-- > "Hello, \"world\"!" +-- +-- ... and Dhall also supports Nix-style multi-line string literals: +-- +-- > dhall +-- > '' +-- > #!/bin/bash +-- > +-- > echo "Hi!" +-- > '' +-- > +-- > Text +-- > +-- > "\n#!/bin/bash\n\necho \"Hi!\"\n" +-- +-- These \"double single quote strings\" ignore all special characters, with one +-- exception: if you want to include a @''@ in the string, you will need to +-- escape it with a preceding @'@ (i.e. use @'''@ to insert @''@ into the final +-- string). +-- +-- These strings also strip leading whitespace using the same rules as Nix. +-- Specifically: \"it strips from each line a number of spaces equal to the +-- 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. + -- $combine -- -- You can combine two records, using the @(/\\)@ operator or the @@ -1222,7 +1263,7 @@ -- shuffled around but not used in any meaningful way until they have been -- loaded into Haskell. -- --- Second, the equality @(==)@ and inequality @(/=)@ operators only work on +-- Second, the equality @(==)@ and inequality @(!=)@ operators only work on -- @Bool@s. You cannot test any other types of values for equality. -- $builtinOverview @@ -1534,7 +1575,7 @@ -- -- Rules: -- --- > Natural/odd (x + y) = Natural/odd x /= Natural/odd y +-- > Natural/odd (x + y) = Natural/odd x != Natural/odd y -- > -- > Natural/odd +0 = False -- > @@ -1984,7 +2025,7 @@ -- > False -- -- Some functions in the Prelude just re-export built-in functions for --- consistency and documentation, such as @Prelude/Natural/even@, which +-- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- -- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even @@ -2088,3 +2129,38 @@ -- If you would like to contribute to the Dhall project you can try to port Dhall -- to other languages besides Haskell so that Dhall configuration files can be -- read into those languages, too. + +-- $faq +-- +-- * Why do lists require a type annotation? +-- +-- Dhall requires type annotations on lists in order to gracefully deal with +-- empty lists. Without a type annotation the compiler would not be able to +-- infer the type of an empty list expression: +-- +-- > [] +-- +-- Unlike Haskell, Dhall cannot infer a polymorphic type for the empty list +-- because Dhall represents polymorphic values as functions of types, like this: +-- +-- > λ(a : Type) → [] : List a +-- +-- If the compiler treated an empty list literal as syntactic short-hand for +-- the above polymorphic function then you'd get the unexpected behavior where +-- a list literal is a function if the list has 0 elements but not a function +-- otherwise. +-- +-- * Why do lists require a type annotation when using `input`, like this: +-- +-- > >>> input (list bool) "[True, False] : List Bool" +-- +-- The type annotation on a list is not a real type annotation. Instead, the +-- annotation on a list is part of the mandatory syntax for lists. This is why +-- you get a parse error instead of a type error if you omit the annotation: +-- +-- > dhall +-- > [1, 2] +-- > (stdin):2:1: error: unexpected +-- > EOF, expected: ":" +-- > +-- > ^ diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -977,6 +977,37 @@ ↳ $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: + + + ┌─────┐ + │ 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❱) + + 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❱ |] where txt0 = Text.toStrict (Dhall.Core.pretty expr0)