dhall 1.0.1 → 1.0.2

raw patch · 6 files changed

+384/−24 lines, 6 filesdep ~basedep ~http-clientdep ~http-client-tlsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, http-client, http-client-tls

API changes (from Hackage documentation)

Files

• dhall.cabal +4/−4
• src/Dhall/Core.hs +163/−1
• src/Dhall/Import.hs +44/−9
• src/Dhall/Parser.hs +57/−1
• src/Dhall/Tutorial.hs +85/−9
• src/Dhall/TypeCheck.hs +31/−0

@@ -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 ,

@@ -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

@@ -20,7 +20,7 @@     > ./id Bool True     > <Ctrl-D>     > 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

@@ -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"

@@ -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 -- > <Ctrl-D> -- -- ... 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 -- > <Ctrl-D> ----- 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\"!"+-- > <Ctrl-D>+-- > Text+-- >+-- > "Hello, \"world\"!"+--+-- ... and Dhall also supports Nix-style multi-line string literals:+--+-- > dhall+-- > ''+-- >     #!/bin/bash+-- >     +-- >     echo "Hi!"+-- > ''+-- > <Ctrl-D>+-- > 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: ":"+-- >     <EOF> +-- >     ^    

@@ -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)