diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,45 @@ +1.9.0 + +* Feature: BREAKING CHANGE TO LANGUAGE AND API: Add `constructors` keyword + * This new keyword generates constructors from a union type + * See the updated Haskell tutorial for more details + * This means that `constructors` is now a reserved keyword + * This adds a new `Constructors` constructor to the `Expr` type + * See: https://github.com/dhall-lang/dhall-haskell/pull/199 +* Feature: BREAKING CHANGE TO THE API: `dhall-format` preserves interpolation + * This changes the `TextLit` constructor to represent an interpolated `Text` + literal + * See: https://github.com/dhall-lang/dhall-haskell/pull/220 +* Feature: You can now define type synonyms using `let` + * See: https://github.com/dhall-lang/dhall-haskell/pull/202 +* Feature: Extend valid set of quoted labels + * See: https://github.com/dhall-lang/dhall-lang/pull/65 + * See: https://github.com/dhall-lang/dhall-lang/pull/77 +* Performance: Improve startup time when importing files, but not URLs + * See: https://github.com/dhall-lang/dhall-haskell/pull/194 +* Security: `localhost`/`127.0.0.1` imports no longer count as local imports + * Specifically: they cannot import environment variables or files + * See: https://github.com/dhall-lang/dhall-haskell/pull/197 +* Security: Fix potential type-checking bug + * See: https://github.com/dhall-lang/dhall-haskell/pull/198 +* Fix: BREAKING CHANGE TO API: Improve localization of error messages + * This required fixing the type of `normalize`/`shift`/`subst` to preserve + the first type parameter of `Expr` (i.e. they no longer delete `Note` + constructors) + * A new `denote` function was added for the explicit purpose of deleting + `Note` constructors + * See: https://github.com/dhall-lang/dhall-haskell/pull/218 +* Expose `MissingEnvironmentVariable` exception type + * See: https://github.com/dhall-lang/dhall-haskell/pull/196 +* Add `genericAuto` + * See: https://github.com/dhall-lang/dhall-haskell/pull/195 +* Add `inputWith` + * See: https://github.com/dhall-lang/dhall-haskell/pull/222 +* Add`loadWithContext` + * See: https://github.com/dhall-lang/dhall-haskell/pull/215 +* Add `pair`/`unit`/`string`/`list` + * See: https://github.com/dhall-lang/dhall-haskell/pull/227 + 1.8.2 * Add `typeWithA` for type-checking custom `Embed`ded values diff --git a/dhall-format/Main.hs b/dhall-format/Main.hs --- a/dhall-format/Main.hs +++ b/dhall-format/Main.hs @@ -20,7 +20,6 @@ subexpressions then you will need to split them into a separate file for now * Preserving multi-line strings (this reduces them to ordinary strings) - * Preserving string interpolation (this expands interpolation to @++@) See the @Dhall.Tutorial@ module for example usage -} diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -1,5 +1,5 @@ Name: dhall -Version: 1.8.2 +Version: 1.9.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1 @@ -83,6 +83,7 @@ Prelude/Text/concatSep tests/parser/*.dhall tests/regression/*.dhall + tests/tutorial/*.dhall Source-Repository head Type: git @@ -162,6 +163,8 @@ optparse-generic >= 1.1.1 && < 1.3, trifecta >= 1.6 && < 1.8, text >= 0.11.1.0 && < 1.3 + Other-Modules: + Paths_dhall Test-Suite test Type: exitcode-stdio-1.0 @@ -178,8 +181,10 @@ Build-Depends: base >= 4 && < 5 , containers >= 0.5.0.0 && < 0.6 , + deepseq >= 1.2.0.1 && < 1.5 , dhall , - tasty >= 0.11.2 && < 0.13, + 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/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -5,6 +5,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} @@ -18,6 +19,7 @@ ( -- * Input input + , inputWith , detailed -- * Types @@ -26,6 +28,7 @@ , Interpret(..) , InvalidType(..) , auto + , genericAuto , InterpretOptions(..) , defaultInterpretOptions , bool @@ -36,6 +39,10 @@ , strictText , maybe , vector + , list + , unit + , string + , pair , GenericInterpret(..) , Inject(..) @@ -61,7 +68,7 @@ import Data.Typeable (Typeable) import Data.Vector (Vector) import Data.Word (Word8, Word16, Word32, Word64) -import Dhall.Core (Expr(..)) +import Dhall.Core (Expr(..), Chunks(..)) import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..)) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) @@ -81,6 +88,7 @@ import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding import qualified Data.Vector +import qualified Dhall.Context import qualified Dhall.Core import qualified Dhall.Import import qualified Dhall.Parser @@ -133,10 +141,26 @@ -- ^ The Dhall program -> IO a -- ^ The decoded value in Haskell -input (Type {..}) txt = do +input ty txt = + inputWith ty Dhall.Context.empty (const Nothing) txt + +{-| Extend 'input' with a custom typing context and normalization process. + +-} +inputWith + :: Type a + -- ^ The type of value to decode from Dhall to Haskell + -> Dhall.Context.Context (Expr Src X) + -- ^ The starting context for type-checking + -> Dhall.Core.Normalizer X + -> Text + -- ^ The Dhall program + -> IO a + -- ^ The decoded value in Haskell +inputWith (Type {..}) ctx n txt = do let delta = Directed "(input)" 0 0 0 0 expr <- throws (Dhall.Parser.exprFromText delta txt) - expr' <- Dhall.Import.load expr + expr' <- Dhall.Import.loadWithContext ctx expr let suffix = ( Data.ByteString.Lazy.toStrict . Data.Text.Lazy.Encoding.encodeUtf8 @@ -150,8 +174,8 @@ bytes' = bytes <> " : " <> suffix _ -> Annot expr' expected - _ <- throws (Dhall.TypeCheck.typeOf annot) - case extract (Dhall.Core.normalize expr') of + _ <- throws (Dhall.TypeCheck.typeWith ctx annot) + case extract (Dhall.Core.normalizeWith n expr') of Just x -> return x Nothing -> Control.Exception.throwIO InvalidType @@ -376,8 +400,8 @@ lazyText :: Type Text lazyText = Type {..} where - extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t) - extract _ = empty + extract (TextLit (Chunks [] t)) = pure (Data.Text.Lazy.Builder.toLazyText t) + extract _ = empty expected = Text @@ -417,6 +441,52 @@ expectedOut = App List expectedIn +{-| Decode a list + +>>> input (list integer) "[1, 2, 3]" +[1,2,3] +-} +list :: Type a -> Type [a] +list = fmap Data.Vector.toList . vector + +{-| Decode `()` from an empty record. + +>>> input unit "{=}" +() +-} +unit :: Type () +unit = Type extractOut expectedOut + where + extractOut (RecordLit fields) | Data.Map.null fields = return () + extractOut _ = Nothing + + expectedOut = Record Data.Map.empty + +{-| Decode a `String` + +>>> input string "\"ABC\"" +"ABC" + +"-} +string :: Type String +string = Data.Text.Lazy.unpack <$> lazyText + +{-| Given a pair of `Type`s, decode a tuple-record into their pairing. + +>>> input (pair natural bool) "{ _1 = +42, _2 = False }" +(42, False) +-} +pair :: Type a -> Type b -> Type (a, b) +pair l r = Type extractOut expectedOut + where + extractOut (RecordLit fields) = + (,) <$> ( Data.Map.lookup "_1" fields >>= extract l ) + <*> ( Data.Map.lookup "_2" fields >>= extract r ) + extractOut _ = Nothing + + expectedOut = Record (Data.Map.fromList [("_1", expected l) + ,("_2", expected r)]) + {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input` @@ -482,6 +552,14 @@ auto :: Interpret a => Type a auto = autoWith defaultInterpretOptions +{-| `genericAuto` is the default implementation for `auto` if you derive + `Interpret`. The difference is that you can use `genericAuto` without + having to explicitly provide an `Interpret` instance for a type as long as + the type derives `Generic` +-} +genericAuto :: (Generic a, GenericInterpret (Rep a)) => Type a +genericAuto = fmap to (evalState (genericAutoWith defaultInterpretOptions) 1) + {-| Use these options to tweak how Dhall derives a generic implementation of `Interpret` -} @@ -692,14 +770,15 @@ instance Inject Text where injectWith _ = InputType {..} where - embed text = TextLit (Data.Text.Lazy.Builder.fromLazyText text) + embed text = + TextLit (Chunks [] (Data.Text.Lazy.Builder.fromLazyText text)) declared = Text instance Inject Data.Text.Text where injectWith _ = InputType {..} where - embed text = TextLit (Data.Text.Lazy.Builder.fromText text) + embed text = TextLit (Chunks [] (Data.Text.Lazy.Builder.fromText text)) declared = Text diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -23,6 +23,7 @@ , PathMode(..) , Path(..) , Var(..) + , Chunks(..) , Expr(..) -- * Normalization @@ -33,6 +34,7 @@ , shift , isNormalized , isNormalizedWith + , denote -- * Pretty-printing , pretty @@ -40,6 +42,7 @@ -- * Miscellaneous , internalError , reservedIdentifiers + , escapeText ) where #if MIN_VERSION_base(4,8,0) @@ -276,8 +279,8 @@ | DoubleShow -- | > Text ~ Text | Text - -- | > TextLit t ~ t - | TextLit Builder + -- | > 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 @@ -325,6 +328,8 @@ -- | > 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 @@ -341,130 +346,146 @@ 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 a >>= _ = TextLit a - 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) - Field a b >>= k = Field (a >>= k) b - Note a b >>= k = Note a (b >>= k) - Embed a >>= k = k a + 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 _ (TextLit a ) = TextLit a - 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 (Field a b ) = Field (first k a) b - first k (Note a b ) = Note (k a) (first k b) - first _ (Embed a ) = Embed a + 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 @@ -573,9 +594,11 @@ prettyLabel :: Text -> Doc ann prettyLabel a = - if Data.HashSet.member a reservedIdentifiers + 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 @@ -586,9 +609,14 @@ prettyDouble :: Double -> Doc ann prettyDouble = Pretty.pretty -prettyText :: Builder -> Doc ann -prettyText a = Pretty.pretty (Builder.toLazyText (buildText a)) +prettyChunks :: Pretty a => Chunks s a -> Doc ann +prettyChunks (Chunks a b) = + "\"" <> foldMap prettyChunk a <> prettyText b <> "\"" + where + 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" @@ -897,16 +925,19 @@ prettyExprD a0 prettyExprD :: Pretty a => Expr s a -> Doc ann -prettyExprD a0@(App _ _) = - enclose' "" "" " " "" (fmap duplicate (reverse (docs a0))) +prettyExprD a0 = case a0 of + App _ _ -> result + Constructors _ -> result + Note _ b -> prettyExprD b + _ -> prettyExprE a0 where - docs (App a b) = prettyExprE b : docs a - docs (Note _ b) = docs b - docs b = [ prettyExprE b ] -prettyExprD (Note _ b) = prettyExprD b -prettyExprD a0 = - prettyExprE a0 + 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 @@ -978,7 +1009,7 @@ prettyExprF (DoubleLit a) = prettyDouble a prettyExprF (TextLit a) = - prettyText a + prettyChunks a prettyExprF (Record a) = prettyRecord a prettyExprF (RecordLit a) = @@ -1059,9 +1090,11 @@ -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder buildLabel label = - if Data.HashSet.member label reservedIdentifiers + 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 @@ -1076,9 +1109,17 @@ buildDouble a = build (show a) -- | Builder corresponding to the @text@ token in "Dhall.Parser" -buildText :: Builder -> Builder -buildText a = "\"" <> Builder.fromLazyText (Text.concatMap adapt text) <> "\"" +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 +-- +-- 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 | '\x23' <= c && c <= '\x5B' = Text.singleton c @@ -1239,9 +1280,10 @@ -- | 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 (Note _ b) = buildExprD b -buildExprD a = buildExprE a +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 @@ -1316,7 +1358,7 @@ buildExprF (DoubleLit a) = buildDouble a buildExprF (TextLit a) = - buildText a + buildChunks a buildExprF (Record a) = buildRecord a buildExprF (RecordLit a) = @@ -1491,7 +1533,7 @@ 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 t a +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 @@ -1571,7 +1613,9 @@ shift _ _ (DoubleLit a) = DoubleLit a shift _ _ DoubleShow = DoubleShow shift _ _ Text = Text -shift _ _ (TextLit a) = TextLit a +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 @@ -1625,10 +1669,13 @@ 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 _ b) = b' +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 @@ -1639,7 +1686,7 @@ > subst x C B ~ B[x := C] -} -subst :: Var -> Expr s a -> Expr t a -> Expr s a +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 @@ -1715,7 +1762,9 @@ subst _ _ (DoubleLit a) = DoubleLit a subst _ _ DoubleShow = DoubleShow subst _ _ Text = Text -subst _ _ (TextLit a) = TextLit a +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 @@ -1760,10 +1809,13 @@ 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 _ b) = b' +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 @@ -1804,6 +1856,68 @@ 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. @@ -1820,7 +1934,7 @@ -} normalizeWith :: Normalizer a -> Expr s a -> Expr t a -normalizeWith ctx e0 = loop (shift 0 "_" e0) +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 @@ -1891,9 +2005,12 @@ 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 ("+" <> buildNatural n) - App IntegerShow (IntegerLit n) -> TextLit (buildNumber n) - App DoubleShow (DoubleLit n) -> TextLit (buildDouble 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' @@ -2064,7 +2181,16 @@ DoubleLit n -> DoubleLit n DoubleShow -> DoubleShow Text -> Text - TextLit t -> TextLit t + 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 -> @@ -2151,6 +2277,18 @@ 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 -> @@ -2175,7 +2313,7 @@ -- | Quickly check if an expression is in normal form isNormalized :: Expr s a -> Bool -isNormalized e = case shift 0 "_" e of -- `shift` is a hack to delete `Note` +isNormalized e = case denote e of Const _ -> True Var _ -> True Lam _ a b -> isNormalized a && isNormalized b @@ -2305,7 +2443,7 @@ DoubleLit _ -> True DoubleShow -> True Text -> True - TextLit _ -> True + TextLit (Chunks xys _) -> all (all isNormalized) xys TextAppend x y -> isNormalized x && isNormalized y && case x of TextLit _ -> @@ -2361,6 +2499,10 @@ Nothing -> True _ -> True _ -> True + Constructors t -> isNormalized t && + case t of + Union _ -> False + _ -> True Field r x -> isNormalized r && case r of RecordLit kvs -> diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -104,6 +104,7 @@ exprFromPath , load , loadWith + , loadWithContext , hashExpression , hashExpressionToCode , Cycle(..) @@ -111,6 +112,7 @@ , Imported(..) , PrettyHttpException(..) , MissingFile(..) + , MissingEnvironmentVariable(..) ) where import Control.Applicative (empty) @@ -119,7 +121,6 @@ import Control.Lens (Lens', zoom) import Control.Monad (join) import Control.Monad.Catch (throwM, MonadCatch(catch)) -import Control.Monad.Trans.Class (lift) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Data.ByteString.Lazy (ByteString) @@ -137,6 +138,7 @@ import Filesystem.Path ((), FilePath) import Dhall.Core ( Expr(..) + , Chunks(..) , HasHome(..) , PathHashed(..) , PathMode(..) @@ -338,6 +340,9 @@ , _manager :: Maybe Manager } +emptyStatus :: Status +emptyStatus = Status [] Map.empty Nothing + canonicalizeAll :: [Path] -> [Path] canonicalizeAll = map canonicalizePath . List.tails @@ -491,8 +496,8 @@ :: Expr s a -> Maybe (CI Data.ByteString.ByteString, Data.ByteString.ByteString) toHeader (RecordLit m) = do - TextLit keyBuilder <- Map.lookup "header" m - TextLit valueBuilder <- Map.lookup "value" m + TextLit (Chunks [] keyBuilder ) <- Map.lookup "header" m + TextLit (Chunks [] valueBuilder) <- Map.lookup "value" m let keyText = Text.toStrict (Builder.toLazyText keyBuilder ) let valueText = Text.toStrict (Builder.toLazyText valueBuilder) let keyBytes = Data.Text.Encoding.encodeUtf8 keyText @@ -582,12 +587,12 @@ bytesPath = Data.Text.Encoding.encodeUtf8 textPath -- | Parse an expression from a `Path` containing a Dhall program -exprFromPath :: Manager -> Path -> IO (Expr Src Path) -exprFromPath m (Path {..}) = case pathType of - File hasHome file -> do +exprFromPath :: Path -> StateT Status IO (Expr Src Path) +exprFromPath (Path {..}) = case pathType of + File hasHome file -> liftIO (do path <- case hasHome of Home -> do - home <- liftIO Filesystem.getHomeDirectory + home <- Filesystem.getHomeDirectory return (home file) Homeless -> do return file @@ -597,7 +602,7 @@ exists <- Filesystem.isFile path if exists then return () - else Control.Exception.throwIO (MissingFile path) + else throwIO (MissingFile path) -- Unfortunately, GHC throws an `InappropriateType` exception -- when trying to read a directory, but does not export the @@ -618,9 +623,10 @@ RawText -> do let pathString = Filesystem.Path.CurrentOS.encodeString path text <- Data.Text.IO.readFile pathString - return (TextLit (build text)) + return (TextLit (Chunks [] (build text))) ) URL url headerPath -> do - request <- HTTP.parseUrlThrow (Text.unpack url) + m <- needManager + request <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) #if MIN_VERSION_http_client(0,5,0) @@ -637,7 +643,7 @@ requestWithHeaders <- case headerPath of Nothing -> return request Just path -> do - expr <- load (Embed (Path path Code)) + expr <- loadStaticIO Dhall.Context.empty (Path path Code) let expected :: Expr Src X expected = App List @@ -660,22 +666,24 @@ _ -> Annot expr expected case Dhall.TypeCheck.typeOf annot of - Left err -> Control.Exception.throwIO err + Left err -> liftIO (throwIO err) Right _ -> return () let expr' = Dhall.Core.normalize expr headers <- case toHeaders expr' of - Just headers -> return headers - Nothing -> Control.Exception.throwIO InternalError + Just headers -> do + return headers + Nothing -> do + liftIO (throwIO InternalError) let requestWithHeaders = request { HTTP.requestHeaders = headers } return requestWithHeaders - response <- HTTP.httpLbs requestWithHeaders m `catch` handler + response <- liftIO (HTTP.httpLbs requestWithHeaders m `catch` handler) let bytes = HTTP.responseBody response text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of - Left err -> throwIO err + Left err -> liftIO (throwIO err) Right text -> return text case pathMode of @@ -690,27 +698,26 @@ -- a directory list let err' = ParseError (Text.Trifecta._errDoc err) - request' <- HTTP.parseUrlThrow (Text.unpack url) + request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) let request'' = request' { HTTP.path = HTTP.path request' <> "/@" } - response' <- HTTP.httpLbs request'' m - `onException` throwIO err' + response' <- liftIO (HTTP.httpLbs request'' m `onException` throwIO err' ) let bytes' = HTTP.responseBody response' text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of - Left _ -> throwIO err' + Left _ -> liftIO (throwIO err') Right text' -> return text' case Text.Trifecta.parseString parser delta (Text.unpack text') of - Failure _ -> throwIO err' + Failure _ -> liftIO (throwIO err') Success expr -> return expr Success expr -> return expr RawText -> do - return (TextLit (build text)) - Env env -> do + return (TextLit (Chunks [] (build text))) + Env env -> liftIO (do x <- System.Environment.lookupEnv (Text.unpack env) case x of Just str -> do @@ -724,8 +731,8 @@ throwIO (ParseError (Text.Trifecta._errDoc errInfo)) Success expr -> do return expr - RawText -> return (TextLit (build str)) - Nothing -> throwIO (MissingEnvironmentVariable env) + RawText -> return (TextLit (Chunks [] (build str))) + Nothing -> throwIO (MissingEnvironmentVariable env) ) where PathHashed {..} = pathHashed @@ -740,41 +747,56 @@ This also returns the true final path (i.e. explicit "/@" at the end for directories) -} -loadDynamic :: forall m . MonadCatch m => (Path -> m (Expr Src Path)) - -> Path -> StateT Status m (Expr Src Path) +loadDynamic + :: forall m . MonadCatch m + => (Path -> StateT Status m (Expr Src Path)) + -> Path + -> StateT Status m (Expr Src Path) loadDynamic from_path p = do paths <- zoom stack State.get - let handler :: SomeException -> m (Expr Src Path) + let handler :: SomeException -> StateT Status m (Expr Src Path) handler e = throwM (Imported (p:paths) e) - lift (from_path (canonicalizePath (p:paths)) `catch` handler) + from_path (canonicalizePath (p:paths)) `catch` handler -loadStaticIO :: Dhall.Context.Context (Expr Src X) -> Path -> StateT Status IO (Expr Src X) -loadStaticIO ctx path = do - m <- needManager - loadStaticWith (exprFromPath m) ctx path +loadStaticIO + :: Dhall.Context.Context (Expr Src X) + -> Path + -> StateT Status IO (Expr Src X) +loadStaticIO = loadStaticWith exprFromPath -- | Resolve all imports within an expression using a custom typing context and Path -- resolving callback in arbitrary `MonadCatch` monad. -loadWith :: MonadCatch m => (Path -> m (Expr Src Path)) - -> Dhall.Context.Context (Expr Src X) -> Expr Src Path -> m (Expr Src X) +loadWith + :: MonadCatch m + => (Path -> StateT Status m (Expr Src Path)) + -> Dhall.Context.Context (Expr Src X) + -> Expr Src Path + -> m (Expr Src X) loadWith from_path ctx = evalStatus (loadStaticWith from_path ctx) -loadStaticWith :: MonadCatch m => (Path -> m (Expr Src Path)) - -> Dhall.Context.Context (Expr Src X) -> Path -> StateT Status m (Expr Src X) +-- | Resolve all imports within an expression using a custom typing context. +-- +-- @load = loadWithContext Dhall.Context.empty@ +loadWithContext + :: Dhall.Context.Context (Expr Src X) + -> Expr Src Path + -> IO (Expr Src X) +loadWithContext ctx = evalStatus (loadStaticIO ctx) + +loadStaticWith + :: MonadCatch m + => (Path -> StateT Status m (Expr Src Path)) + -> Dhall.Context.Context (Expr Src X) + -> Path + -> StateT Status m (Expr Src X) loadStaticWith from_path ctx path = do paths <- zoom stack State.get - let local (Path (PathHashed _ (URL url _)) _) = - case HTTP.parseUrlThrow (Text.unpack url) of - Nothing -> False - Just request -> case HTTP.host request of - "127.0.0.1" -> True - "localhost" -> True - _ -> False - local (Path (PathHashed _ (File _ _ )) _) = True - local (Path (PathHashed _ (Env _ )) _) = True + let local (Path (PathHashed _ (URL _ _ )) _) = False + local (Path (PathHashed _ (File _ _)) _) = True + local (Path (PathHashed _ (Env _ )) _) = True let parent = canonicalizePath paths let here = canonicalizePath (path:paths) @@ -831,15 +853,14 @@ return expr -evalStatus :: (Traversable f, Monad m, Monad f) => - (a -> StateT Status m (f b)) -> f a -> m (f b) -evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) status - where - status = Status [] Map.empty Nothing +evalStatus + :: (Traversable f, Monad m, Monad f) + => (a -> StateT Status m (f b)) -> f a -> m (f b) +evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) emptyStatus -- | Resolve all imports within an expression load :: Expr Src Path -> IO (Expr Src X) -load = evalStatus (loadStaticIO Dhall.Context.empty) +load = loadWithContext Dhall.Context.empty -- | Hash a fully resolved expression hashExpression :: Expr s X -> Data.ByteString.ByteString diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -237,16 +237,12 @@ simpleLabel :: Parser Text simpleLabel = try (do - text <- quotedLabel - Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers)) - return text ) - -quotedLabel :: Parser Text -quotedLabel = try (do c <- Text.Parser.Char.satisfy headCharacter cs <- many (Text.Parser.Char.satisfy tailCharacter) let string = c:cs - return (Data.Text.Lazy.pack string) ) + let text = Data.Text.Lazy.pack string + Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers)) + return text ) where headCharacter c = alpha c || c == '_' @@ -255,9 +251,11 @@ backtickLabel :: Parser Text backtickLabel = do _ <- Text.Parser.Char.char '`' - t <- quotedLabel + t <- some (Text.Parser.Char.satisfy predicate) _ <- Text.Parser.Char.char '`' - return t + return (Data.Text.Lazy.pack t) + where + predicate c = alpha c || digit c || elem c ("-/_:." :: String) label :: Parser Text label = (do @@ -265,16 +263,7 @@ whitespace return t ) "label" --- | Combine consecutive chunks to eliminate gratuitous appends -textAppend :: Expr Src a -> Expr Src a -> Expr Src a -textAppend (TextLit a) (TextLit b) = - TextLit (a <> b) -textAppend (TextLit a) (TextAppend (TextLit b) c) = - TextAppend (TextLit (a <> b)) c -textAppend a b = - TextAppend a b - -doubleQuotedChunk :: Parser a -> Parser (Expr Src a) +doubleQuotedChunk :: Parser a -> Parser (Chunks Src a) doubleQuotedChunk embedded = choice [ interpolation @@ -286,11 +275,11 @@ _ <- Text.Parser.Char.text "${" e <- expression embedded _ <- Text.Parser.Char.char '}' - return e + return (Chunks [(mempty, e)] mempty) unescapedCharacter = do c <- Text.Parser.Char.satisfy predicate - return (TextLit (Data.Text.Lazy.Builder.singleton c)) + return (Chunks [] (Data.Text.Lazy.Builder.singleton c)) where predicate c = ('\x20' <= c && c <= '\x21' ) @@ -311,7 +300,7 @@ , tab , unicode ] - return (TextLit (Data.Text.Lazy.Builder.singleton c)) + return (Chunks [] (Data.Text.Lazy.Builder.singleton c)) where quotationMark = Text.Parser.Char.char '"' @@ -340,25 +329,29 @@ let n = ((n0 * 16 + n1) * 16 + n2) * 16 + n3 return (Data.Char.chr n) -doubleQuotedLiteral :: Parser a -> Parser (Expr Src a) +doubleQuotedLiteral :: Parser a -> Parser (Chunks Src a) doubleQuotedLiteral embedded = do _ <- Text.Parser.Char.char '"' chunks <- many (doubleQuotedChunk embedded) _ <- Text.Parser.Char.char '"' - return (foldr textAppend (TextLit "") chunks) + return (mconcat chunks) -dedent :: Expr Src a -> Expr Src a -dedent expr0 = process trimBegin expr0 +-- | Similar to `Dhall.Core.buildChunks` except that this doesn't bother to +-- render interpolated expressions to avoid a `Buildable a` constraint. The +-- interpolated contents are not necessary for computing how much to dedent a +-- multi-line string +-- +-- This also doesn't include the surrounding quotes since they would interfere +-- with the whitespace detection +buildChunks :: Chunks s a -> Builder +buildChunks (Chunks a b) = foldMap buildChunk a <> escapeText b where - -- This treats variable interpolation as breaking leading whitespace for the - -- purposes of computing the shortest leading whitespace. The "${x}" - -- could really be any text that breaks whitespace - concatFragments (TextAppend (TextLit t) e) = t <> concatFragments e - concatFragments (TextAppend _ e) = "${x}" <> concatFragments e - concatFragments (TextLit t) = t - concatFragments _ = mempty + buildChunk (c, _) = escapeText c <> "${x}" - builder0 = concatFragments expr0 +dedent :: Chunks Src a -> Chunks Src a +dedent chunks0 = process chunks0 + where + builder0 = buildChunks chunks0 text0 = Data.Text.Lazy.Builder.toLazyText builder0 @@ -375,9 +368,9 @@ [] -> 0 _ -> minimum (map indentLength nonEmptyLines) - -- The purpose of this complicated `trim0`/`trim1` is to ensure that we - -- strip leading whitespace without stripping whitespace after variable - -- interpolation + -- The purpose of this complicated `trimBegin`/`trimContinue` is to ensure + -- that we strip leading whitespace without stripping whitespace after + -- variable interpolation -- This is the trim function we use up until the first variable -- interpolation, dedenting all lines @@ -402,16 +395,14 @@ -- This is the loop that drives whether or not to use `trimBegin` or -- `trimContinue`. We call this function with `trimBegin`, but after the -- first interpolation we switch permanently to `trimContinue` - process trim (TextAppend (TextLit t) e) = - TextAppend (TextLit (trim t)) (process trimContinue e) - process _ (TextAppend e0 e1) = - TextAppend e0 (process trimContinue e1) - process trim (TextLit t) = - TextLit (trim t) - process _ e = - e + process (Chunks ((x0, y0):xys) z) = + Chunks ((trimBegin x0, y0):xys') (trimContinue z) + where + xys' = [ (trimContinue x, y) | (x, y) <- xys ] + process (Chunks [] z) = + Chunks [] (trimBegin z) -singleQuoteContinue :: Parser a -> Parser (Expr Src a) +singleQuoteContinue :: Parser a -> Parser (Chunks Src a) singleQuoteContinue embedded = choice [ escapeSingleQuotes @@ -424,44 +415,44 @@ ] where escapeSingleQuotes = do - a <- fmap TextLit "'''" + _ <- "'''" :: Parser Builder b <- singleQuoteContinue embedded - return (textAppend a b) + return ("''" <> b) interpolation = do _ <- Text.Parser.Char.text "${" a <- expression embedded _ <- Text.Parser.Char.char '}' b <- singleQuoteContinue embedded - return (textAppend a b) + return (Chunks [(mempty, a)] mempty <> b) escapeInterpolation = do _ <- Text.Parser.Char.text "''${" b <- singleQuoteContinue embedded - return (textAppend (TextLit "${") b) + return ("${" <> b) endLiteral = do _ <- Text.Parser.Char.text "''" - return (TextLit "") + return mempty unescapedCharacter = do - a <- fmap TextLit (satisfy predicate) + a <- satisfy predicate b <- singleQuoteContinue embedded - return (textAppend a b) + return (Chunks [] a <> b) where predicate c = '\x20' <= c && c <= '\x10FFFF' endOfLine = do - a <- fmap TextLit "\n" <|> fmap TextLit "\r\n" + a <- "\n" <|> "\r\n" b <- singleQuoteContinue embedded - return (textAppend a b) + return (Chunks [] a <> b) tab = do _ <- Text.Parser.Char.char '\t' b <- singleQuoteContinue embedded - return (textAppend (TextLit "\t") b) + return ("\t" <> b) -singleQuoteLiteral :: Parser a -> Parser (Expr Src a) +singleQuoteLiteral :: Parser a -> Parser (Chunks Src a) singleQuoteLiteral embedded = do _ <- Text.Parser.Char.text "''" @@ -482,7 +473,7 @@ textLiteral embedded = (do literal <- doubleQuotedLiteral embedded <|> singleQuoteLiteral embedded whitespace - return literal ) "text literal" + return (TextLit literal) ) "text literal" reserved :: Data.Text.Text -> Parser () reserved x = do _ <- Text.Parser.Char.text x; whitespace @@ -511,6 +502,9 @@ _merge :: Parser () _merge = reserved "merge" +_constructors :: Parser () +_constructors = reserved "constructors" + _NaturalFold :: Parser () _NaturalFold = reserved "Natural/fold" @@ -1151,8 +1145,10 @@ applicationExpression :: Parser a -> Parser (Expr Src a) applicationExpression embedded = do - a <- some (noted (selectorExpression embedded)) - return (foldl1 app a) + f <- (do _constructors; return Constructors) <|> return id + a <- noted (selectorExpression embedded) + b <- many (noted (selectorExpression embedded)) + return (foldl app (f a) b) where app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = Note (Src before after (bytesL <> bytesR)) (App nL nR) diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -923,30 +923,6 @@ -- > -- > "haha" -- --- Every @let@ expression of the form: --- --- > let x : t = y in e --- --- ... is exactly equivalent to: --- --- > (λ(x : t) → e) y --- --- So for example, this @let@ expression: --- --- > let x : Text = "ha" in x ++ x --- --- ... is equivalent to: --- --- > (λ(x : Text) → x ++ x) "ha" --- --- ... which in turn reduces to: --- --- > "ha" ++ "ha" --- --- ... which in turn reduces to: --- --- > "haha" --- -- You need to nest @let@ expressions if you want to define more than one value -- in this way: -- @@ -997,6 +973,13 @@ -- > -- > False -- +-- ... or to define synonyms for types: +-- +-- > $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name' +-- > List Text +-- > +-- > [ "John", "Mary" ] +-- -- __Exercise:__ What do you think the following code will normalize to? -- -- > let x = 1 @@ -1128,6 +1111,36 @@ -- > , Empty -- > ] -- +-- ... and Dhall even provides the @constructors@ keyword to automate this +-- common pattern: +-- +-- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > +-- > in [ MyType.Empty {} +-- > , MyType.Person { name = "John", age = +23 } +-- > , MyType.Person { name = "Amy" , age = +25 } +-- > ] +-- +-- The @constructors@ keyword takes a union type argument and returns a record +-- with one field per union type constructor: +-- +-- > $ dhall --pretty +-- > constructors < Empty : {} | Person : { name : Text, age : Natural } > +-- > +-- > +-- > { Empty : +-- > ∀(Empty : {}) → < Empty : {} | Person : { age : Natural, name : Text } > +-- > , Person : +-- > ∀(Person : { age : Natural, name : Text }) +-- > → < Empty : {} | Person : { age : Natural, name : Text } > +-- > } +-- > +-- > { Empty = +-- > λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } > +-- > , Person = +-- > λ(Person : { age : Natural, name : Text }) +-- > → < Person = Person | Empty : {} > +-- > } +-- -- You can also extract fields during pattern matching such as in the following -- function which renders each value to `Text`: -- @@ -2678,25 +2691,10 @@ -- the above polymorphic function then you'd get the unexpected behavior where -- a list literal is a function if the list has 0 elements but not a function -- otherwise. --- --- * Does Dhall support type synonyms like Haskell? --- --- No. For example, the following expression will not type-check: --- --- > let MyType = Integer in 1 : MyType --- --- Haskell can support type synonyms because Haskell does not allow type-level --- functions like Dhall does. Dhall's support for type-level computation means --- that type synonyms cannot be safely substituted until after the type-checking --- phase, otherwise type-checking might infinitely loop --- --- You can work around this limitation using Dhall's import system by saving the --- type synonym to a path and importing that path, like this: --- --- > cat ./MyType --- > Integer +-- +-- * Does Dhall support user-defined recursive types? -- --- > 1 : ./MyType -- This will type-check +-- No, but you can translate recursive code to non-recursive code by following +-- this guide: -- --- This is because import resolution precedes type-checking and does not run the --- risk of causing the type-checker to diverge +-- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -30,7 +30,7 @@ import Data.Text.Prettyprint.Doc (Pretty(..)) import Data.Traversable (forM) import Data.Typeable (Typeable) -import Dhall.Core (Const(..), Expr(..), Var(..)) +import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..)) import Dhall.Context (Context) import qualified Control.Monad.Trans.State.Strict as State @@ -137,7 +137,9 @@ loop ctx e@(Var (V x n) ) = do case Dhall.Context.lookup x n ctx of Nothing -> Left (TypeError ctx e (UnboundVariable x)) - Just a -> return a + Just a -> do + _ <- loop ctx a + return a loop ctx (Lam x _A b ) = do _ <- loop ctx _A let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) @@ -177,45 +179,23 @@ let nf_A = Dhall.Core.normalize _A let nf_A' = Dhall.Core.normalize _A' Left (TypeError ctx e (TypeMismatch f nf_A a nf_A')) - loop ctx e@(Let f mt r b ) = do - tR <- loop ctx r - ttR <- fmap Dhall.Core.normalize (loop ctx tR) - kR <- case ttR of - Const k -> return k - -- Don't bother to provide a `let`-specific version of this error - -- message because this should never happen anyway - _ -> Left (TypeError ctx e (InvalidInputType tR)) - - let ctx' = fmap (Dhall.Core.shift 1 (V f 0)) (Dhall.Context.insert f tR ctx) - tB <- loop ctx' b - ttB <- fmap Dhall.Core.normalize (loop ctx' tB) - kB <- case ttB of - Const k -> return k - -- Don't bother to provide a `let`-specific version of this error - -- message because this should never happen anyway - _ -> Left (TypeError ctx e (InvalidOutputType tB)) - - case rule kR kB of - Left () -> Left (TypeError ctx e (NoDependentLet tR tB)) - Right _ -> return () - - case mt of - Nothing -> do - return () - Just t -> do - _ <- loop ctx t - let nf_t = Dhall.Core.normalize t - let nf_tR = Dhall.Core.normalize tR - if propEqual nf_tR nf_t + loop ctx e@(Let x mA a0 b0) = do + _A1 <- loop ctx a0 + case mA of + Just _A0 -> do + _ <- loop ctx _A0 + let nf_A0 = Dhall.Core.normalize _A0 + let nf_A1 = Dhall.Core.normalize _A1 + if propEqual _A0 _A1 then return () - else Left (TypeError ctx e (AnnotMismatch r nf_t nf_tR)) - - let r' = Dhall.Core.shift 1 (V f 0) r - let tB' = Dhall.Core.subst (V f 0) r' (Dhall.Core.normalize tB) - let tB'' = Dhall.Core.shift (-1) (V f 0) tB' - return tB'' + else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1)) + Nothing -> return () + let a1 = Dhall.Core.normalize a0 + let a2 = Dhall.Core.shift 1 (V x 0) a1 + let b1 = Dhall.Core.subst (V x 0) a2 b0 + let b2 = Dhall.Core.shift (-1) (V x 0) b1 + loop ctx b2 loop ctx e@(Annot x t ) = do - -- This is mainly just to check that `t` is not `Kind` _ <- loop ctx t t' <- loop ctx x @@ -362,7 +342,13 @@ return (Pi "_" Double Text) loop _ Text = do return (Const Type) - loop _ (TextLit _ ) = do + loop ctx e@(TextLit (Chunks xys _)) = do + let process (_, y) = do + ty <- fmap Dhall.Core.normalize (loop ctx y) + case ty of + Text -> return () + _ -> Left (TypeError ctx e (CantInterpolate y ty)) + mapM_ process xys return Text loop ctx e@(TextAppend l r ) = do tl <- fmap Dhall.Core.normalize (loop ctx l) @@ -496,15 +482,15 @@ mapM_ process (Data.Map.toList kts) return (Const Type) loop ctx e@(RecordLit kvs ) = do - let process (k, v) = do + let process k v = do t <- loop ctx v s <- fmap Dhall.Core.normalize (loop ctx t) case s of Const Type -> return () _ -> Left (TypeError ctx e (InvalidField k v)) - return (k, t) - kts <- mapM process (Data.Map.toAscList kvs) - return (Record (Data.Map.fromAscList kts)) + return t + kts <- Data.Map.traverseWithKey process kvs + return (Record kts) loop ctx e@(Union kts ) = do let process (k, t) = do s <- fmap Dhall.Core.normalize (loop ctx t) @@ -561,6 +547,8 @@ _ -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY)) return (Record (Data.Map.union ktsY ktsX)) loop ctx e@(Merge kvsX kvsY (Just t)) = do + _ <- loop ctx t + tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX) ktsX <- case tKvsX of Record kts -> return kts @@ -634,10 +622,22 @@ _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.Map.toList ktsY) return t + loop ctx e@(Constructors t ) = do + _ <- loop ctx t + + kts <- case Dhall.Core.normalize t of + Union kts -> return kts + t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t')) + + let adapt k t_ = Pi k t_ (Union kts) + + return (Record (Data.Map.mapWithKey adapt kts)) loop ctx e@(Field r x ) = do t <- fmap Dhall.Core.normalize (loop ctx r) case t of - Record kts -> + Record kts -> do + _ <- loop ctx t + case Data.Map.lookup x kts of Just t' -> return t' Nothing -> Left (TypeError ctx e (MissingField x t)) @@ -706,17 +706,18 @@ | InvalidHandlerOutputType Text (Expr s a) (Expr s a) | MissingMergeType | HandlerNotAFunction Text (Expr s a) + | ConstructorsRequiresAUnionType (Expr s a) (Expr s a) | NotARecord Text (Expr s a) (Expr s a) | MissingField Text (Expr s a) | CantAnd (Expr s a) (Expr s a) | CantOr (Expr s a) (Expr s a) | CantEQ (Expr s a) (Expr s a) | CantNE (Expr s a) (Expr s a) + | CantInterpolate (Expr s a) (Expr s a) | CantTextAppend (Expr s a) (Expr s a) | CantListAppend (Expr s a) (Expr s a) | CantAdd (Expr s a) (Expr s a) | CantMultiply (Expr s a) (Expr s a) - | NoDependentLet (Expr s a) (Expr s a) | NoDependentTypes (Expr s a) (Expr s a) deriving (Show) @@ -1725,7 +1726,7 @@ \ └───────────────┘ \n\ \ \n\ \ \n\ - \Your first ❰List❱ elements has this type: \n\ + \Your first ❰List❱ element has this type: \n\ \ \n\ \↳ " <> txt0 <> " \n\ \ \n\ @@ -2746,6 +2747,58 @@ txt0 = build k txt1 = build expr0 +prettyTypeMessage (ConstructorsRequiresAUnionType expr0 expr1) = ErrorMessages {..} + where + short = "❰constructors❱ requires a union type" + + long = + "Explanation: You can only use the ❰constructors❱ keyword on an argument that is \n\ + \a union type literal, like this: \n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────────┐ \n\ + \ │ constructors < Left : Natural, Right : Bool > │ \n\ + \ └───────────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but you cannot use the ❰constructors❱ keyword on any other type of argument.\n\ + \For example, you cannot use a variable argument: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────────────┐ \n\ + \ │ λ(t : Type) → constructors t │ Invalid: ❰t❱ might not be a union type \n\ + \ └──────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌─────────────────────────────────────────────────┐ \n\ + \ │ let t : Type = < Left : Natural, Right : Bool > │ Invalid: Type-checking \n\ + \ │ in constructors t │ precedes normalization \n\ + \ └─────────────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \However, you can import the union type argument: \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────────────┐ \n\ + \ │ constructors ./unionType.dhall │ Valid: Import resolution precedes \n\ + \ └────────────────────────────────┘ type-checking \n\ + \ \n\ + \ \n\ + \────────────────────────────────────────────────────────────────────────────────\n\ + \ \n\ + \You tried to supply the following argument: \n\ + \ \n\ + \↳ " <> txt0 <> " \n\ + \ \n\ + \... which normalized to: \n\ + \ \n\ + \↳ " <> txt1 <> " \n\ + \ \n\ + \... which is not a union type literal \n" + where + txt0 = build expr0 + txt1 = build expr1 + prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..} where short = "Not a record" @@ -2858,6 +2911,70 @@ prettyTypeMessage (CantNE expr0 expr1) = buildBooleanOperator "/=" expr0 expr1 +prettyTypeMessage (CantInterpolate expr0 expr1) = ErrorMessages {..} + where + short = "You can only interpolate ❰Text❱" + + long = + "Explanation: Text interpolation only works on expressions of type ❰Text❱ \n\ + \ \n\ + \For example, these are all valid uses of string interpolation: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────┐ \n\ + \ │ \"ABC${\"DEF\"}GHI\" │ \n\ + \ └──────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────────┐ \n\ + \ │ λ(x : Text) → \"ABC${x}GHI\" │ \n\ + \ └────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────────────────────────────┐ \n\ + \ │ λ(age : Natural) → \"Age: ${Integer/show (Natural/toInteger age)}\" │ \n\ + \ └───────────────────────────────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \Some common reasons why you might get this error: \n\ + \ \n\ + \● You might have thought that string interpolation automatically converts the \n\ + \ interpolated value to a ❰Text❱ representation of that value: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────────────────┐ \n\ + \ │ λ(age : Natural) → \"Age: ${age}\" │ \n\ + \ └──────────────────────────────────┘ \n\ + \ ⇧ \n\ + \ Invalid: ❰age❱ has type ❰Natural❱ \n\ + \ \n\ + \ \n\ + \● You might have forgotten to escape a string interpolation that you wanted \n\ + \ Dhall to ignore and pass through: \n\ + \ \n\ + \ \n\ + \ ┌────────────────┐ \n\ + \ │ \"echo ${HOME}\" │ \n\ + \ └────────────────┘ \n\ + \ ⇧ \n\ + \ ❰HOME❱ is not in scope and this might have meant to use ❰\\${HOME}❱\n\ + \ \n\ + \ \n\ + \────────────────────────────────────────────────────────────────────────────────\n\ + \ \n\ + \You interpolated this expression: \n\ + \ \n\ + \↳ " <> txt0 <> " \n\ + \ \n\ + \... which does not have type ❰Text❱ but instead has type: \n\ + \ \n\ + \↳ " <> txt1 <> " \n" + where + txt0 = build expr0 + txt1 = build expr1 + + + prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..} where short = "❰++❱ only works on ❰Text❱" @@ -2974,91 +3091,6 @@ \↳ " <> txt1 <> " \n\ \ \n\ \... which makes this a forbidden dependent function type \n" - where - txt0 = build expr0 - txt1 = build expr1 - -prettyTypeMessage (NoDependentLet expr0 expr1) = ErrorMessages {..} - where - short = "No dependent ❰let❱" - - long = - "Explanation: The Dhall programming language does not allow ❰let❱ expressions \n\ - \from terms to types. These ❰let❱ expressions are also known as \"dependent ❰let❱\n\ - \expressions\" because you have a type whose value depends on the value of a term.\n\ - \ \n\ - \The Dhall language forbids these dependent ❰let❱ expressions in order to \n\ - \guarantee that ❰let❱ expressions of the form: \n\ - \ \n\ - \ \n\ - \ ┌────────────────────┐ \n\ - \ │ let x : t = r in e │ \n\ - \ └────────────────────┘ \n\ - \ \n\ - \ \n\ - \... are always equivalent to: \n\ - \ \n\ - \ \n\ - \ ┌──────────────────┐ \n\ - \ │ (λ(x : t) → e) r │ \n\ - \ └──────────────────┘ \n\ - \ \n\ - \ \n\ - \This means that both expressions should normalize to the same result and if one \n\ - \of the two fails to type check then the other should fail to type check, too. \n\ - \ \n\ - \For this reason, the following is " <> _NOT <> " legal code: \n\ - \ \n\ - \ \n\ - \ ┌───────────────────┐ \n\ - \ │ let x = 2 in Text │ \n\ - \ └───────────────────┘ \n\ - \ \n\ - \ \n\ - \... because the above ❰let❱ expression is equivalent to: \n\ - \ \n\ - \ \n\ - \ ┌─────────────────────────────┐ \n\ - \ │ let x : Integer = 2 in Text │ \n\ - \ └─────────────────────────────┘ \n\ - \ \n\ - \ \n\ - \... which in turn must be equivalent to: \n\ - \ \n\ - \ \n\ - \ ┌───────────────────────────┐ \n\ - \ │ (λ(x : Integer) → Text) 2 │ \n\ - \ └───────────────────────────┘ \n\ - \ \n\ - \ \n\ - \... which in turn fails to type check because this sub-expression: \n\ - \ \n\ - \ \n\ - \ ┌───────────────────────┐ \n\ - \ │ λ(x : Integer) → Text │ \n\ - \ └───────────────────────┘ \n\ - \ \n\ - \ \n\ - \... has type: \n\ - \ \n\ - \ \n\ - \ ┌───────────────────────┐ \n\ - \ │ ∀(x : Integer) → Text │ \n\ - \ └───────────────────────┘ \n\ - \ \n\ - \ \n\ - \... which is a forbidden dependent function type (i.e. a function from a term to\n\ - \a type). Therefore the equivalent ❰let❱ expression is also forbidden. \n\ - \ \n\ - \Your ❰let❱ expression is invalid because the input has type: \n\ - \ \n\ - \↳ " <> txt0 <> " \n\ - \ \n\ - \... and the output has kind: \n\ - \ \n\ - \↳ " <> txt1 <> " \n\ - \ \n\ - \... which makes this a forbidden dependent ❰let❱ expression \n" where txt0 = build expr0 txt1 = build expr1 diff --git a/tests/Parser.hs b/tests/Parser.hs --- a/tests/Parser.hs +++ b/tests/Parser.hs @@ -108,6 +108,9 @@ "merge" "./tests/parser/merge.dhall" , shouldPass + "constructors" + "./tests/parser/constructors.dhall" + , shouldPass "fields" "./tests/parser/fields.dhall" , shouldPass diff --git a/tests/Regression.hs b/tests/Regression.hs --- a/tests/Regression.hs +++ b/tests/Regression.hs @@ -7,13 +7,18 @@ import qualified Control.Exception import qualified Data.Map +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.Core import qualified Dhall.Parser +import qualified System.Timeout import qualified Test.Tasty import qualified Test.Tasty.HUnit import qualified Util +import Control.DeepSeq (($!!)) import Dhall.Import (Imported) import Dhall.Parser (Src) import Dhall.TypeCheck (TypeError, X) @@ -27,6 +32,9 @@ , issue126 , issue151 , issue164 + , issue201 + , issue209 + , issue216 , parsing0 , typeChecking0 , typeChecking1 @@ -114,6 +122,40 @@ -- single-quoted string _ <- Util.code "./tests/regression/issue164.dhall" return () ) + +issue201 :: TestTree +issue201 = Test.Tasty.HUnit.testCase "Issue #201" (do + -- Verify that type synonyms work + _ <- Util.code "./tests/regression/issue201.dhall" + return () ) + +issue209 :: TestTree +issue209 = Test.Tasty.HUnit.testCase "Issue #209" (do + -- Verify that pretty-printing `constructors` doesn't trigger an infinite + -- loop + e <- Util.code "./tests/regression/issue209.dhall" + let text = Dhall.Core.pretty e + Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $!! text) + return () ) + +opts :: Data.Text.Prettyprint.Doc.LayoutOptions +opts = + Data.Text.Prettyprint.Doc.defaultLayoutOptions + { Data.Text.Prettyprint.Doc.layoutPageWidth = + Data.Text.Prettyprint.Doc.AvailablePerLine 80 1.0 + } + +issue216 :: TestTree +issue216 = Test.Tasty.HUnit.testCase "Issue #216" (do + -- Verify that pretty-printing preserves string interpolation + e <- Util.code "./tests/regression/issue216a.dhall" + let doc = Data.Text.Prettyprint.Doc.pretty e + let docStream = Data.Text.Prettyprint.Doc.layoutSmart opts doc + let text0 = Data.Text.Prettyprint.Doc.Render.Text.renderLazy docStream + + text1 <- Data.Text.Lazy.IO.readFile "./tests/regression/issue216b.dhall" + + Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 ) parsing0 :: TestTree parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do diff --git a/tests/Tutorial.hs b/tests/Tutorial.hs --- a/tests/Tutorial.hs +++ b/tests/Tutorial.hs @@ -10,8 +10,11 @@ import qualified Test.Tasty.HUnit import qualified Util +import Data.Monoid ((<>)) +import Data.Text (Text) import Dhall (Inject) import GHC.Generics (Generic) +import Numeric.Natural (Natural) import Test.Tasty (TestTree) import Test.Tasty.HUnit ((@?=)) @@ -27,6 +30,13 @@ , _Functions_1 , _Functions_2 ] + , Test.Tasty.testGroup "Unions" + [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall" + , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall" + , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall" + , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall" + , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall" + ] ] _Interpolation_0 :: TestTree @@ -67,3 +77,9 @@ f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" f (Example0 { foo = True, bar = False }) @?= False f (Example0 { foo = True, bar = True }) @?= True ) + +example :: Natural -> Text -> Text -> TestTree +example n text0 text1 = + Test.Tasty.HUnit.testCase + ("Example #" <> show n) + (Util.equivalent text0 text1) diff --git a/tests/Util.hs b/tests/Util.hs --- a/tests/Util.hs +++ b/tests/Util.hs @@ -3,6 +3,7 @@ module Util ( code , codeWith + , equivalent , normalize' , normalizeWith' , assertNormalizesTo @@ -47,6 +48,12 @@ Left typeError -> Control.Exception.throwIO typeError Right _ -> return () return expr1 + +equivalent :: Data.Text.Text -> Data.Text.Text -> IO () +equivalent text0 text1 = do + expr0 <- fmap Dhall.Core.normalize (Util.code text0) :: IO (Expr X X) + expr1 <- fmap Dhall.Core.normalize (Util.code text1) :: IO (Expr X X) + assertEqual "Expressions are not equivalent" expr0 expr1 assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO () assertNormalizesTo e expected = do diff --git a/tests/parser/constructors.dhall b/tests/parser/constructors.dhall new file mode 100644 --- /dev/null +++ b/tests/parser/constructors.dhall @@ -0,0 +1,1 @@ +constructors < Left : Natural | Right : Bool > diff --git a/tests/parser/quotedLabel.dhall b/tests/parser/quotedLabel.dhall --- a/tests/parser/quotedLabel.dhall +++ b/tests/parser/quotedLabel.dhall @@ -1,2 +1,1 @@ -let `let` = 1 -in `let` +{ example1 = let `let` = 1 in `let`, example2 = let `:.` = 1 in `:.` } diff --git a/tests/regression/issue201.dhall b/tests/regression/issue201.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue201.dhall @@ -0,0 +1,1 @@ +let Foo = {} in {=} : Foo diff --git a/tests/regression/issue209.dhall b/tests/regression/issue209.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue209.dhall @@ -0,0 +1,1 @@ +constructors <> diff --git a/tests/regression/issue216a.dhall b/tests/regression/issue216a.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue216a.dhall @@ -0,0 +1,5 @@ +let GitHubProject : Type = { owner : Text, repo : Text } in +let gitHubProject = \( github : GitHubProject ) -> + let gitHubRoot = "https://github.com/${github.owner}/${github.repo}" + in { bugReports = "${gitHubRoot}/issues" } +in gitHubProject diff --git a/tests/regression/issue216b.dhall b/tests/regression/issue216b.dhall new file mode 100644 --- /dev/null +++ b/tests/regression/issue216b.dhall @@ -0,0 +1,10 @@ + let GitHubProject : Type = { owner : Text, repo : Text } + +in let gitHubProject = + λ(github : GitHubProject) + → let gitHubRoot = + "https://github.com/${github.owner}/${github.repo}" + + in { bugReports = "${gitHubRoot}/issues" } + +in gitHubProject diff --git a/tests/tutorial/process.dhall b/tests/tutorial/process.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/process.dhall @@ -0,0 +1,6 @@ + λ(union : < Left : Natural | Right : Bool >) +→ let handlers = + { Left = Natural/even -- Natural/even is a built-in function + , Right = λ(b : Bool) → b + } +in merge handlers union : Bool diff --git a/tests/tutorial/unions0A.dhall b/tests/tutorial/unions0A.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions0A.dhall @@ -0,0 +1,1 @@ +./process.dhall < Left = +3 | Right : Bool > diff --git a/tests/tutorial/unions0B.dhall b/tests/tutorial/unions0B.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions0B.dhall @@ -0,0 +1,1 @@ +False diff --git a/tests/tutorial/unions1A.dhall b/tests/tutorial/unions1A.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions1A.dhall @@ -0,0 +1,1 @@ +./process.dhall < Right = True | Left : Natural > diff --git a/tests/tutorial/unions1B.dhall b/tests/tutorial/unions1B.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions1B.dhall @@ -0,0 +1,1 @@ +True diff --git a/tests/tutorial/unions2A.dhall b/tests/tutorial/unions2A.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions2A.dhall @@ -0,0 +1,8 @@ + let Empty = < Empty = {=} | Person : { name : Text, age : Natural } > +in let Person = + λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > +in [ Empty + , Person { name = "John", age = +23 } + , Person { name = "Amy" , age = +25 } + , Empty + ] diff --git a/tests/tutorial/unions2B.dhall b/tests/tutorial/unions2B.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions2B.dhall @@ -0,0 +1,5 @@ +[ < Empty = {=} | Person : { age : Natural, name : Text } > +, < Person = { age = +23, name = "John" } | Empty : {} > +, < Person = { age = +25, name = "Amy" } | Empty : {} > +, < Empty = {=} | Person : { age : Natural, name : Text } > +] diff --git a/tests/tutorial/unions3A.dhall b/tests/tutorial/unions3A.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions3A.dhall @@ -0,0 +1,5 @@ + let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > +in [ MyType.Empty {=} + , MyType.Person { name = "John", age = +23 } + , MyType.Person { name = "Amy" , age = +25 } + ] diff --git a/tests/tutorial/unions3B.dhall b/tests/tutorial/unions3B.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions3B.dhall @@ -0,0 +1,4 @@ +[ < Empty = {=} | Person : { age : Natural, name : Text } > +, < Person = { age = +23, name = "John" } | Empty : {} > +, < Person = { age = +25, name = "Amy" } | Empty : {} > +] diff --git a/tests/tutorial/unions4A.dhall b/tests/tutorial/unions4A.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions4A.dhall @@ -0,0 +1,1 @@ +constructors < Empty : {} | Person : { name : Text, age : Natural } > diff --git a/tests/tutorial/unions4B.dhall b/tests/tutorial/unions4B.dhall new file mode 100644 --- /dev/null +++ b/tests/tutorial/unions4B.dhall @@ -0,0 +1,6 @@ +{ Empty = + λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } > +, Person = + λ(Person : { age : Natural, name : Text }) + → < Person = Person | Empty : {} > +}