diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/dhall-format/Main.hs b/dhall-format/Main.hs --- a/dhall-format/Main.hs +++ b/dhall-format/Main.hs @@ -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 "") diff --git a/dhall-hash/Main.hs b/dhall-hash/Main.hs --- a/dhall-hash/Main.hs +++ b/dhall-hash/Main.hs @@ -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" diff --git a/dhall-repl/Main.hs b/dhall-repl/Main.hs new file mode 100644 --- /dev/null +++ b/dhall-repl/Main.hs @@ -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 diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -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 diff --git a/dhall/Main.hs b/dhall/Main.hs --- a/dhall/Main.hs +++ b/dhall/Main.hs @@ -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') ) diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -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 diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs --- a/src/Dhall/Context.hs +++ b/src/Dhall/Context.hs @@ -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 diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -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" ] diff --git a/src/Dhall/Core.hs-boot b/src/Dhall/Core.hs-boot new file mode 100644 --- /dev/null +++ b/src/Dhall/Core.hs-boot @@ -0,0 +1,7 @@ +module Dhall.Core where + +data Const + +data Var + +data Expr s a diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -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)] ) ) diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -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) diff --git a/src/Dhall/Pretty.hs b/src/Dhall/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Pretty.hs @@ -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 diff --git a/src/Dhall/Pretty/Internal.hs b/src/Dhall/Pretty/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Pretty/Internal.hs @@ -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) + <> " >" diff --git a/src/Dhall/Pretty/Internal.hs-boot b/src/Dhall/Pretty/Internal.hs-boot new file mode 100644 --- /dev/null +++ b/src/Dhall/Pretty/Internal.hs-boot @@ -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 diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -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 () diff --git a/tests/Format.hs b/tests/Format.hs --- a/tests/Format.hs +++ b/tests/Format.hs @@ -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 diff --git a/tests/Normalization.hs b/tests/Normalization.hs --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -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") diff --git a/tests/Parser.hs b/tests/Parser.hs --- a/tests/Parser.hs +++ b/tests/Parser.hs @@ -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 diff --git a/tests/Regression.hs b/tests/Regression.hs --- a/tests/Regression.hs +++ b/tests/Regression.hs @@ -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 diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -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 () diff --git a/tests/TypeCheck.hs b/tests/TypeCheck.hs new file mode 100644 --- /dev/null +++ b/tests/TypeCheck.hs @@ -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 diff --git a/tests/format/emptyRecordA.dhall b/tests/format/emptyRecordA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/emptyRecordA.dhall @@ -0,0 +1,1 @@ +{=} diff --git a/tests/format/emptyRecordB.dhall b/tests/format/emptyRecordB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/emptyRecordB.dhall @@ -0,0 +1,1 @@ +{=} diff --git a/tests/format/escapeNumericLabelA.dhall b/tests/format/escapeNumericLabelA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/escapeNumericLabelA.dhall @@ -0,0 +1,1 @@ +{ `0` = 0 } diff --git a/tests/format/escapeNumericLabelB.dhall b/tests/format/escapeNumericLabelB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/escapeNumericLabelB.dhall @@ -0,0 +1,1 @@ +{ `0` = 0 } diff --git a/tests/format/fieldOrderA.dhall b/tests/format/fieldOrderA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/fieldOrderA.dhall @@ -0,0 +1,1 @@ +{ foo = 1, bar = True } diff --git a/tests/format/fieldOrderB.dhall b/tests/format/fieldOrderB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/fieldOrderB.dhall @@ -0,0 +1,1 @@ +{ foo = 1, bar = True } diff --git a/tests/format/largeExponentA.dhall b/tests/format/largeExponentA.dhall new file mode 100644 --- /dev/null +++ b/tests/format/largeExponentA.dhall @@ -0,0 +1,1 @@ +[ 1.0, 1e1000000000, 1e-1000000000 ] diff --git a/tests/format/largeExponentB.dhall b/tests/format/largeExponentB.dhall new file mode 100644 --- /dev/null +++ b/tests/format/largeExponentB.dhall @@ -0,0 +1,1 @@ +[ 1.0, 1.0e1000000000, 1.0e-1000000000 ] diff --git a/tests/normalization/doubleShowA.dhall b/tests/normalization/doubleShowA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/doubleShowA.dhall @@ -0,0 +1,1 @@ +{ example0 = Double/show -0.42, example1 = Double/show 13.37 } diff --git a/tests/normalization/doubleShowB.dhall b/tests/normalization/doubleShowB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/doubleShowB.dhall @@ -0,0 +1,1 @@ +{ example0 = "-0.42", example1 = "13.37" } diff --git a/tests/normalization/integerShowA.dhall b/tests/normalization/integerShowA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/integerShowA.dhall @@ -0,0 +1,4 @@ +{ example0 = Integer/show 1337 +, example1 = Integer/show -42 +, example2 = Integer/show 0 +} diff --git a/tests/normalization/integerShowB.dhall b/tests/normalization/integerShowB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/integerShowB.dhall @@ -0,0 +1,1 @@ +{ example0 = "1337", example1 = "-42", example2 = "0" } diff --git a/tests/normalization/naturalPlusA.dhall b/tests/normalization/naturalPlusA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalPlusA.dhall @@ -0,0 +1,1 @@ ++1 + +2 diff --git a/tests/normalization/naturalPlusB.dhall b/tests/normalization/naturalPlusB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalPlusB.dhall @@ -0,0 +1,1 @@ ++3 diff --git a/tests/normalization/naturalShowA.dhall b/tests/normalization/naturalShowA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalShowA.dhall @@ -0,0 +1,1 @@ +Natural/show +42 diff --git a/tests/normalization/naturalShowB.dhall b/tests/normalization/naturalShowB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalShowB.dhall @@ -0,0 +1,1 @@ +"+42" diff --git a/tests/normalization/naturalToIntegerA.dhall b/tests/normalization/naturalToIntegerA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalToIntegerA.dhall @@ -0,0 +1,1 @@ +Natural/toInteger +1 diff --git a/tests/normalization/naturalToIntegerB.dhall b/tests/normalization/naturalToIntegerB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/naturalToIntegerB.dhall @@ -0,0 +1,1 @@ +1 diff --git a/tests/normalization/optionalBuildA.dhall b/tests/normalization/optionalBuildA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalBuildA.dhall @@ -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) + ) +} diff --git a/tests/normalization/optionalBuildB.dhall b/tests/normalization/optionalBuildB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalBuildB.dhall @@ -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) + ) +} diff --git a/tests/normalization/optionalBuildFoldA.dhall b/tests/normalization/optionalBuildFoldA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalBuildFoldA.dhall @@ -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)) +} diff --git a/tests/normalization/optionalBuildFoldB.dhall b/tests/normalization/optionalBuildFoldB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalBuildFoldB.dhall @@ -0,0 +1,10 @@ +{ example0 = + λ ( f + : ∀(optional : Type) + → ∀(just : Text → optional) + → ∀(nothing : optional) + → optional + ) + → f +, example1 = [ "foo" ] : Optional Text +} diff --git a/tests/normalization/optionalFoldA.dhall b/tests/normalization/optionalFoldA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalFoldA.dhall @@ -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) + } diff --git a/tests/normalization/optionalFoldB.dhall b/tests/normalization/optionalFoldB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/optionalFoldB.dhall @@ -0,0 +1,1 @@ +{ example0 = +1, example1 = +2 } diff --git a/tests/normalization/remoteSystemsA.dhall b/tests/normalization/remoteSystemsA.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/remoteSystemsA.dhall @@ -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 diff --git a/tests/normalization/remoteSystemsB.dhall b/tests/normalization/remoteSystemsB.dhall new file mode 100644 --- /dev/null +++ b/tests/normalization/remoteSystemsB.dhall @@ -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) "" diff --git a/tests/parser/reservedPrefix.dhall b/tests/parser/reservedPrefix.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/reservedPrefix.dhall @@ -0,0 +1,1 @@ +let TypeSynonym = Integer in 1 : TypeSynonym diff --git a/tests/typecheck/alternativesAreTypesA.dhall b/tests/typecheck/alternativesAreTypesA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/alternativesAreTypesA.dhall @@ -0,0 +1,1 @@ +< Left = List | Right : Type > diff --git a/tests/typecheck/alternativesAreTypesB.dhall b/tests/typecheck/alternativesAreTypesB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/alternativesAreTypesB.dhall @@ -0,0 +1,1 @@ +< Left : Type → Type | Right : Type > diff --git a/tests/typecheck/fieldsAreTypesA.dhall b/tests/typecheck/fieldsAreTypesA.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/fieldsAreTypesA.dhall @@ -0,0 +1,1 @@ +{ x = Bool, y = List } diff --git a/tests/typecheck/fieldsAreTypesB.dhall b/tests/typecheck/fieldsAreTypesB.dhall new file mode 100644 --- /dev/null +++ b/tests/typecheck/fieldsAreTypesB.dhall @@ -0,0 +1,1 @@ +{ x : Type, y : Type → Type }