dhall 1.16.1 → 1.17.0

raw patch · 38 files changed

+2301/−446 lines, 38 filesdep +QuickCheckdep +cborgdep +hashabledep ~bytestringdep ~containersdep ~directoryPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, cborg, hashable, quickcheck-instances, serialise, tasty-quickcheck

Dependency ranges changed: bytestring, containers, directory, insert-ordered-containers, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +43/−0
• benchmark/deep-nested-large-record/Main.hs +2/−1
• benchmark/parser/Main.hs +24/−4
• dhall.cabal +18/−4
• src/Dhall.hs +143/−19
• src/Dhall/Binary.hs +795/−0
• src/Dhall/Core.hs +185/−137
• src/Dhall/Diff.hs +11/−11
• src/Dhall/Format.hs +12/−2
• src/Dhall/Freeze.hs +47/−21
• src/Dhall/Hash.hs +31/−13
• src/Dhall/Import.hs +249/−129
• src/Dhall/Import/HTTP.hs +2/−2
• src/Dhall/Import/Types.hs +73/−21
• src/Dhall/Lint.hs +8/−2
• src/Dhall/Main.hs +59/−20
• src/Dhall/Parser.hs +1/−0
• src/Dhall/Parser/Combinators.hs +6/−0
• src/Dhall/Parser/Expression.hs +11/−10
• src/Dhall/Parser/Token.hs +41/−29
• src/Dhall/Pretty.hs +8/−1
• src/Dhall/Repl.hs +27/−9
• src/Dhall/TH.hs +4/−1
• src/Dhall/Tutorial.hs +5/−5
• src/Dhall/TypeCheck.hs +85/−0
• tests/Import.hs +12/−2
• tests/Normalization.hs +1/−0
• tests/QuickCheck.hs +347/−0
• tests/Tests.hs +2/−0
• tests/TypeCheck.hs +33/−0
• tests/import/fieldOrderA.dhall +1/−0
• tests/import/fieldOrderB.dhall +1/−0
• tests/import/fieldOrderC.dhall +3/−0
• tests/import/issue553A.dhall +5/−0
• tests/import/issue553B.dhall +1/−0
• tests/normalization/naturalBuildB.dhall +3/−3
• tests/typecheck/combineMixedRecords.dhall +1/−0
• tests/typecheck/preferMixedRecords.dhall +1/−0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1,4 +1,5 @@ {-# LANGUAGE RecordWildCards            #-}+ -- | This module contains Dhall's parsing logic  module Dhall.Parser (

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

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

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

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

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

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

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

@@ -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 {..}

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

@@ -186,6 +186,7 @@         [ shouldNormalize "Natural/plus"   "naturalPlus"         , shouldNormalize "Optional/fold"  "optionalFold"         , shouldNormalize "Optional/build" "optionalBuild"+        , shouldNormalize "Natural/build"  "naturalBuild"         ]  conversions :: TestTree

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

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

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

@@ -0,0 +1,1 @@+{ foo = 1, bar = True }

@@ -0,0 +1,1 @@+{ bar = True, foo = 1 }

@@ -0,0 +1,3 @@+{ example0 = ./fieldOrderA.dhall sha256:c8e5944a964f1b35da4f2a7dc16b8de0221a518997fd84b0363a955d8f4459a4 +, example1 = ./fieldOrderB.dhall sha256:c8e5944a964f1b35da4f2a7dc16b8de0221a518997fd84b0363a955d8f4459a4 +}

@@ -0,0 +1,5 @@+    let T = < A : {} | B : {} >++in  let t = constructors T++in  t

@@ -0,0 +1,1 @@+./issue553A.dhall sha256:2324a5352105b6835db60b127c7096c5d5b81027969ccd368d163edc5d9692e0

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

@@ -0,0 +1,1 @@+{ foo = 1 } ∧ { bar = Text }

@@ -0,0 +1,1 @@+{ foo = 1 } ⫽ { bar = Text }