dhall 1.9.1 → 1.10.0
raw patch · 53 files changed
+3756/−3004 lines, 53 filesdep +ansi-terminaldep +directorydep +filepathdep −charsetdep −system-fileiodep −system-filepathdep ~basedep ~optparse-genericdep ~prettyprinternew-component:exe:dhall-replPVP ok
version bump matches the API change (PVP)
Dependencies added: ansi-terminal, directory, filepath, haskeline, insert-ordered-containers, mtl, prettyprinter-ansi-terminal, repline, scientific
Dependencies removed: charset, system-fileio, system-filepath
Dependency ranges changed: base, optparse-generic, prettyprinter, text, trifecta
API changes (from Hackage documentation)
+ Dhall: class GenericInject f
+ Dhall: genericInjectWith :: GenericInject f => InterpretOptions -> State Int (InputType (f a))
+ Dhall: instance Dhall.Inject Data.Scientific.Scientific
+ Dhall: instance Dhall.Interpret Data.Scientific.Scientific
+ Dhall: instance Dhall.Interpret [GHC.Types.Char]
+ Dhall: scientific :: Type Scientific
+ Dhall.Context: match :: Context a -> Maybe (Text, a, Context a)
+ Dhall.Import: Status :: [Path] -> Map Path (Expr Src X) -> Maybe Manager -> Status
+ Dhall.Import: [_cache] :: Status -> Map Path (Expr Src X)
+ Dhall.Import: [_manager] :: Status -> Maybe Manager
+ Dhall.Import: [_stack] :: Status -> [Path]
+ Dhall.Import: data Status
+ Dhall.Import: emptyStatus :: Status
+ Dhall.Pretty: Builtin :: Ann
+ Dhall.Pretty: Keyword :: Ann
+ Dhall.Pretty: Label :: Ann
+ Dhall.Pretty: Literal :: Ann
+ Dhall.Pretty: Operator :: Ann
+ Dhall.Pretty: Syntax :: Ann
+ Dhall.Pretty: annToAnsiStyle :: Ann -> AnsiStyle
+ Dhall.Pretty: data Ann
+ Dhall.Pretty: prettyExpr :: Pretty a => Expr s a -> Doc Ann
+ Dhall.TypeCheck: checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
- Dhall.Core: DoubleLit :: Double -> Expr s a
+ Dhall.Core: DoubleLit :: Scientific -> Expr s a
- Dhall.Core: Record :: (Map Text (Expr s a)) -> Expr s a
+ Dhall.Core: Record :: (InsOrdHashMap Text (Expr s a)) -> Expr s a
- Dhall.Core: RecordLit :: (Map Text (Expr s a)) -> Expr s a
+ Dhall.Core: RecordLit :: (InsOrdHashMap Text (Expr s a)) -> Expr s a
- Dhall.Core: Union :: (Map Text (Expr s a)) -> Expr s a
+ Dhall.Core: Union :: (InsOrdHashMap Text (Expr s a)) -> Expr s a
- Dhall.Core: UnionLit :: Text -> (Expr s a) -> (Map Text (Expr s a)) -> Expr s a
+ Dhall.Core: UnionLit :: Text -> (Expr s a) -> (InsOrdHashMap Text (Expr s a)) -> Expr s a
Files
- CHANGELOG.md +29/−0
- dhall-format/Main.hs +30/−19
- dhall-hash/Main.hs +12/−11
- dhall-repl/Main.hs +232/−0
- dhall.cabal +72/−46
- dhall/Main.hs +39/−24
- src/Dhall.hs +87/−42
- src/Dhall/Context.hs +12/−0
- src/Dhall/Core.hs +1574/−2584
- src/Dhall/Core.hs-boot +7/−0
- src/Dhall/Import.hs +39/−54
- src/Dhall/Parser.hs +30/−22
- src/Dhall/Pretty.hs +6/−0
- src/Dhall/Pretty/Internal.hs +1153/−0
- src/Dhall/Pretty/Internal.hs-boot +31/−0
- src/Dhall/TypeCheck.hs +70/−27
- tests/Format.hs +12/−0
- tests/Normalization.hs +65/−130
- tests/Parser.hs +36/−39
- tests/Regression.hs +20/−6
- tests/Tests.hs +2/−0
- tests/TypeCheck.hs +53/−0
- tests/format/emptyRecordA.dhall +1/−0
- tests/format/emptyRecordB.dhall +1/−0
- tests/format/escapeNumericLabelA.dhall +1/−0
- tests/format/escapeNumericLabelB.dhall +1/−0
- tests/format/fieldOrderA.dhall +1/−0
- tests/format/fieldOrderB.dhall +1/−0
- tests/format/largeExponentA.dhall +1/−0
- tests/format/largeExponentB.dhall +1/−0
- tests/normalization/doubleShowA.dhall +1/−0
- tests/normalization/doubleShowB.dhall +1/−0
- tests/normalization/integerShowA.dhall +4/−0
- tests/normalization/integerShowB.dhall +1/−0
- tests/normalization/naturalPlusA.dhall +1/−0
- tests/normalization/naturalPlusB.dhall +1/−0
- tests/normalization/naturalShowA.dhall +1/−0
- tests/normalization/naturalShowB.dhall +1/−0
- tests/normalization/naturalToIntegerA.dhall +1/−0
- tests/normalization/naturalToIntegerB.dhall +1/−0
- tests/normalization/optionalBuildA.dhall +22/−0
- tests/normalization/optionalBuildB.dhall +12/−0
- tests/normalization/optionalBuildFoldA.dhall +11/−0
- tests/normalization/optionalBuildFoldB.dhall +10/−0
- tests/normalization/optionalFoldA.dhall +7/−0
- tests/normalization/optionalFoldB.dhall +1/−0
- tests/normalization/remoteSystemsA.dhall +55/−0
- tests/normalization/remoteSystemsB.dhall +1/−0
- tests/parser/reservedPrefix.dhall +1/−0
- tests/typecheck/alternativesAreTypesA.dhall +1/−0
- tests/typecheck/alternativesAreTypesB.dhall +1/−0
- tests/typecheck/fieldsAreTypesA.dhall +1/−0
- tests/typecheck/fieldsAreTypesB.dhall +1/−0
CHANGELOG.md view
@@ -1,3 +1,32 @@+1.10.0++* Feature: Records/unions can now have fields/alternatives that are types+ * i.e. `{ foo = Text, bar = List }` is legal now+ * See: https://github.com/dhall-lang/dhall-haskell/pull/273+* Feature: New `dhall-repl` for interactively evaluating Dhall expressions+ * See: https://github.com/dhall-lang/dhall-haskell/pull/266+* Feature: Syntax highlighting+ * See: https://github.com/dhall-lang/dhall-haskell/pull/260+* Feature: BREAKING CHANGE TO THE API: `dhall-format` preserves field order+ * This changes the syntax tree to use an `InsOrdHashMap` instead of a `Map`+* BREAKING CHANGE TO THE API: Use Haskell's `Scientific` type+ * This is fixes the interpreter to correct handle really large/small numbers+ * This also allows marshaling into Haskell's `Scientific` type+ * See: https://github.com/dhall-lang/dhall-haskell/pull/256+* BREAKING CHANGE TO THE API: Remove `system-filepath`/`system-fileio` dependencies+ * Now the library uses `Prelude.FilePath`+ * See: https://github.com/dhall-lang/dhall-haskell/pull/248+* Feature: Labels can now begin with reserved names+ * i.e. `List/map` is now a legal label+ * See: https://github.com/dhall-lang/dhall-haskell/pull/255+* Fix: Rendered labels are now correctly escaped if they are numbers+ * See: https://github.com/dhall-lang/dhall-haskell/pull/252+* Add the instance `Interpret String`.+ * See: https://github.com/dhall-lang/dhall-haskell/pull/247+* Fix: Custom contexts passed to `typeWith` are now checked+ * This prevents a custom context from triggering an infinite loop+ * See: https://github.com/dhall-lang/dhall-haskell/pull/259+ 1.9.1 * `dhall-format` now emits single-quoted strings for multi-line strings
dhall-format/Main.hs view
@@ -1,7 +1,9 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeOperators #-} {-| Utility executable for pretty-printing Dhall code@@ -30,9 +32,8 @@ import Data.Monoid ((<>)) import Data.Version (showVersion) import Dhall.Parser (exprAndHeaderFromText)-import Filesystem.Path.CurrentOS (FilePath)-import Options.Generic (Generic, ParseRecord, type (<?>)(..))-import Prelude hiding (FilePath)+import Dhall.Pretty (annToAnsiStyle, prettyExpr)+import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::)) import System.IO (stderr) import System.Exit (exitFailure, exitSuccess) import Text.Trifecta.Delta (Delta(..))@@ -43,18 +44,18 @@ import qualified Data.Text.IO import qualified Data.Text.Lazy import qualified Data.Text.Lazy.IO-import qualified Data.Text.Prettyprint.Doc as Pretty-import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty-import qualified Filesystem.Path.CurrentOS+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty import qualified Options.Generic+import qualified System.Console.ANSI import qualified System.IO -data Options = Options- { version :: Bool <?> "Display version and exit"- , inplace :: Maybe FilePath <?> "Modify the specified file in-place"+data Options w = Options+ { version :: w ::: Bool <?> "Display version and exit"+ , inplace :: w ::: Maybe FilePath <?> "Modify the specified file in-place" } deriving (Generic) -instance ParseRecord Options+instance ParseRecord (Options Wrapped) opts :: Pretty.LayoutOptions opts =@@ -63,8 +64,8 @@ main :: IO () main = do- options <- Options.Generic.getRecord "Formatter for the Dhall language"- when (unHelpful (version options)) $ do+ Options {..} <- Options.Generic.unwrapRecord "Formatter for the Dhall language"+ when version $ do putStrLn (showVersion Meta.version) exitSuccess @@ -75,17 +76,16 @@ System.Exit.exitFailure Control.Exception.handle handler (do- case unHelpful (inplace options) of+ case inplace of Just file -> do- let fileString = Filesystem.Path.CurrentOS.encodeString file- strictText <- Data.Text.IO.readFile fileString+ strictText <- Data.Text.IO.readFile file let lazyText = Data.Text.Lazy.fromStrict strictText (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) lazyText of Left err -> Control.Exception.throwIO err Right x -> return x let doc = Pretty.pretty header <> Pretty.pretty expr- System.IO.withFile fileString System.IO.WriteMode (\handle -> do+ System.IO.withFile file System.IO.WriteMode (\handle -> do Pretty.renderIO handle (Pretty.layoutSmart opts doc) Data.Text.IO.hPutStrLn handle "" ) Nothing -> do@@ -96,6 +96,17 @@ Left err -> Control.Exception.throwIO err Right x -> return x - let doc = Pretty.pretty header <> Pretty.pretty expr- Pretty.renderIO System.IO.stdout (Pretty.layoutSmart opts doc)- Data.Text.IO.putStrLn "" )+ let doc = Pretty.pretty header <> prettyExpr expr++ supportsANSI <- System.Console.ANSI.hSupportsANSI System.IO.stdout++ if supportsANSI+ then+ Pretty.renderIO+ System.IO.stdout+ (fmap annToAnsiStyle (Pretty.layoutSmart opts doc))+ else+ Pretty.renderIO+ System.IO.stdout+ (Pretty.layoutSmart opts (Pretty.unAnnotate doc))+ Data.Text.IO.putStrLn "")
dhall-hash/Main.hs view
@@ -1,20 +1,21 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeOperators #-} module Main where import Control.Exception (SomeException) import Control.Monad (when)-import Data.Monoid (mempty) import Data.Version (showVersion)-import Dhall.Core (pretty, normalize)+import Dhall.Core (normalize) import Dhall.Import (Imported(..), hashExpressionToCode, load) import Dhall.Parser (Src, exprFromText) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)-import Options.Generic (Generic, ParseRecord, type (<?>)(..))+import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::)) import System.IO (stderr) import System.Exit (exitFailure, exitSuccess) import Text.Trifecta.Delta (Delta(..))@@ -27,17 +28,17 @@ import qualified Options.Generic import qualified System.IO -data Options = Options- { explain :: Bool <?> "Explain error messages in more detail"- , version :: Bool <?> "Display version and exit"+data Options w = Options+ { explain :: w ::: Bool <?> "Explain error messages in more detail"+ , version :: w ::: Bool <?> "Display version and exit" } deriving (Generic) -instance ParseRecord Options+instance ParseRecord (Options Wrapped) main :: IO () main = do- options <- Options.Generic.getRecord "Compiler for the Dhall language"- when (unHelpful (version options)) $ do+ Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"+ when version $ do putStrLn (showVersion Meta.version) exitSuccess let handle =@@ -48,7 +49,7 @@ handler0 e = do let _ = e :: TypeError Src X System.IO.hPutStrLn stderr ""- if unHelpful (explain options)+ if explain then Control.Exception.throwIO (DetailedTypeError e) else do Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"@@ -57,7 +58,7 @@ handler1 (Imported ps e) = do let _ = e :: TypeError Src X System.IO.hPutStrLn stderr ""- if unHelpful (explain options)+ if explain then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) else do Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"
+ dhall-repl/Main.hs view
@@ -0,0 +1,232 @@+{-# language FlexibleContexts #-}+{-# language NamedFieldPuns #-}+{-# language OverloadedStrings #-}++module Main ( main ) 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 qualified Data.Text.Lazy as LazyText+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty ( renderIO )+import qualified Dhall.Context+import qualified Dhall.Core as Dhall ( Var(V), Expr, normalize )+import qualified Dhall.Pretty+import qualified Dhall.Core as Expr ( Expr(..) )+import qualified Dhall.Import as Dhall+import qualified Dhall.Parser as Dhall+import qualified Dhall.TypeCheck as Dhall+import qualified System.Console.Haskeline.MonadException as Haskeline+import qualified System.Console.Repline as Repline+import qualified System.IO+import qualified Text.Trifecta.Delta as Trifecta+++main :: IO ()+main =+ evalStateT+ ( Repline.evalRepl+ "⊢ "+ ( dontCrash . eval )+ options+ ( Repline.Word completer )+ greeter+ )+ emptyEnv+++data Env = Env+ { envBindings :: Dhall.Context.Context Binding+ , envIt :: Maybe Binding+ }+++emptyEnv :: Env+emptyEnv =+ Env+ { envBindings = Dhall.Context.empty+ , envIt = Nothing+ }+++data Binding = Binding+ { bindingExpr :: Dhall.Expr Dhall.Src Dhall.X+ , bindingType :: Dhall.Expr Dhall.Src Dhall.X+ }+++envToContext :: Env -> Dhall.Context.Context Binding+envToContext Env{ envBindings, envIt } =+ case envIt of+ Nothing ->+ envBindings++ Just it ->+ Dhall.Context.insert "it" it envBindings+++parseAndLoad+ :: ( MonadIO m, MonadState Env m )+ => String -> m ( Dhall.Expr Dhall.Src Dhall.X )+parseAndLoad src = do+ parsed <-+ case Dhall.exprFromText ( Trifecta.Columns 0 0 ) ( LazyText.pack src ) of+ Left e ->+ liftIO ( throwIO e )++ Right a ->+ return a++ liftIO ( Dhall.load parsed )+++eval :: ( MonadIO m, MonadState Env m ) => String -> m ()+eval src = do+ loaded <-+ parseAndLoad src++ exprType <-+ typeCheck loaded++ expr <-+ normalize loaded++ modify ( \e -> e { envIt = Just ( Binding expr exprType ) } )++ output expr++++typeOf :: ( MonadIO m, MonadState Env m ) => [String] -> m ()+typeOf [] =+ liftIO ( putStrLn ":type requires an argument to check the type of" )+++typeOf srcs = do+ loaded <-+ parseAndLoad ( unwords srcs )++ exprType <-+ typeCheck loaded++ exprType' <-+ normalize exprType++ output ( Expr.Annot loaded exprType' )++++normalize+ :: MonadState Env m+ => Dhall.Expr Dhall.Src Dhall.X -> m ( Dhall.Expr t Dhall.X )+normalize e = do+ env <-+ get++ return+ ( Dhall.normalize+ ( foldl'+ ( \a (k, Binding { bindingType, bindingExpr }) ->+ Expr.Let k ( Just bindingType ) bindingExpr a+ )+ e+ ( Dhall.Context.toList ( envToContext env ) )+ )+ )+++typeCheck+ :: ( MonadIO m, MonadState Env m )+ => Dhall.Expr Dhall.Src Dhall.X -> m ( Dhall.Expr Dhall.Src Dhall.X )+typeCheck expr = do+ env <-+ get++ case Dhall.typeWith ( bindingType <$> envToContext env ) expr of+ Left e ->+ liftIO ( throwIO e )++ Right a ->+ return a+++addBinding :: ( MonadIO m, MonadState Env m ) => [String] -> m ()+addBinding (k : "=" : srcs) = do+ let+ varName =+ LazyText.pack k++ loaded <-+ parseAndLoad ( unwords srcs )++ t <-+ typeCheck loaded++ expr <-+ normalize loaded++ modify+ ( \e ->+ e+ { envBindings =+ Dhall.Context.insert+ varName+ Binding { bindingType = t, bindingExpr = expr }+ ( envBindings e )+ }+ )++ output+ ( Expr.Annot ( Expr.Var ( Dhall.V varName 0 ) ) t )++addBinding _ =+ liftIO ( fail ":let should be of the form `:let x = y`" )+++options+ :: ( Haskeline.MonadException m, MonadIO m, MonadState Env m )+ => Repline.Options m+options =+ [ ( "type", dontCrash . typeOf )+ , ( "let", dontCrash . addBinding )+ ]+++completer :: Monad m => Repline.WordCompleter m+completer _ =+ return []+++greeter :: MonadIO m => m ()+greeter =+ return ()+++dontCrash :: ( MonadIO m, Haskeline.MonadException m ) => m () -> m ()+dontCrash m =+ Haskeline.catch+ m+ ( \ e@SomeException{} -> liftIO ( putStrLn ( displayException e ) ) )+++output :: ( Pretty.Pretty a, MonadIO m ) => Dhall.Expr s a -> m ()+output expr = do+ let+ opts =+ Pretty.defaultLayoutOptions+ { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }++ liftIO+ ( Pretty.renderIO+ System.IO.stdout+ ( fmap+ Dhall.Pretty.annToAnsiStyle+ ( Pretty.layoutSmart opts ( Dhall.Pretty.prettyExpr expr ) )+ )+ )++ liftIO ( putStrLn "" ) -- Pretty printing doesn't end with a new line
dhall.cabal view
@@ -1,5 +1,5 @@ Name: dhall-Version: 1.9.1+Version: 1.10.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1@@ -82,9 +82,11 @@ Prelude/Text/concatMapSep Prelude/Text/concatSep tests/format/*.dhall+ tests/normalization/*.dhall tests/parser/*.dhall tests/regression/*.dhall tests/tutorial/*.dhall+ tests/typecheck/*.dhall Source-Repository head Type: git@@ -93,64 +95,87 @@ Library Hs-Source-Dirs: src Build-Depends:- base >= 4.9.0.0 && < 5 ,- ansi-wl-pprint < 0.7 ,- base16-bytestring < 0.2 ,- bytestring < 0.11,- case-insensitive < 1.3 ,- charset < 0.4 ,- containers >= 0.5.0.0 && < 0.6 ,- contravariant < 1.5 ,- cryptohash < 0.12,- exceptions >= 0.8.3 && < 0.9 ,- http-client >= 0.4.30 && < 0.6 ,- http-client-tls >= 0.2.0 && < 0.4 ,- lens-family-core >= 1.0.0 && < 1.3 ,- parsers >= 0.12.4 && < 0.13,- prettyprinter >= 1.1.1 && < 1.2 ,- system-filepath >= 0.3.1 && < 0.5 ,- system-fileio >= 0.2.1 && < 0.4 ,- text >= 0.11.1.0 && < 1.3 ,- text-format < 0.4 ,- transformers >= 0.2.0.0 && < 0.6 ,- trifecta >= 1.6 && < 1.8 ,- unordered-containers >= 0.1.3.0 && < 0.3 ,- vector >= 0.11.0.0 && < 0.13+ base >= 4.9.0.0 && < 5 ,+ ansi-wl-pprint < 0.7 ,+ base16-bytestring < 0.2 ,+ bytestring < 0.11,+ case-insensitive < 1.3 ,+ containers >= 0.5.0.0 && < 0.6 ,+ contravariant < 1.5 ,+ cryptohash < 0.12,+ exceptions >= 0.8.3 && < 0.9 ,+ directory >= 1.3 && < 1.4 ,+ filepath >= 1.4 && < 1.5 ,+ http-client >= 0.4.30 && < 0.6 ,+ http-client-tls >= 0.2.0 && < 0.4 ,+ insert-ordered-containers >= 0.1.0.1 && < 0.3 ,+ lens-family-core >= 1.0.0 && < 1.3 ,+ parsers >= 0.12.4 && < 0.13,+ prettyprinter >= 1.2.0.1 && < 1.3 ,+ prettyprinter-ansi-terminal >= 1.1.1 && < 1.2 ,+ scientific >= 0.3.0.0 && < 0.4 ,+ text >= 0.11.1.0 && < 1.3 ,+ text-format < 0.4 ,+ transformers >= 0.2.0.0 && < 0.6 ,+ trifecta >= 1.6 && < 1.8 ,+ unordered-containers >= 0.1.3.0 && < 0.3 ,+ vector >= 0.11.0.0 && < 0.13 Exposed-Modules: Dhall, Dhall.Context, Dhall.Core, Dhall.Import, Dhall.Parser,+ Dhall.Pretty, Dhall.Tutorial, Dhall.TypeCheck+ Other-Modules:+ Dhall.Pretty.Internal GHC-Options: -Wall Executable dhall Hs-Source-Dirs: dhall Main-Is: Main.hs Build-Depends:- base >= 4 && < 5 ,- dhall ,- optparse-generic >= 1.1.1 && < 1.3,- prettyprinter ,- trifecta >= 1.6 && < 1.8,- text >= 0.11.1.0 && < 1.3+ ansi-terminal >= 0.6.3.1 && < 0.8 ,+ base >= 4 && < 5 ,+ dhall ,+ optparse-generic >= 1.1.1 && < 1.4 ,+ prettyprinter ,+ prettyprinter-ansi-terminal >= 1.1.1 && < 1.2 ,+ trifecta >= 1.6 && < 1.8 ,+ text >= 0.11.1.0 && < 1.3 GHC-Options: -Wall Other-Modules: Paths_dhall +Executable dhall-repl+ Hs-Source-Dirs: dhall-repl+ Main-Is: Main.hs+ Build-Depends:+ base >= 4 && < 5 ,+ dhall ,+ haskeline >= 0.7.3.0 && < 0.8 ,+ mtl >= 2.2.1 && < 2.3 ,+ repline >= 0.1.6.0 && < 0.2 ,+ prettyprinter ,+ prettyprinter-ansi-terminal ,+ text ,+ trifecta+ GHC-Options: -Wall+ Executable dhall-format Hs-Source-Dirs: dhall-format Main-Is: Main.hs Build-Depends:- base >= 4 && < 5 ,+ base >= 4 && < 5 ,+ ansi-terminal >= 0.6.3.1 && < 0.8 , dhall ,- optparse-generic >= 1.1.1 && < 1.3,- prettyprinter >= 1.1.1 && < 1.2,- system-filepath >= 0.3.1 && < 0.5,- trifecta >= 1.6 && < 1.8,- text >= 0.11.1.0 && < 1.3+ optparse-generic >= 1.1.1 && < 1.4 ,+ prettyprinter >= 1.2.0.1 && < 1.3 ,+ prettyprinter-ansi-terminal >= 1.1.1 && < 1.2 ,+ trifecta >= 1.6 && < 1.8 ,+ text >= 0.11.1.0 && < 1.3 GHC-Options: -Wall Other-Modules: Paths_dhall@@ -161,7 +186,7 @@ Build-Depends: base >= 4 && < 5 , dhall ,- optparse-generic >= 1.1.1 && < 1.3,+ optparse-generic >= 1.1.1 && < 1.4, trifecta >= 1.6 && < 1.8, text >= 0.11.1.0 && < 1.3 Other-Modules:@@ -179,14 +204,15 @@ Parser Regression Tutorial+ TypeCheck Util Build-Depends:- base >= 4 && < 5 ,- containers >= 0.5.0.0 && < 0.6 ,- deepseq >= 1.2.0.1 && < 1.5 ,- dhall ,- prettyprinter ,- tasty >= 0.11.2 && < 1.1 ,- tasty-hunit >= 0.9.2 && < 0.11,- text >= 0.11.1.0 && < 1.3 ,- vector >= 0.11.0.0 && < 0.13+ base >= 4 && < 5 ,+ deepseq >= 1.2.0.1 && < 1.5 ,+ dhall ,+ insert-ordered-containers ,+ prettyprinter ,+ tasty >= 0.11.2 && < 1.1 ,+ tasty-hunit >= 0.9.2 && < 0.11,+ text >= 0.11.1.0 && < 1.3 ,+ vector >= 0.11.0.0 && < 0.13
dhall/Main.hs view
@@ -1,20 +1,23 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeOperators #-} module Main where import Control.Exception (SomeException) import Control.Monad (when)-import Data.Monoid (mempty, (<>))+import Data.Monoid (mempty) import Data.Version (showVersion) import Dhall.Core (normalize) import Dhall.Import (Imported(..), load)-import Dhall.Parser (Src, exprAndHeaderFromText)+import Dhall.Parser (Src)+import Dhall.Pretty (annToAnsiStyle, prettyExpr) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)-import Options.Generic (Generic, ParseRecord, type (<?>)(..))+import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::)) import System.Exit (exitFailure, exitSuccess) import Text.Trifecta.Delta (Delta(..)) @@ -22,30 +25,34 @@ import qualified Control.Exception import qualified Data.Text.Lazy.IO-import qualified Data.Text.Prettyprint.Doc as Pretty-import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty-import qualified Dhall.Core+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty+import qualified Dhall.Parser import qualified Dhall.TypeCheck import qualified Options.Generic+import qualified System.Console.ANSI import qualified System.IO -data Options = Options- { explain :: Bool <?> "Explain error messages in more detail"- , version :: Bool <?> "Display version and exit"- , pretty :: Bool <?> "Format output"+data Options w = Options+ { explain :: w ::: Bool <?> "Explain error messages in more detail"+ , version :: w ::: Bool <?> "Display version and exit"+ , pretty :: w ::: Bool <?> "Format output" } deriving (Generic) -instance ParseRecord Options+instance ParseRecord (Options Wrapped) opts :: Pretty.LayoutOptions opts = Pretty.defaultLayoutOptions { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } +unbounded :: Pretty.LayoutOptions+unbounded = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }+ main :: IO () main = do- options <- Options.Generic.getRecord "Compiler for the Dhall language"- when (unHelpful (version options)) $ do+ Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"+ when version $ do putStrLn (showVersion Meta.version) exitSuccess @@ -57,7 +64,7 @@ handler0 e = do let _ = e :: TypeError Src X System.IO.hPutStrLn System.IO.stderr ""- if unHelpful (explain options)+ if explain then Control.Exception.throwIO (DetailedTypeError e) else do Data.Text.Lazy.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"@@ -66,7 +73,7 @@ handler1 (Imported ps e) = do let _ = e :: TypeError Src X System.IO.hPutStrLn System.IO.stderr ""- if unHelpful (explain options)+ if explain then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) else do Data.Text.Lazy.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"@@ -82,24 +89,32 @@ System.IO.hSetEncoding System.IO.stdin System.IO.utf8 inText <- Data.Text.Lazy.IO.getContents - (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) inText of+ expr <- case Dhall.Parser.exprFromText (Directed "(stdin)" 0 0 0 0) inText of Left err -> Control.Exception.throwIO err Right x -> return x - let render h e =- if unHelpful (pretty options)- then do- let doc = Pretty.pretty header <> Pretty.pretty e- Pretty.renderIO h (Pretty.layoutSmart opts doc)- Data.Text.Lazy.IO.hPutStrLn h ""- else do- Data.Text.Lazy.IO.hPutStrLn h (Dhall.Core.pretty e)+ let render h e = do+ let doc = prettyExpr e + let layoutOptions = if pretty then opts else unbounded+ let stream = Pretty.layoutSmart layoutOptions doc++ supportsANSI <- System.Console.ANSI.hSupportsANSI h+ let ansiStream =+ if supportsANSI+ then fmap annToAnsiStyle stream+ else Pretty.unAnnotateS stream++ Pretty.renderIO h ansiStream+ Data.Text.Lazy.IO.hPutStrLn h ""++ expr' <- load expr typeExpr <- case Dhall.TypeCheck.typeOf expr' of Left err -> Control.Exception.throwIO err Right typeExpr -> return typeExpr+ render System.IO.stderr (normalize typeExpr) Data.Text.Lazy.IO.hPutStrLn System.IO.stderr mempty render System.IO.stdout (normalize expr') )
src/Dhall.hs view
@@ -9,6 +9,7 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining@@ -34,6 +35,7 @@ , bool , natural , integer+ , scientific , double , lazyText , strictText@@ -44,6 +46,7 @@ , string , pair , GenericInterpret(..)+ , GenericInject(..) , Inject(..) , inject@@ -63,6 +66,7 @@ import Control.Monad.Trans.State.Strict import Data.Functor.Contravariant (Contravariant(..)) import Data.Monoid ((<>))+import Data.Scientific (Scientific) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Typeable (Typeable)@@ -80,7 +84,8 @@ import qualified Control.Exception import qualified Data.ByteString.Lazy import qualified Data.Foldable-import qualified Data.Map+import qualified Data.HashMap.Strict.InsOrd+import qualified Data.Scientific import qualified Data.Sequence import qualified Data.Set import qualified Data.Text@@ -379,19 +384,27 @@ expected = Integer -{-| Decode a `Double`+{-| Decode a `Scientific` ->>> input double "42.0"-42.0+>>> input scientific "1e1000000000"+1.0e1000000000 -}-double :: Type Double-double = Type {..}+scientific :: Type Scientific+scientific = Type {..} where extract (DoubleLit n) = pure n extract _ = empty expected = Double +{-| Decode a `Double`++>>> input double "42.0"+42.0+-}+double :: Type Double+double = fmap Data.Scientific.toRealFloat scientific+ {-| Decode lazy `Text` >>> input lazyText "\"Test\""@@ -457,10 +470,11 @@ unit :: Type () unit = Type extractOut expectedOut where- extractOut (RecordLit fields) | Data.Map.null fields = return ()+ extractOut (RecordLit fields)+ | Data.HashMap.Strict.InsOrd.null fields = return () extractOut _ = Nothing - expectedOut = Record Data.Map.empty+ expectedOut = Record Data.HashMap.Strict.InsOrd.empty {-| Decode a `String` @@ -480,12 +494,17 @@ pair l r = Type extractOut expectedOut where extractOut (RecordLit fields) =- (,) <$> ( Data.Map.lookup "_1" fields >>= extract l )- <*> ( Data.Map.lookup "_2" fields >>= extract r )+ (,) <$> ( Data.HashMap.Strict.InsOrd.lookup "_1" fields >>= extract l )+ <*> ( Data.HashMap.Strict.InsOrd.lookup "_2" fields >>= extract r ) extractOut _ = Nothing - expectedOut = Record (Data.Map.fromList [("_1", expected l)- ,("_2", expected r)])+ expectedOut =+ Record+ (Data.HashMap.Strict.InsOrd.fromList+ [ ("_1", expected l)+ , ("_2", expected r)+ ]+ ) {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input`@@ -512,9 +531,15 @@ instance Interpret Integer where autoWith _ = integer +instance Interpret Scientific where+ autoWith _ = scientific+ instance Interpret Double where autoWith _ = double +instance {-# OVERLAPS #-} Interpret [Char] where+ autoWith _ = string+ instance Interpret Text where autoWith _ = lazyText @@ -599,7 +624,7 @@ where extract _ = Nothing - expected = Union Data.Map.empty+ expected = Union Data.HashMap.Strict.InsOrd.empty instance (Constructor c1, Constructor c2, GenericInterpret f1, GenericInterpret f2) => GenericInterpret (M1 C c1 f1 :+: M1 C c2 f2) where genericAutoWith options@(InterpretOptions {..}) = pure (Type {..})@@ -620,7 +645,7 @@ extract _ = Nothing expected =- Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])+ Union (Data.HashMap.Strict.InsOrd.fromList [(nameL, expectedL), (nameR, expectedR)]) Type extractL expectedL = evalState (genericAutoWith options) 1 Type extractR expectedR = evalState (genericAutoWith options) 1@@ -638,7 +663,8 @@ | otherwise = fmap L1 (extractL u) extract _ = Nothing - expected = Union (Data.Map.insert name expectedR expectedL)+ expected =+ Union (Data.HashMap.Strict.InsOrd.insert name expectedR expectedL) Type extractL (Union expectedL) = evalState (genericAutoWith options) 1 Type extractR expectedR = evalState (genericAutoWith options) 1@@ -656,7 +682,8 @@ | otherwise = fmap R1 (extractR u) extract _ = Nothing - expected = Union (Data.Map.insert name expectedL expectedR)+ expected =+ Union (Data.HashMap.Strict.InsOrd.insert name expectedL expectedR) Type extractL expectedL = evalState (genericAutoWith options) 1 Type extractR (Union expectedR) = evalState (genericAutoWith options) 1@@ -666,7 +693,7 @@ where extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e) - expected = Union (Data.Map.union expectedL expectedR)+ expected = Union (Data.HashMap.Strict.InsOrd.union expectedL expectedR) Type extractL (Union expectedL) = evalState (genericAutoWith options) 1 Type extractR (Union expectedR) = evalState (genericAutoWith options) 1@@ -681,7 +708,7 @@ where extract _ = Just U1 - expected = Record (Data.Map.fromList [])+ expected = Record (Data.HashMap.Strict.InsOrd.fromList []) instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where genericAutoWith options = do@@ -689,8 +716,12 @@ Type extractR expectedR <- genericAutoWith options let Record ktsL = expectedL let Record ktsR = expectedR- pure (Type { extract = liftA2 (liftA2 (:*:)) extractL extractR- , expected = Record (Data.Map.union ktsL ktsR) })+ pure+ (Type+ { extract = liftA2 (liftA2 (:*:)) extractL extractR+ , expected = Record (Data.HashMap.Strict.InsOrd.union ktsL ktsR)+ }+ ) getSelName :: Selector s => M1 i s f a -> State Int String getSelName n = case selName n of@@ -704,10 +735,11 @@ name <- getSelName n let extract (RecordLit m) = do let name' = fieldModifier (Data.Text.Lazy.pack name)- e <- Data.Map.lookup name' m+ e <- Data.HashMap.Strict.InsOrd.lookup name' m fmap (M1 . K1) (extract' e) extract _ = Nothing- let expected = Record (Data.Map.fromList [(key, expected')])+ let expected =+ Record (Data.HashMap.Strict.InsOrd.fromList [(key, expected')]) where key = fieldModifier (Data.Text.Lazy.pack name) pure (Type {..})@@ -831,20 +863,23 @@ declared = Integer --instance Inject Double where+instance Inject Scientific where injectWith _ = InputType {..} where embed = DoubleLit declared = Double +instance Inject Double where+ injectWith =+ fmap (contramap (Data.Scientific.fromFloatDigits @Double)) injectWith+ instance Inject () where injectWith _ = InputType {..} where- embed = const (RecordLit Data.Map.empty)+ embed = const (RecordLit Data.HashMap.Strict.InsOrd.empty) - declared = Record Data.Map.empty+ declared = Record Data.HashMap.Strict.InsOrd.empty instance Inject a => Inject (Maybe a) where injectWith options = InputType embedOut declaredOut@@ -899,11 +934,14 @@ instance (Constructor c1, Constructor c2, GenericInject f1, GenericInject f2) => GenericInject (M1 C c1 f1 :+: M1 C c2 f2) where genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..}) where- embed (L1 (M1 l)) = UnionLit keyL (embedL l) Data.Map.empty- embed (R1 (M1 r)) = UnionLit keyR (embedR r) Data.Map.empty+ embed (L1 (M1 l)) =+ UnionLit keyL (embedL l) Data.HashMap.Strict.InsOrd.empty + embed (R1 (M1 r)) =+ UnionLit keyR (embedR r) Data.HashMap.Strict.InsOrd.empty+ declared =- Union (Data.Map.fromList [(keyL, declaredL), (keyR, declaredR)])+ Union (Data.HashMap.Strict.InsOrd.fromList [(keyL, declaredL), (keyR, declaredR)]) nL :: M1 i c1 f1 a nL = undefined@@ -920,7 +958,8 @@ instance (Constructor c, GenericInject (f :+: g), GenericInject h) => GenericInject ((f :+: g) :+: M1 C c h) where genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..}) where- embed (L1 l) = UnionLit keyL valL (Data.Map.insert keyR declaredR ktsL')+ embed (L1 l) =+ UnionLit keyL valL (Data.HashMap.Strict.InsOrd.insert keyR declaredR ktsL') where UnionLit keyL valL ktsL' = embedL l embed (R1 (M1 r)) = UnionLit keyR (embedR r) ktsL@@ -930,7 +969,7 @@ keyR = constructorModifier (Data.Text.Lazy.pack (conName nR)) - declared = Union (Data.Map.insert keyR declaredR ktsL)+ declared = Union (Data.HashMap.Strict.InsOrd.insert keyR declaredR ktsL) InputType embedL (Union ktsL) = evalState (genericInjectWith options) 1 InputType embedR declaredR = evalState (genericInjectWith options) 1@@ -939,7 +978,8 @@ genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..}) where embed (L1 (M1 l)) = UnionLit keyL (embedL l) ktsR- embed (R1 r) = UnionLit keyR valR (Data.Map.insert keyL declaredL ktsR')+ embed (R1 r) =+ UnionLit keyR valR (Data.HashMap.Strict.InsOrd.insert keyL declaredL ktsR') where UnionLit keyR valR ktsR' = embedR r @@ -948,7 +988,7 @@ keyL = constructorModifier (Data.Text.Lazy.pack (conName nL)) - declared = Union (Data.Map.insert keyL declaredL ktsR)+ declared = Union (Data.HashMap.Strict.InsOrd.insert keyL declaredL ktsR) InputType embedL declaredL = evalState (genericInjectWith options) 1 InputType embedR (Union ktsR) = evalState (genericInjectWith options) 1@@ -956,14 +996,16 @@ instance (GenericInject (f :+: g), GenericInject (h :+: i)) => GenericInject ((f :+: g) :+: (h :+: i)) where genericInjectWith options = pure (InputType {..}) where- embed (L1 l) = UnionLit keyL valR (Data.Map.union ktsL' ktsR)+ embed (L1 l) =+ UnionLit keyL valR (Data.HashMap.Strict.InsOrd.union ktsL' ktsR) where UnionLit keyL valR ktsL' = embedL l- embed (R1 r) = UnionLit keyR valR (Data.Map.union ktsL ktsR')+ embed (R1 r) =+ UnionLit keyR valR (Data.HashMap.Strict.InsOrd.union ktsL ktsR') where UnionLit keyR valR ktsR' = embedR r - declared = Union (Data.Map.union ktsL ktsR)+ declared = Union (Data.HashMap.Strict.InsOrd.union ktsL ktsR) InputType embedL (Union ktsL) = evalState (genericInjectWith options) 1 InputType embedR (Union ktsR) = evalState (genericInjectWith options) 1@@ -973,12 +1015,13 @@ InputType embedInL declaredInL <- genericInjectWith options InputType embedInR declaredInR <- genericInjectWith options - let embed (l :*: r) = RecordLit (Data.Map.union mapL mapR)+ let embed (l :*: r) =+ RecordLit (Data.HashMap.Strict.InsOrd.union mapL mapR) where RecordLit mapL = embedInL l RecordLit mapR = embedInR r - let declared = Record (Data.Map.union mapL mapR)+ let declared = Record (Data.HashMap.Strict.InsOrd.union mapL mapR) where Record mapL = declaredInL Record mapR = declaredInR@@ -988,15 +1031,17 @@ instance GenericInject U1 where genericInjectWith _ = pure (InputType {..}) where- embed _ = RecordLit Data.Map.empty+ embed _ = RecordLit Data.HashMap.Strict.InsOrd.empty - declared = Record Data.Map.empty+ declared = Record Data.HashMap.Strict.InsOrd.empty instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where genericInjectWith opts@(InterpretOptions {..}) = do name <- fieldModifier . Data.Text.Lazy.pack <$> getSelName n- let embed (M1 (K1 x)) = RecordLit (Data.Map.singleton name (embedIn x))- let declared = Record (Data.Map.singleton name declaredIn)+ let embed (M1 (K1 x)) =+ RecordLit (Data.HashMap.Strict.InsOrd.singleton name (embedIn x))+ let declared =+ Record (Data.HashMap.Strict.InsOrd.singleton name declaredIn) pure (InputType {..}) where n :: M1 i s f a
src/Dhall/Context.hs view
@@ -9,6 +9,7 @@ Context , empty , insert+ , match , lookup , toList ) where@@ -40,6 +41,17 @@ insert :: Text -> a -> Context a -> Context a insert k v (Context kvs) = Context ((k, v) : kvs) {-# INLINABLE insert #-}++{-| \"Pattern match\" on a `Context`++> match (insert k v ctx) = Just (k, v, ctx)+> match empty = Nothing+-}+match :: Context a -> Maybe (Text, a, Context a)+match (Context ((k, v) : kvs)) = Just (k, v, Context kvs)+match (Context [] ) = Nothing++{-# INLINABLE match #-} {-| Look up a key by name and index
src/Dhall/Core.hs view
@@ -52,2589 +52,1579 @@ import Control.Applicative (empty) import Data.Bifunctor (Bifunctor(..)) import Data.Foldable-import Data.HashSet (HashSet)-import Data.Map (Map)-import Data.Monoid ((<>))-import Data.String (IsString(..))-import Data.Text.Buildable (Buildable(..))-import Data.Text.Lazy (Text)-import Data.Text.Lazy.Builder (Builder)-import Data.Text.Prettyprint.Doc (Doc, Pretty)-import Data.Traversable-import Data.Vector (Vector)-import Filesystem.Path.CurrentOS (FilePath)-import Numeric.Natural (Natural)-import Prelude hiding (FilePath, succ)--import qualified Control.Monad-import qualified Data.ByteString-import qualified Data.ByteString.Char8-import qualified Data.ByteString.Base16-import qualified Data.Char-import qualified Data.HashSet-import qualified Data.List-import qualified Data.Map-import qualified Data.Maybe-import qualified Data.Text-import qualified Data.Text.Lazy as Text-import qualified Data.Text.Lazy.Builder as Builder-import qualified Data.Text.Prettyprint.Doc as Pretty-import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty-import qualified Data.Vector-import qualified Data.Vector.Mutable-import qualified Filesystem.Path.CurrentOS as Filesystem--{-| Constants for a pure type system-- The only axiom is:--> ⊦ Type : Kind-- ... and the valid rule pairs are:--> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)-> ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions)-> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors)-- These are the same rule pairs as System Fω-- 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, Bounded, Enum)--instance Buildable Const where- build = buildConst---- | Whether or not a path is relative to the user's home directory-data HasHome = Home | Homeless deriving (Eq, Ord, Show)---- | The type of path to import (i.e. local vs. remote vs. environment)-data PathType- = File HasHome FilePath- -- ^ Local path- | URL Text (Maybe PathHashed)- -- ^ URL of emote resource and optional headers stored in a path- | Env Text- -- ^ Environment variable- deriving (Eq, Ord, Show)--instance Buildable PathType where- build (File Home file)- = "~/" <> build txt- where- txt = Text.fromStrict (either id id (Filesystem.toText file))- build (File Homeless file)- | Text.isPrefixOf "./" txt- || Text.isPrefixOf "/" txt- || Text.isPrefixOf "../" txt- = build txt <> " "- | otherwise- = "./" <> build txt <> " "- where- txt = Text.fromStrict (either id id (Filesystem.toText file))- build (URL str Nothing ) = build str <> " "- build (URL str (Just headers)) = build str <> " using " <> build headers <> " "- build (Env env) = "env:" <> build env---- | How to interpret the path's contents (i.e. as Dhall code or raw text)-data PathMode = Code | RawText deriving (Eq, Ord, Show)--data PathHashed = PathHashed- { hash :: Maybe Data.ByteString.ByteString- , pathType :: PathType- } deriving (Eq, Ord, Show)--instance Buildable PathHashed where- build (PathHashed Nothing p) = build p- build (PathHashed (Just h) p) = build p <> "sha256:" <> build string <> " "- where- bytes = Data.ByteString.Base16.encode h-- string = Data.ByteString.Char8.unpack bytes---- | Path to an external resource-data Path = Path- { pathHashed :: PathHashed- , pathMode :: PathMode- } deriving (Eq, Ord, Show)--instance Buildable Path where- build (Path {..}) = build pathHashed <> suffix- where- suffix = case pathMode of- RawText -> "as Text"- Code -> ""--instance Pretty Path where- pretty path = Pretty.pretty (Builder.toLazyText (build path))--{-| Label for a bound variable-- The `Text` field is the variable's name (i.e. \"@x@\").-- The `Int` field disambiguates variables with the same name if there are- multiple bound variables of the same name in scope. Zero refers to the- nearest bound variable and the index increases by one for each bound- variable of the same name going outward. The following diagram may help:--> ┌──refers to──┐-> │ │-> v │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0->-> ┌─────────────────refers to─────────────────┐-> │ │-> v │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1-- This `Int` behaves like a De Bruijn index in the special case where all- variables have the same name.-- You can optionally omit the index if it is @0@:--> ┌─refers to─┐-> │ │-> v │-> λ(x : Type) → λ(y : Type) → λ(x : Type) → x-- Zero indices are omitted when pretty-printing `Var`s and non-zero indices- appear as a numeric suffix.--}-data Var = V Text !Integer- deriving (Eq, Show)--instance IsString Var where- fromString str = V (fromString str) 0--instance Buildable Var where- build = buildVar---- | Syntax tree for expressions-data Expr s a- -- | > Const c ~ c- = Const Const- -- | > Var (V x 0) ~ x- -- > Var (V x n) ~ x@n- | Var Var- -- | > Lam x A b ~ λ(x : A) -> b- | Lam Text (Expr s a) (Expr s a)- -- | > Pi "_" A B ~ A -> B- -- > Pi x A B ~ ∀(x : A) -> B- | Pi Text (Expr s a) (Expr s a)- -- | > App f a ~ f a- | App (Expr s a) (Expr s a)- -- | > Let x Nothing r e ~ let x = r in e- -- > Let x (Just t) r e ~ let x : t = r in e- | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)- -- | > Annot x t ~ x : t- | Annot (Expr s a) (Expr s a)- -- | > Bool ~ Bool- | Bool- -- | > BoolLit b ~ b- | BoolLit Bool- -- | > BoolAnd x y ~ x && y- | BoolAnd (Expr s a) (Expr s a)- -- | > BoolOr x y ~ x || y- | BoolOr (Expr s a) (Expr s a)- -- | > BoolEQ x y ~ x == y- | BoolEQ (Expr s a) (Expr s a)- -- | > BoolNE x y ~ x != y- | BoolNE (Expr s a) (Expr s a)- -- | > BoolIf x y z ~ if x then y else z- | BoolIf (Expr s a) (Expr s a) (Expr s a)- -- | > Natural ~ Natural- | Natural- -- | > NaturalLit n ~ +n- | NaturalLit Natural- -- | > NaturalFold ~ Natural/fold- | NaturalFold- -- | > NaturalBuild ~ Natural/build- | NaturalBuild- -- | > NaturalIsZero ~ Natural/isZero- | NaturalIsZero- -- | > NaturalEven ~ Natural/even- | NaturalEven- -- | > NaturalOdd ~ Natural/odd- | NaturalOdd- -- | > NaturalToInteger ~ Natural/toInteger- | NaturalToInteger- -- | > NaturalShow ~ Natural/show- | NaturalShow- -- | > NaturalPlus x y ~ x + y- | NaturalPlus (Expr s a) (Expr s a)- -- | > NaturalTimes x y ~ x * y- | NaturalTimes (Expr s a) (Expr s a)- -- | > Integer ~ Integer- | Integer- -- | > IntegerLit n ~ n- | IntegerLit Integer- -- | > IntegerShow ~ Integer/show- | IntegerShow- -- | > Double ~ Double- | Double- -- | > DoubleLit n ~ n- | DoubleLit Double- -- | > DoubleShow ~ Double/show- | DoubleShow- -- | > Text ~ Text- | Text- -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3"- | TextLit (Chunks s a)- -- | > TextAppend x y ~ x ++ y- | TextAppend (Expr s a) (Expr s a)- -- | > List ~ List- | List- -- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t- -- > ListLit Nothing [x, y, z] ~ [x, y, z]- | ListLit (Maybe (Expr s a)) (Vector (Expr s a))- -- | > ListAppend x y ~ x # y- | ListAppend (Expr s a) (Expr s a)- -- | > ListBuild ~ List/build- | ListBuild- -- | > ListFold ~ List/fold- | ListFold- -- | > ListLength ~ List/length- | ListLength- -- | > ListHead ~ List/head- | ListHead- -- | > ListLast ~ List/last- | ListLast- -- | > ListIndexed ~ List/indexed- | ListIndexed- -- | > ListReverse ~ List/reverse- | ListReverse- -- | > Optional ~ Optional- | Optional- -- | > OptionalLit t [e] ~ [e] : Optional t- -- > OptionalLit t [] ~ [] : Optional t- | OptionalLit (Expr s a) (Vector (Expr s a))- -- | > OptionalFold ~ Optional/fold- | OptionalFold- -- | > OptionalBuild ~ Optional/build- | OptionalBuild- -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }- | Record (Map Text (Expr s a))- -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }- | RecordLit (Map Text (Expr s a))- -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1 | k2 : t2 >- | Union (Map Text (Expr s a))- -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 >- | UnionLit Text (Expr s a) (Map Text (Expr s a))- -- | > Combine x y ~ x ∧ y- | Combine (Expr s a) (Expr s a)- -- | > CombineRight x y ~ x ⫽ y- | Prefer (Expr s a) (Expr s a)- -- | > Merge x y (Just t ) ~ merge x y : t- -- | > Merge x y Nothing ~ merge x y- | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))- -- | > Constructors e ~ constructors e- | Constructors (Expr s a)- -- | > Field e x ~ e.x- | Field (Expr s a) Text- -- | > Note s x ~ e- | Note s (Expr s a)- -- | > Embed path ~ path- | Embed a- deriving (Functor, Foldable, Traversable, Show, Eq)--instance Applicative (Expr s) where- pure = Embed-- (<*>) = Control.Monad.ap--instance Monad (Expr s) where- return = pure-- Const a >>= _ = Const a- Var a >>= _ = Var a- Lam a b c >>= k = Lam a (b >>= k) (c >>= k)- Pi a b c >>= k = Pi a (b >>= k) (c >>= k)- App a b >>= k = App (a >>= k) (b >>= k)- Let a b c d >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)- Annot a b >>= k = Annot (a >>= k) (b >>= k)- Bool >>= _ = Bool- BoolLit a >>= _ = BoolLit a- BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k)- BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k)- BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k)- BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k)- BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)- Natural >>= _ = Natural- NaturalLit a >>= _ = NaturalLit a- NaturalFold >>= _ = NaturalFold- NaturalBuild >>= _ = NaturalBuild- NaturalIsZero >>= _ = NaturalIsZero- NaturalEven >>= _ = NaturalEven- NaturalOdd >>= _ = NaturalOdd- NaturalToInteger >>= _ = NaturalToInteger- NaturalShow >>= _ = NaturalShow- NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k)- NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)- Integer >>= _ = Integer- IntegerLit a >>= _ = IntegerLit a- IntegerShow >>= _ = IntegerShow- Double >>= _ = Double- DoubleLit a >>= _ = DoubleLit a- DoubleShow >>= _ = DoubleShow- Text >>= _ = Text- TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b)- TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k)- List >>= _ = List- ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)- ListAppend a b >>= k = ListAppend (a >>= k) (b >>= k)- ListBuild >>= _ = ListBuild- ListFold >>= _ = ListFold- ListLength >>= _ = ListLength- ListHead >>= _ = ListHead- ListLast >>= _ = ListLast- ListIndexed >>= _ = ListIndexed- ListReverse >>= _ = ListReverse- Optional >>= _ = Optional- OptionalLit a b >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)- OptionalFold >>= _ = OptionalFold- OptionalBuild >>= _ = OptionalBuild- Record a >>= k = Record (fmap (>>= k) a)- RecordLit a >>= k = RecordLit (fmap (>>= k) a)- Union a >>= k = Union (fmap (>>= k) a)- UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)- Combine a b >>= k = Combine (a >>= k) (b >>= k)- Prefer a b >>= k = Prefer (a >>= k) (b >>= k)- Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)- Constructors a >>= k = Constructors (a >>= k)- Field a b >>= k = Field (a >>= k) b- Note a b >>= k = Note a (b >>= k)- Embed a >>= k = k a--instance Bifunctor Expr where- first _ (Const a ) = Const a- first _ (Var a ) = Var a- first k (Lam a b c ) = Lam a (first k b) (first k c)- first k (Pi a b c ) = Pi a (first k b) (first k c)- first k (App a b ) = App (first k a) (first k b)- first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d)- first k (Annot a b ) = Annot (first k a) (first k b)- first _ Bool = Bool- first _ (BoolLit a ) = BoolLit a- first k (BoolAnd a b ) = BoolAnd (first k a) (first k b)- first k (BoolOr a b ) = BoolOr (first k a) (first k b)- first k (BoolEQ a b ) = BoolEQ (first k a) (first k b)- first k (BoolNE a b ) = BoolNE (first k a) (first k b)- first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c)- first _ Natural = Natural- first _ (NaturalLit a ) = NaturalLit a- first _ NaturalFold = NaturalFold- first _ NaturalBuild = NaturalBuild- first _ NaturalIsZero = NaturalIsZero- first _ NaturalEven = NaturalEven- first _ NaturalOdd = NaturalOdd- first _ NaturalToInteger = NaturalToInteger- first _ NaturalShow = NaturalShow- first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)- first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b)- first _ Integer = Integer- first _ (IntegerLit a ) = IntegerLit a- first _ IntegerShow = IntegerShow- first _ Double = Double- first _ (DoubleLit a ) = DoubleLit a- first _ DoubleShow = DoubleShow- first _ Text = Text- first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b)- first k (TextAppend a b ) = TextAppend (first k a) (first k b)- first _ List = List- first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b)- first k (ListAppend a b ) = ListAppend (first k a) (first k b)- first _ ListBuild = ListBuild- first _ ListFold = ListFold- first _ ListLength = ListLength- first _ ListHead = ListHead- first _ ListLast = ListLast- first _ ListIndexed = ListIndexed- first _ ListReverse = ListReverse- first _ Optional = Optional- first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)- first _ OptionalFold = OptionalFold- first _ OptionalBuild = OptionalBuild- first k (Record a ) = Record (fmap (first k) a)- first k (RecordLit a ) = RecordLit (fmap (first k) a)- first k (Union a ) = Union (fmap (first k) a)- first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c)- first k (Combine a b ) = Combine (first k a) (first k b)- first k (Prefer a b ) = Prefer (first k a) (first k b)- first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c)- first k (Constructors a ) = Constructors (first k a)- first k (Field a b ) = Field (first k a) b- first k (Note a b ) = Note (k a) (first k b)- first _ (Embed a ) = Embed a-- second = fmap--instance IsString (Expr s a) where- fromString str = Var (fromString str)--data Chunks s a = Chunks [(Builder, Expr s a)] Builder- deriving (Functor, Foldable, Traversable, Show, Eq)--instance Monoid (Chunks s a) where- mempty = Chunks [] mempty-- mappend (Chunks xysL zL) (Chunks [] zR) =- Chunks xysL (zL <> zR)- mappend (Chunks xysL zL) (Chunks ((x, y):xysR) zR) =- Chunks (xysL ++ (zL <> x, y):xysR) zR--instance IsString (Chunks s a) where- fromString str = Chunks [] (fromString str)--{- There is a one-to-one correspondence between the builders in this section- and the sub-parsers in "Dhall.Parser". Each builder is named after the- corresponding parser and the relationship between builders exactly matches- the relationship between parsers. This leads to the nice emergent property- of automatically getting all the parentheses and precedences right.-- This approach has one major disadvantage: you can get an infinite loop if- you add a new constructor to the syntax tree without adding a matching- case the corresponding builder.--}--{-| Internal utility for pretty-printing, used when generating element lists- to supply to `enclose` or `enclose'`. This utility indicates that the- compact represent is the same as the multi-line representation for each- element--}-duplicate :: a -> (a, a)-duplicate x = (x, x)---- | Pretty-print a list-list :: [Doc ann] -> Doc ann-list [] = "[]"-list docs = enclose "[ " "[ " ", " ", " " ]" "]" (fmap duplicate docs)---- | Pretty-print union types and literals-angles :: [(Doc ann, Doc ann)] -> Doc ann-angles [] = "<>"-angles docs = enclose "< " "< " " | " "| " " >" ">" docs---- | Pretty-print record types and literals-braces :: [(Doc ann, Doc ann)] -> Doc ann-braces [] = "{}"-braces docs = enclose "{ " "{ " ", " ", " " }" "}" docs---- | Pretty-print anonymous functions and function types-arrows :: [(Doc ann, Doc ann)] -> Doc ann-arrows = enclose' "" " " " → " "→ " --{-| Format an expression that holds a variable number of elements, such as a- list, record, or union--}-enclose- :: Doc ann- -- ^ Beginning document for compact representation- -> Doc ann- -- ^ Beginning document for multi-line representation- -> Doc ann- -- ^ Separator for compact representation- -> Doc ann- -- ^ Separator for multi-line representation- -> Doc ann- -- ^ Ending document for compact representation- -> Doc ann- -- ^ Ending document for multi-line representation- -> [(Doc ann, Doc ann)]- -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@- -> Doc ann-enclose beginShort _ _ _ endShort _ [] =- beginShort <> endShort- where-enclose beginShort beginLong sepShort sepLong endShort endLong docs =- Pretty.group- (Pretty.flatAlt- (Pretty.align- (mconcat (zipWith combineLong (beginLong : repeat sepLong) docsLong) <> endLong)- )- (mconcat (zipWith combineShort (beginShort : repeat sepShort) docsShort) <> endShort)- )- where- docsShort = fmap fst docs-- docsLong = fmap snd docs-- combineLong x y = x <> y <> Pretty.hardline-- combineShort x y = x <> y--{-| Format an expression that holds a variable number of elements without a- trailing document such as nested `let`, nested lambdas, or nested `forall`s--}-enclose'- :: Doc ann- -- ^ Beginning document for compact representation- -> Doc ann- -- ^ Beginning document for multi-line representation- -> Doc ann- -- ^ Separator for compact representation- -> Doc ann- -- ^ Separator for multi-line representation- -> [(Doc ann, Doc ann)]- -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@- -> Doc ann-enclose' beginShort beginLong sepShort sepLong docs =- Pretty.group (Pretty.flatAlt long short)- where- longLines = zipWith (<>) (beginLong : repeat sepLong) docsLong-- long =- Pretty.align (mconcat (Data.List.intersperse Pretty.hardline longLines))-- short = mconcat (zipWith (<>) (beginShort : repeat sepShort) docsShort)-- docsShort = fmap fst docs-- docsLong = fmap snd docs--prettyLabel :: Text -> Doc ann-prettyLabel a =- if Data.HashSet.member a reservedIdentifiers || Text.any predicate a- then "`" <> Pretty.pretty a <> "`"- else Pretty.pretty a- where- predicate c = c == ':' || c == '.'--prettyNumber :: Integer -> Doc ann-prettyNumber = Pretty.pretty--prettyNatural :: Natural -> Doc ann-prettyNatural = Pretty.pretty--prettyDouble :: Double -> Doc ann-prettyDouble = Pretty.pretty--prettyChunks :: Pretty a => Chunks s a -> Doc ann-prettyChunks (Chunks a b) =- if any (\(builder, _) -> hasNewLine builder) a || hasNewLine b- then- Pretty.align- ( "''" <> Pretty.hardline- <> Pretty.align- (foldMap prettyMultilineChunk a <> prettyMultilineBuilder b)- <> "''"- )- else "\"" <> foldMap prettyChunk a <> prettyText b <> "\""- where- hasNewLine builder = Text.any (== '\n') lazyText- where- lazyText = Builder.toLazyText builder-- prettyMultilineChunk (c, d) =- prettyMultilineBuilder c <> "${" <> prettyExprA d <> "}"-- prettyMultilineBuilder builder = mconcat docs- where- lazyText = Builder.toLazyText (escapeSingleQuotedText builder)-- lazyLines = Text.splitOn "\n" lazyText-- docs =- Data.List.intersperse Pretty.hardline (fmap Pretty.pretty lazyLines)-- prettyChunk (c, d) = prettyText c <> "${" <> prettyExprA d <> "}"-- prettyText t = Pretty.pretty (Builder.toLazyText (escapeText t))--prettyConst :: Const -> Doc ann-prettyConst Type = "Type"-prettyConst Kind = "Kind"--prettyVar :: Var -> Doc ann-prettyVar (V x 0) = prettyLabel x-prettyVar (V x n) = prettyLabel x <> "@" <> prettyNumber n--prettyExprA :: Pretty a => Expr s a -> Doc ann-prettyExprA a0@(Annot _ _) =- enclose' "" " " " : " ": " (fmap duplicate (docs a0))- where- docs (Annot a b) = prettyExprB a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprB b ]-prettyExprA (Note _ a) =- prettyExprA a-prettyExprA a0 =- prettyExprB a0--prettyExprB :: Pretty a => Expr s a -> Doc ann-prettyExprB a0@(Lam _ _ _) = arrows (fmap duplicate (docs a0))- where- docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c- where- long = "λ "- <> Pretty.align- ( "( "- <> prettyLabel a- <> Pretty.hardline- <> ": "- <> prettyExprA b- <> Pretty.hardline- <> ")"- )-- short = "λ("- <> prettyLabel a- <> " : "- <> prettyExprA b- <> ")"- docs (Note _ c) = docs c- docs c = [ prettyExprB c ]-prettyExprB a0@(BoolIf _ _ _) =- enclose' "" " " " else " (Pretty.hardline <> "else ") (fmap duplicate (docs a0))- where- docs (BoolIf a b c) =- Pretty.group (Pretty.flatAlt long short) : docs c- where- long =- Pretty.align- ( "if "- <> prettyExprA a- <> Pretty.hardline- <> "then "- <> prettyExprA b- )-- short = "if "- <> prettyExprA a- <> " then "- <> prettyExprA b- docs (Note _ c) = docs c- docs c = [ prettyExprB c ]-prettyExprB a0@(Pi _ _ _) =- arrows (fmap duplicate (docs a0))- where- docs (Pi "_" b c) = prettyExprC b : docs c- docs (Pi a b c) = Pretty.group (Pretty.flatAlt long short) : docs c- where- long = "∀ "- <> Pretty.align- ( "( "- <> prettyLabel a- <> Pretty.hardline- <> ": "- <> prettyExprA b- <> Pretty.hardline- <> ")"- )-- short = "∀("- <> prettyLabel a- <> " : "- <> prettyExprA b- <> ")"- docs (Note _ c) = docs c- docs c = [ prettyExprB c ]-prettyExprB a0@(Let _ _ _ _) =- enclose' "" " " " in " (Pretty.hardline <> "in ")- (fmap duplicate (docs a0))- where- docs (Let a Nothing c d) =- Pretty.group (Pretty.flatAlt long short) : docs d- where- long = "let "- <> Pretty.align- ( prettyLabel a- <> " ="- <> Pretty.hardline- <> " "- <> prettyExprA c- )-- short = "let "- <> prettyLabel a- <> " = "- <> prettyExprA c- docs (Let a (Just b) c d) =- Pretty.group (Pretty.flatAlt long short) : docs d- where- long = "let "- <> Pretty.align- ( prettyLabel a- <> Pretty.hardline- <> ": "- <> prettyExprA b- <> Pretty.hardline- <> "= "- <> prettyExprA c- )-- short = "let "- <> prettyLabel a- <> " : "- <> prettyExprA b- <> " = "- <> prettyExprA c- docs (Note _ d) =- docs d- docs d =- [ prettyExprB d ]-prettyExprB (ListLit Nothing b) =- list (map prettyExprA (Data.Vector.toList b))-prettyExprB (ListLit (Just a) b) =- list (map prettyExprA (Data.Vector.toList b))- <> " : "- <> prettyExprD (App List a)-prettyExprB (OptionalLit a b) =- list (map prettyExprA (Data.Vector.toList b))- <> " : "- <> prettyExprD (App Optional a)-prettyExprB (Merge a b (Just c)) =- Pretty.group (Pretty.flatAlt long short)- where- long =- Pretty.align- ( "merge"- <> Pretty.hardline- <> prettyExprE a- <> Pretty.hardline- <> prettyExprE b- <> Pretty.hardline- <> ": "- <> prettyExprD c- )-- short = "merge "- <> prettyExprE a- <> " "- <> prettyExprE b- <> " : "- <> prettyExprD c-prettyExprB (Merge a b Nothing) =- Pretty.group (Pretty.flatAlt long short)- where- long =- Pretty.align- ( "merge"- <> Pretty.hardline- <> prettyExprE a- <> Pretty.hardline- <> prettyExprE b- )-- short = "merge "- <> prettyExprE a- <> " "- <> prettyExprE b-prettyExprB (Note _ b) =- prettyExprB b-prettyExprB a =- prettyExprC a--prettyExprC :: Pretty a => Expr s a -> Doc ann-prettyExprC = prettyExprC0--prettyExprC0 :: Pretty a => Expr s a -> Doc ann-prettyExprC0 a0@(BoolOr _ _) =- enclose' "" " " " || " "|| " (fmap duplicate (docs a0))- where- docs (BoolOr a b) = prettyExprC1 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC1 b ]-prettyExprC0 (Note _ a) =- prettyExprC0 a-prettyExprC0 a0 =- prettyExprC1 a0--prettyExprC1 :: Pretty a => Expr s a -> Doc ann-prettyExprC1 a0@(TextAppend _ _) =- enclose' "" " " " ++ " "++ " (fmap duplicate (docs a0))- where- docs (TextAppend a b) = prettyExprC2 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC2 b ]-prettyExprC1 (Note _ a) =- prettyExprC1 a-prettyExprC1 a0 =- prettyExprC2 a0--prettyExprC2 :: Pretty a => Expr s a -> Doc ann-prettyExprC2 a0@(NaturalPlus _ _) =- enclose' "" " " " + " "+ " (fmap duplicate (docs a0))- where- docs (NaturalPlus a b) = prettyExprC3 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC3 b ]-prettyExprC2 (Note _ a) =- prettyExprC2 a-prettyExprC2 a0 =- prettyExprC3 a0--prettyExprC3 :: Pretty a => Expr s a -> Doc ann-prettyExprC3 a0@(ListAppend _ _) =- enclose' "" " " " # " "# " (fmap duplicate (docs a0))- where- docs (ListAppend a b) = prettyExprC4 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC4 b ]-prettyExprC3 (Note _ a) =- prettyExprC3 a-prettyExprC3 a0 =- prettyExprC4 a0--prettyExprC4 :: Pretty a => Expr s a -> Doc ann-prettyExprC4 a0@(BoolAnd _ _) =- enclose' "" " " " && " "&& " (fmap duplicate (docs a0))- where- docs (BoolAnd a b) = prettyExprC5 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC5 b ]-prettyExprC4 (Note _ a) =- prettyExprC4 a-prettyExprC4 a0 =- prettyExprC5 a0--prettyExprC5 :: Pretty a => Expr s a -> Doc ann-prettyExprC5 a0@(Combine _ _) =- enclose' "" " " " ∧ " "∧ " (fmap duplicate (docs a0))- where- docs (Combine a b) = prettyExprC6 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC6 b ]-prettyExprC5 (Note _ a) =- prettyExprC5 a-prettyExprC5 a0 =- prettyExprC6 a0--prettyExprC6 :: Pretty a => Expr s a -> Doc ann-prettyExprC6 a0@(Prefer _ _) =- enclose' "" " " " ⫽ " "⫽ " (fmap duplicate (docs a0))- where- docs (Prefer a b) = prettyExprC7 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC7 b ]-prettyExprC6 (Note _ a) =- prettyExprC6 a-prettyExprC6 a0 =- prettyExprC7 a0--prettyExprC7 :: Pretty a => Expr s a -> Doc ann-prettyExprC7 a0@(NaturalTimes _ _) =- enclose' "" " " " * " "* " (fmap duplicate (docs a0))- where- docs (NaturalTimes a b) = prettyExprC8 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC8 b ]-prettyExprC7 (Note _ a) =- prettyExprC7 a-prettyExprC7 a0 =- prettyExprC8 a0--prettyExprC8 :: Pretty a => Expr s a -> Doc ann-prettyExprC8 a0@(BoolEQ _ _) =- enclose' "" " " " == " "== " (fmap duplicate (docs a0))- where- docs (BoolEQ a b) = prettyExprC9 a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprC9 b ]-prettyExprC8 (Note _ a) =- prettyExprC8 a-prettyExprC8 a0 =- prettyExprC9 a0--prettyExprC9 :: Pretty a => Expr s a -> Doc ann-prettyExprC9 a0@(BoolNE _ _) =- enclose' "" " " " != " "!= " (fmap duplicate (docs a0))- where- docs (BoolNE a b) = prettyExprD a : docs b- docs (Note _ b) = docs b- docs b = [ prettyExprD b ]-prettyExprC9 (Note _ a) =- prettyExprC9 a-prettyExprC9 a0 =- prettyExprD a0--prettyExprD :: Pretty a => Expr s a -> Doc ann-prettyExprD a0 = case a0 of- App _ _ -> result- Constructors _ -> result- Note _ b -> prettyExprD b- _ -> prettyExprE a0- where- result = enclose' "" "" " " "" (fmap duplicate (reverse (docs a0)))-- docs (App a b) = prettyExprE b : docs a- docs (Constructors b) = [ prettyExprE b , "constructors" ]- docs (Note _ b) = docs b- docs b = [ prettyExprE b ]--prettyExprE :: Pretty a => Expr s a -> Doc ann-prettyExprE (Field a b) = prettyExprE a <> "." <> prettyLabel b-prettyExprE (Note _ b) = prettyExprE b-prettyExprE a = prettyExprF a--prettyExprF :: Pretty a => Expr s a -> Doc ann-prettyExprF (Var a) =- prettyVar a-prettyExprF (Const k) =- prettyConst k-prettyExprF Bool =- "Bool"-prettyExprF Natural =- "Natural"-prettyExprF NaturalFold =- "Natural/fold"-prettyExprF NaturalBuild =- "Natural/build"-prettyExprF NaturalIsZero =- "Natural/isZero"-prettyExprF NaturalEven =- "Natural/even"-prettyExprF NaturalOdd =- "Natural/odd"-prettyExprF NaturalToInteger =- "Natural/toInteger"-prettyExprF NaturalShow =- "Natural/show"-prettyExprF Integer =- "Integer"-prettyExprF IntegerShow =- "Integer/show"-prettyExprF Double =- "Double"-prettyExprF DoubleShow =- "Double/show"-prettyExprF Text =- "Text"-prettyExprF List =- "List"-prettyExprF ListBuild =- "List/build"-prettyExprF ListFold =- "List/fold"-prettyExprF ListLength =- "List/length"-prettyExprF ListHead =- "List/head"-prettyExprF ListLast =- "List/last"-prettyExprF ListIndexed =- "List/indexed"-prettyExprF ListReverse =- "List/reverse"-prettyExprF Optional =- "Optional"-prettyExprF OptionalFold =- "Optional/fold"-prettyExprF OptionalBuild =- "Optional/build"-prettyExprF (BoolLit True) =- "True"-prettyExprF (BoolLit False) =- "False"-prettyExprF (IntegerLit a) =- prettyNumber a-prettyExprF (NaturalLit a) =- "+" <> prettyNatural a-prettyExprF (DoubleLit a) =- prettyDouble a-prettyExprF (TextLit a) =- prettyChunks a-prettyExprF (Record a) =- prettyRecord a-prettyExprF (RecordLit a) =- prettyRecordLit a-prettyExprF (Union a) =- prettyUnion a-prettyExprF (UnionLit a b c) =- prettyUnionLit a b c-prettyExprF (ListLit Nothing b) =- list (map prettyExprA (Data.Vector.toList b))-prettyExprF (Embed a) =- Pretty.pretty a-prettyExprF (Note _ b) =- prettyExprF b-prettyExprF a =- Pretty.group (Pretty.flatAlt long short)- where- long = Pretty.align ("( " <> prettyExprA a <> Pretty.hardline <> ")")-- short = "(" <> prettyExprA a <> ")"--prettyKeyValue- :: Pretty a- => Doc ann- -> Int- -> (Text, Expr s a)- -> (Doc ann, Doc ann)-prettyKeyValue separator keyLength (key, value) =- ( prettyLabel key <> " " <> separator <> " " <> prettyExprA value- , Pretty.fill keyLength (prettyLabel key)- <> " "- <> separator- <> Pretty.group (Pretty.flatAlt long short)- )- where- long = Pretty.hardline <> " " <> prettyExprA value-- short = " " <> prettyExprA value--prettyRecord :: Pretty a => Map Text (Expr s a) -> Doc ann-prettyRecord a = braces (map adapt (Data.Map.toList a))- where- keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a)))-- adapt = prettyKeyValue ":" keyLength --prettyRecordLit :: Pretty a => Map Text (Expr s a) -> Doc ann-prettyRecordLit a- | Data.Map.null a = "{=}"- | otherwise = braces (map adapt (Data.Map.toList a))- where- keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a)))-- adapt = prettyKeyValue "=" keyLength--prettyUnion :: Pretty a => Map Text (Expr s a) -> Doc ann-prettyUnion a = angles (map adapt (Data.Map.toList a))- where- keyLength = fromIntegral (maximum (map Text.length (Data.Map.keys a)))-- adapt = prettyKeyValue ":" keyLength--prettyUnionLit :: Pretty a => Text -> Expr s a -> Map Text (Expr s a) -> Doc ann-prettyUnionLit a b c = angles (front : map adapt (Data.Map.toList c))- where- keyLength = fromIntegral (maximum (map Text.length (a : Data.Map.keys c)))-- front = prettyKeyValue "=" keyLength (a, b)-- adapt = prettyKeyValue ":" keyLength---- | Pretty-print a value-pretty :: Pretty a => a -> Text-pretty = Pretty.renderLazy . Pretty.layoutPretty options . Pretty.pretty- where- options = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }---- | Builder corresponding to the @label@ token in "Dhall.Parser"-buildLabel :: Text -> Builder-buildLabel label =- if Data.HashSet.member label reservedIdentifiers || Text.any predicate label- then "`" <> build label <> "`"- else build label- where- predicate c = c == ':' || c == '.'---- | Builder corresponding to the @number@ token in "Dhall.Parser"-buildNumber :: Integer -> Builder-buildNumber a = build (show a)---- | Builder corresponding to the @natural@ token in "Dhall.Parser"-buildNatural :: Natural -> Builder-buildNatural a = build (show a)---- | Builder corresponding to the @double@ token in "Dhall.Parser"-buildDouble :: Double -> Builder-buildDouble a = build (show a)---- | Builder corresponding to the @text@ token in "Dhall.Parser"-buildChunks :: Buildable a => Chunks s a -> Builder-buildChunks (Chunks a b) = "\"" <> foldMap buildChunk a <> escapeText b <> "\""- where- buildChunk (c, d) = escapeText c <> "${" <> buildExprA d <> "}"---- | Escape a `Builder` literal using Dhall's escaping rules for single-quoted--- @Text@-escapeSingleQuotedText :: Builder -> Builder-escapeSingleQuotedText inputBuilder = outputBuilder- where- inputText = Builder.toLazyText inputBuilder-- outputText = substitute "${" "''${" (substitute "''" "'''" inputText)-- outputBuilder = Builder.fromLazyText outputText-- substitute before after = Text.intercalate after . Text.splitOn before---- | Escape a `Builder` literal using Dhall's escaping rules------ Note that the result does not include surrounding quotes-escapeText :: Builder -> Builder-escapeText a = Builder.fromLazyText (Text.concatMap adapt text)- where- adapt c- | '\x20' <= c && c <= '\x21' = Text.singleton c- -- '\x22' == '"'- | '\x23' == c = Text.singleton c- -- '\x24' == '$'- | '\x25' <= c && c <= '\x5B' = Text.singleton c- -- '\x5C' == '\\'- | '\x5D' <= c && c <= '\x7F' = Text.singleton c- | c == '"' = "\\\""- | c == '$' = "\\$"- | c == '\\' = "\\\\"- | c == '\b' = "\\b"- | c == '\f' = "\\f"- | c == '\n' = "\\n"- | c == '\r' = "\\r"- | c == '\t' = "\\t"- | otherwise = "\\u" <> showDigits (Data.Char.ord c)-- showDigits r0 = Text.pack (map showDigit [q1, q2, q3, r3])- where- (q1, r1) = r0 `quotRem` 4096- (q2, r2) = r1 `quotRem` 256- (q3, r3) = r2 `quotRem` 16-- showDigit n- | n < 10 = Data.Char.chr (Data.Char.ord '0' + n)- | otherwise = Data.Char.chr (Data.Char.ord 'A' + n - 10)-- text = Builder.toLazyText a---- | Builder corresponding to the @expr@ parser in "Dhall.Parser"-buildExpr :: Buildable a => Expr s a -> Builder-buildExpr = buildExprA---- | Builder corresponding to the @exprA@ parser in "Dhall.Parser"-buildExprA :: Buildable a => Expr s a -> Builder-buildExprA (Annot a b) = buildExprB a <> " : " <> buildExprA b-buildExprA (Note _ b) = buildExprA b-buildExprA a = buildExprB a---- | Builder corresponding to the @exprB@ parser in "Dhall.Parser"-buildExprB :: Buildable a => Expr s a -> Builder-buildExprB (Lam a b c) =- "λ("- <> buildLabel a- <> " : "- <> buildExprA b- <> ") → "- <> buildExprB c-buildExprB (BoolIf a b c) =- "if "- <> buildExprA a- <> " then "- <> buildExprA b- <> " else "- <> buildExprA c-buildExprB (Pi "_" b c) =- buildExprC b- <> " → "- <> buildExprB c-buildExprB (Pi a b c) =- "∀("- <> buildLabel a- <> " : "- <> buildExprA b- <> ") → "- <> buildExprB c-buildExprB (Let a Nothing c d) =- "let "- <> buildLabel a- <> " = "- <> buildExprA c- <> " in "- <> buildExprB d-buildExprB (Let a (Just b) c d) =- "let "- <> buildLabel a- <> " : "- <> buildExprA b- <> " = "- <> buildExprA c- <> " in "- <> buildExprB d-buildExprB (ListLit Nothing b) =- "[" <> buildElems (Data.Vector.toList b) <> "]"-buildExprB (ListLit (Just a) b) =- "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a-buildExprB (OptionalLit a b) =- "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a-buildExprB (Merge a b (Just c)) =- "merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c-buildExprB (Merge a b Nothing) =- "merge " <> buildExprE a <> " " <> buildExprE b-buildExprB (Note _ b) =- buildExprB b-buildExprB a =- buildExprC a---- | Builder corresponding to the @exprC@ parser in "Dhall.Parser"-buildExprC :: Buildable a => Expr s a -> Builder-buildExprC = buildExprC0---- | Builder corresponding to the @exprC0@ parser in "Dhall.Parser"-buildExprC0 :: Buildable a => Expr s a -> Builder-buildExprC0 (BoolOr a b) = buildExprC1 a <> " || " <> buildExprC0 b-buildExprC0 (Note _ b) = buildExprC0 b-buildExprC0 a = buildExprC1 a---- | Builder corresponding to the @exprC1@ parser in "Dhall.Parser"-buildExprC1 :: Buildable a => Expr s a -> Builder-buildExprC1 (TextAppend a b) = buildExprC2 a <> " ++ " <> buildExprC1 b-buildExprC1 (Note _ b) = buildExprC1 b-buildExprC1 a = buildExprC2 a---- | Builder corresponding to the @exprC2@ parser in "Dhall.Parser"-buildExprC2 :: Buildable a => Expr s a -> Builder-buildExprC2 (NaturalPlus a b) = buildExprC3 a <> " + " <> buildExprC2 b-buildExprC2 (Note _ b) = buildExprC2 b-buildExprC2 a = buildExprC3 a---- | Builder corresponding to the @exprC3@ parser in "Dhall.Parser"-buildExprC3 :: Buildable a => Expr s a -> Builder-buildExprC3 (ListAppend a b) = buildExprC4 a <> " # " <> buildExprC3 b-buildExprC3 (Note _ b) = buildExprC3 b-buildExprC3 a = buildExprC4 a---- | Builder corresponding to the @exprC4@ parser in "Dhall.Parser"-buildExprC4 :: Buildable a => Expr s a -> Builder-buildExprC4 (BoolAnd a b) = buildExprC5 a <> " && " <> buildExprC4 b-buildExprC4 (Note _ b) = buildExprC4 b-buildExprC4 a = buildExprC5 a---- | Builder corresponding to the @exprC5@ parser in "Dhall.Parser"-buildExprC5 :: Buildable a => Expr s a -> Builder-buildExprC5 (Combine a b) = buildExprC6 a <> " ∧ " <> buildExprC5 b-buildExprC5 (Note _ b) = buildExprC5 b-buildExprC5 a = buildExprC6 a---- | Builder corresponding to the @exprC6@ parser in "Dhall.Parser"-buildExprC6 :: Buildable a => Expr s a -> Builder-buildExprC6 (Prefer a b) = buildExprC7 a <> " ⫽ " <> buildExprC6 b-buildExprC6 (Note _ b) = buildExprC6 b-buildExprC6 a = buildExprC7 a---- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser"-buildExprC7 :: Buildable a => Expr s a -> Builder-buildExprC7 (NaturalTimes a b) = buildExprC8 a <> " * " <> buildExprC7 b-buildExprC7 (Note _ b) = buildExprC7 b-buildExprC7 a = buildExprC8 a---- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser"-buildExprC8 :: Buildable a => Expr s a -> Builder-buildExprC8 (BoolEQ a b) = buildExprC9 a <> " == " <> buildExprC8 b-buildExprC8 (Note _ b) = buildExprC8 b-buildExprC8 a = buildExprC9 a---- | Builder corresponding to the @exprC9@ parser in "Dhall.Parser"-buildExprC9 :: Buildable a => Expr s a -> Builder-buildExprC9 (BoolNE a b) = buildExprD a <> " != " <> buildExprC9 b-buildExprC9 (Note _ b) = buildExprC9 b-buildExprC9 a = buildExprD a---- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"-buildExprD :: Buildable a => Expr s a -> Builder-buildExprD (App a b) = buildExprD a <> " " <> buildExprE b-buildExprD (Constructors b) = "constructors " <> buildExprE b-buildExprD (Note _ b) = buildExprD b-buildExprD a = buildExprE a---- | Builder corresponding to the @exprE@ parser in "Dhall.Parser"-buildExprE :: Buildable a => Expr s a -> Builder-buildExprE (Field a b) = buildExprE a <> "." <> buildLabel b-buildExprE (Note _ b) = buildExprE b-buildExprE a = buildExprF a---- | Builder corresponding to the @exprF@ parser in "Dhall.Parser"-buildExprF :: Buildable a => Expr s a -> Builder-buildExprF (Var a) =- buildVar a-buildExprF (Const k) =- buildConst k-buildExprF Bool =- "Bool"-buildExprF Natural =- "Natural"-buildExprF NaturalFold =- "Natural/fold"-buildExprF NaturalBuild =- "Natural/build"-buildExprF NaturalIsZero =- "Natural/isZero"-buildExprF NaturalEven =- "Natural/even"-buildExprF NaturalOdd =- "Natural/odd"-buildExprF NaturalToInteger =- "Natural/toInteger"-buildExprF NaturalShow =- "Natural/show"-buildExprF Integer =- "Integer"-buildExprF IntegerShow =- "Integer/show"-buildExprF Double =- "Double"-buildExprF DoubleShow =- "Double/show"-buildExprF Text =- "Text"-buildExprF List =- "List"-buildExprF ListBuild =- "List/build"-buildExprF ListFold =- "List/fold"-buildExprF ListLength =- "List/length"-buildExprF ListHead =- "List/head"-buildExprF ListLast =- "List/last"-buildExprF ListIndexed =- "List/indexed"-buildExprF ListReverse =- "List/reverse"-buildExprF Optional =- "Optional"-buildExprF OptionalFold =- "Optional/fold"-buildExprF OptionalBuild =- "Optional/build"-buildExprF (BoolLit True) =- "True"-buildExprF (BoolLit False) =- "False"-buildExprF (IntegerLit a) =- buildNumber a-buildExprF (NaturalLit a) =- "+" <> buildNatural a-buildExprF (DoubleLit a) =- buildDouble a-buildExprF (TextLit a) =- buildChunks a-buildExprF (Record a) =- buildRecord a-buildExprF (RecordLit a) =- buildRecordLit a-buildExprF (Union a) =- buildUnion a-buildExprF (UnionLit a b c) =- buildUnionLit a b c-buildExprF (ListLit Nothing b) =- "[" <> buildElems (Data.Vector.toList b) <> "]"-buildExprF (Embed a) =- build a-buildExprF (Note _ b) =- buildExprF b-buildExprF a =- "(" <> buildExprA a <> ")"---- | Builder corresponding to the @const@ parser in "Dhall.Parser"-buildConst :: Const -> Builder-buildConst Type = "Type"-buildConst Kind = "Kind"---- | Builder corresponding to the @var@ parser in "Dhall.Parser"-buildVar :: Var -> Builder-buildVar (V x 0) = buildLabel x-buildVar (V x n) = buildLabel x <> "@" <> buildNumber n---- | Builder corresponding to the @elems@ parser in "Dhall.Parser"-buildElems :: Buildable a => [Expr s a] -> Builder-buildElems [] = ""-buildElems [a] = buildExprA a-buildElems (a:bs) = buildExprA a <> ", " <> buildElems bs---- | Builder corresponding to the @recordLit@ parser in "Dhall.Parser"-buildRecordLit :: Buildable a => Map Text (Expr s a) -> Builder-buildRecordLit a | Data.Map.null a =- "{=}"-buildRecordLit a =- "{ " <> buildFieldValues (Data.Map.toList a) <> " }"---- | Builder corresponding to the @fieldValues@ parser in "Dhall.Parser"-buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder-buildFieldValues [] = ""-buildFieldValues [a] = buildFieldValue a-buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs---- | Builder corresponding to the @fieldValue@ parser in "Dhall.Parser"-buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder-buildFieldValue (a, b) = buildLabel a <> " = " <> buildExprA b---- | Builder corresponding to the @record@ parser in "Dhall.Parser"-buildRecord :: Buildable a => Map Text (Expr s a) -> Builder-buildRecord a | Data.Map.null a =- "{}"-buildRecord a =- "{ " <> buildFieldTypes (Data.Map.toList a) <> " }"---- | Builder corresponding to the @fieldTypes@ parser in "Dhall.Parser"-buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder-buildFieldTypes [] = ""-buildFieldTypes [a] = buildFieldType a-buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs---- | Builder corresponding to the @fieldType@ parser in "Dhall.Parser"-buildFieldType :: Buildable a => (Text, Expr s a) -> Builder-buildFieldType (a, b) = buildLabel a <> " : " <> buildExprA b---- | Builder corresponding to the @union@ parser in "Dhall.Parser"-buildUnion :: Buildable a => Map Text (Expr s a) -> Builder-buildUnion a | Data.Map.null a =- "<>"-buildUnion a =- "< " <> buildAlternativeTypes (Data.Map.toList a) <> " >"---- | Builder corresponding to the @alternativeTypes@ parser in "Dhall.Parser"-buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder-buildAlternativeTypes [] =- ""-buildAlternativeTypes [a] =- buildAlternativeType a-buildAlternativeTypes (a:bs) =- buildAlternativeType a <> " | " <> buildAlternativeTypes bs---- | Builder corresponding to the @alternativeType@ parser in "Dhall.Parser"-buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder-buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExprA b---- | Builder corresponding to the @unionLit@ parser in "Dhall.Parser"-buildUnionLit- :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder-buildUnionLit a b c- | Data.Map.null c =- "< "- <> buildLabel a- <> " = "- <> buildExprA b- <> " >"- | otherwise =- "< "- <> buildLabel a- <> " = "- <> buildExprA b- <> " | "- <> buildAlternativeTypes (Data.Map.toList c)- <> " >"---- | Generates a syntactically valid Dhall program-instance Buildable a => Buildable (Expr s a) where- build = buildExpr--instance Pretty a => Pretty (Expr s a) where- pretty = prettyExprA--{-| `shift` is used by both normalization and type-checking to avoid variable- capture by shifting variable indices-- For example, suppose that you were to normalize the following expression:--> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x-- If you were to substitute @y@ with @x@ without shifting any variable- indices, then you would get the following incorrect result:--> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form-- In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in- order to avoid being misinterpreted as the @x@ bound by the innermost- lambda. If we perform that `shift` then we get the correct result:--> λ(a : Type) → λ(x : a) → λ(x : a) → x@1-- As a more worked example, suppose that you were to normalize the following- expression:--> λ(a : Type)-> → λ(f : a → a → a)-> → λ(x : a)-> → λ(x : a)-> → (λ(x : a) → f x x@1) x@1-- The correct normalized result would be:--> λ(a : Type)-> → λ(f : a → a → a)-> → λ(x : a)-> → λ(x : a)-> → f x@1 x-- The above example illustrates how we need to both increase and decrease- variable indices as part of substitution:-- * We need to increase the index of the outer @x\@1@ to @x\@2@ before we- substitute it into the body of the innermost lambda expression in order- to avoid variable capture. This substitution changes the body of the- lambda expression to @(f x\@2 x\@1)@-- * We then remove the innermost lambda and therefore decrease the indices of- both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one- less @x@ variable is now bound within that scope-- Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to- the indices of all variables named @x@ whose indices are greater than- @(n + m)@, where @m@ is the number of bound variables of the same name- within that scope-- In practice, @d@ is always @1@ or @-1@ because we either:-- * increment variables by @1@ to avoid variable capture during substitution- * decrement variables by @1@ when deleting lambdas after substitution-- @n@ starts off at @0@ when substitution begins and increments every time we- descend into a lambda or let expression that binds a variable of the same- name in order to avoid shifting the bound variables by mistake.--}-shift :: Integer -> Var -> Expr s a -> Expr s a-shift _ _ (Const a) = Const a-shift d (V x n) (Var (V x' n')) = Var (V x' n'')- where- n'' = if x == x' && n <= n' then n' + d else n'-shift d (V x n) (Lam x' _A b) = Lam x' _A' b'- where- _A' = shift d (V x n ) _A- b' = shift d (V x n') b- where- n' = if x == x' then n + 1 else n-shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'- where- _A' = shift d (V x n ) _A- _B' = shift d (V x n') _B- where- n' = if x == x' then n + 1 else n-shift d v (App f a) = App f' a'- where- f' = shift d v f- a' = shift d v a-shift d (V x n) (Let f mt r e) = Let f mt' r' e'- where- e' = shift d (V x n') e- where- n' = if x == f then n + 1 else n-- mt' = fmap (shift d (V x n)) mt- r' = shift d (V x n) r-shift d v (Annot a b) = Annot a' b'- where- a' = shift d v a- b' = shift d v b-shift _ _ Bool = Bool-shift _ _ (BoolLit a) = BoolLit a-shift d v (BoolAnd a b) = BoolAnd a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (BoolOr a b) = BoolOr a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (BoolEQ a b) = BoolEQ a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (BoolNE a b) = BoolNE a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (BoolIf a b c) = BoolIf a' b' c'- where- a' = shift d v a- b' = shift d v b- c' = shift d v c-shift _ _ Natural = Natural-shift _ _ (NaturalLit a) = NaturalLit a-shift _ _ NaturalFold = NaturalFold-shift _ _ NaturalBuild = NaturalBuild-shift _ _ NaturalIsZero = NaturalIsZero-shift _ _ NaturalEven = NaturalEven-shift _ _ NaturalOdd = NaturalOdd-shift _ _ NaturalToInteger = NaturalToInteger-shift _ _ NaturalShow = NaturalShow-shift d v (NaturalPlus a b) = NaturalPlus a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (NaturalTimes a b) = NaturalTimes a' b'- where- a' = shift d v a- b' = shift d v b-shift _ _ Integer = Integer-shift _ _ (IntegerLit a) = IntegerLit a-shift _ _ IntegerShow = IntegerShow-shift _ _ Double = Double-shift _ _ (DoubleLit a) = DoubleLit a-shift _ _ DoubleShow = DoubleShow-shift _ _ Text = Text-shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b)- where- a' = fmap (fmap (shift d v)) a-shift d v (TextAppend a b) = TextAppend a' b'- where- a' = shift d v a- b' = shift d v b-shift _ _ List = List-shift d v (ListLit a b) = ListLit a' b'- where- a' = fmap (shift d v) a- b' = fmap (shift d v) b-shift _ _ ListBuild = ListBuild-shift d v (ListAppend a b) = ListAppend a' b'- where- a' = shift d v a- b' = shift d v b-shift _ _ ListFold = ListFold-shift _ _ ListLength = ListLength-shift _ _ ListHead = ListHead-shift _ _ ListLast = ListLast-shift _ _ ListIndexed = ListIndexed-shift _ _ ListReverse = ListReverse-shift _ _ Optional = Optional-shift d v (OptionalLit a b) = OptionalLit a' b'- where- a' = shift d v a- b' = fmap (shift d v) b-shift _ _ OptionalFold = OptionalFold-shift _ _ OptionalBuild = OptionalBuild-shift d v (Record a) = Record a'- where- a' = fmap (shift d v) a-shift d v (RecordLit a) = RecordLit a'- where- a' = fmap (shift d v) a-shift d v (Union a) = Union a'- where- a' = fmap (shift d v) a-shift d v (UnionLit a b c) = UnionLit a b' c'- where- b' = shift d v b- c' = fmap (shift d v) c-shift d v (Combine a b) = Combine a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (Prefer a b) = Prefer a' b'- where- a' = shift d v a- b' = shift d v b-shift d v (Merge a b c) = Merge a' b' c'- where- a' = shift d v a- b' = shift d v b- c' = fmap (shift d v) c-shift d v (Constructors a) = Constructors a'- where- a' = shift d v a-shift d v (Field a b) = Field a' b- where- a' = shift d v a-shift d v (Note a b) = Note a b'- where- b' = shift d v b--- The Dhall compiler enforces that all embedded values are closed expressions--- and `shift` does nothing to a closed expression-shift _ _ (Embed p) = Embed p--{-| Substitute all occurrences of a variable with an expression--> subst x C B ~ B[x := C]--}-subst :: Var -> Expr s a -> Expr s a -> Expr s a-subst _ _ (Const a) = Const a-subst (V x n) e (Lam y _A b) = Lam y _A' b'- where- _A' = subst (V x n ) e _A- b' = subst (V x n') (shift 1 (V y 0) e) b- n' = if x == y then n + 1 else n-subst (V x n) e (Pi y _A _B) = Pi y _A' _B'- where- _A' = subst (V x n ) e _A- _B' = subst (V x n') (shift 1 (V y 0) e) _B- n' = if x == y then n + 1 else n-subst v e (App f a) = App f' a'- where- f' = subst v e f- a' = subst v e a-subst v e (Var v') = if v == v' then e else Var v'-subst (V x n) e (Let f mt r b) = Let f mt' r' b'- where- b' = subst (V x n') (shift 1 (V f 0) e) b- where- n' = if x == f then n + 1 else n-- mt' = fmap (subst (V x n) e) mt- r' = subst (V x n) e r-subst x e (Annot a b) = Annot a' b'- where- a' = subst x e a- b' = subst x e b-subst _ _ Bool = Bool-subst _ _ (BoolLit a) = BoolLit a-subst x e (BoolAnd a b) = BoolAnd a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (BoolOr a b) = BoolOr a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (BoolEQ a b) = BoolEQ a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (BoolNE a b) = BoolNE a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (BoolIf a b c) = BoolIf a' b' c'- where- a' = subst x e a- b' = subst x e b- c' = subst x e c-subst _ _ Natural = Natural-subst _ _ (NaturalLit a) = NaturalLit a-subst _ _ NaturalFold = NaturalFold-subst _ _ NaturalBuild = NaturalBuild-subst _ _ NaturalIsZero = NaturalIsZero-subst _ _ NaturalEven = NaturalEven-subst _ _ NaturalOdd = NaturalOdd-subst _ _ NaturalToInteger = NaturalToInteger-subst _ _ NaturalShow = NaturalShow-subst x e (NaturalPlus a b) = NaturalPlus a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (NaturalTimes a b) = NaturalTimes a' b'- where- a' = subst x e a- b' = subst x e b-subst _ _ Integer = Integer-subst _ _ (IntegerLit a) = IntegerLit a-subst _ _ IntegerShow = IntegerShow-subst _ _ Double = Double-subst _ _ (DoubleLit a) = DoubleLit a-subst _ _ DoubleShow = DoubleShow-subst _ _ Text = Text-subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b)- where- a' = fmap (fmap (subst x e)) a-subst x e (TextAppend a b) = TextAppend a' b'- where- a' = subst x e a- b' = subst x e b-subst _ _ List = List-subst x e (ListLit a b) = ListLit a' b'- where- a' = fmap (subst x e) a- b' = fmap (subst x e) b-subst x e (ListAppend a b) = ListAppend a' b'- where- a' = subst x e a- b' = subst x e b-subst _ _ ListBuild = ListBuild-subst _ _ ListFold = ListFold-subst _ _ ListLength = ListLength-subst _ _ ListHead = ListHead-subst _ _ ListLast = ListLast-subst _ _ ListIndexed = ListIndexed-subst _ _ ListReverse = ListReverse-subst _ _ Optional = Optional-subst x e (OptionalLit a b) = OptionalLit a' b'- where- a' = subst x e a- b' = fmap (subst x e) b-subst _ _ OptionalFold = OptionalFold-subst _ _ OptionalBuild = OptionalBuild-subst x e (Record kts) = Record (fmap (subst x e) kts)-subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs)-subst x e (Union kts) = Union (fmap (subst x e) kts)-subst x e (UnionLit a b kts) = UnionLit a (subst x e b) (fmap (subst x e) kts)-subst x e (Combine a b) = Combine a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (Prefer a b) = Prefer a' b'- where- a' = subst x e a- b' = subst x e b-subst x e (Merge a b c) = Merge a' b' c'- where- a' = subst x e a- b' = subst x e b- c' = fmap (subst x e) c-subst x e (Constructors a) = Constructors a'- where- a' = subst x e a-subst x e (Field a b) = Field a' b- where- a' = subst x e a-subst x e (Note a b) = Note a b'- where- b' = subst x e b--- The Dhall compiler enforces that all embedded values are closed expressions--- and `subst` does nothing to a closed expression-subst _ _ (Embed p) = Embed p--{-| Reduce an expression to its normal form, performing beta reduction-- `normalize` does not type-check the expression. You may want to type-check- expressions before normalizing them since normalization can convert an- ill-typed expression into a well-typed expression.-- However, `normalize` will not fail if the expression is ill-typed and will- leave ill-typed sub-expressions unevaluated.--}-normalize :: Expr s a -> Expr t a-normalize = normalizeWith (const Nothing)--{-| This function is used to determine whether folds like @Natural/fold@ or- @List/fold@ should be lazy or strict in their accumulator based on the type- of the accumulator-- If this function returns `True`, then they will be strict in their- accumulator since we can guarantee an upper bound on the amount of work to- normalize the accumulator on each step of the loop. If this function- returns `False` then they will be lazy in their accumulator and only- normalize the final result at the end of the fold--}-boundedType :: Expr s a -> Bool-boundedType Bool = True-boundedType Natural = True-boundedType Integer = True-boundedType Double = True-boundedType Text = True-boundedType (App List _) = False-boundedType (App Optional t) = boundedType t-boundedType (Record kvs) = all boundedType kvs-boundedType (Union kvs) = all boundedType kvs-boundedType _ = False---- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)-denote :: Expr s a -> Expr t a-denote (Note _ b ) = denote b-denote (Const a ) = Const a-denote (Var a ) = Var a-denote (Lam a b c ) = Lam a (denote b) (denote c)-denote (Pi a b c ) = Pi a (denote b) (denote c)-denote (App a b ) = App (denote a) (denote b)-denote (Let a b c d ) = Let a (fmap denote b) (denote c) (denote d)-denote (Annot a b ) = Annot (denote a) (denote b)-denote Bool = Bool-denote (BoolLit a ) = BoolLit a-denote (BoolAnd a b ) = BoolAnd (denote a) (denote b)-denote (BoolOr a b ) = BoolOr (denote a) (denote b)-denote (BoolEQ a b ) = BoolEQ (denote a) (denote b)-denote (BoolNE a b ) = BoolNE (denote a) (denote b)-denote (BoolIf a b c ) = BoolIf (denote a) (denote b) (denote c)-denote Natural = Natural-denote (NaturalLit a ) = NaturalLit a-denote NaturalFold = NaturalFold-denote NaturalBuild = NaturalBuild-denote NaturalIsZero = NaturalIsZero-denote NaturalEven = NaturalEven-denote NaturalOdd = NaturalOdd-denote NaturalToInteger = NaturalToInteger-denote NaturalShow = NaturalShow-denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b)-denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b)-denote Integer = Integer-denote (IntegerLit a ) = IntegerLit a-denote IntegerShow = IntegerShow-denote Double = Double-denote (DoubleLit a ) = DoubleLit a-denote DoubleShow = DoubleShow-denote Text = Text-denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b)-denote (TextAppend a b ) = TextAppend (denote a) (denote b)-denote List = List-denote (ListLit a b ) = ListLit (fmap denote a) (fmap denote b)-denote (ListAppend a b ) = ListAppend (denote a) (denote b)-denote ListBuild = ListBuild-denote ListFold = ListFold-denote ListLength = ListLength-denote ListHead = ListHead-denote ListLast = ListLast-denote ListIndexed = ListIndexed-denote ListReverse = ListReverse-denote Optional = Optional-denote (OptionalLit a b ) = OptionalLit (denote a) (fmap denote b)-denote OptionalFold = OptionalFold-denote OptionalBuild = OptionalBuild-denote (Record a ) = Record (fmap denote a)-denote (RecordLit a ) = RecordLit (fmap denote a)-denote (Union a ) = Union (fmap denote a)-denote (UnionLit a b c ) = UnionLit a (denote b) (fmap denote c)-denote (Combine a b ) = Combine (denote a) (denote b)-denote (Prefer a b ) = Prefer (denote a) (denote b)-denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c)-denote (Constructors a ) = Constructors (denote a)-denote (Field a b ) = Field (denote a) b-denote (Embed a ) = Embed a--{-| Reduce an expression to its normal form, performing beta reduction and applying- any custom definitions.- - `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`- function allows typing of Dhall functions in a custom typing context whereas - `normalizeWith` allows evaluating Dhall expressions in a custom context. -- To be more precise `normalizeWith` applies the given normalizer when it finds an- application term that it cannot reduce by other means.-- Note that the context used in normalization will determine the properties of normalization.- That is, if the functions in custom context are not total then the Dhall language, evaluated- with those functions is not total either. - --}-normalizeWith :: Normalizer a -> Expr s a -> Expr t a-normalizeWith ctx e0 = loop (denote e0)- where- -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of- -- `loop`. In theory, this might change a failing repro case into- -- a successful one, but the risk of that is low enough to not warrant- -- the `Show` constraint. I care more about proving at the type level- -- that the @a@ and @s@ type parameters are never used- e'' = bimap (\_ -> ()) (\_ -> ()) e0-- text = "NormalizeWith.loop (" <> Data.Text.pack (show e'') <> ")"- loop e = case e of- Const k -> Const k- Var v -> Var v- Lam x _A b -> Lam x _A' b'- where- _A' = loop _A- b' = loop b- Pi x _A _B -> Pi x _A' _B'- where- _A' = loop _A- _B' = loop _B- App f a -> case loop f of- Lam x _A b -> loop b'' -- Beta reduce- where- a' = shift 1 (V x 0) a- b' = subst (V x 0) a' b- b'' = shift (-1) (V x 0) b'- f' -> case App f' a' of- -- fold/build fusion for `List`- App (App ListBuild _) (App (App ListFold _) e') -> loop e'- App (App ListFold _) (App (App ListBuild _) e') -> loop e'- -- fold/build fusion for `Natural`- App NaturalBuild (App NaturalFold e') -> loop e'- App NaturalFold (App NaturalBuild e') -> loop e'-- -- fold/build fusion for `Optional`- App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'- App (App OptionalFold _) (App (App OptionalBuild _) e') -> loop e'-- App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero ->- if boundedType (loop t) then strict else lazy- where- strict = strictLoop n0- lazy = loop ( lazyLoop n0)-- strictLoop !0 = loop zero- strictLoop !n = loop (App succ' (strictLoop (n - 1)))-- lazyLoop !0 = zero- lazyLoop !n = App succ' (lazyLoop (n - 1))- App NaturalBuild k- | check -> NaturalLit n- | otherwise -> App f' a'- where- labeled =- loop (App (App (App k Natural) "Succ") "Zero")-- n = go 0 labeled- where- go !m (App (Var "Succ") e') = go (m + 1) e'- go !m (Var "Zero") = m- go !_ _ = internalError text- check = go labeled- where- go (App (Var "Succ") e') = go e'- go (Var "Zero") = True- go _ = False- App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)- App NaturalEven (NaturalLit n) -> BoolLit (even n)- App NaturalOdd (NaturalLit n) -> BoolLit (odd n)- App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n)- App NaturalShow (NaturalLit n) ->- TextLit (Chunks [] ("+" <> buildNatural n))- App IntegerShow (IntegerLit n) ->- TextLit (Chunks [] (buildNumber n))- App DoubleShow (DoubleLit n) ->- TextLit (Chunks [] (buildDouble n))- App (App OptionalBuild t) k- | check -> OptionalLit t k'- | otherwise -> App f' a'- where- labeled = loop (App (App (App k (App Optional t)) "Just") "Nothing")-- k' = go labeled- where- go (App (Var "Just") e') = pure e'- go (Var "Nothing") = empty- go _ = internalError text- check = go labeled- where- go (App (Var "Just") _) = True- go (Var "Nothing") = True- go _ = False- App (App ListBuild t) k- | check -> ListLit (Just t) (buildVector k')- | otherwise -> App f' a'- where- labeled =- loop (App (App (App k (App List t)) "Cons") "Nil")-- k' cons nil = go labeled- where- go (App (App (Var "Cons") x) e') = cons x (go e')- go (Var "Nil") = nil- go _ = internalError text- check = go labeled- where- go (App (App (Var "Cons") _) e') = go e'- go (Var "Nil") = True- go _ = False- App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil ->- if boundedType (loop t) then strict else lazy- where- strict = Data.Vector.foldr strictCons strictNil xs- lazy = loop (Data.Vector.foldr lazyCons lazyNil xs)-- strictNil = loop nil- lazyNil = nil-- strictCons y ys = loop (App (App cons y) ys)- lazyCons y ys = App (App cons y) ys- App (App ListLength _) (ListLit _ ys) ->- NaturalLit (fromIntegral (Data.Vector.length ys))- App (App ListHead t) (ListLit _ ys) ->- loop (OptionalLit t (Data.Vector.take 1 ys))- App (App ListLast t) (ListLit _ ys) ->- loop (OptionalLit t y)- where- y = if Data.Vector.null ys- then Data.Vector.empty- else Data.Vector.singleton (Data.Vector.last ys)- App (App ListIndexed t) (ListLit _ xs) ->- loop (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs)))- where- t' = Record (Data.Map.fromList kts)- where- kts = [ ("index", Natural)- , ("value", t)- ]- adapt (n, x) = RecordLit (Data.Map.fromList kvs)- where- kvs = [ ("index", NaturalLit (fromIntegral n))- , ("value", x)- ]- App (App ListReverse t) (ListLit _ xs) ->- loop (ListLit (Just t) (Data.Vector.reverse xs))- App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->- loop (maybe nothing just' (toMaybe xs))- where- just' y = App just y- toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList- _ -> case ctx (App f' a') of- Nothing -> App f' a'- Just app' -> loop app'- where- a' = loop a- Let f _ r b -> loop b''- where- r' = shift 1 (V f 0) r- b' = subst (V f 0) r' b- b'' = shift (-1) (V f 0) b'- Annot x _ -> loop x- Bool -> Bool- BoolLit b -> BoolLit b- BoolAnd x y ->- case x' of- BoolLit xn ->- case y' of- BoolLit yn -> BoolLit (xn && yn)- _ -> BoolAnd x' y'- _ -> BoolAnd x' y'- where- x' = loop x- y' = loop y- BoolOr x y ->- case x' of- BoolLit xn ->- case y' of- BoolLit yn -> BoolLit (xn || yn)- _ -> BoolOr x' y'- _ -> BoolOr x' y'- where- x' = loop x- y' = loop y- BoolEQ x y ->- case x' of- BoolLit xn ->- case y' of- BoolLit yn -> BoolLit (xn == yn)- _ -> BoolEQ x' y'- _ -> BoolEQ x' y'- where- x' = loop x- y' = loop y- BoolNE x y ->- case x' of- BoolLit xn ->- case y' of- BoolLit yn -> BoolLit (xn /= yn)- _ -> BoolNE x' y'- _ -> BoolNE x' y'- where- x' = loop x- y' = loop y- BoolIf b true false -> case loop b of- BoolLit True -> true'- BoolLit False -> false'- b' -> BoolIf b' true' false'- where- true' = loop true- false' = loop false- Natural -> Natural- NaturalLit n -> NaturalLit n- NaturalFold -> NaturalFold- NaturalBuild -> NaturalBuild- NaturalIsZero -> NaturalIsZero- NaturalEven -> NaturalEven- NaturalOdd -> NaturalOdd- NaturalToInteger -> NaturalToInteger- NaturalShow -> NaturalShow- NaturalPlus x y ->- case x' of- NaturalLit xn ->- case y' of- NaturalLit yn -> NaturalLit (xn + yn)- _ -> NaturalPlus x' y'- _ -> NaturalPlus x' y'- where- x' = loop x- y' = loop y- NaturalTimes x y ->- case x' of- NaturalLit xn ->- case y' of- NaturalLit yn -> NaturalLit (xn * yn)- _ -> NaturalTimes x' y'- _ -> NaturalTimes x' y'- where- x' = loop x- y' = loop y- Integer -> Integer- IntegerLit n -> IntegerLit n- IntegerShow -> IntegerShow- Double -> Double- DoubleLit n -> DoubleLit n- DoubleShow -> DoubleShow- Text -> Text- TextLit (Chunks xys z) ->- case mconcat chunks of- Chunks [("", x)] "" -> x- c -> TextLit c- where- chunks = concatMap process xys ++ [Chunks [] z]-- process (x, y) = case loop y of- TextLit c -> [Chunks [] x, c]- y' -> [Chunks [(x, y')] mempty]- TextAppend x y ->- case x' of- TextLit xt ->- case y' of- TextLit yt -> TextLit (xt <> yt)- _ -> TextAppend x' y'- _ -> TextAppend x' y'- where- x' = loop x- y' = loop y- List -> List- ListLit t es -> ListLit t' es'- where- t' = fmap loop t- es' = fmap loop es- ListAppend x y ->- case x' of- ListLit t xs ->- case y' of- ListLit _ ys -> ListLit t (xs <> ys)- _ -> ListAppend x' y'- _ -> ListAppend x' y'- where- x' = loop x- y' = loop y- ListBuild -> ListBuild- ListFold -> ListFold- ListLength -> ListLength- ListHead -> ListHead- ListLast -> ListLast- ListIndexed -> ListIndexed- ListReverse -> ListReverse- Optional -> Optional- OptionalLit t es -> OptionalLit t' es'- where- t' = loop t- es' = fmap loop es- OptionalFold -> OptionalFold- OptionalBuild -> OptionalBuild- Record kts -> Record kts'- where- kts' = fmap loop kts- RecordLit kvs -> RecordLit kvs'- where- kvs' = fmap loop kvs- Union kts -> Union kts'- where- kts' = fmap loop kts- UnionLit k v kvs -> UnionLit k v' kvs'- where- v' = loop v- kvs' = fmap loop kvs- Combine x0 y0 ->- let combine x y = case x of- RecordLit kvsX -> case y of- RecordLit kvsY ->- let kvs = Data.Map.unionWith combine kvsX kvsY- in RecordLit (fmap loop kvs)- _ -> Combine x y- _ -> Combine x y- in combine (loop x0) (loop y0)- Prefer x y ->- case x' of- RecordLit kvsX ->- case y' of- RecordLit kvsY ->- RecordLit (fmap loop (Data.Map.union kvsY kvsX))- _ -> Prefer x' y'- _ -> Prefer x' y'- where- x' = loop x- y' = loop y- Merge x y t ->- case x' of- RecordLit kvsX ->- case y' of- UnionLit kY vY _ ->- case Data.Map.lookup kY kvsX of- Just vX -> loop (App vX vY)- Nothing -> Merge x' y' t'- _ -> Merge x' y' t'- _ -> Merge x' y' t'- where- x' = loop x- y' = loop y- t' = fmap loop t- Constructors t ->- case t' of- Union kts -> RecordLit kvs- where- kvs = Data.Map.mapWithKey adapt kts-- adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)- where- rest = Data.Map.delete k kts- _ -> Constructors t'- where- t' = loop t- Field r x ->- case loop r of- RecordLit kvs ->- case Data.Map.lookup x kvs of- Just v -> loop v- Nothing -> Field (RecordLit (fmap loop kvs)) x- r' -> Field r' x- Note _ e' -> loop e'- Embed a -> Embed a---- | Use this to wrap you embedded functions (see `normalizeWith`) to make them--- polymorphic enough to be used.-type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)---- | Check if an expression is in a normal form given a context of evaluation.--- Unlike `isNormalized`, this will fully normalize and traverse through the expression. --- --- It is much more efficient to use `isNormalized`.-isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool-isNormalizedWith ctx e = e == (normalizeWith ctx e)----- | Quickly check if an expression is in normal form-isNormalized :: Expr s a -> Bool-isNormalized e = case denote e of- Const _ -> True- Var _ -> True- Lam _ a b -> isNormalized a && isNormalized b- Pi _ a b -> isNormalized a && isNormalized b- App f a -> isNormalized f && isNormalized a && case App f a of- App (Lam _ _ _) _ -> False-- -- fold/build fusion for `List`- App (App ListBuild _) (App (App ListFold _) _) -> False- App (App ListFold _) (App (App ListBuild _) _) -> False-- -- fold/build fusion for `Natural`- App NaturalBuild (App NaturalFold _) -> False- App NaturalFold (App NaturalBuild _) -> False-- -- fold/build fusion for `Optional`- App (App OptionalBuild _) (App (App OptionalFold _) _) -> False- App (App OptionalFold _) (App (App OptionalBuild _) _) -> False-- App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False- App NaturalBuild k0 -> isNormalized k0 && not (check0 k0)- where- check0 (Lam _ _ (Lam succ _ (Lam zero _ k))) = check1 succ zero k- check0 _ = False-- check1 succ zero (App (Var (V succ' n)) k) =- succ == succ' && n == (if succ == zero then 1 else 0) && check1 succ zero k- check1 _ zero (Var (V zero' 0)) = zero == zero'- check1 _ _ _ = False- App NaturalIsZero (NaturalLit _) -> False- App NaturalEven (NaturalLit _) -> False- App NaturalOdd (NaturalLit _) -> False- App NaturalShow (NaturalLit _) -> False- App NaturalToInteger (NaturalLit _) -> False- App IntegerShow (IntegerLit _) -> False- App DoubleShow (DoubleLit _) -> False- App (App OptionalBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)- where- check0 (Lam _ _ (Lam just _ (Lam nothing _ k))) = check1 just nothing k- check0 _ = False-- check1 just nothing (App (Var (V just' n)) _) =- just == just' && n == (if just == nothing then 1 else 0)- check1 _ nothing (Var (V nothing' 0)) = nothing == nothing'- check1 _ _ _ = False- App (App ListBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)- where- check0 (Lam _ _ (Lam cons _ (Lam nil _ k))) = check1 cons nil k- check0 _ = False-- check1 cons nil (App (Var (V cons' n)) k) =- cons == cons' && n == (if cons == nil then 1 else 0) && check1 cons nil k- check1 _ nil (Var (V nil' 0)) = nil == nil'- check1 _ _ _ = False- App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->- False- App (App ListLength _) (ListLit _ _) -> False- App (App ListHead _) (ListLit _ _) -> False- App (App ListLast _) (ListLit _ _) -> False- App (App ListIndexed _) (ListLit _ _) -> False- App (App ListReverse _) (ListLit _ _) -> False- App (App (App (App (App OptionalFold _) (OptionalLit _ _)) _) _) _ ->- False- _ -> True- Let _ _ _ _ -> False- Annot _ _ -> False- Bool -> True- BoolLit _ -> True- BoolAnd x y -> isNormalized x && isNormalized y &&- case x of- BoolLit _ ->- case y of- BoolLit _ -> False- _ -> True- _ -> True- BoolOr x y -> isNormalized x && isNormalized y &&- case x of- BoolLit _ ->- case y of- BoolLit _ -> False- _ -> True- _ -> True- BoolEQ x y -> isNormalized x && isNormalized y &&- case x of- BoolLit _ ->- case y of- BoolLit _ -> False- _ -> True- _ -> True- BoolNE x y -> isNormalized x && isNormalized y &&- case x of- BoolLit _ ->- case y of- BoolLit _ -> False- _ -> True- _ -> True- BoolIf b true false -> isNormalized b && case b of- BoolLit _ -> False- _ -> isNormalized true && isNormalized false- Natural -> True- NaturalLit _ -> True- NaturalFold -> True- NaturalBuild -> True- NaturalIsZero -> True- NaturalEven -> True- NaturalOdd -> True- 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- Integer -> True- IntegerLit _ -> True- IntegerShow -> True- Double -> True- 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- 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- ListBuild -> True- ListFold -> True- ListLength -> True- ListHead -> True- ListLast -> True- ListIndexed -> True- ListReverse -> True- Optional -> True- OptionalLit t es -> isNormalized t && all isNormalized es- OptionalFold -> True- OptionalBuild -> True- Record kts -> all isNormalized kts- RecordLit kvs -> all isNormalized kvs- Union kts -> all isNormalized kts- UnionLit _ v kvs -> isNormalized v && all isNormalized kvs- Combine x y -> isNormalized x && isNormalized y && combine- where- combine = case x of- RecordLit _ -> case y of- RecordLit _ -> False- _ -> True- _ -> True- Prefer x y -> isNormalized x && isNormalized y && combine- where- combine = case x of- RecordLit _ -> case y of- RecordLit _ -> False- _ -> True- _ -> True- Merge x y t -> isNormalized x && isNormalized y && any isNormalized t &&- case x of- RecordLit kvsX ->- case y of- UnionLit kY _ _ ->- case Data.Map.lookup kY kvsX of- Just _ -> False- Nothing -> True- _ -> True- _ -> True- Constructors t -> isNormalized t &&- case t of- Union _ -> False- _ -> True- Field r x -> isNormalized r &&- case r of- RecordLit kvs ->- case Data.Map.lookup x kvs of- Just _ -> False- Nothing -> True- _ -> True- Note _ e' -> isNormalized e'- Embed _ -> True--_ERROR :: String-_ERROR = "\ESC[1;31mError\ESC[0m"--{-| Utility function used to throw internal errors that should never happen- (in theory) but that are not enforced by the type system--}-internalError :: Data.Text.Text -> forall b . b-internalError text = error (unlines- [ _ERROR <> ": Compiler bug "- , " "- , "Explanation: This error message means that there is a bug in the Dhall compiler."- , "You didn't do anything wrong, but if you would like to see this problem fixed "- , "then you should report the bug at: "- , " "- , "https://github.com/dhall-lang/dhall-haskell/issues "- , " "- , "Please include the following text in your bug report: "- , " "- , "``` "- , Data.Text.unpack text <> " "- , "``` "- ] )--buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a-buildVector f = Data.Vector.reverse (Data.Vector.create (do- let cons a st = do- (len, cap, mv) <- st- if len < cap- then do- Data.Vector.Mutable.write mv len a- return (len + 1, cap, mv)- else do- let cap' = 2 * cap- mv' <- Data.Vector.Mutable.unsafeGrow mv cap'- Data.Vector.Mutable.write mv' len a- return (len + 1, cap', mv')- let nil = do- mv <- Data.Vector.Mutable.unsafeNew 1- return (0, 1, mv)- (len, _, mv) <- f cons nil- return (Data.Vector.Mutable.slice 0 len mv) ))---- | The set of reserved identifiers for the Dhall language-reservedIdentifiers :: HashSet Text-reservedIdentifiers =- Data.HashSet.fromList- [ "let"- , "in"- , "Type"- , "Kind"- , "forall"- , "Bool"- , "True"- , "False"- , "merge"- , "if"- , "then"- , "else"- , "as"- , "using"- , "Natural"- , "Natural/fold"- , "Natural/build"- , "Natural/isZero"- , "Natural/even"- , "Natural/odd"- , "Natural/toInteger"- , "Natural/show"- , "Integer"- , "Integer/show"- , "Double"- , "Double/show"- , "Text"- , "List"- , "List/build"- , "List/fold"- , "List/length"- , "List/head"- , "List/last"- , "List/indexed"- , "List/reverse"- , "Optional"+import Data.HashMap.Strict.InsOrd (InsOrdHashMap)+import Data.HashSet (HashSet)+import Data.Monoid ((<>))+import Data.String (IsString(..))+import Data.Scientific (Scientific)+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+import Data.Text.Prettyprint.Doc (Pretty)+import Data.Traversable+import Data.Vector (Vector)+import {-# SOURCE #-} Dhall.Pretty.Internal+import Numeric.Natural (Natural)+import Prelude hiding (succ)++import qualified Control.Monad+import qualified Data.ByteString+import qualified Data.ByteString.Char8+import qualified Data.ByteString.Base16+import qualified Data.HashMap.Strict.InsOrd+import qualified Data.HashSet+import qualified Data.Maybe+import qualified Data.Text+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Vector+import qualified Data.Vector.Mutable++{-| Constants for a pure type system++ The only axiom is:++> ⊦ Type : Kind++ ... and the valid rule pairs are:++> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)+> ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions)+> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors)++ These are the same rule pairs as System Fω++ 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, Bounded, Enum)++instance Buildable Const where+ build = buildConst++-- | Whether or not a path is relative to the user's home directory+data HasHome = Home | Homeless deriving (Eq, Ord, Show)++-- | The type of path to import (i.e. local vs. remote vs. environment)+data PathType+ = File HasHome FilePath+ -- ^ Local path+ | URL Text (Maybe PathHashed)+ -- ^ URL of emote resource and optional headers stored in a path+ | Env Text+ -- ^ Environment variable+ deriving (Eq, Ord, Show)++instance Buildable PathType where+ build (File Home file)+ = "~/" <> build (Text.pack file)+ build (File Homeless file)+ | Text.isPrefixOf "./" txt+ || Text.isPrefixOf "/" txt+ || Text.isPrefixOf "../" txt+ = build txt <> " "+ | otherwise+ = "./" <> build txt <> " "+ where+ txt = Text.pack file+ build (URL str Nothing ) = build str <> " "+ build (URL str (Just headers)) = build str <> " using " <> build headers <> " "+ build (Env env) = "env:" <> build env++-- | How to interpret the path's contents (i.e. as Dhall code or raw text)+data PathMode = Code | RawText deriving (Eq, Ord, Show)++-- | A `PathType` extended with an optional hash for semantic integrity checks+data PathHashed = PathHashed+ { hash :: Maybe Data.ByteString.ByteString+ , pathType :: PathType+ } deriving (Eq, Ord, Show)++instance Buildable PathHashed where+ build (PathHashed Nothing p) = build p+ build (PathHashed (Just h) p) = build p <> "sha256:" <> build string <> " "+ where+ bytes = Data.ByteString.Base16.encode h++ string = Data.ByteString.Char8.unpack bytes++-- | Path to an external resource+data Path = Path+ { pathHashed :: PathHashed+ , pathMode :: PathMode+ } deriving (Eq, Ord, Show)++instance Buildable Path where+ build (Path {..}) = build pathHashed <> suffix+ where+ suffix = case pathMode of+ RawText -> "as Text"+ Code -> ""++instance Pretty Path where+ pretty path = Pretty.pretty (Builder.toLazyText (build path))++{-| Label for a bound variable++ The `Text` field is the variable's name (i.e. \"@x@\").++ The `Int` field disambiguates variables with the same name if there are+ multiple bound variables of the same name in scope. Zero refers to the+ nearest bound variable and the index increases by one for each bound+ variable of the same name going outward. The following diagram may help:++> ┌──refers to──┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0+>+> ┌─────────────────refers to─────────────────┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1++ This `Int` behaves like a De Bruijn index in the special case where all+ variables have the same name.++ You can optionally omit the index if it is @0@:++> ┌─refers to─┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x++ Zero indices are omitted when pretty-printing `Var`s and non-zero indices+ appear as a numeric suffix.+-}+data Var = V Text !Integer+ deriving (Eq, Show)++instance IsString Var where+ fromString str = V (fromString str) 0++instance Buildable Var where+ build = buildVar++-- | Syntax tree for expressions+data Expr s a+ -- | > Const c ~ c+ = Const Const+ -- | > Var (V x 0) ~ x+ -- > Var (V x n) ~ x@n+ | Var Var+ -- | > Lam x A b ~ λ(x : A) -> b+ | Lam Text (Expr s a) (Expr s a)+ -- | > Pi "_" A B ~ A -> B+ -- > Pi x A B ~ ∀(x : A) -> B+ | Pi Text (Expr s a) (Expr s a)+ -- | > App f a ~ f a+ | App (Expr s a) (Expr s a)+ -- | > Let x Nothing r e ~ let x = r in e+ -- > Let x (Just t) r e ~ let x : t = r in e+ | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)+ -- | > Annot x t ~ x : t+ | Annot (Expr s a) (Expr s a)+ -- | > Bool ~ Bool+ | Bool+ -- | > BoolLit b ~ b+ | BoolLit Bool+ -- | > BoolAnd x y ~ x && y+ | BoolAnd (Expr s a) (Expr s a)+ -- | > BoolOr x y ~ x || y+ | BoolOr (Expr s a) (Expr s a)+ -- | > BoolEQ x y ~ x == y+ | BoolEQ (Expr s a) (Expr s a)+ -- | > BoolNE x y ~ x != y+ | BoolNE (Expr s a) (Expr s a)+ -- | > BoolIf x y z ~ if x then y else z+ | BoolIf (Expr s a) (Expr s a) (Expr s a)+ -- | > Natural ~ Natural+ | Natural+ -- | > NaturalLit n ~ +n+ | NaturalLit Natural+ -- | > NaturalFold ~ Natural/fold+ | NaturalFold+ -- | > NaturalBuild ~ Natural/build+ | NaturalBuild+ -- | > NaturalIsZero ~ Natural/isZero+ | NaturalIsZero+ -- | > NaturalEven ~ Natural/even+ | NaturalEven+ -- | > NaturalOdd ~ Natural/odd+ | NaturalOdd+ -- | > NaturalToInteger ~ Natural/toInteger+ | NaturalToInteger+ -- | > NaturalShow ~ Natural/show+ | NaturalShow+ -- | > NaturalPlus x y ~ x + y+ | NaturalPlus (Expr s a) (Expr s a)+ -- | > NaturalTimes x y ~ x * y+ | NaturalTimes (Expr s a) (Expr s a)+ -- | > Integer ~ Integer+ | Integer+ -- | > IntegerLit n ~ n+ | IntegerLit Integer+ -- | > IntegerShow ~ Integer/show+ | IntegerShow+ -- | > Double ~ Double+ | Double+ -- | > DoubleLit n ~ n+ | DoubleLit Scientific+ -- | > DoubleShow ~ Double/show+ | DoubleShow+ -- | > Text ~ Text+ | Text+ -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3"+ | TextLit (Chunks s a)+ -- | > TextAppend x y ~ x ++ y+ | TextAppend (Expr s a) (Expr s a)+ -- | > List ~ List+ | List+ -- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t+ -- > ListLit Nothing [x, y, z] ~ [x, y, z]+ | ListLit (Maybe (Expr s a)) (Vector (Expr s a))+ -- | > ListAppend x y ~ x # y+ | ListAppend (Expr s a) (Expr s a)+ -- | > ListBuild ~ List/build+ | ListBuild+ -- | > ListFold ~ List/fold+ | ListFold+ -- | > ListLength ~ List/length+ | ListLength+ -- | > ListHead ~ List/head+ | ListHead+ -- | > ListLast ~ List/last+ | ListLast+ -- | > ListIndexed ~ List/indexed+ | ListIndexed+ -- | > ListReverse ~ List/reverse+ | ListReverse+ -- | > Optional ~ Optional+ | Optional+ -- | > OptionalLit t [e] ~ [e] : Optional t+ -- > OptionalLit t [] ~ [] : Optional t+ | OptionalLit (Expr s a) (Vector (Expr s a))+ -- | > OptionalFold ~ Optional/fold+ | OptionalFold+ -- | > OptionalBuild ~ Optional/build+ | OptionalBuild+ -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }+ | Record (InsOrdHashMap Text (Expr s a))+ -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }+ | RecordLit (InsOrdHashMap Text (Expr s a))+ -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1 | k2 : t2 >+ | Union (InsOrdHashMap Text (Expr s a))+ -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 >+ | UnionLit Text (Expr s a) (InsOrdHashMap Text (Expr s a))+ -- | > Combine x y ~ x ∧ y+ | Combine (Expr s a) (Expr s a)+ -- | > CombineRight x y ~ x ⫽ y+ | Prefer (Expr s a) (Expr s a)+ -- | > Merge x y (Just t ) ~ merge x y : t+ -- > Merge x y Nothing ~ merge x y+ | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))+ -- | > Constructors e ~ constructors e+ | Constructors (Expr s a)+ -- | > Field e x ~ e.x+ | Field (Expr s a) Text+ -- | > Note s x ~ e+ | Note s (Expr s a)+ -- | > Embed path ~ path+ | Embed a+ deriving (Functor, Foldable, Traversable, Show, Eq)++instance Applicative (Expr s) where+ pure = Embed++ (<*>) = Control.Monad.ap++instance Monad (Expr s) where+ return = pure++ Const a >>= _ = Const a+ Var a >>= _ = Var a+ Lam a b c >>= k = Lam a (b >>= k) (c >>= k)+ Pi a b c >>= k = Pi a (b >>= k) (c >>= k)+ App a b >>= k = App (a >>= k) (b >>= k)+ Let a b c d >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)+ Annot a b >>= k = Annot (a >>= k) (b >>= k)+ Bool >>= _ = Bool+ BoolLit a >>= _ = BoolLit a+ BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k)+ BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k)+ BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k)+ BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k)+ BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)+ Natural >>= _ = Natural+ NaturalLit a >>= _ = NaturalLit a+ NaturalFold >>= _ = NaturalFold+ NaturalBuild >>= _ = NaturalBuild+ NaturalIsZero >>= _ = NaturalIsZero+ NaturalEven >>= _ = NaturalEven+ NaturalOdd >>= _ = NaturalOdd+ NaturalToInteger >>= _ = NaturalToInteger+ NaturalShow >>= _ = NaturalShow+ NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k)+ NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)+ Integer >>= _ = Integer+ IntegerLit a >>= _ = IntegerLit a+ IntegerShow >>= _ = IntegerShow+ Double >>= _ = Double+ DoubleLit a >>= _ = DoubleLit a+ DoubleShow >>= _ = DoubleShow+ Text >>= _ = Text+ TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b)+ TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k)+ List >>= _ = List+ ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)+ ListAppend a b >>= k = ListAppend (a >>= k) (b >>= k)+ ListBuild >>= _ = ListBuild+ ListFold >>= _ = ListFold+ ListLength >>= _ = ListLength+ ListHead >>= _ = ListHead+ ListLast >>= _ = ListLast+ ListIndexed >>= _ = ListIndexed+ ListReverse >>= _ = ListReverse+ Optional >>= _ = Optional+ OptionalLit a b >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)+ OptionalFold >>= _ = OptionalFold+ OptionalBuild >>= _ = OptionalBuild+ Record a >>= k = Record (fmap (>>= k) a)+ RecordLit a >>= k = RecordLit (fmap (>>= k) a)+ Union a >>= k = Union (fmap (>>= k) a)+ UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)+ Combine a b >>= k = Combine (a >>= k) (b >>= k)+ Prefer a b >>= k = Prefer (a >>= k) (b >>= k)+ Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)+ Constructors a >>= k = Constructors (a >>= k)+ Field a b >>= k = Field (a >>= k) b+ Note a b >>= k = Note a (b >>= k)+ Embed a >>= k = k a++instance Bifunctor Expr where+ first _ (Const a ) = Const a+ first _ (Var a ) = Var a+ first k (Lam a b c ) = Lam a (first k b) (first k c)+ first k (Pi a b c ) = Pi a (first k b) (first k c)+ first k (App a b ) = App (first k a) (first k b)+ first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d)+ first k (Annot a b ) = Annot (first k a) (first k b)+ first _ Bool = Bool+ first _ (BoolLit a ) = BoolLit a+ first k (BoolAnd a b ) = BoolAnd (first k a) (first k b)+ first k (BoolOr a b ) = BoolOr (first k a) (first k b)+ first k (BoolEQ a b ) = BoolEQ (first k a) (first k b)+ first k (BoolNE a b ) = BoolNE (first k a) (first k b)+ first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c)+ first _ Natural = Natural+ first _ (NaturalLit a ) = NaturalLit a+ first _ NaturalFold = NaturalFold+ first _ NaturalBuild = NaturalBuild+ first _ NaturalIsZero = NaturalIsZero+ first _ NaturalEven = NaturalEven+ first _ NaturalOdd = NaturalOdd+ first _ NaturalToInteger = NaturalToInteger+ first _ NaturalShow = NaturalShow+ first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)+ first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b)+ first _ Integer = Integer+ first _ (IntegerLit a ) = IntegerLit a+ first _ IntegerShow = IntegerShow+ first _ Double = Double+ first _ (DoubleLit a ) = DoubleLit a+ first _ DoubleShow = DoubleShow+ first _ Text = Text+ first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b)+ first k (TextAppend a b ) = TextAppend (first k a) (first k b)+ first _ List = List+ first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b)+ first k (ListAppend a b ) = ListAppend (first k a) (first k b)+ first _ ListBuild = ListBuild+ first _ ListFold = ListFold+ first _ ListLength = ListLength+ first _ ListHead = ListHead+ first _ ListLast = ListLast+ first _ ListIndexed = ListIndexed+ first _ ListReverse = ListReverse+ first _ Optional = Optional+ first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)+ first _ OptionalFold = OptionalFold+ first _ OptionalBuild = OptionalBuild+ first k (Record a ) = Record (fmap (first k) a)+ first k (RecordLit a ) = RecordLit (fmap (first k) a)+ first k (Union a ) = Union (fmap (first k) a)+ first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c)+ first k (Combine a b ) = Combine (first k a) (first k b)+ first k (Prefer a b ) = Prefer (first k a) (first k b)+ first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c)+ first k (Constructors a ) = Constructors (first k a)+ first k (Field a b ) = Field (first k a) b+ first k (Note a b ) = Note (k a) (first k b)+ first _ (Embed a ) = Embed a++ second = fmap++instance IsString (Expr s a) where+ fromString str = Var (fromString str)++-- | The body of an interpolated @Text@ literal+data Chunks s a = Chunks [(Builder, Expr s a)] Builder+ deriving (Functor, Foldable, Traversable, Show, Eq)++instance Monoid (Chunks s a) where+ mempty = Chunks [] mempty++ mappend (Chunks xysL zL) (Chunks [] zR) =+ Chunks xysL (zL <> zR)+ mappend (Chunks xysL zL) (Chunks ((x, y):xysR) zR) =+ Chunks (xysL ++ (zL <> x, y):xysR) zR++instance IsString (Chunks s a) where+ fromString str = Chunks [] (fromString str)++{- There is a one-to-one correspondence between the builders in this section+ and the sub-parsers in "Dhall.Parser". Each builder is named after the+ corresponding parser and the relationship between builders exactly matches+ the relationship between parsers. This leads to the nice emergent property+ of automatically getting all the parentheses and precedences right.++ This approach has one major disadvantage: you can get an infinite loop if+ you add a new constructor to the syntax tree without adding a matching+ case the corresponding builder.+-}++-- | Generates a syntactically valid Dhall program+instance Buildable a => Buildable (Expr s a) where+ build = buildExpr++instance Pretty a => Pretty (Expr s a) where+ pretty = Pretty.unAnnotate . prettyExpr++{-| `shift` is used by both normalization and type-checking to avoid variable+ capture by shifting variable indices++ For example, suppose that you were to normalize the following expression:++> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x++ If you were to substitute @y@ with @x@ without shifting any variable+ indices, then you would get the following incorrect result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form++ In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in+ order to avoid being misinterpreted as the @x@ bound by the innermost+ lambda. If we perform that `shift` then we get the correct result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x@1++ As a more worked example, suppose that you were to normalize the following+ expression:++> λ(a : Type)+> → λ(f : a → a → a)+> → λ(x : a)+> → λ(x : a)+> → (λ(x : a) → f x x@1) x@1++ The correct normalized result would be:++> λ(a : Type)+> → λ(f : a → a → a)+> → λ(x : a)+> → λ(x : a)+> → f x@1 x++ The above example illustrates how we need to both increase and decrease+ variable indices as part of substitution:++ * We need to increase the index of the outer @x\@1@ to @x\@2@ before we+ substitute it into the body of the innermost lambda expression in order+ to avoid variable capture. This substitution changes the body of the+ lambda expression to @(f x\@2 x\@1)@++ * We then remove the innermost lambda and therefore decrease the indices of+ both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one+ less @x@ variable is now bound within that scope++ Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to+ the indices of all variables named @x@ whose indices are greater than+ @(n + m)@, where @m@ is the number of bound variables of the same name+ within that scope++ In practice, @d@ is always @1@ or @-1@ because we either:++ * increment variables by @1@ to avoid variable capture during substitution+ * decrement variables by @1@ when deleting lambdas after substitution++ @n@ starts off at @0@ when substitution begins and increments every time we+ descend into a lambda or let expression that binds a variable of the same+ name in order to avoid shifting the bound variables by mistake.+-}+shift :: Integer -> Var -> Expr s a -> Expr s a+shift _ _ (Const a) = Const a+shift d (V x n) (Var (V x' n')) = Var (V x' n'')+ where+ n'' = if x == x' && n <= n' then n' + d else n'+shift d (V x n) (Lam x' _A b) = Lam x' _A' b'+ where+ _A' = shift d (V x n ) _A+ b' = shift d (V x n') b+ where+ n' = if x == x' then n + 1 else n+shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'+ where+ _A' = shift d (V x n ) _A+ _B' = shift d (V x n') _B+ where+ n' = if x == x' then n + 1 else n+shift d v (App f a) = App f' a'+ where+ f' = shift d v f+ a' = shift d v a+shift d (V x n) (Let f mt r e) = Let f mt' r' e'+ where+ e' = shift d (V x n') e+ where+ n' = if x == f then n + 1 else n++ mt' = fmap (shift d (V x n)) mt+ r' = shift d (V x n) r+shift d v (Annot a b) = Annot a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ Bool = Bool+shift _ _ (BoolLit a) = BoolLit a+shift d v (BoolAnd a b) = BoolAnd a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolOr a b) = BoolOr a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolEQ a b) = BoolEQ a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolNE a b) = BoolNE a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolIf a b c) = BoolIf a' b' c'+ where+ a' = shift d v a+ b' = shift d v b+ c' = shift d v c+shift _ _ Natural = Natural+shift _ _ (NaturalLit a) = NaturalLit a+shift _ _ NaturalFold = NaturalFold+shift _ _ NaturalBuild = NaturalBuild+shift _ _ NaturalIsZero = NaturalIsZero+shift _ _ NaturalEven = NaturalEven+shift _ _ NaturalOdd = NaturalOdd+shift _ _ NaturalToInteger = NaturalToInteger+shift _ _ NaturalShow = NaturalShow+shift d v (NaturalPlus a b) = NaturalPlus a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (NaturalTimes a b) = NaturalTimes a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ Integer = Integer+shift _ _ (IntegerLit a) = IntegerLit a+shift _ _ IntegerShow = IntegerShow+shift _ _ Double = Double+shift _ _ (DoubleLit a) = DoubleLit a+shift _ _ DoubleShow = DoubleShow+shift _ _ Text = Text+shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b)+ where+ a' = fmap (fmap (shift d v)) a+shift d v (TextAppend a b) = TextAppend a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ List = List+shift d v (ListLit a b) = ListLit a' b'+ where+ a' = fmap (shift d v) a+ b' = fmap (shift d v) b+shift _ _ ListBuild = ListBuild+shift d v (ListAppend a b) = ListAppend a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ ListFold = ListFold+shift _ _ ListLength = ListLength+shift _ _ ListHead = ListHead+shift _ _ ListLast = ListLast+shift _ _ ListIndexed = ListIndexed+shift _ _ ListReverse = ListReverse+shift _ _ Optional = Optional+shift d v (OptionalLit a b) = OptionalLit a' b'+ where+ a' = shift d v a+ b' = fmap (shift d v) b+shift _ _ OptionalFold = OptionalFold+shift _ _ OptionalBuild = OptionalBuild+shift d v (Record a) = Record a'+ where+ a' = fmap (shift d v) a+shift d v (RecordLit a) = RecordLit a'+ where+ a' = fmap (shift d v) a+shift d v (Union a) = Union a'+ where+ a' = fmap (shift d v) a+shift d v (UnionLit a b c) = UnionLit a b' c'+ where+ b' = shift d v b+ c' = fmap (shift d v) c+shift d v (Combine a b) = Combine a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (Prefer a b) = Prefer a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (Merge a b c) = Merge a' b' c'+ where+ a' = shift d v a+ b' = shift d v b+ c' = fmap (shift d v) c+shift d v (Constructors a) = Constructors a'+ where+ a' = shift d v a+shift d v (Field a b) = Field a' b+ where+ a' = shift d v a+shift d v (Note a b) = Note a b'+ where+ b' = shift d v b+-- The Dhall compiler enforces that all embedded values are closed expressions+-- and `shift` does nothing to a closed expression+shift _ _ (Embed p) = Embed p++{-| Substitute all occurrences of a variable with an expression++> subst x C B ~ B[x := C]+-}+subst :: Var -> Expr s a -> Expr s a -> Expr s a+subst _ _ (Const a) = Const a+subst (V x n) e (Lam y _A b) = Lam y _A' b'+ where+ _A' = subst (V x n ) e _A+ b' = subst (V x n') (shift 1 (V y 0) e) b+ n' = if x == y then n + 1 else n+subst (V x n) e (Pi y _A _B) = Pi y _A' _B'+ where+ _A' = subst (V x n ) e _A+ _B' = subst (V x n') (shift 1 (V y 0) e) _B+ n' = if x == y then n + 1 else n+subst v e (App f a) = App f' a'+ where+ f' = subst v e f+ a' = subst v e a+subst v e (Var v') = if v == v' then e else Var v'+subst (V x n) e (Let f mt r b) = Let f mt' r' b'+ where+ b' = subst (V x n') (shift 1 (V f 0) e) b+ where+ n' = if x == f then n + 1 else n++ mt' = fmap (subst (V x n) e) mt+ r' = subst (V x n) e r+subst x e (Annot a b) = Annot a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ Bool = Bool+subst _ _ (BoolLit a) = BoolLit a+subst x e (BoolAnd a b) = BoolAnd a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolOr a b) = BoolOr a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolEQ a b) = BoolEQ a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolNE a b) = BoolNE a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolIf a b c) = BoolIf a' b' c'+ where+ a' = subst x e a+ b' = subst x e b+ c' = subst x e c+subst _ _ Natural = Natural+subst _ _ (NaturalLit a) = NaturalLit a+subst _ _ NaturalFold = NaturalFold+subst _ _ NaturalBuild = NaturalBuild+subst _ _ NaturalIsZero = NaturalIsZero+subst _ _ NaturalEven = NaturalEven+subst _ _ NaturalOdd = NaturalOdd+subst _ _ NaturalToInteger = NaturalToInteger+subst _ _ NaturalShow = NaturalShow+subst x e (NaturalPlus a b) = NaturalPlus a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (NaturalTimes a b) = NaturalTimes a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ Integer = Integer+subst _ _ (IntegerLit a) = IntegerLit a+subst _ _ IntegerShow = IntegerShow+subst _ _ Double = Double+subst _ _ (DoubleLit a) = DoubleLit a+subst _ _ DoubleShow = DoubleShow+subst _ _ Text = Text+subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b)+ where+ a' = fmap (fmap (subst x e)) a+subst x e (TextAppend a b) = TextAppend a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ List = List+subst x e (ListLit a b) = ListLit a' b'+ where+ a' = fmap (subst x e) a+ b' = fmap (subst x e) b+subst x e (ListAppend a b) = ListAppend a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ ListBuild = ListBuild+subst _ _ ListFold = ListFold+subst _ _ ListLength = ListLength+subst _ _ ListHead = ListHead+subst _ _ ListLast = ListLast+subst _ _ ListIndexed = ListIndexed+subst _ _ ListReverse = ListReverse+subst _ _ Optional = Optional+subst x e (OptionalLit a b) = OptionalLit a' b'+ where+ a' = subst x e a+ b' = fmap (subst x e) b+subst _ _ OptionalFold = OptionalFold+subst _ _ OptionalBuild = OptionalBuild+subst x e (Record kts) = Record (fmap (subst x e) kts)+subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs)+subst x e (Union kts) = Union (fmap (subst x e) kts)+subst x e (UnionLit a b kts) = UnionLit a (subst x e b) (fmap (subst x e) kts)+subst x e (Combine a b) = Combine a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (Prefer a b) = Prefer a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (Merge a b c) = Merge a' b' c'+ where+ a' = subst x e a+ b' = subst x e b+ c' = fmap (subst x e) c+subst x e (Constructors a) = Constructors a'+ where+ a' = subst x e a+subst x e (Field a b) = Field a' b+ where+ a' = subst x e a+subst x e (Note a b) = Note a b'+ where+ b' = subst x e b+-- The Dhall compiler enforces that all embedded values are closed expressions+-- and `subst` does nothing to a closed expression+subst _ _ (Embed p) = Embed p++{-| Reduce an expression to its normal form, performing beta reduction++ `normalize` does not type-check the expression. You may want to type-check+ expressions before normalizing them since normalization can convert an+ ill-typed expression into a well-typed expression.++ However, `normalize` will not fail if the expression is ill-typed and will+ leave ill-typed sub-expressions unevaluated.+-}+normalize :: Expr s a -> Expr t a+normalize = normalizeWith (const Nothing)++{-| This function is used to determine whether folds like @Natural/fold@ or+ @List/fold@ should be lazy or strict in their accumulator based on the type+ of the accumulator++ If this function returns `True`, then they will be strict in their+ accumulator since we can guarantee an upper bound on the amount of work to+ normalize the accumulator on each step of the loop. If this function+ returns `False` then they will be lazy in their accumulator and only+ normalize the final result at the end of the fold+-}+boundedType :: Expr s a -> Bool+boundedType Bool = True+boundedType Natural = True+boundedType Integer = True+boundedType Double = True+boundedType Text = True+boundedType (App List _) = False+boundedType (App Optional t) = boundedType t+boundedType (Record kvs) = all boundedType kvs+boundedType (Union kvs) = all boundedType kvs+boundedType _ = False++-- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)+denote :: Expr s a -> Expr t a+denote (Note _ b ) = denote b+denote (Const a ) = Const a+denote (Var a ) = Var a+denote (Lam a b c ) = Lam a (denote b) (denote c)+denote (Pi a b c ) = Pi a (denote b) (denote c)+denote (App a b ) = App (denote a) (denote b)+denote (Let a b c d ) = Let a (fmap denote b) (denote c) (denote d)+denote (Annot a b ) = Annot (denote a) (denote b)+denote Bool = Bool+denote (BoolLit a ) = BoolLit a+denote (BoolAnd a b ) = BoolAnd (denote a) (denote b)+denote (BoolOr a b ) = BoolOr (denote a) (denote b)+denote (BoolEQ a b ) = BoolEQ (denote a) (denote b)+denote (BoolNE a b ) = BoolNE (denote a) (denote b)+denote (BoolIf a b c ) = BoolIf (denote a) (denote b) (denote c)+denote Natural = Natural+denote (NaturalLit a ) = NaturalLit a+denote NaturalFold = NaturalFold+denote NaturalBuild = NaturalBuild+denote NaturalIsZero = NaturalIsZero+denote NaturalEven = NaturalEven+denote NaturalOdd = NaturalOdd+denote NaturalToInteger = NaturalToInteger+denote NaturalShow = NaturalShow+denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b)+denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b)+denote Integer = Integer+denote (IntegerLit a ) = IntegerLit a+denote IntegerShow = IntegerShow+denote Double = Double+denote (DoubleLit a ) = DoubleLit a+denote DoubleShow = DoubleShow+denote Text = Text+denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b)+denote (TextAppend a b ) = TextAppend (denote a) (denote b)+denote List = List+denote (ListLit a b ) = ListLit (fmap denote a) (fmap denote b)+denote (ListAppend a b ) = ListAppend (denote a) (denote b)+denote ListBuild = ListBuild+denote ListFold = ListFold+denote ListLength = ListLength+denote ListHead = ListHead+denote ListLast = ListLast+denote ListIndexed = ListIndexed+denote ListReverse = ListReverse+denote Optional = Optional+denote (OptionalLit a b ) = OptionalLit (denote a) (fmap denote b)+denote OptionalFold = OptionalFold+denote OptionalBuild = OptionalBuild+denote (Record a ) = Record (fmap denote a)+denote (RecordLit a ) = RecordLit (fmap denote a)+denote (Union a ) = Union (fmap denote a)+denote (UnionLit a b c ) = UnionLit a (denote b) (fmap denote c)+denote (Combine a b ) = Combine (denote a) (denote b)+denote (Prefer a b ) = Prefer (denote a) (denote b)+denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c)+denote (Constructors a ) = Constructors (denote a)+denote (Field a b ) = Field (denote a) b+denote (Embed a ) = Embed a++{-| Reduce an expression to its normal form, performing beta reduction and applying+ any custom definitions.+ + `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`+ function allows typing of Dhall functions in a custom typing context whereas + `normalizeWith` allows evaluating Dhall expressions in a custom context. ++ To be more precise `normalizeWith` applies the given normalizer when it finds an+ application term that it cannot reduce by other means.++ Note that the context used in normalization will determine the properties of normalization.+ That is, if the functions in custom context are not total then the Dhall language, evaluated+ with those functions is not total either. + +-}+normalizeWith :: Normalizer a -> Expr s a -> Expr t a+normalizeWith ctx e0 = loop (denote e0)+ where+ -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of+ -- `loop`. In theory, this might change a failing repro case into+ -- a successful one, but the risk of that is low enough to not warrant+ -- the `Show` constraint. I care more about proving at the type level+ -- that the @a@ and @s@ type parameters are never used+ e'' = bimap (\_ -> ()) (\_ -> ()) e0++ text = "NormalizeWith.loop (" <> Data.Text.pack (show e'') <> ")"+ loop e = case e of+ Const k -> Const k+ Var v -> Var v+ Lam x _A b -> Lam x _A' b'+ where+ _A' = loop _A+ b' = loop b+ Pi x _A _B -> Pi x _A' _B'+ where+ _A' = loop _A+ _B' = loop _B+ App f a -> case loop f of+ Lam x _A b -> loop b'' -- Beta reduce+ where+ a' = shift 1 (V x 0) a+ b' = subst (V x 0) a' b+ b'' = shift (-1) (V x 0) b'+ f' -> case App f' a' of+ -- fold/build fusion for `List`+ App (App ListBuild _) (App (App ListFold _) e') -> loop e'+ App (App ListFold _) (App (App ListBuild _) e') -> loop e'+ -- fold/build fusion for `Natural`+ App NaturalBuild (App NaturalFold e') -> loop e'+ App NaturalFold (App NaturalBuild e') -> loop e'++ -- fold/build fusion for `Optional`+ App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'+ App (App OptionalFold _) (App (App OptionalBuild _) e') -> loop e'++ App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero ->+ if boundedType (loop t) then strict else lazy+ where+ strict = strictLoop n0+ lazy = loop ( lazyLoop n0)++ strictLoop !0 = loop zero+ strictLoop !n = loop (App succ' (strictLoop (n - 1)))++ lazyLoop !0 = zero+ lazyLoop !n = App succ' (lazyLoop (n - 1))+ App NaturalBuild k+ | check -> NaturalLit n+ | otherwise -> App f' a'+ where+ labeled =+ loop (App (App (App k Natural) "Succ") "Zero")++ n = go 0 labeled+ where+ go !m (App (Var "Succ") e') = go (m + 1) e'+ go !m (Var "Zero") = m+ go !_ _ = internalError text+ check = go labeled+ where+ go (App (Var "Succ") e') = go e'+ go (Var "Zero") = True+ go _ = False+ App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)+ App NaturalEven (NaturalLit n) -> BoolLit (even n)+ App NaturalOdd (NaturalLit n) -> BoolLit (odd n)+ App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n)+ App NaturalShow (NaturalLit n) ->+ TextLit (Chunks [] ("+" <> buildNatural n))+ App IntegerShow (IntegerLit n) ->+ TextLit (Chunks [] (buildNumber n))+ App DoubleShow (DoubleLit n) ->+ TextLit (Chunks [] (buildScientific n))+ App (App OptionalBuild t) k+ | check -> OptionalLit t k'+ | otherwise -> App f' a'+ where+ labeled = loop (App (App (App k (App Optional t)) "Just") "Nothing")++ k' = go labeled+ where+ go (App (Var "Just") e') = pure e'+ go (Var "Nothing") = empty+ go _ = internalError text+ check = go labeled+ where+ go (App (Var "Just") _) = True+ go (Var "Nothing") = True+ go _ = False+ App (App ListBuild t) k+ | check -> ListLit (Just t) (buildVector k')+ | otherwise -> App f' a'+ where+ labeled =+ loop (App (App (App k (App List t)) "Cons") "Nil")++ k' cons nil = go labeled+ where+ go (App (App (Var "Cons") x) e') = cons x (go e')+ go (Var "Nil") = nil+ go _ = internalError text+ check = go labeled+ where+ go (App (App (Var "Cons") _) e') = go e'+ go (Var "Nil") = True+ go _ = False+ App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil ->+ if boundedType (loop t) then strict else lazy+ where+ strict = Data.Vector.foldr strictCons strictNil xs+ lazy = loop (Data.Vector.foldr lazyCons lazyNil xs)++ strictNil = loop nil+ lazyNil = nil++ strictCons y ys = loop (App (App cons y) ys)+ lazyCons y ys = App (App cons y) ys+ App (App ListLength _) (ListLit _ ys) ->+ NaturalLit (fromIntegral (Data.Vector.length ys))+ App (App ListHead t) (ListLit _ ys) ->+ loop (OptionalLit t (Data.Vector.take 1 ys))+ App (App ListLast t) (ListLit _ ys) ->+ loop (OptionalLit t y)+ where+ y = if Data.Vector.null ys+ then Data.Vector.empty+ else Data.Vector.singleton (Data.Vector.last ys)+ App (App ListIndexed t) (ListLit _ xs) ->+ loop (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs)))+ where+ t' = Record (Data.HashMap.Strict.InsOrd.fromList kts)+ where+ kts = [ ("index", Natural)+ , ("value", t)+ ]+ adapt (n, x) = RecordLit (Data.HashMap.Strict.InsOrd.fromList kvs)+ where+ kvs = [ ("index", NaturalLit (fromIntegral n))+ , ("value", x)+ ]+ App (App ListReverse t) (ListLit _ xs) ->+ loop (ListLit (Just t) (Data.Vector.reverse xs))+ App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->+ loop (maybe nothing just' (toMaybe xs))+ where+ just' y = App just y+ toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList+ _ -> case ctx (App f' a') of+ Nothing -> App f' a'+ Just app' -> loop app'+ where+ a' = loop a+ Let f _ r b -> loop b''+ where+ r' = shift 1 (V f 0) r+ b' = subst (V f 0) r' b+ b'' = shift (-1) (V f 0) b'+ Annot x _ -> loop x+ Bool -> Bool+ BoolLit b -> BoolLit b+ BoolAnd x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn && yn)+ _ -> BoolAnd x' y'+ _ -> BoolAnd x' y'+ where+ x' = loop x+ y' = loop y+ BoolOr x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn || yn)+ _ -> BoolOr x' y'+ _ -> BoolOr x' y'+ where+ x' = loop x+ y' = loop y+ BoolEQ x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn == yn)+ _ -> BoolEQ x' y'+ _ -> BoolEQ x' y'+ where+ x' = loop x+ y' = loop y+ BoolNE x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn /= yn)+ _ -> BoolNE x' y'+ _ -> BoolNE x' y'+ where+ x' = loop x+ y' = loop y+ BoolIf b true false -> case loop b of+ BoolLit True -> true'+ BoolLit False -> false'+ b' -> BoolIf b' true' false'+ where+ true' = loop true+ false' = loop false+ Natural -> Natural+ NaturalLit n -> NaturalLit n+ NaturalFold -> NaturalFold+ NaturalBuild -> NaturalBuild+ NaturalIsZero -> NaturalIsZero+ NaturalEven -> NaturalEven+ NaturalOdd -> NaturalOdd+ NaturalToInteger -> NaturalToInteger+ NaturalShow -> NaturalShow+ NaturalPlus x y ->+ case x' of+ NaturalLit xn ->+ case y' of+ NaturalLit yn -> NaturalLit (xn + yn)+ _ -> NaturalPlus x' y'+ _ -> NaturalPlus x' y'+ where+ x' = loop x+ y' = loop y+ NaturalTimes x y ->+ case x' of+ NaturalLit xn ->+ case y' of+ NaturalLit yn -> NaturalLit (xn * yn)+ _ -> NaturalTimes x' y'+ _ -> NaturalTimes x' y'+ where+ x' = loop x+ y' = loop y+ Integer -> Integer+ IntegerLit n -> IntegerLit n+ IntegerShow -> IntegerShow+ Double -> Double+ DoubleLit n -> DoubleLit n+ DoubleShow -> DoubleShow+ Text -> Text+ TextLit (Chunks xys z) ->+ case mconcat chunks of+ Chunks [("", x)] "" -> x+ c -> TextLit c+ where+ chunks = concatMap process xys ++ [Chunks [] z]++ process (x, y) = case loop y of+ TextLit c -> [Chunks [] x, c]+ y' -> [Chunks [(x, y')] mempty]+ TextAppend x y ->+ case x' of+ TextLit xt ->+ case y' of+ TextLit yt -> TextLit (xt <> yt)+ _ -> TextAppend x' y'+ _ -> TextAppend x' y'+ where+ x' = loop x+ y' = loop y+ List -> List+ ListLit t es -> ListLit t' es'+ where+ t' = fmap loop t+ es' = fmap loop es+ ListAppend x y ->+ case x' of+ ListLit t xs ->+ case y' of+ ListLit _ ys -> ListLit t (xs <> ys)+ _ -> ListAppend x' y'+ _ -> ListAppend x' y'+ where+ x' = loop x+ y' = loop y+ ListBuild -> ListBuild+ ListFold -> ListFold+ ListLength -> ListLength+ ListHead -> ListHead+ ListLast -> ListLast+ ListIndexed -> ListIndexed+ ListReverse -> ListReverse+ Optional -> Optional+ OptionalLit t es -> OptionalLit t' es'+ where+ t' = loop t+ es' = fmap loop es+ OptionalFold -> OptionalFold+ OptionalBuild -> OptionalBuild+ Record kts -> Record kts'+ where+ kts' = fmap loop kts+ RecordLit kvs -> RecordLit kvs'+ where+ kvs' = fmap loop kvs+ Union kts -> Union kts'+ where+ kts' = fmap loop kts+ UnionLit k v kvs -> UnionLit k v' kvs'+ where+ v' = loop v+ kvs' = fmap loop kvs+ Combine x0 y0 ->+ let combine x y = case x of+ RecordLit kvsX -> case y of+ RecordLit kvsY ->+ let kvs = Data.HashMap.Strict.InsOrd.unionWith combine kvsX kvsY+ in RecordLit (fmap loop kvs)+ _ -> Combine x y+ _ -> Combine x y+ in combine (loop x0) (loop y0)+ Prefer x y ->+ case x' of+ RecordLit kvsX ->+ case y' of+ RecordLit kvsY ->+ RecordLit (fmap loop (Data.HashMap.Strict.InsOrd.union kvsY kvsX))+ _ -> Prefer x' y'+ _ -> Prefer x' y'+ where+ x' = loop x+ y' = loop y+ Merge x y t ->+ case x' of+ RecordLit kvsX ->+ case y' of+ UnionLit kY vY _ ->+ case Data.HashMap.Strict.InsOrd.lookup kY kvsX of+ Just vX -> loop (App vX vY)+ Nothing -> Merge x' y' t'+ _ -> Merge x' y' t'+ _ -> Merge x' y' t'+ where+ x' = loop x+ y' = loop y+ t' = fmap loop t+ Constructors t ->+ case t' of+ Union kts -> RecordLit kvs+ where+ kvs = Data.HashMap.Strict.InsOrd.mapWithKey adapt kts++ adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)+ where+ rest = Data.HashMap.Strict.InsOrd.delete k kts+ _ -> Constructors t'+ where+ t' = loop t+ Field r x ->+ case loop r of+ RecordLit kvs ->+ case Data.HashMap.Strict.InsOrd.lookup x kvs of+ Just v -> loop v+ Nothing -> Field (RecordLit (fmap loop kvs)) x+ r' -> Field r' x+ Note _ e' -> loop e'+ Embed a -> Embed a++-- | Use this to wrap you embedded functions (see `normalizeWith`) to make them+-- polymorphic enough to be used.+type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)++-- | Check if an expression is in a normal form given a context of evaluation.+-- Unlike `isNormalized`, this will fully normalize and traverse through the expression. +-- +-- It is much more efficient to use `isNormalized`.+isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool+isNormalizedWith ctx e = e == (normalizeWith ctx e)+++-- | Quickly check if an expression is in normal form+isNormalized :: Expr s a -> Bool+isNormalized e = case denote e of+ Const _ -> True+ Var _ -> True+ Lam _ a b -> isNormalized a && isNormalized b+ Pi _ a b -> isNormalized a && isNormalized b+ App f a -> isNormalized f && isNormalized a && case App f a of+ App (Lam _ _ _) _ -> False++ -- fold/build fusion for `List`+ App (App ListBuild _) (App (App ListFold _) _) -> False+ App (App ListFold _) (App (App ListBuild _) _) -> False++ -- fold/build fusion for `Natural`+ App NaturalBuild (App NaturalFold _) -> False+ App NaturalFold (App NaturalBuild _) -> False++ -- fold/build fusion for `Optional`+ App (App OptionalBuild _) (App (App OptionalFold _) _) -> False+ App (App OptionalFold _) (App (App OptionalBuild _) _) -> False++ App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False+ App NaturalBuild k0 -> isNormalized k0 && not (check0 k0)+ where+ check0 (Lam _ _ (Lam succ _ (Lam zero _ k))) = check1 succ zero k+ check0 _ = False++ check1 succ zero (App (Var (V succ' n)) k) =+ succ == succ' && n == (if succ == zero then 1 else 0) && check1 succ zero k+ check1 _ zero (Var (V zero' 0)) = zero == zero'+ check1 _ _ _ = False+ App NaturalIsZero (NaturalLit _) -> False+ App NaturalEven (NaturalLit _) -> False+ App NaturalOdd (NaturalLit _) -> False+ App NaturalShow (NaturalLit _) -> False+ App NaturalToInteger (NaturalLit _) -> False+ App IntegerShow (IntegerLit _) -> False+ App DoubleShow (DoubleLit _) -> False+ App (App OptionalBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)+ where+ check0 (Lam _ _ (Lam just _ (Lam nothing _ k))) = check1 just nothing k+ check0 _ = False++ check1 just nothing (App (Var (V just' n)) _) =+ just == just' && n == (if just == nothing then 1 else 0)+ check1 _ nothing (Var (V nothing' 0)) = nothing == nothing'+ check1 _ _ _ = False+ App (App ListBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)+ where+ check0 (Lam _ _ (Lam cons _ (Lam nil _ k))) = check1 cons nil k+ check0 _ = False++ check1 cons nil (App (Var (V cons' n)) k) =+ cons == cons' && n == (if cons == nil then 1 else 0) && check1 cons nil k+ check1 _ nil (Var (V nil' 0)) = nil == nil'+ check1 _ _ _ = False+ App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->+ False+ App (App ListLength _) (ListLit _ _) -> False+ App (App ListHead _) (ListLit _ _) -> False+ App (App ListLast _) (ListLit _ _) -> False+ App (App ListIndexed _) (ListLit _ _) -> False+ App (App ListReverse _) (ListLit _ _) -> False+ App (App (App (App (App OptionalFold _) (OptionalLit _ _)) _) _) _ ->+ False+ _ -> True+ Let _ _ _ _ -> False+ Annot _ _ -> False+ Bool -> True+ BoolLit _ -> True+ BoolAnd x y -> isNormalized x && isNormalized y &&+ case x of+ BoolLit _ ->+ case y of+ BoolLit _ -> False+ _ -> True+ _ -> True+ BoolOr x y -> isNormalized x && isNormalized y &&+ case x of+ BoolLit _ ->+ case y of+ BoolLit _ -> False+ _ -> True+ _ -> True+ BoolEQ x y -> isNormalized x && isNormalized y &&+ case x of+ BoolLit _ ->+ case y of+ BoolLit _ -> False+ _ -> True+ _ -> True+ BoolNE x y -> isNormalized x && isNormalized y &&+ case x of+ BoolLit _ ->+ case y of+ BoolLit _ -> False+ _ -> True+ _ -> True+ BoolIf b true false -> isNormalized b && case b of+ BoolLit _ -> False+ _ -> isNormalized true && isNormalized false+ Natural -> True+ NaturalLit _ -> True+ NaturalFold -> True+ NaturalBuild -> True+ NaturalIsZero -> True+ NaturalEven -> True+ NaturalOdd -> True+ 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+ Integer -> True+ IntegerLit _ -> True+ IntegerShow -> True+ Double -> True+ 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+ 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+ ListBuild -> True+ ListFold -> True+ ListLength -> True+ ListHead -> True+ ListLast -> True+ ListIndexed -> True+ ListReverse -> True+ Optional -> True+ OptionalLit t es -> isNormalized t && all isNormalized es+ OptionalFold -> True+ OptionalBuild -> True+ Record kts -> all isNormalized kts+ RecordLit kvs -> all isNormalized kvs+ Union kts -> all isNormalized kts+ UnionLit _ v kvs -> isNormalized v && all isNormalized kvs+ Combine x y -> isNormalized x && isNormalized y && combine+ where+ combine = case x of+ RecordLit _ -> case y of+ RecordLit _ -> False+ _ -> True+ _ -> True+ Prefer x y -> isNormalized x && isNormalized y && combine+ where+ combine = case x of+ RecordLit _ -> case y of+ RecordLit _ -> False+ _ -> True+ _ -> True+ Merge x y t -> isNormalized x && isNormalized y && any isNormalized t &&+ case x of+ RecordLit kvsX ->+ case y of+ UnionLit kY _ _ ->+ case Data.HashMap.Strict.InsOrd.lookup kY kvsX of+ Just _ -> False+ Nothing -> True+ _ -> True+ _ -> True+ Constructors t -> isNormalized t &&+ case t of+ Union _ -> False+ _ -> True+ Field r x -> isNormalized r &&+ case r of+ RecordLit kvs ->+ case Data.HashMap.Strict.InsOrd.lookup x kvs of+ Just _ -> False+ Nothing -> True+ _ -> True+ Note _ e' -> isNormalized e'+ Embed _ -> True++_ERROR :: String+_ERROR = "\ESC[1;31mError\ESC[0m"++{-| Utility function used to throw internal errors that should never happen+ (in theory) but that are not enforced by the type system+-}+internalError :: Data.Text.Text -> forall b . b+internalError text = error (unlines+ [ _ERROR <> ": Compiler bug "+ , " "+ , "Explanation: This error message means that there is a bug in the Dhall compiler."+ , "You didn't do anything wrong, but if you would like to see this problem fixed "+ , "then you should report the bug at: "+ , " "+ , "https://github.com/dhall-lang/dhall-haskell/issues "+ , " "+ , "Please include the following text in your bug report: "+ , " "+ , "``` "+ , Data.Text.unpack text <> " "+ , "``` "+ ] )++buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a+buildVector f = Data.Vector.reverse (Data.Vector.create (do+ let cons a st = do+ (len, cap, mv) <- st+ if len < cap+ then do+ Data.Vector.Mutable.write mv len a+ return (len + 1, cap, mv)+ else do+ let cap' = 2 * cap+ mv' <- Data.Vector.Mutable.unsafeGrow mv cap'+ Data.Vector.Mutable.write mv' len a+ return (len + 1, cap', mv')+ let nil = do+ mv <- Data.Vector.Mutable.unsafeNew 1+ return (0, 1, mv)+ (len, _, mv) <- f cons nil+ return (Data.Vector.Mutable.slice 0 len mv) ))++-- | The set of reserved identifiers for the Dhall language+reservedIdentifiers :: HashSet Text+reservedIdentifiers =+ Data.HashSet.fromList+ [ "let"+ , "in"+ , "Type"+ , "Kind"+ , "forall"+ , "Bool"+ , "True"+ , "False"+ , "merge"+ , "if"+ , "then"+ , "else"+ , "as"+ , "using"+ , "constructors"+ , "Natural"+ , "Natural/fold"+ , "Natural/build"+ , "Natural/isZero"+ , "Natural/even"+ , "Natural/odd"+ , "Natural/toInteger"+ , "Natural/show"+ , "Integer"+ , "Integer/show"+ , "Double"+ , "Double/show"+ , "Text"+ , "List"+ , "List/build"+ , "List/fold"+ , "List/length"+ , "List/head"+ , "List/last"+ , "List/indexed"+ , "List/reverse"+ , "Optional"+ , "Optional/build" , "Optional/fold" ]
+ src/Dhall/Core.hs-boot view
@@ -0,0 +1,7 @@+module Dhall.Core where++data Const++data Var++data Expr s a
src/Dhall/Import.hs view
@@ -107,6 +107,8 @@ , loadWithContext , hashExpression , hashExpressionToCode+ , Status(..)+ , emptyStatus , Cycle(..) , ReferentiallyOpaque(..) , Imported(..)@@ -124,7 +126,7 @@ import Control.Monad.Trans.State.Strict (StateT) import Data.ByteString.Lazy (ByteString) import Data.CaseInsensitive (CI)-import Data.Map.Strict (Map)+import Data.Map (Map) import Data.Monoid ((<>)) import Data.Text.Buildable (build) import Data.Text.Lazy (Text)@@ -134,7 +136,7 @@ import Data.Traversable (traverse) #endif import Data.Typeable (Typeable)-import Filesystem.Path ((</>), FilePath)+import System.FilePath ((</>)) import Dhall.Core ( Expr(..) , Chunks(..)@@ -154,7 +156,6 @@ #else import Network.HTTP.Client (HttpException(..), Manager) #endif-import Prelude hiding (FilePath) import Text.Trifecta (Result(..)) import Text.Trifecta.Delta (Delta(..)) @@ -166,8 +167,8 @@ import qualified Data.ByteString.Lazy import qualified Data.CaseInsensitive import qualified Data.List as List+import qualified Data.HashMap.Strict.InsOrd import qualified Data.Map.Strict as Map-import qualified Data.Text import qualified Data.Text.Encoding import qualified Data.Text.IO import qualified Data.Text.Lazy as Text@@ -179,12 +180,11 @@ import qualified Dhall.Parser import qualified Dhall.Context import qualified Dhall.TypeCheck-import qualified Filesystem-import qualified Filesystem.Path.CurrentOS import qualified Network.HTTP.Client as HTTP import qualified Network.HTTP.Client.TLS as HTTP-import qualified Filesystem.Path.CurrentOS as Filesystem import qualified System.Environment+import qualified System.Directory+import qualified System.FilePath as FilePath import qualified Text.Parser.Combinators import qualified Text.Parser.Token import qualified Text.Trifecta@@ -314,13 +314,8 @@ show (MissingFile path) = "\n" <> "\ESC[1;31mError\ESC[0m: Missing file "- <> Data.Text.unpack formattedPath+ <> path <> "\n"- where- formattedPath = case Filesystem.Path.CurrentOS.toText path of- (Right t) -> t- (Left t) -> t- <> "\n\ESC[1;31mWarning\ESC[0m: Filename contains non-displayable characters" -- | Exception thrown when an environment variable is missing newtype MissingEnvironmentVariable = MissingEnvironmentVariable { name :: Text }@@ -335,12 +330,19 @@ <> "\n" <> "↳ " <> Text.unpack name +-- | State threaded throughout the import process data Status = Status { _stack :: [Path]+ -- ^ Stack of `Path`s that we've imported along the way to get to the+ -- current point , _cache :: Map Path (Expr Src X)+ -- ^ Cache of imported expressions in order to avoid importing the same+ -- expression twice with different values , _manager :: Maybe Manager+ -- ^ Cache for the `Manager` so that we only acquire it once } +-- | Default starting `Status` emptyStatus :: Status emptyStatus = Status [] Map.empty Nothing @@ -395,27 +397,27 @@ canonicalize :: [PathType] -> PathType canonicalize [] = File Homeless "." canonicalize (File hasHome0 file0:paths0) =- if Filesystem.relative file0 && hasHome0 == Homeless+ if FilePath.isRelative file0 && hasHome0 == Homeless then go file0 paths0- else File hasHome0 (clean file0)+ else File hasHome0 (FilePath.normalise file0) where- go currPath [] = File Homeless (clean currPath)- go currPath (Env _ :_ ) = File Homeless (clean currPath)+ go currPath [] = File Homeless (FilePath.normalise currPath)+ go currPath (Env _ :_ ) = File Homeless (FilePath.normalise currPath) go currPath (URL url0 headers:rest ) = combine prefix suffix where headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers prefix = parentURL (removeAtFromURL url0) - suffix = clean currPath+ suffix = FilePath.normalise currPath -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still -- need to manually handle @.@/@..@'s at the beginning of the path- combine url path = case Filesystem.stripPrefix ".." path of+ combine url path = case List.stripPrefix "../" path of Just path' -> combine url' path' where url' = parentURL (removeAtFromURL url)- Nothing -> case Filesystem.stripPrefix "." path of+ Nothing -> case List.stripPrefix "./" path of Just path' -> combine url path' Nothing -> -- This `last` is safe because the lexer constrains all@@ -425,15 +427,13 @@ '/' -> URL (url <> path') headers' _ -> URL (url <> "/" <> path') headers' where- path' = Text.fromStrict (case Filesystem.toText path of- Left txt -> txt- Right txt -> txt )+ path' = Text.pack path go currPath (File hasHome file:paths) =- if Filesystem.relative file && hasHome == Homeless+ if FilePath.isRelative file && hasHome == Homeless then go file' paths- else File hasHome (clean file')+ else File hasHome (FilePath.normalise file') where- file' = Filesystem.parent (removeAtFromFile file) </> currPath+ file' = FilePath.takeDirectory (removeAtFromFilename file) </> currPath canonicalize (URL path headers:rest) = URL path headers' where headers' = fmap (onPathType (\h -> canonicalize (h:rest))) headers@@ -470,19 +470,11 @@ | Text.isSuffixOf "/" url = Text.dropEnd 1 url | otherwise = url -removeAtFromFile :: FilePath -> FilePath-removeAtFromFile file =- if Filesystem.filename file == "@"- then Filesystem.parent file- else file---- | Remove all @.@'s and @..@'s in the path-clean :: FilePath -> FilePath-clean = strip . Filesystem.collapse- where- strip p = case Filesystem.stripPrefix "." p of- Nothing -> p- Just p' -> p'+removeAtFromFilename :: FilePath -> FilePath+removeAtFromFilename fp =+ if FilePath.takeFileName fp == "@"+ then FilePath.takeDirectory fp+ else fp toHeaders :: Expr s a@@ -497,8 +489,8 @@ :: Expr s a -> Maybe (CI Data.ByteString.ByteString, Data.ByteString.ByteString) toHeader (RecordLit m) = do- TextLit (Chunks [] keyBuilder ) <- Map.lookup "header" m- TextLit (Chunks [] valueBuilder) <- Map.lookup "value" m+ TextLit (Chunks [] keyBuilder ) <- Data.HashMap.Strict.InsOrd.lookup "header" m+ TextLit (Chunks [] valueBuilder) <- Data.HashMap.Strict.InsOrd.lookup "value" m let keyText = Text.toStrict (Builder.toLazyText keyBuilder ) let valueText = Text.toStrict (Builder.toLazyText valueBuilder) let keyBytes = Data.Text.Encoding.encodeUtf8 keyText@@ -569,7 +561,7 @@ -> FilePath -> IO (Text.Trifecta.Result a) parseFromFileEx parser path = do- text <- Data.Text.Lazy.IO.readFile stringPath+ text <- Data.Text.Lazy.IO.readFile path let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 text @@ -579,13 +571,7 @@ return (Text.Trifecta.parseByteString parser delta strictBytes) where- stringPath = Filesystem.Path.CurrentOS.encodeString path-- textPath = case Filesystem.Path.CurrentOS.toText path of- Left text -> text- Right text -> text-- bytesPath = Data.Text.Encoding.encodeUtf8 textPath+ bytesPath = Data.ByteString.Char8.pack path -- | Parse an expression from a `Path` containing a Dhall program exprFromPath :: Path -> StateT Status IO (Expr Src Path)@@ -593,14 +579,14 @@ File hasHome file -> liftIO (do path <- case hasHome of Home -> do- home <- Filesystem.getHomeDirectory+ home <- System.Directory.getHomeDirectory return (home </> file) Homeless -> do return file case pathMode of Code -> do- exists <- Filesystem.isFile path+ exists <- System.Directory.doesFileExist path if exists then return () else throwIO (MissingFile path)@@ -622,8 +608,7 @@ Success expr -> do return expr RawText -> do- let pathString = Filesystem.Path.CurrentOS.encodeString path- text <- Data.Text.IO.readFile pathString+ text <- Data.Text.IO.readFile path return (TextLit (Chunks [] (build text))) ) URL url headerPath -> do m <- needManager@@ -649,7 +634,7 @@ expected = App List ( Record- ( Map.fromList+ ( Data.HashMap.Strict.InsOrd.fromList [("header", Text), ("value", Text)] ) )
src/Dhall/Parser.hs view
@@ -24,9 +24,10 @@ import Control.Monad (MonadPlus) import Data.ByteString (ByteString) import Data.Functor (void)-import Data.Map (Map)+import Data.HashMap.Strict.InsOrd (InsOrdHashMap) import Data.Monoid ((<>)) import Data.Sequence (ViewL(..))+import Data.Scientific (Scientific) import Data.String (IsString(..)) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text)@@ -44,10 +45,11 @@ import qualified Control.Monad import qualified Data.ByteString.Base16.Lazy+import qualified Data.ByteString.Lazy import qualified Data.Char+import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet-import qualified Data.Map-import qualified Data.ByteString.Lazy+import qualified Data.List import qualified Data.Sequence import qualified Data.Text import qualified Data.Text.Encoding@@ -55,7 +57,6 @@ import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding import qualified Data.Vector-import qualified Filesystem.Path.CurrentOS import qualified Text.Parser.Char import qualified Text.Parser.Combinators import qualified Text.Parser.Token@@ -687,11 +688,11 @@ void (Text.Parser.Char.char '→' <?> "\"→\"") <|> void (Text.Parser.Char.text "->") whitespace -doubleLiteral :: Parser Double+doubleLiteral :: Parser Scientific doubleLiteral = (do sign <- fmap (\_ -> negate) (Text.Parser.Char.char '-') <|> pure id- a <- Text.Parser.Token.double+ a <- Text.Parser.Token.scientific return (sign a) ) <?> "double literal" integerLiteral :: Parser Integer@@ -745,25 +746,25 @@ _ <- Text.Parser.Char.char '/' a <- Text.Parser.Char.satisfy headPathCharacter bs <- many (Text.Parser.Char.satisfy pathCharacter)- let string = '/':a:bs- return (File Homeless (Filesystem.Path.CurrentOS.decodeString string))+ let filepath = '/':a:bs+ return (File Homeless filepath) relativePath = do _ <- Text.Parser.Char.text "./" as <- many (Text.Parser.Char.satisfy pathCharacter)- let string = "./" <> as- return (File Homeless (Filesystem.Path.CurrentOS.decodeString string))+ let filepath = "./" <> as+ return (File Homeless filepath) parentPath = do _ <- Text.Parser.Char.text "../" as <- many (Text.Parser.Char.satisfy pathCharacter)- let string = "../" <> as- return (File Homeless (Filesystem.Path.CurrentOS.decodeString string))+ let filepath = "../" <> as+ return (File Homeless filepath) homePath = do _ <- Text.Parser.Char.text "~/" as <- many (Text.Parser.Char.satisfy pathCharacter)- return (File Home (Filesystem.Path.CurrentOS.decodeString as))+ return (File Home as) file :: Parser PathType file = do@@ -1173,6 +1174,7 @@ , alternative05 , alternative06 , alternative07+ , alternative37 , choice [ alternative08@@ -1205,7 +1207,6 @@ , alternative35 , alternative36 ] <?> "built-in expression"- , alternative37 ] ) <|> alternative38@@ -1378,11 +1379,11 @@ where alternative0 = do _equal- return (RecordLit Data.Map.empty)+ return (RecordLit Data.HashMap.Strict.InsOrd.empty) alternative1 = nonEmptyRecordTypeOrLiteral embedded - alternative2 = return (Record Data.Map.empty)+ alternative2 = return (Record Data.HashMap.Strict.InsOrd.empty) nonEmptyRecordTypeOrLiteral :: Parser a -> Parser (Expr Src a) nonEmptyRecordTypeOrLiteral embedded = do@@ -1397,7 +1398,7 @@ _colon d <- expression embedded return (c, d) )- return (Record (Data.Map.fromList ((a, b):e)))+ return (Record (Data.HashMap.Strict.InsOrd.fromList ((a, b):e))) let nonEmptyRecordLiteral = do _equal@@ -1408,13 +1409,14 @@ _equal d <- expression embedded return (c, d) )- return (RecordLit (Data.Map.fromList ((a, b):e)))+ return (RecordLit (Data.HashMap.Strict.InsOrd.fromList ((a, b):e))) nonEmptyRecordType <|> nonEmptyRecordLiteral unionTypeOrLiteral :: Parser a -> Parser (Expr Src a) unionTypeOrLiteral embedded =- nonEmptyUnionTypeOrLiteral embedded <|> return (Union Data.Map.empty)+ nonEmptyUnionTypeOrLiteral embedded+ <|> return (Union Data.HashMap.Strict.InsOrd.empty) nonEmptyUnionTypeOrLiteral :: Parser a -> Parser (Expr Src a) nonEmptyUnionTypeOrLiteral embedded = do@@ -1464,10 +1466,10 @@ whitespace expression embedded -toMap :: [(Text, a)] -> Parser (Map Text a)+toMap :: [(Text, a)] -> Parser (InsOrdHashMap Text a) toMap kvs = do let adapt (k, v) = (k, pure v)- let m = Data.Map.fromListWith (<|>) (fmap adapt kvs)+ let m = fromListWith (<|>) (fmap adapt kvs) let action k vs = case Data.Sequence.viewl vs of EmptyL -> empty v :< vs' ->@@ -1476,7 +1478,13 @@ else Text.Parser.Combinators.unexpected ("duplicate field: " ++ Data.Text.Lazy.unpack k)- Data.Map.traverseWithKey action m+ Data.HashMap.Strict.InsOrd.traverseWithKey action m+ where+ fromListWith combine = Data.List.foldl' snoc nil+ where+ nil = Data.HashMap.Strict.InsOrd.empty++ snoc m (k, v) = Data.HashMap.Strict.InsOrd.insertWith combine k v m -- | Parser for a top-level Dhall expression expr :: Parser (Expr Src Path)
+ src/Dhall/Pretty.hs view
@@ -0,0 +1,6 @@+{-| This module contains logic for pretty-printing expressions, including+ support for syntax highlighting+-}+module Dhall.Pretty ( Ann(..), annToAnsiStyle, prettyExpr ) where++import Dhall.Pretty.Internal
+ src/Dhall/Pretty/Internal.hs view
@@ -0,0 +1,1153 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wall #-}++{-| This module provides internal pretty-printing utilities which are used by+ other modules but are not part of the public facing API+-}++module Dhall.Pretty.Internal (+ Ann(..)+ , annToAnsiStyle+ , prettyExpr+ , buildConst+ , buildVar+ , buildExpr+ , buildNatural+ , buildNumber+ , buildScientific+ , pretty+ , escapeText+ ) where++import {-# SOURCE #-} Dhall.Core++#if MIN_VERSION_base(4,8,0)+#else+import Control.Applicative (Applicative(..), (<$>))+#endif+import Data.Foldable+import Data.HashMap.Strict.InsOrd (InsOrdHashMap)+import Data.Monoid ((<>))+import Data.Scientific (Scientific)+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+import Data.Text.Prettyprint.Doc (Doc, Pretty, space)+import Numeric.Natural (Natural)+import Prelude hiding (succ)+import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Terminal++import qualified Data.Char+import qualified Data.HashMap.Strict.InsOrd+import qualified Data.HashSet+import qualified Data.List+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty+import qualified Data.Vector++{-| Annotation type used to tag elements in a pretty-printed document for+ syntax highlighting purposes+-}+data Ann+ = Keyword -- ^ Used for syntactic keywords+ | Syntax -- ^ Syntax punctuation such as commas, parenthesis, and braces+ | Label -- ^ Record labels+ | Literal -- ^ Literals such as integers and strings+ | Builtin -- ^ Builtin types and values+ | Operator -- ^ Operators++{-| Convert annotations to their corresponding color for syntax highlighting+ purposes+-}+annToAnsiStyle :: Ann -> Terminal.AnsiStyle+annToAnsiStyle Keyword = Terminal.colorDull Terminal.Green+annToAnsiStyle Syntax = Terminal.colorDull Terminal.Green+annToAnsiStyle Label = mempty+annToAnsiStyle Literal = Terminal.colorDull Terminal.Magenta+annToAnsiStyle Builtin = Terminal.underlined+annToAnsiStyle Operator = Terminal.colorDull Terminal.Green++-- | Pretty print an expression+prettyExpr :: Pretty a => Expr s a -> Doc Ann+prettyExpr = prettyExprA++{-| Internal utility for pretty-printing, used when generating element lists+ to supply to `enclose` or `enclose'`. This utility indicates that the+ compact represent is the same as the multi-line representation for each+ element+-}+duplicate :: a -> (a, a)+duplicate x = (x, x)++-- Annotation helpers+keyword, syntax, label, literal, builtin, operator :: Doc Ann -> Doc Ann+keyword = Pretty.annotate Keyword+syntax = Pretty.annotate Syntax+label = Pretty.annotate Label+literal = Pretty.annotate Literal+builtin = Pretty.annotate Builtin+operator = Pretty.annotate Operator++comma, lbracket, rbracket, langle, rangle, lbrace, rbrace, lparen, rparen, pipe, rarrow, backtick, dollar, colon, lambda, forall, equals, dot :: Doc Ann+comma = syntax Pretty.comma+lbracket = syntax Pretty.lbracket+rbracket = syntax Pretty.rbracket+langle = syntax Pretty.langle+rangle = syntax Pretty.rangle+lbrace = syntax Pretty.lbrace+rbrace = syntax Pretty.rbrace+lparen = syntax Pretty.lparen+rparen = syntax Pretty.rparen+pipe = syntax Pretty.pipe+rarrow = syntax "→"+backtick = syntax "`"+dollar = syntax "$"+colon = syntax ":"+lambda = syntax "λ"+forall = syntax "∀"+equals = syntax "="+dot = syntax "."++-- | Pretty-print a list+list :: [Doc Ann] -> Doc Ann+list [] = lbracket <> rbracket+list docs =+ enclose+ (lbracket <> space)+ (lbracket <> space)+ (comma <> space)+ (comma <> space)+ (space <> rbracket)+ rbracket+ (fmap duplicate docs)++-- | Pretty-print union types and literals+angles :: [(Doc Ann, Doc Ann)] -> Doc Ann+angles [] = langle <> rangle+angles docs =+ enclose+ (langle <> space)+ (langle <> space)+ (space <> pipe <> space)+ (pipe <> space)+ (space <> rangle)+ rangle+ docs++-- | Pretty-print record types and literals+braces :: [(Doc Ann, Doc Ann)] -> Doc Ann+braces [] = lbrace <> rbrace+braces docs =+ enclose+ (lbrace <> space)+ (lbrace <> space)+ (comma <> space)+ (comma <> space)+ (space <> rbrace)+ rbrace+ docs++-- | Pretty-print anonymous functions and function types+arrows :: [(Doc Ann, Doc Ann)] -> Doc Ann+arrows =+ enclose'+ ""+ " "+ (" " <> rarrow <> " ")+ (rarrow <> space)++{-| Format an expression that holds a variable number of elements, such as a+ list, record, or union+-}+enclose+ :: Doc ann+ -- ^ Beginning document for compact representation+ -> Doc ann+ -- ^ Beginning document for multi-line representation+ -> Doc ann+ -- ^ Separator for compact representation+ -> Doc ann+ -- ^ Separator for multi-line representation+ -> Doc ann+ -- ^ Ending document for compact representation+ -> Doc ann+ -- ^ Ending document for multi-line representation+ -> [(Doc ann, Doc ann)]+ -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@+ -> Doc ann+enclose beginShort _ _ _ endShort _ [] =+ beginShort <> endShort+ where+enclose beginShort beginLong sepShort sepLong endShort endLong docs =+ Pretty.group+ (Pretty.flatAlt+ (Pretty.align+ (mconcat (zipWith combineLong (beginLong : repeat sepLong) docsLong) <> endLong)+ )+ (mconcat (zipWith combineShort (beginShort : repeat sepShort) docsShort) <> endShort)+ )+ where+ docsShort = fmap fst docs++ docsLong = fmap snd docs++ combineLong x y = x <> y <> Pretty.hardline++ combineShort x y = x <> y++{-| Format an expression that holds a variable number of elements without a+ trailing document such as nested `let`, nested lambdas, or nested `forall`s+-}+enclose'+ :: Doc ann+ -- ^ Beginning document for compact representation+ -> Doc ann+ -- ^ Beginning document for multi-line representation+ -> Doc ann+ -- ^ Separator for compact representation+ -> Doc ann+ -- ^ Separator for multi-line representation+ -> [(Doc ann, Doc ann)]+ -- ^ Elements to format, each of which is a pair: @(compact, multi-line)@+ -> Doc ann+enclose' beginShort beginLong sepShort sepLong docs =+ Pretty.group (Pretty.flatAlt long short)+ where+ longLines = zipWith (<>) (beginLong : repeat sepLong) docsLong++ long =+ Pretty.align (mconcat (Data.List.intersperse Pretty.hardline longLines))++ short = mconcat (zipWith (<>) (beginShort : repeat sepShort) docsShort)++ docsShort = fmap fst docs++ docsLong = fmap snd docs++alpha :: Char -> Bool+alpha c = ('\x41' <= c && c <= '\x5A') || ('\x61' <= c && c <= '\x7A')++digit :: Char -> Bool+digit c = '\x30' <= c && c <= '\x39'++headCharacter :: Char -> Bool+headCharacter c = alpha c || c == '_'++tailCharacter :: Char -> Bool+tailCharacter c = alpha c || digit c || c == '_' || c == '-' || c == '/'++prettyLabel :: Text -> Doc Ann+prettyLabel a = label doc+ where+ doc =+ case Text.uncons a of+ Just (h, t)+ | headCharacter h && Text.all tailCharacter t && not (Data.HashSet.member a reservedIdentifiers)+ -> Pretty.pretty a+ _ -> backtick <> Pretty.pretty a <> backtick++prettyNumber :: Integer -> Doc Ann+prettyNumber = literal . Pretty.pretty++prettyNatural :: Natural -> Doc Ann+prettyNatural = literal . Pretty.pretty++prettyScientific :: Scientific -> Doc Ann+prettyScientific = literal . Pretty.pretty . show++prettyChunks :: Pretty a => Chunks s a -> Doc Ann+prettyChunks (Chunks a b) =+ if any (\(builder, _) -> hasNewLine builder) a || hasNewLine b+ then Pretty.flatAlt long short+ else short+ where+ long =+ Pretty.align+ ( literal ("''" <> Pretty.hardline)+ <> Pretty.align+ (foldMap prettyMultilineChunk a <> prettyMultilineBuilder b)+ <> literal "''"+ )++ short =+ literal "\"" <> foldMap prettyChunk a <> literal (prettyText b <> "\"")++ hasNewLine builder = Text.any (== '\n') lazyText+ where+ lazyText = Builder.toLazyText builder++ prettyMultilineChunk (c, d) =+ prettyMultilineBuilder c <> dollar <> lbrace <> prettyExprA d <> rbrace++ prettyMultilineBuilder builder = literal (mconcat docs)+ where+ lazyText = Builder.toLazyText (escapeSingleQuotedText builder)++ lazyLines = Text.splitOn "\n" lazyText++ docs =+ Data.List.intersperse Pretty.hardline (fmap Pretty.pretty lazyLines)++ prettyChunk (c, d) = prettyText c <> syntax "${" <> prettyExprA d <> syntax rbrace++ prettyText t = literal (Pretty.pretty (Builder.toLazyText (escapeText t)))++prettyConst :: Const -> Doc Ann+prettyConst Type = builtin "Type"+prettyConst Kind = builtin "Kind"++prettyVar :: Var -> Doc Ann+prettyVar (V x 0) = label (Pretty.unAnnotate (prettyLabel x))+prettyVar (V x n) = label (Pretty.unAnnotate (prettyLabel x <> "@" <> prettyNumber n))++prettyExprA :: Pretty a => Expr s a -> Doc Ann+prettyExprA a0@(Annot _ _) =+ enclose'+ ""+ " "+ (" " <> colon <> " ")+ (colon <> space)+ (fmap duplicate (docs a0))+ where+ docs (Annot a b) = prettyExprB a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprB b ]+prettyExprA (Note _ a) =+ prettyExprA a+prettyExprA a0 =+ prettyExprB a0++prettyExprB :: Pretty a => Expr s a -> Doc Ann+prettyExprB a0@(Lam _ _ _) = arrows (fmap duplicate (docs a0))+ where+ docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c+ where+ long = (lambda <> space)+ <> Pretty.align+ ( (lparen <> space)+ <> prettyLabel a+ <> Pretty.hardline+ <> (colon <> space)+ <> prettyExprA b+ <> Pretty.hardline+ <> rparen+ )++ short = (lambda <> lparen)+ <> prettyLabel a+ <> (space <> colon <> space)+ <> prettyExprA b+ <> rparen+ docs (Note _ c) = docs c+ docs c = [ prettyExprB c ]+prettyExprB a0@(BoolIf _ _ _) =+ enclose' "" " " (space <> keyword "else" <> space) (Pretty.hardline <> keyword "else" <> " ") (fmap duplicate (docs a0))+ where+ docs (BoolIf a b c) =+ Pretty.group (Pretty.flatAlt long short) : docs c+ where+ long =+ Pretty.align+ ( (keyword "if" <> " ")+ <> prettyExprA a+ <> Pretty.hardline+ <> (keyword "then" <> " ")+ <> prettyExprA b+ )++ short = (keyword "if" <> " ")+ <> prettyExprA a+ <> (space <> keyword "then" <> space)+ <> prettyExprA b+ docs (Note _ c) = docs c+ docs c = [ prettyExprB c ]+prettyExprB a0@(Pi _ _ _) =+ arrows (fmap duplicate (docs a0))+ where+ docs (Pi "_" b c) = prettyExprC b : docs c+ docs (Pi a b c) = Pretty.group (Pretty.flatAlt long short) : docs c+ where+ long = forall <> space+ <> Pretty.align+ ( lparen <> space+ <> prettyLabel a+ <> Pretty.hardline+ <> colon <> space+ <> prettyExprA b+ <> Pretty.hardline+ <> rparen+ )++ short = forall <> lparen+ <> prettyLabel a+ <> space <> colon <> space+ <> prettyExprA b+ <> rparen+ docs (Note _ c) = docs c+ docs c = [ prettyExprB c ]+prettyExprB a0@(Let _ _ _ _) =+ enclose' "" " " (space <> keyword "in" <> space) (Pretty.hardline <> keyword "in" <> " ")+ (fmap duplicate (docs a0))+ where+ docs (Let a Nothing c d) =+ Pretty.group (Pretty.flatAlt long short) : docs d+ where+ long = keyword "let" <> space+ <> Pretty.align+ ( prettyLabel a+ <> space <> equals+ <> Pretty.hardline+ <> " "+ <> prettyExprA c+ )++ short = keyword "let" <> space+ <> prettyLabel a+ <> (space <> equals <> space)+ <> prettyExprA c+ docs (Let a (Just b) c d) =+ Pretty.group (Pretty.flatAlt long short) : docs d+ where+ long = keyword "let" <> space+ <> Pretty.align+ ( prettyLabel a+ <> Pretty.hardline+ <> colon <> space+ <> prettyExprA b+ <> Pretty.hardline+ <> equals <> space+ <> prettyExprA c+ )++ short = keyword "let" <> space+ <> prettyLabel a+ <> space <> colon <> space+ <> prettyExprA b+ <> space <> equals <> space+ <> prettyExprA c+ docs (Note _ d) =+ docs d+ docs d =+ [ prettyExprB d ]+prettyExprB (ListLit Nothing b) =+ list (map prettyExprA (Data.Vector.toList b))+prettyExprB (ListLit (Just a) b) =+ list (map prettyExprA (Data.Vector.toList b))+ <> " : "+ <> prettyExprD (App List a)+prettyExprB (OptionalLit a b) =+ list (map prettyExprA (Data.Vector.toList b))+ <> " : "+ <> prettyExprD (App Optional a)+prettyExprB (Merge a b (Just c)) =+ Pretty.group (Pretty.flatAlt long short)+ where+ long =+ Pretty.align+ ( keyword "merge"+ <> Pretty.hardline+ <> prettyExprE a+ <> Pretty.hardline+ <> prettyExprE b+ <> Pretty.hardline+ <> colon <> space+ <> prettyExprD c+ )++ short = keyword "merge" <> space+ <> prettyExprE a+ <> " "+ <> prettyExprE b+ <> space <> colon <> space+ <> prettyExprD c+prettyExprB (Merge a b Nothing) =+ Pretty.group (Pretty.flatAlt long short)+ where+ long =+ Pretty.align+ ( keyword "merge"+ <> Pretty.hardline+ <> prettyExprE a+ <> Pretty.hardline+ <> prettyExprE b+ )++ short = keyword "merge" <> space+ <> prettyExprE a+ <> " "+ <> prettyExprE b+prettyExprB (Note _ b) =+ prettyExprB b+prettyExprB a =+ prettyExprC a++prettyExprC :: Pretty a => Expr s a -> Doc Ann+prettyExprC = prettyExprC0++prettyExprC0 :: Pretty a => Expr s a -> Doc Ann+prettyExprC0 a0@(BoolOr _ _) =+ enclose' "" " " (space <> operator "||" <> space) (operator "||" <> " ") (fmap duplicate (docs a0))+ where+ docs (BoolOr a b) = prettyExprC1 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC1 b ]+prettyExprC0 (Note _ a) =+ prettyExprC0 a+prettyExprC0 a0 =+ prettyExprC1 a0++prettyExprC1 :: Pretty a => Expr s a -> Doc Ann+prettyExprC1 a0@(TextAppend _ _) =+ enclose' "" " " (" " <> operator "++" <> " ") (operator "++" <> " ") (fmap duplicate (docs a0))+ where+ docs (TextAppend a b) = prettyExprC2 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC2 b ]+prettyExprC1 (Note _ a) =+ prettyExprC1 a+prettyExprC1 a0 =+ prettyExprC2 a0++prettyExprC2 :: Pretty a => Expr s a -> Doc Ann+prettyExprC2 a0@(NaturalPlus _ _) =+ enclose' "" " " (" " <> operator "+" <> " ") (operator "+" <> " ") (fmap duplicate (docs a0))+ where+ docs (NaturalPlus a b) = prettyExprC3 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC3 b ]+prettyExprC2 (Note _ a) =+ prettyExprC2 a+prettyExprC2 a0 =+ prettyExprC3 a0++prettyExprC3 :: Pretty a => Expr s a -> Doc Ann+prettyExprC3 a0@(ListAppend _ _) =+ enclose' "" " " (" " <> operator "#" <> " ") (operator "#" <> " ") (fmap duplicate (docs a0))+ where+ docs (ListAppend a b) = prettyExprC4 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC4 b ]+prettyExprC3 (Note _ a) =+ prettyExprC3 a+prettyExprC3 a0 =+ prettyExprC4 a0++prettyExprC4 :: Pretty a => Expr s a -> Doc Ann+prettyExprC4 a0@(BoolAnd _ _) =+ enclose' "" " " (" " <> operator "&&" <> " ") (operator "&&" <> " ") (fmap duplicate (docs a0))+ where+ docs (BoolAnd a b) = prettyExprC5 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC5 b ]+prettyExprC4 (Note _ a) =+ prettyExprC4 a+prettyExprC4 a0 =+ prettyExprC5 a0++prettyExprC5 :: Pretty a => Expr s a -> Doc Ann+prettyExprC5 a0@(Combine _ _) =+ enclose' "" " " (" " <> operator "∧" <> " ") (operator "∧" <> " ") (fmap duplicate (docs a0))+ where+ docs (Combine a b) = prettyExprC6 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC6 b ]+prettyExprC5 (Note _ a) =+ prettyExprC5 a+prettyExprC5 a0 =+ prettyExprC6 a0++prettyExprC6 :: Pretty a => Expr s a -> Doc Ann+prettyExprC6 a0@(Prefer _ _) =+ enclose' "" " " (" " <> operator "⫽" <> " ") (operator "⫽" <> " ") (fmap duplicate (docs a0))+ where+ docs (Prefer a b) = prettyExprC7 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC7 b ]+prettyExprC6 (Note _ a) =+ prettyExprC6 a+prettyExprC6 a0 =+ prettyExprC7 a0++prettyExprC7 :: Pretty a => Expr s a -> Doc Ann+prettyExprC7 a0@(NaturalTimes _ _) =+ enclose' "" " " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))+ where+ docs (NaturalTimes a b) = prettyExprC8 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC8 b ]+prettyExprC7 (Note _ a) =+ prettyExprC7 a+prettyExprC7 a0 =+ prettyExprC8 a0++prettyExprC8 :: Pretty a => Expr s a -> Doc Ann+prettyExprC8 a0@(BoolEQ _ _) =+ enclose' "" " " (" " <> operator "==" <> " ") (operator "==" <> " ") (fmap duplicate (docs a0))+ where+ docs (BoolEQ a b) = prettyExprC9 a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprC9 b ]+prettyExprC8 (Note _ a) =+ prettyExprC8 a+prettyExprC8 a0 =+ prettyExprC9 a0++prettyExprC9 :: Pretty a => Expr s a -> Doc Ann+prettyExprC9 a0@(BoolNE _ _) =+ enclose' "" " " (" " <> operator "!=" <> " ") (operator "!=" <> " ") (fmap duplicate (docs a0))+ where+ docs (BoolNE a b) = prettyExprD a : docs b+ docs (Note _ b) = docs b+ docs b = [ prettyExprD b ]+prettyExprC9 (Note _ a) =+ prettyExprC9 a+prettyExprC9 a0 =+ prettyExprD a0++prettyExprD :: Pretty a => Expr s a -> Doc Ann+prettyExprD a0 = case a0 of+ App _ _ -> result+ Constructors _ -> result+ Note _ b -> prettyExprD b+ _ -> prettyExprE a0+ where+ result = enclose' "" "" " " "" (fmap duplicate (reverse (docs a0)))++ docs (App a b) = prettyExprE b : docs a+ docs (Constructors b) = [ prettyExprE b , keyword "constructors" ]+ docs (Note _ b) = docs b+ docs b = [ prettyExprE b ]++prettyExprE :: Pretty a => Expr s a -> Doc Ann+prettyExprE (Field a b) = prettyExprE a <> dot <> prettyLabel b+prettyExprE (Note _ b) = prettyExprE b+prettyExprE a = prettyExprF a++prettyExprF :: Pretty a => Expr s a -> Doc Ann+prettyExprF (Var a) =+ prettyVar a+prettyExprF (Const k) =+ prettyConst k+prettyExprF Bool =+ builtin "Bool"+prettyExprF Natural =+ builtin "Natural"+prettyExprF NaturalFold =+ builtin "Natural/fold"+prettyExprF NaturalBuild =+ builtin "Natural/build"+prettyExprF NaturalIsZero =+ builtin "Natural/isZero"+prettyExprF NaturalEven =+ builtin "Natural/even"+prettyExprF NaturalOdd =+ builtin "Natural/odd"+prettyExprF NaturalToInteger =+ builtin "Natural/toInteger"+prettyExprF NaturalShow =+ builtin "Natural/show"+prettyExprF Integer =+ builtin "Integer"+prettyExprF IntegerShow =+ builtin "Integer/show"+prettyExprF Double =+ builtin "Double"+prettyExprF DoubleShow =+ builtin "Double/show"+prettyExprF Text =+ builtin "Text"+prettyExprF List =+ builtin "List"+prettyExprF ListBuild =+ builtin "List/build"+prettyExprF ListFold =+ builtin "List/fold"+prettyExprF ListLength =+ builtin "List/length"+prettyExprF ListHead =+ builtin "List/head"+prettyExprF ListLast =+ builtin "List/last"+prettyExprF ListIndexed =+ builtin "List/indexed"+prettyExprF ListReverse =+ builtin "List/reverse"+prettyExprF Optional =+ builtin "Optional"+prettyExprF OptionalFold =+ builtin "Optional/fold"+prettyExprF OptionalBuild =+ builtin "Optional/build"+prettyExprF (BoolLit True) =+ builtin "True"+prettyExprF (BoolLit False) =+ builtin "False"+prettyExprF (IntegerLit a) =+ prettyNumber a+prettyExprF (NaturalLit a) =+ literal "+" <> prettyNatural a+prettyExprF (DoubleLit a) =+ prettyScientific a+prettyExprF (TextLit a) =+ prettyChunks a+prettyExprF (Record a) =+ prettyRecord a+prettyExprF (RecordLit a) =+ prettyRecordLit a+prettyExprF (Union a) =+ prettyUnion a+prettyExprF (UnionLit a b c) =+ prettyUnionLit a b c+prettyExprF (ListLit Nothing b) =+ list (map prettyExprA (Data.Vector.toList b))+prettyExprF (Embed a) =+ Pretty.pretty a+prettyExprF (Note _ b) =+ prettyExprF b+prettyExprF a =+ Pretty.group (Pretty.flatAlt long short)+ where+ long = Pretty.align (lparen <> space <> prettyExprA a <> Pretty.hardline <> rparen)++ short = lparen <> prettyExprA a <> rparen++prettyKeyValue :: Pretty a => Doc Ann -> (Text, Expr s a) -> (Doc Ann, Doc Ann)+prettyKeyValue separator (key, value) =+ ( prettyLabel key <> " " <> separator <> " " <> prettyExprA value+ , prettyLabel key+ <> " "+ <> separator+ <> long+ )+ where+ long = Pretty.hardline <> " " <> prettyExprA value++prettyRecord :: Pretty a => InsOrdHashMap Text (Expr s a) -> Doc Ann+prettyRecord =+ braces . map (prettyKeyValue colon) . Data.HashMap.Strict.InsOrd.toList++prettyRecordLit :: Pretty a => InsOrdHashMap Text (Expr s a) -> Doc Ann+prettyRecordLit a+ | Data.HashMap.Strict.InsOrd.null a =+ lbrace <> equals <> rbrace+ | otherwise+ = braces (map (prettyKeyValue equals) (Data.HashMap.Strict.InsOrd.toList a))++prettyUnion :: Pretty a => InsOrdHashMap Text (Expr s a) -> Doc Ann+prettyUnion =+ angles . map (prettyKeyValue colon) . Data.HashMap.Strict.InsOrd.toList++prettyUnionLit+ :: Pretty a => Text -> Expr s a -> InsOrdHashMap Text (Expr s a) -> Doc Ann+prettyUnionLit a b c =+ angles (front : map adapt (Data.HashMap.Strict.InsOrd.toList c))+ where+ front = prettyKeyValue equals (a, b)++ adapt = prettyKeyValue colon++-- | Pretty-print a value+pretty :: Pretty a => a -> Text+pretty = Pretty.renderLazy . Pretty.layoutPretty options . Pretty.pretty+ where+ options = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }++-- | Builder corresponding to the @label@ token in "Dhall.Parser"+buildLabel :: Text -> Builder+buildLabel l = case Text.uncons l of+ Just (h, t)+ | headCharacter h && Text.all tailCharacter t && not (Data.HashSet.member l reservedIdentifiers)+ -> build l+ _ -> "`" <> build l <> "`"+++-- | Builder corresponding to the @number@ token in "Dhall.Parser"+buildNumber :: Integer -> Builder+buildNumber a = build (show a)++-- | Builder corresponding to the @natural@ token in "Dhall.Parser"+buildNatural :: Natural -> Builder+buildNatural a = build (show a)++-- | Builder corresponding to the @double@ token in "Dhall.Parser"+buildScientific :: Scientific -> Builder+buildScientific = build . show++-- | Builder corresponding to the @text@ token in "Dhall.Parser"+buildChunks :: Buildable a => Chunks s a -> Builder+buildChunks (Chunks a b) = "\"" <> foldMap buildChunk a <> escapeText b <> "\""+ where+ buildChunk (c, d) = escapeText c <> "${" <> buildExprA d <> "}"++-- | Escape a `Builder` literal using Dhall's escaping rules for single-quoted+-- @Text@+escapeSingleQuotedText :: Builder -> Builder+escapeSingleQuotedText inputBuilder = outputBuilder+ where+ inputText = Builder.toLazyText inputBuilder++ outputText = substitute "${" "''${" (substitute "''" "'''" inputText)++ outputBuilder = Builder.fromLazyText outputText++ substitute before after = Text.intercalate after . Text.splitOn before++{-| Escape a `Builder` literal using Dhall's escaping rules+ + Note that the result does not include surrounding quotes+-}+escapeText :: Builder -> Builder+escapeText a = Builder.fromLazyText (Text.concatMap adapt text)+ where+ adapt c+ | '\x20' <= c && c <= '\x21' = Text.singleton c+ -- '\x22' == '"'+ | '\x23' == c = Text.singleton c+ -- '\x24' == '$'+ | '\x25' <= c && c <= '\x5B' = Text.singleton c+ -- '\x5C' == '\\'+ | '\x5D' <= c && c <= '\x7F' = Text.singleton c+ | c == '"' = "\\\""+ | c == '$' = "\\$"+ | c == '\\' = "\\\\"+ | c == '\b' = "\\b"+ | c == '\f' = "\\f"+ | c == '\n' = "\\n"+ | c == '\r' = "\\r"+ | c == '\t' = "\\t"+ | otherwise = "\\u" <> showDigits (Data.Char.ord c)++ showDigits r0 = Text.pack (map showDigit [q1, q2, q3, r3])+ where+ (q1, r1) = r0 `quotRem` 4096+ (q2, r2) = r1 `quotRem` 256+ (q3, r3) = r2 `quotRem` 16++ showDigit n+ | n < 10 = Data.Char.chr (Data.Char.ord '0' + n)+ | otherwise = Data.Char.chr (Data.Char.ord 'A' + n - 10)++ text = Builder.toLazyText a++-- | Builder corresponding to the @expr@ parser in "Dhall.Parser"+buildExpr :: Buildable a => Expr s a -> Builder+buildExpr = buildExprA++-- | Builder corresponding to the @exprA@ parser in "Dhall.Parser"+buildExprA :: Buildable a => Expr s a -> Builder+buildExprA (Annot a b) = buildExprB a <> " : " <> buildExprA b+buildExprA (Note _ b) = buildExprA b+buildExprA a = buildExprB a++-- | Builder corresponding to the @exprB@ parser in "Dhall.Parser"+buildExprB :: Buildable a => Expr s a -> Builder+buildExprB (Lam a b c) =+ "λ("+ <> buildLabel a+ <> " : "+ <> buildExprA b+ <> ") → "+ <> buildExprB c+buildExprB (BoolIf a b c) =+ "if "+ <> buildExprA a+ <> " then "+ <> buildExprA b+ <> " else "+ <> buildExprA c+buildExprB (Pi "_" b c) =+ buildExprC b+ <> " → "+ <> buildExprB c+buildExprB (Pi a b c) =+ "∀("+ <> buildLabel a+ <> " : "+ <> buildExprA b+ <> ") → "+ <> buildExprB c+buildExprB (Let a Nothing c d) =+ "let "+ <> buildLabel a+ <> " = "+ <> buildExprA c+ <> " in "+ <> buildExprB d+buildExprB (Let a (Just b) c d) =+ "let "+ <> buildLabel a+ <> " : "+ <> buildExprA b+ <> " = "+ <> buildExprA c+ <> " in "+ <> buildExprB d+buildExprB (ListLit Nothing b) =+ "[" <> buildElems (Data.Vector.toList b) <> "]"+buildExprB (ListLit (Just a) b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a+buildExprB (OptionalLit a b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a+buildExprB (Merge a b (Just c)) =+ "merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c+buildExprB (Merge a b Nothing) =+ "merge " <> buildExprE a <> " " <> buildExprE b+buildExprB (Note _ b) =+ buildExprB b+buildExprB a =+ buildExprC a++-- | Builder corresponding to the @exprC@ parser in "Dhall.Parser"+buildExprC :: Buildable a => Expr s a -> Builder+buildExprC = buildExprC0++-- | Builder corresponding to the @exprC0@ parser in "Dhall.Parser"+buildExprC0 :: Buildable a => Expr s a -> Builder+buildExprC0 (BoolOr a b) = buildExprC1 a <> " || " <> buildExprC0 b+buildExprC0 (Note _ b) = buildExprC0 b+buildExprC0 a = buildExprC1 a++-- | Builder corresponding to the @exprC1@ parser in "Dhall.Parser"+buildExprC1 :: Buildable a => Expr s a -> Builder+buildExprC1 (TextAppend a b) = buildExprC2 a <> " ++ " <> buildExprC1 b+buildExprC1 (Note _ b) = buildExprC1 b+buildExprC1 a = buildExprC2 a++-- | Builder corresponding to the @exprC2@ parser in "Dhall.Parser"+buildExprC2 :: Buildable a => Expr s a -> Builder+buildExprC2 (NaturalPlus a b) = buildExprC3 a <> " + " <> buildExprC2 b+buildExprC2 (Note _ b) = buildExprC2 b+buildExprC2 a = buildExprC3 a++-- | Builder corresponding to the @exprC3@ parser in "Dhall.Parser"+buildExprC3 :: Buildable a => Expr s a -> Builder+buildExprC3 (ListAppend a b) = buildExprC4 a <> " # " <> buildExprC3 b+buildExprC3 (Note _ b) = buildExprC3 b+buildExprC3 a = buildExprC4 a++-- | Builder corresponding to the @exprC4@ parser in "Dhall.Parser"+buildExprC4 :: Buildable a => Expr s a -> Builder+buildExprC4 (BoolAnd a b) = buildExprC5 a <> " && " <> buildExprC4 b+buildExprC4 (Note _ b) = buildExprC4 b+buildExprC4 a = buildExprC5 a++-- | Builder corresponding to the @exprC5@ parser in "Dhall.Parser"+buildExprC5 :: Buildable a => Expr s a -> Builder+buildExprC5 (Combine a b) = buildExprC6 a <> " ∧ " <> buildExprC5 b+buildExprC5 (Note _ b) = buildExprC5 b+buildExprC5 a = buildExprC6 a++-- | Builder corresponding to the @exprC6@ parser in "Dhall.Parser"+buildExprC6 :: Buildable a => Expr s a -> Builder+buildExprC6 (Prefer a b) = buildExprC7 a <> " ⫽ " <> buildExprC6 b+buildExprC6 (Note _ b) = buildExprC6 b+buildExprC6 a = buildExprC7 a++-- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser"+buildExprC7 :: Buildable a => Expr s a -> Builder+buildExprC7 (NaturalTimes a b) = buildExprC8 a <> " * " <> buildExprC7 b+buildExprC7 (Note _ b) = buildExprC7 b+buildExprC7 a = buildExprC8 a++-- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser"+buildExprC8 :: Buildable a => Expr s a -> Builder+buildExprC8 (BoolEQ a b) = buildExprC9 a <> " == " <> buildExprC8 b+buildExprC8 (Note _ b) = buildExprC8 b+buildExprC8 a = buildExprC9 a++-- | Builder corresponding to the @exprC9@ parser in "Dhall.Parser"+buildExprC9 :: Buildable a => Expr s a -> Builder+buildExprC9 (BoolNE a b) = buildExprD a <> " != " <> buildExprC9 b+buildExprC9 (Note _ b) = buildExprC9 b+buildExprC9 a = buildExprD a++-- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"+buildExprD :: Buildable a => Expr s a -> Builder+buildExprD (App a b) = buildExprD a <> " " <> buildExprE b+buildExprD (Constructors b) = "constructors " <> buildExprE b+buildExprD (Note _ b) = buildExprD b+buildExprD a = buildExprE a++-- | Builder corresponding to the @exprE@ parser in "Dhall.Parser"+buildExprE :: Buildable a => Expr s a -> Builder+buildExprE (Field a b) = buildExprE a <> "." <> buildLabel b+buildExprE (Note _ b) = buildExprE b+buildExprE a = buildExprF a++-- | Builder corresponding to the @exprF@ parser in "Dhall.Parser"+buildExprF :: Buildable a => Expr s a -> Builder+buildExprF (Var a) =+ buildVar a+buildExprF (Const k) =+ buildConst k+buildExprF Bool =+ "Bool"+buildExprF Natural =+ "Natural"+buildExprF NaturalFold =+ "Natural/fold"+buildExprF NaturalBuild =+ "Natural/build"+buildExprF NaturalIsZero =+ "Natural/isZero"+buildExprF NaturalEven =+ "Natural/even"+buildExprF NaturalOdd =+ "Natural/odd"+buildExprF NaturalToInteger =+ "Natural/toInteger"+buildExprF NaturalShow =+ "Natural/show"+buildExprF Integer =+ "Integer"+buildExprF IntegerShow =+ "Integer/show"+buildExprF Double =+ "Double"+buildExprF DoubleShow =+ "Double/show"+buildExprF Text =+ "Text"+buildExprF List =+ "List"+buildExprF ListBuild =+ "List/build"+buildExprF ListFold =+ "List/fold"+buildExprF ListLength =+ "List/length"+buildExprF ListHead =+ "List/head"+buildExprF ListLast =+ "List/last"+buildExprF ListIndexed =+ "List/indexed"+buildExprF ListReverse =+ "List/reverse"+buildExprF Optional =+ "Optional"+buildExprF OptionalFold =+ "Optional/fold"+buildExprF OptionalBuild =+ "Optional/build"+buildExprF (BoolLit True) =+ "True"+buildExprF (BoolLit False) =+ "False"+buildExprF (IntegerLit a) =+ buildNumber a+buildExprF (NaturalLit a) =+ "+" <> buildNatural a+buildExprF (DoubleLit a) =+ buildScientific a+buildExprF (TextLit a) =+ buildChunks a+buildExprF (Record a) =+ buildRecord a+buildExprF (RecordLit a) =+ buildRecordLit a+buildExprF (Union a) =+ buildUnion a+buildExprF (UnionLit a b c) =+ buildUnionLit a b c+buildExprF (ListLit Nothing b) =+ "[" <> buildElems (Data.Vector.toList b) <> "]"+buildExprF (Embed a) =+ build a+buildExprF (Note _ b) =+ buildExprF b+buildExprF a =+ "(" <> buildExprA a <> ")"++-- | Builder corresponding to the @const@ parser in "Dhall.Parser"+buildConst :: Const -> Builder+buildConst Type = "Type"+buildConst Kind = "Kind"++-- | Builder corresponding to the @var@ parser in "Dhall.Parser"+buildVar :: Var -> Builder+buildVar (V x 0) = buildLabel x+buildVar (V x n) = buildLabel x <> "@" <> buildNumber n++-- | Builder corresponding to the @elems@ parser in "Dhall.Parser"+buildElems :: Buildable a => [Expr s a] -> Builder+buildElems [] = ""+buildElems [a] = buildExprA a+buildElems (a:bs) = buildExprA a <> ", " <> buildElems bs++-- | Builder corresponding to the @recordLit@ parser in "Dhall.Parser"+buildRecordLit :: Buildable a => InsOrdHashMap Text (Expr s a) -> Builder+buildRecordLit a | Data.HashMap.Strict.InsOrd.null a =+ "{=}"+buildRecordLit a =+ "{ " <> buildFieldValues (Data.HashMap.Strict.InsOrd.toList a) <> " }"++-- | Builder corresponding to the @fieldValues@ parser in "Dhall.Parser"+buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder+buildFieldValues [] = ""+buildFieldValues [a] = buildFieldValue a+buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs++-- | Builder corresponding to the @fieldValue@ parser in "Dhall.Parser"+buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder+buildFieldValue (a, b) = buildLabel a <> " = " <> buildExprA b++-- | Builder corresponding to the @record@ parser in "Dhall.Parser"+buildRecord :: Buildable a => InsOrdHashMap Text (Expr s a) -> Builder+buildRecord a | Data.HashMap.Strict.InsOrd.null a =+ "{}"+buildRecord a =+ "{ " <> buildFieldTypes (Data.HashMap.Strict.InsOrd.toList a) <> " }"++-- | Builder corresponding to the @fieldTypes@ parser in "Dhall.Parser"+buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder+buildFieldTypes [] = ""+buildFieldTypes [a] = buildFieldType a+buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs++-- | Builder corresponding to the @fieldType@ parser in "Dhall.Parser"+buildFieldType :: Buildable a => (Text, Expr s a) -> Builder+buildFieldType (a, b) = buildLabel a <> " : " <> buildExprA b++-- | Builder corresponding to the @union@ parser in "Dhall.Parser"+buildUnion :: Buildable a => InsOrdHashMap Text (Expr s a) -> Builder+buildUnion a | Data.HashMap.Strict.InsOrd.null a =+ "<>"+buildUnion a =+ "< " <> buildAlternativeTypes (Data.HashMap.Strict.InsOrd.toList a) <> " >"++-- | Builder corresponding to the @alternativeTypes@ parser in "Dhall.Parser"+buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder+buildAlternativeTypes [] =+ ""+buildAlternativeTypes [a] =+ buildAlternativeType a+buildAlternativeTypes (a:bs) =+ buildAlternativeType a <> " | " <> buildAlternativeTypes bs++-- | Builder corresponding to the @alternativeType@ parser in "Dhall.Parser"+buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder+buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExprA b++-- | Builder corresponding to the @unionLit@ parser in "Dhall.Parser"+buildUnionLit+ :: Buildable a+ => Text -> Expr s a -> InsOrdHashMap Text (Expr s a) -> Builder+buildUnionLit a b c+ | Data.HashMap.Strict.InsOrd.null c =+ "< "+ <> buildLabel a+ <> " = "+ <> buildExprA b+ <> " >"+ | otherwise =+ "< "+ <> buildLabel a+ <> " = "+ <> buildExprA b+ <> " | "+ <> buildAlternativeTypes (Data.HashMap.Strict.InsOrd.toList c)+ <> " >"
+ src/Dhall/Pretty/Internal.hs-boot view
@@ -0,0 +1,31 @@+module Dhall.Pretty.Internal where++import Data.Scientific (Scientific)+import Data.Text.Buildable (Buildable)+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+import Data.Text.Prettyprint.Doc (Pretty, Doc)+import Numeric.Natural (Natural)+import Prelude++import {-# SOURCE #-} Dhall.Core++data Ann++buildConst :: Const -> Builder++buildVar :: Var -> Builder++buildExpr :: Buildable a => Expr s a -> Builder++prettyExpr :: Pretty a => Expr s a -> Doc Ann++buildNatural :: Natural -> Builder++buildNumber :: Integer -> Builder++buildScientific :: Scientific -> Builder++pretty :: Pretty a => a -> Text++escapeText :: Builder -> Builder
src/Dhall/TypeCheck.hs view
@@ -11,6 +11,7 @@ typeWith , typeOf , typeWithA+ , checkContext -- * Types , Typer@@ -22,6 +23,7 @@ import Control.Exception (Exception) import Data.Foldable (forM_, toList)+import Data.HashMap.Strict.InsOrd (InsOrdHashMap) import Data.Monoid ((<>)) import Data.Set (Set) import Data.Text.Buildable (Buildable(..))@@ -34,7 +36,8 @@ import Dhall.Context (Context) import qualified Control.Monad.Trans.State.Strict as State-import qualified Data.Map+import qualified Data.HashMap.Strict+import qualified Data.HashMap.Strict.InsOrd import qualified Data.Set import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder@@ -63,6 +66,10 @@ nL' = if xL == xL' then nL - 1 else nL nR' = if xR == xR' then nR - 1 else nR +toSortedList :: InsOrdHashMap k v -> [(k, v)]+toSortedList =+ Data.HashMap.Strict.toList . Data.HashMap.Strict.InsOrd.toHashMap+ propEqual :: Eq a => Expr s a -> Expr t a -> Bool propEqual eL0 eR0 = State.evalState@@ -103,7 +110,7 @@ else return False loop [] [] = return True loop _ _ = return False- loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)+ loop (toSortedList ktsL0) (toSortedList ktsR0) go (Union ktsL0) (Union ktsR0) = do let loop ((kL, tL):ktsL) ((kR, tR):ktsR) | kL == kR = do@@ -113,7 +120,7 @@ else return False loop [] [] = return True loop _ _ = return False- loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)+ loop (toSortedList ktsL0) (toSortedList ktsR0) go (Embed eL) (Embed eR) = return (eL == eR) go _ _ = return False @@ -125,11 +132,24 @@ returned type then you may want to `Dhall.Core.normalize` it afterwards. -} typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)-typeWith = typeWithA absurd+typeWith ctx expr = do+ checkContext ctx+ typeWithA absurd ctx expr +{-| Function that converts the value inside an `Embed` constructor into a new+ expression+-} type Typer a = forall s. a -> Expr s a -typeWithA :: Eq a => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a)+{-| Generalization of `typeWith` that allows type-checking the `Embed`+ constructor with custom logic+-}+typeWithA+ :: Eq a+ => Typer a+ -> Context (Expr s a)+ -> Expr s a+ -> Either (TypeError s a) (Expr s a) typeWithA tpa = loop where loop _ (Const c ) = do@@ -436,7 +456,7 @@ return (Pi "a" (Const Type) (Pi "_" (App List "a")- (App List (Record (Data.Map.fromList kts))) ) )+ (App List (Record (Data.HashMap.Strict.InsOrd.fromList kts))) ) ) loop _ ListReverse = do return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a"))) loop _ Optional = do@@ -478,8 +498,9 @@ s <- fmap Dhall.Core.normalize (loop ctx t) case s of Const Type -> return ()+ Const Kind -> return () _ -> Left (TypeError ctx e (InvalidFieldType k t))- mapM_ process (Data.Map.toList kts)+ mapM_ process (Data.HashMap.Strict.InsOrd.toList kts) return (Const Type) loop ctx e@(RecordLit kvs ) = do let process k v = do@@ -487,24 +508,26 @@ s <- fmap Dhall.Core.normalize (loop ctx t) case s of Const Type -> return ()+ Const Kind -> return () _ -> Left (TypeError ctx e (InvalidField k v)) return t- kts <- Data.Map.traverseWithKey process kvs+ kts <- Data.HashMap.Strict.InsOrd.traverseWithKey process kvs return (Record kts) loop ctx e@(Union kts ) = do let process (k, t) = do s <- fmap Dhall.Core.normalize (loop ctx t) case s of Const Type -> return ()+ Const Kind -> return () _ -> Left (TypeError ctx e (InvalidAlternativeType k t))- mapM_ process (Data.Map.toList kts)+ mapM_ process (Data.HashMap.Strict.InsOrd.toList kts) return (Const Type) loop ctx e@(UnionLit k v kts) = do- case Data.Map.lookup k kts of+ case Data.HashMap.Strict.InsOrd.lookup k kts of Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) Nothing -> return () t <- loop ctx v- let union = Union (Data.Map.insert k t kts)+ let union = Union (Data.HashMap.Strict.InsOrd.insert k t kts) _ <- loop ctx union return union loop ctx e@(Combine kvsX kvsY) = do@@ -519,10 +542,13 @@ _ -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY)) let combineTypes ktsL ktsR = do- let ks =- Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)+ let ksL =+ Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsL)+ let ksR =+ Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsR)+ let ks = Data.Set.union ksL ksR kts <- forM (toList ks) (\k -> do- case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of+ case (Data.HashMap.Strict.InsOrd.lookup k ktsL, Data.HashMap.Strict.InsOrd.lookup k ktsR) of (Just (Record ktsL'), Just (Record ktsR')) -> do t <- combineTypes ktsL' ktsR' return (k, t)@@ -532,7 +558,7 @@ return (k, t) _ -> do Left (TypeError ctx e (FieldCollision k)) )- return (Record (Data.Map.fromList kts))+ return (Record (Data.HashMap.Strict.InsOrd.fromList kts)) combineTypes ktsX ktsY loop ctx e@(Prefer kvsX kvsY) = do@@ -545,7 +571,7 @@ ktsY <- case tKvsY of Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY))- return (Record (Data.Map.union ktsY ktsX))+ return (Record (Data.HashMap.Strict.InsOrd.union ktsY ktsX)) loop ctx e@(Merge kvsX kvsY (Just t)) = do _ <- loop ctx t @@ -553,13 +579,13 @@ ktsX <- case tKvsX of Record kts -> return kts _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))- let ksX = Data.Map.keysSet ktsX+ let ksX = Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsX) tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY) ktsY <- case tKvsY of Union kts -> return kts _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))- let ksY = Data.Map.keysSet ktsY+ let ksY = Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsY) let diffX = Data.Set.difference ksX ksY let diffY = Data.Set.difference ksY ksX@@ -569,7 +595,7 @@ else Left (TypeError ctx e (UnusedHandler diffX)) let process (kY, tY) = do- case Data.Map.lookup kY ktsX of+ case Data.HashMap.Strict.InsOrd.lookup kY ktsX of Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of@@ -581,20 +607,20 @@ then return () else Left (TypeError ctx e (InvalidHandlerOutputType kY t t')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))- mapM_ process (Data.Map.toList ktsY)+ mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t loop ctx e@(Merge kvsX kvsY Nothing) = do tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX) ktsX <- case tKvsX of Record kts -> return kts _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))- let ksX = Data.Map.keysSet ktsX+ let ksX = Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsX) tKvsY <- fmap Dhall.Core.normalize (loop ctx kvsY) ktsY <- case tKvsY of Union kts -> return kts _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))- let ksY = Data.Map.keysSet ktsY+ let ksY = Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsY) let diffX = Data.Set.difference ksX ksY let diffY = Data.Set.difference ksY ksX@@ -603,12 +629,12 @@ then return () else Left (TypeError ctx e (UnusedHandler diffX)) - (kX, t) <- case Data.Map.assocs ktsX of+ (kX, t) <- case Data.HashMap.Strict.InsOrd.toList ktsX of [] -> Left (TypeError ctx e MissingMergeType) (kX, Pi _ _ t):_ -> return (kX, t) (kX, tX ):_ -> Left (TypeError ctx e (HandlerNotAFunction kX tX)) let process (kY, tY) = do- case Data.Map.lookup kY ktsX of+ case Data.HashMap.Strict.InsOrd.lookup kY ktsX of Nothing -> Left (TypeError ctx e (MissingHandler diffY)) Just tX -> case tX of@@ -620,7 +646,7 @@ then return () else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t')) _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))- mapM_ process (Data.Map.toList ktsY)+ mapM_ process (Data.HashMap.Strict.InsOrd.toList ktsY) return t loop ctx e@(Constructors t ) = do _ <- loop ctx t@@ -631,14 +657,14 @@ let adapt k t_ = Pi k t_ (Union kts) - return (Record (Data.Map.mapWithKey adapt kts))+ return (Record (Data.HashMap.Strict.InsOrd.mapWithKey adapt kts)) loop ctx e@(Field r x ) = do t <- fmap Dhall.Core.normalize (loop ctx r) case t of Record kts -> do _ <- loop ctx t - case Data.Map.lookup x kts of+ case Data.HashMap.Strict.InsOrd.lookup x kts of Just t' -> return t' Nothing -> Left (TypeError ctx e (MissingField x t)) _ -> Left (TypeError ctx e (NotARecord x r t))@@ -3245,3 +3271,20 @@ source = case expr of Note s _ -> build s _ -> mempty++{-| This function verifies that a custom context is well-formed so that+ type-checking will not loop++ Note that `typeWith` already calls `checkContext` for you on the `Context`+ that you supply+-}+checkContext :: Context (Expr s X) -> Either (TypeError s X) ()+checkContext context =+ case Dhall.Context.match context of+ Nothing -> do+ return ()+ Just (x, v, context') -> do+ let shiftedV = Dhall.Core.shift (-1) (V x 0) v+ let shiftedContext = fmap (Dhall.Core.shift (-1) (V x 0)) context'+ _ <- typeWith shiftedContext shiftedV+ return ()
tests/Format.hs view
@@ -24,6 +24,18 @@ , should "escape ${ for single-quoted strings" "escapeSingleQuotedOpenInterpolation"+ , should+ "preserve the original order of fields"+ "fieldOrder"+ , should+ "escape numeric labels correctly"+ "escapeNumericLabel"+ , should+ "correctly handle scientific notation with a large exponent"+ "largeExponent"+ , should+ "correctly format the empty record literal"+ "emptyRecord" ] opts :: Data.Text.Prettyprint.Doc.LayoutOptions
tests/Normalization.hs view
@@ -4,6 +4,17 @@ module Normalization (normalizationTests) where import Data.Monoid ((<>))+import Data.Text.Lazy (Text)+import Dhall.Core (Expr)+import Dhall.TypeCheck (X)++import qualified Control.Exception+import qualified Data.Text.Lazy+import qualified Dhall.Core+import qualified Dhall.Import+import qualified Dhall.Parser+import qualified Dhall.TypeCheck+ import Dhall.Core import Dhall.Context import Test.Tasty@@ -11,29 +22,38 @@ import Util normalizationTests :: TestTree-normalizationTests = testGroup "normalization" [ constantFolding- , conversions- , fusion- , customization- ]+normalizationTests =+ testGroup "normalization"+ [ constantFolding+ , conversions+ , shouldNormalize "Optional build/fold fusion" "optionalBuildFold"+ , customization+ , shouldNormalize "a remote-systems.conf builder" "remoteSystems"+ ] constantFolding :: TestTree-constantFolding = testGroup "folding of constants" [ naturalPlus- , optionalFold- , optionalBuild- ]+constantFolding =+ testGroup "folding of constants"+ [ shouldNormalize "Natural/plus" "naturalPlus"+ , shouldNormalize "Optional/fold" "optionalFold"+ , shouldNormalize "Optional/build" "optionalBuild"+ ] conversions :: TestTree-conversions = testGroup "conversions" [ naturalShow- , integerShow- , doubleShow- , naturalToInteger- ]+conversions =+ testGroup "conversions"+ [ shouldNormalize "Natural/show" "naturalShow"+ , shouldNormalize "Integer/show" "integerShow"+ , shouldNormalize "Double/show" "doubleShow"+ , shouldNormalize "Natural/toInteger" "naturalToInteger"+ ] customization :: TestTree-customization = testGroup "customization"- [simpleCustomization- ,nestedReduction]+customization =+ testGroup "customization"+ [ simpleCustomization+ , nestedReduction+ ] simpleCustomization :: TestTree simpleCustomization = testCase "simpleCustomization" $ do@@ -60,120 +80,35 @@ e <- codeWith tyCtx "wurble +6" assertNormalizesToWith valCtx e "+5" -naturalPlus :: TestTree-naturalPlus = testCase "natural plus" $ do- e <- code "+1 + +2"- e `assertNormalizesTo` "+3"--naturalToInteger :: TestTree-naturalToInteger = testCase "Natural/toInteger" $ do- e <- code "Natural/toInteger +1"- isNormalized e @?= False- normalize' e @?= "1"--naturalShow :: TestTree-naturalShow = testCase "Natural/show" $ do- e <- code "Natural/show +42"- e `assertNormalizesTo` "\"+42\""--integerShow :: TestTree-integerShow = testCase "Integer/show" $ do- e <- code "[Integer/show 1337, Integer/show -42, Integer/show 0]"- e `assertNormalizesTo` "[ \"1337\", \"-42\", \"0\" ]"--doubleShow :: TestTree-doubleShow = testCase "Double/show" $ do- e <- code "[Double/show -0.42, Double/show 13.37]"- e `assertNormalizesTo` "[ \"-0.42\", \"13.37\" ]"--optionalFold :: TestTree-optionalFold = testGroup "Optional/fold" [ just, nothing ]- where test label inp out = testCase label $ do- e <- code ("Optional/fold Text ([" <> inp <> "] : Optional Text) Natural (λ(j : Text) → +1) +2")- e `assertNormalizesTo` out- just = test "just" "\"foo\"" "+1"- nothing = test "nothing" "" "+2"--optionalBuild :: TestTree-optionalBuild = testGroup "Optional/build" [ optionalBuild1- , optionalBuildShadowing- , optionalBuildIrreducible- ]--optionalBuild1 :: TestTree-optionalBuild1 = testCase "reducible" $ do- e <- code- "Optional/build \n\- \Natural \n\- \( λ(optional : Type) \n\- \→ λ(just : Natural → optional)\n\- \→ λ(nothing : optional) \n\- \→ just +1 \n\- \) \n"- e `assertNormalizesTo` "[ +1 ] : Optional Natural"--optionalBuildShadowing :: TestTree-optionalBuildShadowing = testCase "handles shadowing" $ do- e <- code- "Optional/build \n\- \Integer \n\- \( λ(optional : Type) \n\- \→ λ(x : Integer → optional)\n\- \→ λ(x : optional) \n\- \→ x@1 1 \n\- \) \n"- e `assertNormalizesTo` "[ 1 ] : Optional Integer"+should :: Text -> Text -> TestTree+should name basename =+ Test.Tasty.HUnit.testCase (Data.Text.Lazy.unpack name) $ do+ let actualCode = "./tests/normalization/" <> basename <> "A.dhall"+ let expectedCode = "./tests/normalization/" <> basename <> "B.dhall" -optionalBuildIrreducible :: TestTree-optionalBuildIrreducible = testCase "irreducible" $ do- e <- code- " λ(id : ∀(a : Type) → a → a) \n\- \→ Optional/build \n\- \ Bool \n\- \ ( λ(optional : Type) \n\- \ → λ(just : Bool → optional)\n\- \ → λ(nothing : optional) \n\- \ → id optional (just True) \n\- \ ) \n"- assertNormalized e+ actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr+ actualResolved <- Dhall.Import.load actualExpr+ case Dhall.TypeCheck.typeOf actualResolved of+ Left err -> Control.Exception.throwIO err+ Right _ -> return ()+ let actualNormalized = Dhall.Core.normalize actualResolved :: Expr X X -fusion :: TestTree-fusion = testGroup "Optional build/fold fusion" [ fuseOptionalBF- , fuseOptionalFB- ]+ expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr+ expectedResolved <- Dhall.Import.load expectedExpr+ case Dhall.TypeCheck.typeOf expectedResolved of+ Left err -> Control.Exception.throwIO err+ Right _ -> return ()+ -- Use `denote` instead of `normalize` to enforce that the expected+ -- expression is already in normal form+ let expectedNormalized = Dhall.Core.denote expectedResolved -fuseOptionalBF :: TestTree-fuseOptionalBF = testCase "fold . build" $ do- e0 <- code- " λ( f \n\- \ : ∀(optional : Type) \n\- \ → ∀(just : Text → optional)\n\- \ → ∀(nothing : optional) \n\- \ → optional \n\- \ ) \n\- \→ Optional/fold \n\- \ Text \n\- \ ( Optional/build \n\- \ Text \n\- \ f \n\- \ ) \n"- e1 <- code- " λ( f \n\- \ : ∀(optional : Type) \n\- \ → ∀(just : Text → optional)\n\- \ → ∀(nothing : optional) \n\- \ → optional \n\- \ ) \n\- \→ f \n"- e0 `assertNormalizesTo` (Dhall.Core.pretty e1)+ let message =+ "The normalized expression did not match the expected output"+ Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized -fuseOptionalFB :: TestTree-fuseOptionalFB = testCase "build . fold" $ do- test <- code- "Optional/build \n\- \Text \n\- \( Optional/fold \n\- \ Text \n\- \ ([\"foo\"] : Optional Text)\n\- \) \n"- test `assertNormalizesTo` "[ \"foo\" ] : Optional Text"+shouldNormalize :: Text -> Text -> TestTree+shouldNormalize name = should ("normalize " <> name <> " correctly")
tests/Parser.hs view
@@ -11,64 +11,63 @@ import qualified Dhall.Parser import qualified Test.Tasty import qualified Test.Tasty.HUnit-import qualified Util parserTests :: TestTree parserTests = Test.Tasty.testGroup "parser tests" [ Test.Tasty.testGroup "whitespace"- [ shouldPass+ [ shouldParse "prefix/suffix" "./tests/parser/whitespace.dhall"- , shouldPass+ , shouldParse "block comment" "./tests/parser/blockComment.dhall"- , shouldPass+ , shouldParse "nested block comment" "./tests/parser/nestedBlockComment.dhall"- , shouldPass+ , shouldParse "line comment" "./tests/parser/lineComment.dhall"- , shouldPass+ , shouldParse "Unicode comment" "./tests/parser/unicodeComment.dhall"- , shouldPass+ , shouldParse "whitespace buffet" "./tests/parser/whitespaceBuffet.dhall"- , shouldPass+ , shouldParse "label" "./tests/parser/label.dhall"- , shouldPass+ , shouldParse "quoted label" "./tests/parser/quotedLabel.dhall"- , shouldPass+ , shouldParse "double quoted string" "./tests/parser/doubleQuotedString.dhall"- , shouldPass+ , shouldParse "Unicode double quoted string" "./tests/parser/unicodeDoubleQuotedString.dhall"- , shouldPass+ , shouldParse "escaped double quoted string" "./tests/parser/escapedDoubleQuotedString.dhall"- , shouldPass+ , shouldParse "interpolated double quoted string" "./tests/parser/interpolatedDoubleQuotedString.dhall"- , shouldPass+ , shouldParse "single quoted string" "./tests/parser/singleQuotedString.dhall"- , shouldPass+ , shouldParse "escaped single quoted string" "./tests/parser/escapedSingleQuotedString.dhall"- , shouldPass+ , shouldParse "interpolated single quoted string" "./tests/parser/interpolatedSingleQuotedString.dhall"- , shouldPass+ , shouldParse "double" "./tests/parser/double.dhall"- , shouldPass+ , shouldParse "natural" "./tests/parser/natural.dhall"- , shouldPass+ , shouldParse "identifier" "./tests/parser/identifier.dhall" , shouldParse@@ -83,58 +82,56 @@ , shouldParse "environmentVariables" "./tests/parser/environmentVariables.dhall"- , shouldPass+ , shouldParse "lambda" "./tests/parser/lambda.dhall"- , shouldPass+ , shouldParse "if then else" "./tests/parser/ifThenElse.dhall"- , shouldPass+ , shouldParse "let" "./tests/parser/let.dhall"- , shouldPass+ , shouldParse "forall" "./tests/parser/forall.dhall"- , shouldPass+ , shouldParse "function type" "./tests/parser/functionType.dhall"- , shouldPass+ , shouldParse "operators" "./tests/parser/operators.dhall"- , shouldPass+ , shouldParse "annotations" "./tests/parser/annotations.dhall"- , shouldPass+ , shouldParse "merge" "./tests/parser/merge.dhall"- , shouldPass+ , shouldParse "constructors" "./tests/parser/constructors.dhall"- , shouldPass+ , shouldParse "fields" "./tests/parser/fields.dhall"- , shouldPass+ , shouldParse "record" "./tests/parser/record.dhall"- , shouldPass+ , shouldParse "union" "./tests/parser/union.dhall"- , shouldPass+ , shouldParse "list" "./tests/parser/list.dhall"- , shouldPass+ , shouldParse "builtins" "./tests/parser/builtins.dhall"- , shouldPass+ , shouldParse "large expression" "./tests/parser/largeExpression.dhall"+ , shouldParse+ "names that begin with reserved identifiers"+ "./tests/parser/reservedPrefix.dhall" ] ]--shouldPass :: Text -> Text -> TestTree-shouldPass name code = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do- _ <- Util.code code- return () ) shouldParse :: Text -> FilePath -> TestTree shouldParse name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do
tests/Regression.hs view
@@ -6,13 +6,15 @@ module Regression where import qualified Control.Exception-import qualified Data.Map+import qualified Data.HashMap.Strict.InsOrd import qualified Data.Text.Lazy.IO import qualified Data.Text.Prettyprint.Doc import qualified Data.Text.Prettyprint.Doc.Render.Text import qualified Dhall+import qualified Dhall.Context import qualified Dhall.Core import qualified Dhall.Parser+import qualified Dhall.TypeCheck import qualified System.Timeout import qualified Test.Tasty import qualified Test.Tasty.HUnit@@ -35,6 +37,7 @@ , issue201 , issue209 , issue216+ , issue253 , parsing0 , typeChecking0 , typeChecking1@@ -50,12 +53,12 @@ unnamedFields = Test.Tasty.HUnit.testCase "Unnamed Fields" (do let ty = Dhall.auto @Foo Test.Tasty.HUnit.assertEqual "Good type" (Dhall.expected ty) (Dhall.Core.Union (- Data.Map.fromList [- ("Bar",Dhall.Core.Record (Data.Map.fromList [+ Data.HashMap.Strict.InsOrd.fromList [+ ("Bar",Dhall.Core.Record (Data.HashMap.Strict.InsOrd.fromList [ ("_1",Dhall.Core.Bool),("_2",Dhall.Core.Bool),("_3",Dhall.Core.Bool)]))- , ("Baz",Dhall.Core.Record (Data.Map.fromList [+ , ("Baz",Dhall.Core.Record (Data.HashMap.Strict.InsOrd.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Integer)]))- ,("Foo",Dhall.Core.Record (Data.Map.fromList [+ ,("Foo",Dhall.Core.Record (Data.HashMap.Strict.InsOrd.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool)]))])) let inj = Dhall.inject @Foo@@ -63,7 +66,7 @@ let tu_ty = Dhall.auto @(Integer, Bool) Test.Tasty.HUnit.assertEqual "Auto Tuple" (Dhall.expected tu_ty) (Dhall.Core.Record (- Data.Map.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool) ]))+ Data.HashMap.Strict.InsOrd.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool) ])) let tu_in = Dhall.inject @(Integer, Bool) Test.Tasty.HUnit.assertEqual "Inj. Tuple" (Dhall.declared tu_in) (Dhall.expected tu_ty)@@ -156,6 +159,17 @@ text1 <- Data.Text.Lazy.IO.readFile "./tests/regression/issue216b.dhall" Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 )++issue253 :: TestTree+issue253 = Test.Tasty.HUnit.testCase "Issue #253" (do+ -- Verify that type-checking rejects ill-formed custom contexts+ let context = Dhall.Context.insert "x" "x" Dhall.Context.empty+ let result = Dhall.TypeCheck.typeWith context "x"++ -- If the context is not validated correctly then type-checking will+ -- infinitely loop+ Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $! result)+ return () ) parsing0 :: TestTree parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do
tests/Tests.hs view
@@ -5,6 +5,7 @@ import Parser (parserTests) import Regression (regressionTests) import Tutorial (tutorialTests)+import TypeCheck (typecheckTests) import Format (formatTests) import Test.Tasty @@ -17,6 +18,7 @@ , regressionTests , tutorialTests , formatTests+ , typecheckTests ] main :: IO ()
+ tests/TypeCheck.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE OverloadedStrings #-}++module TypeCheck where++import Data.Monoid (mempty, (<>))+import Data.Text.Lazy (Text)+import Dhall.Core (Expr)+import Dhall.TypeCheck (X)+import Test.Tasty (TestTree)++import qualified Control.Exception+import qualified Data.Text.Lazy+import qualified Dhall.Core+import qualified Dhall.Import+import qualified Dhall.Parser+import qualified Dhall.TypeCheck+import qualified Test.Tasty+import qualified Test.Tasty.HUnit++typecheckTests :: TestTree+typecheckTests =+ Test.Tasty.testGroup "typecheck tests"+ [ should+ "allow type-valued fields in a record"+ "fieldsAreTypes"+ , should+ "allow type-valued alternatives in a union"+ "alternativesAreTypes"+ ]++should :: Text -> Text -> TestTree+should name basename =+ Test.Tasty.HUnit.testCase (Data.Text.Lazy.unpack name) $ do+ let actualCode = "./tests/typecheck/" <> basename <> "A.dhall"+ let expectedCode = "./tests/typecheck/" <> basename <> "B.dhall"++ actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr+ actualResolved <- Dhall.Import.load actualExpr+ actualType <- case Dhall.TypeCheck.typeOf actualResolved of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr+ let actualNormalized = Dhall.Core.normalize actualType :: Expr X X++ expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr+ expectedResolved <- Dhall.Import.load expectedExpr+ let expectedNormalized = Dhall.Core.normalize expectedResolved++ let message = "The expression's type did not match the expected type"+ Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized
+ tests/format/emptyRecordA.dhall view
@@ -0,0 +1,1 @@+{=}
+ tests/format/emptyRecordB.dhall view
@@ -0,0 +1,1 @@+{=}
+ tests/format/escapeNumericLabelA.dhall view
@@ -0,0 +1,1 @@+{ `0` = 0 }
+ tests/format/escapeNumericLabelB.dhall view
@@ -0,0 +1,1 @@+{ `0` = 0 }
+ tests/format/fieldOrderA.dhall view
@@ -0,0 +1,1 @@+{ foo = 1, bar = True }
+ tests/format/fieldOrderB.dhall view
@@ -0,0 +1,1 @@+{ foo = 1, bar = True }
+ tests/format/largeExponentA.dhall view
@@ -0,0 +1,1 @@+[ 1.0, 1e1000000000, 1e-1000000000 ]
+ tests/format/largeExponentB.dhall view
@@ -0,0 +1,1 @@+[ 1.0, 1.0e1000000000, 1.0e-1000000000 ]
+ tests/normalization/doubleShowA.dhall view
@@ -0,0 +1,1 @@+{ example0 = Double/show -0.42, example1 = Double/show 13.37 }
+ tests/normalization/doubleShowB.dhall view
@@ -0,0 +1,1 @@+{ example0 = "-0.42", example1 = "13.37" }
+ tests/normalization/integerShowA.dhall view
@@ -0,0 +1,4 @@+{ example0 = Integer/show 1337+, example1 = Integer/show -42+, example2 = Integer/show 0+}
+ tests/normalization/integerShowB.dhall view
@@ -0,0 +1,1 @@+{ example0 = "1337", example1 = "-42", example2 = "0" }
+ tests/normalization/naturalPlusA.dhall view
@@ -0,0 +1,1 @@++1 + +2
+ tests/normalization/naturalPlusB.dhall view
@@ -0,0 +1,1 @@++3
+ tests/normalization/naturalShowA.dhall view
@@ -0,0 +1,1 @@+Natural/show +42
+ tests/normalization/naturalShowB.dhall view
@@ -0,0 +1,1 @@+"+42"
+ tests/normalization/naturalToIntegerA.dhall view
@@ -0,0 +1,1 @@+Natural/toInteger +1
+ tests/normalization/naturalToIntegerB.dhall view
@@ -0,0 +1,1 @@+1
+ tests/normalization/optionalBuildA.dhall view
@@ -0,0 +1,22 @@+{ example0 =+ Optional/build+ Natural+ ( λ(optional : Type)+ → λ(just : Natural → optional)+ → λ(nothing : optional)+ → just +1+ )+, example1 =+ Optional/build+ Integer+ (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 1)+, example2 =+ λ(id : ∀(a : Type) → a → a)+ → Optional/build+ Bool+ ( λ(optional : Type)+ → λ(just : Bool → optional)+ → λ(nothing : optional)+ → id optional (just True)+ )+}
+ tests/normalization/optionalBuildB.dhall view
@@ -0,0 +1,12 @@+{ example0 = [ +1 ] : Optional Natural+, example1 = [ 1 ] : Optional Integer+, example2 =+ λ(id : ∀(a : Type) → a → a)+ → Optional/build+ Bool+ ( λ(optional : Type)+ → λ(just : Bool → optional)+ → λ(nothing : optional)+ → id optional (just True)+ )+}
+ tests/normalization/optionalBuildFoldA.dhall view
@@ -0,0 +1,11 @@+{ example0 =+ λ ( f+ : ∀(optional : Type)+ → ∀(just : Text → optional)+ → ∀(nothing : optional)+ → optional+ )+ → Optional/fold Text (Optional/build Text f)+, example1 =+ Optional/build Text (Optional/fold Text ([ "foo" ] : Optional Text))+}
+ tests/normalization/optionalBuildFoldB.dhall view
@@ -0,0 +1,10 @@+{ example0 =+ λ ( f+ : ∀(optional : Type)+ → ∀(just : Text → optional)+ → ∀(nothing : optional)+ → optional+ )+ → f+, example1 = [ "foo" ] : Optional Text+}
+ tests/normalization/optionalFoldA.dhall view
@@ -0,0 +1,7 @@+ let f =+ λ(o : Optional Text)+ → Optional/fold Text o Natural (λ(j : Text) → +1) +2++in { example0 = f ([ "foo" ] : Optional Text)+ , example1 = f ([] : Optional Text)+ }
+ tests/normalization/optionalFoldB.dhall view
@@ -0,0 +1,1 @@+{ example0 = +1, example1 = +2 }
+ tests/normalization/remoteSystemsA.dhall view
@@ -0,0 +1,55 @@+ let Text/concatMap =+ https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatMap ++in let Text/concatSep =+ https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatSep ++in let Row =+ { cores :+ Natural+ , host :+ Text+ , key :+ Text+ , mandatoryFeatures :+ List Text+ , platforms :+ List Text+ , speedFactor :+ Natural+ , supportedFeatures :+ List Text+ , user :+ Optional Text+ }++in let renderRow =+ λ ( row+ : Row+ )+ → let host =+ Optional/fold+ Text+ row.user+ Text+ (λ(user : Text) → "${user}@${row.host}")+ row.host+ + in let platforms = Text/concatSep "," row.platforms+ + in let key = row.key+ + in let cores = Integer/show (Natural/toInteger row.cores)+ + in let speedFactor =+ Integer/show (Natural/toInteger row.speedFactor)+ + in let supportedFeatures = Text/concatSep "," row.supportedFeatures+ + in let mandatoryFeatures = Text/concatSep "," row.mandatoryFeatures+ + in ''+ ${host} ${platforms} ${key} ${cores} ${speedFactor} ${supportedFeatures} ${mandatoryFeatures}+ ''++in Text/concatMap Row renderRow
+ tests/normalization/remoteSystemsB.dhall view
@@ -0,0 +1,1 @@+λ(xs : List { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text }) → List/fold { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text } xs Text (λ(x : { cores : Natural, host : Text, key : Text, mandatoryFeatures : List Text, platforms : List Text, speedFactor : Natural, supportedFeatures : List Text, user : Optional Text }) → λ(y : Text) → "${Optional/fold Text x.user Text (λ(user : Text) → "${user}@${x.host}") x.host} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.platforms < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text} ${x.key} ${Integer/show (Natural/toInteger x.cores)} ${Integer/show (Natural/toInteger x.speedFactor)} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.supportedFeatures < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text} ${merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } (List/fold Text x.mandatoryFeatures < Empty : {} | NonEmpty : Text > (λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} >, NonEmpty = λ(result : Text) → < NonEmpty = element ++ "," ++ result | Empty : {} > } status : < Empty : {} | NonEmpty : Text >) < Empty = {=} | NonEmpty : Text >) : Text}\n" ++ y) ""
+ tests/parser/reservedPrefix.dhall view
@@ -0,0 +1,1 @@+let TypeSynonym = Integer in 1 : TypeSynonym
+ tests/typecheck/alternativesAreTypesA.dhall view
@@ -0,0 +1,1 @@+< Left = List | Right : Type >
+ tests/typecheck/alternativesAreTypesB.dhall view
@@ -0,0 +1,1 @@+< Left : Type → Type | Right : Type >
+ tests/typecheck/fieldsAreTypesA.dhall view
@@ -0,0 +1,1 @@+{ x = Bool, y = List }
+ tests/typecheck/fieldsAreTypesB.dhall view
@@ -0,0 +1,1 @@+{ x : Type, y : Type → Type }