diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,72 @@ +1.20.0 + +* Supports version 5.0.0 of the language standard + * See: https://github.com/dhall-lang/dhall-lang/releases/tag/v5.0.0 +* BREAKING CHANGE TO THE LANGUAGE: Implement standardized support for multi-line + literals + * This updates the multi-line support to match the standard + * This is a breaking change because empty lines within the multi-line + literal now require leading whitespace whereas previously they did not + * This is also a breaking change because now a newline is required after + the opening `''` quotes whereas previously it was not required + * If you use `dhall format` then your multi-line literals already have the + necessary leading whitespace +* BREAKING CHANGE TO THE LANGUAGE: `constructors x = x` + * Now the `constructors` keyword behaves like an identity function, since + constructors can already be accessed as fields off the original union + type. + * This is a breaking change since any record of terms that contains a + `constructors` field will now be a forbidden mixed record of types and + terms. + * This is also a breaking change if you annotated the type of what used to + be a `constructors` record. + * `dhall lint` will now remove the obsolete `constructors` keyword for you + * See: https://github.com/dhall-lang/dhall-haskell/pull/693 + * See: https://github.com/dhall-lang/dhall-haskell/pull/701 +* BREAKING CHANGE TO THE API: Restore `Parent` constructor for `Local` type + * This more closely matches the standard and also enables `dhall format` to + produce a leading `../` for imports instead of `./../` + * See: https://github.com/dhall-lang/dhall-haskell/pull/718 +* BUG FIX: Fix type-checking bug for unions + * The first fix was that the inferred type was wrong for unions where + alternatives were types or kinds + * The second fix was that unions that mixed terms/types/kinds were not + properly rejected + * See: https://github.com/dhall-lang/dhall-haskell/pull/763 +* BUG FIX: Change how `dhall repl` handles prior definitions + * This changes the REPL to handle previous bindings as if they were + defined using a large `let` expression instead of adding them to the + context + * This fixes some type-checking false negatives + * See: https://github.com/dhall-lang/dhall-haskell/pull/729 +* Feature: Autocomplete for `dhall repl` + * You can now auto-complete record fields, union constructors, and + identifiers that are in scope + * See: https://github.com/dhall-lang/dhall-haskell/pull/727 +* Feature: GHCJS support + * `dhall` can now be built using GHCJS, although some features are still + not supported for GHCJS, such as: + * Semantic integrity checks + * Custom HTTP headers + * Also, HTTP imports only work for URLs that support CORS + * See: https://github.com/dhall-lang/dhall-haskell/pull/739 +* Feature: Add support for records of records of types + * You can now nest records of types + * See: https://github.com/dhall-lang/dhall-haskell/pull/700 +* Feature: Add `:quit` command for `dhall repl` + * See: https://github.com/dhall-lang/dhall-haskell/pull/719 +* Feature: Add `--json` flag for `dhall {encode,decode}` + * You can now produce/consume CBOR expressions via JSON instead of binary + * See: https://github.com/dhall-lang/dhall-haskell/pull/717 +* Feature: Add decoding logic for `as Text` + * You can now preserve the `as Text` qualifier on imports when serializing + them + * See: https://github.com/dhall-lang/dhall-haskell/pull/712 +* Prenormalize substituted expressions + * This is a performance improvement that reduces the time and memory + consumption when normalizing expressions + * See: https://github.com/dhall-lang/dhall-haskell/pull/765 + 1.19.1 diff --git a/benchmark/map/Main.hs b/benchmark/map/Main.hs new file mode 100644 --- /dev/null +++ b/benchmark/map/Main.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE TypeApplications #-} + +module Main where + +import Criterion.Main (defaultMain, bgroup, bench, whnf, nfIO) + +import qualified Criterion.Main as Criterion +import qualified Dhall.Map as Map + +testData :: Integer -> Map.Map Integer Integer +testData i = foldr (\j -> Map.insert j j) mempty [1 .. i] + +benchOrderedTraversal :: String -> Map.Map Integer Integer -> Criterion.Benchmark +benchOrderedTraversal dataLabel mapData = + bgroup ("Ordered Traversals: " <> dataLabel) + [ bench "traverseWithKey" $ + whnf (Map.traverseWithKey (\_ i -> pure @Maybe $ i ^ i)) mapData + , bench "traverseWithKey_" $ + whnf (Map.traverseWithKey_ (\_ i -> pure @Maybe (i ^ i) *> pure ())) mapData + ] + +benchUnorderedTraversal :: String -> Map.Map Integer Integer -> Criterion.Benchmark +benchUnorderedTraversal dataLabel mapData = + bgroup ("Unordered Traversals: " <> dataLabel) + [ bench "unorderedTraverseWithKey_" $ + whnf (Map.unorderedTraverseWithKey_ (\_ i -> pure @Maybe (i ^ i) *> pure ())) mapData + ] + +main :: IO () +main = do + let !smallMap = testData 10 + !mediumMap = testData 1000 + !largeMap = testData 100000 + defaultMain + [ benchOrderedTraversal "small" smallMap + , benchUnorderedTraversal "small" smallMap + + , benchOrderedTraversal "medium" mediumMap + , benchUnorderedTraversal "medium" mediumMap + + , benchOrderedTraversal "large" largeMap + , benchUnorderedTraversal "large" largeMap + ] diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.19.1 +Version: 1.20.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -39,6 +39,7 @@ tests/normalization/success/haskell-tutorial/combineTypes/*.dhall tests/normalization/success/haskell-tutorial/prefer/*.dhall tests/normalization/success/haskell-tutorial/projection/*.dhall + tests/normalization/success/multiline/*.dhall tests/normalization/success/prelude/Bool/and/*.dhall tests/normalization/success/prelude/Bool/and/*.dhall tests/normalization/success/prelude/Bool/build/*.dhall @@ -296,10 +297,13 @@ Hs-Source-Dirs: src Build-Depends: base >= 4.8.2.0 && < 5 , + aeson >= 1.0.0.0 && < 1.5 , + aeson-pretty < 0.9 , ansi-terminal >= 0.6.3.1 && < 0.9 , bytestring < 0.11, case-insensitive < 1.3 , cborg >= 0.2.0.0 && < 0.3 , + cborg-json < 0.3 , containers >= 0.5.0.0 && < 0.7 , contravariant < 1.6 , cryptonite >= 0.23 && < 1.0 , @@ -335,6 +339,8 @@ Build-Depends: semigroups == 0.18.* Build-Depends: transformers == 0.4.2.* Build-Depends: fail == 4.9.* + if impl(ghcjs) + Build-Depends: ghcjs-xhr Exposed-Modules: Dhall, @@ -381,19 +387,19 @@ Test-Suite tasty Type: exitcode-stdio-1.0 Hs-Source-Dirs: tests - Main-Is: Tests.hs + Main-Is: Dhall/Test/Main.hs GHC-Options: -Wall Other-Modules: - Format - Import - Lint - Normalization - Parser - QuickCheck - Regression - Tutorial - TypeCheck - Util + Dhall.Test.Format + Dhall.Test.Import + Dhall.Test.Lint + Dhall.Test.Normalization + Dhall.Test.Parser + Dhall.Test.QuickCheck + Dhall.Test.Regression + Dhall.Test.Tutorial + Dhall.Test.TypeCheck + Dhall.Test.Util Build-Depends: base >= 4 && < 5 , containers , @@ -405,7 +411,7 @@ QuickCheck >= 2.10 && < 2.13, quickcheck-instances >= 0.3.12 && < 0.4 , serialise , - tasty >= 0.11.2 && < 1.2 , + tasty >= 0.11.2 && < 1.3 , tasty-hunit >= 0.9.2 && < 0.11, tasty-quickcheck >= 0.9.2 && < 0.11, text >= 0.11.1.0 && < 1.3 , @@ -458,7 +464,6 @@ dhall Default-Language: Haskell2010 - Benchmark dhall-command Type: exitcode-stdio-1.0 Main-Is: Main.hs @@ -468,3 +473,14 @@ dhall Default-Language: Haskell2010 ghc-options: -rtsopts -O2 + +Benchmark map-operations + Type: exitcode-stdio-1.0 + Main-Is: Main.hs + Hs-Source-Dirs: benchmark/map + Build-Depends: + base >= 4 && < 5 , + criterion >= 1.1 && < 1.6, + dhall + Default-Language: Haskell2010 +-- ghc-options: -rtsopts -O2 diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -671,7 +671,7 @@ expectedOut = App Optional expectedIn {-| Decode a `Seq` - - + >>> input (sequence natural) "[1, 2, 3]" fromList [1,2,3] -} diff --git a/src/Dhall/Binary.hs b/src/Dhall/Binary.hs --- a/src/Dhall/Binary.hs +++ b/src/Dhall/Binary.hs @@ -39,6 +39,8 @@ , URL(..) , Var(..) ) + +import Data.ByteArray.Encoding (Base(..)) import Data.Foldable (toList) import Data.List.NonEmpty (NonEmpty(..)) import Data.Monoid ((<>)) @@ -48,8 +50,12 @@ import GHC.Float (double2Float, float2Double) import Codec.CBOR.Magic (floatToWord16, wordToFloat16) +import qualified Crypto.Hash +import qualified Data.ByteArray.Encoding +import qualified Data.ByteString import qualified Data.Sequence import qualified Data.Text +import qualified Data.Text.Encoding import qualified Dhall.Map import qualified Dhall.Set import qualified Options.Applicative @@ -386,13 +392,21 @@ case importType of Remote (URL { scheme = scheme₀, ..}) -> TList - ( [ TInt 24, TInt scheme₁, TString authority ] + ( prefix + ++ [ TInt scheme₁, using, TString authority ] ++ map TString (reverse components) ++ [ TString file ] ++ (case query of Nothing -> [ TNull ]; Just q -> [ TString q ]) ++ (case fragment of Nothing -> [ TNull ]; Just f -> [ TString f ]) ) where + using = case headers of + Nothing -> + TNull + Just h -> + importToTerm + (Import { importHashed = h, importMode = Code }) + scheme₁ = case scheme₀ of HTTP -> 0 HTTPS -> 1 @@ -402,7 +416,8 @@ Local prefix₀ path -> TList - ( [ TInt 24, TInt prefix₁ ] + ( prefix + ++ [ TInt prefix₁ ] ++ map TString components₁ ++ [ TString file ] ) @@ -411,18 +426,31 @@ Directory {..} = directory - (prefix₁, components₁) = case (prefix₀, reverse components) of - (Absolute, rest ) -> (2, rest) - (Here , ".." : rest) -> (4, rest) - (Here , rest ) -> (3, rest) - (Home , rest ) -> (5, rest) + prefix₁ = case prefix₀ of + Absolute -> 2 + Here -> 3 + Parent -> 4 + Home -> 5 + components₁ = reverse components + Env x -> - TList [ TInt 24, TInt 6, TString x ] + TList (prefix ++ [ TInt 6, TString x ]) Missing -> - TList [ TInt 24, TInt 7 ] + TList (prefix ++ [ TInt 7 ]) where + prefix = [ TInt 24, h, m ] + where + h = case hash of + Nothing -> + TNull + Just digest -> + TList + [ TString "sha256", TString (Data.Text.pack (show digest)) ] + + m = TInt (case importMode of Code -> 0; RawText -> 1) + Import {..} = import_ ImportHashed {..} = importHashed @@ -661,7 +689,28 @@ (xys, z) <- process xs return (TextLit (Chunks xys z)) -decode (TList (TInt 24 : TInt n : xs)) = do +decode (TList (TInt 24 : h : TInt mode : TInt n : xs)) = do + hash <- case h of + TNull -> do + return Nothing + + TList [ TString "sha256", TString base16Text ] -> do + let base16Bytes = Data.Text.Encoding.encodeUtf8 base16Text + digestBytes <- case Data.ByteArray.Encoding.convertFromBase Base16 base16Bytes of + Left _ -> empty + Right digestBytes -> return (digestBytes :: Data.ByteString.ByteString) + + digest <- Crypto.Hash.digestFromByteString digestBytes + return (Just digest) + + _ -> do + empty + + importMode <- case mode of + 0 -> return Code + 1 -> return RawText + _ -> empty + let remote scheme = do let process [ TString file, q, f ] = do query <- case q of @@ -679,16 +728,21 @@ process _ = do empty - (authority, paths, file, query, fragment) <- case xs of - TString authority : ys -> do + (headers, authority, paths, file, query, fragment) <- case xs of + headers₀ : TString authority : ys -> do + headers₁ <- case headers₀ of + TNull -> return Nothing + _ -> do + Embed (Import { importHashed = headers }) <- decode headers₀ + return (Just headers) (paths, file, query, fragment) <- process ys - return (authority, paths, file, query, fragment) - _ -> empty + return (headers₁, authority, paths, file, query, fragment) + _ -> do + empty let components = reverse paths let directory = Directory {..} let path = File {..} - let headers = Nothing return (Remote (URL {..})) @@ -703,11 +757,7 @@ (paths, file) <- process xs - let finalPaths = case n of - 4 -> ".." : paths - _ -> paths - - let components = reverse finalPaths + let components = reverse paths let directory = Directory {..} return (Local prefix (File {..})) @@ -724,15 +774,14 @@ 1 -> remote HTTPS 2 -> local Absolute 3 -> local Here - 4 -> local Here + 4 -> local Parent 5 -> local Home 6 -> env 7 -> missing _ -> empty - let hash = Nothing let importHashed = ImportHashed {..} - let importMode = Code + return (Embed (Import {..})) decode (TList (TInt 25 : xs)) = do let process (TString x : _A₁ : a₁ : ls₁) = do diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -157,6 +157,8 @@ -- ^ Absolute path | Here -- ^ Path relative to @.@ + | Parent + -- ^ Path relative to @..@ | Home -- ^ Path relative to @~@ deriving (Eq, Generic, Ord, Show) @@ -164,6 +166,7 @@ instance Pretty FilePrefix where pretty Absolute = "" pretty Here = "." + pretty Parent = ".." pretty Home = "~" data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show) @@ -188,12 +191,21 @@ | Missing deriving (Eq, Generic, Ord, Show) +parent :: File +parent = File { directory = Directory { components = [ ".." ] }, file = "" } + instance Semigroup ImportType where Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁) Remote (URL { path = path₀, ..}) <> Local Here path₁ = Remote (URL { path = path₀ <> path₁, ..}) + Local prefix file₀ <> Local Parent file₁ = + Local prefix (file₀ <> parent <> file₁) + + Remote (URL { path = path₀, .. }) <> Local Parent path₁ = + Remote (URL { path = path₀ <> parent <> path₁, .. }) + import₀ <> Remote (URL { headers = headers₀, .. }) = Remote (URL { headers = headers₁, .. }) where @@ -1575,14 +1587,16 @@ Just e1 -> loop e1 Nothing -> do f' <- loop f + a' <- loop a case f' of - Lam x _A b -> loop b'' - where - a' = shift 1 (V x 0) a - b' = subst (V x 0) a' b - b'' = shift (-1) (V x 0) b' + Lam x _A b₀ -> do + + let a₂ = shift 1 (V x 0) a' + let b₁ = subst (V x 0) a₂ b₀ + let b₂ = shift (-1) (V x 0) b₁ + + loop b₂ _ -> do - a' <- loop a case App f' a' of -- build/fold fusion for `List` App (App ListBuild _) (App (App ListFold _) e') -> loop e' @@ -1597,8 +1611,8 @@ t' <- loop t if boundedType t' then strict else lazy where - strict = strictLoop n0 - lazy = loop ( lazyLoop n0) + strict = strictLoop (fromIntegral n0 :: Integer) + lazy = loop ( lazyLoop (fromIntegral n0 :: Integer)) strictLoop !0 = loop zero strictLoop !n = App succ' <$> strictLoop (n - 1) >>= loop @@ -1702,15 +1716,18 @@ case res2 of Nothing -> pure (App f' a') Just app' -> loop app' - Let (Binding x _ a₀ :| ls₀) b₀ -> loop b₂ - where - rest = case ls₀ of - [] -> b₀ - l₁ : ls₁ -> Let (l₁ :| ls₁) b₀ + Let (Binding x _ a₀ :| ls₀) b₀ -> do + a₁ <- loop a₀ - a₁ = shift 1 (V x 0) a₀ - b₁ = subst (V x 0) a₁ rest - b₂ = shift (-1) (V x 0) b₁ + rest <- case ls₀ of + [] -> loop b₀ + l₁ : ls₁ -> loop (Let (l₁ :| ls₁) b₀) + + let a₂ = shift 1 (V x 0) a₁ + let b₁ = subst (V x 0) a₂ rest + let b₂ = shift (-1) (V x 0) b₁ + + loop b₂ Annot x _ -> loop x Bool -> pure Bool BoolLit b -> pure (BoolLit b) @@ -1897,14 +1914,8 @@ Constructors t -> do t' <- loop t case t' of - Union kts -> pure (RecordLit kvs) - where - kvs = Dhall.Map.mapWithKey adapt kts - - adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest) - where - rest = Dhall.Map.delete k kts - _ -> pure (Constructors t') + u@(Union _) -> pure u + _ -> pure $ Constructors t' Field r x -> do r' <- loop r case r' of diff --git a/src/Dhall/Diff.hs b/src/Dhall/Diff.hs --- a/src/Dhall/Diff.hs +++ b/src/Dhall/Diff.hs @@ -11,7 +11,9 @@ module Dhall.Diff ( -- * Diff - diffNormalized + Diff (..) + , diffExpression + , diffNormalized , Dhall.Diff.diff ) where @@ -362,7 +364,7 @@ | allDifferent parts = difference listSkeleton listSkeleton | otherwise = bracketed (foldMap diffPart parts) where - allDifferent = not . any isBoth + allDifferent = any (not . isBoth) -- Sections of the list that are only in left, only in right, or in both parts = diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -455,6 +455,10 @@ Absolute -> do return "/" + Parent -> do + pwd <- Directory.getCurrentDirectory + return (FilePath.takeDirectory pwd) + Here -> do Directory.getCurrentDirectory diff --git a/src/Dhall/Import/HTTP.hs b/src/Dhall/Import/HTTP.hs --- a/src/Dhall/Import/HTTP.hs +++ b/src/Dhall/Import/HTTP.hs @@ -13,14 +13,19 @@ import Data.Semigroup ((<>)) import Lens.Family.State.Strict (zoom) -import qualified Control.Exception import qualified Control.Monad.Trans.State.Strict as State import qualified Data.Text as Text -import qualified Data.Text.Lazy -import qualified Data.Text.Lazy.Encoding import Dhall.Import.Types +#ifdef __GHCJS__ +import qualified JavaScript.XHR +#else +import qualified Control.Exception +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Encoding +#endif + #if MIN_VERSION_http_client(0,5,0) import Network.HTTP.Client (HttpException(..), HttpExceptionContent(..), Manager) @@ -111,6 +116,18 @@ :: String -> Maybe [(CI ByteString, ByteString)] -> StateT (Status m) IO (String, Text.Text) +#ifdef __GHCJS__ +fetchFromHttpUrl url Nothing = do + (statusCode, body) <- liftIO (JavaScript.XHR.get (Text.pack url)) + + case statusCode of + 200 -> return () + _ -> fail (url <> " returned a non-200 status code: " <> show statusCode) + + return (url, body) +fetchFromHttpUrl _ _ = do + fail "Dhall does not yet support custom headers when built using GHCJS" +#else fetchFromHttpUrl url mheaders = do m <- needManager @@ -134,3 +151,4 @@ case Data.Text.Lazy.Encoding.decodeUtf8' bytes of Left err -> liftIO (Control.Exception.throwIO err) Right text -> return (url, Data.Text.Lazy.toStrict text) +#endif diff --git a/src/Dhall/Lint.hs b/src/Dhall/Lint.hs --- a/src/Dhall/Lint.hs +++ b/src/Dhall/Lint.hs @@ -19,6 +19,7 @@ * removes unused @let@ bindings * consolidates nested @let@ bindings to use a multiple-@let@ binding * switches legacy @List@-like @Optional@ literals to use @Some@ / @None@ instead + * removes the `constructors` keyword -} lint :: Expr s Import -> Expr t Import lint expression = loop (Dhall.Core.denote expression) @@ -234,9 +235,7 @@ b' = loop b c' = fmap loop c loop (Constructors a) = - Constructors a' - where - a' = loop a + loop a loop (Field a b) = Field a' b where diff --git a/src/Dhall/Main.hs b/src/Dhall/Main.hs --- a/src/Dhall/Main.hs +++ b/src/Dhall/Main.hs @@ -36,10 +36,16 @@ import System.Exit (exitFailure) import System.IO (Handle) +import qualified Codec.CBOR.JSON +import qualified Codec.CBOR.Read +import qualified Codec.CBOR.Write import qualified Codec.Serialise import qualified Control.Exception import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.Aeson +import qualified Data.Aeson.Encode.Pretty import qualified Data.ByteString.Lazy +import qualified Data.ByteString.Lazy.Char8 import qualified Data.Text import qualified Data.Text.IO import qualified Data.Text.Prettyprint.Doc as Pretty @@ -87,8 +93,8 @@ | Hash | Diff { expr1 :: Text, expr2 :: Text } | Lint { inplace :: Maybe FilePath } - | Encode - | Decode + | Encode { json :: Bool } + | Decode { json :: Bool } -- | `Parser` for the `Options` type parseOptions :: Parser Options @@ -164,11 +170,11 @@ <|> subcommand "encode" "Encode a Dhall expression to binary" - (pure Encode) + (Encode <$> parseJSONFlag) <|> subcommand "decode" "Decode a Dhall expression from binary" - (pure Decode) + (Decode <$> parseJSONFlag) <|> (Default <$> parseAnnotate) where argument = @@ -194,6 +200,12 @@ <> Options.Applicative.metavar "FILE" ) + parseJSONFlag = + Options.Applicative.switch + ( Options.Applicative.long "json" + <> Options.Applicative.help "Use JSON representation of CBOR" + ) + throws :: Exception e => Either e a -> IO a throws (Left e) = Control.Exception.throwIO e throws (Right a) = return a @@ -370,20 +382,42 @@ renderDoc System.IO.stdout doc - Encode -> do + Encode {..} -> do expression <- getExpression - let term = - Dhall.Binary.encodeWithVersion standardVersion expression + let term = Dhall.Binary.encodeWithVersion standardVersion expression let bytes = Codec.Serialise.serialise term - Data.ByteString.Lazy.putStr bytes + if json + then do + let decoder = Codec.CBOR.JSON.decodeValue False - Decode -> do + (_, value) <- throws (Codec.CBOR.Read.deserialiseFromBytes decoder bytes) + + let jsonBytes = Data.Aeson.Encode.Pretty.encodePretty value + + Data.ByteString.Lazy.Char8.putStrLn jsonBytes + + else do + Data.ByteString.Lazy.putStr bytes + + Decode {..} -> do bytes <- Data.ByteString.Lazy.getContents - term <- throws (Codec.Serialise.deserialiseOrFail bytes) + term <- do + if json + then do + value <- case Data.Aeson.eitherDecode' bytes of + Left string -> fail string + Right value -> return value + + let encoding = Codec.CBOR.JSON.encodeValue value + + let cborBytes = Codec.CBOR.Write.toLazyByteString encoding + throws (Codec.Serialise.deserialiseOrFail cborBytes) + else do + throws (Codec.Serialise.deserialiseOrFail bytes) expression <- throws (Dhall.Binary.decodeWithVersion term) diff --git a/src/Dhall/Map.hs b/src/Dhall/Map.hs --- a/src/Dhall/Map.hs +++ b/src/Dhall/Map.hs @@ -43,6 +43,7 @@ , mapWithKey , traverseWithKey , traverseWithKey_ + , unorderedTraverseWithKey_ , foldMapWithKey -- * Conversions @@ -53,6 +54,7 @@ import Control.Applicative ((<|>)) import Data.Data (Data) +import Data.Foldable (traverse_) import Data.Semigroup import Prelude hiding (filter, lookup) @@ -462,6 +464,17 @@ :: Ord k => Applicative f => (k -> a -> f ()) -> Map k a -> f () traverseWithKey_ f m = Data.Functor.void (traverseWithKey f m) {-# INLINABLE traverseWithKey_ #-} + +{-| Travese all of the key-value pairs in a 'Map', not preserving their + original order, where the result of the computation can be forgotten. + + Note that this is an optimisation over 'traverseWithKey_' since we do + not care in what order we traverse the pairs. +-} +unorderedTraverseWithKey_ + :: Ord k => Applicative f => (k -> a -> f ()) -> Map k a -> f () +unorderedTraverseWithKey_ f = Data.Functor.void . traverse_ (uncurry f) . toList +{-# INLINABLE unorderedTraverseWithKey_ #-} {-| Convert a `Map` to a list of key-value pairs in the original order of keys diff --git a/src/Dhall/Parser/Expression.hs b/src/Dhall/Parser/Expression.hs --- a/src/Dhall/Parser/Expression.hs +++ b/src/Dhall/Parser/Expression.hs @@ -10,6 +10,7 @@ import Control.Applicative (Alternative(..), optional) import Data.ByteArray.Encoding (Base(..)) import Data.Functor (void) +import Data.List.NonEmpty (NonEmpty(..)) import Data.Semigroup (Semigroup(..)) import Data.Text (Text) import Dhall.Core @@ -20,6 +21,7 @@ import qualified Data.ByteArray.Encoding import qualified Data.ByteString import qualified Data.Char +import qualified Data.Foldable import qualified Data.List.NonEmpty import qualified Data.Sequence import qualified Data.Text @@ -499,15 +501,10 @@ singleQuoteLiteral = do _ <- Text.Parser.Char.text "''" - - -- This is technically not in the grammar, but it's still equivalent to the - -- original grammar and an easy way to discard the first character if it's - -- a newline - _ <- optional endOfLine - + _ <- endOfLine a <- singleQuoteContinue - return (dedent a) + return (toDoubleQuoted a) where endOfLine = void (Text.Parser.Char.char '\n' ) @@ -632,9 +629,9 @@ where parentPath = do _ <- ".." :: Parser Text - File (Directory segments) final <- file_ + file <- file_ - return (Local Here (File (Directory (segments ++ [".."])) final)) + return (Local Parent file) herePath = do _ <- "." :: Parser Text @@ -724,50 +721,53 @@ renderChunk :: (Text, Expr s a) -> Text renderChunk (c, _) = c <> "${x}" -dedent :: Chunks Src a -> Chunks Src a -dedent chunks0 = process chunks0 - where - text0 = renderChunks chunks0 +splitOn :: Text -> Text -> NonEmpty Text +splitOn needle haystack = + case Data.Text.splitOn needle haystack of + [] -> "" :| [] + t : ts -> t :| ts - lines0 = Data.Text.lines text0 +linesLiteral :: Chunks s a -> NonEmpty (Chunks s a) +linesLiteral (Chunks [] suffix) = + fmap (Chunks []) (splitOn "\n" suffix) +linesLiteral (Chunks ((prefix, interpolation) : pairs₀) suffix₀) = + foldr + Data.List.NonEmpty.cons + (Chunks ((lastLine, interpolation) : pairs₁) suffix₁ :| chunks) + (fmap (Chunks []) initLines) + where + splitLines = splitOn "\n" prefix - isEmpty = Data.Text.all Data.Char.isSpace + initLines = Data.List.NonEmpty.init splitLines + lastLine = Data.List.NonEmpty.last splitLines - nonEmptyLines = filter (not . isEmpty) lines0 + Chunks pairs₁ suffix₁ :| chunks = linesLiteral (Chunks pairs₀ suffix₀) - indentLength line = - Data.Text.length (Data.Text.takeWhile Data.Char.isSpace line) +unlinesLiteral :: NonEmpty (Chunks s a) -> Chunks s a +unlinesLiteral chunks = + Data.Foldable.fold (Data.List.NonEmpty.intersperse "\n" chunks) - shortestIndent = case nonEmptyLines of - [] -> 0 - _ -> minimum (map indentLength nonEmptyLines) +leadingSpaces :: Chunks s a -> Int +leadingSpaces chunks = + Data.Text.length (Data.Text.takeWhile Data.Char.isSpace firstText) + where + firstText = + case chunks of + Chunks [] suffix -> suffix + Chunks ((prefix, _) : _ ) _ -> prefix - -- The purpose of this complicated `trimBegin`/`trimContinue` is to ensure - -- that we strip leading whitespace without stripping whitespace after - -- variable interpolation +dropLiteral :: Int -> Chunks s a -> Chunks s a +dropLiteral n (Chunks [] suffix) = + Chunks [] (Data.Text.drop n suffix) +dropLiteral n (Chunks ((prefix, interpolation) : rest) suffix) = + Chunks ((Data.Text.drop n prefix, interpolation) : rest) suffix - -- This is the trim function we use up until the first variable - -- interpolation, dedenting all lines - trimBegin = - Data.Text.intercalate "\n" - . map (Data.Text.drop shortestIndent) - . Data.Text.splitOn "\n" +toDoubleQuoted :: Chunks Src a -> Chunks Src a +toDoubleQuoted literal = + unlinesLiteral (fmap (dropLiteral indent) literals) + where + literals = linesLiteral literal - -- This is the trim function we use after each variable interpolation - -- where we indent each line except the first line (since it's not a true - -- beginning of a line) - trimContinue text = Data.Text.intercalate "\n" lines_ - where - lines_ = case Data.Text.splitOn "\n" text of - [] -> [] - l:ls -> l:map (Data.Text.drop shortestIndent) ls + l :| ls = literals - -- This is the loop that drives whether or not to use `trimBegin` or - -- `trimContinue`. We call this function with `trimBegin`, but after the - -- first interpolation we switch permanently to `trimContinue` - process (Chunks ((x0, y0):xys) z) = - Chunks ((trimBegin x0, y0):xys') (trimContinue z) - where - xys' = [ (trimContinue x, y) | (x, y) <- xys ] - process (Chunks [] z) = - Chunks [] (trimBegin z) + indent = Data.Foldable.foldl' min (leadingSpaces l) (fmap leadingSpaces ls) diff --git a/src/Dhall/Repl.hs b/src/Dhall/Repl.hs --- a/src/Dhall/Repl.hs +++ b/src/Dhall/Repl.hs @@ -1,8 +1,9 @@ -- | This module contains the implementation of the @dhall repl@ subcommand -{-# language FlexibleContexts #-} -{-# language NamedFieldPuns #-} +{-# language FlexibleContexts #-} +{-# language NamedFieldPuns #-} {-# language OverloadedStrings #-} +{-# language RecordWildCards #-} module Dhall.Repl ( -- * Repl @@ -13,13 +14,20 @@ import Control.Monad.IO.Class ( MonadIO, liftIO ) import Control.Monad.State.Class ( MonadState, get, modify ) import Control.Monad.State.Strict ( evalStateT ) -import Data.List ( foldl' ) +import Data.List ( elemIndex, isPrefixOf, nub ) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Semigroup ((<>)) import Dhall.Binary (StandardVersion(..)) +import Dhall.Context (Context) import Dhall.Import (standardVersion) import Dhall.Pretty (CharacterSet(..)) import Lens.Family (set) +import System.Console.Haskeline (Interrupt(..)) +import System.Console.Haskeline.Completion ( Completion, simpleCompletion ) +import System.Environment ( getEnvironment ) import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.HashSet import qualified Data.Text as Text import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty ( renderIO ) @@ -31,13 +39,17 @@ import qualified Dhall.Pretty import qualified Dhall.Core as Expr ( Expr(..) ) import qualified Dhall.Import as Dhall +import qualified Dhall.Map as Map import qualified Dhall.Parser as Dhall import qualified Dhall.TypeCheck as Dhall import qualified System.Console.ANSI +import qualified System.Console.Haskeline.Completion as Haskeline import qualified System.Console.Haskeline.MonadException as Haskeline import qualified System.Console.Repline as Repline import qualified System.IO +type Repl = Repline.HaskelineT (State.StateT Env IO) + -- | Implementation of the @dhall repl@ subcommand repl :: CharacterSet -> Bool -> StandardVersion -> IO () repl characterSet explain _standardVersion = @@ -49,8 +61,8 @@ ( pure "⊢ " ) ( dontCrash . eval ) options - (Just ':') - ( Repline.Word completer ) + ( Just optionsPrefix ) + completer greeter ) (emptyEnv { characterSet, explain, _standardVersion }) @@ -148,43 +160,63 @@ output System.IO.stdout exprType' +applyContext + :: Context Binding + -> Dhall.Expr Dhall.Src Dhall.X + -> Dhall.Expr Dhall.Src Dhall.X +applyContext context expression = + case bindings of + [] -> expression + b : bs -> Dhall.Core.Let (b :| bs) expression + where + definitions = reverse $ Dhall.Context.toList context + convertBinding (variable, Binding {..}) = Dhall.Core.Binding {..} + where + annotation = Just bindingType + value = bindingExpr + + bindings = fmap convertBinding definitions + normalize :: MonadState Env m => Dhall.Expr Dhall.Src Dhall.X -> m ( Dhall.Expr t Dhall.X ) normalize e = do - env <- - get + env <- get - return - ( Dhall.normalize - ( foldl' - ( \a (k, Binding { bindingType, bindingExpr }) -> - Expr.Let (pure (Dhall.Core.Binding k (Just bindingType) bindingExpr)) a - ) - e - ( Dhall.Context.toList ( envToContext env ) ) - ) - ) + return (Dhall.normalize (applyContext (envToContext env) e)) typeCheck :: ( MonadIO m, MonadState Env m ) => Dhall.Expr Dhall.Src Dhall.X -> m ( Dhall.Expr Dhall.Src Dhall.X ) -typeCheck expr = do - env <- - get +typeCheck expression = do + env <- get let wrap = if explain env then Dhall.detailed else id - case Dhall.typeWith ( bindingType <$> envToContext env ) expr of - Left e -> - liftIO ( wrap (throwIO e) ) + case Dhall.typeOf (applyContext (envToContext env) expression) of + Left e -> liftIO ( wrap (throwIO e) ) + Right a -> return a - Right a -> - return a +-- Separate the equal sign to be its own word in order to simplify parsing +-- This is intended to be used with the options that require assignment +separateEqual :: [String] -> [String] +separateEqual [] = [] +separateEqual (x:xs) + -- Handle the case where there is no space between the var and "=" + | Just i <- elemIndex '=' x + = let (a, _:b) = splitAt i x + in a : "=" : b : xs + -- Handle the case where there is no space between the "=" and the expression + | ('=':y):ys <- xs + = x : "=" : y : ys + | otherwise + = x : xs + + addBinding :: ( MonadIO m, MonadState Env m ) => [String] -> m () addBinding (k : "=" : srcs) = do let @@ -234,20 +266,105 @@ liftIO (System.IO.withFile file System.IO.WriteMode handler) saveBinding _ = fail ":save should be of the form `:save x = y`" +cmdQuit :: ( MonadIO m, MonadState Env m ) => [String] -> m () +cmdQuit _ = do + liftIO (putStrLn "Goodbye.") + liftIO (throwIO Interrupt) + +optionsPrefix :: Char +optionsPrefix = ':' + + options :: ( Haskeline.MonadException m, MonadIO m, MonadState Env m ) => Repline.Options m options = [ ( "type", dontCrash . typeOf ) - , ( "let", dontCrash . addBinding ) - , ( "save", dontCrash . saveBinding ) + , ( "let", dontCrash . addBinding . separateEqual ) + , ( "save", dontCrash . saveBinding . separateEqual ) + , ( "quit", cmdQuit ) ] -completer :: Monad m => Repline.WordCompleter m -completer _ = - return [] +completer + :: (Monad m, MonadIO m, MonadState Env m) + => Repline.CompleterStyle m +completer = + Repline.Prefix + (Haskeline.completeWordWithPrev (Just '\\') separators completeFunc) + [] + where + -- Separators that can be found on the left of something we want to + -- autocomplete + separators :: String + separators = " \t[(,=+*&|}#?>:" + +completeFunc + :: (Monad m, MonadIO m, MonadState Env m) + => String -> String -> m [Completion] +completeFunc reversedPrev word + + -- Complete commands + | reversedPrev == ":" + = pure . listCompletion $ fst <$> (options :: Repline.Options Repl) + + -- Complete file paths + | any (`isPrefixOf` word) [ "/", "./", "../", "~/" ] + = Haskeline.listFiles word + + -- Complete environment variables + | reverse "env:" `isPrefixOf` reversedPrev + = listCompletion . fmap fst <$> liftIO getEnvironment + + -- Complete record fields and union alternatives + | '.' `elem` word + = do + Env { envBindings } <- get + + let var:subFields = Text.split (== '.') (Text.pack word) + + case Dhall.Context.lookup var 0 envBindings of + + Nothing -> pure [] + + Just binding -> do + let candidates = algebraicComplete subFields (bindingExpr binding) + pure $ listCompletion (Text.unpack . (var <>) <$> candidates) + + -- Complete variables in scope and all reserved identifiers + | otherwise + = do + Env { envBindings } <- get + + let vars = map fst $ Dhall.Context.toList envBindings + reserved = Data.HashSet.toList Dhall.Core.reservedIdentifiers + + pure . listCompletion . map Text.unpack . nub $ vars ++ reserved + + where + listCompletion = map simpleCompletion . filter (word `isPrefixOf`) + + algebraicComplete :: [Text.Text] -> Dhall.Expr Dhall.Src Dhall.X -> [Text.Text] + algebraicComplete subFields expr = + let keys = fmap ("." <>) . Map.keys + + withMap m + | [] <- subFields = keys m + -- Stop on last subField (we care about the keys at this level) + | [_] <- subFields = keys m + | f:fs <- subFields = + maybe + [] + (fmap (("." <> f) <>) . algebraicComplete fs) + (Map.lookup f m) + + in case expr of + Dhall.Core.Record m -> withMap m + Dhall.Core.RecordLit m -> withMap m + Dhall.Core.Union m -> withMap m + Dhall.Core.UnionLit _ _ m -> withMap m + _ -> [] greeter :: MonadIO m => m () diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -510,12 +510,8 @@ else Left (TypeError ctx e (FieldAnnotationMismatch k t c k0 t0 Sort)) _ -> Left (TypeError ctx e (InvalidFieldType k t)) - Dhall.Map.traverseWithKey_ process rest - - case c of - Type -> return (Const Type) - Kind -> return (Const Sort) - Sort -> return (Const Sort) + Dhall.Map.unorderedTraverseWithKey_ process rest + return (Const c) loop ctx e@(RecordLit kvs ) = do case Dhall.Map.toList kvs of [] -> return (Record mempty) @@ -557,14 +553,37 @@ kts <- Dhall.Map.traverseWithKey process kvs return (Record kts) loop ctx e@(Union kts ) = do - let process k t = do - s <- fmap Dhall.Core.normalize (loop ctx t) - case s of - Const Type -> return () - Const Kind -> return () - _ -> Left (TypeError ctx e (InvalidAlternativeType k t)) - Dhall.Map.traverseWithKey_ process kts - return (Const Type) + case Dhall.Map.uncons kts of + Nothing -> do + return (Const Type) + + Just (k0, t0, rest) -> do + s0 <- fmap Dhall.Core.normalize (loop ctx t0) + + c0 <- case s0 of + Const c0 -> do + return c0 + + _ -> do + Left (TypeError ctx e (InvalidAlternativeType k0 t0)) + + let process k t = do + s <- fmap Dhall.Core.normalize (loop ctx t) + + c <- case s of + Const c -> do + return c + + _ -> do + Left (TypeError ctx e (InvalidAlternativeType k t)) + + if c0 == c + then return () + else Left (TypeError ctx e (AlternativeAnnotationMismatch k t c k0 t0 c0)) + + Dhall.Map.unorderedTraverseWithKey_ process rest + + return (Const c0) loop ctx e@(UnionLit k v kts) = do case Dhall.Map.lookup k kts of Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) @@ -771,13 +790,10 @@ loop ctx e@(Constructors t ) = do _ <- loop ctx t - kts <- case Dhall.Core.normalize t of - Union kts -> return kts - t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t')) - - let adapt k t_ = Pi k t_ (Union kts) + case Dhall.Core.normalize t of + u@(Union _) -> loop ctx u + t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t')) - return (Record (Dhall.Map.mapWithKey adapt kts)) loop ctx e@(Field r x ) = do t <- fmap Dhall.Core.normalize (loop ctx r) @@ -871,6 +887,7 @@ | FieldMismatch Text (Expr s a) Const Text (Expr s a) Const | InvalidAlternative Text (Expr s a) | InvalidAlternativeType Text (Expr s a) + | AlternativeAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const | ListAppendMismatch (Expr s a) (Expr s a) | DuplicateAlternative Text | MustCombineARecord Char (Expr s a) (Expr s a) @@ -2314,6 +2331,61 @@ prettyTypeMessage (InvalidAlternativeType k expr0) = ErrorMessages {..} where + short = "Invalid alternative type" + + long = + "Explanation: Every union type specifies the type of each alternative, like this:\n\ + \ \n\ + \ \n\ + \ The type of the first alternative is ❰Bool❱ \n\ + \ ⇩ \n\ + \ ┌──────────────────────────────────┐ \n\ + \ │ < Left : Bool, Right : Natural > │ A union type with two alternatives \n\ + \ └──────────────────────────────────┘ \n\ + \ ⇧ \n\ + \ The type of the second alternative is ❰Natural❱ \n\ + \ \n\ + \ \n\ + \However, these alternatives can only be annotated with ❰Type❱s, ❰Kind❱s, or \n\ + \❰Sort❱s. For example, the following union types are " <> _NOT <> " valid: \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────────┐ \n\ + \ │ < Left : Bool, Right : 1 > │ Invalid union type \n\ + \ └────────────────────────────┘ \n\ + \ ⇧ \n\ + \ This is a ❰Natural❱ and not a ❰Type❱, ❰Kind❱, or \n\ + \ ❰Sort❱ \n\ + \ \n\ + \ \n\ + \Some common reasons why you might get this error: \n\ + \ \n\ + \● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one \n\ + \ alternative: \n\ + \ \n\ + \ ┌─────────────────┐ \n\ + \ │ < Example : 1 > │ \n\ + \ └─────────────────┘ \n\ + \ ⇧ \n\ + \ This could be ❰=❱ instead \n\ + \ \n\ + \ \n\ + \────────────────────────────────────────────────────────────────────────────────\n\ + \ \n\ + \You provided a union type with an alternative named: \n\ + \ \n\ + \" <> txt0 <> "\n\ + \ \n\ + \... annotated with the following expression which is not a ❰Type❱, ❰Kind❱, or \n\ + \❰Sort❱: \n\ + \ \n\ + \" <> txt1 <> "\n" + where + txt0 = insert k + txt1 = insert expr0 + +prettyTypeMessage (InvalidAlternative k expr0) = ErrorMessages {..} + where short = "Invalid alternative" long = @@ -2328,35 +2400,15 @@ \ └──────────────────────────────────┘ \n\ \ \n\ \ \n\ - \However, this value must be a term and not a type. For example, the following \n\ + \However, this value must be a term, type, or kind. For example, the following \n\ \values are " <> _NOT <> " valid: \n\ \ \n\ \ \n\ - \ ┌──────────────────────────────────┐ \n\ - \ │ < Left = Text, Right : Natural > │ Invalid union literal \n\ - \ └──────────────────────────────────┘ \n\ - \ ⇧ \n\ - \ This is a type and not a term \n\ - \ \n\ - \ \n\ - \ ┌───────────────────────────────┐ \n\ - \ │ < Left = Type, Right : Type > │ Invalid union type \n\ - \ └───────────────────────────────┘ \n\ + \ ┌─────────────────┐ \n\ + \ │ < Left = Sort > │ Invalid union literal \n\ + \ └─────────────────┘ \n\ \ ⇧ \n\ - \ This is a kind and not a term \n\ - \ \n\ - \ \n\ - \Some common reasons why you might get this error: \n\ - \ \n\ - \● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one \n\ - \ alternative: \n\ - \ \n\ - \ \n\ - \ ┌────────────────────┐ \n\ - \ │ < Example = Text > │ \n\ - \ └────────────────────┘ \n\ - \ ⇧ \n\ - \ This could be ❰:❱ instead \n\ + \ This is not a term, type, or kind \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ @@ -2369,71 +2421,75 @@ \ \n\ \" <> txt1 <> "\n\ \ \n\ - \... which is not a term \n" + \... which is not a term, type, or kind. \n" where txt0 = insert k txt1 = insert expr0 -prettyTypeMessage (InvalidAlternative k expr0) = ErrorMessages {..} +prettyTypeMessage (AlternativeAnnotationMismatch k0 expr0 c0 k1 expr1 c1) = ErrorMessages {..} where - short = "Invalid alternative" + short = "Alternative annotation mismatch" long = - "Explanation: Every union type specifies the type of each alternative, like this:\n\ + "Explanation: Every union type annotates each alternative with a ❰Type❱ or a \n\ + \❰Kind❱, like this: \n\ \ \n\ \ \n\ - \ The type of the first alternative is ❰Bool❱ \n\ - \ ⇩ \n\ - \ ┌──────────────────────────────────┐ \n\ - \ │ < Left : Bool, Right : Natural > │ A union type with two alternatives \n\ - \ └──────────────────────────────────┘ \n\ - \ ⇧ \n\ - \ The type of the second alternative is ❰Natural❱ \n\ + \ ┌───────────────────────────────────┐ \n\ + \ │ < Left : Natural | Right : Bool > │ Every alternative is annotated with a\n\ + \ └───────────────────────────────────┘ ❰Type❱ \n\ \ \n\ \ \n\ - \However, these alternatives can only be annotated with types. For example, the \n\ - \following union types are " <> _NOT <> " valid: \n\ + \ ┌────────────────────────────────────┐ \n\ + \ │ < Foo : Type → Type | Bar : Type > │ Every alternative is annotated with \n\ + \ └────────────────────────────────────┘ a ❰Kind❱ \n\ \ \n\ \ \n\ - \ ┌────────────────────────────┐ \n\ - \ │ < Left : Bool, Right : 1 > │ Invalid union type \n\ - \ └────────────────────────────┘ \n\ - \ ⇧ \n\ - \ This is a term and not a type \n\ + \ ┌────────────────┐ \n\ + \ │ < Baz : Kind > │ Every alternative is annotated with a ❰Sort❱ \n\ + \ └────────────────┘ \n\ \ \n\ \ \n\ + \However, you cannot have a union type that mixes ❰Type❱s, ❰Kind❱s, or ❰Sort❱s \n\ + \for the annotations: \n\ + \ \n\ + \ \n\ + \ This is a ❰Type❱ annotation \n\ + \ ⇩ \n\ \ ┌───────────────────────────────┐ \n\ - \ │ < Left : Bool, Right : Type > │ Invalid union type \n\ + \ │ { foo : Natural, bar : Type } │ Invalid union type \n\ \ └───────────────────────────────┘ \n\ \ ⇧ \n\ - \ This is a kind and not a type \n\ + \ ... but this is a ❰Kind❱ annotation \n\ \ \n\ \ \n\ - \Some common reasons why you might get this error: \n\ + \You provided a union type with an alternative named: \n\ \ \n\ - \● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one \n\ - \ alternative: \n\ + \" <> txt0 <> "\n\ \ \n\ - \ ┌─────────────────┐ \n\ - \ │ < Example : 1 > │ \n\ - \ └─────────────────┘ \n\ - \ ⇧ \n\ - \ This could be ❰=❱ instead \n\ + \... annotated with the following expression: \n\ \ \n\ + \" <> txt1 <> "\n\ \ \n\ - \────────────────────────────────────────────────────────────────────────────────\n\ + \... which is a " <> level c0 <> " whereas another alternative named: \n\ \ \n\ - \You provided a union type with an alternative named: \n\ + \" <> txt2 <> "\n\ \ \n\ - \" <> txt0 <> "\n\ + \... annotated with the following expression: \n\ \ \n\ - \... annotated with the following expression which is not a type: \n\ + \" <> txt3 <> "\n\ \ \n\ - \" <> txt1 <> "\n" + \... is a " <> level c1 <> ", which does not match \n" where - txt0 = insert k + txt0 = insert k0 txt1 = insert expr0 + txt2 = insert k1 + txt3 = insert expr1 + level Type = "❰Type❱" + level Kind = "❰Kind❱" + level Sort = "❰Sort❱" + prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..} where short = "You can only append ❰List❱s with matching element types\n" @@ -3432,7 +3488,7 @@ buildBooleanOperator "==" expr0 expr1 prettyTypeMessage (CantNE expr0 expr1) = - buildBooleanOperator "/=" expr0 expr1 + buildBooleanOperator "!=" expr0 expr1 prettyTypeMessage (CantInterpolate expr0 expr1) = ErrorMessages {..} where diff --git a/tests/Dhall/Test/Format.hs b/tests/Dhall/Test/Format.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Format.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Format where + +import Data.Monoid (mempty, (<>)) +import Data.Text (Text) +import Dhall.Pretty (CharacterSet(..)) +import Test.Tasty (TestTree) + +import qualified Control.Exception +import qualified Data.Text +import qualified Data.Text.IO +import qualified Data.Text.Prettyprint.Doc +import qualified Data.Text.Prettyprint.Doc.Render.Text +import qualified Dhall.Parser +import qualified Dhall.Pretty +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +tests :: TestTree +tests = + Test.Tasty.testGroup "format tests" + [ should + Unicode + "prefer multi-line strings when newlines present" + "multiline" + , should + Unicode + "escape ${ for single-quoted strings" + "escapeSingleQuotedOpenInterpolation" + , should + Unicode + "preserve the original order of fields" + "fieldOrder" + , should + Unicode + "preserve the original order of projections" + "projectionOrder" + , should + Unicode + "escape numeric labels correctly" + "escapeNumericLabel" + , should + Unicode + "correctly handle scientific notation with a large exponent" + "largeExponent" + , should + Unicode + "round a double to the nearest representable value. Ties go to even least significant bit" + "doubleRound" + , should + Unicode + "correctly format the empty record literal" + "emptyRecord" + , should + Unicode + "indent then/else to the same column" + "ifThenElse" + , should + Unicode + "handle indenting long imports correctly without trailing space per line" + "importLines" + , should + Unicode + "handle indenting small imports correctly without trailing space inline" + "importLines2" + , should + Unicode + "not remove parentheses when accessing a field of a record" + "importAccess" + , should + Unicode + "handle formatting sha256 imports correctly" + "sha256Printing" + , should + Unicode + "handle formatting of Import suffix correctly" + "importSuffix" + , should + ASCII + "be able to format with ASCII characters" + "ascii" + , should + Unicode + "preserve Unicode characters" + "unicode" + , should + Unicode + "not replace `../` with `./../`" + "parent" + ] + +should :: CharacterSet -> Text -> Text -> TestTree +should characterSet name basename = + Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do + let inputFile = + Data.Text.unpack ("./tests/format/" <> basename <> "A.dhall") + let outputFile = + Data.Text.unpack ("./tests/format/" <> basename <> "B.dhall") + inputText <- Data.Text.IO.readFile inputFile + + expr <- case Dhall.Parser.exprFromText mempty inputText of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + let doc = Dhall.Pretty.prettyCharacterSet characterSet expr + let docStream = Data.Text.Prettyprint.Doc.layoutSmart Dhall.Pretty.layoutOpts doc + let actualText = Data.Text.Prettyprint.Doc.Render.Text.renderStrict docStream + + expectedText <- Data.Text.IO.readFile outputFile + + let message = + "The formatted expression did not match the expected output" + Test.Tasty.HUnit.assertEqual message expectedText actualText diff --git a/tests/Dhall/Test/Import.hs b/tests/Dhall/Test/Import.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Import.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Import where + +import Data.Text (Text) +import Test.Tasty (TestTree) +import Dhall.Import (MissingImports(..)) +import Control.Exception (catch, throwIO) +import Data.Monoid ((<>)) + +import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.Text +import qualified Data.Text.IO +import qualified Dhall.Parser +import qualified Dhall.Import +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +tests :: TestTree +tests = + Test.Tasty.testGroup "import tests" + [ Test.Tasty.testGroup "import alternatives" + [ shouldFail + 3 + "alternative of several unset env variables" + "./tests/import/failure/alternativeEnv.dhall" + , shouldFail + 1 + "alternative of env variable and missing" + "./tests/import/failure/alternativeEnvMissing.dhall" + , shouldFail + 0 + "just missing" + "./tests/import/failure/missing.dhall" + , shouldNotFail + "alternative of env variable, missing, and a Natural" + "./tests/import/success/alternativeEnvNaturalA.dhall" + , shouldNotFail + "alternative of env variable and a Natural" + "./tests/import/success/alternativeEnvSimpleA.dhall" + , shouldNotFail + "alternative of a Natural and missing" + "./tests/import/success/alternativeNaturalA.dhall" + ] + , Test.Tasty.testGroup "import relative to argument" + [ shouldNotFailRelative + "works" + "./tests/import/data/foo/bar" + "./tests/import/success/relative.dhall" + , shouldNotFailRelative + "a semantic integrity check if fields are reordered" + "./tests/import/success/" + "./tests/import/success/fieldOrderA.dhall" + , shouldNotFailRelative + "a semantic integrity check when importing an expression using `constructors`" + "./tests/import/success/" + "./tests/import/success/issue553B.dhall" + ] + ] + +shouldNotFail :: Text -> FilePath -> TestTree +shouldNotFail name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.IO.readFile path + actualExpr <- case Dhall.Parser.exprFromText mempty text of + Left err -> throwIO err + Right expr -> return expr + _ <- Dhall.Import.load actualExpr + return ()) + +shouldNotFailRelative :: Text -> FilePath -> FilePath -> TestTree +shouldNotFailRelative name dir path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.IO.readFile path + expr <- case Dhall.Parser.exprFromText mempty text of + Left err -> throwIO err + Right expr -> return expr + + _ <- State.evalStateT (Dhall.Import.loadWith expr) (Dhall.Import.emptyStatus dir) + + return ()) + +shouldFail :: Int -> Text -> FilePath -> TestTree +shouldFail failures name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.IO.readFile path + actualExpr <- case Dhall.Parser.exprFromText mempty text of + Left err -> throwIO err + Right expr -> return expr + catch + (do + _ <- Dhall.Import.load actualExpr + fail "Import should have failed, but it succeeds") + (\(MissingImports es) -> case length es == failures of + True -> pure () + False -> fail ("Should have failed " + <> show failures + <> " times, but failed with: \n" + <> show es)) ) diff --git a/tests/Dhall/Test/Lint.hs b/tests/Dhall/Test/Lint.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Lint.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Lint where + +import Data.Monoid (mempty, (<>)) +import Data.Text (Text) +import Test.Tasty (TestTree) + +import qualified Control.Exception +import qualified Data.Text +import qualified Data.Text.IO +import qualified Dhall.Core +import qualified Dhall.Import +import qualified Dhall.Lint +import qualified Dhall.Parser +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +tests :: TestTree +tests = + Test.Tasty.testGroup "format tests" + [ should + "correctly handle multi-let expressions" + "success/multilet" + ] + +should :: Text -> Text -> TestTree +should name basename = + Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do + let inputFile = + Data.Text.unpack ("./tests/lint/" <> basename <> "A.dhall") + let outputFile = + Data.Text.unpack ("./tests/lint/" <> basename <> "B.dhall") + + inputText <- Data.Text.IO.readFile inputFile + + parsedInput <- case Dhall.Parser.exprFromText mempty inputText of + Left exception -> Control.Exception.throwIO exception + Right expression -> return expression + + let lintedInput = Dhall.Lint.lint parsedInput + + actualExpression <- Dhall.Import.load lintedInput + + outputText <- Data.Text.IO.readFile outputFile + + parsedOutput <- case Dhall.Parser.exprFromText mempty outputText of + Left exception -> Control.Exception.throwIO exception + Right expression -> return expression + + resolvedOutput <- Dhall.Import.load parsedOutput + + let expectedExpression = Dhall.Core.denote resolvedOutput + + let message = + "The linted expression did not match the expected output" + + Test.Tasty.HUnit.assertEqual message expectedExpression actualExpression diff --git a/tests/Dhall/Test/Main.hs b/tests/Dhall/Test/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Main.hs @@ -0,0 +1,38 @@ +module Main where + +import Test.Tasty (TestTree) + +import qualified Dhall.Test.Format +import qualified Dhall.Test.Import +import qualified Dhall.Test.Lint +import qualified Dhall.Test.Normalization +import qualified Dhall.Test.Parser +import qualified Dhall.Test.QuickCheck +import qualified Dhall.Test.Regression +import qualified Dhall.Test.Tutorial +import qualified Dhall.Test.TypeCheck +import qualified System.Directory +import qualified System.Environment +import qualified Test.Tasty + +import System.FilePath (()) + +allTests :: TestTree +allTests = + Test.Tasty.testGroup "Dhall Tests" + [ Dhall.Test.Normalization.tests + , Dhall.Test.Parser.tests + , Dhall.Test.Regression.tests + , Dhall.Test.Tutorial.tests + , Dhall.Test.Format.tests + , Dhall.Test.TypeCheck.tests + , Dhall.Test.Import.tests + , Dhall.Test.QuickCheck.tests + , Dhall.Test.Lint.tests + ] + +main :: IO () +main = do + pwd <- System.Directory.getCurrentDirectory + System.Environment.setEnv "XDG_CACHE_HOME" (pwd ".cache") + Test.Tasty.defaultMain allTests diff --git a/tests/Dhall/Test/Normalization.hs b/tests/Dhall/Test/Normalization.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Normalization.hs @@ -0,0 +1,310 @@ +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Normalization where + +import Data.Monoid ((<>)) +import Data.Text (Text) +import Dhall.Core (Expr) +import Dhall.TypeCheck (X) + +import qualified Control.Exception +import qualified Data.Text +import qualified Dhall.Core +import qualified Dhall.Import +import qualified Dhall.Parser +import qualified Dhall.TypeCheck + +import Dhall.Core +import Dhall.Context +import Test.Tasty +import Test.Tasty.HUnit +import Dhall.Test.Util + +tests :: TestTree +tests = + testGroup "normalization" + [ tutorialExamples + , preludeExamples + , simplifications + , constantFolding + , conversions + , customization + , shouldNormalize + "Optional build/fold fusion" + "success/simple/optionalBuildFold" + , shouldNormalize + "a remote-systems.conf builder" + "success/remoteSystems" + , shouldNormalize + "multi-line strings correctly" + "success/simple/multiLine" + , shouldNormalize + "the // operator and sort the fields" + "success/simple/sortOperator" + , multiline + ] + +tutorialExamples :: TestTree +tutorialExamples = + testGroup "Tutorial examples" + [ shouldNormalize "⩓" "./success/haskell-tutorial/combineTypes/0" + , shouldNormalize "//\\\\" "./success/haskell-tutorial/combineTypes/1" + , shouldNormalize "//" "./success/haskell-tutorial/prefer/0" + , shouldNormalize "projection" "./success/haskell-tutorial/projection/0" + , shouldNormalize "access record" "./success/haskell-tutorial/access/0" + , shouldNormalize "access union" "./success/haskell-tutorial/access/1" + ] + +preludeExamples :: TestTree +preludeExamples = + testGroup "Prelude examples" + [ shouldNormalize "Bool/and" "./success/prelude/Bool/and/0" + , shouldNormalize "Bool/and" "./success/prelude/Bool/and/1" + , shouldNormalize "Bool/build" "./success/prelude/Bool/build/0" + , shouldNormalize "Bool/build" "./success/prelude/Bool/build/1" + , shouldNormalize "Bool/even" "./success/prelude/Bool/even/0" + , shouldNormalize "Bool/even" "./success/prelude/Bool/even/1" + , shouldNormalize "Bool/even" "./success/prelude/Bool/even/2" + , shouldNormalize "Bool/even" "./success/prelude/Bool/even/3" + , shouldNormalize "Bool/fold" "./success/prelude/Bool/fold/0" + , shouldNormalize "Bool/fold" "./success/prelude/Bool/fold/1" + , shouldNormalize "Bool/not" "./success/prelude/Bool/not/0" + , shouldNormalize "Bool/not" "./success/prelude/Bool/not/1" + , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/0" + , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/1" + , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/2" + , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/3" + , shouldNormalize "Bool/or" "./success/prelude/Bool/or/0" + , shouldNormalize "Bool/or" "./success/prelude/Bool/or/1" + , shouldNormalize "Bool/show" "./success/prelude/Bool/show/0" + , shouldNormalize "Bool/show" "./success/prelude/Bool/show/1" + , shouldNormalize "Double/show" "./success/prelude/Double/show/0" + , shouldNormalize "Double/show" "./success/prelude/Double/show/1" + , shouldNormalize "Integer/show" "./success/prelude/Integer/show/0" + , shouldNormalize "Integer/show" "./success/prelude/Integer/show/1" + , shouldNormalize "Integer/toDouble" "./success/prelude/Integer/toDouble/0" + , shouldNormalize "Integer/toDouble" "./success/prelude/Integer/toDouble/1" + , shouldNormalize "List/all" "./success/prelude/List/all/0" + , shouldNormalize "List/all" "./success/prelude/List/all/1" + , shouldNormalize "List/any" "./success/prelude/List/any/0" + , shouldNormalize "List/any" "./success/prelude/List/any/1" + , shouldNormalize "List/build" "./success/prelude/List/build/0" + , shouldNormalize "List/build" "./success/prelude/List/build/1" + , shouldNormalize "List/concat" "./success/prelude/List/concat/0" + , shouldNormalize "List/concat" "./success/prelude/List/concat/1" + , shouldNormalize "List/concatMap" "./success/prelude/List/concatMap/0" + , shouldNormalize "List/concatMap" "./success/prelude/List/concatMap/1" + , shouldNormalize "List/filter" "./success/prelude/List/filter/0" + , shouldNormalize "List/filter" "./success/prelude/List/filter/1" + , shouldNormalize "List/fold" "./success/prelude/List/fold/0" + , shouldNormalize "List/fold" "./success/prelude/List/fold/1" + , shouldNormalize "List/fold" "./success/prelude/List/fold/2" + , shouldNormalize "List/generate" "./success/prelude/List/generate/0" + , shouldNormalize "List/generate" "./success/prelude/List/generate/1" + , shouldNormalize "List/head" "./success/prelude/List/head/0" + , shouldNormalize "List/head" "./success/prelude/List/head/1" + , shouldNormalize "List/indexed" "./success/prelude/List/indexed/0" + , shouldNormalize "List/indexed" "./success/prelude/List/indexed/1" + , shouldNormalize "List/iterate" "./success/prelude/List/iterate/0" + , shouldNormalize "List/iterate" "./success/prelude/List/iterate/1" + , shouldNormalize "List/last" "./success/prelude/List/last/0" + , shouldNormalize "List/last" "./success/prelude/List/last/1" + , shouldNormalize "List/length" "./success/prelude/List/length/0" + , shouldNormalize "List/length" "./success/prelude/List/length/1" + , shouldNormalize "List/map" "./success/prelude/List/map/0" + , shouldNormalize "List/map" "./success/prelude/List/map/1" + , shouldNormalize "List/null" "./success/prelude/List/null/0" + , shouldNormalize "List/null" "./success/prelude/List/null/1" + , shouldNormalize "List/replicate" "./success/prelude/List/replicate/0" + , shouldNormalize "List/replicate" "./success/prelude/List/replicate/1" + , shouldNormalize "List/reverse" "./success/prelude/List/reverse/0" + , shouldNormalize "List/reverse" "./success/prelude/List/reverse/1" + , shouldNormalize "List/shifted" "./success/prelude/List/shifted/0" + , shouldNormalize "List/shifted" "./success/prelude/List/shifted/1" + , shouldNormalize "List/unzip" "./success/prelude/List/unzip/0" + , shouldNormalize "List/unzip" "./success/prelude/List/unzip/1" + , shouldNormalize "Natural/build" "./success/prelude/Natural/build/0" + , shouldNormalize "Natural/build" "./success/prelude/Natural/build/1" + , shouldNormalize "Natural/enumerate" "./success/prelude/Natural/enumerate/0" + , shouldNormalize "Natural/enumerate" "./success/prelude/Natural/enumerate/1" + , shouldNormalize "Natural/even" "./success/prelude/Natural/even/0" + , shouldNormalize "Natural/even" "./success/prelude/Natural/even/1" + , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/0" + , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/1" + , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/2" + , shouldNormalize "Natural/isZero" "./success/prelude/Natural/isZero/0" + , shouldNormalize "Natural/isZero" "./success/prelude/Natural/isZero/1" + , shouldNormalize "Natural/odd" "./success/prelude/Natural/odd/0" + , shouldNormalize "Natural/odd" "./success/prelude/Natural/odd/1" + , shouldNormalize "Natural/product" "./success/prelude/Natural/product/0" + , shouldNormalize "Natural/product" "./success/prelude/Natural/product/1" + , shouldNormalize "Natural/show" "./success/prelude/Natural/show/0" + , shouldNormalize "Natural/show" "./success/prelude/Natural/show/1" + , shouldNormalize "Natural/sum" "./success/prelude/Natural/sum/0" + , shouldNormalize "Natural/sum" "./success/prelude/Natural/sum/1" + , shouldNormalize "Natural/toDouble" "./success/prelude/Natural/toDouble/0" + , shouldNormalize "Natural/toDouble" "./success/prelude/Natural/toDouble/1" + , shouldNormalize "Natural/toInteger" "./success/prelude/Natural/toInteger/0" + , shouldNormalize "Natural/toInteger" "./success/prelude/Natural/toInteger/1" + , shouldNormalize "Optional/all" "./success/prelude/Optional/all/0" + , shouldNormalize "Optional/all" "./success/prelude/Optional/all/1" + , shouldNormalize "Optional/any" "./success/prelude/Optional/any/0" + , shouldNormalize "Optional/any" "./success/prelude/Optional/any/1" + , shouldNormalize "Optional/build" "./success/prelude/Optional/build/0" + , shouldNormalize "Optional/build" "./success/prelude/Optional/build/1" + , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/0" + , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/1" + , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/2" + , shouldNormalize "Optional/filter" "./success/prelude/Optional/filter/0" + , shouldNormalize "Optional/filter" "./success/prelude/Optional/filter/1" + , shouldNormalize "Optional/fold" "./success/prelude/Optional/fold/0" + , shouldNormalize "Optional/fold" "./success/prelude/Optional/fold/1" + , shouldNormalize "Optional/head" "./success/prelude/Optional/head/0" + , shouldNormalize "Optional/head" "./success/prelude/Optional/head/1" + , shouldNormalize "Optional/head" "./success/prelude/Optional/head/2" + , shouldNormalize "Optional/last" "./success/prelude/Optional/last/0" + , shouldNormalize "Optional/last" "./success/prelude/Optional/last/1" + , shouldNormalize "Optional/last" "./success/prelude/Optional/last/2" + , shouldNormalize "Optional/length" "./success/prelude/Optional/length/0" + , shouldNormalize "Optional/length" "./success/prelude/Optional/length/1" + , shouldNormalize "Optional/map" "./success/prelude/Optional/map/0" + , shouldNormalize "Optional/map" "./success/prelude/Optional/map/1" + , shouldNormalize "Optional/null" "./success/prelude/Optional/null/0" + , shouldNormalize "Optional/null" "./success/prelude/Optional/null/1" + , shouldNormalize "Optional/toList" "./success/prelude/Optional/toList/0" + , shouldNormalize "Optional/toList" "./success/prelude/Optional/toList/1" + , shouldNormalize "Optional/unzip" "./success/prelude/Optional/unzip/0" + , shouldNormalize "Optional/unzip" "./success/prelude/Optional/unzip/1" + , shouldNormalize "Text/concat" "./success/prelude/Text/concat/0" + , shouldNormalize "Text/concat" "./success/prelude/Text/concat/1" + , shouldNormalize "Text/concatMap" "./success/prelude/Text/concatMap/0" + , shouldNormalize "Text/concatMap" "./success/prelude/Text/concatMap/1" + , shouldNormalize "Text/concatMapSep" "./success/prelude/Text/concatMapSep/0" + , shouldNormalize "Text/concatMapSep" "./success/prelude/Text/concatMapSep/1" + , shouldNormalize "Text/concatSep" "./success/prelude/Text/concatSep/0" + , shouldNormalize "Text/concatSep" "./success/prelude/Text/concatSep/1" + ] + +simplifications :: TestTree +simplifications = + testGroup "Simplifications" + [ shouldNormalize "if/then/else" "./success/simplifications/ifThenElse" + , shouldNormalize "||" "./success/simplifications/or" + , shouldNormalize "&&" "./success/simplifications/and" + , shouldNormalize "==" "./success/simplifications/eq" + , shouldNormalize "!=" "./success/simplifications/ne" + ] + +constantFolding :: TestTree +constantFolding = + testGroup "folding of constants" + [ shouldNormalize "Natural/plus" "success/simple/naturalPlus" + , shouldNormalize "Optional/fold" "success/simple/optionalFold" + , shouldNormalize "Optional/build" "success/simple/optionalBuild" + , shouldNormalize "Natural/build" "success/simple/naturalBuild" + ] + +conversions :: TestTree +conversions = + testGroup "conversions" + [ shouldNormalize "Natural/show" "success/simple/naturalShow" + , shouldNormalize "Integer/show" "success/simple/integerShow" + , shouldNormalize "Double/show" "success/simple/doubleShow" + , shouldNormalize "Natural/toInteger" "success/simple/naturalToInteger" + , shouldNormalize "Integer/toDouble" "success/simple/integerToDouble" + ] + +customization :: TestTree +customization = + testGroup "customization" + [ simpleCustomization + , nestedReduction + ] + +multiline :: TestTree +multiline = + testGroup "Multi-line literals" + [ shouldNormalize + "multi-line escape sequences" + "./success/multiline/escape" + , shouldNormalize + "a multi-line literal with a hanging indent" + "./success/multiline/hangingIndent" + , shouldNormalize + "a multi-line literal with an interior indent" + "./success/multiline/interiorIndent" + , shouldNormalize + "a multi-line literal with an interpolated expression" + "./success/multiline/interpolation" + , should + "preserve comments within a multi-line literal" + "./success/multiline/preserveComment" + , shouldNormalize + "a multi-line literal with one line" + "./success/multiline/singleLine" + , shouldNormalize + "a multi-line literal with two lines" + "./success/multiline/twoLines" + ] + +simpleCustomization :: TestTree +simpleCustomization = testCase "simpleCustomization" $ do + let tyCtx = insert "min" (Pi "_" Natural (Pi "_" Natural Natural)) empty + valCtx e = case e of + (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> pure (Just (NaturalLit (min x y))) + _ -> pure Nothing + e <- codeWith tyCtx "min (min 11 12) 8 + 1" + assertNormalizesToWith valCtx e "9" + +nestedReduction :: TestTree +nestedReduction = testCase "doubleReduction" $ do + minType <- insert "min" <$> code "Natural → Natural → Natural" + fiveorlessType <- insert "fiveorless" <$> code "Natural → Natural" + wurbleType <- insert "wurble" <$> code "Natural → Integer" + let tyCtx = minType . fiveorlessType . wurbleType $ empty + valCtx e = case e of + (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> pure (Just (NaturalLit (min x y))) + (App (Var (V "wurble" 0)) (NaturalLit x)) -> pure (Just + (App (Var (V "fiveorless" 0)) (NaturalPlus (NaturalLit x) (NaturalLit 2)))) + (App (Var (V "fiveorless" 0)) (NaturalLit x)) -> pure (Just + (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2)))) + _ -> pure Nothing + e <- codeWith tyCtx "wurble 6" + assertNormalizesToWith valCtx e "5" + +should :: Text -> Text -> TestTree +should name basename = + Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do + let actualCode = "./tests/normalization/" <> basename <> "A.dhall" + let expectedCode = "./tests/normalization/" <> basename <> "B.dhall" + + actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + actualResolved <- Dhall.Import.load actualExpr + case Dhall.TypeCheck.typeOf actualResolved of + Left err -> Control.Exception.throwIO err + Right _ -> return () + let actualNormalized = + Dhall.Core.alphaNormalize + (Dhall.Core.normalize actualResolved :: Expr X X) + + expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + expectedResolved <- Dhall.Import.load expectedExpr + case Dhall.TypeCheck.typeOf expectedResolved of + Left err -> Control.Exception.throwIO err + Right _ -> return () + -- Use `denote` instead of `normalize` to enforce that the expected + -- expression is already in normal form + let expectedNormalized = + Dhall.Core.alphaNormalize (Dhall.Core.denote expectedResolved) + + let message = + "The normalized expression did not match the expected output" + Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized + +shouldNormalize :: Text -> Text -> TestTree +shouldNormalize name = should ("normalize " <> name <> " correctly") diff --git a/tests/Dhall/Test/Parser.hs b/tests/Dhall/Test/Parser.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Parser.hs @@ -0,0 +1,184 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Parser where + +import Data.Text (Text) +import Test.Tasty (TestTree) + +import qualified Control.Exception +import qualified Data.Text +import qualified Data.Text.IO +import qualified Dhall.Parser +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +tests :: TestTree +tests = + Test.Tasty.testGroup "parser tests" + [ Test.Tasty.testGroup "whitespace" + [ shouldParse + "prefix/suffix" + "./tests/parser/success/whitespace" + , shouldParse + "block comment" + "./tests/parser/success/blockComment" + , shouldParse + "nested block comment" + "./tests/parser/success/nestedBlockComment" + , shouldParse + "line comment" + "./tests/parser/success/lineComment" + , shouldParse + "Unicode comment" + "./tests/parser/success/unicodeComment" + , shouldParse + "whitespace buffet" + "./tests/parser/success/whitespaceBuffet" + ] + , shouldParse + "label" + "./tests/parser/success/label" + , shouldParse + "quoted label" + "./tests/parser/success/quotedLabel" + , shouldParse + "double quoted string" + "./tests/parser/success/doubleQuotedString" + , shouldParse + "Unicode double quoted string" + "./tests/parser/success/unicodeDoubleQuotedString" + , shouldParse + "escaped double quoted string" + "./tests/parser/success/escapedDoubleQuotedString" + , shouldParse + "interpolated double quoted string" + "./tests/parser/success/interpolatedDoubleQuotedString" + , shouldParse + "single quoted string" + "./tests/parser/success/singleQuotedString" + , shouldParse + "escaped single quoted string" + "./tests/parser/success/escapedSingleQuotedString" + , shouldParse + "interpolated single quoted string" + "./tests/parser/success/interpolatedSingleQuotedString" + , shouldParse + "double" + "./tests/parser/success/double" + , shouldParse + "natural" + "./tests/parser/success/natural" + , shouldParse + "identifier" + "./tests/parser/success/identifier" + , shouldParse + "paths" + "./tests/parser/success/paths" + , shouldParse + "path termination" + "./tests/parser/success/pathTermination" + , shouldParse + "urls" + "./tests/parser/success/urls" + , shouldParse + "environmentVariables" + "./tests/parser/success/environmentVariables" + , shouldParse + "lambda" + "./tests/parser/success/lambda" + , shouldParse + "if then else" + "./tests/parser/success/ifThenElse" + , shouldParse + "let" + "./tests/parser/success/let" + , shouldParse + "forall" + "./tests/parser/success/forall" + , shouldParse + "function type" + "./tests/parser/success/functionType" + , shouldParse + "operators" + "./tests/parser/success/operators" + , shouldParse + "annotations" + "./tests/parser/success/annotations" + , shouldParse + "merge" + "./tests/parser/success/merge" + , shouldParse + "constructors" + "./tests/parser/success/constructors" + , shouldParse + "fields" + "./tests/parser/success/fields" + , shouldParse + "record" + "./tests/parser/success/record" + , shouldParse + "union" + "./tests/parser/success/union" + , shouldParse + "list" + "./tests/parser/success/list" + , shouldParse + "builtins" + "./tests/parser/success/builtins" + , shouldParse + "import alternatives" + "./tests/parser/success/importAlt" + , shouldParse + "large expression" + "./tests/parser/success/largeExpression" + , shouldParse + "names that begin with reserved identifiers" + "./tests/parser/success/reservedPrefix" + , shouldParse + "interpolated expressions with leading whitespace" + "./tests/parser/success/template" + , shouldParse + "collections with type annotations containing imports" + "./tests/parser/success/collectionImportType" + , shouldParse + "a parenthesized custom header import" + "./tests/parser/success/parenthesizeUsing" + , shouldNotParse + "accessing a field of an import without parentheses" + "./tests/parser/failure/importAccess.dhall" + , shouldParse + "Sort" + "./tests/parser/success/sort" + , shouldParse + "quoted path components" + "./tests/parser/success/quotedPaths" + , shouldNotParse + "positive double out of bounds" + "./tests/parser/failure/doubleBoundsPos.dhall" + , shouldNotParse + "negative double out of bounds" + "./tests/parser/failure/doubleBoundsNeg.dhall" + , shouldParse + "as Text" + "./tests/parser/success/asText" + , shouldParse + "custom headers" + "./tests/parser/success/customHeaders" + , shouldNotParse + "a multi-line literal without an initial newline" + "./tests/parser/failure/mandatoryNewline.dhall" + ] + +shouldParse :: Text -> FilePath -> TestTree +shouldParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.IO.readFile (path <> "A.dhall") + case Dhall.Parser.exprFromText mempty text of + Left err -> Control.Exception.throwIO err + Right _ -> return () ) + +shouldNotParse :: Text -> FilePath -> TestTree +shouldNotParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do + text <- Data.Text.IO.readFile path + case Dhall.Parser.exprFromText mempty text of + Left _ -> return () + Right _ -> fail "Unexpected successful parser" ) diff --git a/tests/Dhall/Test/QuickCheck.hs b/tests/Dhall/Test/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/QuickCheck.hs @@ -0,0 +1,379 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Dhall.Test.QuickCheck where + +import Codec.Serialise (DeserialiseFailure(..)) +import Control.Monad (guard) +import Data.Either (isRight) +import Data.List.NonEmpty (NonEmpty(..)) +import Dhall.Map (Map) +import Dhall.Core + ( Binding(..) + , Chunks(..) + , Const(..) + , Directory(..) + , Expr(..) + , File(..) + , FilePrefix(..) + , Import(..) + , ImportHashed(..) + , ImportMode(..) + , ImportType(..) + , Scheme(..) + , URL(..) + , Var(..) + ) +import Dhall.Set (Set) +import Numeric.Natural (Natural) +import Test.QuickCheck + (Arbitrary(..), Gen, Property, genericShrink, (===), (==>)) +import Test.QuickCheck.Instances () +import Test.Tasty (TestTree) + +import qualified Codec.Serialise +import qualified Data.Coerce +import qualified Dhall.Map +import qualified Data.Sequence +import qualified Dhall.Binary +import qualified Dhall.Core +import qualified Dhall.Diff +import qualified Dhall.Set +import qualified Dhall.TypeCheck +import qualified Test.QuickCheck +import qualified Test.Tasty.QuickCheck + +newtype DeserialiseFailureWithEq = D DeserialiseFailure + deriving (Show) + +instance Eq DeserialiseFailureWithEq where + D (DeserialiseFailure aL bL) == D (DeserialiseFailure aR bR) = + aL == aR && bL == bR + +instance (Arbitrary a, Ord a) => Arbitrary (Set a) where + arbitrary = Dhall.Set.fromList <$> arbitrary + +lift0 :: a -> Gen a +lift0 = pure + +lift1 :: Arbitrary a => (a -> b) -> Gen b +lift1 f = f <$> arbitrary + +lift2 :: (Arbitrary a, Arbitrary b) => (a -> b -> c) -> Gen c +lift2 f = f <$> arbitrary <*> arbitrary + +lift3 :: (Arbitrary a, Arbitrary b, Arbitrary c) => (a -> b -> c -> d) -> Gen d +lift3 f = f <$> arbitrary <*> arbitrary <*> arbitrary + +lift4 + :: (Arbitrary a, Arbitrary b, Arbitrary c, Arbitrary d) + => (a -> b -> c -> d -> e) -> Gen e +lift4 f = f <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary + +lift5 + :: ( Arbitrary a + , Arbitrary b + , Arbitrary c + , Arbitrary d + , Arbitrary e + ) + => (a -> b -> c -> d -> e -> f) -> Gen f +lift5 f = + f <$> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + +lift6 + :: ( Arbitrary a + , Arbitrary b + , Arbitrary c + , Arbitrary d + , Arbitrary e + , Arbitrary f + ) + => (a -> b -> c -> d -> e -> f -> g) -> Gen g +lift6 f = + f <$> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + +natural :: (Arbitrary a, Num a) => Gen a +natural = + Test.QuickCheck.frequency + [ (7, arbitrary) + , (1, fmap (\x -> x + (2 ^ (64 :: Int))) arbitrary) + ] + +integer :: (Arbitrary a, Num a) => Gen a +integer = + Test.QuickCheck.frequency + [ (7, arbitrary) + , (1, fmap (\x -> x + (2 ^ (64 :: Int))) arbitrary) + , (1, fmap (\x -> x - (2 ^ (64 :: Int))) arbitrary) + ] + +instance (Ord k, Arbitrary k, Arbitrary v) => Arbitrary (Map k v) where + arbitrary = do + n <- Test.QuickCheck.choose (0, 2) + kvs <- Test.QuickCheck.vectorOf n ((,) <$> arbitrary <*> arbitrary) + return (Dhall.Map.fromList kvs) + + shrink = + map Dhall.Map.fromList + . shrink + . Dhall.Map.toList + +instance (Arbitrary s, Arbitrary a) => Arbitrary (Binding s a) where + arbitrary = lift3 Binding + + shrink = genericShrink + +instance (Arbitrary s, Arbitrary a) => Arbitrary (Chunks s a) where + arbitrary = do + n <- Test.QuickCheck.choose (0, 2) + Chunks <$> Test.QuickCheck.vectorOf n arbitrary <*> arbitrary + + shrink = genericShrink + +instance Arbitrary Const where + arbitrary = Test.QuickCheck.oneof [ pure Type, pure Kind, pure Sort ] + + shrink = genericShrink + +instance Arbitrary Directory where + arbitrary = lift1 Directory + + shrink = genericShrink + +averageDepth :: Natural +averageDepth = 3 + +averageNumberOfSubExpressions :: Double +averageNumberOfSubExpressions = 1 - 1 / fromIntegral averageDepth + +probabilityOfNullaryConstructor :: Double +probabilityOfNullaryConstructor = 1 / fromIntegral averageDepth + +numberOfConstructors :: Natural +numberOfConstructors = 50 + +instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where + arbitrary = + Test.QuickCheck.suchThat + (Test.QuickCheck.frequency + [ ( 7, lift1 Const) + , ( 7, lift1 Var) + , ( 1, Test.QuickCheck.oneof [ lift2 (Lam "_"), lift3 Lam ]) + , ( 1, Test.QuickCheck.oneof [ lift2 (Pi "_"), lift3 Pi ]) + , ( 1, lift2 App) + , let letExpression = do + n <- Test.QuickCheck.choose (0, 2) + binding <- arbitrary + bindings <- Test.QuickCheck.vectorOf n arbitrary + body <- arbitrary + return (Let (binding :| bindings) body) + in ( 1, Test.QuickCheck.oneof [ letExpression ]) + , ( 1, lift2 Annot) + , ( 7, lift0 Bool) + , ( 7, lift1 BoolLit) + , ( 1, lift2 BoolAnd) + , ( 1, lift2 BoolOr) + , ( 1, lift2 BoolEQ) + , ( 1, lift2 BoolNE) + , ( 1, lift3 BoolIf) + , ( 7, lift0 Natural) + , ( 7, fmap NaturalLit natural) + , ( 7, lift0 NaturalFold) + , ( 7, lift0 NaturalBuild) + , ( 7, lift0 NaturalIsZero) + , ( 7, lift0 NaturalEven) + , ( 7, lift0 NaturalOdd) + , ( 7, lift0 NaturalToInteger) + , ( 7, lift0 NaturalShow) + , ( 1, lift2 NaturalPlus) + , ( 1, lift2 NaturalTimes) + , ( 7, lift0 Integer) + , ( 7, fmap IntegerLit integer) + , ( 7, lift0 IntegerShow) + , ( 7, lift0 Double) + , ( 7, lift1 DoubleLit) + , ( 7, lift0 DoubleShow) + , ( 7, lift0 Text) + , ( 1, lift1 TextLit) + , ( 1, lift2 TextAppend) + , ( 7, lift0 List) + , let listLit = do + n <- Test.QuickCheck.choose (0, 3) + xs <- Test.QuickCheck.vectorOf n arbitrary + let ys = Data.Sequence.fromList xs + ListLit <$> arbitrary <*> pure ys + + in ( 1, listLit) + , ( 1, lift2 ListAppend) + , ( 7, lift0 ListBuild) + , ( 7, lift0 ListFold) + , ( 7, lift0 ListLength) + , ( 7, lift0 ListHead) + , ( 7, lift0 ListLast) + , ( 7, lift0 ListIndexed) + , ( 7, lift0 ListReverse) + , ( 7, lift0 Optional) + , ( 1, lift2 OptionalLit) + , ( 7, lift0 OptionalFold) + , ( 7, lift0 OptionalBuild) + , ( 1, lift1 Record) + , ( 1, lift1 RecordLit) + , ( 1, lift1 Union) + , ( 1, lift3 UnionLit) + , ( 1, lift2 Combine) + , ( 1, lift2 CombineTypes) + , ( 1, lift2 Prefer) + , ( 1, lift3 Merge) + , ( 1, lift1 Constructors) + , ( 1, lift2 Field) + , ( 1, lift2 Project) + , ( 7, lift1 Embed) + ] + ) + standardizedExpression + + shrink expression = filter standardizedExpression (genericShrink expression) + +standardizedExpression :: Expr s a -> Bool +standardizedExpression (ListLit Nothing xs) = not (Data.Sequence.null xs) +standardizedExpression (ListLit (Just _ ) xs) = Data.Sequence.null xs +standardizedExpression (Note _ _ ) = False +standardizedExpression _ = True + +instance Arbitrary File where + arbitrary = lift2 File + + shrink = genericShrink + +instance Arbitrary FilePrefix where + arbitrary = Test.QuickCheck.oneof [ pure Absolute, pure Here, pure Home ] + + shrink = genericShrink + +instance Arbitrary ImportType where + arbitrary = + Test.QuickCheck.suchThat + (Test.QuickCheck.oneof + [ lift2 Local + , lift5 (\a b c d e -> Remote (URL a b c d e Nothing)) + , lift1 Env + , lift0 Missing + ] + ) + standardizedImportType + + shrink importType = + filter standardizedImportType (genericShrink importType) + +standardizedImportType :: ImportType -> Bool +standardizedImportType (Remote (URL _ _ _ _ _ (Just _))) = False +standardizedImportType _ = True + +instance Arbitrary ImportHashed where + arbitrary = + Test.QuickCheck.suchThat + (lift1 (ImportHashed Nothing)) + standardizedImportHashed + + shrink (ImportHashed { importType = oldImportType, .. }) = do + newImportType <- shrink oldImportType + let importHashed = ImportHashed { importType = newImportType, .. } + guard (standardizedImportHashed importHashed) + return importHashed + +standardizedImportHashed :: ImportHashed -> Bool +standardizedImportHashed (ImportHashed (Just _) _) = False +standardizedImportHashed _ = True + +-- The standard does not yet specify how to encode `as Text`, so don't test it +-- yet +instance Arbitrary ImportMode where + arbitrary = lift0 Code + + shrink = genericShrink + +instance Arbitrary Import where + arbitrary = lift2 Import + + shrink = genericShrink + +instance Arbitrary Scheme where + arbitrary = Test.QuickCheck.oneof [ pure HTTP, pure HTTPS ] + + shrink = genericShrink + +instance Arbitrary URL where + arbitrary = lift6 URL + + shrink = genericShrink + +instance Arbitrary Var where + arbitrary = + Test.QuickCheck.oneof + [ fmap (V "_") natural + , lift1 (\t -> V t 0) + , lift1 V <*> natural + ] + + shrink = genericShrink + +binaryRoundtrip :: Expr () Import -> Property +binaryRoundtrip expression = + wrap + (fmap + Dhall.Binary.decodeWithVersion + (Codec.Serialise.deserialiseOrFail + (Codec.Serialise.serialise + (Dhall.Binary.encodeWithVersion Dhall.Binary.defaultStandardVersion expression) + ) + ) + ) + === wrap (Right (Right expression)) + where + wrap + :: Either DeserialiseFailure a + -> Either DeserialiseFailureWithEq a + wrap = Data.Coerce.coerce + +isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property +isNormalizedIsConsistentWithNormalize expression = + Dhall.Core.isNormalized expression + === (Dhall.Core.normalize expression == expression) + +isSameAsSelf :: Expr () Import -> Property +isSameAsSelf expression = + hasNoImportAndTypechecks ==> Dhall.Diff.same (Dhall.Diff.diffExpression expression expression) + where hasNoImportAndTypechecks = + case traverse (\_ -> Left ()) expression of + Right importlessExpression -> isRight (Dhall.TypeCheck.typeOf importlessExpression) + Left _ -> False + +tests :: TestTree +tests = + Test.Tasty.QuickCheck.testProperties + "QuickCheck" + [ ( "Binary serialization should round-trip" + , Test.QuickCheck.property binaryRoundtrip + ) + , ( "isNormalized should be consistent with normalize" + , Test.QuickCheck.property + (Test.QuickCheck.withMaxSuccess 10000 isNormalizedIsConsistentWithNormalize) + ) + , ( "An expression should have no difference with itself" + , Test.QuickCheck.property + (Test.QuickCheck.withMaxSuccess 10000 isSameAsSelf) + ) + ] diff --git a/tests/Dhall/Test/Regression.hs b/tests/Dhall/Test/Regression.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Regression.hs @@ -0,0 +1,239 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Regression where + +import qualified Control.Exception +import qualified Data.Text.Lazy.IO +import qualified Data.Text.Prettyprint.Doc +import qualified Data.Text.Prettyprint.Doc.Render.Text +import qualified Dhall +import qualified Dhall.Context +import qualified Dhall.Core +import qualified Dhall.Map +import qualified Dhall.Parser +import qualified Dhall.Pretty +import qualified Dhall.Test.Util as Util +import qualified Dhall.TypeCheck +import qualified System.Timeout +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +import Control.DeepSeq (($!!)) +import Dhall.Import (Imported) +import Dhall.Parser (Src) +import Dhall.TypeCheck (TypeError, X) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit ((@?=)) + +tests :: TestTree +tests = + Test.Tasty.testGroup "regression tests" + [ issue96 + , issue126 + , issue151 + , issue164 + , issue201 + , issue209 + , issue216 + , issue253 + , parsing0 + , typeChecking0 + , typeChecking1 + , typeChecking2 + , unnamedFields + , trailingSpaceAfterStringLiterals + ] + +data Foo = Foo Integer Bool | Bar Bool Bool Bool | Baz Integer Integer + deriving (Show, Dhall.Generic, Dhall.Interpret, Dhall.Inject) + +unnamedFields :: TestTree +unnamedFields = Test.Tasty.HUnit.testCase "Unnamed Fields" (do + let ty = Dhall.auto :: Dhall.Type Foo + Test.Tasty.HUnit.assertEqual "Good type" (Dhall.expected ty) + (Dhall.Core.Union + (Dhall.Map.fromList + [ ("Foo",Dhall.Core.Record (Dhall.Map.fromList [ + ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool)])) + , ("Bar",Dhall.Core.Record (Dhall.Map.fromList [ + ("_1",Dhall.Core.Bool),("_2",Dhall.Core.Bool),("_3",Dhall.Core.Bool)])) + , ("Baz",Dhall.Core.Record (Dhall.Map.fromList [ + ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Integer)])) + ] + ) + ) + + let inj = Dhall.inject :: Dhall.InputType Foo + Test.Tasty.HUnit.assertEqual "Good Inject" (Dhall.declared inj) (Dhall.expected ty) + + let tu_ty = Dhall.auto :: Dhall.Type (Integer, Bool) + Test.Tasty.HUnit.assertEqual "Auto Tuple" (Dhall.expected tu_ty) (Dhall.Core.Record ( + Dhall.Map.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool) ])) + + let tu_in = Dhall.inject :: Dhall.InputType (Integer, Bool) + Test.Tasty.HUnit.assertEqual "Inj. Tuple" (Dhall.declared tu_in) (Dhall.expected tu_ty) + + return () ) + +issue96 :: TestTree +issue96 = Test.Tasty.HUnit.testCase "Issue #96" (do + -- Verify that parsing should not fail + _ <- Util.code "\"bar'baz\"" + return () ) + +issue126 :: TestTree +issue126 = Test.Tasty.HUnit.testCase "Issue #126" (do + e <- Util.code "''\nfoo\nbar\n''" + Util.normalize' e @?= "''\nfoo\nbar\n''" ) + +issue151 :: TestTree +issue151 = Test.Tasty.HUnit.testCase "Issue #151" (do + let shouldNotTypeCheck text = do + let handler :: Imported (TypeError Src X) -> IO Bool + handler _ = return True + + let typeCheck = do + _ <- Util.code text + return False + b <- Control.Exception.handle handler typeCheck + Test.Tasty.HUnit.assertBool "The expression should not type-check" b + + -- These two examples contain the following expression that loops infinitely + -- if you normalize the expression before type-checking the expression: + -- + -- (λ(x : A) → x x) (λ(x : A) → x x) + -- + -- There was a bug in the Dhall type-checker were expressions were not + -- being type-checked before being added to the context (which is a + -- violation of the standard type-checking rules for a pure type system). + -- The reason this is problematic is that several places in the + -- type-checking logic assume that the context is safe to normalize. + -- + -- Both of these examples exercise area of the type-checker logic that + -- assume that the context is normalized. If you fail to type-check terms + -- before adding them to the context then this test will "fail" with an + -- infinite loop. This test "succeeds" if the examples terminate + -- immediately with a type-checking failure. + shouldNotTypeCheck "./tests/regression/issue151a.dhall" + shouldNotTypeCheck "./tests/regression/issue151b.dhall" ) + +issue164 :: TestTree +issue164 = Test.Tasty.HUnit.testCase "Issue #164" (do + -- Verify that parsing should not fail on a single-quote within a + -- single-quoted string + _ <- Util.code "./tests/regression/issue164.dhall" + return () ) + +issue201 :: TestTree +issue201 = Test.Tasty.HUnit.testCase "Issue #201" (do + -- Verify that type synonyms work + _ <- Util.code "./tests/regression/issue201.dhall" + return () ) + +issue209 :: TestTree +issue209 = Test.Tasty.HUnit.testCase "Issue #209" (do + -- Verify that pretty-printing `constructors` doesn't trigger an infinite + -- loop + e <- Util.code "./tests/regression/issue209.dhall" + let text = Dhall.Core.pretty e + Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $!! text) + return () ) + +issue216 :: TestTree +issue216 = Test.Tasty.HUnit.testCase "Issue #216" (do + -- Verify that pretty-printing preserves string interpolation + e <- Util.code "./tests/regression/issue216a.dhall" + let doc = Data.Text.Prettyprint.Doc.pretty e + let docStream = Data.Text.Prettyprint.Doc.layoutSmart Dhall.Pretty.layoutOpts doc + let text0 = Data.Text.Prettyprint.Doc.Render.Text.renderLazy docStream + + text1 <- Data.Text.Lazy.IO.readFile "./tests/regression/issue216b.dhall" + + Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 ) + +issue253 :: TestTree +issue253 = Test.Tasty.HUnit.testCase "Issue #253" (do + -- Verify that type-checking rejects ill-formed custom contexts + let context = Dhall.Context.insert "x" "x" Dhall.Context.empty + let result = Dhall.TypeCheck.typeWith context "x" + + -- If the context is not validated correctly then type-checking will + -- infinitely loop + Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $! result) + return () ) + +parsing0 :: TestTree +parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do + -- Verify that parsing should not fail + -- + -- In 267093f8cddf1c2f909f2d997c31fd0a7cb2440a I broke the parser when left + -- factoring the grammer by failing to handle the source tested by this + -- regression test. The root of the problem was that the parser was trying + -- to parse `List ./Node` as `Field List "/Node"` instead of + -- `App List (Embed (Path (File Homeless "./Node") Code))`. The latter is + -- the correct parse because `/Node` is not a valid field label, but the + -- mistaken parser was committed to the incorrect parse and never attempted + -- the correct parse. + case Dhall.Parser.exprFromText mempty "List ./Node" of + Left e -> Control.Exception.throwIO e + Right _ -> return () ) + +typeChecking0 :: TestTree +typeChecking0 = Test.Tasty.HUnit.testCase "Type-checking regression #0" (do + -- There used to be a bug in the type-checking logic where `T` would be + -- added to the context when inferring the type of `λ(x : T) → x`, but was + -- missing from the context when inferring the kind of the inferred type + -- (i.e. the kind of `∀(x : T) → T`). This led to an unbound variable + -- error when inferring the kind + -- + -- This bug was originally reported in issue #10 + _ <- Util.code "let Day : Type = Natural in λ(x : Day) → x" + return () ) + +typeChecking1 :: TestTree +typeChecking1 = Test.Tasty.HUnit.testCase "Type-checking regression #1" (do + -- There used to be a bug in the type-checking logic when inferring the + -- type of `let`. Specifically, given an expression of the form: + -- + -- let x : t = e1 in e2 + -- + -- ... the type-checker would not substitute `x` for `e1` in the inferred + -- of the `let` expression. This meant that if the inferred type contained + -- any references to `x` then these references would escape their scope and + -- result in unbound variable exceptions + -- + -- This regression test exercises that code path by creating a `let` + -- expression where the inferred type before substitution (`∀(x : b) → b` in + -- this example), contains a reference to the `let`-bound variable (`b`) + -- that needs to be substituted with `a` in order to produce the final + -- correct inferred type (`∀(x : a) → a`). If this test passes then + -- substitution worked correctly. If substitution doesn't occur then you + -- expect an `Unbound variable` error from `b` escaping its scope due to + -- being returned as part of the inferred type + _ <- Util.code "λ(a : Type) → let b : Type = a in λ(x : b) → x" + return () ) + +typeChecking2 :: TestTree +typeChecking2 = Test.Tasty.HUnit.testCase "Type-checking regression #2" (do + -- There used to be a bug in the type-checking logic where `let` bound + -- variables would not correctly shadow variables of the same name when + -- inferring the type of of the `let` expression + -- + -- This example exercises this code path with a `let` expression where the + -- `let`-bound variable (`a`) has the same name as its own type (`a`). If + -- shadowing works correctly then the final `a` in the expression should + -- refer to the `let`-bound variable and not its type. An invalid reference + -- to the shadowed type `a` would result in an invalid dependently typed + -- function + _ <- Util.code "λ(a : Type) → λ(x : a) → let a : a = x in a" + return () ) + +trailingSpaceAfterStringLiterals :: TestTree +trailingSpaceAfterStringLiterals = + Test.Tasty.HUnit.testCase "Trailing space after string literals" (do + -- Verify that string literals parse correctly with trailing space + -- (Yes, I did get this wrong at some point) + _ <- Util.code "(''\nABC'' ++ \"DEF\" )" + return () ) diff --git a/tests/Dhall/Test/Tutorial.hs b/tests/Dhall/Test/Tutorial.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Tutorial.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.Tutorial where + +import qualified Data.Vector +import qualified Dhall +import qualified Dhall.Test.Util as Util +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +import Data.Monoid ((<>)) +import Data.Text (Text) +import Dhall (Inject) +import GHC.Generics (Generic) +import Numeric.Natural (Natural) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit ((@?=)) + +tests :: TestTree +tests = + Test.Tasty.testGroup "tutorial" + [ Test.Tasty.testGroup "Interpolation" + [ _Interpolation_0 + , _Interpolation_1 + ] + , Test.Tasty.testGroup "Functions" + [ _Functions_0 + , _Functions_1 + , _Functions_2 + ] + , Test.Tasty.testGroup "Unions" + [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall" + , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall" + , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall" + , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall" + , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall" + ] + ] + +_Interpolation_0 :: TestTree +_Interpolation_0 = Test.Tasty.HUnit.testCase "Example #0" (do + e <- Util.code + " let name = \"John Doe\" \n\ + \in let age = 21 \n\ + \in \"My name is ${name} and my age is ${Natural/show age}\"\n" + Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" ) + +_Interpolation_1 :: TestTree +_Interpolation_1 = Test.Tasty.HUnit.testCase "Example #1" (do + e <- Util.code + "''\n\ + \ for file in *; do \n\ + \ echo \"Found ''${file}\"\n\ + \ done \n\ + \'' \n" + Util.assertNormalized e ) + +_Functions_0 :: TestTree +_Functions_0 = Test.Tasty.HUnit.testCase "Example #0" (do + let text = "\\(n : Bool) -> [ n && True, n && False, n || True, n || False ]" + makeBools <- Dhall.input Dhall.auto text + makeBools True @?= Data.Vector.fromList [True,False,True,True] ) + +_Functions_1 :: TestTree +_Functions_1 = Test.Tasty.HUnit.testCase "Example #1" (do + let text = "λ(x : Bool) → λ(y : Bool) → x && y" + makeBools <- Dhall.input Dhall.auto text + makeBools True False @?= False ) + +data Example0 = Example0 { foo :: Bool, bar :: Bool } + deriving (Generic, Inject) + +_Functions_2 :: TestTree +_Functions_2 = Test.Tasty.HUnit.testCase "Example #2" (do + f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" + f (Example0 { foo = True, bar = False }) @?= False + f (Example0 { foo = True, bar = True }) @?= True ) + +example :: Natural -> Text -> Text -> TestTree +example n text0 text1 = + Test.Tasty.HUnit.testCase + ("Example #" <> show n) + (Util.equivalent text0 text1) diff --git a/tests/Dhall/Test/TypeCheck.hs b/tests/Dhall/Test/TypeCheck.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/TypeCheck.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Test.TypeCheck where + +import Data.Monoid (mempty, (<>)) +import Data.Text (Text) +import Dhall.Import (Imported) +import Dhall.Parser (Src) +import Dhall.TypeCheck (TypeError, X) +import Test.Tasty (TestTree) + +import qualified Control.Exception +import qualified Data.Text +import qualified Dhall.Core +import qualified Dhall.Import +import qualified Dhall.Parser +import qualified Dhall.TypeCheck +import qualified Test.Tasty +import qualified Test.Tasty.HUnit + +tests :: TestTree +tests = + Test.Tasty.testGroup "typecheck tests" + [ preludeExamples + , accessTypeChecks + , should + "allow type-valued fields in a record" + "success/simple/fieldsAreTypes" + , should + "allow type-valued alternatives in a union" + "success/simple/alternativesAreTypes" + , should + "allow anonymous functions in types to be judgmentally equal" + "success/simple/anonymousFunctionsInTypes" + , should + "correctly handle α-equivalent merge alternatives" + "success/simple/mergeEquivalence" + , should + "allow Kind variables" + "success/simple/kindParameter" + , shouldNotTypeCheck + "combining records of terms and types" + "failure/combineMixedRecords" + , shouldNotTypeCheck + "preferring a record of types over a record of terms" + "failure/preferMixedRecords" + , should + "allow records of types of mixed kinds" + "success/recordOfTypes" + , should + "allow accessing a type from a record" + "success/accessType" + , should + "allow accessing a type from a Boehm-Berarducci-encoded record" + "success/accessEncodedType" + , shouldNotTypeCheck + "Hurkens' paradox" + "failure/hurkensParadox" + , should + "allow accessing a constructor from a type stored inside a record" + "success/simple/mixedFieldAccess" + , should + "allow a record of a record of types" + "success/recordOfRecordOfTypes" + , should + "allow a union of types of of mixed kinds" + "success/simple/unionsOfTypes" + , shouldNotTypeCheck + "Unions mixing terms and and types" + "failure/mixedUnions" + ] + +preludeExamples :: TestTree +preludeExamples = + Test.Tasty.testGroup "Prelude examples" + [ should "Monoid" "./success/prelude/Monoid/00" + , should "Monoid" "./success/prelude/Monoid/01" + , should "Monoid" "./success/prelude/Monoid/02" + , should "Monoid" "./success/prelude/Monoid/03" + , should "Monoid" "./success/prelude/Monoid/04" + , should "Monoid" "./success/prelude/Monoid/05" + , should "Monoid" "./success/prelude/Monoid/06" + , should "Monoid" "./success/prelude/Monoid/07" + , should "Monoid" "./success/prelude/Monoid/08" + , should "Monoid" "./success/prelude/Monoid/09" + , should "Monoid" "./success/prelude/Monoid/10" + ] + +accessTypeChecks :: TestTree +accessTypeChecks = + Test.Tasty.testGroup "typecheck access" + [ should "record" "./success/simple/access/0" + , should "record" "./success/simple/access/1" + ] + +should :: Text -> Text -> TestTree +should name basename = + Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do + let actualCode = "./tests/typecheck/" <> basename <> "A.dhall" + let expectedCode = "./tests/typecheck/" <> basename <> "B.dhall" + + actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + let annotatedExpr = Dhall.Core.Annot actualExpr expectedExpr + + resolvedExpr <- Dhall.Import.load annotatedExpr + case Dhall.TypeCheck.typeOf resolvedExpr of + Left err -> Control.Exception.throwIO err + Right _ -> return () + +shouldNotTypeCheck :: Text -> Text -> TestTree +shouldNotTypeCheck name basename = + Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do + let code = "./tests/typecheck/" <> basename <> ".dhall" + + expression <- case Dhall.Parser.exprFromText mempty code of + Left exception -> Control.Exception.throwIO exception + Right expression -> return expression + + let io :: IO Bool + io = do + _ <- Dhall.Import.load expression + return True + + let handler :: Imported (TypeError Src X)-> IO Bool + handler _ = return False + + typeChecked <- Control.Exception.handle handler io + + if typeChecked + then fail (Data.Text.unpack code <> " should not have type-checked") + else return () diff --git a/tests/Dhall/Test/Util.hs b/tests/Dhall/Test/Util.hs new file mode 100644 --- /dev/null +++ b/tests/Dhall/Test/Util.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} + +module Dhall.Test.Util + ( code + , codeWith + , equivalent + , normalize' + , normalizeWith' + , assertNormalizesTo + , assertNormalizesToWith + , assertNormalized + , assertTypeChecks + ) where + +import qualified Control.Exception +import qualified Data.Functor +import Data.Bifunctor (first) +import Data.Text (Text) +import qualified Dhall.Core +import Dhall.Core (Expr, Normalizer) +import qualified Dhall.Context +import Dhall.Context (Context) +import qualified Dhall.Import +import qualified Dhall.Parser +import Dhall.Parser (Src) +import qualified Dhall.TypeCheck +import Dhall.TypeCheck (X) +import Test.Tasty.HUnit + +normalize' :: Expr Src X -> Text +normalize' = Dhall.Core.pretty . Dhall.Core.normalize + +normalizeWith' :: Normalizer X -> Expr Src X -> Text +normalizeWith' ctx = Dhall.Core.pretty . Dhall.Core.normalizeWith ctx + +code :: Text -> IO (Expr Src X) +code = codeWith Dhall.Context.empty + +codeWith :: Context (Expr Src X) -> Text -> IO (Expr Src X) +codeWith ctx expr = do + expr0 <- case Dhall.Parser.exprFromText mempty expr of + Left parseError -> Control.Exception.throwIO parseError + Right expr0 -> return expr0 + expr1 <- Dhall.Import.load expr0 + case Dhall.TypeCheck.typeWith ctx expr1 of + Left typeError -> Control.Exception.throwIO typeError + Right _ -> return () + return expr1 + +equivalent :: Text -> Text -> IO () +equivalent text0 text1 = do + expr0 <- fmap Dhall.Core.normalize (code text0) :: IO (Expr X X) + expr1 <- fmap Dhall.Core.normalize (code text1) :: IO (Expr X X) + assertEqual "Expressions are not equivalent" expr0 expr1 + +assertNormalizesTo :: Expr Src X -> Text -> IO () +assertNormalizesTo e expected = do + assertBool msg (not $ Dhall.Core.isNormalized e) + normalize' e @?= expected + where msg = "Given expression is already in normal form" + +assertNormalizesToWith :: Normalizer X -> Expr Src X -> Text -> IO () +assertNormalizesToWith ctx e expected = do + assertBool msg (not $ Dhall.Core.isNormalizedWith ctx (first (const ()) e)) + normalizeWith' ctx e @?= expected + where msg = "Given expression is already in normal form" + +assertNormalized :: Expr Src X -> IO () +assertNormalized e = do + assertBool msg1 (Dhall.Core.isNormalized e) + assertEqual msg2 (normalize' e) (Dhall.Core.pretty e) + where msg1 = "Expression was not in normal form" + msg2 = "Normalization is not supposed to change the expression" + +assertTypeChecks :: Text -> IO () +assertTypeChecks text = Data.Functor.void (code text) diff --git a/tests/Format.hs b/tests/Format.hs deleted file mode 100644 --- a/tests/Format.hs +++ /dev/null @@ -1,110 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Format where - -import Data.Monoid (mempty, (<>)) -import Data.Text (Text) -import Dhall.Pretty (CharacterSet(..)) -import Test.Tasty (TestTree) - -import qualified Control.Exception -import qualified Data.Text -import qualified Data.Text.IO -import qualified Data.Text.Prettyprint.Doc -import qualified Data.Text.Prettyprint.Doc.Render.Text -import qualified Dhall.Parser -import qualified Dhall.Pretty -import qualified Test.Tasty -import qualified Test.Tasty.HUnit - -formatTests :: TestTree -formatTests = - Test.Tasty.testGroup "format tests" - [ should - Unicode - "prefer multi-line strings when newlines present" - "multiline" - , should - Unicode - "escape ${ for single-quoted strings" - "escapeSingleQuotedOpenInterpolation" - , should - Unicode - "preserve the original order of fields" - "fieldOrder" - , should - Unicode - "preserve the original order of projections" - "projectionOrder" - , should - Unicode - "escape numeric labels correctly" - "escapeNumericLabel" - , should - Unicode - "correctly handle scientific notation with a large exponent" - "largeExponent" - , should - Unicode - "round a double to the nearest representable value. Ties go to even least significant bit" - "doubleRound" - , should - Unicode - "correctly format the empty record literal" - "emptyRecord" - , should - Unicode - "indent then/else to the same column" - "ifThenElse" - , should - Unicode - "handle indenting long imports correctly without trailing space per line" - "importLines" - , should - Unicode - "handle indenting small imports correctly without trailing space inline" - "importLines2" - , should - Unicode - "not remove parentheses when accessing a field of a record" - "importAccess" - , should - Unicode - "handle formatting sha256 imports correctly" - "sha256Printing" - , should - Unicode - "handle formatting of Import suffix correctly" - "importSuffix" - , should - ASCII - "be able to format with ASCII characters" - "ascii" - , should - Unicode - "preserve Unicode characters" - "unicode" - ] - -should :: CharacterSet -> Text -> Text -> TestTree -should characterSet name basename = - Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do - let inputFile = - Data.Text.unpack ("./tests/format/" <> basename <> "A.dhall") - let outputFile = - Data.Text.unpack ("./tests/format/" <> basename <> "B.dhall") - inputText <- Data.Text.IO.readFile inputFile - - expr <- case Dhall.Parser.exprFromText mempty inputText of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - - let doc = Dhall.Pretty.prettyCharacterSet characterSet expr - let docStream = Data.Text.Prettyprint.Doc.layoutSmart Dhall.Pretty.layoutOpts doc - let actualText = Data.Text.Prettyprint.Doc.Render.Text.renderStrict docStream - - expectedText <- Data.Text.IO.readFile outputFile - - let message = - "The formatted expression did not match the expected output" - Test.Tasty.HUnit.assertEqual message expectedText actualText diff --git a/tests/Import.hs b/tests/Import.hs deleted file mode 100644 --- a/tests/Import.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Import where - -import Data.Text (Text) -import Test.Tasty (TestTree) -import Dhall.Import (MissingImports(..)) -import Control.Exception (catch, throwIO) -import Data.Monoid ((<>)) - -import qualified Control.Monad.Trans.State.Strict as State -import qualified Data.Text -import qualified Data.Text.IO -import qualified Dhall.Parser -import qualified Dhall.Import -import qualified Test.Tasty -import qualified Test.Tasty.HUnit - -importTests :: TestTree -importTests = - Test.Tasty.testGroup "import tests" - [ Test.Tasty.testGroup "import alternatives" - [ shouldFail - 3 - "alternative of several unset env variables" - "./tests/import/failure/alternativeEnv.dhall" - , shouldFail - 1 - "alternative of env variable and missing" - "./tests/import/failure/alternativeEnvMissing.dhall" - , shouldFail - 0 - "just missing" - "./tests/import/failure/missing.dhall" - , shouldNotFail - "alternative of env variable, missing, and a Natural" - "./tests/import/success/alternativeEnvNaturalA.dhall" - , shouldNotFail - "alternative of env variable and a Natural" - "./tests/import/success/alternativeEnvSimpleA.dhall" - , shouldNotFail - "alternative of a Natural and missing" - "./tests/import/success/alternativeNaturalA.dhall" - ] - , Test.Tasty.testGroup "import relative to argument" - [ shouldNotFailRelative - "works" - "./tests/import/data/foo/bar" - "./tests/import/success/relative.dhall" - , shouldNotFailRelative - "a semantic integrity check if fields are reordered" - "./tests/import/success/" - "./tests/import/success/fieldOrderA.dhall" - , shouldNotFailRelative - "a semantic integrity check when importing an expression using `constructors`" - "./tests/import/success/" - "./tests/import/success/issue553B.dhall" - ] - ] - -shouldNotFail :: Text -> FilePath -> TestTree -shouldNotFail name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do - text <- Data.Text.IO.readFile path - actualExpr <- case Dhall.Parser.exprFromText mempty text of - Left err -> throwIO err - Right expr -> return expr - _ <- Dhall.Import.load actualExpr - return ()) - -shouldNotFailRelative :: Text -> FilePath -> FilePath -> TestTree -shouldNotFailRelative name dir path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do - text <- Data.Text.IO.readFile path - expr <- case Dhall.Parser.exprFromText mempty text of - Left err -> throwIO err - Right expr -> return expr - - _ <- State.evalStateT (Dhall.Import.loadWith expr) (Dhall.Import.emptyStatus dir) - - return ()) - -shouldFail :: Int -> Text -> FilePath -> TestTree -shouldFail failures name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do - text <- Data.Text.IO.readFile path - actualExpr <- case Dhall.Parser.exprFromText mempty text of - Left err -> throwIO err - Right expr -> return expr - catch - (do - _ <- Dhall.Import.load actualExpr - fail "Import should have failed, but it succeeds") - (\(MissingImports es) -> case length es == failures of - True -> pure () - False -> fail ("Should have failed " - <> show failures - <> " times, but failed with: \n" - <> show es)) ) diff --git a/tests/Lint.hs b/tests/Lint.hs deleted file mode 100644 --- a/tests/Lint.hs +++ /dev/null @@ -1,58 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Lint where - -import Data.Monoid (mempty, (<>)) -import Data.Text (Text) -import Test.Tasty (TestTree) - -import qualified Control.Exception -import qualified Data.Text -import qualified Data.Text.IO -import qualified Dhall.Core -import qualified Dhall.Import -import qualified Dhall.Lint -import qualified Dhall.Parser -import qualified Test.Tasty -import qualified Test.Tasty.HUnit - -lintTests :: TestTree -lintTests = - Test.Tasty.testGroup "format tests" - [ should - "correctly handle multi-let expressions" - "success/multilet" - ] - -should :: Text -> Text -> TestTree -should name basename = - Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do - let inputFile = - Data.Text.unpack ("./tests/lint/" <> basename <> "A.dhall") - let outputFile = - Data.Text.unpack ("./tests/lint/" <> basename <> "B.dhall") - - inputText <- Data.Text.IO.readFile inputFile - - parsedInput <- case Dhall.Parser.exprFromText mempty inputText of - Left exception -> Control.Exception.throwIO exception - Right expression -> return expression - - let lintedInput = Dhall.Lint.lint parsedInput - - actualExpression <- Dhall.Import.load lintedInput - - outputText <- Data.Text.IO.readFile outputFile - - parsedOutput <- case Dhall.Parser.exprFromText mempty outputText of - Left exception -> Control.Exception.throwIO exception - Right expression -> return expression - - resolvedOutput <- Dhall.Import.load parsedOutput - - let expectedExpression = Dhall.Core.denote resolvedOutput - - let message = - "The linted expression did not match the expected output" - - Test.Tasty.HUnit.assertEqual message expectedExpression actualExpression diff --git a/tests/Normalization.hs b/tests/Normalization.hs deleted file mode 100644 --- a/tests/Normalization.hs +++ /dev/null @@ -1,275 +0,0 @@ -{-# LANGUAGE OverloadedLists #-} -{-# LANGUAGE OverloadedStrings #-} - -module Normalization (normalizationTests) where - -import Data.Monoid ((<>)) -import Data.Text (Text) -import Dhall.Core (Expr) -import Dhall.TypeCheck (X) - -import qualified Control.Exception -import qualified Data.Text -import qualified Dhall.Core -import qualified Dhall.Import -import qualified Dhall.Parser -import qualified Dhall.TypeCheck - -import Dhall.Core -import Dhall.Context -import Test.Tasty -import Test.Tasty.HUnit -import Util - -normalizationTests :: TestTree -normalizationTests = - testGroup "normalization" - [ tutorialExamples - , preludeExamples - , simplifications - , constantFolding - , conversions - , shouldNormalize "Optional build/fold fusion" "success/simple/optionalBuildFold" - , customization - , shouldNormalize "a remote-systems.conf builder" "success/remoteSystems" - , shouldNormalize "multi-line strings correctly" "success/simple/multiLine" - , shouldNormalize "the // operator and sort the fields" "success/simple/sortOperator" - ] - -tutorialExamples :: TestTree -tutorialExamples = - testGroup "Tutorial examples" - [ shouldNormalize "⩓" "./success/haskell-tutorial/combineTypes/0" - , shouldNormalize "//\\\\" "./success/haskell-tutorial/combineTypes/1" - , shouldNormalize "//" "./success/haskell-tutorial/prefer/0" - , shouldNormalize "projection" "./success/haskell-tutorial/projection/0" - , shouldNormalize "access record" "./success/haskell-tutorial/access/0" - , shouldNormalize "access union" "./success/haskell-tutorial/access/1" - ] - -preludeExamples :: TestTree -preludeExamples = - testGroup "Prelude examples" - [ shouldNormalize "Bool/and" "./success/prelude/Bool/and/0" - , shouldNormalize "Bool/and" "./success/prelude/Bool/and/1" - , shouldNormalize "Bool/build" "./success/prelude/Bool/build/0" - , shouldNormalize "Bool/build" "./success/prelude/Bool/build/1" - , shouldNormalize "Bool/even" "./success/prelude/Bool/even/0" - , shouldNormalize "Bool/even" "./success/prelude/Bool/even/1" - , shouldNormalize "Bool/even" "./success/prelude/Bool/even/2" - , shouldNormalize "Bool/even" "./success/prelude/Bool/even/3" - , shouldNormalize "Bool/fold" "./success/prelude/Bool/fold/0" - , shouldNormalize "Bool/fold" "./success/prelude/Bool/fold/1" - , shouldNormalize "Bool/not" "./success/prelude/Bool/not/0" - , shouldNormalize "Bool/not" "./success/prelude/Bool/not/1" - , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/0" - , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/1" - , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/2" - , shouldNormalize "Bool/odd" "./success/prelude/Bool/odd/3" - , shouldNormalize "Bool/or" "./success/prelude/Bool/or/0" - , shouldNormalize "Bool/or" "./success/prelude/Bool/or/1" - , shouldNormalize "Bool/show" "./success/prelude/Bool/show/0" - , shouldNormalize "Bool/show" "./success/prelude/Bool/show/1" - , shouldNormalize "Double/show" "./success/prelude/Double/show/0" - , shouldNormalize "Double/show" "./success/prelude/Double/show/1" - , shouldNormalize "Integer/show" "./success/prelude/Integer/show/0" - , shouldNormalize "Integer/show" "./success/prelude/Integer/show/1" - , shouldNormalize "Integer/toDouble" "./success/prelude/Integer/toDouble/0" - , shouldNormalize "Integer/toDouble" "./success/prelude/Integer/toDouble/1" - , shouldNormalize "List/all" "./success/prelude/List/all/0" - , shouldNormalize "List/all" "./success/prelude/List/all/1" - , shouldNormalize "List/any" "./success/prelude/List/any/0" - , shouldNormalize "List/any" "./success/prelude/List/any/1" - , shouldNormalize "List/build" "./success/prelude/List/build/0" - , shouldNormalize "List/build" "./success/prelude/List/build/1" - , shouldNormalize "List/concat" "./success/prelude/List/concat/0" - , shouldNormalize "List/concat" "./success/prelude/List/concat/1" - , shouldNormalize "List/concatMap" "./success/prelude/List/concatMap/0" - , shouldNormalize "List/concatMap" "./success/prelude/List/concatMap/1" - , shouldNormalize "List/filter" "./success/prelude/List/filter/0" - , shouldNormalize "List/filter" "./success/prelude/List/filter/1" - , shouldNormalize "List/fold" "./success/prelude/List/fold/0" - , shouldNormalize "List/fold" "./success/prelude/List/fold/1" - , shouldNormalize "List/fold" "./success/prelude/List/fold/2" - , shouldNormalize "List/generate" "./success/prelude/List/generate/0" - , shouldNormalize "List/generate" "./success/prelude/List/generate/1" - , shouldNormalize "List/head" "./success/prelude/List/head/0" - , shouldNormalize "List/head" "./success/prelude/List/head/1" - , shouldNormalize "List/indexed" "./success/prelude/List/indexed/0" - , shouldNormalize "List/indexed" "./success/prelude/List/indexed/1" - , shouldNormalize "List/iterate" "./success/prelude/List/iterate/0" - , shouldNormalize "List/iterate" "./success/prelude/List/iterate/1" - , shouldNormalize "List/last" "./success/prelude/List/last/0" - , shouldNormalize "List/last" "./success/prelude/List/last/1" - , shouldNormalize "List/length" "./success/prelude/List/length/0" - , shouldNormalize "List/length" "./success/prelude/List/length/1" - , shouldNormalize "List/map" "./success/prelude/List/map/0" - , shouldNormalize "List/map" "./success/prelude/List/map/1" - , shouldNormalize "List/null" "./success/prelude/List/null/0" - , shouldNormalize "List/null" "./success/prelude/List/null/1" - , shouldNormalize "List/replicate" "./success/prelude/List/replicate/0" - , shouldNormalize "List/replicate" "./success/prelude/List/replicate/1" - , shouldNormalize "List/reverse" "./success/prelude/List/reverse/0" - , shouldNormalize "List/reverse" "./success/prelude/List/reverse/1" - , shouldNormalize "List/shifted" "./success/prelude/List/shifted/0" - , shouldNormalize "List/shifted" "./success/prelude/List/shifted/1" - , shouldNormalize "List/unzip" "./success/prelude/List/unzip/0" - , shouldNormalize "List/unzip" "./success/prelude/List/unzip/1" - , shouldNormalize "Natural/build" "./success/prelude/Natural/build/0" - , shouldNormalize "Natural/build" "./success/prelude/Natural/build/1" - , shouldNormalize "Natural/enumerate" "./success/prelude/Natural/enumerate/0" - , shouldNormalize "Natural/enumerate" "./success/prelude/Natural/enumerate/1" - , shouldNormalize "Natural/even" "./success/prelude/Natural/even/0" - , shouldNormalize "Natural/even" "./success/prelude/Natural/even/1" - , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/0" - , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/1" - , shouldNormalize "Natural/fold" "./success/prelude/Natural/fold/2" - , shouldNormalize "Natural/isZero" "./success/prelude/Natural/isZero/0" - , shouldNormalize "Natural/isZero" "./success/prelude/Natural/isZero/1" - , shouldNormalize "Natural/odd" "./success/prelude/Natural/odd/0" - , shouldNormalize "Natural/odd" "./success/prelude/Natural/odd/1" - , shouldNormalize "Natural/product" "./success/prelude/Natural/product/0" - , shouldNormalize "Natural/product" "./success/prelude/Natural/product/1" - , shouldNormalize "Natural/show" "./success/prelude/Natural/show/0" - , shouldNormalize "Natural/show" "./success/prelude/Natural/show/1" - , shouldNormalize "Natural/sum" "./success/prelude/Natural/sum/0" - , shouldNormalize "Natural/sum" "./success/prelude/Natural/sum/1" - , shouldNormalize "Natural/toDouble" "./success/prelude/Natural/toDouble/0" - , shouldNormalize "Natural/toDouble" "./success/prelude/Natural/toDouble/1" - , shouldNormalize "Natural/toInteger" "./success/prelude/Natural/toInteger/0" - , shouldNormalize "Natural/toInteger" "./success/prelude/Natural/toInteger/1" - , shouldNormalize "Optional/all" "./success/prelude/Optional/all/0" - , shouldNormalize "Optional/all" "./success/prelude/Optional/all/1" - , shouldNormalize "Optional/any" "./success/prelude/Optional/any/0" - , shouldNormalize "Optional/any" "./success/prelude/Optional/any/1" - , shouldNormalize "Optional/build" "./success/prelude/Optional/build/0" - , shouldNormalize "Optional/build" "./success/prelude/Optional/build/1" - , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/0" - , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/1" - , shouldNormalize "Optional/concat" "./success/prelude/Optional/concat/2" - , shouldNormalize "Optional/filter" "./success/prelude/Optional/filter/0" - , shouldNormalize "Optional/filter" "./success/prelude/Optional/filter/1" - , shouldNormalize "Optional/fold" "./success/prelude/Optional/fold/0" - , shouldNormalize "Optional/fold" "./success/prelude/Optional/fold/1" - , shouldNormalize "Optional/head" "./success/prelude/Optional/head/0" - , shouldNormalize "Optional/head" "./success/prelude/Optional/head/1" - , shouldNormalize "Optional/head" "./success/prelude/Optional/head/2" - , shouldNormalize "Optional/last" "./success/prelude/Optional/last/0" - , shouldNormalize "Optional/last" "./success/prelude/Optional/last/1" - , shouldNormalize "Optional/last" "./success/prelude/Optional/last/2" - , shouldNormalize "Optional/length" "./success/prelude/Optional/length/0" - , shouldNormalize "Optional/length" "./success/prelude/Optional/length/1" - , shouldNormalize "Optional/map" "./success/prelude/Optional/map/0" - , shouldNormalize "Optional/map" "./success/prelude/Optional/map/1" - , shouldNormalize "Optional/null" "./success/prelude/Optional/null/0" - , shouldNormalize "Optional/null" "./success/prelude/Optional/null/1" - , shouldNormalize "Optional/toList" "./success/prelude/Optional/toList/0" - , shouldNormalize "Optional/toList" "./success/prelude/Optional/toList/1" - , shouldNormalize "Optional/unzip" "./success/prelude/Optional/unzip/0" - , shouldNormalize "Optional/unzip" "./success/prelude/Optional/unzip/1" - , shouldNormalize "Text/concat" "./success/prelude/Text/concat/0" - , shouldNormalize "Text/concat" "./success/prelude/Text/concat/1" - , shouldNormalize "Text/concatMap" "./success/prelude/Text/concatMap/0" - , shouldNormalize "Text/concatMap" "./success/prelude/Text/concatMap/1" - , shouldNormalize "Text/concatMapSep" "./success/prelude/Text/concatMapSep/0" - , shouldNormalize "Text/concatMapSep" "./success/prelude/Text/concatMapSep/1" - , shouldNormalize "Text/concatSep" "./success/prelude/Text/concatSep/0" - , shouldNormalize "Text/concatSep" "./success/prelude/Text/concatSep/1" - ] - -simplifications :: TestTree -simplifications = - testGroup "Simplifications" - [ shouldNormalize "if/then/else" "./success/simplifications/ifThenElse" - , shouldNormalize "||" "./success/simplifications/or" - , shouldNormalize "&&" "./success/simplifications/and" - , shouldNormalize "==" "./success/simplifications/eq" - , shouldNormalize "!=" "./success/simplifications/ne" - ] - -constantFolding :: TestTree -constantFolding = - testGroup "folding of constants" - [ shouldNormalize "Natural/plus" "success/simple/naturalPlus" - , shouldNormalize "Optional/fold" "success/simple/optionalFold" - , shouldNormalize "Optional/build" "success/simple/optionalBuild" - , shouldNormalize "Natural/build" "success/simple/naturalBuild" - ] - -conversions :: TestTree -conversions = - testGroup "conversions" - [ shouldNormalize "Natural/show" "success/simple/naturalShow" - , shouldNormalize "Integer/show" "success/simple/integerShow" - , shouldNormalize "Double/show" "success/simple/doubleShow" - , shouldNormalize "Natural/toInteger" "success/simple/naturalToInteger" - , shouldNormalize "Integer/toDouble" "success/simple/integerToDouble" - ] - -customization :: TestTree -customization = - testGroup "customization" - [ simpleCustomization - , nestedReduction - ] - -simpleCustomization :: TestTree -simpleCustomization = testCase "simpleCustomization" $ do - let tyCtx = insert "min" (Pi "_" Natural (Pi "_" Natural Natural)) empty - valCtx e = case e of - (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> pure (Just (NaturalLit (min x y))) - _ -> pure Nothing - e <- codeWith tyCtx "min (min 11 12) 8 + 1" - assertNormalizesToWith valCtx e "9" - -nestedReduction :: TestTree -nestedReduction = testCase "doubleReduction" $ do - minType <- insert "min" <$> code "Natural → Natural → Natural" - fiveorlessType <- insert "fiveorless" <$> code "Natural → Natural" - wurbleType <- insert "wurble" <$> code "Natural → Integer" - let tyCtx = minType . fiveorlessType . wurbleType $ empty - valCtx e = case e of - (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> pure (Just (NaturalLit (min x y))) - (App (Var (V "wurble" 0)) (NaturalLit x)) -> pure (Just - (App (Var (V "fiveorless" 0)) (NaturalPlus (NaturalLit x) (NaturalLit 2)))) - (App (Var (V "fiveorless" 0)) (NaturalLit x)) -> pure (Just - (App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2)))) - _ -> pure Nothing - e <- codeWith tyCtx "wurble 6" - assertNormalizesToWith valCtx e "5" - -should :: Text -> Text -> TestTree -should name basename = - Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do - let actualCode = "./tests/normalization/" <> basename <> "A.dhall" - let expectedCode = "./tests/normalization/" <> basename <> "B.dhall" - - actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - actualResolved <- Dhall.Import.load actualExpr - case Dhall.TypeCheck.typeOf actualResolved of - Left err -> Control.Exception.throwIO err - Right _ -> return () - let actualNormalized = - Dhall.Core.alphaNormalize - (Dhall.Core.normalize actualResolved :: Expr X X) - - expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - expectedResolved <- Dhall.Import.load expectedExpr - case Dhall.TypeCheck.typeOf expectedResolved of - Left err -> Control.Exception.throwIO err - Right _ -> return () - -- Use `denote` instead of `normalize` to enforce that the expected - -- expression is already in normal form - let expectedNormalized = - Dhall.Core.alphaNormalize (Dhall.Core.denote expectedResolved) - - let message = - "The normalized expression did not match the expected output" - Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized - -shouldNormalize :: Text -> Text -> TestTree -shouldNormalize name = should ("normalize " <> name <> " correctly") diff --git a/tests/Parser.hs b/tests/Parser.hs deleted file mode 100644 --- a/tests/Parser.hs +++ /dev/null @@ -1,175 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Parser where - -import Data.Text (Text) -import Test.Tasty (TestTree) - -import qualified Control.Exception -import qualified Data.Text -import qualified Data.Text.IO -import qualified Dhall.Parser -import qualified Test.Tasty -import qualified Test.Tasty.HUnit - -parserTests :: TestTree -parserTests = - Test.Tasty.testGroup "parser tests" - [ Test.Tasty.testGroup "whitespace" - [ shouldParse - "prefix/suffix" - "./tests/parser/success/whitespace" - , shouldParse - "block comment" - "./tests/parser/success/blockComment" - , shouldParse - "nested block comment" - "./tests/parser/success/nestedBlockComment" - , shouldParse - "line comment" - "./tests/parser/success/lineComment" - , shouldParse - "Unicode comment" - "./tests/parser/success/unicodeComment" - , shouldParse - "whitespace buffet" - "./tests/parser/success/whitespaceBuffet" - ] - , shouldParse - "label" - "./tests/parser/success/label" - , shouldParse - "quoted label" - "./tests/parser/success/quotedLabel" - , shouldParse - "double quoted string" - "./tests/parser/success/doubleQuotedString" - , shouldParse - "Unicode double quoted string" - "./tests/parser/success/unicodeDoubleQuotedString" - , shouldParse - "escaped double quoted string" - "./tests/parser/success/escapedDoubleQuotedString" - , shouldParse - "interpolated double quoted string" - "./tests/parser/success/interpolatedDoubleQuotedString" - , shouldParse - "single quoted string" - "./tests/parser/success/singleQuotedString" - , shouldParse - "escaped single quoted string" - "./tests/parser/success/escapedSingleQuotedString" - , shouldParse - "interpolated single quoted string" - "./tests/parser/success/interpolatedSingleQuotedString" - , shouldParse - "double" - "./tests/parser/success/double" - , shouldParse - "natural" - "./tests/parser/success/natural" - , shouldParse - "identifier" - "./tests/parser/success/identifier" - , shouldParse - "paths" - "./tests/parser/success/paths" - , shouldParse - "path termination" - "./tests/parser/success/pathTermination" - , shouldParse - "urls" - "./tests/parser/success/urls" - , shouldParse - "environmentVariables" - "./tests/parser/success/environmentVariables" - , shouldParse - "lambda" - "./tests/parser/success/lambda" - , shouldParse - "if then else" - "./tests/parser/success/ifThenElse" - , shouldParse - "let" - "./tests/parser/success/let" - , shouldParse - "forall" - "./tests/parser/success/forall" - , shouldParse - "function type" - "./tests/parser/success/functionType" - , shouldParse - "operators" - "./tests/parser/success/operators" - , shouldParse - "annotations" - "./tests/parser/success/annotations" - , shouldParse - "merge" - "./tests/parser/success/merge" - , shouldParse - "constructors" - "./tests/parser/success/constructors" - , shouldParse - "fields" - "./tests/parser/success/fields" - , shouldParse - "record" - "./tests/parser/success/record" - , shouldParse - "union" - "./tests/parser/success/union" - , shouldParse - "list" - "./tests/parser/success/list" - , shouldParse - "builtins" - "./tests/parser/success/builtins" - , shouldParse - "import alternatives" - "./tests/parser/success/importAlt" - , shouldParse - "large expression" - "./tests/parser/success/largeExpression" - , shouldParse - "names that begin with reserved identifiers" - "./tests/parser/success/reservedPrefix" - , shouldParse - "interpolated expressions with leading whitespace" - "./tests/parser/success/template" - , shouldParse - "collections with type annotations containing imports" - "./tests/parser/success/collectionImportType" - , shouldParse - "a parenthesized custom header import" - "./tests/parser/success/parenthesizeUsing" - , shouldNotParse - "accessing a field of an import without parentheses" - "./tests/parser/failure/importAccess.dhall" - , shouldParse - "Sort" - "./tests/parser/success/sort" - , shouldParse - "quoted path components" - "./tests/parser/success/quotedPaths" - , shouldNotParse - "positive double out of bounds" - "./tests/parser/failure/doubleBoundsPos.dhall" - , shouldNotParse - "negative double out of bounds" - "./tests/parser/failure/doubleBoundsNeg.dhall" - ] - -shouldParse :: Text -> FilePath -> TestTree -shouldParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do - text <- Data.Text.IO.readFile (path <> "A.dhall") - case Dhall.Parser.exprFromText mempty text of - Left err -> Control.Exception.throwIO err - Right _ -> return () ) - -shouldNotParse :: Text -> FilePath -> TestTree -shouldNotParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do - text <- Data.Text.IO.readFile path - case Dhall.Parser.exprFromText mempty text of - Left _ -> return () - Right _ -> fail "Unexpected successful parser" ) diff --git a/tests/QuickCheck.hs b/tests/QuickCheck.hs deleted file mode 100644 --- a/tests/QuickCheck.hs +++ /dev/null @@ -1,364 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE StandaloneDeriving #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - -module QuickCheck where - -import Codec.Serialise (DeserialiseFailure(..)) -import Control.Monad (guard) -import Data.List.NonEmpty (NonEmpty(..)) -import Dhall.Map (Map) -import Dhall.Core - ( Binding(..) - , Chunks(..) - , Const(..) - , Directory(..) - , Expr(..) - , File(..) - , FilePrefix(..) - , Import(..) - , ImportHashed(..) - , ImportMode(..) - , ImportType(..) - , Scheme(..) - , URL(..) - , Var(..) - ) -import Dhall.Set (Set) -import Numeric.Natural (Natural) -import Test.QuickCheck - (Arbitrary(..), Gen, Property, genericShrink, (===)) -import Test.QuickCheck.Instances () -import Test.Tasty (TestTree) - -import qualified Codec.Serialise -import qualified Data.Coerce -import qualified Dhall.Map -import qualified Data.Sequence -import qualified Dhall.Binary -import qualified Dhall.Core -import qualified Dhall.Set -import qualified Test.QuickCheck -import qualified Test.Tasty.QuickCheck - -newtype DeserialiseFailureWithEq = D DeserialiseFailure - deriving (Show) - -instance Eq DeserialiseFailureWithEq where - D (DeserialiseFailure aL bL) == D (DeserialiseFailure aR bR) = - aL == aR && bL == bR - -instance (Arbitrary a, Ord a) => Arbitrary (Set a) where - arbitrary = Dhall.Set.fromList <$> arbitrary - -lift0 :: a -> Gen a -lift0 = pure - -lift1 :: Arbitrary a => (a -> b) -> Gen b -lift1 f = f <$> arbitrary - -lift2 :: (Arbitrary a, Arbitrary b) => (a -> b -> c) -> Gen c -lift2 f = f <$> arbitrary <*> arbitrary - -lift3 :: (Arbitrary a, Arbitrary b, Arbitrary c) => (a -> b -> c -> d) -> Gen d -lift3 f = f <$> arbitrary <*> arbitrary <*> arbitrary - -lift4 - :: (Arbitrary a, Arbitrary b, Arbitrary c, Arbitrary d) - => (a -> b -> c -> d -> e) -> Gen e -lift4 f = f <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - -lift5 - :: ( Arbitrary a - , Arbitrary b - , Arbitrary c - , Arbitrary d - , Arbitrary e - ) - => (a -> b -> c -> d -> e -> f) -> Gen f -lift5 f = - f <$> arbitrary - <*> arbitrary - <*> arbitrary - <*> arbitrary - <*> arbitrary - -lift6 - :: ( Arbitrary a - , Arbitrary b - , Arbitrary c - , Arbitrary d - , Arbitrary e - , Arbitrary f - ) - => (a -> b -> c -> d -> e -> f -> g) -> Gen g -lift6 f = - f <$> arbitrary - <*> arbitrary - <*> arbitrary - <*> arbitrary - <*> arbitrary - <*> arbitrary - -natural :: (Arbitrary a, Num a) => Gen a -natural = - Test.QuickCheck.frequency - [ (7, arbitrary) - , (1, fmap (\x -> x + (2 ^ (64 :: Int))) arbitrary) - ] - -integer :: (Arbitrary a, Num a) => Gen a -integer = - Test.QuickCheck.frequency - [ (7, arbitrary) - , (1, fmap (\x -> x + (2 ^ (64 :: Int))) arbitrary) - , (1, fmap (\x -> x - (2 ^ (64 :: Int))) arbitrary) - ] - -instance (Ord k, Arbitrary k, Arbitrary v) => Arbitrary (Map k v) where - arbitrary = do - n <- Test.QuickCheck.choose (0, 2) - kvs <- Test.QuickCheck.vectorOf n ((,) <$> arbitrary <*> arbitrary) - return (Dhall.Map.fromList kvs) - - shrink = - map Dhall.Map.fromList - . shrink - . Dhall.Map.toList - -instance (Arbitrary s, Arbitrary a) => Arbitrary (Binding s a) where - arbitrary = lift3 Binding - - shrink = genericShrink - -instance (Arbitrary s, Arbitrary a) => Arbitrary (Chunks s a) where - arbitrary = do - n <- Test.QuickCheck.choose (0, 2) - Chunks <$> Test.QuickCheck.vectorOf n arbitrary <*> arbitrary - - shrink = genericShrink - -instance Arbitrary Const where - arbitrary = Test.QuickCheck.oneof [ pure Type, pure Kind, pure Sort ] - - shrink = genericShrink - -instance Arbitrary Directory where - arbitrary = lift1 Directory - - shrink = genericShrink - -averageDepth :: Natural -averageDepth = 3 - -averageNumberOfSubExpressions :: Double -averageNumberOfSubExpressions = 1 - 1 / fromIntegral averageDepth - -probabilityOfNullaryConstructor :: Double -probabilityOfNullaryConstructor = 1 / fromIntegral averageDepth - -numberOfConstructors :: Natural -numberOfConstructors = 50 - -instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where - arbitrary = - Test.QuickCheck.suchThat - (Test.QuickCheck.frequency - [ ( 7, lift1 Const) - , ( 7, lift1 Var) - , ( 1, Test.QuickCheck.oneof [ lift2 (Lam "_"), lift3 Lam ]) - , ( 1, Test.QuickCheck.oneof [ lift2 (Pi "_"), lift3 Pi ]) - , ( 1, lift2 App) - , let letExpression = do - n <- Test.QuickCheck.choose (0, 2) - binding <- arbitrary - bindings <- Test.QuickCheck.vectorOf n arbitrary - body <- arbitrary - return (Let (binding :| bindings) body) - in ( 1, Test.QuickCheck.oneof [ letExpression ]) - , ( 1, lift2 Annot) - , ( 7, lift0 Bool) - , ( 7, lift1 BoolLit) - , ( 1, lift2 BoolAnd) - , ( 1, lift2 BoolOr) - , ( 1, lift2 BoolEQ) - , ( 1, lift2 BoolNE) - , ( 1, lift3 BoolIf) - , ( 7, lift0 Natural) - , ( 7, fmap NaturalLit natural) - , ( 7, lift0 NaturalFold) - , ( 7, lift0 NaturalBuild) - , ( 7, lift0 NaturalIsZero) - , ( 7, lift0 NaturalEven) - , ( 7, lift0 NaturalOdd) - , ( 7, lift0 NaturalToInteger) - , ( 7, lift0 NaturalShow) - , ( 1, lift2 NaturalPlus) - , ( 1, lift2 NaturalTimes) - , ( 7, lift0 Integer) - , ( 7, fmap IntegerLit integer) - , ( 7, lift0 IntegerShow) - , ( 7, lift0 Double) - , ( 7, lift1 DoubleLit) - , ( 7, lift0 DoubleShow) - , ( 7, lift0 Text) - , ( 1, lift1 TextLit) - , ( 1, lift2 TextAppend) - , ( 7, lift0 List) - , let listLit = do - n <- Test.QuickCheck.choose (0, 3) - xs <- Test.QuickCheck.vectorOf n arbitrary - let ys = Data.Sequence.fromList xs - ListLit <$> arbitrary <*> pure ys - - in ( 1, listLit) - , ( 1, lift2 ListAppend) - , ( 7, lift0 ListBuild) - , ( 7, lift0 ListFold) - , ( 7, lift0 ListLength) - , ( 7, lift0 ListHead) - , ( 7, lift0 ListLast) - , ( 7, lift0 ListIndexed) - , ( 7, lift0 ListReverse) - , ( 7, lift0 Optional) - , ( 1, lift2 OptionalLit) - , ( 7, lift0 OptionalFold) - , ( 7, lift0 OptionalBuild) - , ( 1, lift1 Record) - , ( 1, lift1 RecordLit) - , ( 1, lift1 Union) - , ( 1, lift3 UnionLit) - , ( 1, lift2 Combine) - , ( 1, lift2 CombineTypes) - , ( 1, lift2 Prefer) - , ( 1, lift3 Merge) - , ( 1, lift1 Constructors) - , ( 1, lift2 Field) - , ( 1, lift2 Project) - , ( 7, lift1 Embed) - ] - ) - standardizedExpression - - shrink expression = filter standardizedExpression (genericShrink expression) - -standardizedExpression :: Expr s a -> Bool -standardizedExpression (ListLit Nothing xs) = not (Data.Sequence.null xs) -standardizedExpression (ListLit (Just _ ) xs) = Data.Sequence.null xs -standardizedExpression (Note _ _ ) = False -standardizedExpression _ = True - -instance Arbitrary File where - arbitrary = lift2 File - - shrink = genericShrink - -instance Arbitrary FilePrefix where - arbitrary = Test.QuickCheck.oneof [ pure Absolute, pure Here, pure Home ] - - shrink = genericShrink - -instance Arbitrary ImportType where - arbitrary = - Test.QuickCheck.suchThat - (Test.QuickCheck.oneof - [ lift2 Local - , lift5 (\a b c d e -> Remote (URL a b c d e Nothing)) - , lift1 Env - , lift0 Missing - ] - ) - standardizedImportType - - shrink importType = - filter standardizedImportType (genericShrink importType) - -standardizedImportType :: ImportType -> Bool -standardizedImportType (Remote (URL _ _ _ _ _ (Just _))) = False -standardizedImportType _ = True - -instance Arbitrary ImportHashed where - arbitrary = - Test.QuickCheck.suchThat - (lift1 (ImportHashed Nothing)) - standardizedImportHashed - - shrink (ImportHashed { importType = oldImportType, .. }) = do - newImportType <- shrink oldImportType - let importHashed = ImportHashed { importType = newImportType, .. } - guard (standardizedImportHashed importHashed) - return importHashed - -standardizedImportHashed :: ImportHashed -> Bool -standardizedImportHashed (ImportHashed (Just _) _) = False -standardizedImportHashed _ = True - --- The standard does not yet specify how to encode `as Text`, so don't test it --- yet -instance Arbitrary ImportMode where - arbitrary = lift0 Code - - shrink = genericShrink - -instance Arbitrary Import where - arbitrary = lift2 Import - - shrink = genericShrink - -instance Arbitrary Scheme where - arbitrary = Test.QuickCheck.oneof [ pure HTTP, pure HTTPS ] - - shrink = genericShrink - -instance Arbitrary URL where - arbitrary = lift6 URL - - shrink = genericShrink - -instance Arbitrary Var where - arbitrary = - Test.QuickCheck.oneof - [ fmap (V "_") natural - , lift1 (\t -> V t 0) - , lift1 V <*> natural - ] - - shrink = genericShrink - -binaryRoundtrip :: Expr () Import -> Property -binaryRoundtrip expression = - wrap - (fmap - Dhall.Binary.decodeWithVersion - (Codec.Serialise.deserialiseOrFail - (Codec.Serialise.serialise - (Dhall.Binary.encodeWithVersion Dhall.Binary.defaultStandardVersion expression) - ) - ) - ) - === wrap (Right (Right expression)) - where - wrap - :: Either DeserialiseFailure a - -> Either DeserialiseFailureWithEq a - wrap = Data.Coerce.coerce - -isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property -isNormalizedIsConsistentWithNormalize expression = - Dhall.Core.isNormalized expression - === (Dhall.Core.normalize expression == expression) - -quickcheckTests :: TestTree -quickcheckTests - = Test.Tasty.QuickCheck.testProperties - "QuickCheck" - [ ( "Binary serialization should round-trip" - , Test.QuickCheck.property binaryRoundtrip - ) - , ( "isNormalized should be consistent with normalize" - , Test.QuickCheck.property - (Test.QuickCheck.withMaxSuccess 10000 isNormalizedIsConsistentWithNormalize) - ) - ] diff --git a/tests/Regression.hs b/tests/Regression.hs deleted file mode 100644 --- a/tests/Regression.hs +++ /dev/null @@ -1,243 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE OverloadedStrings #-} - -module Regression where - -import qualified Control.Exception -import qualified Data.Text.Lazy.IO -import qualified Data.Text.Prettyprint.Doc -import qualified Data.Text.Prettyprint.Doc.Render.Text -import qualified Dhall -import qualified Dhall.Context -import qualified Dhall.Core -import qualified Dhall.Map -import qualified Dhall.Parser -import qualified Dhall.Pretty -import qualified Dhall.TypeCheck -import qualified System.Timeout -import qualified Test.Tasty -import qualified Test.Tasty.HUnit -import qualified Util - -import Control.DeepSeq (($!!)) -import Dhall.Import (Imported) -import Dhall.Parser (Src) -import Dhall.TypeCheck (TypeError, X) -import Test.Tasty (TestTree) -import Test.Tasty.HUnit ((@?=)) - -regressionTests :: TestTree -regressionTests = - Test.Tasty.testGroup "regression tests" - [ issue96 - , issue126 - , issue151 - , issue164 - , issue201 - , issue209 - , issue216 - , issue253 - , parsing0 - , typeChecking0 - , typeChecking1 - , typeChecking2 - , unnamedFields - , trailingSpaceAfterStringLiterals - ] - -data Foo = Foo Integer Bool | Bar Bool Bool Bool | Baz Integer Integer - deriving (Show, Dhall.Generic, Dhall.Interpret, Dhall.Inject) - -unnamedFields :: TestTree -unnamedFields = Test.Tasty.HUnit.testCase "Unnamed Fields" (do - let ty = Dhall.auto :: Dhall.Type Foo - Test.Tasty.HUnit.assertEqual "Good type" (Dhall.expected ty) - (Dhall.Core.Union - (Dhall.Map.fromList - [ ("Foo",Dhall.Core.Record (Dhall.Map.fromList [ - ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool)])) - , ("Bar",Dhall.Core.Record (Dhall.Map.fromList [ - ("_1",Dhall.Core.Bool),("_2",Dhall.Core.Bool),("_3",Dhall.Core.Bool)])) - , ("Baz",Dhall.Core.Record (Dhall.Map.fromList [ - ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Integer)])) - ] - ) - ) - - let inj = Dhall.inject :: Dhall.InputType Foo - Test.Tasty.HUnit.assertEqual "Good Inject" (Dhall.declared inj) (Dhall.expected ty) - - let tu_ty = Dhall.auto :: Dhall.Type (Integer, Bool) - Test.Tasty.HUnit.assertEqual "Auto Tuple" (Dhall.expected tu_ty) (Dhall.Core.Record ( - Dhall.Map.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool) ])) - - let tu_in = Dhall.inject :: Dhall.InputType (Integer, Bool) - Test.Tasty.HUnit.assertEqual "Inj. Tuple" (Dhall.declared tu_in) (Dhall.expected tu_ty) - - return () ) - -issue96 :: TestTree -issue96 = Test.Tasty.HUnit.testCase "Issue #96" (do - -- Verify that parsing should not fail - _ <- Util.code "\"bar'baz\"" - return () ) - -issue126 :: TestTree -issue126 = Test.Tasty.HUnit.testCase "Issue #126" (do - e <- Util.code - "''\n\ - \ foo\n\ - \ bar\n\ - \''" - Util.normalize' e @?= "''\nfoo\nbar\n''" ) - -issue151 :: TestTree -issue151 = Test.Tasty.HUnit.testCase "Issue #151" (do - let shouldNotTypeCheck text = do - let handler :: Imported (TypeError Src X) -> IO Bool - handler _ = return True - - let typeCheck = do - _ <- Util.code text - return False - b <- Control.Exception.handle handler typeCheck - Test.Tasty.HUnit.assertBool "The expression should not type-check" b - - -- These two examples contain the following expression that loops infinitely - -- if you normalize the expression before type-checking the expression: - -- - -- (λ(x : A) → x x) (λ(x : A) → x x) - -- - -- There was a bug in the Dhall type-checker were expressions were not - -- being type-checked before being added to the context (which is a - -- violation of the standard type-checking rules for a pure type system). - -- The reason this is problematic is that several places in the - -- type-checking logic assume that the context is safe to normalize. - -- - -- Both of these examples exercise area of the type-checker logic that - -- assume that the context is normalized. If you fail to type-check terms - -- before adding them to the context then this test will "fail" with an - -- infinite loop. This test "succeeds" if the examples terminate - -- immediately with a type-checking failure. - shouldNotTypeCheck "./tests/regression/issue151a.dhall" - shouldNotTypeCheck "./tests/regression/issue151b.dhall" ) - -issue164 :: TestTree -issue164 = Test.Tasty.HUnit.testCase "Issue #164" (do - -- Verify that parsing should not fail on a single-quote within a - -- single-quoted string - _ <- Util.code "./tests/regression/issue164.dhall" - return () ) - -issue201 :: TestTree -issue201 = Test.Tasty.HUnit.testCase "Issue #201" (do - -- Verify that type synonyms work - _ <- Util.code "./tests/regression/issue201.dhall" - return () ) - -issue209 :: TestTree -issue209 = Test.Tasty.HUnit.testCase "Issue #209" (do - -- Verify that pretty-printing `constructors` doesn't trigger an infinite - -- loop - e <- Util.code "./tests/regression/issue209.dhall" - let text = Dhall.Core.pretty e - Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $!! text) - return () ) - -issue216 :: TestTree -issue216 = Test.Tasty.HUnit.testCase "Issue #216" (do - -- Verify that pretty-printing preserves string interpolation - e <- Util.code "./tests/regression/issue216a.dhall" - let doc = Data.Text.Prettyprint.Doc.pretty e - let docStream = Data.Text.Prettyprint.Doc.layoutSmart Dhall.Pretty.layoutOpts doc - let text0 = Data.Text.Prettyprint.Doc.Render.Text.renderLazy docStream - - text1 <- Data.Text.Lazy.IO.readFile "./tests/regression/issue216b.dhall" - - Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 ) - -issue253 :: TestTree -issue253 = Test.Tasty.HUnit.testCase "Issue #253" (do - -- Verify that type-checking rejects ill-formed custom contexts - let context = Dhall.Context.insert "x" "x" Dhall.Context.empty - let result = Dhall.TypeCheck.typeWith context "x" - - -- If the context is not validated correctly then type-checking will - -- infinitely loop - Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $! result) - return () ) - -parsing0 :: TestTree -parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do - -- Verify that parsing should not fail - -- - -- In 267093f8cddf1c2f909f2d997c31fd0a7cb2440a I broke the parser when left - -- factoring the grammer by failing to handle the source tested by this - -- regression test. The root of the problem was that the parser was trying - -- to parse `List ./Node` as `Field List "/Node"` instead of - -- `App List (Embed (Path (File Homeless "./Node") Code))`. The latter is - -- the correct parse because `/Node` is not a valid field label, but the - -- mistaken parser was committed to the incorrect parse and never attempted - -- the correct parse. - case Dhall.Parser.exprFromText mempty "List ./Node" of - Left e -> Control.Exception.throwIO e - Right _ -> return () ) - -typeChecking0 :: TestTree -typeChecking0 = Test.Tasty.HUnit.testCase "Type-checking regression #0" (do - -- There used to be a bug in the type-checking logic where `T` would be - -- added to the context when inferring the type of `λ(x : T) → x`, but was - -- missing from the context when inferring the kind of the inferred type - -- (i.e. the kind of `∀(x : T) → T`). This led to an unbound variable - -- error when inferring the kind - -- - -- This bug was originally reported in issue #10 - _ <- Util.code "let Day : Type = Natural in λ(x : Day) → x" - return () ) - -typeChecking1 :: TestTree -typeChecking1 = Test.Tasty.HUnit.testCase "Type-checking regression #1" (do - -- There used to be a bug in the type-checking logic when inferring the - -- type of `let`. Specifically, given an expression of the form: - -- - -- let x : t = e1 in e2 - -- - -- ... the type-checker would not substitute `x` for `e1` in the inferred - -- of the `let` expression. This meant that if the inferred type contained - -- any references to `x` then these references would escape their scope and - -- result in unbound variable exceptions - -- - -- This regression test exercises that code path by creating a `let` - -- expression where the inferred type before substitution (`∀(x : b) → b` in - -- this example), contains a reference to the `let`-bound variable (`b`) - -- that needs to be substituted with `a` in order to produce the final - -- correct inferred type (`∀(x : a) → a`). If this test passes then - -- substitution worked correctly. If substitution doesn't occur then you - -- expect an `Unbound variable` error from `b` escaping its scope due to - -- being returned as part of the inferred type - _ <- Util.code "λ(a : Type) → let b : Type = a in λ(x : b) → x" - return () ) - -typeChecking2 :: TestTree -typeChecking2 = Test.Tasty.HUnit.testCase "Type-checking regression #2" (do - -- There used to be a bug in the type-checking logic where `let` bound - -- variables would not correctly shadow variables of the same name when - -- inferring the type of of the `let` expression - -- - -- This example exercises this code path with a `let` expression where the - -- `let`-bound variable (`a`) has the same name as its own type (`a`). If - -- shadowing works correctly then the final `a` in the expression should - -- refer to the `let`-bound variable and not its type. An invalid reference - -- to the shadowed type `a` would result in an invalid dependently typed - -- function - _ <- Util.code "λ(a : Type) → λ(x : a) → let a : a = x in a" - return () ) - -trailingSpaceAfterStringLiterals :: TestTree -trailingSpaceAfterStringLiterals = - Test.Tasty.HUnit.testCase "Trailing space after string literals" (do - -- Verify that string literals parse correctly with trailing space - -- (Yes, I did get this wrong at some point) - _ <- Util.code "(''ABC'' ++ \"DEF\" )" - return () ) diff --git a/tests/Tests.hs b/tests/Tests.hs deleted file mode 100644 --- a/tests/Tests.hs +++ /dev/null @@ -1,36 +0,0 @@ -module Main where - -import Lint (lintTests) -import Normalization (normalizationTests) -import Parser (parserTests) -import Regression (regressionTests) -import QuickCheck (quickcheckTests) -import Tutorial (tutorialTests) -import TypeCheck (typecheckTests) -import Format (formatTests) -import Import (importTests) -import System.FilePath (()) -import Test.Tasty - -import qualified System.Directory -import qualified System.Environment - -allTests :: TestTree -allTests = - testGroup "Dhall Tests" - [ normalizationTests - , parserTests - , regressionTests - , tutorialTests - , formatTests - , typecheckTests - , importTests - , quickcheckTests - , lintTests - ] - -main :: IO () -main = do - pwd <- System.Directory.getCurrentDirectory - System.Environment.setEnv "XDG_CACHE_HOME" (pwd ".cache") - defaultMain allTests diff --git a/tests/Tutorial.hs b/tests/Tutorial.hs deleted file mode 100644 --- a/tests/Tutorial.hs +++ /dev/null @@ -1,85 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE OverloadedStrings #-} - -module Tutorial where - -import qualified Data.Vector -import qualified Dhall -import qualified Test.Tasty -import qualified Test.Tasty.HUnit -import qualified Util - -import Data.Monoid ((<>)) -import Data.Text (Text) -import Dhall (Inject) -import GHC.Generics (Generic) -import Numeric.Natural (Natural) -import Test.Tasty (TestTree) -import Test.Tasty.HUnit ((@?=)) - -tutorialTests :: TestTree -tutorialTests = - Test.Tasty.testGroup "tutorial" - [ Test.Tasty.testGroup "Interpolation" - [ _Interpolation_0 - , _Interpolation_1 - ] - , Test.Tasty.testGroup "Functions" - [ _Functions_0 - , _Functions_1 - , _Functions_2 - ] - , Test.Tasty.testGroup "Unions" - [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall" - , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall" - , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall" - , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall" - , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall" - ] - ] - -_Interpolation_0 :: TestTree -_Interpolation_0 = Test.Tasty.HUnit.testCase "Example #0" (do - e <- Util.code - " let name = \"John Doe\" \n\ - \in let age = 21 \n\ - \in \"My name is ${name} and my age is ${Natural/show age}\"\n" - Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" ) - -_Interpolation_1 :: TestTree -_Interpolation_1 = Test.Tasty.HUnit.testCase "Example #1" (do - e <- Util.code - "'' \n\ - \ for file in *; do \n\ - \ echo \"Found ''${file}\"\n\ - \ done \n\ - \'' \n" - Util.assertNormalized e ) - -_Functions_0 :: TestTree -_Functions_0 = Test.Tasty.HUnit.testCase "Example #0" (do - let text = "\\(n : Bool) -> [ n && True, n && False, n || True, n || False ]" - makeBools <- Dhall.input Dhall.auto text - makeBools True @?= Data.Vector.fromList [True,False,True,True] ) - -_Functions_1 :: TestTree -_Functions_1 = Test.Tasty.HUnit.testCase "Example #1" (do - let text = "λ(x : Bool) → λ(y : Bool) → x && y" - makeBools <- Dhall.input Dhall.auto text - makeBools True False @?= False ) - -data Example0 = Example0 { foo :: Bool, bar :: Bool } - deriving (Generic, Inject) - -_Functions_2 :: TestTree -_Functions_2 = Test.Tasty.HUnit.testCase "Example #2" (do - f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" - f (Example0 { foo = True, bar = False }) @?= False - f (Example0 { foo = True, bar = True }) @?= True ) - -example :: Natural -> Text -> Text -> TestTree -example n text0 text1 = - Test.Tasty.HUnit.testCase - ("Example #" <> show n) - (Util.equivalent text0 text1) diff --git a/tests/TypeCheck.hs b/tests/TypeCheck.hs deleted file mode 100644 --- a/tests/TypeCheck.hs +++ /dev/null @@ -1,131 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module TypeCheck where - -import Data.Monoid (mempty, (<>)) -import Data.Text (Text) -import Dhall.Import (Imported) -import Dhall.Parser (Src) -import Dhall.TypeCheck (TypeError, X) -import Test.Tasty (TestTree) - -import qualified Control.Exception -import qualified Data.Text -import qualified Dhall.Core -import qualified Dhall.Import -import qualified Dhall.Parser -import qualified Dhall.TypeCheck -import qualified Test.Tasty -import qualified Test.Tasty.HUnit - -typecheckTests :: TestTree -typecheckTests = - Test.Tasty.testGroup "typecheck tests" - [ preludeExamples - , accessTypeChecks - , should - "allow type-valued fields in a record" - "success/simple/fieldsAreTypes" - , should - "allow type-valued alternatives in a union" - "success/simple/alternativesAreTypes" - , should - "allow anonymous functions in types to be judgmentally equal" - "success/simple/anonymousFunctionsInTypes" - , should - "correctly handle α-equivalent merge alternatives" - "success/simple/mergeEquivalence" - , should - "allow Kind variables" - "success/simple/kindParameter" - , shouldNotTypeCheck - "combining records of terms and types" - "failure/combineMixedRecords" - , shouldNotTypeCheck - "preferring a record of types over a record of terms" - "failure/preferMixedRecords" - , should - "allow records of types of mixed kinds" - "success/recordOfTypes" - , should - "allow Boehm-Berarducci-encoded records of types of mixed kinds" - "success/encodedRecordOfTypes" - , should - "allow accessing a type from a record" - "success/accessType" - , should - "allow accessing a type from a Boehm-Berarducci-encoded record" - "success/accessEncodedType" - , shouldNotTypeCheck - "Hurkens' paradox" - "failure/hurkensParadox" - , should - "allow accessing a constructor from a type stored inside a record" - "success/simple/mixedFieldAccess" - ] - -preludeExamples :: TestTree -preludeExamples = - Test.Tasty.testGroup "Prelude examples" - [ should "Monoid" "./success/prelude/Monoid/00" - , should "Monoid" "./success/prelude/Monoid/01" - , should "Monoid" "./success/prelude/Monoid/02" - , should "Monoid" "./success/prelude/Monoid/03" - , should "Monoid" "./success/prelude/Monoid/04" - , should "Monoid" "./success/prelude/Monoid/05" - , should "Monoid" "./success/prelude/Monoid/06" - , should "Monoid" "./success/prelude/Monoid/07" - , should "Monoid" "./success/prelude/Monoid/08" - , should "Monoid" "./success/prelude/Monoid/09" - , should "Monoid" "./success/prelude/Monoid/10" - ] - -accessTypeChecks :: TestTree -accessTypeChecks = - Test.Tasty.testGroup "typecheck access" - [ should "record" "./success/simple/access/0" - , should "record" "./success/simple/access/1" - ] - -should :: Text -> Text -> TestTree -should name basename = - Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do - let actualCode = "./tests/typecheck/" <> basename <> "A.dhall" - let expectedCode = "./tests/typecheck/" <> basename <> "B.dhall" - - actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of - Left err -> Control.Exception.throwIO err - Right expr -> return expr - - let annotatedExpr = Dhall.Core.Annot actualExpr expectedExpr - - resolvedExpr <- Dhall.Import.load annotatedExpr - case Dhall.TypeCheck.typeOf resolvedExpr of - Left err -> Control.Exception.throwIO err - Right _ -> return () - -shouldNotTypeCheck :: Text -> Text -> TestTree -shouldNotTypeCheck name basename = - Test.Tasty.HUnit.testCase (Data.Text.unpack name) $ do - let code = "./tests/typecheck/" <> basename <> ".dhall" - - expression <- case Dhall.Parser.exprFromText mempty code of - Left exception -> Control.Exception.throwIO exception - Right expression -> return expression - - let io :: IO Bool - io = do - _ <- Dhall.Import.load expression - return True - - let handler :: Imported (TypeError Src X)-> IO Bool - handler _ = return False - - typeChecked <- Control.Exception.handle handler io - - if typeChecked - then fail (Data.Text.unpack code <> " should not have type-checked") - else return () diff --git a/tests/Util.hs b/tests/Util.hs deleted file mode 100644 --- a/tests/Util.hs +++ /dev/null @@ -1,76 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RankNTypes #-} -module Util - ( code - , codeWith - , equivalent - , normalize' - , normalizeWith' - , assertNormalizesTo - , assertNormalizesToWith - , assertNormalized - , assertTypeChecks - ) where - -import qualified Control.Exception -import qualified Data.Functor -import Data.Bifunctor (first) -import Data.Text (Text) -import qualified Dhall.Core -import Dhall.Core (Expr, Normalizer) -import qualified Dhall.Context -import Dhall.Context (Context) -import qualified Dhall.Import -import qualified Dhall.Parser -import Dhall.Parser (Src) -import qualified Dhall.TypeCheck -import Dhall.TypeCheck (X) -import Test.Tasty.HUnit - -normalize' :: Expr Src X -> Text -normalize' = Dhall.Core.pretty . Dhall.Core.normalize - -normalizeWith' :: Normalizer X -> Expr Src X -> Text -normalizeWith' ctx = Dhall.Core.pretty . Dhall.Core.normalizeWith ctx - -code :: Text -> IO (Expr Src X) -code = codeWith Dhall.Context.empty - -codeWith :: Context (Expr Src X) -> Text -> IO (Expr Src X) -codeWith ctx expr = do - expr0 <- case Dhall.Parser.exprFromText mempty expr of - Left parseError -> Control.Exception.throwIO parseError - Right expr0 -> return expr0 - expr1 <- Dhall.Import.load expr0 - case Dhall.TypeCheck.typeWith ctx expr1 of - Left typeError -> Control.Exception.throwIO typeError - Right _ -> return () - return expr1 - -equivalent :: Text -> Text -> IO () -equivalent text0 text1 = do - expr0 <- fmap Dhall.Core.normalize (Util.code text0) :: IO (Expr X X) - expr1 <- fmap Dhall.Core.normalize (Util.code text1) :: IO (Expr X X) - assertEqual "Expressions are not equivalent" expr0 expr1 - -assertNormalizesTo :: Expr Src X -> Text -> IO () -assertNormalizesTo e expected = do - assertBool msg (not $ Dhall.Core.isNormalized e) - normalize' e @?= expected - where msg = "Given expression is already in normal form" - -assertNormalizesToWith :: Normalizer X -> Expr Src X -> Text -> IO () -assertNormalizesToWith ctx e expected = do - assertBool msg (not $ Dhall.Core.isNormalizedWith ctx (first (const ()) e)) - normalizeWith' ctx e @?= expected - where msg = "Given expression is already in normal form" - -assertNormalized :: Expr Src X -> IO () -assertNormalized e = do - assertBool msg1 (Dhall.Core.isNormalized e) - assertEqual msg2 (normalize' e) (Dhall.Core.pretty e) - where msg1 = "Expression was not in normal form" - msg2 = "Normalization is not supposed to change the expression" - -assertTypeChecks :: Text -> IO () -assertTypeChecks text = Data.Functor.void (code text) diff --git a/tests/format/parentA.dhall b/tests/format/parentA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/parentA.dhall @@ -0,0 +1,1 @@ +../a diff --git a/tests/format/parentB.dhall b/tests/format/parentB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/parentB.dhall @@ -0,0 +1,1 @@ +../a diff --git a/tests/import/success/fieldOrderA.dhall b/tests/import/success/fieldOrderA.dhall --- a/tests/import/success/fieldOrderA.dhall +++ b/tests/import/success/fieldOrderA.dhall @@ -1,5 +1,5 @@ { example0 = - ./../data/fieldOrder/1.dhall sha256:4a7866b88389e18cf481b525544fd7903325252faf3a86c8fdc981298c788a9b + ../data/fieldOrder/1.dhall sha256:4a7866b88389e18cf481b525544fd7903325252faf3a86c8fdc981298c788a9b , example1 = - ./../data/fieldOrder/2.dhall sha256:4a7866b88389e18cf481b525544fd7903325252faf3a86c8fdc981298c788a9b + ../data/fieldOrder/2.dhall sha256:4a7866b88389e18cf481b525544fd7903325252faf3a86c8fdc981298c788a9b } diff --git a/tests/import/success/issue553B.dhall b/tests/import/success/issue553B.dhall --- a/tests/import/success/issue553B.dhall +++ b/tests/import/success/issue553B.dhall @@ -1,1 +1,1 @@ -./issue553A.dhall sha256:6fb582c043889dd5a4c97176f8a58d2633252b5374cb71e288b93bc3757f9643 +./issue553A.dhall sha256:e2d014696fb7d773727ae5aa42dc20bbd2447ea82bcb5971ccbb7763906edace diff --git a/tests/normalization/success/multiline/escapeA.dhall b/tests/normalization/success/multiline/escapeA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/escapeA.dhall @@ -0,0 +1,9 @@ +-- Verify that an implementation is processing escape sequences correctly + +'' +''${ +''' +$ +" +\ +'' diff --git a/tests/normalization/success/multiline/escapeB.dhall b/tests/normalization/success/multiline/escapeB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/escapeB.dhall @@ -0,0 +1,1 @@ +"\${\n''\n\$\n\"\n\\\n" diff --git a/tests/normalization/success/multiline/hangingIndentA.dhall b/tests/normalization/success/multiline/hangingIndentA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/hangingIndentA.dhall @@ -0,0 +1,15 @@ +{- The indent is computed as the minimum number of leading spaces over all lines + in a multi-line literal, including the line right before the closing quotes. + In this case, there are three lines: + + * The first line containing " foo" with two leading spaces + * The second line containing " bar" with two leading spaces + * The third line containing " " with two leading spaces + + Therefore we strip two leading spaces from all three lines +-} + +'' + foo + bar + '' diff --git a/tests/normalization/success/multiline/hangingIndentB.dhall b/tests/normalization/success/multiline/hangingIndentB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/hangingIndentB.dhall @@ -0,0 +1,1 @@ +"foo\nbar\n" diff --git a/tests/normalization/success/multiline/interestingA.dhall b/tests/normalization/success/multiline/interestingA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interestingA.dhall @@ -0,0 +1,7 @@ +-- Non-trivial example that combines several multi-line literal features + +λ(x : Text) → '' + ${x} baz + bar + foo + '' diff --git a/tests/normalization/success/multiline/interestingB.dhall b/tests/normalization/success/multiline/interestingB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interestingB.dhall @@ -0,0 +1,1 @@ +λ(x : Text) → "${x} baz\n bar\n foo\n " diff --git a/tests/normalization/success/multiline/interiorIndentA.dhall b/tests/normalization/success/multiline/interiorIndentA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interiorIndentA.dhall @@ -0,0 +1,16 @@ +{- The indent is computed as the minimum number of leading spaces over all lines + in a multi-line literal, including the line right before the closing quotes. + In this case, there are three lines: + + * The first line containing " foo" with two leading spaces + * The second line containing " bar" with two leading spaces + * The third line containing "" with zero leading spaces + + Since the last line has zero leading spaces, the minimum number of leading + spaces over all three lines is zero, so we don't strip any spaces. +-} + +'' + foo + bar +'' diff --git a/tests/normalization/success/multiline/interiorIndentB.dhall b/tests/normalization/success/multiline/interiorIndentB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interiorIndentB.dhall @@ -0,0 +1,1 @@ +" foo\n bar\n" diff --git a/tests/normalization/success/multiline/interpolationA.dhall b/tests/normalization/success/multiline/interpolationA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interpolationA.dhall @@ -0,0 +1,9 @@ +{- This example verifies that an implementation is correctly breaking leading + spaces at interpolated expressions. The first line has the fewest number of + leading spaces (2) due to the interruption by the interpolated expression. +-} + +'' +${Natural/show 1} foo + bar +'' diff --git a/tests/normalization/success/multiline/interpolationB.dhall b/tests/normalization/success/multiline/interpolationB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/interpolationB.dhall @@ -0,0 +1,1 @@ +"${Natural/show 1} foo\n bar\n" diff --git a/tests/normalization/success/multiline/preserveCommentA.dhall b/tests/normalization/success/multiline/preserveCommentA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/preserveCommentA.dhall @@ -0,0 +1,8 @@ +{- A comment within the interior of a multi-line literal counts as part of the + literal +-} + +'' +-- Hello +{- world -} +'' diff --git a/tests/normalization/success/multiline/preserveCommentB.dhall b/tests/normalization/success/multiline/preserveCommentB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/preserveCommentB.dhall @@ -0,0 +1,1 @@ +"-- Hello\n{- world -}\n" diff --git a/tests/normalization/success/multiline/singleLineA.dhall b/tests/normalization/success/multiline/singleLineA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/singleLineA.dhall @@ -0,0 +1,6 @@ +{- This is how you encode a multi-line literal that contains no newlines + + The leading newline is stripped +-} +'' +foo'' diff --git a/tests/normalization/success/multiline/singleLineB.dhall b/tests/normalization/success/multiline/singleLineB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/singleLineB.dhall @@ -0,0 +1,1 @@ +"foo" diff --git a/tests/normalization/success/multiline/twoLinesA.dhall b/tests/normalization/success/multiline/twoLinesA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/twoLinesA.dhall @@ -0,0 +1,7 @@ +{- Verify that an implementation is correctly preserving newlines in the + corresponding double-quoted literal +-} + +'' +foo +bar'' diff --git a/tests/normalization/success/multiline/twoLinesB.dhall b/tests/normalization/success/multiline/twoLinesB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/success/multiline/twoLinesB.dhall @@ -0,0 +1,1 @@ +"foo\nbar" diff --git a/tests/normalization/success/remoteSystemsA.dhall b/tests/normalization/success/remoteSystemsA.dhall --- a/tests/normalization/success/remoteSystemsA.dhall +++ b/tests/normalization/success/remoteSystemsA.dhall @@ -1,6 +1,6 @@ -let Text/concatMap = (./../../../Prelude/package.dhall).`Text`.concatMap +let Text/concatMap = (../../../Prelude/package.dhall).`Text`.concatMap -let Text/concatSep = (./../../../Prelude/package.dhall).`Text`.concatSep +let Text/concatSep = (../../../Prelude/package.dhall).`Text`.concatSep let Row = { cores : diff --git a/tests/normalization/success/remoteSystemsB.dhall b/tests/normalization/success/remoteSystemsB.dhall --- a/tests/normalization/success/remoteSystemsB.dhall +++ b/tests/normalization/success/remoteSystemsB.dhall @@ -1,1 +1,212 @@ -λ(xs : List { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text }) → List/fold { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text } xs Text (λ(x : { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text }) → λ(y : Text) → "${Optional/fold Text x.user Text (λ(user : Text) → "${user}@${x.host}") x.host} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.platforms < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text} ${x.key} ${Integer/show (Natural/toInteger x.cores)} ${Integer/show (Natural/toInteger x.speedFactor)} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.supportedFeatures < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.mandatoryFeatures < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text}\n" ++ y) "" + λ ( _ + : List + { cores : + Natural + , host : + Text + , key : + Text + , mandatoryFeatures : + List Text + , platforms : + List Text + , speedFactor : + Natural + , supportedFeatures : + List Text + , user : + Optional Text + } + ) +→ List/fold + { cores : + Natural + , host : + Text + , key : + Text + , mandatoryFeatures : + List Text + , platforms : + List Text + , speedFactor : + Natural + , supportedFeatures : + List Text + , user : + Optional Text + } + _ + Text + ( λ ( _ + : { cores : + Natural + , host : + Text + , key : + Text + , mandatoryFeatures : + List Text + , platforms : + List Text + , speedFactor : + Natural + , supportedFeatures : + List Text + , user : + Optional Text + } + ) + → λ(_ : Text) + → '' + ${Optional/fold + Text + _@1.user + Text + (λ(user : Text) → "${user}@${_@1.host}") + _@1.host} ${merge + { Empty = λ(_ : {}) → "", NonEmpty = λ(_ : Text) → _ } + ( List/fold + Text + _@1.platforms + < Empty : {} | NonEmpty : Text > + ( λ(_ : Text) + → λ(_ : < Empty : {} | NonEmpty : Text >) + → merge + { Empty = + λ(_ : {}) → < NonEmpty = _@2 | Empty : {} > + , NonEmpty = + λ(_ : Text) + → < NonEmpty = _@2 ++ "," ++ _ | Empty : {} > + } + _ + : < Empty : {} | NonEmpty : Text > + ) + < Empty = {=} | NonEmpty : Text > + ) + : Text} ${_@1.key} ${Integer/show + ( Natural/toInteger _@1.cores + )} ${Integer/show + ( Natural/toInteger + _@1.speedFactor + )} ${merge + { Empty = + λ(_ : {}) → "" + , NonEmpty = + λ(_ : Text) → _ + } + ( List/fold + Text + _@1.supportedFeatures + < Empty : + {} + | NonEmpty : + Text + > + ( λ(_ : Text) + → λ ( _ + : < Empty : + {} + | NonEmpty : + Text + > + ) + → merge + { Empty = + λ(_ : {}) + → < NonEmpty = + _@2 + | Empty : + {} + > + , NonEmpty = + λ(_ : Text) + → < NonEmpty = + _@2 + ++ "," + ++ _ + | Empty : + {} + > + } + _ + : < Empty : + {} + | NonEmpty : + Text + > + ) + < Empty = + {=} + | NonEmpty : + Text + > + ) + : Text} ${merge + { Empty = + λ(_ : {}) + → "" + , NonEmpty = + λ ( _ + : Text + ) + → _ + } + ( List/fold + Text + _@1.mandatoryFeatures + < Empty : + {} + | NonEmpty : + Text + > + ( λ ( _ + : Text + ) + → λ ( _ + : < Empty : + {} + | NonEmpty : + Text + > + ) + → merge + { Empty = + λ ( _ + : {} + ) + → < NonEmpty = + _@2 + | Empty : + {} + > + , NonEmpty = + λ ( _ + : Text + ) + → < NonEmpty = + _@2 + ++ "," + ++ _ + | Empty : + {} + > + } + _ + : < Empty : + {} + | NonEmpty : + Text + > + ) + < Empty = + {=} + | NonEmpty : + Text + > + ) + : Text} + '' + ++ _ + ) + "" diff --git a/tests/parser/failure/mandatoryNewline.dhall b/tests/parser/failure/mandatoryNewline.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/failure/mandatoryNewline.dhall @@ -0,0 +1,2 @@ +-- Multi-line literals require a mandatory newline after the opening quotes +''ABC'' diff --git a/tests/parser/success/asTextA.dhall b/tests/parser/success/asTextA.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/success/asTextA.dhall @@ -0,0 +1,1 @@ +https://example.com/foo as Text diff --git a/tests/parser/success/asTextB.dhall b/tests/parser/success/asTextB.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/success/asTextB.dhall @@ -0,0 +1,11 @@ +[ + 24, + null, + 1, + null, + 1, + "example.com", + "foo", + null, + null +] diff --git a/tests/parser/success/collectionImportTypeB.dhall b/tests/parser/success/collectionImportTypeB.dhall --- a/tests/parser/success/collectionImportTypeB.dhall +++ b/tests/parser/success/collectionImportTypeB.dhall @@ -5,6 +5,8 @@ 5, [ 24, + null, + 0, 3, "type.dhall" ] @@ -13,6 +15,8 @@ 4, [ 24, + null, + 0, 3, "type.dhall" ] diff --git a/tests/parser/success/customHeadersA.dhall b/tests/parser/success/customHeadersA.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/success/customHeadersA.dhall @@ -0,0 +1,1 @@ +https://example.com/foo using ./headers.dhall diff --git a/tests/parser/success/customHeadersB.dhall b/tests/parser/success/customHeadersB.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/success/customHeadersB.dhall @@ -0,0 +1,17 @@ +[ + 24, + null, + 0, + [ + 24, + null, + 0, + 3, + "headers.dhall" + ], + 1, + "example.com", + "foo", + null, + null +] diff --git a/tests/parser/success/doubleB.dhall b/tests/parser/success/doubleB.dhall --- a/tests/parser/success/doubleB.dhall +++ b/tests/parser/success/doubleB.dhall @@ -1,24 +1,9 @@ [ 4, null, - [ - 17, - 1.1 - ], - [ - 17, - -1.1 - ], - [ - 17, - 10.0 - ], - [ - 17, - 11.0 - ], - [ - 17, - -1.1 - ] + 1.1, + -1.1, + 10, + 11, + -1.1 ] diff --git a/tests/parser/success/environmentVariablesB.dhall b/tests/parser/success/environmentVariablesB.dhall --- a/tests/parser/success/environmentVariablesB.dhall +++ b/tests/parser/success/environmentVariablesB.dhall @@ -3,11 +3,15 @@ null, [ 24, + null, + 0, 6, "FOO" ], [ 24, + null, + 0, 6, "\\\"\\\\\\a\\b\\f\\n\\r\\t\\v" ] diff --git a/tests/parser/success/importAltB.dhall b/tests/parser/success/importAltB.dhall --- a/tests/parser/success/importAltB.dhall +++ b/tests/parser/success/importAltB.dhall @@ -12,22 +12,30 @@ 11, [ 24, + null, + 1, 6, "UNSET1" ], [ 24, + null, + 0, 6, "UNSET2" ] ], [ 24, + null, + 0, 7 ] ], [ 24, + null, + 0, 6, "UNSET3" ] diff --git a/tests/parser/success/parenthesizeUsingB.dhall b/tests/parser/success/parenthesizeUsingB.dhall --- a/tests/parser/success/parenthesizeUsingB.dhall +++ b/tests/parser/success/parenthesizeUsingB.dhall @@ -1,5 +1,20 @@ [ 24, + [ + "sha256", + "b0e3ec1797b32c80c0bcb7e8254b08c7e9e35e75e6b410c7ac21477ab90167ad" + ], + 0, + [ + 24, + [ + "sha256", + "16173e984d35ee3ffd8b6b79167df89480e67d1cd03ea5d0fc93689e4d928e61" + ], + 0, + 3, + "a.dhall" + ], 1, "raw.githubusercontent.com", "dhall-lang", diff --git a/tests/parser/success/pathTerminationA.dhall b/tests/parser/success/pathTerminationA.dhall --- a/tests/parser/success/pathTerminationA.dhall +++ b/tests/parser/success/pathTerminationA.dhall @@ -1,3 +1,3 @@ -- Verify that certain punctuation marks terminate paths correctly λ(x : ./example) -→ ./example[./example, ./example{bar = ./example, qux = ./example}, ./example] +→ [./example, {bar = , qux = ./example}, ./example] diff --git a/tests/parser/success/pathTerminationB.dhall b/tests/parser/success/pathTerminationB.dhall --- a/tests/parser/success/pathTerminationB.dhall +++ b/tests/parser/success/pathTerminationB.dhall @@ -3,65 +3,51 @@ "x", [ 24, + null, + 0, 3, "example" ], [ - 0, + 4, + null, [ 24, + null, + 0, 3, "example" ], [ - 4, - null, - [ - 24, - 3, - "example" - ], - [ - 0, - [ + 8, + { + "qux": [ 24, + null, + 0, 3, "example" ], - [ - 8, - { - "bar": [ - 0, - [ - 24, - 3, - "example" - ], - [ - 12, - "baz", - [ - 24, - 3, - "example" - ], - {} - ] - ], - "qux": [ - 24, - 3, - "example" - ] - } + "bar": [ + 12, + "baz", + [ + 24, + null, + 0, + 3, + "example" + ], + {} ] - ], - [ - 24, - 3, - "example" - ] + } + ], + [ + 24, + null, + 0, + 3, + "example" ] ] ] diff --git a/tests/parser/success/pathsB.dhall b/tests/parser/success/pathsB.dhall --- a/tests/parser/success/pathsB.dhall +++ b/tests/parser/success/pathsB.dhall @@ -3,18 +3,24 @@ null, [ 24, + null, + 0, 2, "absolute", "path" ], [ 24, + null, + 0, 3, "relative", "path" ], [ 24, + null, + 0, 5, "home", "anchored", @@ -22,6 +28,8 @@ ], [ 24, + null, + 0, 2, "ipfs", "QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx", diff --git a/tests/parser/success/quotedPathsB.dhall b/tests/parser/success/quotedPathsB.dhall --- a/tests/parser/success/quotedPathsB.dhall +++ b/tests/parser/success/quotedPathsB.dhall @@ -3,6 +3,8 @@ { "example0": [ 24, + null, + 0, 2, "foo", "bar", @@ -10,6 +12,9 @@ ], "example1": [ 24, + null, + 0, + null, 1, "example.com", "foo", diff --git a/tests/parser/success/urlsB.dhall b/tests/parser/success/urlsB.dhall --- a/tests/parser/success/urlsB.dhall +++ b/tests/parser/success/urlsB.dhall @@ -3,7 +3,10 @@ null, [ 24, + null, 0, + null, + 0, "example.com", "someFile.dhall", null, @@ -11,6 +14,9 @@ ], [ 24, + null, + 0, + null, 1, "john:doe@example.com:8080", "foo", @@ -20,7 +26,10 @@ ], [ 24, + null, 0, + null, + 0, "prelude.dhall-lang.org", "package.dhall", null, @@ -28,6 +37,9 @@ ], [ 24, + null, + 0, + null, 1, "ipfs.io", "ipfs", @@ -38,6 +50,9 @@ ], [ 24, + null, + 0, + null, 1, "raw.githubusercontent.com", "dhall-lang", @@ -50,6 +65,9 @@ ], [ 24, + null, + 0, + null, 1, "127.0.0.1", "index.dhall", @@ -58,6 +76,9 @@ ], [ 24, + null, + 0, + null, 1, "[::]", "index.dhall", @@ -66,6 +87,9 @@ ], [ 24, + null, + 0, + null, 1, "[2001:0db8:85a3:0000:0000:8a2e:0370:7334]", "tutorial.dhall", @@ -74,6 +98,9 @@ ], [ 24, + null, + 0, + null, 1, "-._~%2C!$&'()*+,;=:@-._~%2C!$&'()*+,;=:", "foo", diff --git a/tests/regression/issue164.dhall b/tests/regression/issue164.dhall --- a/tests/regression/issue164.dhall +++ b/tests/regression/issue164.dhall @@ -1,1 +1,2 @@ -''Single quotes like ' should be allowed in a single-quoted string'' +'' +Single quotes like ' should be allowed in a single-quoted string'' diff --git a/tests/tutorial/unions4B.dhall b/tests/tutorial/unions4B.dhall --- a/tests/tutorial/unions4B.dhall +++ b/tests/tutorial/unions4B.dhall @@ -1,6 +1,1 @@ -{ Empty = - λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } > -, Person = - λ(Person : { age : Natural, name : Text }) - → < Person = Person | Empty : {} > -} +< Empty : {} | Person : { name : Text, age : Natural } > diff --git a/tests/typecheck/failure/mixedUnions.dhall b/tests/typecheck/failure/mixedUnions.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/failure/mixedUnions.dhall @@ -0,0 +1,1 @@ +< Left : Natural | Right : Type > diff --git a/tests/typecheck/success/encodedRecordOfTypesA.dhall b/tests/typecheck/success/encodedRecordOfTypesA.dhall deleted file mode 100644 --- a/tests/typecheck/success/encodedRecordOfTypesA.dhall +++ /dev/null @@ -1,3 +0,0 @@ - λ(k : Kind) -→ λ(makeRecord : ∀(x : Type) → ∀(y : Type → Type) → k) -→ makeRecord Text List diff --git a/tests/typecheck/success/encodedRecordOfTypesB.dhall b/tests/typecheck/success/encodedRecordOfTypesB.dhall deleted file mode 100644 --- a/tests/typecheck/success/encodedRecordOfTypesB.dhall +++ /dev/null @@ -1,1 +0,0 @@ -∀(k : Kind) → ∀(makeRecord : ∀(x : Type) → ∀(y : Type → Type) → k) → k diff --git a/tests/typecheck/success/recordOfRecordOfTypesA.dhall b/tests/typecheck/success/recordOfRecordOfTypesA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/success/recordOfRecordOfTypesA.dhall @@ -0,0 +1,3 @@ +let types = { Scopes = < Public : {} | Private : {} >} +let prelude = { types = types } +in prelude.types.Scopes.Public {=} diff --git a/tests/typecheck/success/recordOfRecordOfTypesB.dhall b/tests/typecheck/success/recordOfRecordOfTypesB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/success/recordOfRecordOfTypesB.dhall @@ -0,0 +1,1 @@ +< Public : {} | Private : {} > diff --git a/tests/typecheck/success/simple/unionsOfTypesA.dhall b/tests/typecheck/success/simple/unionsOfTypesA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/success/simple/unionsOfTypesA.dhall @@ -0,0 +1,1 @@ +< Left = List | Right : Type > diff --git a/tests/typecheck/success/simple/unionsOfTypesB.dhall b/tests/typecheck/success/simple/unionsOfTypesB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/success/simple/unionsOfTypesB.dhall @@ -0,0 +1,1 @@ +< Left : Type → Type | Right : Type >