diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,46 @@ +1.17.0 + +* This release corresponds to version 2.0.0 of the language standard +* BREAKING CHANGE TO THE LANGUAGE AND API: Binary serialization support + * This is a breaking change to the hash for all semantic integrity checks + * The hash used by the semantic integrity check is now based on the + binary representation instead of a text representation of the + expression + * You can pin the new hashes by supplying the `--protocol-version 1.0` + option on the command line until you need support for newer language + features + * This also includes a breaking change to `ImportType` in the API +* BREAKING CHANGE TO THE LANGUAGE: Disallow combining records of terms and + types + * This is mainly for consistency and to improve type errors that would + have otherwise happened further downstream + * This should not affect the vast majority of code + * See: https://github.com/dhall-lang/dhall-haskell/pull/538 +* BUG FIX: Semantic integrity checks now work for imported expression using + the `constructors` keyword + * See: https://github.com/dhall-lang/dhall-haskell/pull/554 +* BUG FIX: Fix α-normalization of expressions with bound variables named `_` + * See: https://github.com/dhall-lang/dhall-haskell/pull/524 +* BUG FIX: Fix `isNormalized` to match `normalize` + * See: https://github.com/dhall-lang/dhall-haskell/pull/522 +* BUG FIX: `dhall lint` now correctly handles nested `let` expressions + * See: https://github.com/dhall-lang/dhall-haskell/pull/555 +* FEATURE: Imports protected by a semantic integrity check are now cached + * See: https://github.com/dhall-lang/dhall-haskell/pull/533 +* The default `dhall` command no longer outputs the type to `stderr` + * You can add back the type as a type annotation using the + `--annotate` switch + * See: https://github.com/dhall-lang/dhall-haskell/pull/544 +* New utilities for building `InputTypes` + * See: https://github.com/dhall-lang/dhall-haskell/pull/530 +* Improve parsing performance for long variable names + * See: https://github.com/dhall-lang/dhall-haskell/pull/526 +* More succinct type diffs for function types + * See: https://github.com/dhall-lang/dhall-haskell/pull/540 +* Identifier names can now begin with keywords + * i.e. `ifChanged` and `lettuce` are now legal identifiers + * See: https://github.com/dhall-lang/dhall-haskell/pull/551 + 1.16.1 * Fix test failure due to missing test data file diff --git a/benchmark/deep-nested-large-record/Main.hs b/benchmark/deep-nested-large-record/Main.hs --- a/benchmark/deep-nested-large-record/Main.hs +++ b/benchmark/deep-nested-large-record/Main.hs @@ -1,8 +1,9 @@ {-# LANGUAGE OverloadedStrings #-} module Main (main) where -import qualified Criterion as Criterion import Criterion.Main (defaultMain) + +import qualified Criterion as Criterion import qualified Data.Sequence as Seq import qualified Dhall.Core as Core import qualified Dhall.Import as Import diff --git a/benchmark/parser/Main.hs b/benchmark/parser/Main.hs --- a/benchmark/parser/Main.hs +++ b/benchmark/parser/Main.hs @@ -8,9 +8,12 @@ import System.Directory +import qualified Codec.Serialise import qualified Criterion.Main as Criterion +import qualified Data.ByteString.Lazy import qualified Data.Text as T import qualified Data.Text.IO as TIO +import qualified Dhall.Binary import qualified Dhall.Parser as Dhall type PreludeFiles = Map FilePath T.Text @@ -42,12 +45,29 @@ benchExprFromText name expr = bench name $ whnf (Dhall.exprFromText "(input)") expr +benchExprFromBytes + :: String -> Data.ByteString.Lazy.ByteString -> Criterion.Benchmark +benchExprFromBytes name bytes = bench name (whnf f bytes) + where + f bytes = do + term <- case Codec.Serialise.deserialiseOrFail bytes of + Left _ -> Nothing + Right term -> return term + case Dhall.Binary.decode term of + Left _ -> Nothing + Right expression -> return expression + main :: IO () main = do prelude <- loadPreludeFiles - issue108 <- TIO.readFile "benchmark/examples/issue108.dhall" + issue108Text <- TIO.readFile "benchmark/examples/issue108.dhall" + issue108Bytes <- Data.ByteString.Lazy.readFile "benchmark/examples/issue108.dhall.bin" defaultMain - [ benchParser prelude - , bgroup "Issue #108" $ - [ benchExprFromText "108" issue108 ] + [ bgroup "Issue #108" + [ benchExprFromText "Text" issue108Text + , benchExprFromBytes "Binary" issue108Bytes + ] + , benchExprFromText "Long variable names" (T.replicate 1000000 "x") + , benchExprFromText "Large number of function arguments" (T.replicate 10000 "x ") + , benchParser prelude ] diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.16.1 +Version: 1.17.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -173,13 +173,15 @@ ansi-terminal >= 0.6.3.1 && < 0.9 , bytestring < 0.11, case-insensitive < 1.3 , + cborg >= 0.2.0.0 && < 0.3 , containers >= 0.5.0.0 && < 0.6 , contravariant < 1.6 , cryptonite >= 0.23 && < 1.0 , Diff >= 0.2 && < 0.4 , - directory >= 1.3 && < 1.4 , + directory >= 1.2.7.1 && < 1.4 , exceptions >= 0.8.3 && < 0.11, filepath >= 1.4 && < 1.5 , + hashable < 1.3 , haskeline >= 0.7.3.0 && < 0.8 , insert-ordered-containers >= 0.2.1.0 && < 0.3 , lens-family-core >= 1.0.0 && < 1.3 , @@ -191,6 +193,7 @@ prettyprinter >= 1.2.0.1 && < 1.3 , prettyprinter-ansi-terminal >= 1.1.1 && < 1.2 , repline >= 0.1.6.0 && < 0.2 , + serialise >= 0.2.0.0 && < 0.3 , scientific >= 0.3.0.0 && < 0.4 , template-haskell < 2.14, text >= 0.11.1.0 && < 1.3 , @@ -207,6 +210,7 @@ Exposed-Modules: Dhall, + Dhall.Binary, Dhall.Context, Dhall.Core, Dhall.Diff, @@ -253,19 +257,27 @@ Import Normalization Parser + QuickCheck Regression Tutorial TypeCheck Util Build-Depends: base >= 4 && < 5 , + containers , deepseq >= 1.2.0.1 && < 1.5 , dhall , - insert-ordered-containers , + hashable , + insert-ordered-containers == 0.2.1.0 , prettyprinter , + QuickCheck >= 2.10 && < 2.12, + quickcheck-instances >= 0.3.12 && < 0.4 , + serialise , tasty >= 0.11.2 && < 1.2 , tasty-hunit >= 0.9.2 && < 0.11, + tasty-quickcheck >= 0.9.2 && < 0.11, text >= 0.11.1.0 && < 1.3 , + transformers , vector >= 0.11.0.0 && < 0.13 Default-Language: Haskell2010 @@ -287,10 +299,12 @@ Main-Is: benchmark/parser/Main.hs Build-Depends: base >= 4 && < 5 , + bytestring , containers >= 0.5.0.0 && < 0.6, criterion >= 1.1 && < 1.6, dhall , - directory >= 1.3 && < 1.4, + directory >= 1.2.7.1 && < 1.4, + serialise , text >= 0.11.1.0 && < 1.3 Default-Language: Haskell2010 diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -28,6 +28,7 @@ , sourceName , startingContext , normalizer + , protocolVersion , defaultInputSettings , InputSettings , defaultEvaluateSettings @@ -66,9 +67,15 @@ , Inject(..) , inject + , RecordInputType(..) + , inputFieldWith + , inputField + , inputRecord -- * Miscellaneous , rawInput + , (>$<) + , (>*<) -- * Re-exports , Natural @@ -81,7 +88,8 @@ import Control.Applicative (empty, liftA2, (<|>), Alternative) import Control.Exception (Exception) import Control.Monad.Trans.State.Strict -import Data.Functor.Contravariant (Contravariant(..)) +import Data.Functor.Contravariant (Contravariant(..), (>$<)) +import Data.Functor.Contravariant.Divisible (Divisible(..), divided) import Data.Monoid ((<>)) import Data.Scientific (Scientific) import Data.Sequence (Seq) @@ -89,18 +97,20 @@ import Data.Typeable (Typeable) import Data.Vector (Vector) import Data.Word (Word8, Word16, Word32, Word64) +import Dhall.Binary (ProtocolVersion(..)) import Dhall.Core (Expr(..), Chunks(..)) import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..)) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) import GHC.Generics -import Lens.Family (LensLike', view) +import Lens.Family (LensLike', set, view) import Numeric.Natural (Natural) import Prelude hiding (maybe, sequence) import System.FilePath (takeDirectory) import qualified Control.Applicative import qualified Control.Exception +import qualified Control.Monad.Trans.State.Strict as State import qualified Data.Foldable import qualified Data.Functor.Compose import qualified Data.Functor.Product @@ -112,6 +122,7 @@ import qualified Data.Text.IO import qualified Data.Text.Lazy import qualified Data.Vector +import qualified Dhall.Binary import qualified Dhall.Context import qualified Dhall.Core import qualified Dhall.Import @@ -189,7 +200,8 @@ -- | @since 1.16 data EvaluateSettings = EvaluateSettings { _startingContext :: Dhall.Context.Context (Expr Src X) - , _normalizer :: Dhall.Core.ReifiedNormalizer X + , _normalizer :: Dhall.Core.ReifiedNormalizer X + , _protocolVersion :: ProtocolVersion } -- | Default evaluation settings: no extra entries in the initial @@ -199,7 +211,8 @@ defaultEvaluateSettings :: EvaluateSettings defaultEvaluateSettings = EvaluateSettings { _startingContext = Dhall.Context.empty - , _normalizer = Dhall.Core.ReifiedNormalizer (const Nothing) + , _normalizer = Dhall.Core.ReifiedNormalizer (const Nothing) + , _protocolVersion = Dhall.Binary.defaultProtocolVersion } -- | Access the starting context used for evaluation and type-checking. @@ -226,6 +239,17 @@ => LensLike' f EvaluateSettings (Dhall.Core.ReifiedNormalizer X) l k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s)) +-- | Access the protocol version used when encoding or decoding Dhall +-- expressions to and from a binary representation +-- +-- @since 1.17 +protocolVersion + :: (Functor f, HasEvaluateSettings s) + => LensLike' f s ProtocolVersion +protocolVersion = evaluateSettings . l + where + l k s = fmap (\x -> s { _protocolVersion = x}) (k (_protocolVersion s)) + -- | @since 1.16 class HasEvaluateSettings s where evaluateSettings @@ -282,12 +306,20 @@ -- ^ The decoded value in Haskell inputWithSettings settings (Type {..}) txt = do expr <- throws (Dhall.Parser.exprFromText (view sourceName settings) txt) - expr' <- Dhall.Import.loadDirWith - (view rootDirectory settings) - Dhall.Import.exprFromImport - (view startingContext settings) - (Dhall.Core.getReifiedNormalizer (view normalizer settings)) - expr + + let InputSettings {..} = settings + + let EvaluateSettings {..} = _evaluateSettings + + let transform = + set Dhall.Import.protocolVersion _protocolVersion + . set Dhall.Import.normalizer _normalizer + . set Dhall.Import.startingContext _startingContext + + let status = transform (Dhall.Import.emptyStatus _rootDirectory) + + expr' <- State.evalStateT (Dhall.Import.loadWith expr) status + let suffix = Dhall.Pretty.Internal.prettyToStrictText expected let annot = case expr' of Note (Src begin end bytes) _ -> @@ -367,12 +399,20 @@ -- ^ The fully normalized AST inputExprWithSettings settings txt = do expr <- throws (Dhall.Parser.exprFromText (view sourceName settings) txt) - expr' <- Dhall.Import.loadDirWith - (view rootDirectory settings) - Dhall.Import.exprFromImport - (view startingContext settings) - (Dhall.Core.getReifiedNormalizer (view normalizer settings)) - expr + + let InputSettings {..} = settings + + let EvaluateSettings {..} = _evaluateSettings + + let transform = + set Dhall.Import.protocolVersion _protocolVersion + . set Dhall.Import.normalizer _normalizer + . set Dhall.Import.startingContext _startingContext + + let status = transform (Dhall.Import.emptyStatus _rootDirectory) + + expr' <- State.evalStateT (Dhall.Import.loadWith expr) status + _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) expr') pure (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr') @@ -658,9 +698,9 @@ vector :: Type a -> Type (Vector a) vector = fmap Data.Vector.fromList . list -{-| Decode `()` from an empty record. +{-| Decode @()@ from an empty record. ->>> input unit "{=}" -- GHC doesn't print the result if it is @()@ +>>> input unit "{=}" -- GHC doesn't print the result if it is () -} unit :: Type () @@ -677,7 +717,7 @@ >>> input string "\"ABC\"" "ABC" -"-} +-} string :: Type String string = Data.Text.Lazy.unpack <$> lazyText @@ -1333,3 +1373,87 @@ ) ( Data.Functor.Compose.Compose extractBody ) ) + +{-| The 'RecordInputType' divisible (contravariant) functor allows you to build + an 'InputType' injector for a Dhall record. + + For example, let's take the following Haskell data type: + +> data Project = Project +> { projectName :: Text +> , projectDescription :: Text +> , projectStars :: Natural +> } + + And assume that we have the following Dhall record that we would like to + parse as a @Project@: + +> { name = +> "dhall-haskell" +> , description = +> "A configuration language guaranteed to terminate" +> , stars = +> 289 +> } + + Our injector has type 'InputType' @Project@, but we can't build that out of any + smaller injectors, as 'InputType's cannot be combined (they are only 'Contravariant's). + However, we can use an 'InputRecordType' to build an 'InputType' for @Project@: + +> injectProject :: InputType Project +> injectProject = +> inputRecord +> ( adapt >$< inputFieldWith "name" inject +> >*< inputFieldWith "description" inject +> >*< inputFieldWith "stars" inject +> ) +> where +> adapt (Project{..}) = (projectName, (projectDescription, projectStars)) + + Or, since we are simply using the `Inject` instance to inject each field, we could write + +> injectProject :: InputType Project +> injectProject = +> inputRecord +> ( adapt >$< inputField "name" +> >*< inputField "description" +> >*< inputField "stars" +> ) +> where +> adapt (Project{..}) = (projectName, (projectDescription, projectStars)) + +-} + +-- | Infix 'divided' +(>*<) :: Divisible f => f a -> f b -> f (a, b) +(>*<) = divided + +infixr 5 >*< + +newtype RecordInputType a + = RecordInputType (Data.HashMap.Strict.InsOrd.InsOrdHashMap Text (InputType a)) + +instance Contravariant RecordInputType where + contramap f (RecordInputType inputTypeRecord) = RecordInputType $ contramap f <$> inputTypeRecord + +instance Divisible RecordInputType where + divide f (RecordInputType bInputTypeRecord) (RecordInputType cInputTypeRecord) = + RecordInputType + $ Data.HashMap.Strict.InsOrd.union + ((contramap $ fst . f) <$> bInputTypeRecord) + ((contramap $ snd . f) <$> cInputTypeRecord) + conquer = RecordInputType Data.HashMap.Strict.InsOrd.empty + +inputFieldWith :: Text -> InputType a -> RecordInputType a +inputFieldWith name inputType = RecordInputType $ Data.HashMap.Strict.InsOrd.singleton name inputType + +inputField :: Inject a => Text -> RecordInputType a +inputField name = inputFieldWith name inject + +inputRecord :: RecordInputType a -> InputType a +inputRecord (RecordInputType inputTypeRecord) = InputType makeRecordLit recordType + where + recordType = Record $ declared <$> inputTypeRecord + makeRecordLit x = RecordLit $ (($ x) . embed) <$> inputTypeRecord + + diff --git a/src/Dhall/Binary.hs b/src/Dhall/Binary.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Binary.hs @@ -0,0 +1,795 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} + +{-| This module contains logic for converting Dhall expressions to and from + CBOR expressions which can in turn be converted to and from a binary + representation +-} + +module Dhall.Binary + ( -- * Protocol versions + ProtocolVersion(..) + , defaultProtocolVersion + , parseProtocolVersion + + -- * Encoding and decoding + , encode + , decode + + -- * Exceptions + , DecodingFailure(..) + ) where + +import Codec.CBOR.Term (Term(..)) +import Control.Applicative (empty) +import Control.Exception (Exception) +import Dhall.Core + ( Chunks(..) + , Const(..) + , Directory(..) + , Expr(..) + , File(..) + , FilePrefix(..) + , Import(..) + , ImportHashed(..) + , ImportMode(..) + , ImportType(..) + , Scheme(..) + , URL(..) + , Var(..) + ) +import Data.Monoid ((<>)) +import Data.Text (Text) +import Options.Applicative (Parser) +import Prelude hiding (exponent) + +import qualified Data.Foldable +import qualified Data.HashMap.Strict.InsOrd +import qualified Data.Scientific +import qualified Data.Sequence +import qualified Data.Set +import qualified Data.Text +import qualified Options.Applicative + +-- | Supported protocol version strings +data ProtocolVersion + = V_1_0 + -- ^ Protocol version string "1.0" + +defaultProtocolVersion :: ProtocolVersion +defaultProtocolVersion = V_1_0 + +parseProtocolVersion :: Parser ProtocolVersion +parseProtocolVersion = + Options.Applicative.option readProtocolVersion + ( Options.Applicative.long "protocol-version" + <> Options.Applicative.metavar "X.Y" + <> Options.Applicative.value defaultProtocolVersion + ) + where + readProtocolVersion = do + string <- Options.Applicative.str + case string :: Text of + "1.0" -> return V_1_0 + _ -> fail "Unsupported protocol version" + +{-| Convert a function applied to multiple arguments to the base function and + the list of arguments +-} +unApply :: Expr s a -> (Expr s a, [Expr s a]) +unApply e = (baseFunction₀, diffArguments₀ []) + where + ~(baseFunction₀, diffArguments₀) = go e + + go (App f a) = (baseFunction, diffArguments . (a :)) + where + ~(baseFunction, diffArguments) = go f + go baseFunction = (baseFunction, id) + +encode_1_0 :: Expr s Import -> Term +encode_1_0 (Var (V "_" n)) = + TInteger n +encode_1_0 (Var (V x 0)) = + TString x +encode_1_0 (Var (V x n)) = + TList [ TString x, TInteger n ] +encode_1_0 NaturalBuild = + TString "Natural/build" +encode_1_0 NaturalFold = + TString "Natural/fold" +encode_1_0 NaturalIsZero = + TString "Natural/isZero" +encode_1_0 NaturalEven = + TString "Natural/even" +encode_1_0 NaturalOdd = + TString "Natural/odd" +encode_1_0 NaturalToInteger = + TString "Natural/toInteger" +encode_1_0 NaturalShow = + TString "Natural/show" +encode_1_0 IntegerToDouble = + TString "Integer/toDouble" +encode_1_0 IntegerShow = + TString "Integer/show" +encode_1_0 DoubleShow = + TString "Double/show" +encode_1_0 ListBuild = + TString "List/build" +encode_1_0 ListFold = + TString "List/fold" +encode_1_0 ListLength = + TString "List/length" +encode_1_0 ListHead = + TString "List/head" +encode_1_0 ListLast = + TString "List/last" +encode_1_0 ListIndexed = + TString "List/indexed" +encode_1_0 ListReverse = + TString "List/reverse" +encode_1_0 OptionalFold = + TString "Optional/fold" +encode_1_0 OptionalBuild = + TString "Optional/build" +encode_1_0 Bool = + TString "Bool" +encode_1_0 Optional = + TString "Optional" +encode_1_0 Natural = + TString "Natural" +encode_1_0 Integer = + TString "Integer" +encode_1_0 Double = + TString "Double" +encode_1_0 Text = + TString "Text" +encode_1_0 List = + TString "List" +encode_1_0 (Const Type) = + TString "Type" +encode_1_0 (Const Kind) = + TString "Kind" +encode_1_0 e@(App _ _) = + TList ([ TInt 0, f₁ ] ++ map encode_1_0 arguments) + where + (f₀, arguments) = unApply e + + f₁ = encode_1_0 f₀ +encode_1_0 (Lam "_" _A₀ b₀) = + TList [ TInt 1, _A₁, b₁ ] + where + _A₁ = encode_1_0 _A₀ + b₁ = encode_1_0 b₀ +encode_1_0 (Lam x _A₀ b₀) = + TList [ TInt 1, TString x, _A₁, b₁ ] + where + _A₁ = encode_1_0 _A₀ + b₁ = encode_1_0 b₀ +encode_1_0 (Pi "_" _A₀ _B₀) = + TList [ TInt 2, _A₁, _B₁ ] + where + _A₁ = encode_1_0 _A₀ + _B₁ = encode_1_0 _B₀ +encode_1_0 (Pi x _A₀ _B₀) = + TList [ TInt 2, TString x, _A₁, _B₁ ] + where + _A₁ = encode_1_0 _A₀ + _B₁ = encode_1_0 _B₀ +encode_1_0 (BoolOr l₀ r₀) = + TList [ TInt 3, TInt 0, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (BoolAnd l₀ r₀) = + TList [ TInt 3, TInt 1, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (BoolEQ l₀ r₀) = + TList [ TInt 3, TInt 2, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (BoolNE l₀ r₀) = + TList [ TInt 3, TInt 3, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (NaturalPlus l₀ r₀) = + TList [ TInt 3, TInt 4, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (NaturalTimes l₀ r₀) = + TList [ TInt 3, TInt 5, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (TextAppend l₀ r₀) = + TList [ TInt 3, TInt 6, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (ListAppend l₀ r₀) = + TList [ TInt 3, TInt 7, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (Combine l₀ r₀) = + TList [ TInt 3, TInt 8, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (Prefer l₀ r₀) = + TList [ TInt 3, TInt 9, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (CombineTypes l₀ r₀) = + TList [ TInt 3, TInt 10, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (ImportAlt l₀ r₀) = + TList [ TInt 3, TInt 11, l₁, r₁ ] + where + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (ListLit _T₀ xs₀) + | null xs₀ = TList [ TInt 4, _T₁ ] + | otherwise = TList ([ TInt 4, TNull ] ++ xs₁) + where + _T₁ = case _T₀ of + Nothing -> TNull + Just t -> encode_1_0 t + + xs₁ = map encode_1_0 (Data.Foldable.toList xs₀) +encode_1_0 (OptionalLit _T₀ Nothing) = + TList [ TInt 5, _T₁ ] + where + _T₁ = encode_1_0 _T₀ +encode_1_0 (OptionalLit _T₀ (Just t₀)) = + TList [ TInt 5, _T₁, t₁ ] + where + _T₁ = encode_1_0 _T₀ + t₁ = encode_1_0 t₀ +encode_1_0 (Merge t₀ u₀ Nothing) = + TList [ TInt 6, t₁, u₁ ] + where + t₁ = encode_1_0 t₀ + u₁ = encode_1_0 u₀ +encode_1_0 (Merge t₀ u₀ (Just _T₀)) = + TList [ TInt 6, t₁, u₁, _T₁ ] + where + t₁ = encode_1_0 t₀ + u₁ = encode_1_0 u₀ + _T₁ = encode_1_0 _T₀ +encode_1_0 (Record xTs₀) = + TList [ TInt 7, TMap xTs₁ ] + where + xTs₁ = do + (x₀, _T₀) <- Data.HashMap.Strict.InsOrd.toList xTs₀ + let x₁ = TString x₀ + let _T₁ = encode_1_0 _T₀ + return (x₁, _T₁) +encode_1_0 (RecordLit xts₀) = + TList [ TInt 8, TMap xts₁ ] + where + xts₁ = do + (x₀, t₀) <- Data.HashMap.Strict.InsOrd.toList xts₀ + let x₁ = TString x₀ + let t₁ = encode_1_0 t₀ + return (x₁, t₁) +encode_1_0 (Field t₀ x) = + TList [ TInt 9, t₁, TString x ] + where + t₁ = encode_1_0 t₀ +encode_1_0 (Project t₀ xs₀) = + TList ([ TInt 10, t₁ ] ++ xs₁) + where + t₁ = encode_1_0 t₀ + xs₁ = map TString (Data.Foldable.toList xs₀) +encode_1_0 (Union xTs₀) = + TList [ TInt 11, TMap xTs₁ ] + where + xTs₁ = do + (x₀, _T₀) <- Data.HashMap.Strict.InsOrd.toList xTs₀ + let x₁ = TString x₀ + let _T₁ = encode_1_0 _T₀ + return (x₁, _T₁) +encode_1_0 (UnionLit x t₀ yTs₀) = + TList [ TInt 12, TString x, t₁, TMap yTs₁ ] + where + t₁ = encode_1_0 t₀ + + yTs₁ = do + (y₀, _T₀) <- Data.HashMap.Strict.InsOrd.toList yTs₀ + let y₁ = TString y₀ + let _T₁ = encode_1_0 _T₀ + return (y₁, _T₁) +encode_1_0 (Constructors u₀) = + TList [ TInt 13, u₁ ] + where + u₁ = encode_1_0 u₀ +encode_1_0 (BoolLit b) = + TBool b +encode_1_0 (BoolIf t₀ l₀ r₀) = + TList [ TInt 14, t₁, l₁, r₁ ] + where + t₁ = encode_1_0 t₀ + l₁ = encode_1_0 l₀ + r₁ = encode_1_0 r₀ +encode_1_0 (NaturalLit n) = + TList [ TInt 15, TInteger (fromIntegral n) ] +encode_1_0 (IntegerLit n) = + TList [ TInt 16, TInteger n ] +encode_1_0 (DoubleLit n) = + TList [ TInt 17, TTagged 4 (TList [ TInt exponent, TInteger mantissa ]) ] + where + normalized = Data.Scientific.normalize n + + exponent = Data.Scientific.base10Exponent normalized + + mantissa = Data.Scientific.coefficient normalized +encode_1_0 (TextLit (Chunks xys₀ z₀)) = + TList ([ TInt 18 ] ++ xys₁ ++ [ z₁ ]) + where + xys₁ = do + (x₀, y₀) <- xys₀ + let x₁ = TString x₀ + let y₁ = encode_1_0 y₀ + [ x₁, y₁ ] + + z₁ = TString z₀ +encode_1_0 (Embed x) = + importToTerm x +encode_1_0 (Let x Nothing a₀ b₀) = + TList [ TInt 25, TString x, a₁, b₁ ] + where + a₁ = encode_1_0 a₀ + b₁ = encode_1_0 b₀ +encode_1_0 (Let x (Just _A₀) a₀ b₀) = + TList [ TInt 25, TString x, _A₁, a₁, b₁ ] + where + a₁ = encode_1_0 a₀ + _A₁ = encode_1_0 _A₀ + b₁ = encode_1_0 b₀ +encode_1_0 (Annot t₀ _T₀) = + TList [ TInt 26, t₁, _T₁ ] + where + t₁ = encode_1_0 t₀ + _T₁ = encode_1_0 _T₀ +encode_1_0 (Note _ e) = + encode_1_0 e + +importToTerm :: Import -> Term +importToTerm import_ = + case importType of + Remote (URL { scheme = scheme₀, ..}) -> + TList + ( [ TInt 24, TInt scheme₁, 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 + scheme₁ = case scheme₀ of + HTTP -> 0 + HTTPS -> 1 + File {..} = path + + Directory {..} = directory + + Local prefix₀ path -> + TList + ( [ TInt 24, TInt prefix₁ ] + ++ map TString components₁ + ++ [ TString file ] + ) + where + File {..} = path + + 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) + + Env x -> + TList [ TInt 24, TInt 6, TString x ] + + Missing -> + TList [ TInt 24, TInt 7 ] + where + Import {..} = import_ + + ImportHashed {..} = importHashed + +decode_1_0 :: Term -> Maybe (Expr s Import) +decode_1_0 (TInt n) = + return (Var (V "_" (fromIntegral n))) +decode_1_0 (TInteger n) = + return (Var (V "_" n)) +decode_1_0 (TString "Natural/build") = + return NaturalBuild +decode_1_0 (TString "Natural/fold") = + return NaturalFold +decode_1_0 (TString "Natural/isZero") = + return NaturalIsZero +decode_1_0 (TString "Natural/even") = + return NaturalEven +decode_1_0 (TString "Natural/odd") = + return NaturalOdd +decode_1_0 (TString "Natural/toInteger") = + return NaturalToInteger +decode_1_0 (TString "Natural/show") = + return NaturalShow +decode_1_0 (TString "Integer/toDouble") = + return IntegerToDouble +decode_1_0 (TString "Integer/show") = + return IntegerShow +decode_1_0 (TString "Double/show") = + return DoubleShow +decode_1_0 (TString "List/build") = + return ListBuild +decode_1_0 (TString "List/fold") = + return ListFold +decode_1_0 (TString "List/length") = + return ListLength +decode_1_0 (TString "List/head") = + return ListHead +decode_1_0 (TString "List/last") = + return ListLast +decode_1_0 (TString "List/indexed") = + return ListIndexed +decode_1_0 (TString "List/reverse") = + return ListReverse +decode_1_0 (TString "Optional/fold") = + return OptionalFold +decode_1_0 (TString "Optional/build") = + return OptionalBuild +decode_1_0 (TString "Bool") = + return Bool +decode_1_0 (TString "Optional") = + return Optional +decode_1_0 (TString "Natural") = + return Natural +decode_1_0 (TString "Integer") = + return Integer +decode_1_0 (TString "Double") = + return Double +decode_1_0 (TString "Text") = + return Text +decode_1_0 (TString "List") = + return List +decode_1_0 (TString "Type") = + return (Const Type) +decode_1_0 (TString "Kind") = + return (Const Kind) +decode_1_0 (TString x) = + return (Var (V x 0)) +decode_1_0 (TList [ TString x, TInt n ]) = + return (Var (V x (fromIntegral n))) +decode_1_0 (TList [ TString x, TInteger n ]) = + return (Var (V x n)) +decode_1_0 (TList (TInt 0 : f₁ : xs₁)) = do + f₀ <- decode_1_0 f₁ + xs₀ <- traverse decode_1_0 xs₁ + return (foldl App f₀ xs₀) +decode_1_0 (TList [ TInt 1, _A₁, b₁ ]) = do + _A₀ <- decode_1_0 _A₁ + b₀ <- decode_1_0 b₁ + return (Lam "_" _A₀ b₀) +decode_1_0 (TList [ TInt 1, TString x, _A₁, b₁ ]) = do + _A₀ <- decode_1_0 _A₁ + b₀ <- decode_1_0 b₁ + return (Lam x _A₀ b₀) +decode_1_0 (TList [ TInt 2, _A₁, _B₁ ]) = do + _A₀ <- decode_1_0 _A₁ + _B₀ <- decode_1_0 _B₁ + return (Pi "_" _A₀ _B₀) +decode_1_0 (TList [ TInt 2, TString x, _A₁, _B₁ ]) = do + _A₀ <- decode_1_0 _A₁ + _B₀ <- decode_1_0 _B₁ + return (Pi x _A₀ _B₀) +decode_1_0 (TList [ TInt 3, TInt n, l₁, r₁ ]) = do + l₀ <- decode_1_0 l₁ + r₀ <- decode_1_0 r₁ + op <- case n of + 0 -> return BoolOr + 1 -> return BoolAnd + 2 -> return BoolEQ + 3 -> return BoolNE + 4 -> return NaturalPlus + 5 -> return NaturalTimes + 6 -> return TextAppend + 7 -> return ListAppend + 8 -> return Combine + 9 -> return Prefer + 10 -> return CombineTypes + 11 -> return ImportAlt + _ -> empty + return (op l₀ r₀) +decode_1_0 (TList [ TInt 4, _T₁ ]) = do + _T₀ <- decode_1_0 _T₁ + return (ListLit (Just _T₀) empty) +decode_1_0 (TList (TInt 4 : TNull : xs₁ )) = do + xs₀ <- traverse decode_1_0 xs₁ + return (ListLit Nothing (Data.Sequence.fromList xs₀)) +decode_1_0 (TList [ TInt 5, _T₁ ]) = do + _T₀ <- decode_1_0 _T₁ + return (OptionalLit _T₀ Nothing) +decode_1_0 (TList [ TInt 5, _T₁, t₁ ]) = do + _T₀ <- decode_1_0 _T₁ + t₀ <- decode_1_0 t₁ + return (OptionalLit _T₀ (Just t₀)) +decode_1_0 (TList [ TInt 6, t₁, u₁ ]) = do + t₀ <- decode_1_0 t₁ + u₀ <- decode_1_0 u₁ + return (Merge t₀ u₀ Nothing) +decode_1_0 (TList [ TInt 6, t₁, u₁, _T₁ ]) = do + t₀ <- decode_1_0 t₁ + u₀ <- decode_1_0 u₁ + _T₀ <- decode_1_0 _T₁ + return (Merge t₀ u₀ (Just _T₀)) +decode_1_0 (TList [ TInt 7, TMap xTs₁ ]) = do + let process (TString x, _T₁) = do + _T₀ <- decode_1_0 _T₁ + + return (x, _T₀) + process _ = + empty + + xTs₀ <- traverse process xTs₁ + + return (Record (Data.HashMap.Strict.InsOrd.fromList xTs₀)) +decode_1_0 (TList [ TInt 8, TMap xts₁ ]) = do + let process (TString x, t₁) = do + t₀ <- decode_1_0 t₁ + + return (x, t₀) + process _ = + empty + + xts₀ <- traverse process xts₁ + + return (RecordLit (Data.HashMap.Strict.InsOrd.fromList xts₀)) +decode_1_0 (TList [ TInt 9, t₁, TString x ]) = do + t₀ <- decode_1_0 t₁ + + return (Field t₀ x) +decode_1_0 (TList (TInt 10 : t₁ : xs₁)) = do + t₀ <- decode_1_0 t₁ + + let process (TString x) = return x + process _ = empty + + xs₀ <- traverse process xs₁ + + return (Project t₀ (Data.Set.fromList xs₀)) +decode_1_0 (TList [ TInt 11, TMap xTs₁ ]) = do + let process (TString x, _T₁) = do + _T₀ <- decode_1_0 _T₁ + + return (x, _T₀) + process _ = + empty + + xTs₀ <- traverse process xTs₁ + + return (Union (Data.HashMap.Strict.InsOrd.fromList xTs₀)) +decode_1_0 (TList [ TInt 12, TString x, t₁, TMap yTs₁ ]) = do + t₀ <- decode_1_0 t₁ + + let process (TString y, _T₁) = do + _T₀ <- decode_1_0 _T₁ + + return (y, _T₀) + process _ = + empty + + yTs₀ <- traverse process yTs₁ + + return (UnionLit x t₀ (Data.HashMap.Strict.InsOrd.fromList yTs₀)) +decode_1_0 (TList [ TInt 13, u₁ ]) = do + u₀ <- decode_1_0 u₁ + + return (Constructors u₀) +decode_1_0 (TBool b) = do + return (BoolLit b) +decode_1_0 (TList [ TInt 14, t₁, l₁, r₁ ]) = do + t₀ <- decode_1_0 t₁ + l₀ <- decode_1_0 l₁ + r₀ <- decode_1_0 r₁ + + return (BoolIf t₀ l₀ r₀) +decode_1_0 (TList [ TInt 15, TInt n ]) = do + return (NaturalLit (fromIntegral n)) +decode_1_0 (TList [ TInt 15, TInteger n ]) = do + return (NaturalLit (fromInteger n)) +decode_1_0 (TList [ TInt 16, TInt n ]) = do + return (IntegerLit (fromIntegral n)) +decode_1_0 (TList [ TInt 16, TInteger n ]) = do + return (IntegerLit n) +decode_1_0 (TList [ TInt 17, TTagged 4 (TList [ TInt exponent, TInteger mantissa ]) ]) = do + return (DoubleLit (Data.Scientific.scientific mantissa exponent)) +decode_1_0 (TList [ TInt 17, TTagged 4 (TList [ TInt exponent, TInt mantissa ]) ]) = do + return (DoubleLit (Data.Scientific.scientific (fromIntegral mantissa) exponent)) +decode_1_0 (TList (TInt 18 : xs)) = do + let process (TString x : y₁ : zs) = do + y₀ <- decode_1_0 y₁ + + ~(xys, z) <- process zs + + return ((x, y₀) : xys, z) + process [ TString z ] = do + return ([], z) + process _ = do + empty + + (xys, z) <- process xs + + return (TextLit (Chunks xys z)) +decode_1_0 (TList (TInt 24 : TInt n : xs)) = do + let remote scheme = do + let process [ TString file, q, f ] = do + query <- case q of + TNull -> return Nothing + TString x -> return (Just x) + _ -> empty + fragment <- case f of + TNull -> return Nothing + TString x -> return (Just x) + _ -> empty + return ([], file, query, fragment) + process (TString path : ys) = do + (paths, file, query, fragment) <- process ys + return (path : paths, file, query, fragment) + process _ = do + empty + + (authority, paths, file, query, fragment) <- case xs of + TString authority : ys -> do + (paths, file, query, fragment) <- process ys + return (authority, paths, file, query, fragment) + _ -> empty + + let components = reverse paths + let directory = Directory {..} + let path = File {..} + let headers = Nothing + + return (Remote (URL {..})) + + let local prefix = do + let process [ TString file ] = do + return ([], file) + process (TString path : ys) = do + (paths, file) <- process ys + return (path : paths, file) + process _ = + empty + + (paths, file) <- process xs + + let finalPaths = case n of + 4 -> ".." : paths + _ -> paths + + let components = reverse finalPaths + let directory = Directory {..} + + return (Local prefix (File {..})) + + let env = do + case xs of + [ TString x ] -> return (Env x) + _ -> empty + + let missing = return Missing + + importType <- case n of + 0 -> remote HTTP + 1 -> remote HTTPS + 2 -> local Absolute + 3 -> local Here + 4 -> local Here + 5 -> local Home + 6 -> env + 7 -> missing + _ -> empty + + let hash = Nothing + let importHashed = ImportHashed {..} + let importMode = Code + return (Embed (Import {..})) +decode_1_0 (TList [ TInt 25, TString x, a₁, b₁ ]) = do + a₀ <- decode_1_0 a₁ + b₀ <- decode_1_0 b₁ + return (Let x Nothing a₀ b₀) +decode_1_0 (TList [ TInt 25, TString x, _A₁, a₁, b₁ ]) = do + _A₀ <- decode_1_0 _A₁ + a₀ <- decode_1_0 a₁ + b₀ <- decode_1_0 b₁ + return (Let x (Just _A₀) a₀ b₀) +decode_1_0 (TList [ TInt 26, t₁, _T₁ ]) = do + t₀ <- decode_1_0 t₁ + _T₀ <- decode_1_0 _T₁ + return (Annot t₀ _T₀) +decode_1_0 _ = + empty + +-- | Encode a Dhall expression using protocol version @1.0@ +encodeWithVersion_1_0 :: Expr s Import -> Term +encodeWithVersion_1_0 expression = + TList [ TString "1.0", encode_1_0 expression ] + +{-| Decode a Dhall expression + + This auto-detects whiich protocol version to decode based on the included + protocol version string in the decoded expression +-} +decode :: Term -> Either DecodingFailure (Expr s Import) +decode term = do + (version, subTerm) <- case term of + TList [ TString version, subTerm ] -> + return (version, subTerm) + _ -> + fail ("Cannot decode the version from this decoded CBOR expression: " <> show term) + + maybeExpression <- case version of + "1.0" -> do + return (decode_1_0 subTerm) + _ -> do + fail ("This decoded version is not supported: " <> Data.Text.unpack version) + + case maybeExpression of + Nothing -> + fail ("This decoded CBOR expression does not represent a valid Dhall expression: " <> show subTerm) + Just expression -> + return expression + +-- | Encode a Dhall expression using the specified `ProtocolVersion` +encode :: ProtocolVersion -> Expr s Import -> Term +encode V_1_0 = encodeWithVersion_1_0 + +data DecodingFailure + = CannotDecodeProtocolVersionString Term + | UnsupportedProtocolVersionString Text + | CBORIsNotDhall Term + deriving (Eq) + +instance Exception DecodingFailure + +_ERROR :: String +_ERROR = "\ESC[1;31mError\ESC[0m" + +instance Show DecodingFailure where + show (CannotDecodeProtocolVersionString term) = + _ERROR <> ": Cannot decode version string\n" + <> "\n" + <> "This CBOR expression does not contain a protocol version string in any\n" + <> "recognizable format\n" + <> "\n" + <> "↳ " <> show term <> "\n" + show (UnsupportedProtocolVersionString version) = + _ERROR <> ": Unsupported version string\n" + <> "\n" + <> "The encoded Dhall expression was tagged with a protocol version string of:\n" + <> "\n" + <> "↳ " <> show version <> "\n" + <> "\n" + <> "... but this implementation cannot decode that protocol version\n" + <> "\n" + <> "Some common reasons why you might get this error:\n" + <> "\n" + <> "● You are using an old version of the interpreter and need to upgrade\n" + show (CBORIsNotDhall term) = + _ERROR <> ": Cannot decode CBOR to Dhall\n" + <> "\n" + <> "The following CBOR expression does not encode a valid Dhall expression\n" + <> "\n" + <> "↳ " <> show term <> "\n" diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -1,8 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} @@ -26,7 +25,9 @@ , ImportHashed(..) , ImportMode(..) , ImportType(..) + , URL(..) , Path + , Scheme(..) , Var(..) , Chunks(..) , Expr(..) @@ -63,6 +64,7 @@ import Data.Bifunctor (Bifunctor(..)) import Data.Data (Data) import Data.Foldable +import Data.Hashable (Hashable) import Data.HashMap.Strict.InsOrd (InsOrdHashMap) import Data.HashSet (HashSet) import Data.String (IsString(..)) @@ -74,13 +76,16 @@ import Data.Text.Prettyprint.Doc (Pretty) import Data.Traversable import {-# SOURCE #-} Dhall.Pretty.Internal +import GHC.Generics (Generic) import Numeric.Natural (Natural) import Prelude hiding (succ) import qualified Control.Monad import qualified Crypto.Hash +import qualified Data.List import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet +import qualified Data.Ord import qualified Data.Sequence import qualified Data.Set import qualified Data.Text @@ -103,7 +108,7 @@ Note that Dhall does not support functions from terms to types and therefore Dhall is not a dependently typed language -} -data Const = Type | Kind deriving (Show, Eq, Data, Bounded, Enum) +data Const = Type | Kind deriving (Show, Eq, Data, Bounded, Enum, Generic) instance Pretty Const where pretty = Pretty.unAnnotate . prettyConst @@ -115,7 +120,7 @@ @Directory { components = [ "baz", "bar", "foo" ] }@ -} newtype Directory = Directory { components :: [Text] } - deriving (Eq, Ord, Show) + deriving (Eq, Generic, Ord, Show) instance Semigroup Directory where Directory components₀ <> Directory components₁ = @@ -133,7 +138,7 @@ data File = File { directory :: Directory , file :: Text - } deriving (Eq, Ord, Show) + } deriving (Eq, Generic, Ord, Show) instance Pretty File where pretty (File {..}) = Pretty.pretty directory <> "/" <> Pretty.pretty file @@ -142,6 +147,7 @@ File directory₀ _ <> File directory₁ file = File (directory₀ <> directory₁) file +-- | The beginning of a file path which anchors subsequent path components data FilePrefix = Absolute -- ^ Absolute path @@ -149,29 +155,40 @@ -- ^ Path relative to @.@ | Home -- ^ Path relative to @~@ - deriving (Eq, Ord, Show) + deriving (Eq, Generic, Ord, Show) instance Pretty FilePrefix where pretty Absolute = "" pretty Here = "." pretty Home = "~" +data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show) + +data URL = URL + { scheme :: Scheme + , authority :: Text + , path :: File + , query :: Maybe Text + , fragment :: Maybe Text + , headers :: Maybe ImportHashed + } deriving (Eq, Generic, Ord, Show) + -- | The type of import (i.e. local vs. remote vs. environment) data ImportType = Local FilePrefix File -- ^ Local path - | URL Text File Text (Maybe ImportHashed) + | Remote URL -- ^ URL of remote resource and optional headers stored in an import | Env Text -- ^ Environment variable | Missing - deriving (Eq, Ord, Show) + deriving (Eq, Generic, Ord, Show) instance Semigroup ImportType where Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁) - URL prefix file₀ suffix headers <> Local Here file₁ = - URL prefix (file₀ <> file₁) suffix headers + Remote (URL { path = path₀, ..}) <> Local Here path₁ = + Remote (URL { path = path₀ <> path₁, ..}) _ <> import₁ = import₁ @@ -180,26 +197,41 @@ pretty (Local prefix file) = Pretty.pretty prefix <> Pretty.pretty file - pretty (URL prefix file suffix headers) = - Pretty.pretty prefix - <> Pretty.pretty file - <> Pretty.pretty suffix + pretty (Remote (URL {..})) = + schemeDoc + <> "://" + <> Pretty.pretty authority + <> Pretty.pretty path + <> queryDoc + <> fragmentDoc <> foldMap prettyHeaders headers where prettyHeaders h = " using " <> Pretty.pretty h + schemeDoc = case scheme of + HTTP -> "http" + HTTPS -> "https" + + queryDoc = case query of + Nothing -> "" + Just q -> "?" <> Pretty.pretty q + + fragmentDoc = case fragment of + Nothing -> "" + Just f -> "#" <> Pretty.pretty f + pretty (Env env) = "env:" <> Pretty.pretty env pretty Missing = "missing" -- | How to interpret the import's contents (i.e. as Dhall code or raw text) -data ImportMode = Code | RawText deriving (Eq, Ord, Show) +data ImportMode = Code | RawText deriving (Eq, Generic, Ord, Show) -- | A `ImportType` extended with an optional hash for semantic integrity checks data ImportHashed = ImportHashed { hash :: Maybe (Crypto.Hash.Digest SHA256) , importType :: ImportType - } deriving (Eq, Ord, Show) + } deriving (Eq, Generic, Ord, Show) instance Semigroup ImportHashed where ImportHashed _ importType₀ <> ImportHashed hash importType₁ = @@ -215,7 +247,7 @@ data Import = Import { importHashed :: ImportHashed , importMode :: ImportMode - } deriving (Eq, Ord, Show) + } deriving (Eq, Generic, Ord, Show) instance Semigroup Import where Import importHashed₀ _ <> Import importHashed₁ code = @@ -267,7 +299,7 @@ appear as a numeric suffix. -} data Var = V Text !Integer - deriving (Data, Eq, Show) + deriving (Data, Generic, Eq, Show) instance IsString Var where fromString str = V (fromString str) 0 @@ -409,7 +441,7 @@ | ImportAlt (Expr s a) (Expr s a) -- | > Embed import ~ import | Embed a - deriving (Functor, Foldable, Traversable, Show, Eq, Data) + deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Data) instance Applicative (Expr s) where pure = Embed @@ -555,7 +587,7 @@ -- | The body of an interpolated @Text@ literal data Chunks s a = Chunks [(Text, Expr s a)] Text - deriving (Functor, Foldable, Traversable, Show, Eq, Data) + deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Data) instance Data.Semigroup.Semigroup (Chunks s a) where Chunks xysL zL <> Chunks [] zR = @@ -962,62 +994,73 @@ -- and `subst` does nothing to a closed expression subst _ _ (Embed p) = Embed p -{-| α-normalize an expression by renaming all variables to @\"_\"@ and using - De Bruijn indices to distinguish them +{-| α-normalize an expression by renaming all bound variables to @\"_\"@ and + using De Bruijn indices to distinguish them + +>>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x")))) +Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1))))) + + α-normalization does not affect free variables: + +>>> alphaNormalize "x" +Var (V "x" 0) + -} alphaNormalize :: Expr s a -> Expr s a alphaNormalize (Const c) = Const c alphaNormalize (Var v) = Var v +alphaNormalize (Lam "_" _A₀ b₀) = + Lam "_" _A₁ b₁ + where + _A₁ = alphaNormalize _A₀ + b₁ = alphaNormalize b₀ alphaNormalize (Lam x _A₀ b₀) = - Lam "_" _A₁ b₃ + Lam "_" _A₁ b₄ where _A₁ = alphaNormalize _A₀ - v₀ = Var (V "_" 0) - v₁ = shift 1 (V x 0) v₀ - b₁ = subst (V x 0) v₁ b₀ - b₂ = shift (-1) (V x 0) b₁ - b₃ = alphaNormalize b₂ + b₁ = shift 1 (V "_" 0) b₀ + b₂ = subst (V x 0) (Var (V "_" 0)) b₁ + b₃ = shift (-1) (V x 0) b₂ + b₄ = alphaNormalize b₃ +alphaNormalize (Pi "_" _A₀ _B₀) = + Pi "_" _A₁ _B₁ + where + _A₁ = alphaNormalize _A₀ + _B₁ = alphaNormalize _B₀ alphaNormalize (Pi x _A₀ _B₀) = - Pi "_" _A₁ _B₃ + Pi "_" _A₁ _B₄ where _A₁ = alphaNormalize _A₀ - v₀ = Var (V "_" 0) - v₁ = shift 1 (V x 0) v₀ - _B₁ = subst (V x 0) v₁ _B₀ - _B₂ = shift (-1) (V x 0) _B₁ - _B₃ = alphaNormalize _B₂ + _B₁ = shift 1 (V "_" 0) _B₀ + _B₂ = subst (V x 0) (Var (V "_" 0)) _B₁ + _B₃ = shift (-1) (V x 0) _B₂ + _B₄ = alphaNormalize _B₃ alphaNormalize (App f₀ a₀) = App f₁ a₁ where f₁ = alphaNormalize f₀ a₁ = alphaNormalize a₀ -alphaNormalize (Let x (Just _A₀) a₀ b₀) = - Let "_" (Just _A₁) a₁ b₃ +alphaNormalize (Let "_" mA₀ a₀ b₀) = + Let "_" mA₁ a₁ b₁ where - _A₁ = alphaNormalize _A₀ - - a₁ = alphaNormalize a₀ - - v₀ = Var (V "_" 0) - v₁ = shift 1 (V x 0) v₀ - b₁ = subst (V x 0) v₁ b₀ - b₂ = shift (-1) (V x 0) b₁ - b₃ = alphaNormalize b₂ -alphaNormalize (Let x Nothing a₀ b₀) = - Let "_" Nothing a₁ b₃ + mA₁ = fmap alphaNormalize mA₀ + a₁ = alphaNormalize a₀ + b₁ = alphaNormalize b₀ +alphaNormalize (Let x mA₀ a₀ b₀) = + Let "_" mA₁ a₁ b₄ where - a₁ = alphaNormalize a₀ + mA₁ = fmap alphaNormalize mA₀ + a₁ = alphaNormalize a₀ - v₀ = Var (V "_" 0) - v₁ = shift 1 (V x 0) v₀ - b₁ = subst (V x 0) v₁ b₀ - b₂ = shift (-1) (V x 0) b₁ - b₃ = alphaNormalize b₂ + b₁ = shift 1 (V "_" 0) b₀ + b₂ = subst (V x 0) (Var (V "_" 0)) b₁ + b₃ = shift (-1) (V x 0) b₂ + b₄ = alphaNormalize b₃ alphaNormalize (Annot t₀ _T₀) = Annot t₁ _T₁ where @@ -1331,6 +1374,12 @@ denote (ImportAlt a b ) = ImportAlt (denote a) (denote b) denote (Embed a ) = Embed a +sortMap :: (Ord k, Hashable k) => InsOrdHashMap k v -> InsOrdHashMap k v +sortMap = + Data.HashMap.Strict.InsOrd.fromList + . Data.List.sortBy (Data.Ord.comparing fst) + . Data.HashMap.Strict.InsOrd.toList + {-| Reduce an expression to its normal form, performing beta reduction and applying any custom definitions. @@ -1606,16 +1655,16 @@ es' = fmap loop es OptionalFold -> OptionalFold OptionalBuild -> OptionalBuild - Record kts -> Record kts' + Record kts -> Record (sortMap kts') where kts' = fmap loop kts - RecordLit kvs -> RecordLit kvs' + RecordLit kvs -> RecordLit (sortMap kvs') where kvs' = fmap loop kvs - Union kts -> Union kts' + Union kts -> Union (sortMap kts') where kts' = fmap loop kts - UnionLit k v kvs -> UnionLit k v' kvs' + UnionLit k v kvs -> UnionLit k v' (sortMap kvs') where v' = loop v kvs' = fmap loop kvs @@ -1729,7 +1778,7 @@ -- | Quickly check if an expression is in normal form -isNormalized :: Expr s a -> Bool +isNormalized :: Eq a => Expr s a -> Bool isNormalized e = case denote e of Const _ -> True Var _ -> True @@ -1773,37 +1822,32 @@ Annot _ _ -> False Bool -> True BoolLit _ -> True - BoolAnd x y -> isNormalized x && isNormalized y && - case x of - BoolLit _ -> - case y of - BoolLit _ -> False - _ -> True - _ -> True - BoolOr x y -> isNormalized x && isNormalized y && - case x of - BoolLit _ -> - case y of - BoolLit _ -> False - _ -> True - _ -> True - BoolEQ x y -> isNormalized x && isNormalized y && - case x of - BoolLit _ -> - case y of - BoolLit _ -> False - _ -> True - _ -> True - BoolNE x y -> isNormalized x && isNormalized y && - case x of - BoolLit _ -> - case y of - BoolLit _ -> False - _ -> True - _ -> True - BoolIf b true false -> isNormalized b && case b of - BoolLit _ -> False - _ -> isNormalized true && isNormalized false + BoolAnd x y -> isNormalized x && isNormalized y && decide x y + where + decide (BoolLit _) _ = False + decide _ (BoolLit _) = False + decide l r = not (judgmentallyEqual l r) + BoolOr x y -> isNormalized x && isNormalized y && decide x y + where + decide (BoolLit _) _ = False + decide _ (BoolLit _) = False + decide l r = not (judgmentallyEqual l r) + BoolEQ x y -> isNormalized x && isNormalized y && decide x y + where + decide (BoolLit True) _ = False + decide _ (BoolLit True) = False + decide l r = not (judgmentallyEqual l r) + BoolNE x y -> isNormalized x && isNormalized y && decide x y + where + decide (BoolLit False) _ = False + decide _ (BoolLit False ) = False + decide l r = not (judgmentallyEqual l r) + BoolIf x y z -> + isNormalized x && isNormalized y && isNormalized z && decide x y z + where + decide (BoolLit _) _ _ = False + decide _ (BoolLit True) (BoolLit False) = False + decide _ l r = not (judgmentallyEqual l r) Natural -> True NaturalLit _ -> True NaturalFold -> True @@ -1813,20 +1857,20 @@ NaturalOdd -> True NaturalShow -> True NaturalToInteger -> True - NaturalPlus x y -> isNormalized x && isNormalized y && - case x of - NaturalLit _ -> - case y of - NaturalLit _ -> False - _ -> True - _ -> True - NaturalTimes x y -> isNormalized x && isNormalized y && - case x of - NaturalLit _ -> - case y of - NaturalLit _ -> False - _ -> True - _ -> True + NaturalPlus x y -> isNormalized x && isNormalized y && decide x y + where + decide (NaturalLit 0) _ = False + decide _ (NaturalLit 0) = False + decide (NaturalLit _) (NaturalLit _) = False + decide _ _ = True + NaturalTimes x y -> isNormalized x && isNormalized y && decide x y + where + decide (NaturalLit 0) _ = False + decide _ (NaturalLit 0) = False + decide (NaturalLit 1) _ = False + decide _ (NaturalLit 1) = False + decide (NaturalLit _) (NaturalLit _) = False + decide _ _ = True Integer -> True IntegerLit _ -> True IntegerShow -> True @@ -1835,23 +1879,29 @@ DoubleLit _ -> True DoubleShow -> True Text -> True - TextLit (Chunks xys _) -> all (all isNormalized) xys - TextAppend x y -> isNormalized x && isNormalized y && - case x of - TextLit _ -> - case y of - TextLit _ -> False - _ -> True - _ -> True + TextLit (Chunks [("", _)] "") -> False + TextLit (Chunks xys _) -> all (all check) xys + where + check y = isNormalized y && case y of + TextLit _ -> False + _ -> True + TextAppend x y -> isNormalized x && isNormalized y && decide x y + where + isEmpty (Chunks [] "") = True + isEmpty _ = False + + decide (TextLit m) _ | isEmpty m = False + decide _ (TextLit n) | isEmpty n = False + decide (TextLit _) (TextLit _) = False + decide _ _ = True List -> True ListLit t es -> all isNormalized t && all isNormalized es - ListAppend x y -> isNormalized x && isNormalized y && - case x of - ListLit _ _ -> - case y of - ListLit _ _ -> False - _ -> True - _ -> True + ListAppend x y -> isNormalized x && isNormalized y && decide x y + where + decide (ListLit _ m) _ | Data.Sequence.null m = False + decide _ (ListLit _ n) | Data.Sequence.null n = False + decide (ListLit _ _) (ListLit _ _) = False + decide _ _ = True ListBuild -> True ListFold -> True ListLength -> True @@ -1867,28 +1917,25 @@ RecordLit kvs -> all isNormalized kvs Union kts -> all isNormalized kts UnionLit _ v kvs -> isNormalized v && all isNormalized kvs - Combine x y -> isNormalized x && isNormalized y && combine + Combine x y -> isNormalized x && isNormalized y && decide x y where - combine = case x of - RecordLit _ -> case y of - RecordLit _ -> False - _ -> True - _ -> True - CombineTypes x y -> isNormalized x && isNormalized y && combine + decide (RecordLit m) _ | Data.HashMap.Strict.InsOrd.null m = False + decide _ (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = False + decide (RecordLit _) (RecordLit _) = False + decide _ _ = True + CombineTypes x y -> isNormalized x && isNormalized y && decide x y where - combine = case x of - Record _ -> case y of - Record _ -> False - _ -> True - _ -> True - Prefer x y -> isNormalized x && isNormalized y && combine + decide (Record m) _ | Data.HashMap.Strict.InsOrd.null m = False + decide _ (Record n) | Data.HashMap.Strict.InsOrd.null n = False + decide (Record _) (Record _) = False + decide _ _ = True + Prefer x y -> isNormalized x && isNormalized y && decide x y where - combine = case x of - RecordLit _ -> case y of - RecordLit _ -> False - _ -> True - _ -> True - Merge x y t -> isNormalized x && isNormalized y && any isNormalized t && + decide (RecordLit m) _ | Data.HashMap.Strict.InsOrd.null m = False + decide _ (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = False + decide (RecordLit _) (RecordLit _) = False + decide _ _ = True + Merge x y t -> isNormalized x && isNormalized y && all isNormalized t && case x of RecordLit kvsX -> case y of @@ -2007,3 +2054,4 @@ , "Optional/build" , "Optional/fold" ] + diff --git a/src/Dhall/Diff.hs b/src/Dhall/Diff.hs --- a/src/Dhall/Diff.hs +++ b/src/Dhall/Diff.hs @@ -453,14 +453,7 @@ <> " " <> ignore skeleton (Pi {}) = - forall - <> lparen - <> ignore - <> " " - <> colon - <> " " - <> ignore - <> rparen + ignore <> " " <> rarrow <> " " @@ -723,13 +716,20 @@ docs (Pi aL bL cL) (Pi aR bR cR) = Data.List.NonEmpty.cons (align doc) (docs cL cR) where - doc = forall + doc | same docA && same docB = ignore + | otherwise = + forall <> lparen - <> format " " (diffLabel aL aR) + <> format " " docA <> colon <> " " - <> format mempty (diffExpression bL bR) + <> format mempty docB <> rparen + where + docA = diffLabel aL aR + + docB = diffExpression bL bR + docs aL aR = pure (diffExpression aL aR) diffExpression l@(Pi {}) r = mismatch l r diff --git a/src/Dhall/Format.hs b/src/Dhall/Format.hs --- a/src/Dhall/Format.hs +++ b/src/Dhall/Format.hs @@ -1,7 +1,12 @@ {-# LANGUAGE OverloadedStrings #-} -module Dhall.Format ( format ) where +-- | This module contains the implementation of the @dhall format@ subcommand +module Dhall.Format + ( -- * Format + format + ) where + import Dhall.Parser (exprAndHeaderFromText) import Dhall.Pretty (annToAnsiStyle, prettyExpr, layoutOpts) @@ -14,7 +19,12 @@ import qualified System.Console.ANSI import qualified System.IO -format :: Maybe FilePath -> IO () +-- | Implementation of the @dhall format@ subcommand +format + :: Maybe FilePath + -- ^ Modify file in-place if present, otherwise read from @stdin@ and write + -- to @stdout@ + -> IO () format inplace = do case inplace of Just file -> do diff --git a/src/Dhall/Freeze.hs b/src/Dhall/Freeze.hs --- a/src/Dhall/Freeze.hs +++ b/src/Dhall/Freeze.hs @@ -1,34 +1,57 @@ {-# LANGUAGE OverloadedStrings #-} -module Dhall.Freeze ( +-- | This module contains the implementation of the @dhall freeze@ subcommand + +module Dhall.Freeze + ( -- * Freeze freeze , hashImport ) where -import Dhall.Core -import Dhall.Import (load, hashExpression) -import Dhall.Parser (exprAndHeaderFromText, Src) -import Dhall.Pretty (annToAnsiStyle, layoutOpts) - -import System.Console.ANSI (hSupportsANSI) import Data.Monoid ((<>)) import Data.Maybe (fromMaybe) import Data.Text +import Dhall.Binary (ProtocolVersion(..)) +import Dhall.Core (Expr(..), Import(..), ImportHashed(..)) +import Dhall.Import (hashExpression, protocolVersion) +import Dhall.Parser (exprAndHeaderFromText, Src) +import Dhall.Pretty (annToAnsiStyle, layoutOpts) +import Lens.Family (set) +import System.Console.ANSI (hSupportsANSI) +import qualified Control.Exception +import qualified Control.Monad.Trans.State.Strict as State import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty -import qualified Control.Exception import qualified Data.Text.IO +import qualified Dhall.Core +import qualified Dhall.Import +import qualified Dhall.TypeCheck import qualified System.IO readInput :: Maybe FilePath -> IO Text readInput = maybe Data.Text.IO.getContents Data.Text.IO.readFile -hashImport :: Import -> IO Import -hashImport import_ = do - expression <- Dhall.Import.load (Embed import_) - let expressionHash = Just (Dhall.Import.hashExpression expression) +-- | Retrieve an `Import` and update the hash to match the latest contents +hashImport :: ProtocolVersion -> Import -> IO Import +hashImport _protocolVersion import_ = do + let status = + set protocolVersion _protocolVersion (Dhall.Import.emptyStatus ".") + + expression <- State.evalStateT (Dhall.Import.loadWith (Embed import_)) status + + case Dhall.TypeCheck.typeOf expression of + Left exception -> Control.Exception.throwIO exception + Right _ -> return () + + let normalizedExpression = + Dhall.Core.alphaNormalize (Dhall.Core.normalize expression) + + let expressionHash = + Just (Dhall.Import.hashExpression _protocolVersion normalizedExpression) + let newImportHashed = (importHashed import_) { hash = expressionHash } + return $ import_ { importHashed = newImportHashed } parseExpr :: String -> Text -> IO (Text, Expr Src Import) @@ -37,11 +60,6 @@ Left err -> Control.Exception.throwIO err Right x -> return x -freezeExpr :: (Text, Expr s Import) -> IO (Text, Expr s Import) -freezeExpr (t, e) = do - e' <- traverse hashImport e - return (t, e') - writeExpr :: Maybe FilePath -> (Text, Expr s Import) -> IO () writeExpr inplace (header, expr) = do let doc = Pretty.pretty header <> Pretty.pretty expr @@ -60,9 +78,17 @@ else Pretty.renderIO System.IO.stdout (Pretty.layoutSmart layoutOpts (Pretty.unAnnotate doc)) -freeze :: Maybe FilePath -> IO () -freeze inplace = do - expr <- readInput inplace - parseExpr srcInfo expr >>= freezeExpr >>= writeExpr inplace +-- | Implementation of the @dhall freeze@ subcommand +freeze + :: Maybe FilePath + -- ^ Modify file in-place if present, otherwise read from @stdin@ and write + -- to @stdout@ + -> ProtocolVersion + -> IO () +freeze inplace _protocolVersion = do + text <- readInput inplace + (header, parsedExpression) <- parseExpr srcInfo text + frozenExpression <- traverse (hashImport _protocolVersion) parsedExpression + writeExpr inplace (header, frozenExpression) where srcInfo = fromMaybe "(stdin)" inplace diff --git a/src/Dhall/Hash.hs b/src/Dhall/Hash.hs --- a/src/Dhall/Hash.hs +++ b/src/Dhall/Hash.hs @@ -1,26 +1,44 @@ {-# LANGUAGE OverloadedStrings #-} -module Dhall.Hash ( hash ) where +-- | This module contains the implementation of the @dhall hash@ subcommand +module Dhall.Hash + ( -- * Hash + hash + ) where + +import Dhall.Binary (ProtocolVersion) import Dhall.Parser (exprFromText) -import Dhall.Import (hashExpressionToCode, load) +import Dhall.Import (hashExpressionToCode, protocolVersion) +import Lens.Family (set) +import qualified Control.Monad.Trans.State.Strict as State import qualified Control.Exception +import qualified Dhall.Core +import qualified Dhall.Import import qualified Dhall.TypeCheck import qualified Data.Text.IO -hash :: IO () -hash = do - inText <- Data.Text.IO.getContents +-- | Implementation of the @dhall hash@ subcommand +hash :: ProtocolVersion -> IO () +hash _protocolVersion = do + inText <- Data.Text.IO.getContents - expr <- case exprFromText "(stdin)" inText of - Left err -> Control.Exception.throwIO err - Right expr -> return expr + parsedExpression <- case exprFromText "(stdin)" inText of + Left exception -> Control.Exception.throwIO exception + Right parsedExpression -> return parsedExpression - expr' <- load expr + let status = + set protocolVersion _protocolVersion (Dhall.Import.emptyStatus ".") - _ <- case Dhall.TypeCheck.typeOf expr' of - Left err -> Control.Exception.throwIO err - Right _ -> return () + resolvedExpression <- State.evalStateT (Dhall.Import.loadWith parsedExpression) status - Data.Text.IO.putStrLn (hashExpressionToCode expr') + case Dhall.TypeCheck.typeOf resolvedExpression of + Left exception -> Control.Exception.throwIO exception + Right _ -> return () + + let normalizedExpression = + Dhall.Core.alphaNormalize (Dhall.Core.normalize resolvedExpression) + + Data.Text.IO.putStrLn + (hashExpressionToCode _protocolVersion normalizedExpression) diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -102,12 +102,17 @@ exprFromImport , load , loadWith - , loadDirWith - , loadWithContext , hashExpression , hashExpressionToCode - , Status(..) + , Status , emptyStatus + , stack + , cache + , manager + , protocolVersion + , normalizer + , startingContext + , resolver , Cycle(..) , ReferentiallyOpaque(..) , Imported(..) @@ -117,8 +122,11 @@ , MissingImports(..) ) where +import Control.Applicative (Alternative(..)) +import Codec.CBOR.Term (Term) import Control.Applicative (empty) import Control.Exception (Exception, SomeException, throwIO, toException) +import Control.Monad (guard) import Control.Monad.Catch (throwM, MonadCatch(catch), catches, Handler(..)) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) @@ -133,6 +141,7 @@ #endif import Data.Typeable (Typeable) import System.FilePath (()) +import Dhall.Binary (ProtocolVersion(..)) import Dhall.Core ( Expr(..) , Chunks(..) @@ -143,6 +152,9 @@ , ImportType(..) , ImportMode(..) , Import(..) + , ReifiedNormalizer(..) + , Scheme(..) + , URL(..) ) #ifdef MIN_VERSION_http_client import Dhall.Import.HTTP @@ -153,25 +165,28 @@ import Dhall.TypeCheck (X(..)) import Lens.Family.State.Strict (zoom) -import qualified Control.Monad.Trans.State.Strict as State +import qualified Codec.Serialise +import qualified Control.Monad.Trans.Maybe as Maybe +import qualified Control.Monad.Trans.State.Strict as State import qualified Crypto.Hash import qualified Data.ByteString +import qualified Data.ByteString.Lazy import qualified Data.CaseInsensitive import qualified Data.Foldable - import qualified Data.HashMap.Strict.InsOrd -import qualified Data.List.NonEmpty as NonEmpty -import qualified Data.Map.Strict as Map +import qualified Data.List.NonEmpty as NonEmpty +import qualified Data.Map.Strict as Map import qualified Data.Text.Encoding -import qualified Data.Text as Text +import qualified Data.Text as Text import qualified Data.Text.IO +import qualified Dhall.Binary import qualified Dhall.Core import qualified Dhall.Parser -import qualified Dhall.Context import qualified Dhall.Pretty.Internal import qualified Dhall.TypeCheck import qualified System.Environment -import qualified System.Directory +import qualified System.Directory as Directory +import qualified System.FilePath as FilePath import qualified Text.Megaparsec import qualified Text.Parser.Combinators import qualified Text.Parser.Token @@ -355,8 +370,8 @@ canonicalize (Local prefix file) = Local prefix (canonicalize file) - canonicalize (URL prefix file suffix header) = - URL prefix (canonicalize file) suffix header + canonicalize (Remote (URL {..})) = + Remote (URL { path = canonicalize path, ..}) canonicalize (Env name) = Env name @@ -420,23 +435,153 @@ <> "↳ " <> show actualHash <> "\n" -- | Parse an expression from a `Import` containing a Dhall program -exprFromImport :: Import -> StateT Status IO (Expr Src Import) -exprFromImport (Import {..}) = do +exprFromImport :: Import -> StateT (Status IO) IO (Expr Src Import) +exprFromImport import_@(Import {..}) = do let ImportHashed {..} = importHashed + case hash of + Nothing -> do + exprFromUncachedImport import_ + + Just expectedHash -> do + Status {..} <- State.get + + result <- Maybe.runMaybeT (getCacheFile expectedHash) + + case result of + Just (Read, cacheFile) -> do + bytesStrict <- liftIO (Data.ByteString.readFile cacheFile) + + let actualHash = Crypto.Hash.hash bytesStrict + + if expectedHash == actualHash + then return () + else liftIO (Control.Exception.throwIO (HashMismatch {..})) + + let bytesLazy = Data.ByteString.Lazy.fromStrict bytesStrict + + term <- case Codec.Serialise.deserialiseOrFail bytesLazy of + Left exception -> + liftIO (Control.Exception.throwIO exception) + + Right term -> + return term + + case Dhall.Binary.decode term of + Left exception -> + liftIO (Control.Exception.throwIO exception) + + Right expression -> + return expression + + Just (Write, cacheFile) -> do + expression <- exprFromUncachedImport import_ + + let _stack' = NonEmpty.cons import_ _stack + zoom stack (State.put _stack') + resolvedExpression <- loadWith expression + zoom stack (State.put _stack) + + case Dhall.TypeCheck.typeWith _startingContext resolvedExpression of + Left _ -> do + return () + + Right _ -> do + let normalizedExpression = + Dhall.Core.alphaNormalize + (Dhall.Core.normalizeWith + (getReifiedNormalizer _normalizer) + resolvedExpression + ) + + let bytes = + encodeExpression _protocolVersion normalizedExpression + + let actualHash = Crypto.Hash.hash bytes + + if expectedHash == actualHash + then return () + else liftIO (Control.Exception.throwIO (HashMismatch {..})) + + liftIO (Data.ByteString.writeFile cacheFile bytes) + + return expression + + Nothing -> do + exprFromUncachedImport import_ + +data CacheMode = Read | Write + +getCacheFile + :: (Alternative m, MonadIO m) + => Crypto.Hash.Digest SHA256 -> m (CacheMode, FilePath) +getCacheFile hash = do + let assertDirectory directory = do + let private = transform Directory.emptyPermissions + where + transform = + Directory.setOwnerReadable True + . Directory.setOwnerWritable True + . Directory.setOwnerSearchable True + + let accessible path = + Directory.readable path + && Directory.writable path + && Directory.searchable path + + directoryExists <- liftIO (Directory.doesDirectoryExist directory) + + if directoryExists + then do + permissions <- liftIO (Directory.getPermissions directory) + + guard (accessible permissions) + + else do + assertDirectory (FilePath.takeDirectory directory) + + liftIO (Directory.createDirectory directory) + + liftIO (Directory.setPermissions directory private) + + cacheDirectory <- liftIO $ Directory.getXdgDirectory Directory.XdgCache "" + + assertDirectory cacheDirectory + + let dhallDirectory = cacheDirectory "dhall" + + assertDirectory dhallDirectory + + let cacheFile = dhallDirectory show hash + + cacheFileExists <- liftIO (Directory.doesPathExist cacheFile) + + if cacheFileExists + then do + True <- liftIO (Directory.doesFileExist cacheFile) + + return (Read, cacheFile) + + else do + return (Write, cacheFile) + +exprFromUncachedImport :: Import -> StateT (Status IO) IO (Expr Src Import) +exprFromUncachedImport (Import {..}) = do + let ImportHashed {..} = importHashed + (path, text) <- case importType of Local prefix (File {..}) -> liftIO $ do let Directory {..} = directory prefixPath <- case prefix of Home -> do - System.Directory.getHomeDirectory + Directory.getHomeDirectory Absolute -> do return "/" Here -> do - System.Directory.getCurrentDirectory + Directory.getCurrentDirectory let cs = map Text.unpack (file : components) @@ -444,7 +589,7 @@ let path = foldr cons prefixPath cs - exists <- System.Directory.doesFileExist path + exists <- Directory.doesFileExist path if exists then return () @@ -454,18 +599,23 @@ return (path, text) - URL prefix file suffix maybeHeaders -> do + Remote (URL scheme authority file query fragment maybeHeaders) -> do + let prefix = + (case scheme of HTTP -> "http"; HTTPS -> "https") + <> "://" + <> authority + let fileText = Dhall.Pretty.Internal.prettyToStrictText file + + let suffix = + (case query of Nothing -> ""; Just q -> "?" <> q) + <> (case fragment of Nothing -> ""; Just f -> "#" <> f) let url = Text.unpack (prefix <> fileText <> suffix) mheaders <- case maybeHeaders of Nothing -> return Nothing Just importHashed_ -> do - expr <- loadStaticWith - exprFromImport - Dhall.Context.empty - (const Nothing) - (Embed (Import importHashed_ Code)) + expr <- loadWith (Embed (Import importHashed_ Code)) let expected :: Expr Src X expected = @@ -528,63 +678,23 @@ RawText -> do return (TextLit (Chunks [] text)) --- | Resolve all imports within an expression using a custom typing --- context and `Import`-resolving callback in arbitrary `MonadCatch` --- monad. --- --- This resolves imports relative to @.@ (the current working directory). -loadWith - :: MonadCatch m - => (Import -> StateT Status m (Expr Src Import)) - -> Dhall.Context.Context (Expr Src X) - -> Dhall.Core.Normalizer X - -> Expr Src Import - -> m (Expr Src X) -loadWith from_import ctx n expr = - loadDirWith "." from_import ctx n expr - --- | Resolve all imports within an expression using a custom typing --- context and `Import`-resolving callback in arbitrary `MonadCatch` --- monad, relative to a given directory. --- --- @since 1.16 -loadDirWith - :: MonadCatch m - => FilePath - -> (Import -> StateT Status m (Expr Src Import)) - -> Dhall.Context.Context (Expr Src X) - -> Dhall.Core.Normalizer X - -> Expr Src Import - -> m (Expr Src X) -loadDirWith dir from_import ctx n expr = do - State.evalStateT (loadStaticWith from_import ctx n expr) (emptyStatus dir) - --- | Resolve all imports within an expression, relative to @.@ (the --- current working directory), using a custom typing context. --- --- @load = loadWithContext Dhall.Context.empty@ -loadWithContext - :: Dhall.Context.Context (Expr Src X) - -> Dhall.Core.Normalizer X - -> Expr Src Import - -> IO (Expr Src X) -loadWithContext ctx n expr = - loadDirWith "." exprFromImport ctx n expr +-- | Default starting `Status`, importing relative to the given directory. +emptyStatus :: FilePath -> Status IO +emptyStatus = emptyStatusWith exprFromImport +{-| Generalized version of `load` --- | This loads a \"static\" expression (i.e. an expression free of imports) -loadStaticWith - :: MonadCatch m - => (Import -> StateT Status m (Expr Src Import)) - -> Dhall.Context.Context (Expr Src X) - -> Dhall.Core.Normalizer X - -> Expr Src Import - -> StateT Status m (Expr Src X) -loadStaticWith from_import ctx n expr₀ = case expr₀ of + You can configure the desired behavior through the initial `Status` that you + supply +-} +loadWith :: MonadCatch m => Expr Src Import -> StateT (Status m) m (Expr Src X) +loadWith expr₀ = case expr₀ of Embed import_ -> do - imports <- zoom stack State.get + Status {..} <- State.get - let local (Import (ImportHashed _ (URL {})) _) = False + let imports = _stack + + let local (Import (ImportHashed _ (Remote {})) _) = False local (Import (ImportHashed _ (Local {})) _) = True local (Import (ImportHashed _ (Env {})) _) = True local (Import (ImportHashed _ (Missing {})) _) = True @@ -600,8 +710,7 @@ expr <- if here `elem` canonicalizeAll imports then throwMissingImport (Imported imports (Cycle import_)) else do - m <- zoom cache State.get - case Map.lookup here m of + case Map.lookup here _cache of Just expr -> return expr Nothing -> do -- Here we have to match and unwrap the @MissingImports@ @@ -614,7 +723,7 @@ let handler₀ :: (MonadCatch m) => MissingImports - -> StateT Status m (Expr Src Import) + -> StateT (Status m) m (Expr Src Import) handler₀ e@(MissingImports []) = throwM e handler₀ (MissingImports [e]) = throwMissingImport (Imported imports' e) @@ -626,19 +735,18 @@ handler₁ :: (MonadCatch m) => SomeException - -> StateT Status m (Expr Src Import) + -> StateT (Status m) m (Expr Src Import) handler₁ e = throwMissingImport (Imported imports' e) -- This loads a \"dynamic\" expression (i.e. an expression -- that might still contain imports) - let loadDynamic = - from_import here + let loadDynamic = _resolver here expr' <- loadDynamic `catches` [ Handler handler₀, Handler handler₁ ] zoom stack (State.put imports') - expr'' <- loadStaticWith from_import ctx n expr' + expr'' <- loadWith expr' zoom stack (State.put imports) -- Type-check expressions here for three separate reasons: @@ -651,43 +759,45 @@ -- -- There is no need to check expressions that have been -- cached, since they have already been checked - expr''' <- case Dhall.TypeCheck.typeWith ctx expr'' of + expr''' <- case Dhall.TypeCheck.typeWith _startingContext expr'' of Left err -> throwM (Imported imports' err) - Right _ -> return (Dhall.Core.normalizeWith n expr'') - zoom cache (State.put $! Map.insert here expr''' m) + Right _ -> return (Dhall.Core.normalizeWith (getReifiedNormalizer _normalizer) expr'') + zoom cache (State.put $! Map.insert here expr''' _cache) return expr''' case hash (importHashed import_) of Nothing -> do return () Just expectedHash -> do - let actualHash = hashExpression expr + let actualHash = + hashExpression _protocolVersion (Dhall.Core.alphaNormalize expr) + if expectedHash == actualHash then return () else throwMissingImport (Imported imports' (HashMismatch {..})) return expr - ImportAlt a b -> loop a `catch` handler₀ + ImportAlt a b -> loadWith a `catch` handler₀ where handler₀ (MissingImports es₀) = - loop b `catch` handler₁ + loadWith b `catch` handler₁ where handler₁ (MissingImports es₁) = throwM (MissingImports (es₀ ++ es₁)) Const a -> pure (Const a) Var a -> pure (Var a) - Lam a b c -> Lam <$> pure a <*> loop b <*> loop c - Pi a b c -> Pi <$> pure a <*> loop b <*> loop c - App a b -> App <$> loop a <*> loop b - Let a b c d -> Let <$> pure a <*> mapM loop b <*> loop c <*> loop d - Annot a b -> Annot <$> loop a <*> loop b + Lam a b c -> Lam <$> pure a <*> loadWith b <*> loadWith c + Pi a b c -> Pi <$> pure a <*> loadWith b <*> loadWith c + App a b -> App <$> loadWith a <*> loadWith b + Let a b c d -> Let <$> pure a <*> mapM loadWith b <*> loadWith c <*> loadWith d + Annot a b -> Annot <$> loadWith a <*> loadWith b Bool -> pure Bool BoolLit a -> pure (BoolLit a) - BoolAnd a b -> BoolAnd <$> loop a <*> loop b - BoolOr a b -> BoolOr <$> loop a <*> loop b - BoolEQ a b -> BoolEQ <$> loop a <*> loop b - BoolNE a b -> BoolNE <$> loop a <*> loop b - BoolIf a b c -> BoolIf <$> loop a <*> loop b <*> loop c + BoolAnd a b -> BoolAnd <$> loadWith a <*> loadWith b + BoolOr a b -> BoolOr <$> loadWith a <*> loadWith b + BoolEQ a b -> BoolEQ <$> loadWith a <*> loadWith b + BoolNE a b -> BoolNE <$> loadWith a <*> loadWith b + BoolIf a b c -> BoolIf <$> loadWith a <*> loadWith b <*> loadWith c Natural -> pure Natural NaturalLit a -> pure (NaturalLit a) NaturalFold -> pure NaturalFold @@ -697,8 +807,8 @@ NaturalOdd -> pure NaturalOdd NaturalToInteger -> pure NaturalToInteger NaturalShow -> pure NaturalShow - NaturalPlus a b -> NaturalPlus <$> loop a <*> loop b - NaturalTimes a b -> NaturalTimes <$> loop a <*> loop b + NaturalPlus a b -> NaturalPlus <$> loadWith a <*> loadWith b + NaturalTimes a b -> NaturalTimes <$> loadWith a <*> loadWith b Integer -> pure Integer IntegerLit a -> pure (IntegerLit a) IntegerShow -> pure IntegerShow @@ -707,11 +817,11 @@ DoubleLit a -> pure (DoubleLit a) DoubleShow -> pure DoubleShow Text -> pure Text - TextLit (Chunks a b) -> fmap TextLit (Chunks <$> mapM (mapM loop) a <*> pure b) - TextAppend a b -> TextAppend <$> loop a <*> loop b + TextLit (Chunks a b) -> fmap TextLit (Chunks <$> mapM (mapM loadWith) a <*> pure b) + TextAppend a b -> TextAppend <$> loadWith a <*> loadWith b List -> pure List - ListLit a b -> ListLit <$> mapM loop a <*> mapM loop b - ListAppend a b -> ListAppend <$> loop a <*> loop b + ListLit a b -> ListLit <$> mapM loadWith a <*> mapM loadWith b + ListAppend a b -> ListAppend <$> loadWith a <*> loadWith b ListBuild -> pure ListBuild ListFold -> pure ListFold ListLength -> pure ListLength @@ -720,41 +830,51 @@ ListIndexed -> pure ListIndexed ListReverse -> pure ListReverse Optional -> pure Optional - OptionalLit a b -> OptionalLit <$> loop a <*> mapM loop b + OptionalLit a b -> OptionalLit <$> loadWith a <*> mapM loadWith b OptionalFold -> pure OptionalFold OptionalBuild -> pure OptionalBuild - Record a -> Record <$> mapM loop a - RecordLit a -> RecordLit <$> mapM loop a - Union a -> Union <$> mapM loop a - UnionLit a b c -> UnionLit <$> pure a <*> loop b <*> mapM loop c - Combine a b -> Combine <$> loop a <*> loop b - CombineTypes a b -> CombineTypes <$> loop a <*> loop b - Prefer a b -> Prefer <$> loop a <*> loop b - Merge a b c -> Merge <$> loop a <*> loop b <*> mapM loop c - Constructors a -> Constructors <$> loop a - Field a b -> Field <$> loop a <*> pure b - Project a b -> Project <$> loop a <*> pure b - Note a b -> Note <$> pure a <*> loop b - where - loop = loadStaticWith from_import ctx n - + Record a -> Record <$> mapM loadWith a + RecordLit a -> RecordLit <$> mapM loadWith a + Union a -> Union <$> mapM loadWith a + UnionLit a b c -> UnionLit <$> pure a <*> loadWith b <*> mapM loadWith c + Combine a b -> Combine <$> loadWith a <*> loadWith b + CombineTypes a b -> CombineTypes <$> loadWith a <*> loadWith b + Prefer a b -> Prefer <$> loadWith a <*> loadWith b + Merge a b c -> Merge <$> loadWith a <*> loadWith b <*> mapM loadWith c + Constructors a -> Constructors <$> loadWith a + Field a b -> Field <$> loadWith a <*> pure b + Project a b -> Project <$> loadWith a <*> pure b + Note a b -> Note <$> pure a <*> loadWith b -- | Resolve all imports within an expression load :: Expr Src Import -> IO (Expr Src X) -load = loadWithContext Dhall.Context.empty (const Nothing) +load expression = State.evalStateT (loadWith expression) (emptyStatus ".") --- | Hash a fully resolved expression -hashExpression :: Expr s X -> (Crypto.Hash.Digest SHA256) -hashExpression expr = Crypto.Hash.hash actualBytes +encodeExpression + :: forall s . ProtocolVersion -> Expr s X -> Data.ByteString.ByteString +encodeExpression _protocolVersion expression = bytesStrict where - text = Dhall.Core.pretty (Dhall.Core.normalize expr) - actualBytes = Data.Text.Encoding.encodeUtf8 text + intermediateExpression :: Expr s Import + intermediateExpression = fmap absurd expression + term :: Term + term = Dhall.Binary.encode _protocolVersion intermediateExpression + + bytesLazy = Codec.Serialise.serialise term + + bytesStrict = Data.ByteString.Lazy.toStrict bytesLazy + +-- | Hash a fully resolved expression +hashExpression :: ProtocolVersion -> Expr s X -> (Crypto.Hash.Digest SHA256) +hashExpression _protocolVersion expression = + Crypto.Hash.hash (encodeExpression _protocolVersion expression) + {-| Convenience utility to hash a fully resolved expression and return the base-16 encoded hash with the @sha256:@ prefix In other words, the output of this function can be pasted into Dhall source code to add an integrity check to an import -} -hashExpressionToCode :: Expr s X -> Text -hashExpressionToCode expr = "sha256:" <> Text.pack (show (hashExpression expr)) +hashExpressionToCode :: ProtocolVersion -> Expr s X -> Text +hashExpressionToCode _protocolVersion expr = + "sha256:" <> Text.pack (show (hashExpression _protocolVersion expr)) 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 @@ -75,7 +75,7 @@ <> show e' #endif -needManager :: StateT Status IO Manager +needManager :: StateT (Status m) IO Manager needManager = do x <- zoom manager State.get case join (fmap fromDynamic x) of @@ -97,7 +97,7 @@ fetchFromHttpUrl :: String -> Maybe [(CI ByteString, ByteString)] - -> StateT Status IO (String, Text.Text) + -> StateT (Status m) IO (String, Text.Text) fetchFromHttpUrl url mheaders = do m <- needManager diff --git a/src/Dhall/Import/Types.hs b/src/Dhall/Import/Types.hs --- a/src/Dhall/Import/Types.hs +++ b/src/Dhall/Import/Types.hs @@ -1,48 +1,87 @@ -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall #-} module Dhall.Import.Types where import Control.Exception (Exception) +import Control.Monad.Trans.State.Strict (StateT) import Data.Dynamic import Data.List.NonEmpty (NonEmpty) import Data.Map (Map) import Data.Semigroup ((<>)) -import Lens.Family (LensLike') -import System.FilePath (isRelative, splitDirectories) - -import qualified Data.Map as Map -import qualified Data.Text - +import Dhall.Binary (ProtocolVersion(..)) +import Dhall.Context (Context) import Dhall.Core - ( Directory (..), Expr, File (..), FilePrefix (..), Import (..) - , ImportHashed (..), ImportMode (..), ImportType (..) + ( Directory (..) + , Expr + , File (..) + , FilePrefix (..) + , Import (..) + , ImportHashed (..) + , ImportMode (..) + , ImportType (..) + , ReifiedNormalizer(..) ) import Dhall.Parser (Src) import Dhall.TypeCheck (X) +import Lens.Family (LensLike') +import System.FilePath (isRelative, splitDirectories) +import qualified Dhall.Binary +import qualified Dhall.Context +import qualified Data.Map as Map +import qualified Data.Text -- | State threaded throughout the import process -data Status = Status - { _stack :: NonEmpty Import +data Status m = Status + { _stack :: NonEmpty Import -- ^ Stack of `Import`s that we've imported along the way to get to the -- current point - , _cache :: Map Import (Expr Src X) + + , _cache :: Map Import (Expr Src X) -- ^ Cache of imported expressions in order to avoid importing the same -- expression twice with different values + , _manager :: Maybe Dynamic -- ^ Cache for the HTTP `Manager` so that we only acquire it once + + , _protocolVersion :: ProtocolVersion + + , _normalizer :: ReifiedNormalizer X + + , _startingContext :: Context (Expr Src X) + + , _resolver :: Import -> StateT (Status m) m (Expr Src Import) } --- | Default starting `Status`, importing relative to the given directory. -emptyStatus :: FilePath -> Status -emptyStatus dir = Status (pure rootImport) Map.empty Nothing +-- | Default starting `Status` that is polymorphic in the base `Monad` +emptyStatusWith + :: (Import -> StateT (Status m) m (Expr Src Import)) + -> FilePath + -> Status m +emptyStatusWith _resolver rootDirectory = Status {..} where - prefix = if isRelative dir + _stack = pure rootImport + + _cache = Map.empty + + _manager = Nothing + + _protocolVersion = Dhall.Binary.defaultProtocolVersion + + _normalizer = ReifiedNormalizer (const Nothing) + + _startingContext = Dhall.Context.empty + + prefix = if isRelative rootDirectory then Here else Absolute - pathComponents = fmap Data.Text.pack (reverse (splitDirectories dir)) + pathComponents = + fmap Data.Text.pack (reverse (splitDirectories rootDirectory)) + dirAsFile = File (Directory pathComponents) "." + -- Fake import to set the directory we're relative to. rootImport = Import { importHashed = ImportHashed @@ -52,17 +91,30 @@ , importMode = Code } - -stack :: Functor f => LensLike' f Status (NonEmpty Import) +stack :: Functor f => LensLike' f (Status m) (NonEmpty Import) stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) -cache :: Functor f => LensLike' f Status (Map Import (Expr Src X)) +cache :: Functor f => LensLike' f (Status m) (Map Import (Expr Src X)) cache k s = fmap (\x -> s { _cache = x }) (k (_cache s)) -manager :: Functor f => LensLike' f Status (Maybe Dynamic) +manager :: Functor f => LensLike' f (Status m) (Maybe Dynamic) manager k s = fmap (\x -> s { _manager = x }) (k (_manager s)) +protocolVersion :: Functor f => LensLike' f (Status m) ProtocolVersion +protocolVersion k s = + fmap (\x -> s { _protocolVersion = x }) (k (_protocolVersion s)) +normalizer :: Functor f => LensLike' f (Status m) (ReifiedNormalizer X) +normalizer k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s)) + +startingContext :: Functor f => LensLike' f (Status m) (Context (Expr Src X)) +startingContext k s = + fmap (\x -> s { _startingContext = x }) (k (_startingContext s)) + +resolver + :: Functor f + => LensLike' f (Status m) (Import -> StateT (Status m) m (Expr Src Import)) +resolver k s = fmap (\x -> s { _resolver = x }) (k (_resolver s)) {-| This exception indicates that there was an internal error in Dhall's import-related logic diff --git a/src/Dhall/Lint.hs b/src/Dhall/Lint.hs --- a/src/Dhall/Lint.hs +++ b/src/Dhall/Lint.hs @@ -1,3 +1,5 @@ +-- | This module contains the implementation of the @dhall lint@ command + module Dhall.Lint ( -- * Lint lint @@ -8,6 +10,10 @@ import qualified Dhall.Core +{-| Automatically improve a Dhall expression + + Currently this only removes unused @let@ bindings +-} lint :: Expr s Import -> Expr t Import lint expression = loop (Dhall.Core.denote expression) where @@ -28,8 +34,8 @@ a' = loop a b' = loop b loop (Let a b c d) - | not (V a 0 `Dhall.Core.freeIn` d) = - loop d + | not (V a 0 `Dhall.Core.freeIn` d') = + d' | otherwise = Let a b' c' d' where diff --git a/src/Dhall/Main.hs b/src/Dhall/Main.hs --- a/src/Dhall/Main.hs +++ b/src/Dhall/Main.hs @@ -1,26 +1,36 @@ +{-| This module contains the top-level entrypoint and options parsing for the + @dhall@ executable +-} + {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} module Dhall.Main - ( -- Commands - parseOptions + ( -- * Options + Options(..) + , Mode(..) + , parseOptions , parserInfoOptions + + -- * Execution , command , main ) where import Control.Applicative (optional, (<|>)) import Control.Exception (Exception, SomeException) -import Data.Monoid (mempty, (<>)) +import Data.Monoid ((<>)) import Data.Text (Text) import Data.Text.Prettyprint.Doc (Pretty) import Data.Version (showVersion) -import Dhall.Core (Expr, Import) -import Dhall.Import (Imported(..), load) +import Dhall.Binary (ProtocolVersion) +import Dhall.Core (Expr(..), Import) +import Dhall.Import (Imported(..)) import Dhall.Parser (Src) import Dhall.Pretty (annToAnsiStyle, prettyExpr, layoutOpts) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) +import Lens.Family (set) import Options.Applicative (Parser, ParserInfo) import System.Exit (exitFailure) import System.IO (Handle) @@ -28,16 +38,19 @@ import qualified Paths_dhall as Meta import qualified Control.Exception +import qualified Control.Monad.Trans.State.Strict as State import qualified Data.Text import qualified Data.Text.IO import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty import qualified Dhall +import qualified Dhall.Binary import qualified Dhall.Core import qualified Dhall.Diff import qualified Dhall.Format import qualified Dhall.Freeze import qualified Dhall.Hash +import qualified Dhall.Import import qualified Dhall.Lint import qualified Dhall.Parser import qualified Dhall.Repl @@ -47,14 +60,17 @@ import qualified System.Console.ANSI import qualified System.IO +-- | Top-level program options data Options = Options - { mode :: Mode - , explain :: Bool - , plain :: Bool + { mode :: Mode + , explain :: Bool + , plain :: Bool + , protocolVersion :: ProtocolVersion } +-- | The subcommands for the @dhall@ executable data Mode - = Default + = Default { annotate :: Bool } | Version | Resolve | Type @@ -74,8 +90,14 @@ <> Options.Applicative.metavar "FILE" ) +-- | `Parser` for the `Options` type parseOptions :: Parser Options -parseOptions = Options <$> parseMode <*> parseExplain <*> parsePlain +parseOptions = + Options + <$> parseMode + <*> parseExplain + <*> parsePlain + <*> Dhall.Binary.parseProtocolVersion where parseExplain = Options.Applicative.switch @@ -102,7 +124,7 @@ <|> subcommand "lint" "Improve Dhall code" parseLint <|> formatSubcommand <|> freezeSubcommand - <|> pure Default + <|> parseDefault where subcommand name description modeParser = Options.Applicative.subparser @@ -147,6 +169,13 @@ where parseFreeze = Freeze <$> optional parseInplace + parseDefault = Default <$> parseAnnotate + where + parseAnnotate = + Options.Applicative.switch + ( Options.Applicative.long "annotate" + ) + data ImportResolutionDisabled = ImportResolutionDisabled deriving (Exception) instance Show ImportResolutionDisabled where @@ -166,6 +195,7 @@ assertNoImports expression = throws (traverse (\_ -> Left ImportResolutionDisabled) expression) +-- | `ParserInfo` for the `Options` type parserInfoOptions :: ParserInfo Options parserInfoOptions = Options.Applicative.info @@ -174,10 +204,15 @@ <> Options.Applicative.fullDesc ) +-- | Run the command specified by the `Options` type command :: Options -> IO () command (Options {..}) = do GHC.IO.Encoding.setLocaleEncoding System.IO.utf8 + let status = + set Dhall.Import.protocolVersion protocolVersion (Dhall.Import.emptyStatus ".") + + let handle = Control.Exception.handle handler2 . Control.Exception.handle handler1 @@ -225,23 +260,26 @@ Version -> do putStrLn (showVersion Meta.version) - Default -> do + Default {..} -> do expression <- getExpression - resolvedExpression <- load expression + resolvedExpression <- State.evalStateT (Dhall.Import.loadWith expression) status inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression) - render System.IO.stderr (Dhall.Core.normalize inferredType) + let normalizedExpression = Dhall.Core.normalize resolvedExpression - Data.Text.IO.hPutStrLn System.IO.stderr mempty + let annotatedExpression = + if annotate + then Annot normalizedExpression inferredType + else normalizedExpression - render System.IO.stdout (Dhall.Core.normalize resolvedExpression) + render System.IO.stdout annotatedExpression Resolve -> do expression <- getExpression - resolvedExpression <- load expression + resolvedExpression <- State.evalStateT (Dhall.Import.loadWith expression) status render System.IO.stdout resolvedExpression @@ -264,7 +302,7 @@ render System.IO.stdout (Dhall.Core.normalize inferredType) Repl -> do - Dhall.Repl.repl explain + Dhall.Repl.repl explain protocolVersion Diff expr1 expr2 -> do expression1 <- Dhall.inputExpr expr1 @@ -280,10 +318,10 @@ Dhall.Format.format inplace Freeze inplace -> do - Dhall.Freeze.freeze inplace + Dhall.Freeze.freeze inplace protocolVersion Hash -> do - Dhall.Hash.hash + Dhall.Hash.hash protocolVersion Lint inplace -> do case inplace of @@ -320,6 +358,7 @@ System.IO.stdout (Pretty.layoutSmart layoutOpts (Pretty.unAnnotate doc)) +-- | Entry point for the @dhall@ executable main :: IO () main = do options <- Options.Applicative.execParser parserInfoOptions diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -1,4 +1,5 @@ {-# LANGUAGE RecordWildCards #-} + -- | This module contains Dhall's parsing logic module Dhall.Parser ( diff --git a/src/Dhall/Parser/Combinators.hs b/src/Dhall/Parser/Combinators.hs --- a/src/Dhall/Parser/Combinators.hs +++ b/src/Dhall/Parser/Combinators.hs @@ -131,6 +131,12 @@ satisfy :: (Char -> Bool) -> Parser Text satisfy = fmap Data.Text.singleton . Text.Parser.Char.satisfy +takeWhile :: (Char -> Bool) -> Parser Text +takeWhile predicate = Parser (Text.Megaparsec.takeWhileP Nothing predicate) + +takeWhile1 :: (Char -> Bool) -> Parser Text +takeWhile1 predicate = Parser (Text.Megaparsec.takeWhile1P Nothing predicate) + noDuplicates :: Ord a => [a] -> Parser (Set a) noDuplicates = go Data.Set.empty where 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 @@ -1,3 +1,4 @@ +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} -- | Parsing Dhall expressions. @@ -168,7 +169,7 @@ makeOperatorExpression subExpression operatorParser operator embedded = noted (do a <- subExpression embedded - b <- many (do operatorParser; subExpression embedded) + b <- Text.Megaparsec.many (do operatorParser; subExpression embedded) return (foldr1 operator (a:b)) ) importAltExpression :: Parser a -> Parser (Expr Src a) @@ -223,7 +224,7 @@ applicationExpression embedded = do f <- (do _constructors; return Constructors) <|> return id a <- noted (importExpression embedded) - b <- many (noted (importExpression embedded)) + b <- Text.Megaparsec.many (noted (importExpression embedded)) return (foldl app (f a) b) where app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = @@ -246,7 +247,7 @@ let left x e = Field e x let right xs e = Project e xs - b <- many (try (do _dot; fmap left label <|> fmap right labels)) + b <- Text.Megaparsec.many (try (do _dot; fmap left label <|> fmap right labels)) return (foldl (\e k -> k e) a b) ) primitiveExpression :: Parser a -> Parser (Expr Src a) @@ -526,7 +527,7 @@ doubleQuotedLiteral :: Parser a -> Parser (Chunks Src a) doubleQuotedLiteral embedded = do _ <- Text.Parser.Char.char '"' - chunks <- many (doubleQuotedChunk embedded) + chunks <- Text.Megaparsec.many (doubleQuotedChunk embedded) _ <- Text.Parser.Char.char '"' return (mconcat chunks) @@ -626,7 +627,7 @@ let nonEmptyRecordType = do _colon b <- expression embedded - e <- many (do + e <- Text.Megaparsec.many (do _comma c <- label _colon @@ -638,7 +639,7 @@ let nonEmptyRecordLiteral = do _equal b <- expression embedded - e <- many (do + e <- Text.Megaparsec.many (do _comma c <- label _equal @@ -666,7 +667,7 @@ let alternative0 = do _equal b <- expression embedded - kvs <- many (do + kvs <- Text.Megaparsec.many (do _bar c <- label _colon @@ -693,7 +694,7 @@ nonEmptyListLiteral embedded = (do _openBracket a <- expression embedded - b <- many (do _comma; expression embedded) + b <- Text.Megaparsec.many (do _comma; expression embedded) _closeBracket return (ListLit Nothing (Data.Sequence.fromList (a:b))) ) "list literal" @@ -757,12 +758,12 @@ http :: Parser ImportType http = do - (prefix, path, suffix) <- httpRaw + url <- httpRaw whitespace headers <- optional (do _using (importHashed_ <|> (_openParens *> importHashed_ <* _closeParens)) ) - return (URL prefix path suffix headers) + return (Remote (url { headers })) missing :: Parser ImportType missing = do diff --git a/src/Dhall/Parser/Token.hs b/src/Dhall/Parser/Token.hs --- a/src/Dhall/Parser/Token.hs +++ b/src/Dhall/Parser/Token.hs @@ -6,7 +6,7 @@ import Dhall.Parser.Combinators -import Control.Applicative (Alternative(..)) +import Control.Applicative (Alternative(..), optional) import Data.Functor (void) import Data.Semigroup (Semigroup(..)) import Data.Set (Set) @@ -34,6 +34,9 @@ whitespace :: Parser () whitespace = Text.Parser.Combinators.skipMany whitespaceChunk +nonemptyWhitespace :: Parser () +nonemptyWhitespace = Text.Parser.Combinators.skipSome whitespaceChunk + alpha :: Char -> Bool alpha c = ('\x41' <= c && c <= '\x5A') || ('\x61' <= c && c <= '\x7A') @@ -155,10 +158,9 @@ simpleLabel :: Parser Text simpleLabel = try (do - c <- Text.Parser.Char.satisfy headCharacter - cs <- many (Text.Parser.Char.satisfy tailCharacter) - let string = c:cs - let text = Data.Text.pack string + c <- Text.Parser.Char.satisfy headCharacter + rest <- Dhall.Parser.Combinators.takeWhile tailCharacter + let text = Data.Text.cons c rest Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers)) return text ) where @@ -169,9 +171,9 @@ backtickLabel :: Parser Text backtickLabel = do _ <- Text.Parser.Char.char '`' - t <- some (Text.Parser.Char.satisfy predicate) + t <- takeWhile1 predicate _ <- Text.Parser.Char.char '`' - return (Data.Text.pack t) + return t where predicate c = alpha c || digit c || elem c ("$-/_:." :: String) @@ -247,20 +249,27 @@ return (File {..}) -scheme :: Parser Text -scheme = "http" <> option "s" +scheme_ :: Parser Scheme +scheme_ = + ("http" :: Parser Text) + *> ((("s" :: Parser Text) *> pure HTTPS) <|> pure HTTP) + <* ("://" :: Parser Text) -httpRaw :: Parser (Text, File, Text) +httpRaw :: Parser URL httpRaw = do - prefixText <- scheme <> "://" <> authority - file <- file_ - suffixText <- option ("?" <> query) <> option ("#" <> fragment) + scheme <- scheme_ + authority <- authority_ + path <- file_ + query <- optional (("?" :: Parser Text) *> query_) + fragment <- optional (("#" :: Parser Text) *> fragment_) - return (prefixText, file, suffixText) + let headers = Nothing -authority :: Parser Text -authority = option (try (userinfo <> "@")) <> host <> option (":" <> port) + return (URL {..}) +authority_ :: Parser Text +authority_ = option (try (userinfo <> "@")) <> host <> option (":" <> port) + userinfo :: Parser Text userinfo = star (satisfy predicate <|> pctEncoded) where @@ -369,13 +378,13 @@ where predicate c = unreserved c || subDelims c || c == ':' || c == '@' -query :: Parser Text -query = star (pchar <|> satisfy predicate) +query_ :: Parser Text +query_ = star (pchar <|> satisfy predicate) where predicate c = c == '/' || c == '?' -fragment :: Parser Text -fragment = star (pchar <|> satisfy predicate) +fragment_ :: Parser Text +fragment_ = star (pchar <|> satisfy predicate) where predicate c = c == '/' || c == '?' @@ -392,32 +401,35 @@ reserved :: Data.Text.Text -> Parser () reserved x = do _ <- Text.Parser.Char.text x; whitespace +keyword :: Data.Text.Text -> Parser () +keyword x = try (do _ <- Text.Parser.Char.text x; nonemptyWhitespace) + _if :: Parser () -_if = reserved "if" +_if = keyword "if" _then :: Parser () -_then = reserved "then" +_then = keyword "then" _else :: Parser () -_else = reserved "else" +_else = keyword "else" _let :: Parser () -_let = reserved "let" +_let = keyword "let" _in :: Parser () -_in = reserved "in" +_in = keyword "in" _as :: Parser () -_as = reserved "as" +_as = keyword "as" _using :: Parser () -_using = reserved "using" +_using = keyword "using" _merge :: Parser () -_merge = reserved "merge" +_merge = keyword "merge" _constructors :: Parser () -_constructors = reserved "constructors" +_constructors = keyword "constructors" _NaturalFold :: Parser () _NaturalFold = reserved "Natural/fold" diff --git a/src/Dhall/Pretty.hs b/src/Dhall/Pretty.hs --- a/src/Dhall/Pretty.hs +++ b/src/Dhall/Pretty.hs @@ -1,11 +1,18 @@ {-| This module contains logic for pretty-printing expressions, including support for syntax highlighting -} -module Dhall.Pretty ( Ann(..), annToAnsiStyle, prettyExpr, layoutOpts ) where +module Dhall.Pretty + ( -- * Pretty + Ann(..) + , annToAnsiStyle + , prettyExpr + , layoutOpts + ) where import Dhall.Pretty.Internal import qualified Data.Text.Prettyprint.Doc as Pretty +-- | Default layout options layoutOpts :: Pretty.LayoutOptions layoutOpts = Pretty.defaultLayoutOptions diff --git a/src/Dhall/Repl.hs b/src/Dhall/Repl.hs --- a/src/Dhall/Repl.hs +++ b/src/Dhall/Repl.hs @@ -1,19 +1,29 @@ +-- | This module contains the implementation of the @dhall repl@ subcommand + {-# language FlexibleContexts #-} {-# language NamedFieldPuns #-} {-# language OverloadedStrings #-} -module Dhall.Repl ( repl ) where +module Dhall.Repl + ( -- * Repl + repl + ) where import Control.Exception ( SomeException(SomeException), displayException, throwIO ) 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 Dhall.Binary (ProtocolVersion(..)) +import Dhall.Import (protocolVersion) +import Lens.Family (set) +import qualified Control.Monad.Trans.State.Strict as State 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 ) import qualified Dhall +import qualified Dhall.Binary import qualified Dhall.Context import qualified Dhall.Core as Dhall ( Var(V), Expr, normalize ) import qualified Dhall.Pretty @@ -26,9 +36,9 @@ import qualified System.Console.Repline as Repline import qualified System.IO - -repl :: Bool -> IO () -repl explain = if explain then Dhall.detailed io else io +-- | Implementation of the @dhall repl@ subcommand +repl :: Bool -> ProtocolVersion -> IO () +repl explain _protocolVersion = if explain then Dhall.detailed io else io where io = evalStateT @@ -39,13 +49,14 @@ ( Repline.Word completer ) greeter ) - (emptyEnv { explain }) + (emptyEnv { explain, _protocolVersion }) data Env = Env - { envBindings :: Dhall.Context.Context Binding - , envIt :: Maybe Binding - , explain :: Bool + { envBindings :: Dhall.Context.Context Binding + , envIt :: Maybe Binding + , explain :: Bool + , _protocolVersion :: ProtocolVersion } @@ -55,6 +66,7 @@ { envBindings = Dhall.Context.empty , envIt = Nothing , explain = False + , _protocolVersion = Dhall.Binary.defaultProtocolVersion } @@ -78,6 +90,9 @@ :: ( MonadIO m, MonadState Env m ) => String -> m ( Dhall.Expr Dhall.Src Dhall.X ) parseAndLoad src = do + env <- + get + parsed <- case Dhall.exprFromText "(stdin)" ( Text.pack src ) of Left e -> @@ -86,7 +101,10 @@ Right a -> return a - liftIO ( Dhall.load parsed ) + let status = + set protocolVersion (_protocolVersion env) (Dhall.emptyStatus ".") + + liftIO ( State.evalStateT (Dhall.loadWith parsed) status ) eval :: ( MonadIO m, MonadState Env m ) => String -> m () diff --git a/src/Dhall/TH.hs b/src/Dhall/TH.hs --- a/src/Dhall/TH.hs +++ b/src/Dhall/TH.hs @@ -21,7 +21,10 @@ time with all imports resolved, making it easy to keep your Dhall configs and Haskell interpreters in sync. -} -module Dhall.TH where +module Dhall.TH + ( -- * Template Haskell + staticDhallExpression + ) where import Data.Typeable import Language.Haskell.TH.Quote (dataToExpQ) -- 7.10 compatibility. diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -1427,7 +1427,7 @@ -- Dhall URL imports let you add or modify request headers with the @using@ -- keyword: -- --- > https://example.com using ./headers +-- > https://example.com/example.dhall using ./headers -- -- ... where you can replace @./headers@ with any import that points to a Dhall -- expression of the following type: @@ -1451,16 +1451,16 @@ -- You cannot inline the headers within the same file as the URL. You must -- provide them as a separate import. That means that this is /not/ legal code: -- --- > http://example.com using [ { header = "Accept", value = "application/dhall" } ] -- NOT legal +-- > http://example.com/example.dhall using [ { header = "Accept", value = "application/dhall" } ] -- NOT legal -- -- Dhall will forward imports if you import an expression from a URL that -- contains a relative import. For example, if you import an expression like -- this: -- --- > http://example.com using ./headers +-- > http://example.com/example.dhall using ./headers -- --- ... and @http:\/\/example.com@ contains a relative import of @./foo@ then --- Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. +-- ... and @http:\/\/example.com/example.dhall@ contains a relative import of @./foo@ +-- then Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. -- $integrity -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -556,6 +556,20 @@ Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY)) + ttKvsX <- fmap Dhall.Core.normalize (loop ctx tKvsX) + constX <- case ttKvsX of + Const constX -> return constX + _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY)) + + ttKvsY <- fmap Dhall.Core.normalize (loop ctx tKvsY) + constY <- case ttKvsY of + Const constY -> return constY + _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY)) + + if constX == constY + then return () + else Left (TypeError ctx e (RecordMismatch '∧' kvsX kvsY constX constY)) + let combineTypes ktsL ktsR = do let ksL = Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsL) @@ -632,6 +646,21 @@ ktsY <- case tKvsY of Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) + + ttKvsX <- fmap Dhall.Core.normalize (loop ctx tKvsX) + constX <- case ttKvsX of + Const constX -> return constX + _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) + + ttKvsY <- fmap Dhall.Core.normalize (loop ctx tKvsY) + constY <- case ttKvsY of + Const constY -> return constY + _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) + + if constX == constY + then return () + else Left (TypeError ctx e (RecordMismatch '⫽' kvsX kvsY constX constY)) + return (Record (Data.HashMap.Strict.InsOrd.union ktsY ktsX)) loop ctx e@(Merge kvsX kvsY (Just t)) = do _ <- loop ctx t @@ -807,6 +836,7 @@ | ListAppendMismatch (Expr s a) (Expr s a) | DuplicateAlternative Text | MustCombineARecord Char (Expr s a) (Expr s a) + | RecordMismatch Char (Expr s a) (Expr s a) Const Const | CombineTypesRequiresRecordType (Expr s a) (Expr s a) | RecordTypeMismatch Const Const (Expr s a) (Expr s a) | FieldCollision Text @@ -2453,6 +2483,61 @@ op = pretty c txt0 = insert expr0 txt1 = insert expr1 + +prettyTypeMessage (RecordMismatch c expr0 expr1 const0 const1) = ErrorMessages {..} + where + short = "Record mismatch" + + long = + "Explanation: You can only use the ❰" <> op <> "❱ operator to combine records if they both \n\ + \store terms or both store types. \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────────────┐ \n\ + \ │ { foo = 1 } " <> op <> " { baz = True } │ Valid: Both records store terms \n\ + \ └──────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌─────────────────────────────────┐ \n\ + \ │ { foo = Bool } " <> op <> " { bar = Text } │ Valid: Both records store types \n\ + \ └─────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but you cannot combine two records if one of the records stores types and \n\ + \the other record stores terms. \n\ + \ \n\ + \For example, the following expression is " <> _NOT <> " valid: \n\ + \ \n\ + \ \n\ + \ Record of terms \n\ + \ ⇩ \n\ + \ ┌──────────────────────────────┐ \n\ + \ │ { foo = 1 } " <> op <> " { bar = Text } │ Invalid: Mixing terms and types \n\ + \ └──────────────────────────────┘ \n\ + \ ⇧ \n\ + \ Record of types \n\ + \ \n\ + \ \n\ + \You tried to combine the following record: \n\ + \ \n\ + \" <> txt0 <> "\n\ + \ \n\ + \... which stores " <> class0 <> ", with the following record: \n\ + \ \n\ + \" <> txt1 <> "\n\ + \ \n\ + \... which stores " <> class1 <> ". \n" + where + op = pretty c + + txt0 = insert expr0 + txt1 = insert expr1 + + toClass Type = "terms" + toClass Kind = "types" + + class0 = toClass const0 + class1 = toClass const1 prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) = ErrorMessages {..} diff --git a/tests/Import.hs b/tests/Import.hs --- a/tests/Import.hs +++ b/tests/Import.hs @@ -8,9 +8,9 @@ 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.Context import qualified Dhall.Parser import qualified Dhall.Import import qualified Test.Tasty @@ -47,6 +47,14 @@ "works" "./tests/import/data/foo/bar" "./tests/import/relative.dhall" + , shouldNotFailRelative + "a semantic integrity check if fields are reordered" + "./tests/import/" + "./tests/import/fieldOrderC.dhall" + , shouldNotFailRelative + "a semantic integrity check when importing an expression using `constructors`" + "./tests/import/" + "./tests/import/issue553B.dhall" ] ] @@ -65,7 +73,9 @@ expr <- case Dhall.Parser.exprFromText mempty text of Left err -> throwIO err Right expr -> return expr - _ <- Dhall.Import.loadDirWith dir Dhall.Import.exprFromImport Dhall.Context.empty (const Nothing) expr + + _ <- State.evalStateT (Dhall.Import.loadWith expr) (Dhall.Import.emptyStatus dir) + return ()) shouldFail :: Int -> Text -> FilePath -> TestTree diff --git a/tests/Normalization.hs b/tests/Normalization.hs --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -186,6 +186,7 @@ [ shouldNormalize "Natural/plus" "naturalPlus" , shouldNormalize "Optional/fold" "optionalFold" , shouldNormalize "Optional/build" "optionalBuild" + , shouldNormalize "Natural/build" "naturalBuild" ] conversions :: TestTree diff --git a/tests/QuickCheck.hs b/tests/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/tests/QuickCheck.hs @@ -0,0 +1,347 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module QuickCheck where + +import Codec.Serialise (DeserialiseFailure(..)) +import Control.Monad (guard) +import Data.Hashable (Hashable) +import Data.HashMap.Strict.InsOrd (InsOrdHashMap) +import Dhall.Core + ( Chunks(..) + , Const(..) + , Directory(..) + , Expr(..) + , File(..) + , FilePrefix(..) + , Import(..) + , ImportHashed(..) + , ImportMode(..) + , ImportType(..) + , Scheme(..) + , URL(..) + , Var(..) + ) +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 Data.HashMap.Strict.InsOrd +import qualified Data.Sequence +import qualified Dhall.Binary +import qualified Dhall.Core +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 + +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 (Eq k, Hashable k, Arbitrary k, Arbitrary v) => Arbitrary (InsOrdHashMap k v) where + arbitrary = do + n <- Test.QuickCheck.choose (0, 2) + kvs <- Test.QuickCheck.vectorOf n ((,) <$> arbitrary <*> arbitrary) + return (Data.HashMap.Strict.InsOrd.fromList kvs) + + shrink = + map Data.HashMap.Strict.InsOrd.fromList + . shrink + . Data.HashMap.Strict.InsOrd.toList + +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 ] + + 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) + , ( 1, Test.QuickCheck.oneof [ lift3 (Let "_"), lift4 Let ]) + , ( 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.decode + (Codec.Serialise.deserialiseOrFail + (Codec.Serialise.serialise + (Dhall.Binary.encode Dhall.Binary.defaultProtocolVersion 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/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -3,6 +3,7 @@ import Normalization (normalizationTests) import Parser (parserTests) import Regression (regressionTests) +import QuickCheck (quickcheckTests) import Tutorial (tutorialTests) import TypeCheck (typecheckTests) import Format (formatTests) @@ -19,6 +20,7 @@ , formatTests , typecheckTests , importTests + , quickcheckTests ] main :: IO () diff --git a/tests/TypeCheck.hs b/tests/TypeCheck.hs --- a/tests/TypeCheck.hs +++ b/tests/TypeCheck.hs @@ -4,6 +4,9 @@ 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 @@ -43,6 +46,13 @@ , should "correctly handle α-equivalent merge alternatives" "mergeEquivalence" + + , shouldNotTypeCheck + "combining records of terms and types" + "combineMixedRecords" + , shouldNotTypeCheck + "preferring a record of types over a record of terms" + "preferMixedRecords" ] should :: Text -> Text -> TestTree @@ -64,3 +74,26 @@ 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/import/fieldOrderA.dhall b/tests/import/fieldOrderA.dhall new file mode 100644 --- /dev/null +++ b/tests/import/fieldOrderA.dhall @@ -0,0 +1,1 @@ +{ foo = 1, bar = True } diff --git a/tests/import/fieldOrderB.dhall b/tests/import/fieldOrderB.dhall new file mode 100644 --- /dev/null +++ b/tests/import/fieldOrderB.dhall @@ -0,0 +1,1 @@ +{ bar = True, foo = 1 } diff --git a/tests/import/fieldOrderC.dhall b/tests/import/fieldOrderC.dhall new file mode 100644 --- /dev/null +++ b/tests/import/fieldOrderC.dhall @@ -0,0 +1,3 @@ +{ example0 = ./fieldOrderA.dhall sha256:c8e5944a964f1b35da4f2a7dc16b8de0221a518997fd84b0363a955d8f4459a4 +, example1 = ./fieldOrderB.dhall sha256:c8e5944a964f1b35da4f2a7dc16b8de0221a518997fd84b0363a955d8f4459a4 +} diff --git a/tests/import/issue553A.dhall b/tests/import/issue553A.dhall new file mode 100644 --- /dev/null +++ b/tests/import/issue553A.dhall @@ -0,0 +1,5 @@ + let T = < A : {} | B : {} > + +in let t = constructors T + +in t diff --git a/tests/import/issue553B.dhall b/tests/import/issue553B.dhall new file mode 100644 --- /dev/null +++ b/tests/import/issue553B.dhall @@ -0,0 +1,1 @@ +./issue553A.dhall sha256:2324a5352105b6835db60b127c7096c5d5b81027969ccd368d163edc5d9692e0 diff --git a/tests/normalization/naturalBuildB.dhall b/tests/normalization/naturalBuildB.dhall --- a/tests/normalization/naturalBuildB.dhall +++ b/tests/normalization/naturalBuildB.dhall @@ -1,7 +1,7 @@ { example0 = - +1 + 1 , example1 = - +1 + 1 , example2 = - λ(id : ∀(a : Type) → a → a) → id Natural +1 + λ(id : ∀(a : Type) → a → a) → id Natural 1 } diff --git a/tests/typecheck/combineMixedRecords.dhall b/tests/typecheck/combineMixedRecords.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/combineMixedRecords.dhall @@ -0,0 +1,1 @@ +{ foo = 1 } ∧ { bar = Text } diff --git a/tests/typecheck/preferMixedRecords.dhall b/tests/typecheck/preferMixedRecords.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/preferMixedRecords.dhall @@ -0,0 +1,1 @@ +{ foo = 1 } ⫽ { bar = Text }