dhall 1.32.0 → 1.33.0
raw patch · 177 files changed
+2208/−2333 lines, 177 filesbinary-addedPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
- Dhall: ExtractErrors :: NonEmpty (ExtractError s a) -> ExtractErrors s a
- Dhall: instance (Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Data.Typeable.Internal.Typeable s, Data.Typeable.Internal.Typeable a) => GHC.Exception.Type.Exception (Dhall.ExtractErrors s a)
- Dhall: instance (Dhall.FromDhall a, Data.Hashable.Class.Hashable a, GHC.Classes.Ord a, GHC.Show.Show a) => Dhall.FromDhall (Data.HashSet.Base.HashSet a)
- Dhall: instance (Dhall.ToDhall k, Dhall.ToDhall v) => Dhall.ToDhall (Data.HashMap.Base.HashMap k v)
- Dhall: instance (GHC.Classes.Eq k, Data.Hashable.Class.Hashable k, Dhall.FromDhall k, Dhall.FromDhall v) => Dhall.FromDhall (Data.HashMap.Base.HashMap k v)
- Dhall: instance (GHC.Generics.Selector s, Dhall.FromDhall a) => Dhall.GenericFromDhall (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
- Dhall: instance (GHC.Generics.Selector s1, GHC.Generics.Selector s2, Dhall.FromDhall a1, Dhall.FromDhall a2) => Dhall.GenericFromDhall (GHC.Generics.M1 GHC.Generics.S s1 (GHC.Generics.K1 i1 a1) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s2 (GHC.Generics.K1 i2 a2))
- Dhall: instance Dhall.GenericFromDhall GHC.Generics.U1
- Dhall: instance Dhall.GenericFromDhall GHC.Generics.V1
- Dhall: instance Dhall.ToDhall a => Dhall.ToDhall (Data.HashSet.Base.HashSet a)
- Dhall: instance GHC.Base.Semigroup (Dhall.ExtractErrors s a)
- Dhall: instance forall k (c1 :: GHC.Generics.Meta) (f1 :: k -> *). (GHC.Generics.Constructor c1, Dhall.GenericFromDhall f1) => Dhall.GenericFromDhallUnion (GHC.Generics.M1 GHC.Generics.C c1 f1)
- Dhall: instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Dhall.GenericFromDhall f => Dhall.GenericFromDhall (GHC.Generics.M1 GHC.Generics.C c f)
- Dhall: instance forall k (f :: k -> *) (d :: GHC.Generics.Meta). Dhall.GenericFromDhall f => Dhall.GenericFromDhall (GHC.Generics.M1 GHC.Generics.D d f)
- Dhall: instance forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *). (Dhall.GenericFromDhall (f GHC.Generics.:*: g), Dhall.GenericFromDhall (h GHC.Generics.:*: i)) => Dhall.GenericFromDhall ((f GHC.Generics.:*: g) GHC.Generics.:*: (h GHC.Generics.:*: i))
- Dhall: instance forall k (f :: k -> *) (g :: k -> *) (s :: GHC.Generics.Meta) a i. (Dhall.GenericFromDhall (f GHC.Generics.:*: g), GHC.Generics.Selector s, Dhall.FromDhall a) => Dhall.GenericFromDhall ((f GHC.Generics.:*: g) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
- Dhall: instance forall k (f :: k -> *) (g :: k -> *). Dhall.GenericFromDhallUnion (f GHC.Generics.:+: g) => Dhall.GenericFromDhall (f GHC.Generics.:+: g)
- Dhall: instance forall k (f1 :: k -> *) (f2 :: k -> *). (Dhall.GenericFromDhallUnion f1, Dhall.GenericFromDhallUnion f2) => Dhall.GenericFromDhallUnion (f1 GHC.Generics.:+: f2)
- Dhall: instance forall k (s :: GHC.Generics.Meta) a (f :: k -> *) (g :: k -> *) i. (GHC.Generics.Selector s, Dhall.FromDhall a, Dhall.GenericFromDhall (f GHC.Generics.:*: g)) => Dhall.GenericFromDhall (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a) GHC.Generics.:*: (f GHC.Generics.:*: g))
- Dhall: newtype ExtractErrors s a
- Dhall.Core: OptionalBuild :: Expr s a
- Dhall.Core: OptionalFold :: Expr s a
- Dhall.Deriving: instance forall k a (tag :: k). (GHC.Generics.Generic a, Dhall.GenericFromDhall (GHC.Generics.Rep a), Dhall.Deriving.ModifyOptions tag) => Dhall.FromDhall (Dhall.Deriving.Codec tag a)
- Dhall.Deriving: instance forall k1 k2 (a :: k2) (b :: k1). (Dhall.Deriving.ModifyOptions a, Dhall.Deriving.ModifyOptions b) => Dhall.Deriving.ModifyOptions (a Dhall.Deriving.<<< b)
- Dhall.Deriving: instance forall k1 k2 (a :: k2) (b :: k1). (Dhall.Deriving.TextFunction a, Dhall.Deriving.TextFunction b) => Dhall.Deriving.TextFunction (a Dhall.Deriving.<<< b)
- Dhall.Import: data MissingFile
- Dhall.Lint: replaceOptionalBuildFold :: Expr s a -> Maybe (Expr s a)
- Dhall.Lint: replaceSaturatedOptionalFold :: Expr s a -> Maybe (Expr s a)
- Dhall.Parser.Token: _OptionalBuild :: Parser ()
- Dhall.Parser.Token: _OptionalFold :: Parser ()
+ Dhall: DhallErrors :: NonEmpty e -> DhallErrors e
+ Dhall: ExpectedTypeError :: ExpectedTypeError -> ExtractError s a
+ Dhall: RecursiveTypeError :: ExpectedTypeError
+ Dhall: data ExpectedTypeError
+ Dhall: instance (Dhall.FromDhall a, Data.Hashable.Class.Hashable a, GHC.Classes.Ord a, GHC.Show.Show a) => Dhall.FromDhall (Data.HashSet.Internal.HashSet a)
+ Dhall: instance (Dhall.ToDhall k, Dhall.ToDhall v) => Dhall.ToDhall (Data.HashMap.Internal.HashMap k v)
+ Dhall: instance (GHC.Classes.Eq k, Data.Hashable.Class.Hashable k, Dhall.FromDhall k, Dhall.FromDhall v) => Dhall.FromDhall (Data.HashMap.Internal.HashMap k v)
+ Dhall: instance (GHC.Show.Show (Dhall.DhallErrors e), Data.Typeable.Internal.Typeable e) => GHC.Exception.Type.Exception (Dhall.DhallErrors e)
+ Dhall: instance Dhall.GenericFromDhall a (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
+ Dhall: instance Dhall.GenericFromDhall a1 (GHC.Generics.M1 GHC.Generics.S s1 (GHC.Generics.K1 i1 a1) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s2 (GHC.Generics.K1 i2 a2))
+ Dhall: instance Dhall.GenericFromDhall a2 (GHC.Generics.M1 GHC.Generics.S s1 (GHC.Generics.K1 i1 a1) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s2 (GHC.Generics.K1 i2 a2))
+ Dhall: instance Dhall.ToDhall a => Dhall.ToDhall (Data.HashSet.Internal.HashSet a)
+ Dhall: instance GHC.Base.Functor Dhall.DhallErrors
+ Dhall: instance GHC.Base.Semigroup (Dhall.DhallErrors e)
+ Dhall: instance GHC.Classes.Eq Dhall.ExpectedTypeError
+ Dhall: instance GHC.Classes.Eq e => GHC.Classes.Eq (Dhall.DhallErrors e)
+ Dhall: instance GHC.Exception.Type.Exception Dhall.ExpectedTypeError
+ Dhall: instance GHC.Show.Show Dhall.ExpectedTypeError
+ Dhall: instance GHC.Show.Show Dhall.ExpectedTypeErrors
+ Dhall: instance forall k1 k2 (c1 :: GHC.Generics.Meta) (t :: k1) (f1 :: k2 -> *). (GHC.Generics.Constructor c1, Dhall.GenericFromDhall t f1) => Dhall.GenericFromDhallUnion t (GHC.Generics.M1 GHC.Generics.C c1 f1)
+ Dhall: instance forall k1 k2 (s :: GHC.Generics.Meta) a (t :: k1) (f :: k2 -> *) (g :: k2 -> *) i. (GHC.Generics.Selector s, Dhall.FromDhall a, Dhall.GenericFromDhall t (f GHC.Generics.:*: g)) => Dhall.GenericFromDhall t (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a) GHC.Generics.:*: (f GHC.Generics.:*: g))
+ Dhall: instance forall k1 k2 (s :: GHC.Generics.Meta) a (t :: k1) i. (GHC.Generics.Selector s, Dhall.FromDhall a) => Dhall.GenericFromDhall t (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
+ Dhall: instance forall k1 k2 (s1 :: GHC.Generics.Meta) (s2 :: GHC.Generics.Meta) a1 a2 (t :: k1) i1 i2. (GHC.Generics.Selector s1, GHC.Generics.Selector s2, Dhall.FromDhall a1, Dhall.FromDhall a2) => Dhall.GenericFromDhall t (GHC.Generics.M1 GHC.Generics.S s1 (GHC.Generics.K1 i1 a1) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s2 (GHC.Generics.K1 i2 a2))
+ Dhall: instance forall k1 k2 (t :: k1) (f :: k2 -> *) (c :: GHC.Generics.Meta). Dhall.GenericFromDhall t f => Dhall.GenericFromDhall t (GHC.Generics.M1 GHC.Generics.C c f)
+ Dhall: instance forall k1 k2 (t :: k1) (f :: k2 -> *) (d :: GHC.Generics.Meta). Dhall.GenericFromDhall t f => Dhall.GenericFromDhall t (GHC.Generics.M1 GHC.Generics.D d f)
+ Dhall: instance forall k1 k2 (t :: k1) (f :: k2 -> *) (g :: k2 -> *) (h :: k2 -> *) (i :: k2 -> *). (Dhall.GenericFromDhall t (f GHC.Generics.:*: g), Dhall.GenericFromDhall t (h GHC.Generics.:*: i)) => Dhall.GenericFromDhall t ((f GHC.Generics.:*: g) GHC.Generics.:*: (h GHC.Generics.:*: i))
+ Dhall: instance forall k1 k2 (t :: k1) (f :: k2 -> *) (g :: k2 -> *) (s :: GHC.Generics.Meta) a i. (Dhall.GenericFromDhall t (f GHC.Generics.:*: g), GHC.Generics.Selector s, Dhall.FromDhall a) => Dhall.GenericFromDhall t ((f GHC.Generics.:*: g) GHC.Generics.:*: GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
+ Dhall: instance forall k1 k2 (t :: k1) (f :: k2 -> *) (g :: k2 -> *). Dhall.GenericFromDhallUnion t (f GHC.Generics.:+: g) => Dhall.GenericFromDhall t (f GHC.Generics.:+: g)
+ Dhall: instance forall k1 k2 (t :: k1) (f1 :: k2 -> *) (f2 :: k2 -> *). (Dhall.GenericFromDhallUnion t f1, Dhall.GenericFromDhallUnion t f2) => Dhall.GenericFromDhallUnion t (f1 GHC.Generics.:+: f2)
+ Dhall: instance forall k1 k2 (t :: k1). Dhall.GenericFromDhall t GHC.Generics.U1
+ Dhall: instance forall k1 k2 (t :: k1). Dhall.GenericFromDhall t GHC.Generics.V1
+ Dhall: newtype DhallErrors e
+ Dhall: showDhallErrors :: Show e => String -> DhallErrors e -> String
+ Dhall: type ExpectedTypeErrors = DhallErrors ExpectedTypeError
+ Dhall: type Expector = Validation ExpectedTypeErrors
+ Dhall: type ExtractErrors s a = DhallErrors (ExtractError s a)
+ Dhall.Deriving: instance forall k a (tag :: k). (GHC.Generics.Generic a, Dhall.GenericFromDhall a (GHC.Generics.Rep a), Dhall.Deriving.ModifyOptions tag) => Dhall.FromDhall (Dhall.Deriving.Codec tag a)
+ Dhall.Deriving: instance forall k1 k2 (a :: k1) (b :: k2). (Dhall.Deriving.ModifyOptions a, Dhall.Deriving.ModifyOptions b) => Dhall.Deriving.ModifyOptions (a Dhall.Deriving.<<< b)
+ Dhall.Deriving: instance forall k1 k2 (a :: k1) (b :: k2). (Dhall.Deriving.TextFunction a, Dhall.Deriving.TextFunction b) => Dhall.Deriving.TextFunction (a Dhall.Deriving.<<< b)
+ Dhall.Import: newtype MissingFile
+ Dhall.Main: [noted] :: Mode -> Bool
+ Dhall.Parser.Expression: srcAnd :: Parser a -> Parser (Src, a)
+ Dhall.Parser.Token: anyLabelOrSome :: Parser Text
- Dhall: Decoder :: (Expr Src Void -> Extractor Src Void a) -> Expr Src Void -> Decoder a
+ Dhall: Decoder :: (Expr Src Void -> Extractor Src Void a) -> Expector (Expr Src Void) -> Decoder a
- Dhall: RecordDecoder :: Product (Const (Map Text (Expr Src Void))) (Compose ((->) (Expr Src Void)) (Extractor Src Void)) a -> RecordDecoder a
+ Dhall: RecordDecoder :: Product (Const (Map Text (Expector (Expr Src Void)))) (Compose ((->) (Expr Src Void)) (Extractor Src Void)) a -> RecordDecoder a
- Dhall: [expected] :: Decoder a -> Expr Src Void
+ Dhall: [expected] :: Decoder a -> Expector (Expr Src Void)
- Dhall: [getErrors] :: ExtractErrors s a -> NonEmpty (ExtractError s a)
+ Dhall: [getErrors] :: DhallErrors e -> NonEmpty e
- Dhall: autoWith :: (FromDhall a, Generic a, GenericFromDhall (Rep a)) => InputNormalizer -> Decoder a
+ Dhall: autoWith :: (FromDhall a, Generic a, GenericFromDhall a (Rep a)) => InputNormalizer -> Decoder a
- Dhall: class GenericFromDhall f
+ Dhall: class GenericFromDhall t f
- Dhall: genericAuto :: (Generic a, GenericFromDhall (Rep a)) => Decoder a
+ Dhall: genericAuto :: (Generic a, GenericFromDhall a (Rep a)) => Decoder a
- Dhall: genericAutoWith :: (Generic a, GenericFromDhall (Rep a)) => InterpretOptions -> Decoder a
+ Dhall: genericAutoWith :: (Generic a, GenericFromDhall a (Rep a)) => InterpretOptions -> Decoder a
- Dhall: genericAutoWithNormalizer :: GenericFromDhall f => InputNormalizer -> InterpretOptions -> State Int (Decoder (f a))
+ Dhall: genericAutoWithNormalizer :: GenericFromDhall t f => Proxy t -> InputNormalizer -> InterpretOptions -> State Int (Decoder (f a))
- Dhall: typeError :: Expr s a -> Expr s a -> Extractor s a b
+ Dhall: typeError :: Expector (Expr s a) -> Expr s a -> Extractor s a b
- Dhall.Binary: encodeExpression :: Expr Void Import -> ByteString
+ Dhall.Binary: encodeExpression :: Serialise (Expr Void a) => Expr Void a -> ByteString
- Dhall.Deriving: type Bare = 'Bare
+ Dhall.Deriving: type Bare = 'Bare
- Dhall.Deriving: type Smart = 'Smart
+ Dhall.Deriving: type Smart = 'Smart
- Dhall.Deriving: type Wrapped = 'Wrapped
+ Dhall.Deriving: type Wrapped = 'Wrapped
- Dhall.Main: Decode :: Input -> Bool -> Mode
+ Dhall.Main: Decode :: Input -> Bool -> Bool -> Mode
- Dhall.Main: SyntaxTree :: Input -> Mode
+ Dhall.Main: SyntaxTree :: Input -> Bool -> Mode
- Dhall.TypeCheck: absurd :: () => Void -> a
+ Dhall.TypeCheck: absurd :: Void -> a
Files
- CHANGELOG.md +38/−2
- benchmark/examples/issue108.dhall +3/−2
- dhall-lang/Prelude/Bool/and +2/−2
- dhall-lang/Prelude/Bool/build +2/−2
- dhall-lang/Prelude/Bool/even +2/−2
- dhall-lang/Prelude/Bool/fold +5/−5
- dhall-lang/Prelude/Bool/odd +2/−2
- dhall-lang/Prelude/Bool/or +2/−2
- dhall-lang/Prelude/Function/compose +7/−7
- dhall-lang/Prelude/Integer/abs +2/−4
- dhall-lang/Prelude/Integer/equal +3/−3
- dhall-lang/Prelude/Integer/lessThanEqual +3/−5
- dhall-lang/Prelude/Integer/multiply +7/−13
- dhall-lang/Prelude/Integer/subtract +8/−16
- dhall-lang/Prelude/Integer/toNatural +2/−2
- dhall-lang/Prelude/JSON/Tagged +4/−4
- dhall-lang/Prelude/JSON/Type +33/−44
- dhall-lang/Prelude/JSON/array +13/−13
- dhall-lang/Prelude/JSON/bool +13/−13
- dhall-lang/Prelude/JSON/double +13/−13
- dhall-lang/Prelude/JSON/integer +13/−13
- dhall-lang/Prelude/JSON/natural +13/−13
- dhall-lang/Prelude/JSON/null +12/−12
- dhall-lang/Prelude/JSON/object +15/−15
- dhall-lang/Prelude/JSON/omitNullFields +37/−39
- dhall-lang/Prelude/JSON/renderAs +76/−82
- dhall-lang/Prelude/JSON/renderInteger.dhall +2/−4
- dhall-lang/Prelude/JSON/string +13/−13
- dhall-lang/Prelude/JSON/tagInline +4/−4
- dhall-lang/Prelude/JSON/tagNested +6/−6
- dhall-lang/Prelude/List/all +4/−4
- dhall-lang/Prelude/List/any +4/−4
- dhall-lang/Prelude/List/build +11/−11
- dhall-lang/Prelude/List/concat +7/−7
- dhall-lang/Prelude/List/concatMap +8/−8
- dhall-lang/Prelude/List/default +3/−3
- dhall-lang/Prelude/List/drop +7/−9
- dhall-lang/Prelude/List/filter +7/−7
- dhall-lang/Prelude/List/fold +16/−16
- dhall-lang/Prelude/List/generate +10/−10
- dhall-lang/Prelude/List/iterate +13/−13
- dhall-lang/Prelude/List/map +8/−8
- dhall-lang/Prelude/List/package.dhall +4/−1
- dhall-lang/Prelude/List/partition +7/−9
- dhall-lang/Prelude/List/replicate +7/−7
- dhall-lang/Prelude/List/shifted +20/−20
- dhall-lang/Prelude/List/take +7/−7
- dhall-lang/Prelude/List/unpackOptionals +37/−0
- dhall-lang/Prelude/List/unzip +14/−14
- dhall-lang/Prelude/List/zip +37/−29
- dhall-lang/Prelude/Location/Type +2/−3
- dhall-lang/Prelude/Map/keyValue +4/−4
- dhall-lang/Prelude/Map/keys +3/−3
- dhall-lang/Prelude/Map/map +8/−8
- dhall-lang/Prelude/Map/values +3/−3
- dhall-lang/Prelude/Natural/build +14/−14
- dhall-lang/Prelude/Natural/enumerate +8/−8
- dhall-lang/Prelude/Natural/fold +13/−13
- dhall-lang/Prelude/Natural/listMax +2/−2
- dhall-lang/Prelude/Natural/listMin +4/−4
- dhall-lang/Prelude/Natural/product +2/−2
- dhall-lang/Prelude/Natural/sort +6/−6
- dhall-lang/Prelude/Natural/sum +2/−2
- dhall-lang/Prelude/Optional/all +4/−4
- dhall-lang/Prelude/Optional/any +4/−4
- dhall-lang/Prelude/Optional/build +23/−23
- dhall-lang/Prelude/Optional/concat +3/−3
- dhall-lang/Prelude/Optional/default +4/−4
- dhall-lang/Prelude/Optional/filter +15/−15
- dhall-lang/Prelude/Optional/fold +12/−12
- dhall-lang/Prelude/Optional/head +6/−6
- dhall-lang/Prelude/Optional/last +6/−6
- dhall-lang/Prelude/Optional/length +3/−3
- dhall-lang/Prelude/Optional/map +5/−5
- dhall-lang/Prelude/Optional/null +3/−3
- dhall-lang/Prelude/Optional/toList +3/−3
- dhall-lang/Prelude/Optional/unzip +8/−8
- dhall-lang/Prelude/Text/concat +2/−2
- dhall-lang/Prelude/Text/concatMap +4/−4
- dhall-lang/Prelude/Text/concatMapSep +10/−10
- dhall-lang/Prelude/Text/concatSep +8/−8
- dhall-lang/Prelude/Text/defaultMap +4/−4
- dhall-lang/Prelude/XML/Type +12/−12
- dhall-lang/Prelude/XML/element +13/−13
- dhall-lang/Prelude/XML/leaf +6/−8
- dhall-lang/Prelude/XML/render +10/−13
- dhall-lang/Prelude/XML/text +13/−13
- dhall-lang/Prelude/package.dhall +1/−1
- dhall-lang/tests/import/cache/dhall/12203871180b87ecaba8b53fffb2a8b52d3fce98098fab09a6f759358b9e8042eedc binary
- dhall-lang/tests/import/cache/dhall/1220618f785ce8f3930a9144398f576f0a992544b51212bc9108c31b4e670dc6ed21 +1/−0
- dhall-lang/tests/import/cache/dhall/1220efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd binary
- dhall-lang/tests/import/success/hashFromCacheA.dhall +2/−2
- dhall-lang/tests/import/success/hashFromCacheB.dhall +3/−3
- dhall-lang/tests/normalization/success/remoteSystemsA.dhall +5/−6
- dhall-lang/tests/normalization/success/remoteSystemsB.dhall +3/−6
- dhall-lang/tests/normalization/success/simple/optionalBuildA.dhall +0/−32
- dhall-lang/tests/normalization/success/simple/optionalBuildB.dhall +0/−9
- dhall-lang/tests/normalization/success/simple/optionalBuildFoldA.dhall +0/−1
- dhall-lang/tests/normalization/success/simple/optionalBuildFoldB.dhall +0/−1
- dhall-lang/tests/normalization/success/simple/optionalFoldA.dhall +0/−7
- dhall-lang/tests/normalization/success/simple/optionalFoldB.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalBuildA.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalBuildB.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalBuildFoldFusionA.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalBuildFoldFusionB.dhall +0/−3
- dhall-lang/tests/normalization/success/unit/OptionalBuildImplementationA.dhall +0/−3
- dhall-lang/tests/normalization/success/unit/OptionalBuildImplementationB.dhall +0/−3
- dhall-lang/tests/normalization/success/unit/OptionalFoldA.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalFoldB.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalFoldNoneA.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalFoldNoneB.dhall +0/−1
- dhall-lang/tests/normalization/success/unit/OptionalFoldSomeA.dhall +0/−4
- dhall-lang/tests/normalization/success/unit/OptionalFoldSomeB.dhall +0/−1
- dhall-lang/tests/parser/failure/unit/UrlWithQuotedPath.dhall +1/−0
- dhall-lang/tests/parser/success/builtinsA.dhall +35/−32
- dhall-lang/tests/parser/success/builtinsB.dhallb binary
- dhall-lang/tests/parser/success/largeExpressionA.dhall +5/−6
- dhall-lang/tests/parser/success/largeExpressionB.dhallb binary
- dhall-lang/tests/parser/success/quotedLabelA.dhall +1/−0
- dhall-lang/tests/parser/success/quotedLabelB.dhallb binary
- dhall-lang/tests/parser/success/quotedRecordLabelA.dhall +1/−0
- dhall-lang/tests/parser/success/quotedRecordLabelB.dhallb +1/−0
- dhall-lang/tests/parser/success/quotedUnionLabelA.dhall +1/−0
- dhall-lang/tests/parser/success/quotedUnionLabelB.dhallb +1/−0
- dhall-lang/tests/parser/success/unit/import/quotedPathsA.dhall +1/−3
- dhall-lang/tests/parser/success/unit/import/quotedPathsB.dhallb binary
- dhall-lang/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeA.dhall +0/−1
- dhall-lang/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeB.dhallb binary
- dhall-lang/tests/semantic-hash/success/remoteSystemsA.dhall +5/−6
- dhall-lang/tests/semantic-hash/success/remoteSystemsB.hash +1/−1
- dhall-lang/tests/semantic-hash/success/simple/optionalBuildA.dhall +0/−32
- dhall-lang/tests/semantic-hash/success/simple/optionalBuildB.hash +0/−1
- dhall-lang/tests/semantic-hash/success/simple/optionalBuildFoldA.dhall +0/−1
- dhall-lang/tests/semantic-hash/success/simple/optionalBuildFoldB.hash +0/−1
- dhall-lang/tests/semantic-hash/success/simple/optionalFoldA.dhall +0/−7
- dhall-lang/tests/semantic-hash/success/simple/optionalFoldB.hash +0/−1
- dhall-lang/tests/type-inference/success/preludeB.dhall +382/−383
- dhall-lang/tests/type-inference/success/unit/OptionalBuildA.dhall +0/−1
- dhall-lang/tests/type-inference/success/unit/OptionalBuildB.dhall +0/−7
- dhall-lang/tests/type-inference/success/unit/OptionalFoldA.dhall +0/−1
- dhall-lang/tests/type-inference/success/unit/OptionalFoldB.dhall +0/−6
- dhall.cabal +8/−11
- src/Dhall.hs +227/−173
- src/Dhall/Binary.hs +131/−121
- src/Dhall/Deriving.hs +2/−2
- src/Dhall/Diff.hs +5/−12
- src/Dhall/DirectoryTree.hs +53/−53
- src/Dhall/Eval.hs +0/−40
- src/Dhall/Format.hs +13/−20
- src/Dhall/Freeze.hs +29/−50
- src/Dhall/Import.hs +90/−59
- src/Dhall/Lint.hs +2/−72
- src/Dhall/Main.hs +84/−72
- src/Dhall/Normalize.hs +4/−31
- src/Dhall/Parser/Expression.hs +37/−29
- src/Dhall/Parser/Token.hs +31/−41
- src/Dhall/Pretty/Internal.hs +19/−20
- src/Dhall/Syntax.hs +43/−39
- src/Dhall/Tutorial.hs +34/−0
- src/Dhall/TypeCheck.hs +0/−28
- src/Dhall/Util.hs +2/−1
- tests/Dhall/Test/Dhall.hs +23/−4
- tests/Dhall/Test/Import.hs +28/−20
- tests/Dhall/Test/QuickCheck.hs +18/−2
- tests/Dhall/Test/Regression.hs +6/−5
- tests/Dhall/Test/Substitution.hs +10/−5
- tests/Dhall/Test/TypeInference.hs +13/−3
- tests/format/applicationMultilineA.dhall +2/−2
- tests/format/applicationMultilineB.dhall +2/−2
- tests/format/issue1805KeywordRecordFieldShouldBeQuotedA.dhall +1/−0
- tests/format/issue1805KeywordRecordFieldShouldBeQuotedB.dhall +1/−0
- tests/format/issue1805SomeQuotedInLetButNotInRecordA.dhall +1/−0
- tests/format/issue1805SomeQuotedInLetButNotInRecordB.dhall +1/−0
- tests/format/urlsA.dhall +0/−6
- tests/format/urlsB.dhall +0/−6
- tests/lint/success/optionalFoldBuildA.dhall +0/−4
- tests/lint/success/optionalFoldBuildB.dhall +0/−18
CHANGELOG.md view
@@ -1,3 +1,41 @@+1.33.0++* [Supports version 17.0.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v17.0.0)+ * BREAKING CHANGE: [URLs no longer support quoted path components](https://github.com/dhall-lang/dhall-haskell/pull/1812)+ * BREAKING CHANGE: [`Optional/{fold,build}` are no longer built-ins](https://github.com/dhall-lang/dhall-haskell/pull/1802)+ * [Record fields now permit empty labels](https://github.com/dhall-lang/dhall-haskell/pull/1812)+* BREAKING CHANGE: [Fail instead of hanging when deriving `FromDhall` for recursive types](https://github.com/dhall-lang/dhall-haskell/pull/1825)+ * This is a breaking change as now the `expected` type returns an+ `Expector (Expr Src Void)` (essentially an `Either`) instead of+ `Expr Src Void`+ * If you really don't want to handle the new error-related wrapper, you can+ get the old behavior using a partial pattern match (which will be partial,+ still an improvement over the previous behavior, which was hanging)+* [Fix invalid cache entries](https://github.com/dhall-lang/dhall-haskell/pull/1793)+ * The interpreter will now correct cached expressions that are incorrect+ and warn you when this happens+ * Specifically, if there is a hash mismatch from the cached expression the+ interpreter will resolve the import again and fix the cache if the+ resolved import matches the expected hash+* [Make `encodeExpression` polymorphic](https://github.com/dhall-lang/dhall-haskell/pull/1789)+ * `encodeExpression` now has a more general type, which means that you+ can use it to serialise expressions without imports (i.e.+ ones of type `Expr Void Void`)+* [Add `--quiet` option for `dhall decode`](https://github.com/dhall-lang/dhall-haskell/pull/1803)+* [Add `--noted` flag for `dhall haskell-syntax-tree`](https://github.com/dhall-lang/dhall-haskell/pull/1843)+* Performance improvements:+ * There were several performance improvements related to binary decoding,+ which should improve cache lookup speed+ * [#1807](https://github.com/dhall-lang/dhall-haskell/pull/1807)+ * [#1809](https://github.com/dhall-lang/dhall-haskell/pull/1809)+ * [#1857](https://github.com/dhall-lang/dhall-haskell/pull/1857)+* Improvements to error messages+ * [#1824](https://github.com/dhall-lang/dhall-haskell/pull/1824)+ * [#1849](https://github.com/dhall-lang/dhall-haskell/pull/1849)+ * [#1851](https://github.com/dhall-lang/dhall-haskell/pull/1851)+* Fixes to haddocks+ * [#1815](https://github.com/dhall-lang/dhall-haskell/pull/1815)+ 1.32.0 * [Supports version 16.0.0 of the standard](https://github.com/dhall-lang/dhall-lang/releases/tag/v16.0.0)@@ -11,8 +49,6 @@ * For example, `< A : Bool | B : Type >` is legal now * You can now write `someRecord with a.b.c = x` to update a nested fields- * [Add support for record puns](https://github.com/dhall-lang/dhall-haskell/pull/1710)- * You can now write `{ x, y }` as a shorthand for `{ x = x, y = y }` * DEPRECATION: [Deprecate `Dhall.Parser.exprA`](https://github.com/dhall-lang/dhall-haskell/pull/1740) * `Dhall.Parser` module will eventually drop support for parsing custom import types
benchmark/examples/issue108.dhall view
@@ -15,8 +15,9 @@ {} | MIPS64el_Linux : {} | PowerPC_Linux : {} | X86_64_Cygwin : {} | X86_64_Darwin : {} | X86_64_FreeBSD : {} | X86_64_Linux : {} | X86_64_Solaris : {} > , 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 = λ(_ : {}) → "",+Text } ) → λ(y : Text) →+merge { None = x.host, Some = λ(user : Text) → "${user}@${x.host}" } x.user+++ " " ++ ( merge { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result } ( List/fold < AArch64_Linux : {} | ARMv5tel_Linux : {} | ARMv7l_Linux : {} | I686_Cygwin : {} | I686_Linux : {} | MIPS64el_Linux : {} | PowerPC_Linux : {} | X86_64_Cygwin : {} | X86_64_Darwin :
dhall-lang/Prelude/Bool/and view
@@ -4,8 +4,8 @@ -} let and : List Bool → Bool- = λ(xs : List Bool)- → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True+ = λ(xs : List Bool) →+ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True let example0 = assert : and [ True, False, True ] ≡ False
dhall-lang/Prelude/Bool/build view
@@ -3,8 +3,8 @@ -} let build : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool- = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)- → f Bool True False+ = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) →+ f Bool True False let example0 = assert
dhall-lang/Prelude/Bool/even view
@@ -6,8 +6,8 @@ -} let even : List Bool → Bool- = λ(xs : List Bool)- → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True+ = λ(xs : List Bool) →+ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True let example0 = assert : even [ False, True, False ] ≡ True
dhall-lang/Prelude/Bool/fold view
@@ -3,11 +3,11 @@ -} let fold : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool- = λ(b : Bool)- → λ(bool : Type)- → λ(true : bool)- → λ(false : bool)- → if b then true else false+ = λ(b : Bool) →+ λ(bool : Type) →+ λ(true : bool) →+ λ(false : bool) →+ if b then true else false let example0 = assert : fold True Natural 0 1 ≡ 0
dhall-lang/Prelude/Bool/odd view
@@ -6,8 +6,8 @@ -} let odd : List Bool → Bool- = λ(xs : List Bool)- → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False+ = λ(xs : List Bool) →+ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False let example0 = assert : odd [ True, False, True ] ≡ False
dhall-lang/Prelude/Bool/or view
@@ -4,8 +4,8 @@ -} let or : List Bool → Bool- = λ(xs : List Bool)- → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False+ = λ(xs : List Bool) →+ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False let example0 = assert : or [ True, False, True ] ≡ True
dhall-lang/Prelude/Function/compose view
@@ -3,13 +3,13 @@ -} let compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c- = λ(A : Type)- → λ(B : Type)- → λ(C : Type)- → λ(f : A → B)- → λ(g : B → C)- → λ(x : A)- → g (f x)+ = λ(A : Type) →+ λ(B : Type) →+ λ(C : Type) →+ λ(f : A → B) →+ λ(g : B → C) →+ λ(x : A) →+ g (f x) let example0 = assert
dhall-lang/Prelude/Integer/abs view
@@ -3,11 +3,9 @@ -} let abs : Integer → Natural- = λ(n : Integer)- → if Natural/isZero (Integer/clamp n)-+ = λ(n : Integer) →+ if Natural/isZero (Integer/clamp n) then Integer/clamp (Integer/negate n)- else Integer/clamp n let example0 = assert : abs +7 ≡ 7
dhall-lang/Prelude/Integer/equal view
@@ -7,9 +7,9 @@ let equal : Integer → Integer → Bool- = λ(a : Integer)- → λ(b : Integer)- → Natural/equal (Integer/clamp a) (Integer/clamp b)+ = λ(a : Integer) →+ λ(b : Integer) →+ Natural/equal (Integer/clamp a) (Integer/clamp b) && Natural/equal (Integer/clamp (Integer/negate a)) (Integer/clamp (Integer/negate b))
dhall-lang/Prelude/Integer/lessThanEqual view
@@ -19,15 +19,13 @@ let lessThanEqual : Integer → Integer → Bool- = λ(x : Integer)- → λ(y : Integer)- → if nonPositive x-+ = λ(x : Integer) →+ λ(y : Integer) →+ if nonPositive x then nonNegative y || Natural/greaterThanEqual (Integer/clamp (Integer/negate x)) (Integer/clamp (Integer/negate y))- else Natural/lessThanEqual (Integer/clamp x) (Integer/clamp y) let example0 = assert : lessThanEqual +5 +6 ≡ True
dhall-lang/Prelude/Integer/multiply view
@@ -7,26 +7,20 @@ ? ./nonPositive let multiplyNonNegative =- λ(x : Integer)- → λ(y : Integer)- → Natural/toInteger (Integer/clamp x * Integer/clamp y)+ λ(x : Integer) →+ λ(y : Integer) →+ Natural/toInteger (Integer/clamp x * Integer/clamp y) let multiply : Integer → Integer → Integer- = λ(m : Integer)- → λ(n : Integer)- → if nonPositive m-- then if nonPositive n-+ = λ(m : Integer) →+ λ(n : Integer) →+ if nonPositive m+ then if nonPositive n then multiplyNonNegative (Integer/negate m) (Integer/negate n)- else Integer/negate (multiplyNonNegative (Integer/negate m) n)- else if nonPositive n- then Integer/negate (multiplyNonNegative m (Integer/negate n))- else multiplyNonNegative m n let example0 = assert : multiply +3 +5 ≡ +15
dhall-lang/Prelude/Integer/subtract view
@@ -6,40 +6,32 @@ ? ./nonPositive let subtractNonNegative =- λ(xi : Integer)- → λ(yi : Integer)- → let xn = Integer/clamp xi+ λ(xi : Integer) →+ λ(yi : Integer) →+ let xn = Integer/clamp xi let yn = Integer/clamp yi let dn = Natural/subtract xn yn - in if Natural/isZero dn-+ in if Natural/isZero dn then Integer/negate (Natural/toInteger (Natural/subtract yn xn))- else Natural/toInteger dn let subtract : Integer → Integer → Integer- = λ(m : Integer)- → λ(n : Integer)- → if nonPositive m-- then if nonPositive n-+ = λ(m : Integer) →+ λ(n : Integer) →+ if nonPositive m+ then if nonPositive n then subtractNonNegative (Integer/negate n) (Integer/negate m)- else Natural/toInteger (Integer/clamp (Integer/negate m) + Integer/clamp n)- else if nonPositive n- then Integer/negate ( Natural/toInteger (Integer/clamp m + Integer/clamp (Integer/negate n)) )- else subtractNonNegative m n let example0 = assert : subtract +3 +5 ≡ +2
dhall-lang/Prelude/Integer/toNatural view
@@ -7,8 +7,8 @@ let toNatural : Integer → Optional Natural- = λ(n : Integer)- → if nonNegative n then Some (Integer/clamp n) else None Natural+ = λ(n : Integer) →+ if nonNegative n then Some (Integer/clamp n) else None Natural let example0 = assert : toNatural +7 ≡ Some 7
dhall-lang/Prelude/JSON/Tagged view
@@ -20,8 +20,8 @@ let wrap : Provisioner → Tagged Provisioner- = λ(x : Provisioner)- → { field = "type", nesting = Nesting.Nested "params", contents = x }+ = λ(x : Provisioner) →+ { field = "type", nesting = Nesting.Nested "params", contents = x } in { provisioners = map@@ -62,8 +62,8 @@ -} let Tagged : Type → Type- = λ(a : Type)- → { field : Text+ = λ(a : Type) →+ { field : Text , nesting : ./Nesting sha256:6284802edd41d5d725aa1ec7687e614e21ad1be7e14dd10996bfa9625105c335 ? ./Nesting
dhall-lang/Prelude/JSON/Type view
@@ -9,32 +9,23 @@ ... corresponds to the following Dhall expression: ```- λ(JSON : Type)-→ λ ( json- : { array :- List JSON → JSON- , bool :- Bool → JSON- , null :- JSON- , double :- Double → JSON- , integer :- Integer → JSON- , object :- List { mapKey : Text, mapValue : JSON } → JSON- , string :- Text → JSON- }- )-→ json.object- [ { mapKey = "foo", mapValue = json.null }- , { mapKey =- "bar"- , mapValue =- json.array [ json.double 1.0, json.bool True ]+λ(JSON : Type) →+λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , null : JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON }- ]+ ) →+ json.object+ [ { mapKey = "foo", mapValue = json.null }+ , { mapKey = "bar"+ , mapValue = json.array [ json.double 1.0, json.bool True ]+ }+ ] ``` You do not need to create these values directly, though. You can use@@ -45,29 +36,27 @@ let JSON = ./package.dhall in JSON.object- [ { mapKey = "foo", mapValue = JSON.null }- , { mapKey =- "bar"- , mapValue =- JSON.array [ JSON.double 1.0, JSON.bool True ]- }- ]+ [ { mapKey = "foo", mapValue = JSON.null }+ , { mapKey = "bar"+ , mapValue = JSON.array [ JSON.double 1.0, JSON.bool True ]+ }+ ] ``` -} let JSON/Type : Type- = ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ = ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON in JSON/Type
dhall-lang/Prelude/JSON/array view
@@ -21,18 +21,18 @@ let array : List JSON → JSON- = λ(x : List JSON)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.array (List/map JSON@1 JSON (λ(j : JSON@1) → j JSON json) x)+ = λ(x : List JSON) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.array (List/map JSON@1 JSON (λ(j : JSON@1) → j JSON json) x) in array
dhall-lang/Prelude/JSON/bool view
@@ -16,18 +16,18 @@ let bool : Bool → JSON- = λ(x : Bool)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.bool x+ = λ(x : Bool) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.bool x in bool
dhall-lang/Prelude/JSON/double view
@@ -16,18 +16,18 @@ let double : Double → JSON- = λ(x : Double)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.double x+ = λ(x : Double) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.double x in double
dhall-lang/Prelude/JSON/integer view
@@ -16,18 +16,18 @@ let integer : Integer → JSON- = λ(x : Integer)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.integer x+ = λ(x : Integer) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.integer x in integer
dhall-lang/Prelude/JSON/natural view
@@ -12,18 +12,18 @@ let natural : Natural → JSON- = λ(x : Natural)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.integer (Natural/toInteger x)+ = λ(x : Natural) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.integer (Natural/toInteger x) in natural
dhall-lang/Prelude/JSON/null view
@@ -12,17 +12,17 @@ let null : JSON- = λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.null+ = λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.null in null
dhall-lang/Prelude/JSON/object view
@@ -27,24 +27,24 @@ let object : List { mapKey : Text, mapValue : JSON } → JSON- = λ(x : List { mapKey : Text, mapValue : JSON })- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.object+ = λ(x : List { mapKey : Text, mapValue : JSON }) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.object ( List/map { mapKey : Text, mapValue : JSON@1 } { mapKey : Text, mapValue : JSON }- ( λ(kv : { mapKey : Text, mapValue : JSON@1 })- → { mapKey = kv.mapKey, mapValue = kv.mapValue JSON json }+ ( λ(kv : { mapKey : Text, mapValue : JSON@1 }) →+ { mapKey = kv.mapKey, mapValue = kv.mapValue JSON json } ) x )
dhall-lang/Prelude/JSON/omitNullFields view
@@ -16,19 +16,19 @@ let omitNullFields : JSON.Type → JSON.Type- = λ(old : JSON.Type)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → let result =+ = λ(old : JSON.Type) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ let result = old { value : JSON, isNull : Bool } { string =@@ -38,32 +38,30 @@ , integer = λ(x : Integer) → { value = json.integer x, isNull = False } , object =- λ ( keyValues- : List- { mapKey : Text- , mapValue : { value : JSON, isNull : Bool }- }- )- → let value =+ λ ( keyValues+ : List+ { mapKey : Text+ , mapValue : { value : JSON, isNull : Bool }+ }+ ) →+ let value = json.object ( List/concatMap { mapKey : Text , mapValue : { value : JSON, isNull : Bool } } { mapKey : Text, mapValue : JSON }- ( λ ( keyValue- : { mapKey : Text- , mapValue :- { value : JSON, isNull : Bool }- }- )- → if keyValue.mapValue.isNull-+ ( λ ( keyValue+ : { mapKey : Text+ , mapValue :+ { value : JSON, isNull : Bool }+ }+ ) →+ if keyValue.mapValue.isNull then [] : List { mapKey : Text , mapValue : JSON }- else [ keyValue.{ mapKey } ∧ { mapValue = keyValue.mapValue.value@@ -73,21 +71,21 @@ keyValues ) - in { value = value, isNull = False }+ in { value, isNull = False } , array =- λ(xs : List { value : JSON, isNull : Bool })- → let value =+ λ(xs : List { value : JSON, isNull : Bool }) →+ let value = json.array ( List/map { value : JSON, isNull : Bool } JSON- ( λ(x : { value : JSON, isNull : Bool })- → x.value+ ( λ(x : { value : JSON, isNull : Bool }) →+ x.value ) xs ) - in { value = value, isNull = False }+ in { value, isNull = False } , bool = λ(x : Bool) → { value = json.bool x, isNull = False } , null = { value = json.null, isNull = True } }@@ -95,10 +93,10 @@ in result.value let property =- λ(a : Text)- → λ(b : Double)- → λ(c : Bool)- → assert+ λ(a : Text) →+ λ(b : Double) →+ λ(c : Bool) →+ assert : omitNullFields ( JSON.object ( toMap
dhall-lang/Prelude/JSON/renderAs view
@@ -42,12 +42,12 @@ let List/uncons : ∀(a : Type) → List a → Optional (NonEmpty a)- = λ(a : Type)- → λ(ls : List a)- → Optional/map+ = λ(a : Type) →+ λ(ls : List a) →+ Optional/map a (NonEmpty a)- (λ(head : a) → { head = head, tail = List/drop 1 a ls })+ (λ(head : a) → { head, tail = List/drop 1 a ls }) (List/head a ls) let NonEmpty/singleton@@ -60,9 +60,9 @@ let NonEmpty/concat : ∀(a : Type) → NonEmpty (NonEmpty a) → NonEmpty a- = λ(a : Type)- → λ(lss : NonEmpty (NonEmpty a))- → { head = lss.head.head+ = λ(a : Type) →+ λ(lss : NonEmpty (NonEmpty a)) →+ { head = lss.head.head , tail = lss.head.tail # List/concatMap (NonEmpty a) a (NonEmpty/toList a) lss.tail@@ -70,32 +70,32 @@ let NonEmpty/map : ∀(a : Type) → ∀(b : Type) → (a → b) → NonEmpty a → NonEmpty b- = λ(a : Type)- → λ(b : Type)- → λ(fn : a → b)- → λ(ls : NonEmpty a)- → { head = fn ls.head, tail = List/map a b fn ls.tail }+ = λ(a : Type) →+ λ(b : Type) →+ λ(fn : a → b) →+ λ(ls : NonEmpty a) →+ { head = fn ls.head, tail = List/map a b fn ls.tail } let NonEmpty/mapHead : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(fn : a → a)- → λ(ls : NonEmpty a)- → ls ⫽ { head = fn ls.head }+ = λ(a : Type) →+ λ(fn : a → a) →+ λ(ls : NonEmpty a) →+ ls ⫽ { head = fn ls.head } let NonEmpty/mapTail : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(fn : a → a)- → λ(ls : NonEmpty a)- → ls ⫽ { tail = List/map a a fn ls.tail }+ = λ(a : Type) →+ λ(fn : a → a) →+ λ(ls : NonEmpty a) →+ ls ⫽ { tail = List/map a a fn ls.tail } let List/splitAt : Natural → ∀(a : Type) → List a → { head : List a, tail : List a }- = λ(index : Natural)- → λ(a : Type)- → λ(ls : List a)- → { head = List/take index a ls, tail = List/drop index a ls }+ = λ(index : Natural) →+ λ(a : Type) →+ λ(ls : List a) →+ { head = List/take index a ls, tail = List/drop index a ls } let _testSplitAt0 = assert@@ -117,33 +117,31 @@ ≡ { head = [] : List Natural, tail = [] : List Natural } let List/splitLast =- λ(a : Type)- → λ(ls : List a)- → List/splitAt (Natural/subtract 1 (List/length a ls)) a ls+ λ(a : Type) →+ λ(ls : List a) →+ List/splitAt (Natural/subtract 1 (List/length a ls)) a ls let NonEmpty/prepend : ∀(a : Type) → a → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(prefix : a)- → λ(ls : NonEmpty a)- → { head = prefix, tail = NonEmpty/toList a ls }+ = λ(a : Type) →+ λ(prefix : a) →+ λ(ls : NonEmpty a) →+ { head = prefix, tail = NonEmpty/toList a ls } let NonEmpty/append : ∀(a : Type) → a → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(suffix : a)- → λ(ls : NonEmpty a)- → { head = ls.head, tail = ls.tail # [ suffix ] }+ = λ(a : Type) →+ λ(suffix : a) →+ λ(ls : NonEmpty a) →+ { head = ls.head, tail = ls.tail # [ suffix ] } let NonEmpty/mapLast : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(fn : a → a)- → λ(ls : NonEmpty a)- → if List/null a ls.tail-+ = λ(a : Type) →+ λ(fn : a → a) →+ λ(ls : NonEmpty a) →+ if List/null a ls.tail then { head = fn ls.head, tail = [] : List a }- else let split = List/splitLast a ls.tail in { head = ls.head@@ -152,13 +150,11 @@ let NonEmpty/mapLeading : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a- = λ(a : Type)- → λ(fn : a → a)- → λ(ls : NonEmpty a)- → if List/null a ls.tail-+ = λ(a : Type) →+ λ(fn : a → a) →+ λ(ls : NonEmpty a) →+ if List/null a ls.tail then ls- else let split = List/splitLast a ls.tail in { head = fn ls.head@@ -175,8 +171,8 @@ let Block/toLines : Block → Lines- = λ(block : Block)- → merge+ = λ(block : Block) →+ merge { Simple = NonEmpty/singleton Text , Complex = Function/identity Lines }@@ -184,11 +180,11 @@ let manyBlocks : ∀(a : Type) → Text → (NonEmpty a → Lines) → List a → Block- = λ(a : Type)- → λ(ifEmpty : Text)- → λ(render : NonEmpty a → Lines)- → λ(inputs : List a)- → merge+ = λ(a : Type) →+ λ(ifEmpty : Text) →+ λ(render : NonEmpty a → Lines) →+ λ(inputs : List a) →+ merge { Some = λ(inputs : NonEmpty a) → Block.Complex (render inputs) , None = Block.Simple ifEmpty }@@ -196,8 +192,8 @@ let blockToText : Block → Text- = λ(block : Block)- → Text/concatMap+ = λ(block : Block) →+ Text/concatMap Text (λ(line : Text) → line ++ "\n") (NonEmpty/toList Text (Block/toLines block))@@ -215,10 +211,10 @@ let ObjectField = { mapKey : Text, mapValue : Block } let renderJSONStruct =- λ(prefix : Text)- → λ(suffix : Text)- → λ(blocks : NonEmpty Lines)- → let indent = NonEmpty/map Text Text addIndent+ λ(prefix : Text) →+ λ(suffix : Text) →+ λ(blocks : NonEmpty Lines) →+ let indent = NonEmpty/map Text Text addIndent let appendComma : Lines → Lines@@ -228,40 +224,38 @@ let block = NonEmpty/concat Text blocks - in if List/null Text block.tail-+ in if List/null Text block.tail then NonEmpty/singleton Text "${prefix} ${block.head} ${suffix}"- else NonEmpty/prepend Text prefix (NonEmpty/append Text suffix (indent block)) let renderObject =- λ(format : Format)- → λ(fields : NonEmpty ObjectField)- → let keystr = λ(field : ObjectField) → "${Text/show field.mapKey}:"+ λ(format : Format) →+ λ(fields : NonEmpty ObjectField) →+ let keystr = λ(field : ObjectField) → "${Text/show field.mapKey}:" let prefixKeyOnFirst =- λ(field : ObjectField)- → NonEmpty/mapHead+ λ(field : ObjectField) →+ NonEmpty/mapHead Text (addPrefix "${keystr field} ") (Block/toLines field.mapValue) let prependKeyLine =- λ(field : ObjectField)- → NonEmpty/prepend+ λ(field : ObjectField) →+ NonEmpty/prepend Text (keystr field) (Block/toLines field.mapValue) let renderYAMLField =- λ(field : ObjectField)- → merge+ λ(field : ObjectField) →+ merge { Simple =- λ(line : Text)- → NonEmpty/singleton Text "${keystr field} ${line}"+ λ(line : Text) →+ NonEmpty/singleton Text "${keystr field} ${line}" , Complex = λ(_ : Lines) → indentTail (prependKeyLine field) } field.mapValue@@ -280,16 +274,16 @@ format let renderYAMLArrayField =- λ(block : Block)- → NonEmpty/mapHead+ λ(block : Block) →+ NonEmpty/mapHead Text (addPrefix "- ") (indentTail (Block/toLines block)) let renderArray =- λ(format : Format)- → λ(fields : NonEmpty Block)- → merge+ λ(format : Format) →+ λ(fields : NonEmpty Block) →+ merge { JSON = renderJSONStruct "["@@ -304,9 +298,9 @@ let renderAs : Format → JSON.Type → Text- = λ(format : Format)- → λ(json : JSON.Type)- → blockToText+ = λ(format : Format) →+ λ(json : JSON.Type) →+ blockToText ( json Block { string = λ(x : Text) → Block.Simple (Text/show x)
dhall-lang/Prelude/JSON/renderInteger.dhall view
@@ -8,11 +8,9 @@ let renderInteger : Integer → Text- = λ(integer : Integer)- → if Integer/nonNegative integer-+ = λ(integer : Integer) →+ if Integer/nonNegative integer then Natural/show (Integer/clamp integer)- else Integer/show integer let positive = assert : renderInteger +1 ≡ "1"
dhall-lang/Prelude/JSON/string view
@@ -16,18 +16,18 @@ let string : Text → JSON- = λ(x : Text)- → λ(JSON : Type)- → λ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → json.string x+ = λ(x : Text) →+ λ(JSON : Type) →+ λ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ json.string x in string
dhall-lang/Prelude/JSON/tagInline view
@@ -10,10 +10,10 @@ let tagInline : Text → ∀(a : Type) → a → Tagged a- = λ(tagFieldName : Text)- → λ(a : Type)- → λ(contents : a)- → { nesting = Nesting.Inline, field = tagFieldName, contents = contents }+ = λ(tagFieldName : Text) →+ λ(a : Type) →+ λ(contents : a) →+ { nesting = Nesting.Inline, field = tagFieldName, contents } let example0 = let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
dhall-lang/Prelude/JSON/tagNested view
@@ -10,13 +10,13 @@ let tagNested : Text → Text → ∀(a : Type) → a → Tagged a- = λ(contentsFieldName : Text)- → λ(tagFieldName : Text)- → λ(a : Type)- → λ(contents : a)- → { nesting = Nesting.Nested contentsFieldName+ = λ(contentsFieldName : Text) →+ λ(tagFieldName : Text) →+ λ(a : Type) →+ λ(contents : a) →+ { nesting = Nesting.Nested contentsFieldName , field = tagFieldName- , contents = contents+ , contents } let example0 =
dhall-lang/Prelude/List/all view
@@ -4,10 +4,10 @@ -} let all : ∀(a : Type) → (a → Bool) → List a → Bool- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : List a)- → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : List a) →+ List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True let example0 = assert : all Natural Natural/even [ 2, 3, 5 ] ≡ False
dhall-lang/Prelude/List/any view
@@ -4,10 +4,10 @@ -} let any : ∀(a : Type) → (a → Bool) → List a → Bool- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : List a)- → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : List a) →+ List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False let example0 = assert : any Natural Natural/even [ 2, 3, 5 ] ≡ True
dhall-lang/Prelude/List/build view
@@ -2,19 +2,19 @@ `build` is the inverse of `fold` -} let build- : ∀(a : Type)- → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)- → List a+ : ∀(a : Type) →+ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →+ List a = List/build let example0 = assert : build Text- ( λ(list : Type)- → λ(cons : Text → list → list)- → λ(nil : list)- → cons "ABC" (cons "DEF" nil)+ ( λ(list : Type) →+ λ(cons : Text → list → list) →+ λ(nil : list) →+ cons "ABC" (cons "DEF" nil) ) ≡ [ "ABC", "DEF" ] @@ -22,10 +22,10 @@ assert : build Text- ( λ(list : Type)- → λ(cons : Text → list → list)- → λ(nil : list)- → nil+ ( λ(list : Type) →+ λ(cons : Text → list → list) →+ λ(nil : list) →+ nil ) ≡ ([] : List Text)
dhall-lang/Prelude/List/concat view
@@ -3,14 +3,14 @@ -} let concat : ∀(a : Type) → List (List a) → List a- = λ(a : Type)- → λ(xss : List (List a))- → List/build+ = λ(a : Type) →+ λ(xss : List (List a)) →+ List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → λ(nil : list)- → List/fold+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ λ(nil : list) →+ List/fold (List a) xss list
dhall-lang/Prelude/List/concatMap view
@@ -4,15 +4,15 @@ -} let concatMap : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b- = λ(a : Type)- → λ(b : Type)- → λ(f : a → List b)- → λ(xs : List a)- → List/build+ = λ(a : Type) →+ λ(b : Type) →+ λ(f : a → List b) →+ λ(xs : List a) →+ List/build b- ( λ(list : Type)- → λ(cons : b → list → list)- → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons)+ ( λ(list : Type) →+ λ(cons : b → list → list) →+ List/fold a xs list (λ(x : a) → List/fold b (f x) list cons) ) let example0 =
dhall-lang/Prelude/List/default view
@@ -4,9 +4,9 @@ -} let default : ∀(a : Type) → Optional (List a) → List a- = λ(a : Type)- → λ(o : Optional (List a))- → merge { Some = λ(l : List a) → l, None = [] : List a } o+ = λ(a : Type) →+ λ(o : Optional (List a)) →+ merge { Some = λ(l : List a) → l, None = [] : List a } o let example0 = assert : default Bool (None (List Bool)) ≡ ([] : List Bool)
dhall-lang/Prelude/List/drop view
@@ -5,19 +5,17 @@ let drop : ∀(n : Natural) → ∀(a : Type) → List a → List a- = λ(n : Natural)- → λ(a : Type)- → λ(xs : List a)- → List/fold+ = λ(n : Natural) →+ λ(a : Type) →+ λ(xs : List a) →+ List/fold { index : Natural, value : a } (List/indexed a xs) (List a)- ( λ(x : { index : Natural, value : a })- → λ(xs : List a)- → if Natural/greaterThanEqual x.index n-+ ( λ(x : { index : Natural, value : a }) →+ λ(xs : List a) →+ if Natural/greaterThanEqual x.index n then [ x.value ] # xs- else xs ) ([] : List a)
dhall-lang/Prelude/List/filter view
@@ -5,14 +5,14 @@ -} let filter : ∀(a : Type) → (a → Bool) → List a → List a- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : List a)- → List/build+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : List a) →+ List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ List/fold a xs list
dhall-lang/Prelude/List/fold view
@@ -5,12 +5,12 @@ `fold` just replaces each `cons` and `nil` with something else -} let fold- : ∀(a : Type)- → List a- → ∀(list : Type)- → ∀(cons : a → list → list)- → ∀(nil : list)- → list+ : ∀(a : Type) →+ List a →+ ∀(list : Type) →+ ∀(cons : a → list → list) →+ ∀(nil : list) →+ list = List/fold let example0 =@@ -25,8 +25,8 @@ let example1 = assert- : ( λ(nil : Natural)- → fold+ : ( λ(nil : Natural) →+ fold Natural [ 2, 3, 5 ] Natural@@ -37,15 +37,15 @@ let example2 = assert- : ( λ(list : Type)- → λ(cons : Natural → list → list)- → λ(nil : list)- → fold Natural [ 2, 3, 5 ] list cons nil+ : ( λ(list : Type) →+ λ(cons : Natural → list → list) →+ λ(nil : list) →+ fold Natural [ 2, 3, 5 ] list cons nil )- ≡ ( λ(list : Type)- → λ(cons : Natural → list → list)- → λ(nil : list)- → cons 2 (cons 3 (cons 5 nil))+ ≡ ( λ(list : Type) →+ λ(cons : Natural → list → list) →+ λ(nil : list) →+ cons 2 (cons 3 (cons 5 nil)) ) in fold
dhall-lang/Prelude/List/generate view
@@ -4,22 +4,22 @@ -} let generate : Natural → ∀(a : Type) → (Natural → a) → List a- = λ(n : Natural)- → λ(a : Type)- → λ(f : Natural → a)- → List/build+ = λ(n : Natural) →+ λ(a : Type) →+ λ(f : Natural → a) →+ List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ List/fold { index : Natural, value : {} } ( List/indexed {} ( List/build {}- ( λ(list : Type)- → λ(cons : {} → list → list)- → Natural/fold n list (cons {=})+ ( λ(list : Type) →+ λ(cons : {} → list → list) →+ Natural/fold n list (cons {=}) ) ) )
dhall-lang/Prelude/List/iterate view
@@ -4,29 +4,29 @@ -} let iterate : Natural → ∀(a : Type) → (a → a) → a → List a- = λ(n : Natural)- → λ(a : Type)- → λ(f : a → a)- → λ(x : a)- → List/build+ = λ(n : Natural) →+ λ(a : Type) →+ λ(f : a → a) →+ λ(x : a) →+ List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ List/fold { index : Natural, value : {} } ( List/indexed {} ( List/build {}- ( λ(list : Type)- → λ(cons : {} → list → list)- → Natural/fold n list (cons {=})+ ( λ(list : Type) →+ λ(cons : {} → list → list) →+ Natural/fold n list (cons {=}) ) ) ) list- ( λ(y : { index : Natural, value : {} })- → cons (Natural/fold y.index a f x)+ ( λ(y : { index : Natural, value : {} }) →+ cons (Natural/fold y.index a f x) ) )
dhall-lang/Prelude/List/map view
@@ -3,15 +3,15 @@ -} let map : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b- = λ(a : Type)- → λ(b : Type)- → λ(f : a → b)- → λ(xs : List a)- → List/build+ = λ(a : Type) →+ λ(b : Type) →+ λ(f : a → b) →+ λ(xs : List a) →+ List/build b- ( λ(list : Type)- → λ(cons : b → list → list)- → List/fold a xs list (λ(x : a) → cons (f x))+ ( λ(list : Type) →+ λ(cons : b → list → list) →+ List/fold a xs list (λ(x : a) → cons (f x)) ) let example0 =
dhall-lang/Prelude/List/package.dhall view
@@ -70,10 +70,13 @@ , take = ./take sha256:b3e08ee8c3a5bf3d8ccee6b2b2008fbb8e51e7373aef6f1af67ad10078c9fbfa ? ./take+, unpackOptionals =+ ./unpackOptionals sha256:0cbaa920f429cf7fc3907f8a9143203fe948883913560e6e1043223e6b3d05e4+ ? ./unpackOptionals , unzip = ./unzip sha256:4d6003e9e683a289fe33f4c90f958eb1e08ea0bbb474210fcd90d1885c9660e9 ? ./unzip , zip =- ./zip sha256:7be343f42cddb7e3b5884611ae5c8731e76e52b22d7bb45420cae7c9a82be0ca+ ./zip sha256:85ed955eabf3998767f4ad2a28e57d40cd4c68a95519d79e9b622f1d26d979da ? ./zip }
dhall-lang/Prelude/List/partition view
@@ -8,19 +8,17 @@ let partition : ∀(a : Type) → (a → Bool) → List a → Partition a- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : List a)- → List/fold+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : List a) →+ List/fold a xs (Partition a)- ( λ(x : a)- → λ(p : Partition a)- → if f x-+ ( λ(x : a) →+ λ(p : Partition a) →+ if f x then { true = [ x ] # p.true, false = p.false }- else { true = p.true, false = [ x ] # p.false } ) { true = [] : List a, false = [] : List a }
dhall-lang/Prelude/List/replicate view
@@ -3,14 +3,14 @@ -} let replicate : Natural → ∀(a : Type) → a → List a- = λ(n : Natural)- → λ(a : Type)- → λ(x : a)- → List/build+ = λ(n : Natural) →+ λ(a : Type) →+ λ(x : a) →+ List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → Natural/fold n list (cons x)+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ Natural/fold n list (cons x) ) let example0 = assert : replicate 9 Natural 1 ≡ [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
dhall-lang/Prelude/List/shifted view
@@ -3,38 +3,38 @@ number of elements in preceding lists -} let shifted- : ∀(a : Type)- → List (List { index : Natural, value : a })- → List { index : Natural, value : a }- = λ(a : Type)- → λ(kvss : List (List { index : Natural, value : a }))- → List/build+ : ∀(a : Type) →+ List (List { index : Natural, value : a }) →+ List { index : Natural, value : a }+ = λ(a : Type) →+ λ(kvss : List (List { index : Natural, value : a })) →+ List/build { index : Natural, value : a }- ( λ(list : Type)- → λ(cons : { index : Natural, value : a } → list → list)- → λ(nil : list)- → let result =+ ( λ(list : Type) →+ λ(cons : { index : Natural, value : a } → list → list) →+ λ(nil : list) →+ let result = List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff : Natural → list }- ( λ(kvs : List { index : Natural, value : a })- → λ(y : { count : Natural, diff : Natural → list })- → let length =+ ( λ(kvs : List { index : Natural, value : a }) →+ λ(y : { count : Natural, diff : Natural → list }) →+ let length = List/length { index : Natural, value : a } kvs in { count = y.count + length , diff =- λ(n : Natural)- → List/fold+ λ(n : Natural) →+ List/fold { index : Natural, value : a } kvs list- ( λ ( kvOld- : { index : Natural, value : a }- )- → λ(z : list)- → let kvNew =+ ( λ ( kvOld+ : { index : Natural, value : a }+ ) →+ λ(z : list) →+ let kvNew = { index = kvOld.index + n , value = kvOld.value }
dhall-lang/Prelude/List/take view
@@ -5,16 +5,16 @@ let take : ∀(n : Natural) → ∀(a : Type) → List a → List a- = λ(n : Natural)- → λ(a : Type)- → λ(xs : List a)- → List/fold+ = λ(n : Natural) →+ λ(a : Type) →+ λ(xs : List a) →+ List/fold { index : Natural, value : a } (List/indexed a xs) (List a)- ( λ(x : { index : Natural, value : a })- → λ(xs : List a)- → if Natural/lessThan x.index n then [ x.value ] # xs else xs+ ( λ(x : { index : Natural, value : a }) →+ λ(xs : List a) →+ if Natural/lessThan x.index n then [ x.value ] # xs else xs ) ([] : List a)
+ dhall-lang/Prelude/List/unpackOptionals view
@@ -0,0 +1,37 @@+{-+Unpack Optionals in a List, omitting None items.+-}++let List/concatMap =+ ./concatMap sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64+ ? ./concatMap++let Optional/toList =+ ../Optional/toList sha256:d78f160c619119ef12389e48a629ce293d69f7624c8d016b7a4767ab400344c4+ ? ../Optional/toList++let unpackOptionals+ : ∀(a : Type) → ∀(l : List (Optional a)) → List a+ = λ(a : Type) → List/concatMap (Optional a) a (Optional/toList a)++let property1 =+ λ(a : Type) → λ(x : a) → assert : unpackOptionals a [ Some x ] ≡ [ x ]++let property2 =+ λ(a : Type) → assert : unpackOptionals a [ None a ] ≡ ([] : List a)++let example0 =+ assert+ : unpackOptionals Natural [ Some 1, None Natural, Some 3 ] ≡ [ 1, 3 ]++let example1 =+ assert+ : unpackOptionals Natural ([] : List (Optional Natural))+ ≡ ([] : List Natural)++let example2 =+ assert+ : unpackOptionals Natural [ None Natural, None Natural ]+ ≡ ([] : List Natural)++in unpackOptionals
dhall-lang/Prelude/List/unzip view
@@ -2,19 +2,19 @@ Unzip a `List` into two separate `List`s -} let unzip- : ∀(a : Type)- → ∀(b : Type)- → List { _1 : a, _2 : b }- → { _1 : List a, _2 : List b }- = λ(a : Type)- → λ(b : Type)- → λ(xs : List { _1 : a, _2 : b })- → { _1 =+ : ∀(a : Type) →+ ∀(b : Type) →+ List { _1 : a, _2 : b } →+ { _1 : List a, _2 : List b }+ = λ(a : Type) →+ λ(b : Type) →+ λ(xs : List { _1 : a, _2 : b }) →+ { _1 = List/build a- ( λ(list : Type)- → λ(cons : a → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : a → list → list) →+ List/fold { _1 : a, _2 : b } xs list@@ -23,9 +23,9 @@ , _2 = List/build b- ( λ(list : Type)- → λ(cons : b → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : b → list → list) →+ List/fold { _1 : a, _2 : b } xs list
dhall-lang/Prelude/List/zip view
@@ -3,47 +3,55 @@ Resulting `List` will have the length of the shortest of its arguments. -}-let List/drop =- ./drop sha256:af983ba3ead494dd72beed05c0f3a17c36a4244adedf7ced502c6512196ed0cf+let List/index =+ ./index sha256:e657b55ecae4d899465c3032cb1a64c6aa6dc2aa3034204f3c15ce5c96c03e63+ ? ./index let zip : ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }- = λ(a : Type)- → λ(xa : List a)- → λ(b : Type)- → λ(xb : List b)- → let Carry = { acc : List { _1 : a, _2 : b }, context : List b }-- let cons =- λ(elem : a)- → λ(prev : Carry)- → let nextAcc =- merge- { Some =- λ(bb : b) → [ { _1 = elem, _2 = bb } ] # prev.acc- , None = prev.acc- }- (List/head b prev.context)-- in { acc = nextAcc, context = List/drop 1 b prev.context }-- let nil = { acc = [] : List { _1 : a, _2 : b }, context = xb }-- let result = List/fold a xa Carry cons nil+ = λ(a : Type) →+ λ(xs : List a) →+ λ(b : Type) →+ λ(ys : List b) →+ let ixs = List/indexed a xs - in result.acc+ in List/build+ { _1 : a, _2 : b }+ ( λ(list : Type) →+ λ(cons : { _1 : a, _2 : b } → list → list) →+ λ(nil : list) →+ List/fold+ { index : Natural, value : a }+ ixs+ list+ ( λ(ix : { index : Natural, value : a }) →+ λ(rest : list) →+ merge+ { None = rest+ , Some =+ λ(y : b) → cons { _1 = ix.value, _2 = y } rest+ }+ (List/index ix.index b ys)+ )+ nil+ ) let example0 = assert- : zip Text [ "ABC", "DEF", "GHI" ] Bool [ True, False, True ]- ≡ [ { _1 = "ABC", _2 = True }- , { _1 = "DEF", _2 = False }- , { _1 = "GHI", _2 = True }+ : zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1, 2, 3 ]+ ≡ [ { _1 = "ABC", _2 = 1 }+ , { _1 = "DEF", _2 = 2 }+ , { _1 = "GHI", _2 = 3 } ] let example1 = assert : zip Text [ "ABC" ] Bool ([] : List Bool) ≡ ([] : List { _1 : Text, _2 : Bool })++let example2 =+ assert+ : zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1 ]+ ≡ [ { _1 = "ABC", _2 = 1 } ] in zip
dhall-lang/Prelude/Location/Type view
@@ -6,9 +6,8 @@ let example0 = assert- : ( missing sha256:f428188ff9d77ea15bc2bcd0da3f8ed81b304e175b07ade42a3b0fb02941b2aa as Location- ? missing as Location- )+ : missing sha256:f428188ff9d77ea15bc2bcd0da3f8ed81b304e175b07ade42a3b0fb02941b2aa as Location+ ? missing as Location ≡ < Environment : Text | Local : Text | Missing
dhall-lang/Prelude/Map/keyValue view
@@ -3,10 +3,10 @@ homogeneous record by dhall-to-json and dhall-to-yaml. -} let keyValue =- λ(v : Type)- → λ(key : Text)- → λ(value : v)- → { mapKey = key, mapValue = value }+ λ(v : Type) →+ λ(key : Text) →+ λ(value : v) →+ { mapKey = key, mapValue = value } let example0 = assert : keyValue Natural "foo" 2 ≡ { mapKey = "foo", mapValue = 2 }
dhall-lang/Prelude/Map/keys view
@@ -15,9 +15,9 @@ let keys : ∀(k : Type) → ∀(v : Type) → Map k v → List k- = λ(k : Type)- → λ(v : Type)- → List/map (Entry k v) k (λ(x : Entry k v) → x.mapKey)+ = λ(k : Type) →+ λ(v : Type) →+ List/map (Entry k v) k (λ(x : Entry k v) → x.mapKey) let example0 = assert
dhall-lang/Prelude/Map/map view
@@ -15,16 +15,16 @@ let map : ∀(k : Type) → ∀(a : Type) → ∀(b : Type) → (a → b) → Map k a → Map k b- = λ(k : Type)- → λ(a : Type)- → λ(b : Type)- → λ(f : a → b)- → λ(m : Map k a)- → List/map+ = λ(k : Type) →+ λ(a : Type) →+ λ(b : Type) →+ λ(f : a → b) →+ λ(m : Map k a) →+ List/map (Entry k a) (Entry k b)- ( λ(before : Entry k a)- → { mapKey = before.mapKey, mapValue = f before.mapValue }+ ( λ(before : Entry k a) →+ { mapKey = before.mapKey, mapValue = f before.mapValue } ) m
dhall-lang/Prelude/Map/values view
@@ -15,9 +15,9 @@ let values : ∀(k : Type) → ∀(v : Type) → Map k v → List v- = λ(k : Type)- → λ(v : Type)- → List/map (Entry k v) v (λ(x : Entry k v) → x.mapValue)+ = λ(k : Type) →+ λ(v : Type) →+ List/map (Entry k v) v (λ(x : Entry k v) → x.mapValue) let example0 = assert
dhall-lang/Prelude/Natural/build view
@@ -2,31 +2,31 @@ `build` is the inverse of `fold` -} let build- : ( ∀(natural : Type)- → ∀(succ : natural → natural)- → ∀(zero : natural)- → natural- )- → Natural+ : ( ∀(natural : Type) →+ ∀(succ : natural → natural) →+ ∀(zero : natural) →+ natural+ ) →+ Natural = Natural/build let example0 = assert : build- ( λ(natural : Type)- → λ(succ : natural → natural)- → λ(zero : natural)- → succ (succ (succ zero))+ ( λ(natural : Type) →+ λ(succ : natural → natural) →+ λ(zero : natural) →+ succ (succ (succ zero)) ) ≡ 3 let example1 = assert : build- ( λ(natural : Type)- → λ(succ : natural → natural)- → λ(zero : natural)- → zero+ ( λ(natural : Type) →+ λ(succ : natural → natural) →+ λ(zero : natural) →+ zero ) ≡ 0
dhall-lang/Prelude/Natural/enumerate view
@@ -4,20 +4,20 @@ -} let enumerate : Natural → List Natural- = λ(n : Natural)- → List/build+ = λ(n : Natural) →+ List/build Natural- ( λ(list : Type)- → λ(cons : Natural → list → list)- → List/fold+ ( λ(list : Type) →+ λ(cons : Natural → list → list) →+ List/fold { index : Natural, value : {} } ( List/indexed {} ( List/build {}- ( λ(list : Type)- → λ(cons : {} → list → list)- → Natural/fold n list (cons {=})+ ( λ(list : Type) →+ λ(cons : {} → list → list) →+ Natural/fold n list (cons {=}) ) ) )
dhall-lang/Prelude/Natural/fold view
@@ -5,11 +5,11 @@ replaces each `succ` and `zero` with something else -} let fold- : Natural- → ∀(natural : Type)- → ∀(succ : natural → natural)- → ∀(zero : natural)- → natural+ : Natural →+ ∀(natural : Type) →+ ∀(succ : natural → natural) →+ ∀(zero : natural) →+ natural = Natural/fold let example0 = assert : fold 3 Natural (λ(x : Natural) → 5 * x) 1 ≡ 125@@ -21,15 +21,15 @@ let example2 = assert- : ( λ(natural : Type)- → λ(succ : natural → natural)- → λ(zero : natural)- → fold 3 natural succ zero+ : ( λ(natural : Type) →+ λ(succ : natural → natural) →+ λ(zero : natural) →+ fold 3 natural succ zero )- ≡ ( λ(natural : Type)- → λ(succ : natural → natural)- → λ(zero : natural)- → succ (succ (succ zero))+ ≡ ( λ(natural : Type) →+ λ(succ : natural → natural) →+ λ(zero : natural) →+ succ (succ (succ zero)) ) in fold
dhall-lang/Prelude/Natural/listMax view
@@ -12,8 +12,8 @@ let listMax : List Natural → Optional Natural- = λ(xs : List Natural)- → Optional/map+ = λ(xs : List Natural) →+ Optional/map Natural Natural (λ(n : Natural) → List/fold Natural xs Natural max n)
dhall-lang/Prelude/Natural/listMin view
@@ -12,12 +12,12 @@ let listMin : List Natural → Optional Natural- = λ(xs : List Natural)- → Optional/map+ = λ(xs : List Natural) →+ Optional/map Natural Natural- ( λ(n : Natural)- → if Natural/isZero n then n else List/fold Natural xs Natural min n+ ( λ(n : Natural) →+ if Natural/isZero n then n else List/fold Natural xs Natural min n ) (List/head Natural xs)
dhall-lang/Prelude/Natural/product view
@@ -3,8 +3,8 @@ -} let product : List Natural → Natural- = λ(xs : List Natural)- → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) 1+ = λ(xs : List Natural) →+ List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) 1 let example0 = assert : product [ 2, 3, 5 ] ≡ 30
dhall-lang/Prelude/Natural/sort view
@@ -16,8 +16,8 @@ let Accumulator = { sorted : List Natural, rest : List Natural } let partitionMinima =- λ(xs : List Natural)- → merge+ λ(xs : List Natural) →+ merge { Some = λ(m : Natural) → List/partition Natural (greaterThanEqual m) xs , None = { true = [] : List Natural, false = [] : List Natural }@@ -29,8 +29,8 @@ : partitionMinima [ 2, 1, 1, 3 ] ≡ { true = [ 1, 1 ], false = [ 2, 3 ] } let step =- λ(x : Accumulator)- → let p = partitionMinima x.rest+ λ(x : Accumulator) →+ let p = partitionMinima x.rest in { sorted = x.sorted # p.true, rest = p.false } @@ -41,8 +41,8 @@ let sort : List Natural → List Natural- = λ(xs : List Natural)- → let x =+ = λ(xs : List Natural) →+ let x = Natural/fold (List/length Natural xs) Accumulator
dhall-lang/Prelude/Natural/sum view
@@ -3,8 +3,8 @@ -} let sum : List Natural → Natural- = λ(xs : List Natural)- → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) 0+ = λ(xs : List Natural) →+ List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) 0 let example = assert : sum [ 2, 3, 5 ] ≡ 10
dhall-lang/Prelude/Optional/all view
@@ -4,10 +4,10 @@ -} let all : ∀(a : Type) → (a → Bool) → Optional a → Bool- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : Optional a)- → merge { Some = f, None = True } xs+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : Optional a) →+ merge { Some = f, None = True } xs let example0 = assert : all Natural Natural/even (Some 3) ≡ False
dhall-lang/Prelude/Optional/any view
@@ -4,10 +4,10 @@ -} let any : ∀(a : Type) → (a → Bool) → Optional a → Bool- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : Optional a)- → merge { Some = f, None = False } xs+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : Optional a) →+ merge { Some = f, None = False } xs let example0 = assert : any Natural Natural/even (Some 2) ≡ True
dhall-lang/Prelude/Optional/build view
@@ -2,30 +2,30 @@ `build` is the inverse of `fold` -} let build- : ∀(a : Type)- → ( ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional- )- → Optional a- = λ(a : Type)- → λ ( build- : ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional- )- → build (Optional a) (λ(x : a) → Some x) (None a)+ : ∀(a : Type) →+ ( ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional+ ) →+ Optional a+ = λ(a : Type) →+ λ ( build+ : ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional+ ) →+ build (Optional a) (λ(x : a) → Some x) (None a) let example0 = assert : build Natural- ( λ(optional : Type)- → λ(some : Natural → optional)- → λ(none : optional)- → some 1+ ( λ(optional : Type) →+ λ(some : Natural → optional) →+ λ(none : optional) →+ some 1 ) ≡ Some 1 @@ -33,10 +33,10 @@ assert : build Natural- ( λ(optional : Type)- → λ(some : Natural → optional)- → λ(none : optional)- → none+ ( λ(optional : Type) →+ λ(some : Natural → optional) →+ λ(none : optional) →+ none ) ≡ None Natural
dhall-lang/Prelude/Optional/concat view
@@ -3,9 +3,9 @@ -} let concat : ∀(a : Type) → Optional (Optional a) → Optional a- = λ(a : Type)- → λ(x : Optional (Optional a))- → merge { Some = λ(y : Optional a) → y, None = None a } x+ = λ(a : Type) →+ λ(x : Optional (Optional a)) →+ merge { Some = λ(y : Optional a) → y, None = None a } x let example0 = assert : concat Natural (Some (Some 1)) ≡ Some 1
dhall-lang/Prelude/Optional/default view
@@ -3,10 +3,10 @@ -} let default : ∀(a : Type) → a → Optional a → a- = λ(a : Type)- → λ(default : a)- → λ(o : Optional a)- → merge { Some = λ(x : a) → x, None = default } o+ = λ(a : Type) →+ λ(default : a) →+ λ(o : Optional a) →+ merge { Some = λ(x : a) → x, None = default } o let example0 = assert : default Bool False (None Bool) ≡ False
dhall-lang/Prelude/Optional/filter view
@@ -3,23 +3,23 @@ -} let filter : ∀(a : Type) → (a → Bool) → Optional a → Optional a- = λ(a : Type)- → λ(f : a → Bool)- → λ(xs : Optional a)- → ( λ(a : Type)- → λ ( build- : ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional- )- → build (Optional a) (λ(x : a) → Some x) (None a)+ = λ(a : Type) →+ λ(f : a → Bool) →+ λ(xs : Optional a) →+ ( λ(a : Type) →+ λ ( build+ : ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional+ ) →+ build (Optional a) (λ(x : a) → Some x) (None a) ) a- ( λ(optional : Type)- → λ(some : a → optional)- → λ(none : optional)- → merge+ ( λ(optional : Type) →+ λ(some : a → optional) →+ λ(none : optional) →+ merge { Some = λ(x : a) → if f x then some x else none, None = none } xs )
dhall-lang/Prelude/Optional/fold view
@@ -2,18 +2,18 @@ `fold` is the primitive function for consuming `Optional` values -} let fold- : ∀(a : Type)- → Optional a- → ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional- = λ(a : Type)- → λ(o : Optional a)- → λ(optional : Type)- → λ(some : a → optional)- → λ(none : optional)- → merge { Some = some, None = none } o+ : ∀(a : Type) →+ Optional a →+ ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional+ = λ(a : Type) →+ λ(o : Optional a) →+ λ(optional : Type) →+ λ(some : a → optional) →+ λ(none : optional) →+ merge { Some = some, None = none } o let example0 = assert : fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 ≡ 2
dhall-lang/Prelude/Optional/head view
@@ -3,15 +3,15 @@ -} let head : ∀(a : Type) → List (Optional a) → Optional a- = λ(a : Type)- → λ(xs : List (Optional a))- → List/fold+ = λ(a : Type) →+ λ(xs : List (Optional a)) →+ List/fold (Optional a) xs (Optional a)- ( λ(l : Optional a)- → λ(r : Optional a)- → merge { Some = λ(x : a) → Some x, None = r } l+ ( λ(l : Optional a) →+ λ(r : Optional a) →+ merge { Some = λ(x : a) → Some x, None = r } l ) (None a)
dhall-lang/Prelude/Optional/last view
@@ -3,15 +3,15 @@ -} let last : ∀(a : Type) → List (Optional a) → Optional a- = λ(a : Type)- → λ(xs : List (Optional a))- → List/fold+ = λ(a : Type) →+ λ(xs : List (Optional a)) →+ List/fold (Optional a) xs (Optional a)- ( λ(l : Optional a)- → λ(r : Optional a)- → merge { Some = λ(x : a) → Some x, None = l } r+ ( λ(l : Optional a) →+ λ(r : Optional a) →+ merge { Some = λ(x : a) → Some x, None = l } r ) (None a)
dhall-lang/Prelude/Optional/length view
@@ -3,9 +3,9 @@ -} let length : ∀(a : Type) → Optional a → Natural- = λ(a : Type)- → λ(xs : Optional a)- → merge { Some = λ(_ : a) → 1, None = 0 } xs+ = λ(a : Type) →+ λ(xs : Optional a) →+ merge { Some = λ(_ : a) → 1, None = 0 } xs let example0 = assert : length Natural (Some 2) ≡ 1
dhall-lang/Prelude/Optional/map view
@@ -3,11 +3,11 @@ -} let map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b- = λ(a : Type)- → λ(b : Type)- → λ(f : a → b)- → λ(o : Optional a)- → merge { Some = λ(x : a) → Some (f x), None = None b } o+ = λ(a : Type) →+ λ(b : Type) →+ λ(f : a → b) →+ λ(o : Optional a) →+ merge { Some = λ(x : a) → Some (f x), None = None b } o let example0 = assert : map Natural Bool Natural/even (Some 3) ≡ Some False
dhall-lang/Prelude/Optional/null view
@@ -3,9 +3,9 @@ -} let null : ∀(a : Type) → Optional a → Bool- = λ(a : Type)- → λ(xs : Optional a)- → merge { Some = λ(_ : a) → False, None = True } xs+ = λ(a : Type) →+ λ(xs : Optional a) →+ merge { Some = λ(_ : a) → False, None = True } xs let example0 = assert : null Natural (Some 2) ≡ False
dhall-lang/Prelude/Optional/toList view
@@ -3,9 +3,9 @@ -} let toList : ∀(a : Type) → Optional a → List a- = λ(a : Type)- → λ(o : Optional a)- → merge { Some = λ(x : a) → [ x ] : List a, None = [] : List a } o+ = λ(a : Type) →+ λ(o : Optional a) →+ merge { Some = λ(x : a) → [ x ] : List a, None = [] : List a } o let example0 = assert : toList Natural (Some 1) ≡ [ 1 ]
dhall-lang/Prelude/Optional/unzip view
@@ -2,14 +2,14 @@ Unzip an `Optional` value into two separate `Optional` values -} let unzip- : ∀(a : Type)- → ∀(b : Type)- → Optional { _1 : a, _2 : b }- → { _1 : Optional a, _2 : Optional b }- = λ(a : Type)- → λ(b : Type)- → λ(xs : Optional { _1 : a, _2 : b })- → { _1 =+ : ∀(a : Type) →+ ∀(b : Type) →+ Optional { _1 : a, _2 : b } →+ { _1 : Optional a, _2 : Optional b }+ = λ(a : Type) →+ λ(b : Type) →+ λ(xs : Optional { _1 : a, _2 : b }) →+ { _1 = merge { Some = λ(x : { _1 : a, _2 : b }) → Some x._1, None = None a } xs
dhall-lang/Prelude/Text/concat view
@@ -3,8 +3,8 @@ -} let concat : List Text → Text- = λ(xs : List Text)- → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) ""+ = λ(xs : List Text) →+ List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" let example0 = assert : concat [ "ABC", "DEF", "GHI" ] ≡ "ABCDEFGHI"
dhall-lang/Prelude/Text/concatMap view
@@ -3,10 +3,10 @@ -} let concatMap : ∀(a : Type) → (a → Text) → List a → Text- = λ(a : Type)- → λ(f : a → Text)- → λ(xs : List a)- → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) ""+ = λ(a : Type) →+ λ(f : a → Text) →+ λ(xs : List a) →+ List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) "" let example0 = assert
dhall-lang/Prelude/Text/concatMapSep view
@@ -6,22 +6,22 @@ let concatMapSep : ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text- = λ(separator : Text)- → λ(a : Type)- → λ(f : a → Text)- → λ(elements : List a)- → let status =+ = λ(separator : Text) →+ λ(a : Type) →+ λ(f : a → Text) →+ λ(elements : List a) →+ let status = List/fold a elements Status- ( λ(x : a)- → λ(status : Status)- → merge+ ( λ(x : a) →+ λ(status : Status) →+ merge { Empty = Status.NonEmpty (f x) , NonEmpty =- λ(result : Text)- → Status.NonEmpty (f x ++ separator ++ result)+ λ(result : Text) →+ Status.NonEmpty (f x ++ separator ++ result) } status )
dhall-lang/Prelude/Text/concatSep view
@@ -5,20 +5,20 @@ let concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text- = λ(separator : Text)- → λ(elements : List Text)- → let status =+ = λ(separator : Text) →+ λ(elements : List Text) →+ let status = List/fold Text elements Status- ( λ(element : Text)- → λ(status : Status)- → merge+ ( λ(element : Text) →+ λ(status : Status) →+ merge { Empty = Status.NonEmpty element , NonEmpty =- λ(result : Text)- → Status.NonEmpty (element ++ separator ++ result)+ λ(result : Text) →+ Status.NonEmpty (element ++ separator ++ result) } status )
dhall-lang/Prelude/Text/defaultMap view
@@ -3,10 +3,10 @@ -} let defaultMap : ∀(a : Type) → (a → Text) → Optional a → Text- = λ(a : Type)- → λ(f : a → Text)- → λ(o : Optional a)- → merge { Some = f, None = "" } o+ = λ(a : Type) →+ λ(f : a → Text) →+ λ(o : Optional a) →+ merge { Some = f, None = "" } o let example0 = assert : defaultMap Natural Natural/show (Some 0) ≡ "0"
dhall-lang/Prelude/XML/Type view
@@ -46,17 +46,17 @@ let XML/Type : Type- = ∀(XML : Type)- → ∀ ( xml- : { text : Text → XML- , element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- }- )- → XML+ = ∀(XML : Type) →+ ∀ ( xml+ : { text : Text → XML+ , element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ }+ ) →+ XML in XML/Type
dhall-lang/Prelude/XML/element view
@@ -36,19 +36,19 @@ let element : Args → XML- = λ(elem : Args)- → λ(XML : Type)- → λ ( xml- : { text : Text → XML- , element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- }- )- → xml.element+ = λ(elem : Args) →+ λ(XML : Type) →+ λ ( xml+ : { text : Text → XML+ , element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ }+ ) →+ xml.element { attributes = elem.attributes , name = elem.name , content = List/map XML@1 XML (λ(x : XML@1) → x XML xml) elem.content
dhall-lang/Prelude/XML/leaf view
@@ -18,13 +18,11 @@ ? ./element let leaf- : { attributes : List { mapKey : Text, mapValue : Text }, name : Text }- → XML- = λ ( elem- : { attributes : List { mapKey : Text, mapValue : Text }- , name : Text- }- )- → element (elem ⫽ { content = [] : List XML })+ : { attributes : List { mapKey : Text, mapValue : Text }, name : Text } →+ XML+ = λ ( elem+ : { attributes : List { mapKey : Text, mapValue : Text }, name : Text }+ ) →+ element (elem ⫽ { content = [] : List XML }) in leaf
dhall-lang/Prelude/XML/render view
@@ -40,25 +40,22 @@ let render : XML → Text- = λ(x : XML)- → x+ = λ(x : XML) →+ x Text { text = λ(d : Text) → d , element =- λ ( elem- : { attributes : List { mapKey : Text, mapValue : Text }- , content : List Text- , name : Text- }- )- → let attribs = Text/concatMap Attr renderAttr elem.attributes+ λ ( elem+ : { attributes : List { mapKey : Text, mapValue : Text }+ , content : List Text+ , name : Text+ }+ ) →+ let attribs = Text/concatMap Attr renderAttr elem.attributes in "<${elem.name}${attribs}"- ++ ( if Natural/isZero- (List/length Text elem.content)-+ ++ ( if Natural/isZero (List/length Text elem.content) then "/>"- else ">${Text/concat elem.content}</${elem.name}>" ) }
dhall-lang/Prelude/XML/text view
@@ -20,18 +20,18 @@ let text : Text → XML- = λ(d : Text)- → λ(XML : Type)- → λ ( xml- : { text : Text → XML- , element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- }- )- → xml.text d+ = λ(d : Text) →+ λ(XML : Type) →+ λ ( xml+ : { text : Text → XML+ , element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ }+ ) →+ xml.text d in text
dhall-lang/Prelude/package.dhall view
@@ -11,7 +11,7 @@ ./Integer/package.dhall sha256:d1a572ca3a764781496847e4921d7d9a881c18ffcfac6ae28d0e5299066938a0 ? ./Integer/package.dhall , List =- ./List/package.dhall sha256:10b6d87a09a77bfc1fdef554b7e62abb1b1f0a9267776d834f598ab240ef526c+ ./List/package.dhall sha256:547cd881988c6c5e3673ae80491224158e93a4627690db0196cb5efbbf00d2ba ? ./List/package.dhall , Location = ./Location/package.dhall sha256:0eb4e4a60814018009c720f6820aaa13cf9491eb1b09afb7b832039c6ee4d470
+ dhall-lang/tests/import/cache/dhall/12203871180b87ecaba8b53fffb2a8b52d3fce98098fab09a6f759358b9e8042eedc view
binary file changed (absent → 42 bytes)
+ dhall-lang/tests/import/cache/dhall/1220618f785ce8f3930a9144398f576f0a992544b51212bc9108c31b4e670dc6ed21 view
@@ -0,0 +1,1 @@+xevil string from bad cache
− dhall-lang/tests/import/cache/dhall/1220efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd
binary file changed (49 → absent bytes)
dhall-lang/tests/import/success/hashFromCacheA.dhall view
@@ -6,6 +6,6 @@ resolved by its hash. (If you're interested, the value is a fully-αβ-normalized copy of-Prelude/Optional/null at time of test creation)+Prelude/Optional/null) -}-missing sha256:efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd+missing sha256:3871180b87ecaba8b53fffb2a8b52d3fce98098fab09a6f759358b9e8042eedc
dhall-lang/tests/import/success/hashFromCacheB.dhall view
@@ -1,3 +1,3 @@- λ(_ : Type)-→ λ(_ : Optional _)-→ Optional/fold _@1 _ Bool (λ(_ : _@1) → False) True+λ(_ : Type) →+λ(_ : Optional _) →+ merge { None = True, Some = λ(_ : _@1) → False } _
dhall-lang/tests/normalization/success/remoteSystemsA.dhall view
@@ -26,12 +26,11 @@ : Row ) → let host =- Optional/fold- Text- row.user- Text- (λ(user : Text) → "${user}@${row.host}")- row.host+ merge+ { None = row.host+ , Some = λ(user : Text) → "${user}@${row.host}"+ }+ row.user let platforms = Text/concatSep "," row.platforms
dhall-lang/tests/normalization/success/remoteSystemsB.dhall view
@@ -59,12 +59,9 @@ ) → λ(y : Text) → ''- ${Optional/fold- Text- x.user- Text- (λ(user : Text) → "${user}@${x.host}")- x.host} ${merge+ ${merge+ { None = x.host, Some = λ(user : Text) → "${user}@${x.host}" }+ x.user} ${merge { Empty = "", NonEmpty = λ(result : Text) → result } ( List/fold Text
− dhall-lang/tests/normalization/success/simple/optionalBuildA.dhall
@@ -1,32 +0,0 @@-{ 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)- )-, example3 =- λ(a : Type)- → λ(x : a)- → Optional/build- a- ( λ(optional : Type)- → λ(just : a → optional)- → λ(nothing : optional)- → just x- )-}
− dhall-lang/tests/normalization/success/simple/optionalBuildB.dhall
@@ -1,9 +0,0 @@-{ example0 =- Some 1-, example1 =- Some +1-, example2 =- λ(id : ∀(a : Type) → a → a) → id (Optional Bool) (Some True)-, example3 =- λ(a : Type) → λ(x : a) → Some x-}
− dhall-lang/tests/normalization/success/simple/optionalBuildFoldA.dhall
@@ -1,1 +0,0 @@-Optional/build Text (Optional/fold Text (Some "foo"))
− dhall-lang/tests/normalization/success/simple/optionalBuildFoldB.dhall
@@ -1,1 +0,0 @@-Some "foo"
− dhall-lang/tests/normalization/success/simple/optionalFoldA.dhall
@@ -1,7 +0,0 @@- let f =- λ(o : Optional Text)- → Optional/fold Text o Natural (λ(j : Text) → 1) 2--in { example0 = f (Some "foo")- , example1 = f (None Text)- }
− dhall-lang/tests/normalization/success/simple/optionalFoldB.dhall
@@ -1,1 +0,0 @@-{ example0 = 1, example1 = 2 }
− dhall-lang/tests/normalization/success/unit/OptionalBuildA.dhall
@@ -1,1 +0,0 @@-Optional/build
− dhall-lang/tests/normalization/success/unit/OptionalBuildB.dhall
@@ -1,1 +0,0 @@-Optional/build
− dhall-lang/tests/normalization/success/unit/OptionalBuildFoldFusionA.dhall
@@ -1,1 +0,0 @@-λ(T : Type) → λ(x : Optional T) → Optional/build T (Optional/fold T x)
− dhall-lang/tests/normalization/success/unit/OptionalBuildFoldFusionB.dhall
@@ -1,3 +0,0 @@- λ(T : Type)-→ λ(x : Optional T)-→ Optional/fold T x (Optional T) (λ(a : T) → Some a) (None T)
− dhall-lang/tests/normalization/success/unit/OptionalBuildImplementationA.dhall
@@ -1,3 +0,0 @@- λ(T : Type)-→ λ(f : ∀(optional : Type) → (T → optional) → optional → optional)-→ Optional/build T f
− dhall-lang/tests/normalization/success/unit/OptionalBuildImplementationB.dhall
@@ -1,3 +0,0 @@- λ(T : Type)-→ λ(f : ∀(optional : Type) → (T → optional) → optional → optional)-→ f (Optional T) (λ(a : T) → Some a) (None T)
− dhall-lang/tests/normalization/success/unit/OptionalFoldA.dhall
@@ -1,1 +0,0 @@-Optional/fold
− dhall-lang/tests/normalization/success/unit/OptionalFoldB.dhall
@@ -1,1 +0,0 @@-Optional/fold
− dhall-lang/tests/normalization/success/unit/OptionalFoldNoneA.dhall
@@ -1,1 +0,0 @@-λ(T : Type) → λ(x : Bool) → Optional/fold T (None T) Bool (λ(_ : T) → False) x
− dhall-lang/tests/normalization/success/unit/OptionalFoldNoneB.dhall
@@ -1,1 +0,0 @@-λ(T : Type) → λ(x : Bool) → x
− dhall-lang/tests/normalization/success/unit/OptionalFoldSomeA.dhall
@@ -1,4 +0,0 @@- λ(T : Type)-→ λ(x : T)-→ λ(y : Bool)-→ Optional/fold T (Some x) Bool (λ(_ : T) → False) y
− dhall-lang/tests/normalization/success/unit/OptionalFoldSomeB.dhall
@@ -1,1 +0,0 @@-λ(T : Type) → λ(x : T) → λ(y : Bool) → False
+ dhall-lang/tests/parser/failure/unit/UrlWithQuotedPath.dhall view
@@ -0,0 +1,1 @@+https://example.com/"a%20b"/c
dhall-lang/tests/parser/success/builtinsA.dhall view
@@ -1,32 +1,35 @@- λ ( x- : { field0 : Bool- , field1 : Optional (Optional Bool)- , field2 : Natural- , field3 : Integer- , field4 : Double- , field5 : Text- , field6 : List (List Bool)- }- )-→ { field00 = Natural/fold- , field01 = Natural/build- , field02 = Natural/isZero- , field03 = Natural/even- , field04 = Natural/odd- , field05 = Natural/toInteger- , field06 = Natural/show- , field07 = Integer/show- , field08 = Double/show- , field09 = List/build- , field10 = List/fold- , field11 = List/length- , field12 = List/head- , field13 = List/last- , field14 = List/indexed- , field15 = List/reverse- , field16 = Optional/fold- , field17 = Optional/build- , field18 = True- , field19 = False- , field20 = None- }+[ Natural/fold+, Natural/build+, Natural/isZero+, Natural/even+, Natural/odd+, Natural/toInteger+, Natural/show+, Integer/toDouble+, Integer/show+, Integer/negate+, Integer/clamp+, Natural/subtract+, Double/show+, List/build+, List/fold+, List/length+, List/head+, List/last+, List/indexed+, List/reverse+, Text/show+, Bool+, True+, False+, Optional+, None+, Natural+, Integer+, Double+, Text+, List+, Type+, Kind+, Sort+]
dhall-lang/tests/parser/success/builtinsB.dhallb view
binary file changed (544 → 348 bytes)
dhall-lang/tests/parser/success/largeExpressionA.dhall view
@@ -97,12 +97,11 @@ } ) → λ(y : Text)- → Optional/fold- Text- x.user- Text- (λ(user : Text) → user ++ "@" ++ x.host ++ "")- x.host+ → merge+ { None = x.host+ , Some = λ(user : Text) → user ++ "@" ++ x.host ++ ""+ }+ x.user ++ " " ++ ( merge { Empty = "", NonEmpty = λ(result : Text) → result }
dhall-lang/tests/parser/success/largeExpressionB.dhallb view
binary file changed (3518 → 3507 bytes)
dhall-lang/tests/parser/success/quotedLabelA.dhall view
@@ -1,4 +1,5 @@ { example1 = let `let` = 1 in `let` , example2 = let `:.` = 1 in `:.` , example3 = let `$ref` = 1 in `$ref`+, example4 = let `` = 1 in `` }
dhall-lang/tests/parser/success/quotedLabelB.dhallb view
binary file changed (81 → 101 bytes)
+ dhall-lang/tests/parser/success/quotedRecordLabelA.dhall view
@@ -0,0 +1,1 @@+{foo = 1, `` = 2, ` ` = 3}
+ dhall-lang/tests/parser/success/quotedRecordLabelB.dhallb view
@@ -0,0 +1,1 @@+£`a cfoo
+ dhall-lang/tests/parser/success/quotedUnionLabelA.dhall view
@@ -0,0 +1,1 @@+<foo: Natural|``: Natural|` `: Natural>
+ dhall-lang/tests/parser/success/quotedUnionLabelB.dhallb view
@@ -0,0 +1,1 @@+£`gNaturala gNaturalcfoogNatural
dhall-lang/tests/parser/success/unit/import/quotedPathsA.dhall view
@@ -1,3 +1,1 @@-{ example0 = /"foo"/bar/"baz qux"-, example1 = https://example.com/foo/"bar?baz"?qux-}+/"foo"/bar/"baz qux"
dhall-lang/tests/parser/success/unit/import/quotedPathsB.dhallb view
binary file changed (80 → 22 bytes)
− dhall-lang/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeA.dhall
@@ -1,1 +0,0 @@-https://example.com/"a%20b"/c
− dhall-lang/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeB.dhallb
binary file changed (30 → absent bytes)
dhall-lang/tests/semantic-hash/success/remoteSystemsA.dhall view
@@ -26,12 +26,11 @@ : Row ) → let host =- Optional/fold- Text- row.user- Text- (λ(user : Text) → "${user}@${row.host}")- row.host+ merge+ { None = row.host+ , Some = λ(user : Text) → "${user}@${row.host}"+ }+ row.user let platforms = Text/concatSep "," row.platforms
dhall-lang/tests/semantic-hash/success/remoteSystemsB.hash view
@@ -1,1 +1,1 @@-sha256:1591a538ac60355f6f988d01edb3b8622d2631b93177a90ad7172e0f88b67da5+sha256:573b0d8fbc28c09c155cf239963b6ba71941aace25e23806043017f7fe75098b
− dhall-lang/tests/semantic-hash/success/simple/optionalBuildA.dhall
@@ -1,32 +0,0 @@-{ 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)- )-, example3 =- λ(a : Type)- → λ(x : a)- → Optional/build- a- ( λ(optional : Type)- → λ(just : a → optional)- → λ(nothing : optional)- → just x- )-}
− dhall-lang/tests/semantic-hash/success/simple/optionalBuildB.hash
@@ -1,1 +0,0 @@-sha256:57937e066a166baf3d712e744d9aec91894f14d7b25138a6f60c7b7577cc986b
− dhall-lang/tests/semantic-hash/success/simple/optionalBuildFoldA.dhall
@@ -1,1 +0,0 @@-Optional/build Text (Optional/fold Text (Some "foo"))
− dhall-lang/tests/semantic-hash/success/simple/optionalBuildFoldB.hash
@@ -1,1 +0,0 @@-sha256:29dc3b0c8df03521d3bb92d3b7d996a70a5dbca8de8607ffaf9f888a2213e73b
− dhall-lang/tests/semantic-hash/success/simple/optionalFoldA.dhall
@@ -1,7 +0,0 @@- let f =- λ(o : Optional Text)- → Optional/fold Text o Natural (λ(j : Text) → 1) 2--in { example0 = f (Some "foo")- , example1 = f (None Text)- }
− dhall-lang/tests/semantic-hash/success/simple/optionalFoldB.hash
@@ -1,1 +0,0 @@-sha256:225b0c8ffa394c837aebfce636806e3f39511d87331b6ef734311689a2ec8a7e
dhall-lang/tests/type-inference/success/preludeB.dhall view
@@ -13,13 +13,13 @@ , Double : { show : Double → Text } , Function : { compose :- ∀(A : Type)- → ∀(B : Type)- → ∀(C : Type)- → ∀(f : A → B)- → ∀(g : B → C)- → ∀(x : A)- → C+ ∀(A : Type) →+ ∀(B : Type) →+ ∀(C : Type) →+ ∀(f : A → B) →+ ∀(g : B → C) →+ ∀(x : A) →+ C , identity : ∀(a : Type) → ∀(x : a) → a } , Integer :@@ -47,250 +47,248 @@ , Tagged : ∀(a : Type) → Type , Type : Type , array :- ∀ ( x- : List- ( ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object :- List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON- )- )- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀ ( x+ : List+ ( ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON+ )+ ) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , bool :- ∀(x : Bool)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Bool) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , double :- ∀(x : Double)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Double) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , integer :- ∀(x : Integer)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Integer) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , keyText : ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } , keyValue :- ∀(v : Type)- → ∀(key : Text)- → ∀(value : v)- → { mapKey : Text, mapValue : v }+ ∀(v : Type) →+ ∀(key : Text) →+ ∀(value : v) →+ { mapKey : Text, mapValue : v } , natural :- ∀(x : Natural)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Natural) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , null :- ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , number :- ∀(x : Double)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Double) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , object :- ∀ ( x- : List- { mapKey : Text- , mapValue :- ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object :- List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON- }- )- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON+ ∀ ( x+ : List+ { mapKey : Text+ , mapValue :+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON }- )- → JSON+ ) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , omitNullFields :- ∀ ( old- : ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON- )- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀ ( old+ : ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON+ ) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , render :- ∀ ( json- : ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON- )- → Text+ ∀ ( json+ : ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON+ ) →+ Text , renderInteger : ∀(integer : Integer) → Text , renderYAML :- ∀ ( json- : ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON- )- → Text+ ∀ ( json+ : ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON+ ) →+ Text , string :- ∀(x : Text)- → ∀(JSON : Type)- → ∀ ( json- : { array : List JSON → JSON- , bool : Bool → JSON- , double : Double → JSON- , integer : Integer → JSON- , null : JSON- , object : List { mapKey : Text, mapValue : JSON } → JSON- , string : Text → JSON- }- )- → JSON+ ∀(x : Text) →+ ∀(JSON : Type) →+ ∀ ( json+ : { array : List JSON → JSON+ , bool : Bool → JSON+ , double : Double → JSON+ , integer : Integer → JSON+ , null : JSON+ , object : List { mapKey : Text, mapValue : JSON } → JSON+ , string : Text → JSON+ }+ ) →+ JSON , tagInline :- ∀(tagFieldName : Text)- → ∀(a : Type)- → ∀(contents : a)- → { contents : a, field : Text, nesting : < Inline | Nested : Text > }+ ∀(tagFieldName : Text) →+ ∀(a : Type) →+ ∀(contents : a) →+ { contents : a, field : Text, nesting : < Inline | Nested : Text > } , tagNested :- ∀(contentsFieldName : Text)- → ∀(tagFieldName : Text)- → ∀(a : Type)- → ∀(contents : a)- → { contents : a, field : Text, nesting : < Inline | Nested : Text > }+ ∀(contentsFieldName : Text) →+ ∀(tagFieldName : Text) →+ ∀(a : Type) →+ ∀(contents : a) →+ { contents : a, field : Text, nesting : < Inline | Nested : Text > } } , List : { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool , build :- ∀(a : Type)- → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)- → List a+ ∀(a : Type) →+ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →+ List a , concat : ∀(a : Type) → ∀(xss : List (List a)) → List a , concatMap : ∀(a : Type) → ∀(b : Type) → ∀(f : a → List b) → ∀(xs : List a) → List b@@ -299,12 +297,12 @@ , empty : ∀(a : Type) → List a , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a , fold :- ∀(a : Type)- → List a- → ∀(list : Type)- → ∀(cons : a → list → list)- → ∀(nil : list)- → list+ ∀(a : Type) →+ List a →+ ∀(list : Type) →+ ∀(cons : a → list → list) →+ ∀(nil : list) →+ list , generate : ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a , head : ∀(a : Type) → List a → Optional a , index : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → Optional a@@ -315,28 +313,29 @@ , map : ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b , null : ∀(a : Type) → ∀(xs : List a) → Bool , partition :- ∀(a : Type)- → ∀(f : a → Bool)- → ∀(xs : List a)- → { false : List a, true : List a }+ ∀(a : Type) →+ ∀(f : a → Bool) →+ ∀(xs : List a) →+ { false : List a, true : List a } , replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a , reverse : ∀(a : Type) → List a → List a , shifted :- ∀(a : Type)- → ∀(kvss : List (List { index : Natural, value : a }))- → List { index : Natural, value : a }+ ∀(a : Type) →+ ∀(kvss : List (List { index : Natural, value : a })) →+ List { index : Natural, value : a } , take : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → List a+ , unpackOptionals : ∀(a : Type) → ∀(xs : List (Optional a)) → List a , unzip :- ∀(a : Type)- → ∀(b : Type)- → ∀(xs : List { _1 : a, _2 : b })- → { _1 : List a, _2 : List b }+ ∀(a : Type) →+ ∀(b : Type) →+ ∀(xs : List { _1 : a, _2 : b }) →+ { _1 : List a, _2 : List b } , zip :- ∀(a : Type)- → ∀(xa : List a)- → ∀(b : Type)- → ∀(xb : List b)- → List { _1 : a, _2 : b }+ ∀(a : Type) →+ ∀(xs : List a) →+ ∀(b : Type) →+ ∀(ys : List b) →+ List { _1 : a, _2 : b } } , Location : { Type : Type } , Map :@@ -346,46 +345,46 @@ , keyText : ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } , keyValue :- ∀(v : Type)- → ∀(key : Text)- → ∀(value : v)- → { mapKey : Text, mapValue : v }+ ∀(v : Type) →+ ∀(key : Text) →+ ∀(value : v) →+ { mapKey : Text, mapValue : v } , keys :- ∀(k : Type)- → ∀(v : Type)- → ∀(xs : List { mapKey : k, mapValue : v })- → List k+ ∀(k : Type) →+ ∀(v : Type) →+ ∀(xs : List { mapKey : k, mapValue : v }) →+ List k , map :- ∀(k : Type)- → ∀(a : Type)- → ∀(b : Type)- → ∀(f : a → b)- → ∀(m : List { mapKey : k, mapValue : a })- → List { mapKey : k, mapValue : b }+ ∀(k : Type) →+ ∀(a : Type) →+ ∀(b : Type) →+ ∀(f : a → b) →+ ∀(m : List { mapKey : k, mapValue : a }) →+ List { mapKey : k, mapValue : b } , values :- ∀(k : Type)- → ∀(v : Type)- → ∀(xs : List { mapKey : k, mapValue : v })- → List v+ ∀(k : Type) →+ ∀(v : Type) →+ ∀(xs : List { mapKey : k, mapValue : v }) →+ List v } , Monoid : ∀(m : Type) → Type , Natural : { build :- ( ∀(natural : Type)- → ∀(succ : natural → natural)- → ∀(zero : natural)- → natural- )- → Natural+ ( ∀(natural : Type) →+ ∀(succ : natural → natural) →+ ∀(zero : natural) →+ natural+ ) →+ Natural , enumerate : ∀(n : Natural) → List Natural , equal : ∀(a : Natural) → ∀(b : Natural) → Bool , even : Natural → Bool , fold :- Natural- → ∀(natural : Type)- → ∀(succ : natural → natural)- → ∀(zero : natural)- → natural+ Natural →+ ∀(natural : Type) →+ ∀(succ : natural → natural) →+ ∀(zero : natural) →+ natural , greaterThan : ∀(x : Natural) → ∀(y : Natural) → Bool , greaterThanEqual : ∀(x : Natural) → ∀(y : Natural) → Bool , isZero : Natural → Bool@@ -408,50 +407,50 @@ { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool , build :- ∀(a : Type)- → ∀ ( build- : ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional- )- → Optional a+ ∀(a : Type) →+ ∀ ( build+ : ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional+ ) →+ Optional a , concat : ∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a , default : ∀(a : Type) → ∀(default : a) → ∀(o : Optional a) → a , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a , fold :- ∀(a : Type)- → ∀(o : Optional a)- → ∀(optional : Type)- → ∀(some : a → optional)- → ∀(none : optional)- → optional+ ∀(a : Type) →+ ∀(o : Optional a) →+ ∀(optional : Type) →+ ∀(some : a → optional) →+ ∀(none : optional) →+ optional , head : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a , last : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a , length : ∀(a : Type) → ∀(xs : Optional a) → Natural , map :- ∀(a : Type)- → ∀(b : Type)- → ∀(f : a → b)- → ∀(o : Optional a)- → Optional b+ ∀(a : Type) →+ ∀(b : Type) →+ ∀(f : a → b) →+ ∀(o : Optional a) →+ Optional b , null : ∀(a : Type) → ∀(xs : Optional a) → Bool , toList : ∀(a : Type) → ∀(o : Optional a) → List a , unzip :- ∀(a : Type)- → ∀(b : Type)- → ∀(xs : Optional { _1 : a, _2 : b })- → { _1 : Optional a, _2 : Optional b }+ ∀(a : Type) →+ ∀(b : Type) →+ ∀(xs : Optional { _1 : a, _2 : b }) →+ { _1 : Optional a, _2 : Optional b } } , Text : { concat : ∀(xs : List Text) → Text , concatMap : ∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text , concatMapSep :- ∀(separator : Text)- → ∀(a : Type)- → ∀(f : a → Text)- → ∀(elements : List a)- → Text+ ∀(separator : Text) →+ ∀(a : Type) →+ ∀(f : a → Text) →+ ∀(elements : List a) →+ Text , concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text , default : ∀(o : Optional Text) → Text , defaultMap : ∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text@@ -464,87 +463,87 @@ , attribute : ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } , element :- ∀ ( elem- : { attributes : List { mapKey : Text, mapValue : Text }- , content :- List- ( ∀(XML : Type)- → ∀ ( xml- : { element :- { attributes :- List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- , text : Text → XML- }- )- → XML- )- , name : Text- }- )- → ∀(XML : Type)- → ∀ ( xml- : { element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- , text : Text → XML- }- )- → XML+ ∀ ( elem+ : { attributes : List { mapKey : Text, mapValue : Text }+ , content :+ List+ ( ∀(XML : Type) →+ ∀ ( xml+ : { element :+ { attributes :+ List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ , text : Text → XML+ }+ ) →+ XML+ )+ , name : Text+ }+ ) →+ ∀(XML : Type) →+ ∀ ( xml+ : { element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ , text : Text → XML+ }+ ) →+ XML , emptyAttributes : List { mapKey : Text, mapValue : Text } , leaf :- ∀ ( elem- : { attributes : List { mapKey : Text, mapValue : Text }- , name : Text- }- )- → ∀(XML : Type)- → ∀ ( xml- : { element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- , text : Text → XML- }- )- → XML+ ∀ ( elem+ : { attributes : List { mapKey : Text, mapValue : Text }+ , name : Text+ }+ ) →+ ∀(XML : Type) →+ ∀ ( xml+ : { element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ , text : Text → XML+ }+ ) →+ XML , render :- ∀ ( x- : ∀(XML : Type)- → ∀ ( xml- : { element :- { attributes : List { mapKey : Text, mapValue : Text }- , content : List XML- , name : Text- }- → XML- , text : Text → XML- }- )- → XML- )- → Text- , text :- ∀(d : Text)- → ∀(XML : Type)- → ∀ ( xml- : { element :+ ∀ ( x+ : ∀(XML : Type) →+ ∀ ( xml+ : { element : { attributes : List { mapKey : Text, mapValue : Text } , content : List XML , name : Text- }- → XML- , text : Text → XML- }- )- → XML+ } →+ XML+ , text : Text → XML+ }+ ) →+ XML+ ) →+ Text+ , text :+ ∀(d : Text) →+ ∀(XML : Type) →+ ∀ ( xml+ : { element :+ { attributes : List { mapKey : Text, mapValue : Text }+ , content : List XML+ , name : Text+ } →+ XML+ , text : Text → XML+ }+ ) →+ XML } }
− dhall-lang/tests/type-inference/success/unit/OptionalBuildA.dhall
@@ -1,1 +0,0 @@-Optional/build
− dhall-lang/tests/type-inference/success/unit/OptionalBuildB.dhall
@@ -1,7 +0,0 @@- ∀(a : Type)-→ ( ∀(optional : Type)- → ∀(just : a → optional)- → ∀(nothing : optional)- → optional- )-→ Optional a
− dhall-lang/tests/type-inference/success/unit/OptionalFoldA.dhall
@@ -1,1 +0,0 @@-Optional/fold
− dhall-lang/tests/type-inference/success/unit/OptionalFoldB.dhall
@@ -1,6 +0,0 @@- ∀(a : Type)-→ Optional a-→ ∀(optional : Type)-→ ∀(just : a → optional)-→ ∀(nothing : optional)-→ optional
dhall.cabal view
@@ -1,5 +1,5 @@ Name: dhall-Version: 1.32.0+Version: 1.33.0 Cabal-Version: >=1.10 Build-Type: Simple Tested-With: GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.1@@ -110,6 +110,7 @@ dhall-lang/Prelude/List/reverse dhall-lang/Prelude/List/shifted dhall-lang/Prelude/List/take+ dhall-lang/Prelude/List/unpackOptionals dhall-lang/Prelude/List/unzip dhall-lang/Prelude/List/zip dhall-lang/Prelude/Location/Type@@ -188,7 +189,8 @@ dhall-lang/tests/binary-decode/success/unit/*.dhallb dhall-lang/tests/binary-decode/success/unit/imports/*.dhall dhall-lang/tests/binary-decode/success/unit/imports/*.dhallb- dhall-lang/tests/import/cache/dhall/1220efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd+ dhall-lang/tests/import/cache/dhall/12203871180b87ecaba8b53fffb2a8b52d3fce98098fab09a6f759358b9e8042eedc+ dhall-lang/tests/import/cache/dhall/1220618f785ce8f3930a9144398f576f0a992544b51212bc9108c31b4e670dc6ed21 dhall-lang/tests/import/data/*.dhall dhall-lang/tests/import/data/*.txt dhall-lang/tests/import/failure/*.dhall@@ -447,7 +449,7 @@ Hs-Source-Dirs: src Build-Depends: base >= 4.9.1.0 && < 5 ,- aeson >= 1.0.0.0 && < 1.5 ,+ aeson >= 1.0.0.0 && < 1.6 , aeson-pretty < 0.9 , ansi-terminal >= 0.6.3.1 && < 0.11, atomic-write >= 0.2.0.7 && < 0.3 ,@@ -511,7 +513,7 @@ if flag(with-http) Build-Depends: http-types >= 0.7.0 && < 0.13,- http-client >= 0.4.30 && < 0.7 ,+ http-client >= 0.4.30 && < 0.8 , http-client-tls >= 0.2.0 && < 0.4 Other-Extensions:@@ -648,7 +650,7 @@ serialise , special-values < 0.2 , spoon < 0.4 ,- tasty >= 0.11.2 && < 1.3 ,+ tasty >= 0.11.2 && < 1.4 , tasty-expected-failure < 0.12, tasty-hunit >= 0.10 && < 0.11, tasty-quickcheck >= 0.9.2 && < 0.11,@@ -673,13 +675,8 @@ directory , filepath < 1.5 , mockery < 0.4 ,- doctest >= 0.7.0 && < 0.17+ doctest >= 0.7.0 && < 0.18 Default-Language: Haskell2010- -- `doctest` doesn't work with `MIN_VERSION` macros before GHC 8- --- -- See: https://ghc.haskell.org/trac/ghc/ticket/10970- if impl(ghc < 8.0)- Buildable: False Benchmark dhall-parser Type: exitcode-stdio-1.0
src/Dhall.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ApplicativeDo #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveFunctor #-}@@ -5,6 +6,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-}@@ -50,7 +52,7 @@ , FromDhall(..) , Interpret , InvalidDecoder(..)- , ExtractErrors(..)+ , ExtractErrors , ExtractError(..) , Extractor , MonadicExtractor@@ -58,6 +60,9 @@ , extractError , toMonadic , fromMonadic+ , ExpectedTypeErrors+ , ExpectedTypeError(..)+ , Expector , auto , genericAuto , genericAutoWith@@ -95,7 +100,6 @@ , union , constructor , GenericFromDhall(..)- , GenericToDhall(..) , ToDhall(..) , Inject@@ -111,8 +115,11 @@ , encodeConstructor , unionEncoder , (>|<)+ , GenericToDhall(..) -- * Miscellaneous+ , DhallErrors(..)+ , showDhallErrors , rawInput , (>$<) , (>*<)@@ -144,7 +151,7 @@ import Data.Sequence (Seq) import Data.Text (Text) import Data.Text.Prettyprint.Doc (Pretty)-import Data.Typeable (Typeable)+import Data.Typeable (Typeable, Proxy(..)) import Data.Vector (Vector) import Data.Void (Void) import Data.Word (Word8, Word16, Word32, Word64)@@ -196,6 +203,24 @@ -- >>> import Data.Word (Word8, Word16, Word32, Word64) -- >>> import Dhall.Pretty.Internal (prettyExpr) +{-| A newtype suitable for collecting one or more errors+-}+newtype DhallErrors e = DhallErrors+ { getErrors :: NonEmpty e+ } deriving (Eq, Functor, Semigroup)++instance (Show (DhallErrors e), Typeable e) => Exception (DhallErrors e)++{-| Render a given prefix and some errors to a string.+-}+showDhallErrors :: Show e => String -> DhallErrors e -> String+showDhallErrors _ (DhallErrors (e :| [])) = show e+showDhallErrors ctx (DhallErrors es) = prefix <> (unlines . Data.List.NonEmpty.toList . fmap show $ es)+ where+ prefix =+ "Multiple errors were encountered" ++ ctx ++ ": \n\+ \ \n"+ {-| Useful synonym for the `Validation` type used when marshalling Dhall expressions -}@@ -207,16 +232,38 @@ type MonadicExtractor s a = Either (ExtractErrors s a) {-| Generate a type error during extraction by specifying the expected type- and the actual type+ and the actual type.+ The expected type is not yet determined. -}-typeError :: Expr s a -> Expr s a -> Extractor s a b-typeError expected actual =- Failure . ExtractErrors . pure . TypeMismatch $ InvalidDecoder expected actual+typeError :: Expector (Expr s a) -> Expr s a -> Extractor s a b+typeError expected actual = Failure $ case expected of+ Failure e -> fmap ExpectedTypeError e+ Success expected' -> DhallErrors $ pure $ TypeMismatch $ InvalidDecoder expected' actual -- | Turn a `Text` message into an extraction failure extractError :: Text -> Extractor s a b-extractError = Failure . ExtractErrors . pure . ExtractError+extractError = Failure . DhallErrors . pure . ExtractError +{-| Useful synonym for the `Validation` type used when marshalling Dhall+ expressions+-}+type Expector = Validation ExpectedTypeErrors++{-| One or more errors returned when determining the Dhall type of a+ Haskell expression+-}+type ExpectedTypeErrors = DhallErrors ExpectedTypeError++{-| Error type used when determining the Dhall type of a Haskell expression+-}+data ExpectedTypeError = RecursiveTypeError+ deriving (Eq, Show)++instance Exception ExpectedTypeError++instance Show ExpectedTypeErrors where+ show = showDhallErrors " while determining the expected type"+ -- | Switches from an @Applicative@ extraction result, able to accumulate errors, -- to a @Monad@ extraction result, able to chain sequential operations toMonadic :: Extractor s a b -> MonadicExtractor s a b@@ -230,19 +277,10 @@ {-| One or more errors returned from extracting a Dhall expression to a Haskell expression -}-newtype ExtractErrors s a = ExtractErrors- { getErrors :: NonEmpty (ExtractError s a)- } deriving Semigroup+type ExtractErrors s a = DhallErrors (ExtractError s a) instance (Pretty s, Pretty a, Typeable s, Typeable a) => Show (ExtractErrors s a) where- show (ExtractErrors (e :| [])) = show e- show (ExtractErrors es) = prefix <> (unlines . Data.List.NonEmpty.toList . fmap show $ es)- where- prefix =- "Multiple errors were encountered during extraction: \n\- \ \n"--instance (Pretty s, Pretty a, Typeable s, Typeable a) => Exception (ExtractErrors s a)+ show = showDhallErrors " during extraction" {-| Extraction of a value can fail for two reasons, either a type mismatch (which should not happen, as expressions are type-checked against the expected type before being passed to @extract@), or@@ -250,11 +288,13 @@ -} data ExtractError s a = TypeMismatch (InvalidDecoder s a)+ | ExpectedTypeError ExpectedTypeError | ExtractError Text instance (Pretty s, Pretty a, Typeable s, Typeable a) => Show (ExtractError s a) where- show (TypeMismatch e) = show e- show (ExtractError es) =+ show (TypeMismatch e) = show e+ show (ExpectedTypeError e) = show e+ show (ExtractError es) = _ERROR <> ": Failed extraction \n\ \ \n\ \The expression type-checked successfully but the transformation to the target \n\@@ -450,14 +490,18 @@ -> IO a -- ^ The decoded value in Haskell inputWithSettings settings (Decoder {..}) txt = do- let suffix = Dhall.Pretty.Internal.prettyToStrictText expected+ expected' <- case expected of+ Success x -> return x+ Failure e -> Control.Exception.throwIO e++ let suffix = Dhall.Pretty.Internal.prettyToStrictText expected' let annotate substituted = case substituted of Note (Src begin end bytes) _ ->- Note (Src begin end bytes') (Annot substituted expected)+ Note (Src begin end bytes') (Annot substituted expected') where bytes' = bytes <> " : " <> suffix _ ->- Annot substituted expected+ Annot substituted expected' normExpr <- inputHelper annotate settings txt @@ -717,7 +761,7 @@ data Decoder a = Decoder { extract :: Expr Src Void -> Extractor Src Void a -- ^ Extracts Haskell value from the Dhall expression- , expected :: Expr Src Void+ , expected :: Expector (Expr Src Void) -- ^ Dhall type of the Haskell value } deriving (Functor)@@ -733,7 +777,7 @@ extract (BoolLit b) = pure b extract expr = typeError expected expr - expected = Bool+ expected = pure Bool {-| Decode a `Natural` @@ -744,9 +788,9 @@ natural = Decoder {..} where extract (NaturalLit n) = pure n- extract expr = typeError Natural expr+ extract expr = typeError expected expr - expected = Natural+ expected = pure Natural {-| Decode an `Integer` @@ -757,9 +801,9 @@ integer = Decoder {..} where extract (IntegerLit n) = pure n- extract expr = typeError Integer expr+ extract expr = typeError expected expr - expected = Integer+ expected = pure Integer {-| Decode a `Scientific` @@ -778,9 +822,9 @@ double = Decoder {..} where extract (DoubleLit (DhallDouble n)) = pure n- extract expr = typeError Double expr+ extract expr = typeError expected expr - expected = Double+ expected = pure Double {-| Decode lazy `Text` @@ -799,9 +843,10 @@ strictText = Decoder {..} where extract (TextLit (Chunks [] t)) = pure t- extract expr = typeError Text expr+ extract expr = typeError expected expr - expected = Text+ expected = pure Text+ {-| Decode a `Maybe` >>> input (maybe natural) "Some 1"@@ -814,7 +859,7 @@ extractOut (App None _) = pure Nothing extractOut expr = typeError expectedOut expr - expectedOut = App Optional expectedIn+ expectedOut = App Optional <$> expectedIn {-| Decode a `Seq` @@ -827,7 +872,7 @@ extractOut (ListLit _ es) = traverse extractIn es extractOut expr = typeError expectedOut expr - expectedOut = App List expectedIn+ expectedOut = App List <$> expectedIn {-| Decode a list @@ -881,7 +926,7 @@ Success o -> o Failure _e -> error "FromDhall: You cannot decode a function if it does not have the correct type" ) - expectedOut = Pi "_" declared expectedIn+ expectedOut = Pi "_" declared <$> expectedIn {-| Decode a `Set` from a `List` @@ -1001,7 +1046,7 @@ Failure f -> Failure f extractOut expr = typeError expectedOut expr - expectedOut = App List expectedIn+ expectedOut = App List <$> expectedIn {-| Decode a `Map` from a @toMap@ expression or generally a @Prelude.Map.Type@ @@ -1051,7 +1096,10 @@ = liftA2 (,) (extract k key) (extract v value) extractOut expr = typeError expectedOut expr - expectedOut = Record (Dhall.Map.fromList [("mapKey", expected k), ("mapValue", expected v)])+ expectedOut = do+ k' <- expected k+ v' <- expected v+ pure $ Record $ Dhall.Map.fromList [("mapKey", k'), ("mapValue", v')] {-| Decode @()@ from an empty record. @@ -1059,13 +1107,13 @@ -} unit :: Decoder ()-unit = Decoder extractOut expectedOut+unit = Decoder {..} where- extractOut (RecordLit fields)+ extract (RecordLit fields) | Data.Foldable.null fields = pure ()- extractOut expr = typeError (Record mempty) expr+ extract expr = typeError expected expr - expectedOut = Record mempty+ expected = pure $ Record mempty {-| Decode 'Void' from an empty union. @@ -1092,17 +1140,14 @@ pair l r = Decoder extractOut expectedOut where extractOut expr@(RecordLit fields) =- (,) <$> ( Data.Maybe.maybe (typeError expectedOut expr) (extract l) $ Dhall.Map.lookup "_1" fields)- <*> ( Data.Maybe.maybe (typeError expectedOut expr) (extract r) $ Dhall.Map.lookup "_2" fields)+ (,) <$> Data.Maybe.maybe (typeError expectedOut expr) (extract l) (Dhall.Map.lookup "_1" fields)+ <*> Data.Maybe.maybe (typeError expectedOut expr) (extract r) (Dhall.Map.lookup "_2" fields) extractOut expr = typeError expectedOut expr - expectedOut =- Record- (Dhall.Map.fromList- [ ("_1", expected l)- , ("_2", expected r)- ]- )+ expectedOut = do+ l' <- expected l+ r' <- expected r+ pure $ Record $ Dhall.Map.fromList [("_1", l'), ("_2", r')] {-| Any value that implements `FromDhall` can be automatically decoded based on the inferred return type of `input`@@ -1124,7 +1169,7 @@ class FromDhall a where autoWith :: InputNormalizer -> Decoder a default autoWith- :: (Generic a, GenericFromDhall (Rep a)) => InputNormalizer -> Decoder a+ :: (Generic a, GenericFromDhall a (Rep a)) => InputNormalizer -> Decoder a autoWith _ = genericAuto {-| A compatibility alias for `FromDhall`@@ -1216,14 +1261,13 @@ resultToFix (Result x) = Fix (fmap resultToFix x) instance FromDhall (f (Result f)) => FromDhall (Result f) where- autoWith inputNormalizer = Decoder { expected = expected_, extract = extract_ }+ autoWith inputNormalizer = Decoder {..} where- expected_ = "result"+ extract (App _ expr) =+ fmap Result (Dhall.extract (autoWith inputNormalizer) expr)+ extract expr = typeError expected expr - extract_ (App _ expression) = do- fmap Result (extract (autoWith inputNormalizer) expression)- extract_ expression = do- typeError expression expected_+ expected = pure "result" -- | You can use this instance to marshal recursive types from Dhall to Haskell. --@@ -1300,42 +1344,42 @@ -- > -- > print (convert x :: Expr) instance (Functor f, FromDhall (f (Result f))) => FromDhall (Fix f) where- autoWith inputNormalizer = Decoder { expected = expected_, extract = extract_ }+ autoWith inputNormalizer = Decoder {..} where- expected_ =- Pi "result" (Const Dhall.Core.Type)- (Pi "Make" (Pi "_" (expected (autoWith inputNormalizer :: Decoder (f (Result f)))) "result")- "result"- )-- extract_ expression0 = extract0 expression0+ extract expr0 = extract0 expr0 where- die = typeError expected_ expression0+ die = typeError expected expr0 - extract0 (Lam x _ expression) = extract1 (rename x "result" expression)- extract0 _ = die+ extract0 (Lam x _ expr) = extract1 (rename x "result" expr)+ extract0 _ = die - extract1 (Lam y _ expression) = extract2 (rename y "Make" expression)- extract1 _ = die+ extract1 (Lam y _ expr) = extract2 (rename y "Make" expr)+ extract1 _ = die - extract2 expression = fmap resultToFix (extract (autoWith inputNormalizer) expression)+ extract2 expr = fmap resultToFix (Dhall.extract (autoWith inputNormalizer) expr) - rename a b expression- | a /= b = Dhall.Core.subst (V a 0) (Var (V b 0)) (Dhall.Core.shift 1 (V b 0) expression)- | otherwise = expression+ rename a b expr+ | a /= b = Dhall.Core.subst (V a 0) (Var (V b 0)) (Dhall.Core.shift 1 (V b 0) expr)+ | otherwise = expr + expected = (\x -> Pi "result" (Const Dhall.Core.Type) (Pi "Make" (Pi "_" x "result") "result"))+ <$> Dhall.expected (autoWith inputNormalizer :: Decoder (f (Result f)))+ {-| `genericAuto` is the default implementation for `auto` if you derive `FromDhall`. The difference is that you can use `genericAuto` without having to explicitly provide a `FromDhall` instance for a type as long as the type derives `Generic` -}-genericAuto :: (Generic a, GenericFromDhall (Rep a)) => Decoder a+genericAuto :: (Generic a, GenericFromDhall a (Rep a)) => Decoder a genericAuto = genericAutoWith defaultInterpretOptions {-| `genericAutoWith` is a configurable version of `genericAuto`. -}-genericAutoWith :: (Generic a, GenericFromDhall (Rep a)) => InterpretOptions -> Decoder a-genericAutoWith options = fmap to (evalState (genericAutoWithNormalizer defaultInputNormalizer options) 1)+genericAutoWith :: (Generic a, GenericFromDhall a (Rep a)) => InterpretOptions -> Decoder a+genericAutoWith options = withProxy (\p -> fmap to (evalState (genericAutoWithNormalizer p defaultInputNormalizer options) 1))+ where+ withProxy :: (Proxy a -> Decoder a) -> Decoder a+ withProxy f = f Proxy {-| Use these options to tweak how Dhall derives a generic implementation of@@ -1406,20 +1450,20 @@ {-| This is the underlying class that powers the `FromDhall` class's support for automatically deriving a generic implementation -}-class GenericFromDhall f where- genericAutoWithNormalizer :: InputNormalizer -> InterpretOptions -> State Int (Decoder (f a))+class GenericFromDhall t f where+ genericAutoWithNormalizer :: Proxy t -> InputNormalizer -> InterpretOptions -> State Int (Decoder (f a)) -instance GenericFromDhall f => GenericFromDhall (M1 D d f) where- genericAutoWithNormalizer inputNormalizer options = do- res <- genericAutoWithNormalizer inputNormalizer options+instance GenericFromDhall t f => GenericFromDhall t (M1 D d f) where+ genericAutoWithNormalizer p inputNormalizer options = do+ res <- genericAutoWithNormalizer p inputNormalizer options pure (fmap M1 res) -instance GenericFromDhall V1 where- genericAutoWithNormalizer _ _ = pure Decoder {..}+instance GenericFromDhall t V1 where+ genericAutoWithNormalizer _ _ _ = pure Decoder {..} where extract expr = typeError expected expr - expected = Union mempty+ expected = pure $ Union mempty unsafeExpectUnion :: Text -> Expr Src Void -> Dhall.Map.Map Text (Maybe (Expr Src Void))@@ -1475,40 +1519,42 @@ extractUnionConstructor _ = empty -class GenericFromDhallUnion f where- genericUnionAutoWithNormalizer :: InputNormalizer -> InterpretOptions -> UnionDecoder (f a)+class GenericFromDhallUnion t f where+ genericUnionAutoWithNormalizer :: Proxy t -> InputNormalizer -> InterpretOptions -> UnionDecoder (f a) -instance (GenericFromDhallUnion f1, GenericFromDhallUnion f2) => GenericFromDhallUnion (f1 :+: f2) where- genericUnionAutoWithNormalizer inputNormalizer options =+instance (GenericFromDhallUnion t f1, GenericFromDhallUnion t f2) => GenericFromDhallUnion t (f1 :+: f2) where+ genericUnionAutoWithNormalizer p inputNormalizer options = (<>)- (L1 <$> genericUnionAutoWithNormalizer inputNormalizer options)- (R1 <$> genericUnionAutoWithNormalizer inputNormalizer options)+ (L1 <$> genericUnionAutoWithNormalizer p inputNormalizer options)+ (R1 <$> genericUnionAutoWithNormalizer p inputNormalizer options) -instance (Constructor c1, GenericFromDhall f1) => GenericFromDhallUnion (M1 C c1 f1) where- genericUnionAutoWithNormalizer inputNormalizer options@(InterpretOptions {..}) =- constructor name (evalState (genericAutoWithNormalizer inputNormalizer options) 1)+instance (Constructor c1, GenericFromDhall t f1) => GenericFromDhallUnion t (M1 C c1 f1) where+ genericUnionAutoWithNormalizer p inputNormalizer options@(InterpretOptions {..}) =+ constructor name (evalState (genericAutoWithNormalizer p inputNormalizer options) 1) where n :: M1 C c1 f1 a n = undefined name = constructorModifier (Data.Text.pack (conName n)) -instance GenericFromDhallUnion (f :+: g) => GenericFromDhall (f :+: g) where- genericAutoWithNormalizer inputNormalizer options =- pure (union (genericUnionAutoWithNormalizer inputNormalizer options))+instance GenericFromDhallUnion t (f :+: g) => GenericFromDhall t (f :+: g) where+ genericAutoWithNormalizer p inputNormalizer options =+ pure (union (genericUnionAutoWithNormalizer p inputNormalizer options)) -instance GenericFromDhall f => GenericFromDhall (M1 C c f) where- genericAutoWithNormalizer inputNormalizer options = do- res <- genericAutoWithNormalizer inputNormalizer options+instance GenericFromDhall t f => GenericFromDhall t (M1 C c f) where+ genericAutoWithNormalizer p inputNormalizer options = do+ res <- genericAutoWithNormalizer p inputNormalizer options pure (fmap M1 res) -instance GenericFromDhall U1 where- genericAutoWithNormalizer _ _ = pure (Decoder {..})+instance GenericFromDhall t U1 where+ genericAutoWithNormalizer _ _ _ = pure (Decoder {..}) where extract _ = pure U1 - expected = Record (Dhall.Map.fromList [])+ expected = pure expected' + expected' = Record (Dhall.Map.fromList [])+ getSelName :: Selector s => M1 i s f a -> State Int Text getSelName n = case selName n of "" -> do i <- get@@ -1516,35 +1562,35 @@ pure (Data.Text.pack ("_" ++ show i)) nn -> pure (Data.Text.pack nn) -instance (GenericFromDhall (f :*: g), GenericFromDhall (h :*: i)) => GenericFromDhall ((f :*: g) :*: (h :*: i)) where- genericAutoWithNormalizer inputNormalizer options = do- Decoder extractL expectedL <- genericAutoWithNormalizer inputNormalizer options- Decoder extractR expectedR <- genericAutoWithNormalizer inputNormalizer options+instance (GenericFromDhall t (f :*: g), GenericFromDhall t (h :*: i)) => GenericFromDhall t ((f :*: g) :*: (h :*: i)) where+ genericAutoWithNormalizer p inputNormalizer options = do+ Decoder extractL expectedL <- genericAutoWithNormalizer p inputNormalizer options+ Decoder extractR expectedR <- genericAutoWithNormalizer p inputNormalizer options - let ktsL = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" expectedL- let ktsR = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" expectedR+ let ktsL = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" <$> expectedL+ let ktsR = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" <$> expectedR - let expected = Record (Dhall.Map.union ktsL ktsR)+ let expected = Record <$> (Dhall.Map.union <$> ktsL <*> ktsR) let extract expression = liftA2 (:*:) (extractL expression) (extractR expression) return (Decoder {..}) -instance (GenericFromDhall (f :*: g), Selector s, FromDhall a) => GenericFromDhall ((f :*: g) :*: M1 S s (K1 i a)) where- genericAutoWithNormalizer inputNormalizer options@InterpretOptions{..} = do+instance (GenericFromDhall t (f :*: g), Selector s, FromDhall a) => GenericFromDhall t ((f :*: g) :*: M1 S s (K1 i a)) where+ genericAutoWithNormalizer p inputNormalizer options@InterpretOptions{..} = do let nR :: M1 S s (K1 i a) r nR = undefined nameR <- fmap fieldModifier (getSelName nR) - Decoder extractL expectedL <- genericAutoWithNormalizer inputNormalizer options+ Decoder extractL expectedL <- genericAutoWithNormalizer p inputNormalizer options let Decoder extractR expectedR = autoWith inputNormalizer - let ktsL = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" expectedL+ let ktsL = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" <$> expectedL - let expected = Record (Dhall.Map.insert nameR expectedR ktsL)+ let expected = Record <$> (Dhall.Map.insert nameR <$> expectedR <*> ktsL) let extract expression = do let die = typeError expected expression@@ -1561,8 +1607,8 @@ return (Decoder {..}) -instance (Selector s, FromDhall a, GenericFromDhall (f :*: g)) => GenericFromDhall (M1 S s (K1 i a) :*: (f :*: g)) where- genericAutoWithNormalizer inputNormalizer options@InterpretOptions{..} = do+instance (Selector s, FromDhall a, GenericFromDhall t (f :*: g)) => GenericFromDhall t (M1 S s (K1 i a) :*: (f :*: g)) where+ genericAutoWithNormalizer p inputNormalizer options@InterpretOptions{..} = do let nL :: M1 S s (K1 i a) r nL = undefined @@ -1570,11 +1616,11 @@ let Decoder extractL expectedL = autoWith inputNormalizer - Decoder extractR expectedR <- genericAutoWithNormalizer inputNormalizer options+ Decoder extractR expectedR <- genericAutoWithNormalizer p inputNormalizer options - let ktsR = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" expectedR+ let ktsR = unsafeExpectRecord "genericAutoWithNormalizer (:*:)" <$> expectedR - let expected = Record (Dhall.Map.insert nameL expectedL ktsR)+ let expected = Record <$> (Dhall.Map.insert nameL <$> expectedL <*> ktsR) let extract expression = do let die = typeError expected expression@@ -1591,8 +1637,20 @@ return (Decoder {..}) -instance (Selector s1, Selector s2, FromDhall a1, FromDhall a2) => GenericFromDhall (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where- genericAutoWithNormalizer inputNormalizer InterpretOptions{..} = do+instance {-# OVERLAPPING #-} GenericFromDhall a1 (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where+ genericAutoWithNormalizer _ _ _ = pure $ Decoder+ { extract = \_ -> Failure $ DhallErrors $ pure $ ExpectedTypeError RecursiveTypeError+ , expected = Failure $ DhallErrors $ pure RecursiveTypeError+ }++instance {-# OVERLAPPING #-} GenericFromDhall a2 (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where+ genericAutoWithNormalizer _ _ _ = pure $ Decoder+ { extract = \_ -> Failure $ DhallErrors $ pure $ ExpectedTypeError RecursiveTypeError+ , expected = Failure $ DhallErrors $ pure RecursiveTypeError+ }++instance {-# OVERLAPPABLE #-} (Selector s1, Selector s2, FromDhall a1, FromDhall a2) => GenericFromDhall t (M1 S s1 (K1 i1 a1) :*: M1 S s2 (K1 i2 a2)) where+ genericAutoWithNormalizer _ inputNormalizer InterpretOptions{..} = do let nL :: M1 S s1 (K1 i1 a1) r nL = undefined @@ -1605,11 +1663,13 @@ let Decoder extractL expectedL = autoWith inputNormalizer let Decoder extractR expectedR = autoWith inputNormalizer - let expected =- Record+ let expected = do+ l <- expectedL+ r <- expectedR+ pure $ Record (Dhall.Map.fromList- [ (nameL, expectedL)- , (nameR, expectedR)+ [ (nameL, l)+ , (nameR, r) ] ) @@ -1628,8 +1688,14 @@ return (Decoder {..}) -instance (Selector s, FromDhall a) => GenericFromDhall (M1 S s (K1 i a)) where- genericAutoWithNormalizer inputNormalizer InterpretOptions{..} = do+instance {-# OVERLAPPING #-} GenericFromDhall a (M1 S s (K1 i a)) where+ genericAutoWithNormalizer _ _ _ = pure $ Decoder+ { extract = \_ -> Failure $ DhallErrors $ pure $ ExpectedTypeError RecursiveTypeError+ , expected = Failure $ DhallErrors $ pure RecursiveTypeError+ }++instance {-# OVERLAPPABLE #-} (Selector s, FromDhall a) => GenericFromDhall t (M1 S s (K1 i a)) where+ genericAutoWithNormalizer _ inputNormalizer InterpretOptions{..} = do let n :: M1 S s (K1 i a) r n = undefined @@ -1644,7 +1710,7 @@ Smart | selName n == "" -> expected' _ ->- Record (Dhall.Map.singleton name expected')+ Record . Dhall.Map.singleton name <$> expected' let extract0 expression = fmap (M1 . K1) (extract' expression) @@ -1661,7 +1727,6 @@ _ -> do die - let extract = case singletonConstructors of Bare -> extract0@@ -2303,14 +2368,9 @@ RecordDecoder ( Data.Functor.Product.Product ( Control.Applicative.Const- ( Dhall.Map.Map- Text- ( Expr Src Void )- )+ (Dhall.Map.Map Text (Expector (Expr Src Void))) )- ( Data.Functor.Compose.Compose- ( (->) ( Expr Src Void ) )- (Extractor Src Void)+ ( Data.Functor.Compose.Compose ((->) (Expr Src Void)) (Extractor Src Void) ) a )@@ -2319,34 +2379,26 @@ -- | Run a 'RecordDecoder' to build a 'Decoder'. record :: RecordDecoder a -> Dhall.Decoder a-record ( RecordDecoder ( Data.Functor.Product.Pair ( Control.Applicative.Const fields ) ( Data.Functor.Compose.Compose extractF ) ) ) =- Decoder- { extract =- extractF- , expected =- Record fields- }+record ( RecordDecoder ( Data.Functor.Product.Pair ( Control.Applicative.Const fields ) ( Data.Functor.Compose.Compose extract ) ) ) = Decoder {..}+ where+ expected = Record <$> traverse id fields -- | Parse a single field of a record. field :: Text -> Decoder a -> RecordDecoder a-field key valueDecoder@(Decoder extract expected) =- let+field key (Decoder {..}) =+ RecordDecoder+ ( Data.Functor.Product.Pair+ ( Control.Applicative.Const+ (Dhall.Map.singleton key expected)+ )+ ( Data.Functor.Compose.Compose extractBody )+ )+ where extractBody expr@(RecordLit fields) = case Dhall.Map.lookup key fields of Just v -> extract v- _ -> typeError expected expr+ _ -> typeError expected expr extractBody expr = typeError expected expr- in- RecordDecoder- ( Data.Functor.Product.Pair- ( Control.Applicative.Const- ( Dhall.Map.singleton- key- ( Dhall.expected valueDecoder )- )- )- ( Data.Functor.Compose.Compose extractBody )- ) {-| The 'UnionDecoder' monoid allows you to build a 'Decoder' from a Dhall union @@ -2394,23 +2446,25 @@ -- | Run a 'UnionDecoder' to build a 'Decoder'. union :: UnionDecoder a -> Decoder a-union (UnionDecoder (Data.Functor.Compose.Compose mp)) = Decoder- { extract = extractF- , expected = Union expect- }+union (UnionDecoder (Data.Functor.Compose.Compose mp)) = Decoder {..} where- expect = (notEmptyRecord . Dhall.expected) <$> mp+ extract expr = case expected' of+ Failure e -> Failure $ fmap ExpectedTypeError e+ Success x -> extract' expr x - extractF e0 =- let result = do- (fld, e1, rest) <- extractUnionConstructor e0+ extract' e0 mp' = Data.Maybe.maybe (typeError expected e0) (uncurry Dhall.extract) $ do+ (fld, e1, rest) <- extractUnionConstructor e0 - t <- Dhall.Map.lookup fld mp+ t <- Dhall.Map.lookup fld mp - guard $ Dhall.Core.Union rest `Dhall.Core.judgmentallyEqual`- Dhall.Core.Union (Dhall.Map.delete fld expect)- pure (t, e1)- in Data.Maybe.maybe (typeError (Union expect) e0) (uncurry extract) result+ guard $+ Dhall.Core.Union rest `Dhall.Core.judgmentallyEqual` Dhall.Core.Union (Dhall.Map.delete fld mp')++ pure (t, e1)++ expected = Union <$> expected'++ expected' = traverse (fmap notEmptyRecord . Dhall.expected) mp -- | Parse a single constructor of a union constructor :: Text -> Decoder a -> UnionDecoder a
src/Dhall/Binary.hs view
@@ -50,23 +50,23 @@ , Var(..) ) -import Data.Foldable (toList, foldl')+import Data.Foldable (toList) import Data.Monoid ((<>)) import Data.Text (Text) import Data.Void (Void, absurd) import GHC.Float (double2Float, float2Double) import Numeric.Half (fromHalf, toHalf) +import qualified Codec.CBOR.ByteArray import qualified Codec.CBOR.Decoding as Decoding import qualified Codec.CBOR.Encoding as Encoding import qualified Codec.CBOR.Read as Read import qualified Codec.Serialise as Serialise-import qualified Control.Monad as Monad import qualified Data.ByteArray import qualified Data.ByteString import qualified Data.ByteString.Lazy+import qualified Data.ByteString.Short import qualified Data.Sequence-import qualified Data.Text as Text import qualified Dhall.Crypto import qualified Dhall.Map import qualified Dhall.Set@@ -128,24 +128,24 @@ case tokenType₀ of TypeUInt -> do- !n <- Decoding.decodeWord+ !n <- fromIntegral <$> Decoding.decodeWord - return (Var (V "_" (fromIntegral n)))+ return (Var (V "_" n)) TypeUInt64 -> do- !n <- Decoding.decodeWord64+ !n <- fromIntegral <$> Decoding.decodeWord64 - return (Var (V "_" (fromIntegral n)))+ return (Var (V "_" n)) TypeFloat16 -> do- !n <- Decoding.decodeFloat+ !n <- float2Double <$> Decoding.decodeFloat - return (DoubleLit (DhallDouble (float2Double n)))+ return (DoubleLit (DhallDouble n)) TypeFloat32 -> do- !n <- Decoding.decodeFloat+ !n <- float2Double <$> Decoding.decodeFloat - return (DoubleLit (DhallDouble (float2Double n)))+ return (DoubleLit (DhallDouble n)) TypeFloat64 -> do !n <- Decoding.decodeDouble@@ -158,45 +158,45 @@ return (BoolLit b) TypeString -> do- s <- Decoding.decodeString+ !ba <- Decoding.decodeUtf8ByteArray - case s of- "Natural/build" -> return NaturalBuild- "Natural/fold" -> return NaturalFold- "Natural/isZero" -> return NaturalIsZero- "Natural/even" -> return NaturalEven- "Natural/odd" -> return NaturalOdd- "Natural/toInteger" -> return NaturalToInteger- "Natural/show" -> return NaturalShow- "Natural/subtract" -> return NaturalSubtract- "Integer/toDouble" -> return IntegerToDouble- "Integer/clamp" -> return IntegerClamp- "Integer/negate" -> return IntegerNegate- "Integer/show" -> return IntegerShow- "Double/show" -> return DoubleShow- "List/build" -> return ListBuild- "List/fold" -> return ListFold- "List/length" -> return ListLength- "List/head" -> return ListHead- "List/last" -> return ListLast- "List/indexed" -> return ListIndexed- "List/reverse" -> return ListReverse- "Optional/fold" -> return OptionalFold- "Optional/build" -> return OptionalBuild- "Bool" -> return Bool- "Optional" -> return Optional- "None" -> return None- "Natural" -> return Natural- "Integer" -> return Integer- "Double" -> return Double- "Text" -> return Text- "Text/show" -> return TextShow- "List" -> return List- "Type" -> return (Const Type)- "Kind" -> return (Const Kind)- "Sort" -> return (Const Sort)- _ -> die ("Unrecognized built-in: " <> Text.unpack s)+ let sb = Codec.CBOR.ByteArray.toShortByteString ba + case Data.ByteString.Short.length sb of+ 4 | sb == "Bool" -> return Bool+ | sb == "List" -> return List+ | sb == "None" -> return None+ | sb == "Text" -> return Text+ | sb == "Type" -> return (Const Type)+ | sb == "Kind" -> return (Const Kind)+ | sb == "Sort" -> return (Const Sort)+ 6 | sb == "Double" -> return Double+ 7 | sb == "Integer" -> return Integer+ | sb == "Natural" -> return Natural+ 8 | sb == "Optional" -> return Optional+ 9 | sb == "List/fold" -> return ListFold+ | sb == "List/head" -> return ListHead+ | sb == "List/last" -> return ListLast+ | sb == "Text/show" -> return TextShow+ 10 | sb == "List/build" -> return ListBuild+ 11 | sb == "Double/show" -> return DoubleShow+ | sb == "List/length" -> return ListLength+ | sb == "Natural/odd" -> return NaturalOdd+ 12 | sb == "Integer/show" -> return IntegerShow+ | sb == "List/indexed" -> return ListIndexed+ | sb == "List/reverse" -> return ListReverse+ | sb == "Natural/even" -> return NaturalEven+ | sb == "Natural/fold" -> return NaturalFold+ | sb == "Natural/show" -> return NaturalShow+ 13 | sb == "Integer/clamp" -> return IntegerClamp+ | sb == "Natural/build" -> return NaturalBuild+ 14 | sb == "Integer/negate" -> return IntegerNegate+ | sb == "Natural/isZero" -> return NaturalIsZero+ 16 | sb == "Integer/toDouble" -> return IntegerToDouble+ | sb == "Natural/subtract" -> return NaturalSubtract+ 17 | sb == "Natural/toInteger" -> return NaturalToInteger+ _ -> die ("Unrecognized built-in: " <> show sb)+ TypeListLen -> do len <- Decoding.decodeListLen @@ -218,14 +218,14 @@ case tokenType₂ of TypeUInt -> do- !n <- Decoding.decodeWord+ !n <- fromIntegral <$> Decoding.decodeWord - return (Var (V x (fromIntegral n)))+ return (Var (V x n)) TypeUInt64 -> do- !n <- Decoding.decodeWord64+ !n <- fromIntegral <$> Decoding.decodeWord64 - return (Var (V x (fromIntegral n)))+ return (Var (V x n)) _ -> do die ("Unexpected token type for variable index: " <> show tokenType₂)@@ -235,15 +235,19 @@ case tag of 0 -> do- f <- go+ !f <- go - xs <- Monad.replicateM (len - 2) go+ let loop n !acc+ | n <= 0 = return acc+ | otherwise = do+ !x <- go+ loop (n - 1) (App acc x) - if null xs- then die "Non-standard encoding of a function with no arguments"- else return ()+ let nArgs = len - 2 - return (foldl' App f xs)+ if nArgs <= 0+ then die "Non-standard encoding of a function with no arguments"+ else loop nArgs f 1 -> do case len of@@ -331,8 +335,8 @@ _ -> do Decoding.decodeNull - xs <- Monad.replicateM (len - 2) go- return (ListLit Nothing (Data.Sequence.fromList xs))+ xs <- Data.Sequence.replicateA (len - 2) go+ return (ListLit Nothing xs) 5 -> do Decoding.decodeNull@@ -361,7 +365,7 @@ 7 -> do mapLength <- Decoding.decodeMapLen - xTs <- Monad.replicateM mapLength $ do+ xTs <- replicateDecoder mapLength $ do x <- Decoding.decodeString _T <- go@@ -373,7 +377,7 @@ 8 -> do mapLength <- Decoding.decodeMapLen - xts <- Monad.replicateM mapLength $ do+ xts <- replicateDecoder mapLength $ do x <- Decoding.decodeString t <- go@@ -412,7 +416,7 @@ die ("Unexpected token type for projection: " <> show tokenType₂) _ -> do- xs <- Monad.replicateM (len - 2) Decoding.decodeString+ xs <- replicateDecoder (len - 2) Decoding.decodeString return (Left (Dhall.Set.fromList xs)) @@ -421,7 +425,7 @@ 11 -> do mapLength <- Decoding.decodeMapLen - xTs <- Monad.replicateM mapLength $ do+ xTs <- replicateDecoder mapLength $ do x <- Decoding.decodeString tokenType₂ <- Decoding.peekTokenType@@ -455,18 +459,18 @@ case tokenType₂ of TypeUInt -> do- n <- Decoding.decodeWord+ !n <- fromIntegral <$> Decoding.decodeWord - return (NaturalLit (fromIntegral n))+ return (NaturalLit n) TypeUInt64 -> do- n <- Decoding.decodeWord64+ !n <- fromIntegral <$> Decoding.decodeWord64 - return (NaturalLit (fromIntegral n))+ return (NaturalLit n) TypeInteger -> do- n <- Decoding.decodeInteger- return (NaturalLit (fromIntegral n))+ !n <- fromIntegral <$> Decoding.decodeInteger+ return (NaturalLit n) _ -> do die ("Unexpected token type for Natural literal: " <> show tokenType₂)@@ -476,24 +480,24 @@ case tokenType₂ of TypeUInt -> do- n <- Decoding.decodeWord+ !n <- fromIntegral <$> Decoding.decodeWord - return (IntegerLit (fromIntegral n))+ return (IntegerLit n) TypeUInt64 -> do- n <- Decoding.decodeWord64+ !n <- fromIntegral <$> Decoding.decodeWord64 - return (IntegerLit (fromIntegral n))+ return (IntegerLit n) TypeNInt -> do- n <- Decoding.decodeNegWord+ !n <- fromIntegral <$> Decoding.decodeNegWord - return (IntegerLit (-1 - fromIntegral n))+ return (IntegerLit $! (-1 - n)) TypeNInt64 -> do- n <- Decoding.decodeNegWord64+ !n <- fromIntegral <$> Decoding.decodeNegWord64 - return (IntegerLit (-1 - fromIntegral n))+ return (IntegerLit $! (-1 - n)) TypeInteger -> do n <- Decoding.decodeInteger return (IntegerLit n)@@ -502,7 +506,7 @@ die ("Unexpected token type for Integer literal: " <> show tokenType₂) 18 -> do- xys <- Monad.replicateM ((len - 2) `quot` 2) $ do+ xys <- replicateDecoder ((len - 2) `quot` 2) $ do x <- Decoding.decodeString y <- go@@ -522,7 +526,7 @@ fmap Embed (decodeEmbed len) 25 -> do- bindings <- Monad.replicateM ((len - 2) `quot` 3) $ do+ bindings <- replicateDecoder ((len - 2) `quot` 3) $ do x <- Decoding.decodeString tokenType₂ <- Decoding.peekTokenType@@ -597,106 +601,100 @@ <> Encoding.encodeInt n NaturalBuild ->- Encoding.encodeString "Natural/build"+ Encoding.encodeUtf8ByteArray "Natural/build" NaturalFold ->- Encoding.encodeString "Natural/fold"+ Encoding.encodeUtf8ByteArray "Natural/fold" NaturalIsZero ->- Encoding.encodeString "Natural/isZero"+ Encoding.encodeUtf8ByteArray "Natural/isZero" NaturalEven ->- Encoding.encodeString "Natural/even"+ Encoding.encodeUtf8ByteArray "Natural/even" NaturalOdd ->- Encoding.encodeString "Natural/odd"+ Encoding.encodeUtf8ByteArray "Natural/odd" NaturalToInteger ->- Encoding.encodeString "Natural/toInteger"+ Encoding.encodeUtf8ByteArray "Natural/toInteger" NaturalShow ->- Encoding.encodeString "Natural/show"+ Encoding.encodeUtf8ByteArray "Natural/show" NaturalSubtract ->- Encoding.encodeString "Natural/subtract"+ Encoding.encodeUtf8ByteArray "Natural/subtract" IntegerToDouble ->- Encoding.encodeString "Integer/toDouble"+ Encoding.encodeUtf8ByteArray "Integer/toDouble" IntegerClamp ->- Encoding.encodeString "Integer/clamp"+ Encoding.encodeUtf8ByteArray "Integer/clamp" IntegerNegate ->- Encoding.encodeString "Integer/negate"+ Encoding.encodeUtf8ByteArray "Integer/negate" IntegerShow ->- Encoding.encodeString "Integer/show"+ Encoding.encodeUtf8ByteArray "Integer/show" DoubleShow ->- Encoding.encodeString "Double/show"+ Encoding.encodeUtf8ByteArray "Double/show" ListBuild ->- Encoding.encodeString "List/build"+ Encoding.encodeUtf8ByteArray "List/build" ListFold ->- Encoding.encodeString "List/fold"+ Encoding.encodeUtf8ByteArray "List/fold" ListLength ->- Encoding.encodeString "List/length"+ Encoding.encodeUtf8ByteArray "List/length" ListHead ->- Encoding.encodeString "List/head"+ Encoding.encodeUtf8ByteArray "List/head" ListLast ->- Encoding.encodeString "List/last"+ Encoding.encodeUtf8ByteArray "List/last" ListIndexed ->- Encoding.encodeString "List/indexed"+ Encoding.encodeUtf8ByteArray "List/indexed" ListReverse ->- Encoding.encodeString "List/reverse"-- OptionalFold ->- Encoding.encodeString "Optional/fold"-- OptionalBuild ->- Encoding.encodeString "Optional/build"+ Encoding.encodeUtf8ByteArray "List/reverse" Bool ->- Encoding.encodeString "Bool"+ Encoding.encodeUtf8ByteArray "Bool" Optional ->- Encoding.encodeString "Optional"+ Encoding.encodeUtf8ByteArray "Optional" None ->- Encoding.encodeString "None"+ Encoding.encodeUtf8ByteArray "None" Natural ->- Encoding.encodeString "Natural"+ Encoding.encodeUtf8ByteArray "Natural" Integer ->- Encoding.encodeString "Integer"+ Encoding.encodeUtf8ByteArray "Integer" Double ->- Encoding.encodeString "Double"+ Encoding.encodeUtf8ByteArray "Double" Text ->- Encoding.encodeString "Text"+ Encoding.encodeUtf8ByteArray "Text" TextShow ->- Encoding.encodeString "Text/show"+ Encoding.encodeUtf8ByteArray "Text/show" List ->- Encoding.encodeString "List"+ Encoding.encodeUtf8ByteArray "List" Const Type ->- Encoding.encodeString "Type"+ Encoding.encodeUtf8ByteArray "Type" Const Kind ->- Encoding.encodeString "Kind"+ Encoding.encodeUtf8ByteArray "Kind" Const Sort ->- Encoding.encodeString "Sort"+ Encoding.encodeUtf8ByteArray "Sort" a@App{} -> encodeListN@@ -1034,7 +1032,7 @@ authority <- Decoding.decodeString - paths <- Monad.replicateM (len - 8) Decoding.decodeString+ paths <- replicateDecoder (len - 8) Decoding.decodeString file <- Decoding.decodeString @@ -1054,7 +1052,7 @@ return (Remote (URL {..})) let local prefix = do- paths <- Monad.replicateM (len - 5) Decoding.decodeString+ paths <- replicateDecoder (len - 5) Decoding.decodeString file <- Decoding.decodeString @@ -1178,7 +1176,7 @@ decode = decodeExpressionInternal decodeImport -- | Encode a Dhall expression as a CBOR-encoded `ByteString`-encodeExpression :: Expr Void Import -> ByteString+encodeExpression :: Serialise (Expr Void a) => Expr Void a -> ByteString encodeExpression = Serialise.serialise -- | Decode a Dhall expression from a CBOR `Term`@@ -1251,3 +1249,15 @@ <> "↳ 0x" <> concatMap toHex (Data.ByteString.Lazy.unpack bytes) <> "\n" where toHex = Printf.printf "%02x "++-- | This specialized version of 'Control.Monad.replicateM' reduces+-- decoding timings by roughly 10%.+replicateDecoder :: Int -> Decoder s a -> Decoder s [a]+replicateDecoder n0 decoder = go n0+ where+ go n+ | n <= 0 = pure []+ | otherwise = do+ x <- decoder+ xs <- go (n - 1)+ pure (x:xs)
src/Dhall/Deriving.hs view
@@ -91,7 +91,7 @@ -- to 'genericAutoWith'. newtype Codec tag a = Codec { unCodec :: a } -instance (Generic a, GenericFromDhall (Rep a), ModifyOptions tag) => FromDhall (Codec tag a) where+instance (Generic a, GenericFromDhall a (Rep a), ModifyOptions tag) => FromDhall (Codec tag a) where autoWith _ = Codec <$> genericAutoWith (modifyOptions @tag defaultInterpretOptions) instance (Generic a, GenericToDhall (Rep a), ModifyOptions tag) => ToDhall (Codec tag a) where@@ -378,7 +378,7 @@ | + `Times New Roman` : … | … >-, name : - { … : … }+, name : - { … : … } (a record type) + Text } ...
src/Dhall/Diff.hs view
@@ -430,12 +430,14 @@ <> rarrow <> " " <> ignore+ <> " (a function)" skeleton (Pi {}) = ignore <> " " <> rarrow <> " " <> ignore+ <> " (a function type)" skeleton (App Optional _) = "Optional " <> ignore@@ -556,6 +558,7 @@ <> ignore <> " " <> rbrace+ <> " (a record type)" skeleton (RecordLit {}) = lbrace <> " "@@ -566,6 +569,7 @@ <> ignore <> " " <> rbrace+ <> " (a record)" skeleton (Union {}) = langle <> " "@@ -576,6 +580,7 @@ <> ignore <> " " <> rangle+ <> " (a union type)" skeleton (Combine {}) = ignore <> " "@@ -1271,18 +1276,6 @@ diffPrimitiveExpression l@None r = mismatch l r diffPrimitiveExpression l r@None =- mismatch l r-diffPrimitiveExpression OptionalFold OptionalFold =- "…"-diffPrimitiveExpression l@OptionalFold r =- mismatch l r-diffPrimitiveExpression l r@OptionalFold =- mismatch l r-diffPrimitiveExpression OptionalBuild OptionalBuild =- "…"-diffPrimitiveExpression l@OptionalBuild r =- mismatch l r-diffPrimitiveExpression l r@OptionalBuild = mismatch l r diffPrimitiveExpression (BoolLit aL) (BoolLit aR) = diffBool aL aR
src/Dhall/DirectoryTree.hs view
@@ -10,11 +10,11 @@ ) where import Control.Applicative (empty)-import Control.Exception (Exception)-import Data.Monoid ((<>))-import Data.Void (Void)-import Dhall.Syntax (Chunks(..), Expr(..))-import System.FilePath ((</>))+import Control.Exception (Exception)+import Data.Monoid ((<>))+import Data.Void (Void)+import Dhall.Syntax (Chunks (..), Expr (..))+import System.FilePath ((</>)) import qualified Control.Exception as Exception import qualified Data.Foldable as Foldable@@ -147,54 +147,54 @@ Pretty.renderString (Dhall.Pretty.layout message) where message =- Util._ERROR <> ": Not a valid directory tree expression\n\- \ \n\- \Explanation: Only a subset of Dhall expressions can be converted to a directory \n\- \tree. Specifically, record literals or maps can be converted to directories, \n\- \❰Text❱ literals can be converted to files, and ❰Optional❱ values are included if\n\- \❰Some❱ and omitted if ❰None❱. Values of union types can also be converted if \n\- \they are an alternative which has a non-nullary constructor whose argument is of\n\- \an otherwise convertible type. No other type of value can be translated to a \n\- \directory tree. \n\- \ \n\- \For example, this is a valid expression that can be translated to a directory \n\- \tree: \n\- \ \n\- \ \n\- \ ┌──────────────────────────────────┐ \n\- \ │ { `example.json` = \"[1, true]\" } │ \n\- \ └──────────────────────────────────┘ \n\- \ \n\- \ \n\- \In contrast, the following expression is not allowed due to containing a \n\- \❰Natural❱ field, which cannot be translated in this way: \n\- \ \n\- \ \n\- \ ┌───────────────────────┐ \n\- \ │ { `example.txt` = 1 } │ \n\- \ └───────────────────────┘ \n\- \ \n\- \ \n\- \Note that key names cannot contain path separators: \n\- \ \n\- \ \n\- \ ┌───────────────────────────────────┐ \n\- \ │ { `directory/example.txt` = \"ABC\" │ Invalid: Key contains a forward slash \n\- \ └───────────────────────────────────┘ \n\- \ \n\- \ \n\- \Instead, you need to refactor the expression to use nested records instead: \n\- \ \n\- \ \n\- \ ┌───────────────────────────────────────────┐ \n\- \ │ { directory = { `example.txt` = \"ABC\" } } │ \n\- \ └───────────────────────────────────────────┘ \n\- \ \n\- \ \n\- \You tried to translate the following expression to a directory tree: \n\- \ \n\+ Util._ERROR <> ": Not a valid directory tree expression \n\+ \ \n\+ \Explanation: Only a subset of Dhall expressions can be converted to a directory \n\+ \tree. Specifically, record literals or maps can be converted to directories, \n\+ \❰Text❱ literals can be converted to files, and ❰Optional❱ values are included if \n\+ \❰Some❱ and omitted if ❰None❱. Values of union types can also be converted if \n\+ \they are an alternative which has a non-nullary constructor whose argument is of \n\+ \an otherwise convertible type. No other type of value can be translated to a \n\+ \directory tree. \n\+ \ \n\+ \For example, this is a valid expression that can be translated to a directory \n\+ \tree: \n\+ \ \n\+ \ \n\+ \ ┌──────────────────────────────────┐ \n\+ \ │ { `example.json` = \"[1, true]\" } │ \n\+ \ └──────────────────────────────────┘ \n\+ \ \n\+ \ \n\+ \In contrast, the following expression is not allowed due to containing a \n\+ \❰Natural❱ field, which cannot be translated in this way: \n\+ \ \n\+ \ \n\+ \ ┌───────────────────────┐ \n\+ \ │ { `example.txt` = 1 } │ \n\+ \ └───────────────────────┘ \n\+ \ \n\+ \ \n\+ \Note that key names cannot contain path separators: \n\+ \ \n\+ \ \n\+ \ ┌─────────────────────────────────────┐ \n\+ \ │ { `directory/example.txt` = \"ABC\" } │ Invalid: Key contains a forward slash\n\+ \ └─────────────────────────────────────┘ \n\+ \ \n\+ \ \n\+ \Instead, you need to refactor the expression to use nested records instead: \n\+ \ \n\+ \ \n\+ \ ┌───────────────────────────────────────────┐ \n\+ \ │ { directory = { `example.txt` = \"ABC\" } } │ \n\+ \ └───────────────────────────────────────────┘ \n\+ \ \n\+ \ \n\+ \You tried to translate the following expression to a directory tree: \n\+ \ \n\ \" <> Util.insert unexpectedExpression <> "\n\- \ \n\- \... which is not an expression that can be translated to a directory tree. \n"+ \ \n\+ \... which is not an expression that can be translated to a directory tree. \n" instance Exception FilesystemError
src/Dhall/Eval.hs view
@@ -211,8 +211,6 @@ | VOptional (Val a) | VSome (Val a) | VNone (Val a)- | VOptionalFold (Val a) !(Val a) (Val a) !(Val a) !(Val a)- | VOptionalBuild (Val a) !(Val a) | VRecord !(Map Text (Val a)) | VRecordLit !(Map Text (Val a)) | VUnion !(Map Text (Maybe (Val a)))@@ -671,32 +669,6 @@ VSome (eval env t) None -> VPrim $ \ ~a -> VNone a- OptionalFold ->- VPrim $ \ ~a ->- VPrim $ \case- VNone _ ->- VHLam (Typed "optional" (VConst Type)) $ \optional ->- VHLam (Typed "some" (a ~> optional)) $ \_some ->- VHLam (Typed "none" optional) $ \none ->- none- VSome t ->- VHLam (Typed "optional" (VConst Type)) $ \optional ->- VHLam (Typed "some" (a ~> optional)) $ \some ->- VHLam (Typed "none" optional) $ \_none ->- some `vApp` t- opt ->- VPrim $ \o ->- VPrim $ \s ->- VPrim $ \n ->- VOptionalFold a opt o s n- OptionalBuild ->- VPrim $ \ ~a ->- VPrim $ \case- VPrimVar -> VOptionalBuild a VPrimVar- t -> t- `vApp` VOptional a- `vApp` VHLam (Typed "a" a) VSome- `vApp` VNone a Record kts -> VRecord (Map.sort (fmap (eval env) kts)) RecordLit kts ->@@ -937,8 +909,6 @@ conv env t t' (VNone _, VNone _) -> True- (VOptionalBuild _ t, VOptionalBuild _ t') ->- conv env t t' (VRecord m, VRecord m') -> eqMapsBy (conv env) m m' (VRecordLit m, VRecordLit m') ->@@ -969,8 +939,6 @@ eqMapsBy (eqMaybeBy (conv env)) m m' && k == k' && eqMaybeBy (conv env) mt mt' (VEmbed a, VEmbed a') -> a == a'- (VOptionalFold a t _ u v, VOptionalFold a' t' _ u' v') ->- conv env a a' && conv env t t' && conv env u u' && conv env v v' (_, _) -> False where@@ -1123,10 +1091,6 @@ Some (quote env t) VNone t -> None `qApp` t- VOptionalFold a o t u v ->- OptionalFold `qApp` a `qApp` o `qApp` t `qApp` u `qApp` v- VOptionalBuild a t ->- OptionalBuild `qApp` a `qApp` t VRecord m -> Record (fmap (quote env) m) VRecordLit m ->@@ -1303,10 +1267,6 @@ Some (go t) None -> None- OptionalFold ->- OptionalFold- OptionalBuild ->- OptionalBuild Record kts -> Record (fmap go kts) RecordLit kts ->
src/Dhall/Format.hs view
@@ -49,20 +49,25 @@ <> Dhall.Pretty.prettyCharacterSet characterSet expr <> "\n") - let layoutInput = do- headerAndExpr <- Dhall.Util.getExpressionAndHeader censor input+ originalText <- case input of+ InputFile file -> Data.Text.IO.readFile file+ StandardInput -> Data.Text.IO.getContents - return (layoutHeaderAndExpr headerAndExpr)+ headerAndExpr <- Dhall.Util.getExpressionAndHeaderFromStdinText censor originalText + let docStream = layoutHeaderAndExpr headerAndExpr++ let formattedText = Pretty.Text.renderStrict docStream+ case outputMode of Write -> do- docStream <- layoutInput- case input of InputFile file -> do- AtomicWrite.LazyText.atomicWriteFile- file- (Pretty.Text.renderLazy docStream)+ if originalText == formattedText+ then return ()+ else AtomicWrite.LazyText.atomicWriteFile+ file+ (Pretty.Text.renderLazy docStream) StandardInput -> do supportsANSI <- System.Console.ANSI.hSupportsANSI System.IO.stdout@@ -74,18 +79,6 @@ else (Pretty.unAnnotateS docStream)) Check -> do- originalText <- case input of- InputFile file -> Data.Text.IO.readFile file- StandardInput -> Data.Text.IO.getContents-- docStream <- case input of- InputFile _ -> layoutInput- StandardInput -> do- headerAndExpr <- Dhall.Util.getExpressionAndHeaderFromStdinText censor originalText- return (layoutHeaderAndExpr headerAndExpr)-- let formattedText = Pretty.Text.renderStrict docStream- if originalText == formattedText then return () else do
src/Dhall/Freeze.hs view
@@ -16,10 +16,7 @@ , Intent(..) ) where -import Data.Bifunctor (first) import Data.Monoid ((<>))-import Data.Text-import Dhall.Parser (Src) import Dhall.Pretty (CharacterSet) import Dhall.Syntax (Expr(..), Import(..), ImportHashed(..), ImportType(..)) import Dhall.Util@@ -40,7 +37,6 @@ import qualified Dhall.Core as Core import qualified Dhall.Import import qualified Dhall.Optics-import qualified Dhall.Parser as Parser import qualified Dhall.Pretty import qualified Dhall.TypeCheck import qualified Dhall.Util as Util@@ -95,30 +91,6 @@ Remote {} -> freezeImport directory import_ _ -> return import_ -writeExpr :: Input -> (Text, Expr Src Import) -> CharacterSet -> IO ()-writeExpr input (header, expr) characterSet = do- let doc = Pretty.pretty header- <> Dhall.Pretty.prettyCharacterSet characterSet expr- <> "\n"-- let stream = Dhall.Pretty.layout doc-- let unAnnotated = Pretty.unAnnotateS stream-- case input of- InputFile file ->- AtomicWrite.LazyText.atomicWriteFile- file- (Pretty.Text.renderLazy unAnnotated)-- StandardInput -> do- supportsANSI <- System.Console.ANSI.hSupportsANSI System.IO.stdout- if supportsANSI- then- Pretty.renderIO System.IO.stdout (Dhall.Pretty.annToAnsiStyle <$> stream)- else- Pretty.renderIO System.IO.stdout unAnnotated- -- | Specifies which imports to freeze data Scope = OnlyRemoteImports@@ -153,37 +125,44 @@ let rewrite = freezeExpression directory scope intent - case outputMode of- Write -> do- (Header header, parsedExpression) <- do- Util.getExpressionAndHeader censor input-- frozenExpression <- rewrite parsedExpression+ originalText <- case input of+ InputFile file -> Text.IO.readFile file+ StandardInput -> Text.IO.getContents - writeExpr input (header, frozenExpression) characterSet+ (Header header, parsedExpression) <- Util.getExpressionAndHeaderFromStdinText censor originalText - Check -> do- originalText <- case input of- InputFile file -> Text.IO.readFile file- StandardInput -> Text.IO.getContents+ frozenExpression <- rewrite parsedExpression - let name = case input of- InputFile file -> file- StandardInput -> "(input)"+ let doc = Pretty.pretty header+ <> Dhall.Pretty.prettyCharacterSet characterSet frozenExpression+ <> "\n" - (Header header, parsedExpression) <- do- Core.throws (first Parser.censor (Parser.exprAndHeaderFromText name originalText))+ let stream = Dhall.Pretty.layout doc - frozenExpression <- rewrite parsedExpression+ let modifiedText = Pretty.Text.renderStrict stream - let doc = Pretty.pretty header- <> Dhall.Pretty.prettyCharacterSet characterSet frozenExpression- <> "\n"+ case outputMode of+ Write -> do+ let unAnnotated = Pretty.unAnnotateS stream - let stream = Dhall.Pretty.layout doc+ case input of+ InputFile file ->+ if originalText == modifiedText+ then return ()+ else+ AtomicWrite.LazyText.atomicWriteFile+ file+ (Pretty.Text.renderLazy unAnnotated) - let modifiedText = Pretty.Text.renderStrict stream+ StandardInput -> do+ supportsANSI <- System.Console.ANSI.hSupportsANSI System.IO.stdout+ if supportsANSI+ then+ Pretty.renderIO System.IO.stdout (Dhall.Pretty.annToAnsiStyle <$> stream)+ else+ Pretty.renderIO System.IO.stdout unAnnotated + Check -> do if originalText == modifiedText then return () else do
src/Dhall/Import.hs view
@@ -3,9 +3,9 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall #-} {-| Dhall lets you import external expressions located either in local files or@@ -138,41 +138,53 @@ , HashMismatch(..) ) where -import Control.Applicative (Alternative(..), liftA2)-import Control.Exception (Exception, SomeException, IOException, toException)-import Control.Monad (when)-import Control.Monad.Catch (throwM, MonadCatch(catch), handle)-import Control.Monad.IO.Class (MonadIO(..))-import Control.Monad.Trans.Class (lift)+import Control.Applicative (Alternative (..), liftA2)+import Control.Exception+ ( Exception+ , IOException+ , SomeException+ , toException+ )+import Control.Monad (when)+import Control.Monad.Catch (MonadCatch (catch), handle, throwM)+import Control.Monad.IO.Class (MonadIO (..))+import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.State.Strict (StateT)-import Data.ByteString (ByteString)-import Data.CaseInsensitive (CI)-import Data.List.NonEmpty (NonEmpty(..))-import Data.Semigroup (Semigroup(..))-import Data.Text (Text)-import Data.Void (Void, absurd)-import Data.Typeable (Typeable)-import System.FilePath ((</>))-import Dhall.Binary (StandardVersion(..))+import Data.ByteString (ByteString)+import Data.CaseInsensitive (CI)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Semigroup (Semigroup (..))+import Data.Text (Text)+import Data.Typeable (Typeable)+import Data.Void (Void, absurd)+import Dhall.Binary (StandardVersion (..))+ import Dhall.Syntax- ( Expr(..)- , Chunks(..)- , Directory(..)- , File(..)- , FilePrefix(..)- , ImportHashed(..)- , ImportType(..)- , ImportMode(..)- , Import(..)- , URL(..)+ ( Chunks (..)+ , Directory (..)+ , Expr (..)+ , File (..)+ , FilePrefix (..)+ , Import (..)+ , ImportHashed (..)+ , ImportMode (..)+ , ImportType (..)+ , URL (..) , bindingExprs )++import System.FilePath ((</>)) #ifdef WITH_HTTP import Dhall.Import.HTTP #endif import Dhall.Import.Types -import Dhall.Parser (Parser(..), ParseError(..), Src(..), SourcedException(..))+import Dhall.Parser+ ( ParseError (..)+ , Parser (..)+ , SourcedException (..)+ , Src (..)+ ) import Lens.Family.State.Strict (zoom) import qualified Codec.CBOR.Encoding as Encoding@@ -185,8 +197,8 @@ import qualified Data.CaseInsensitive import qualified Data.Foldable import qualified Data.List.NonEmpty as NonEmpty-import qualified Data.Text.Encoding import qualified Data.Text as Text+import qualified Data.Text.Encoding import qualified Data.Text.IO import qualified Dhall.Binary import qualified Dhall.Core@@ -198,11 +210,11 @@ import qualified Dhall.Syntax as Syntax import qualified Dhall.TypeCheck import qualified System.AtomicWrite.Writer.ByteString.Binary as AtomicWrite.Binary+import qualified System.Directory as Directory import qualified System.Environment+import qualified System.FilePath as FilePath import qualified System.Info import qualified System.IO-import qualified System.Directory as Directory-import qualified System.FilePath as FilePath import qualified Text.Megaparsec import qualified Text.Parser.Combinators import qualified Text.Parser.Token@@ -279,7 +291,7 @@ toDisplay = drop 1 (reverse canonical) -- | Exception thrown when an imported file is missing-data MissingFile = MissingFile FilePath+newtype MissingFile = MissingFile FilePath deriving (Typeable) instance Exception MissingFile@@ -297,7 +309,7 @@ instance Exception MissingEnvironmentVariable instance Show MissingEnvironmentVariable where- show (MissingEnvironmentVariable {..}) =+ show MissingEnvironmentVariable{..} = "\n" <> "\ESC[1;31mError\ESC[0m: Missing environment variable\n" <> "\n"@@ -410,9 +422,13 @@ instance Exception HashMismatch instance Show HashMismatch where- show (HashMismatch {..}) =+ show HashMismatch{..} = "\n"- <> "\ESC[1;31mError\ESC[0m: Import integrity check failed\n"+ <> "\ESC[1;31mError\ESC[0m: " <> makeHashMismatchMessage expectedHash actualHash++makeHashMismatchMessage :: Dhall.Crypto.SHA256Digest -> Dhall.Crypto.SHA256Digest -> String+makeHashMismatchMessage expectedHash actualHash =+ "Import integrity check failed\n" <> "\n" <> "Expected hash:\n" <> "\n"@@ -431,16 +447,16 @@ let Directory {..} = directory prefixPath <- case prefix of- Home -> do+ Home -> Directory.getHomeDirectory - Absolute -> do+ Absolute -> return "/" - Parent -> do+ Parent -> return ".." - Here -> do+ Here -> return "." let cs = map Text.unpack (file : components)@@ -490,10 +506,14 @@ -- therefore not cached semantically), as well as those that aren't cached yet. loadImportWithSemanticCache :: Chained -> StateT Status IO ImportSemantics loadImportWithSemanticCache- import_@(Chained (Import (ImportHashed Nothing _) _)) = do+ import_@(Chained (Import (ImportHashed Nothing _) _)) = loadImportWithSemisemanticCache import_ loadImportWithSemanticCache+ import_@(Chained (Import _ Location)) = do+ loadImportWithSemisemanticCache import_++loadImportWithSemanticCache import_@(Chained (Import (ImportHashed (Just semanticHash) _) _)) = do Status { .. } <- State.get mCached <-@@ -506,20 +526,25 @@ let actualHash = Dhall.Crypto.sha256Hash bytesStrict if semanticHash == actualHash- then return ()- else do- Status { _stack } <- State.get- throwMissingImport (Imported _stack (HashMismatch {expectedHash = semanticHash, ..}))+ then do+ let bytesLazy = Data.ByteString.Lazy.fromStrict bytesStrict - let bytesLazy = Data.ByteString.Lazy.fromStrict bytesStrict+ importSemantics <- case Dhall.Binary.decodeExpression bytesLazy of+ Left err -> throwMissingImport (Imported _stack err)+ Right e -> return e - importSemantics <- case Dhall.Binary.decodeExpression bytesLazy of- Left err -> throwMissingImport (Imported _stack err)- Right e -> return e+ return (ImportSemantics {..})+ else do+ printWarning $+ makeHashMismatchMessage semanticHash actualHash+ <> "\n"+ <> "The interpreter will attempt to fix the cached import\n"+ fetch - return (ImportSemantics {..}) - Nothing -> do+ Nothing -> fetch+ where+ fetch = do ImportSemantics { importSemantics } <- loadImportWithSemisemanticCache import_ let variants = map (\version -> encodeExpression version (Dhall.Core.alphaNormalize importSemantics))@@ -534,6 +559,8 @@ return (ImportSemantics {..}) ++ -- Fetch encoded normal form from "semantic cache" fetchFromSemanticCache :: Dhall.Crypto.SHA256Digest -> IO (Maybe Data.ByteString.ByteString) fetchFromSemanticCache expectedHash = Maybe.runMaybeT $ do@@ -599,7 +626,7 @@ let bytesLazy = Data.ByteString.Lazy.fromStrict bytesStrict importSemantics <- case Dhall.Binary.decodeExpression bytesLazy of- Left err -> throwMissingImport (Imported _stack err)+ Left err -> throwMissingImport (Imported _stack err) Right sem -> return sem return importSemantics@@ -756,12 +783,7 @@ getOrCreateCacheDirectory :: (MonadCatch m, Alternative m, MonadIO m) => Bool -> FilePath -> m FilePath getOrCreateCacheDirectory showWarning cacheName = do let warn message = do- let warning =- "\n"- <> "\ESC[1;33mWarning\ESC[0m: "- <> message-- when showWarning (liftIO (System.IO.hPutStrLn System.IO.stderr warning))+ when showWarning (printWarning message) empty @@ -774,7 +796,7 @@ <> "... the following exception was thrown:\n" <> "\n" <> "↳ " <> show ioex <> "\n"- + warn ioExMsg let setPermissions dir = do@@ -853,7 +875,7 @@ createDirectory dir setPermissions dir- + cacheBaseDirectory <- getCacheBaseDirectory showWarning let directory = cacheBaseDirectory </> cacheName@@ -943,7 +965,7 @@ _ <- case (Dhall.TypeCheck.typeOf annot) of Left err -> throwMissingImport (Imported _stack err)- Right _ -> return ()+ Right _ -> return () return (Dhall.Core.normalize loadedExpr) @@ -1031,6 +1053,15 @@ -- | Resolve all imports within an expression load :: Expr Src Import -> IO (Expr Src Void) load = loadRelativeTo "." UseSemanticCache++printWarning :: (MonadIO m) => String -> m ()+printWarning message = do+ let warning =+ "\n"+ <> "\ESC[1;33mWarning\ESC[0m: "+ <> message++ liftIO $ System.IO.hPutStrLn System.IO.stderr warning -- | Resolve all imports within an expression, importing relative to the given -- directory.
src/Dhall/Lint.hs view
@@ -14,8 +14,6 @@ , fixAssert , fixParentPath , removeLetInLet- , replaceOptionalBuildFold- , replaceSaturatedOptionalFold , useToMap ) where @@ -24,7 +22,6 @@ import Dhall.Syntax ( Binding(..) , Chunks(..)- , Const(..) , Directory(..) , Expr(..) , File(..)@@ -51,21 +48,16 @@ * fixes @let a = x ≡ y@ to be @let a = assert : x ≡ y@ * consolidates nested @let@ bindings to use a multiple-@let@ binding with 'removeLetInLet' * fixes paths of the form @.\/..\/foo@ to @..\/foo@- * Replaces deprecated @Optional\/fold@ and @Optional\/build@ built-ins -} lint :: Expr s Import -> Expr s Import-lint = Dhall.Optics.rewriteOf subExpressions lowerPriorityRewrite- . Dhall.Optics.rewriteOf subExpressions higherPriorityRewrite+lint = Dhall.Optics.rewriteOf subExpressions rewrite where- lowerPriorityRewrite e =+ rewrite e = fixAssert e <|> removeUnusedBindings e <|> fixParentPath e <|> removeLetInLet e- <|> replaceOptionalBuildFold e - higherPriorityRewrite = replaceSaturatedOptionalFold- -- | Remove unused `Let` bindings. removeUnusedBindings :: Eq a => Expr s a -> Maybe (Expr s a) -- Don't remove assertions!@@ -131,68 +123,6 @@ removeLetInLet :: Expr s a -> Maybe (Expr s a) removeLetInLet (Let binding (Note _ l@Let{})) = Just (Let binding l) removeLetInLet _ = Nothing---- | This replaces @Optional/fold@ and @Optional/build@, both of which can be--- implemented within the language-replaceOptionalBuildFold :: Expr s a -> Maybe (Expr s a)-replaceOptionalBuildFold OptionalBuild =- Just- (Lam "a" (Const Type)- (Lam "build"- (Pi "optional" (Const Type)- (Pi "some" (Pi "_" "a" "optional")- (Pi "none" "optional" "optional")- )- )- (App (App (App "build" (App Optional "a")) (Lam "x" "a" (Some "x"))) (App None "a"))- )- )-replaceOptionalBuildFold OptionalFold =- Just- (Lam "a" (Const Type)- (Lam "o" (App Optional "a")- (Lam "optional" (Const Type)- (Lam "some" (Pi "_" "a" "optional")- (Lam "none" "optional"- (Merge- (RecordLit- [ ("Some", "some")- , ("None", "none")- ]- )- "o"- Nothing- )- )- )- )- )- )-replaceOptionalBuildFold _ =- Nothing---- | This replaces a saturated @Optional/fold@ with the equivalent @merge@--- expression-replaceSaturatedOptionalFold :: Expr s a -> Maybe (Expr s a)-replaceSaturatedOptionalFold- (App- (Core.shallowDenote -> App- (Core.shallowDenote -> App- (Core.shallowDenote -> App- (Core.shallowDenote -> App- (Core.shallowDenote -> OptionalFold)- _- )- o- )- _- )- some- )- none- ) = Just (Merge (RecordLit [ ("Some", some), ("None", none) ]) o Nothing)-replaceSaturatedOptionalFold _ =- Nothing -- | This replaces a record of key-value pairs with the equivalent use of -- @toMap@
src/Dhall/Main.hs view
@@ -20,41 +20,49 @@ , main ) where -import Control.Applicative (optional, (<|>))-import Control.Exception (Handler(..), SomeException)-import Control.Monad (when)-import Data.Bifunctor (first)-import Data.List.NonEmpty (NonEmpty(..))-import Data.Monoid ((<>))-import Data.Text (Text)+import Control.Applicative (optional, (<|>))+import Control.Exception (Handler (..), SomeException)+import Control.Monad (when)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Monoid ((<>))+import Data.Text (Text) import Data.Text.Prettyprint.Doc (Doc, Pretty)-import Data.Void (Void)-import Dhall.Freeze (Intent(..), Scope(..))-import Dhall.Import (Imported(..), Depends(..), SemanticCacheMode(..), _semanticCacheMode)-import Dhall.Parser (Src)-import Dhall.Pretty (Ann, CharacterSet(..), annToAnsiStyle)-import Dhall.TypeCheck (Censored(..), DetailedTypeError(..), TypeError)-import Dhall.Version (dhallVersionString)-import Options.Applicative (Parser, ParserInfo)-import System.Exit (ExitCode, exitFailure)-import System.IO (Handle)-import Text.Dot ((.->.))+import Data.Void (Void)+import Dhall.Freeze (Intent (..), Scope (..))+import Dhall.Import+ ( Depends (..)+ , Imported (..)+ , SemanticCacheMode (..)+ , _semanticCacheMode+ )+import Dhall.Parser (Src)+import Dhall.Pretty (Ann, CharacterSet (..), annToAnsiStyle)+import Dhall.TypeCheck+ ( Censored (..)+ , DetailedTypeError (..)+ , TypeError+ )+import Dhall.Version (dhallVersionString)+import Options.Applicative (Parser, ParserInfo)+import System.Exit (ExitCode, exitFailure)+import System.IO (Handle)+import Text.Dot ((.->.)) import Dhall.Core- ( Expr(Annot)- , Import(..)- , ImportHashed(..)- , ImportType(..)- , URL(..)+ ( Expr (Annot)+ , Import (..)+ , ImportHashed (..)+ , ImportType (..)+ , URL (..) , pretty ) import Dhall.Util- ( Censor(..)- , CheckFailed(..)+ ( Censor (..)+ , CheckFailed (..) , Header (..)- , Input(..)- , OutputMode(..)- , Output(..)+ , Input (..)+ , Output (..)+ , OutputMode (..) ) import qualified Codec.CBOR.JSON@@ -82,11 +90,10 @@ import qualified Dhall.Import import qualified Dhall.Import.Types import qualified Dhall.Lint-import qualified Dhall.Parser as Parser import qualified Dhall.Map-import qualified Dhall.Tags import qualified Dhall.Pretty import qualified Dhall.Repl+import qualified Dhall.Tags import qualified Dhall.TypeCheck import qualified Dhall.Util import qualified GHC.IO.Encoding@@ -94,8 +101,8 @@ import qualified System.AtomicWrite.Writer.LazyText as AtomicWrite.LazyText import qualified System.Console.ANSI import qualified System.Exit as Exit-import qualified System.IO import qualified System.FilePath+import qualified System.IO import qualified Text.Dot import qualified Text.Pretty.Simple @@ -149,10 +156,10 @@ , followSymlinks :: Bool } | Encode { file :: Input, json :: Bool }- | Decode { file :: Input, json :: Bool }+ | Decode { file :: Input, json :: Bool, quiet :: Bool } | Text { file :: Input } | DirectoryTree { file :: Input, path :: FilePath }- | SyntaxTree { file :: Input }+ | SyntaxTree { file :: Input, noted :: Bool } data ResolveMode = Dot@@ -263,7 +270,7 @@ Convert "decode" "Decode a Dhall expression from binary"- (Decode <$> parseFile <*> parseJSONFlag)+ (Decode <$> parseFile <*> parseJSONFlag <*> parseQuiet) <|> subcommand Miscellaneous "repl"@@ -293,7 +300,7 @@ Debugging "haskell-syntax-tree" "Output the parsed syntax tree (for debugging)"- (SyntaxTree <$> parseFile)+ (SyntaxTree <$> parseFile <*> parseNoted) <|> ( Default <$> parseFile <*> parseOutput@@ -380,7 +387,7 @@ parseQuiet = Options.Applicative.switch ( Options.Applicative.long "quiet"- <> Options.Applicative.help "Don't print the inferred type"+ <> Options.Applicative.help "Don't print the result" ) parseInplace = fmap f (optional p)@@ -470,6 +477,12 @@ <> Options.Applicative.metavar "PATH" ) + parseNoted =+ Options.Applicative.switch+ ( Options.Applicative.long "noted"+ <> Options.Applicative.help "Print `Note` constructors"+ )+ -- | `ParserInfo` for the `Options` type parserInfoOptions :: ParserInfo Options parserInfoOptions =@@ -501,8 +514,7 @@ let toStatus = Dhall.Import.emptyStatus . rootDirectory - let getExpression = Dhall.Util.getExpression censor- let getExpressionAndHeader = Dhall.Util.getExpressionAndHeader censor+ let getExpression = Dhall.Util.getExpression censor let handle io = Control.Exception.catches io@@ -739,42 +751,34 @@ Data.Text.IO.putStrLn (Dhall.Import.hashExpressionToCode normalizedExpression) Lint {..} -> do- case outputMode of- Write -> do- (Header header, expression) <- do- getExpressionAndHeader input-- let lintedExpression = Dhall.Lint.lint expression-- let doc = Pretty.pretty header- <> Dhall.Pretty.prettyCharacterSet characterSet lintedExpression-- case input of- InputFile file -> writeDocToFile file doc-- StandardInput -> renderDoc System.IO.stdout doc+ originalText <- case input of+ InputFile file -> Data.Text.IO.readFile file+ StandardInput -> Data.Text.IO.getContents - Check -> do- originalText <- case input of- InputFile file -> Data.Text.IO.readFile file- StandardInput -> Data.Text.IO.getContents+ (Header header, expression) <- do+ Dhall.Util.getExpressionAndHeaderFromStdinText censor originalText - let name = case input of- InputFile file -> file- StandardInput -> "(input)"+ let lintedExpression = Dhall.Lint.lint expression - (Header header, expression) <- do- Dhall.Core.throws (first Parser.censor (Parser.exprAndHeaderFromText name originalText))+ let doc = Pretty.pretty header+ <> Dhall.Pretty.prettyCharacterSet characterSet lintedExpression - let lintedExpression = Dhall.Lint.lint expression+ let stream = Dhall.Pretty.layout doc - let doc = Pretty.pretty header- <> Dhall.Pretty.prettyCharacterSet characterSet lintedExpression+ let modifiedText = Pretty.Text.renderStrict stream <> "\n" - let stream = Dhall.Pretty.layout doc+ case outputMode of+ Write -> do+ case input of+ InputFile file ->+ if originalText == modifiedText+ then return ()+ else writeDocToFile file doc - let modifiedText = Pretty.Text.renderStrict stream <> "\n"+ StandardInput ->+ renderDoc System.IO.stdout doc + Check -> do if originalText == modifiedText then return () else do@@ -822,9 +826,15 @@ Dhall.Core.throws (Dhall.Binary.decodeExpression bytes) - let doc = Dhall.Pretty.prettyCharacterSet characterSet (Dhall.Core.renote expression :: Expr Src Import)+ if quiet+ then return ()+ else do+ let doc =+ Dhall.Pretty.prettyCharacterSet+ characterSet+ (Dhall.Core.renote expression :: Expr Src Import) - renderDoc System.IO.stdout doc+ renderDoc System.IO.stdout doc Text {..} -> do expression <- getExpression file@@ -872,10 +882,12 @@ SyntaxTree {..} -> do expression <- getExpression file - let denoted :: Expr Void Import- denoted = Dhall.Core.denote expression-- Text.Pretty.Simple.pPrintNoColor denoted+ if noted then+ Text.Pretty.Simple.pPrintNoColor expression+ else+ let denoted :: Expr Void Import+ denoted = Dhall.Core.denote expression+ in Text.Pretty.Simple.pPrintNoColor denoted -- | Entry point for the @dhall@ executable main :: IO ()
src/Dhall/Normalize.hs view
@@ -33,7 +33,6 @@ , Binding(Binding) , Chunks(..) , DhallDouble(..)- , Const(..) , PreferAnnotation(..) ) @@ -335,14 +334,6 @@ App IntegerToDouble (IntegerLit n) -> pure (DoubleLit ((DhallDouble . read . show) n)) App DoubleShow (DoubleLit (DhallDouble n)) -> pure (TextLit (Chunks [] (Data.Text.pack (show n))))- App (App OptionalBuild _A₀) g ->- loop (App (App (App g optional) just) nothing)- where- optional = App Optional _A₀-- just = Lam "a" _A₀ (Some "a")-- nothing = App None _A₀ App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil) where _A₁ = shift 1 "a" _A₀@@ -403,21 +394,6 @@ ] App (App ListReverse _) (ListLit t xs) -> loop (ListLit t (Data.Sequence.reverse xs))-- App (App OptionalFold t0) x0 -> do- t1 <- loop t0- let optional = Var (V "optional" 0)- let lam term = (Lam "optional"- (Const Type)- (Lam "some"- (Pi "_" t1 optional)- (Lam "none" optional term)))- x1 <- loop x0- pure $ case x1 of- App None _ -> lam (Var (V "none" 0))- Some x' -> lam (App (Var (V "some" 0)) x')- _ -> App (App OptionalFold t1) x1- App TextShow (TextLit (Chunks [] oldText)) -> loop (TextLit (Chunks [] newText)) where@@ -550,8 +526,6 @@ where a' = loop a None -> pure None- OptionalFold -> pure OptionalFold- OptionalBuild -> pure OptionalBuild Record kts -> Record . Dhall.Map.sort <$> kts' where kts' = traverse loop kts@@ -770,7 +744,6 @@ App IntegerShow (IntegerLit _) -> False App IntegerToDouble (IntegerLit _) -> False App DoubleShow (DoubleLit _) -> False- App (App OptionalBuild _) _ -> False App (App ListBuild _) _ -> False App (App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _) _ -> False App (App ListLength _) (ListLit _ _) -> False@@ -778,8 +751,6 @@ App (App ListLast _) (ListLit _ _) -> False App (App ListIndexed _) (ListLit _ _) -> False App (App ListReverse _) (ListLit _ _) -> False- App (App OptionalFold _) (Some _) -> False- App (App OptionalFold _) (App None _) -> False App TextShow (TextLit (Chunks [] _)) -> False _ -> True@@ -873,8 +844,6 @@ Optional -> True Some a -> loop a None -> True- OptionalFold -> True- OptionalBuild -> True Record kts -> Dhall.Map.isSorted kts && all loop kts RecordLit kvs -> Dhall.Map.isSorted kvs && all loop kvs Union kts -> Dhall.Map.isSorted kts && all (all loop) kts@@ -951,3 +920,7 @@ denote' = Syntax.denote strippedExpression = denote' expression++{- $setup+>>> import Dhall.Syntax (Const(..))+-}
src/Dhall/Parser/Expression.hs view
@@ -7,16 +7,16 @@ -- | Parsing Dhall expressions. module Dhall.Parser.Expression where -import Control.Applicative (liftA2, Alternative(..), optional)-import Data.ByteArray.Encoding (Base(..))-import Data.Foldable (foldl')-import Data.Functor (void)-import Data.List.NonEmpty (NonEmpty(..))-import Data.Semigroup (Semigroup(..))-import Data.Text (Text)+import Control.Applicative (Alternative (..), liftA2, optional)+import Data.ByteArray.Encoding (Base (..))+import Data.Foldable (foldl')+import Data.Functor (void)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Semigroup (Semigroup (..))+import Data.Text (Text)+import Dhall.Src (Src (..)) import Dhall.Syntax-import Dhall.Src (Src(..))-import Prelude hiding (const, pi)+import Prelude hiding (const, pi) import Text.Parser.Combinators (choice, try, (<?>)) import qualified Control.Monad@@ -64,6 +64,14 @@ after <- getSourcePos return (Src before after tokens) +-- | Same as `src`, except also return the parsed value+srcAnd :: Parser a -> Parser (Src, a)+srcAnd parser = do+ before <- getSourcePos+ (tokens, x) <- Text.Megaparsec.match parser+ after <- getSourcePos+ return (Src before after tokens, x)+ {-| Wrap a `Parser` to still match the same text, but to wrap the resulting `Expr` in a `Note` constructor containing the `Src` span -}@@ -240,6 +248,8 @@ a <- parseFirstOperatorExpression + whitespace+ let alternative4A = do _arrow whitespace@@ -314,21 +324,24 @@ nil = (firstApplicationExpression, applicationExpression) - makeOperatorExpression firstSubExpression operatorParser subExpression =- noted (do- a <- firstSubExpression+ makeOperatorExpression firstSubExpression operatorParser subExpression = do+ a <- firstSubExpression - whitespace+ bs <- Text.Megaparsec.many $ do+ (Src _ _ textOp, op0) <- srcAnd (try (whitespace *> operatorParser)) - b <- Text.Megaparsec.many $ do- op <- operatorParser+ r0 <- subExpression - r <- subExpression+ let l@(Note (Src startL _ textL) _) `op` r@(Note (Src _ endR textR) _) =+ Note (Src startL endR (textL <> textOp <> textR)) (l `op0` r)+ -- We shouldn't hit this branch if things are working, but+ -- that is not enforced in the types+ l `op` r =+ l `op0` r - whitespace+ return (`op` r0) - return (\l -> l `op` r)- return (foldl' (\x f -> f x) a b))+ return (foldl' (\x f -> f x) a bs) operatorParsers :: [Parser (Expr s a -> Expr s a -> Expr s a)] operatorParsers =@@ -547,12 +560,7 @@ , ListReverse <$ _ListReverse , List <$ _List ]- 'O' ->- choice- [ OptionalFold <$ _OptionalFold- , OptionalBuild <$ _OptionalBuild- , Optional <$ _Optional- ]+ 'O' -> Optional <$ _Optional 'B' -> Bool <$ _Bool 'S' -> Const Sort <$ _Sort 'T' ->@@ -766,7 +774,7 @@ nonEmptyRecordTypeOrLiteral = do let nonEmptyRecordType = do- a <- try (anyLabel <* whitespace <* _colon)+ a <- try (anyLabelOrSome <* whitespace <* _colon) nonemptyWhitespace @@ -779,7 +787,7 @@ whitespace - c <- anyLabel+ c <- anyLabelOrSome whitespace @@ -798,7 +806,7 @@ return (Record m) let keysValue = do- keys <- Combinators.NonEmpty.sepBy1 anyLabel (try (whitespace *> _dot) *> whitespace)+ keys <- Combinators.NonEmpty.sepBy1 anyLabelOrSome (try (whitespace *> _dot) *> whitespace) let normalRecordEntry = do try (whitespace *> _equal)@@ -844,7 +852,7 @@ _ <- optional (_bar *> whitespace) let unionTypeEntry = do- a <- anyLabel+ a <- anyLabelOrSome whitespace b <- optional (_colon *> nonemptyWhitespace *> expression <* whitespace) return (a, b)
src/Dhall/Parser/Token.hs view
@@ -14,6 +14,7 @@ char, file_, label,+ anyLabelOrSome, anyLabel, labels, httpRaw,@@ -57,8 +58,6 @@ _ListLast, _ListIndexed, _ListReverse,- _OptionalFold,- _OptionalBuild, _Bool, _Natural, _Integer,@@ -108,16 +107,16 @@ _with, ) where -import Dhall.Parser.Combinators+import Dhall.Parser.Combinators -import Control.Applicative (Alternative(..), optional)-import Data.Bits ((.&.))-import Data.Functor (void, ($>))-import Data.Semigroup (Semigroup(..))-import Data.Text (Text)+import Control.Applicative (Alternative (..), optional)+import Data.Bits ((.&.))+import Data.Functor (void, ($>))+import Data.Semigroup (Semigroup (..))+import Data.Text (Text)+import Dhall.Set (Set) import Dhall.Syntax-import Dhall.Set (Set)-import Prelude hiding (const, pi)+import Prelude hiding (const, pi) import Text.Parser.Combinators (choice, try, (<?>)) import qualified Control.Monad@@ -129,15 +128,14 @@ import qualified Data.Scientific as Scientific import qualified Data.Text import qualified Dhall.Set-import qualified Network.URI.Encode as URI.Encode import qualified Text.Megaparsec import qualified Text.Megaparsec.Char.Lexer import qualified Text.Parser.Char-import qualified Text.Parser.Token import qualified Text.Parser.Combinators+import qualified Text.Parser.Token import Numeric.Natural (Natural)-import Prelude hiding (const, pi)+import Prelude hiding (const, pi) -- | Returns `True` if the given `Int` is a valid Unicode codepoint validCodepoint :: Int -> Bool@@ -407,13 +405,14 @@ blockCommentContinue simpleLabel :: Bool -> Parser Text-simpleLabel allowReserved = try (do+simpleLabel allowReserved = try $ do c <- Text.Parser.Char.satisfy headCharacter rest <- Dhall.Parser.Combinators.takeWhile tailCharacter let t = Data.Text.cons c rest- Control.Monad.guard (allowReserved || not (Data.HashSet.member t reservedIdentifiers))- return t )- where+ let isNotAKeyword = not $ t `Data.HashSet.member` reservedKeywords+ let isNotAReservedIdentifier = not $ t `Data.HashSet.member` reservedIdentifiers+ Control.Monad.guard (isNotAKeyword && (allowReserved || isNotAReservedIdentifier))+ return t headCharacter :: Char -> Bool headCharacter c = alpha c || c == '_'@@ -424,7 +423,7 @@ backtickLabel :: Parser Text backtickLabel = do _ <- char '`'- t <- takeWhile1 predicate+ t <- Dhall.Parser.Combinators.takeWhile predicate _ <- char '`' return t where@@ -449,9 +448,9 @@ emptyLabels = pure Dhall.Set.empty nonEmptyLabels = do- x <- anyLabel+ x <- anyLabelOrSome whitespace- xs <- many (do _comma; whitespace; l <- anyLabel; whitespace; return l)+ xs <- many (do _comma; whitespace; l <- anyLabelOrSome; whitespace; return l) noDuplicates (x : xs) {-| Parse a label (e.g. a variable\/field\/alternative name)@@ -472,6 +471,14 @@ t <- backtickLabel <|> simpleLabel True return t ) <?> "any label" +{-| Same as `anyLabel` except that `Some` is allowed++ This corresponds to the @any-label-or-some@ rule in the official grammar+-}++anyLabelOrSome :: Parser Text+anyLabelOrSome = try anyLabel <|> ("Some" <$ _Some)+ {-| Parse a valid Bash environment variable name This corresponds to the @bash-environment-variable@ rule in the official@@ -547,14 +554,11 @@ _ <- char '"' t <- Text.Megaparsec.takeWhile1P Nothing quotedPathCharacter _ <- char '"'-- case componentType of- FileComponent -> do- return t- URLComponent -> do- return (URI.Encode.encodeText t)+ return t - quotedPathData <|> pathData+ case componentType of+ FileComponent -> quotedPathData <|> pathData+ URLComponent -> pathData -- | Parse a `File` file_ :: ComponentType -> Parser File@@ -987,20 +991,6 @@ -} _ListReverse :: Parser () _ListReverse = builtin "List/reverse"--{-| Parse the @Optional/fold@ built-in-- This corresponds to the @Optional-fold@ rule from the official grammar--}-_OptionalFold :: Parser ()-_OptionalFold = builtin "Optional/fold"--{-| Parse the @Optional/build@ built-in-- This corresponds to the @Optional-build@ rule from the official grammar--}-_OptionalBuild :: Parser ()-_OptionalBuild = builtin "Optional/build" {-| Parse the @Bool@ built-in
src/Dhall/Pretty/Internal.hs view
@@ -64,28 +64,28 @@ ) where import Data.Foldable-import Data.List.NonEmpty (NonEmpty(..))-import Data.Monoid ((<>))-import Data.Text (Text)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Monoid ((<>))+import Data.Text (Text) import Data.Text.Prettyprint.Doc (Doc, Pretty, space)-import Dhall.Map (Map)-import Dhall.Set (Set)-import Dhall.Src (Src(..))+import Dhall.Map (Map)+import Dhall.Set (Set)+import Dhall.Src (Src (..)) import Dhall.Syntax-import Numeric.Natural (Natural)-import Prelude hiding (succ)-import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Terminal+import Numeric.Natural (Natural)+import Prelude hiding (succ) import qualified Data.Char import qualified Data.HashSet import qualified Data.List-import qualified Data.List.NonEmpty as NonEmpty+import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Set-import qualified Data.Text as Text-import qualified Data.Text.Prettyprint.Doc as Pretty-import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty-import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty-import qualified Dhall.Map as Map+import qualified Data.Text as Text+import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Terminal+import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty+import qualified Dhall.Map as Map import qualified Dhall.Set {-| Annotation type used to tag elements in a pretty-printed document for@@ -439,9 +439,12 @@ escapeLabel allowReserved l = case Text.uncons l of Just (h, t)- | headCharacter h && Text.all tailCharacter t && (allowReserved || not (Data.HashSet.member l reservedIdentifiers))+ | headCharacter h && Text.all tailCharacter t && (notReservedIdentifier || (allowReserved && someOrNotLanguageKeyword)) -> l _ -> "`" <> l <> "`"+ where+ notReservedIdentifier = not (Data.HashSet.member l reservedIdentifiers)+ someOrNotLanguageKeyword = l == "Some" || not (Data.HashSet.member l reservedKeywords) prettyLabelShared :: Bool -> Text -> Doc Ann prettyLabelShared b l = label (Pretty.pretty (escapeLabel b l))@@ -1202,10 +1205,6 @@ builtin "Optional" prettyPrimitiveExpression None = builtin "None"- prettyPrimitiveExpression OptionalFold =- builtin "Optional/fold"- prettyPrimitiveExpression OptionalBuild =- builtin "Optional/build" prettyPrimitiveExpression (BoolLit True) = builtin "True" prettyPrimitiveExpression (BoolLit False) =
src/Dhall/Syntax.hs view
@@ -60,6 +60,7 @@ -- * Reserved identifiers , reservedIdentifiers+ , reservedKeywords -- * `Text` manipulation , toDoubleQuoted@@ -74,41 +75,44 @@ , internalError ) where -import Control.DeepSeq (NFData)-import Data.Bifunctor (Bifunctor(..))-import Data.Bits (xor)-import Data.Data (Data)+import Control.DeepSeq (NFData)+import Data.Bifunctor (Bifunctor (..))+import Data.Bits (xor)+import Data.Data (Data) import Data.Foldable-import Data.HashSet (HashSet)-import Data.List.NonEmpty (NonEmpty(..))-import Data.String (IsString(..))-import Data.Semigroup (Semigroup(..))-import Data.Sequence (Seq)-import Data.Text (Text)-import Data.Text.Prettyprint.Doc (Doc, Pretty)+import Data.HashSet (HashSet)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Semigroup (Semigroup (..))+import Data.Sequence (Seq)+import Data.String (IsString (..))+import Data.Text (Text)+import Data.Text.Prettyprint.Doc (Doc, Pretty) import Data.Traversable-import Data.Void (Void)-import Dhall.Map (Map)-import Dhall.Set (Set)-import Dhall.Src (Src(..))+import Data.Void (Void)+import Dhall.Map (Map) import {-# SOURCE #-} Dhall.Pretty.Internal-import GHC.Generics (Generic)-import Instances.TH.Lift ()+import Dhall.Set (Set)+import Dhall.Src (Src (..))+import GHC.Generics (Generic)+import Instances.TH.Lift () import Language.Haskell.TH.Syntax (Lift)-import Numeric.Natural (Natural)-import Prelude hiding (succ)-import Unsafe.Coerce (unsafeCoerce)+import Numeric.Natural (Natural)+import Prelude hiding (succ)+import Unsafe.Coerce (unsafeCoerce) import qualified Control.Monad import qualified Data.HashSet-import qualified Data.List.NonEmpty as NonEmpty+import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Text-import qualified Data.Text.Prettyprint.Doc as Pretty+import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Dhall.Crypto-import qualified Dhall.Optics as Optics-import qualified Lens.Family as Lens-import qualified Network.URI as URI+import qualified Dhall.Optics as Optics+import qualified Lens.Family as Lens+import qualified Network.URI as URI +-- $setup+-- >>> import Dhall.Binary () -- For the orphan instance for `Serialise (Expr Void Import)`+ {-| Constants for a pure type system The axioms are:@@ -178,7 +182,9 @@ {- | Record the binding part of a @let@ expression. For example,+ > let {- A -} x {- B -} : {- C -} Bool = {- D -} True in x+ will be instantiated as follows: * @bindingSrc0@ corresponds to the @A@ comment.@@ -427,10 +433,6 @@ | Some (Expr s a) -- | > None ~ None | None- -- | > 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 }@@ -657,8 +659,6 @@ unsafeSubExpressions _ Optional = pure Optional unsafeSubExpressions f (Some a) = Some <$> f a unsafeSubExpressions _ None = pure None-unsafeSubExpressions _ OptionalFold = pure OptionalFold-unsafeSubExpressions _ OptionalBuild = pure OptionalBuild unsafeSubExpressions f (Record a) = Record <$> traverse f a unsafeSubExpressions f ( RecordLit a ) = RecordLit <$> traverse f a unsafeSubExpressions f (Union a) = Union <$> traverse (traverse f) a@@ -948,11 +948,11 @@ shallowDenote (Note _ e) = shallowDenote e shallowDenote e = e --- | The set of reserved identifiers for the Dhall language-reservedIdentifiers :: HashSet Text-reservedIdentifiers =+-- | The set of reserved keywords according to the `keyword` rule in the grammar+reservedKeywords :: HashSet Text+reservedKeywords = Data.HashSet.fromList- [ -- Keywords according to the `keyword` rule in the grammar+ [ "if" , "then" , "else"@@ -969,9 +969,15 @@ , "assert" , "forall" , "with"+ ] - -- Builtins according to the `builtin` rule in the grammar- , "Natural/fold"+-- | The set of reserved identifiers for the Dhall language+-- | Contains also all keywords from "reservedKeywords"+reservedIdentifiers :: HashSet Text+reservedIdentifiers = reservedKeywords <>+ Data.HashSet.fromList+ [ -- Builtins according to the `builtin` rule in the grammar+ "Natural/fold" , "Natural/build" , "Natural/isZero" , "Natural/even"@@ -994,8 +1000,6 @@ , "List/last" , "List/indexed" , "List/reverse"- , "Optional/fold"- , "Optional/build" , "Text/show" , "Bool" , "True"
src/Dhall/Tutorial.hs view
@@ -80,6 +80,9 @@ -- * Prelude -- $prelude + -- * Limitations+ -- $limitations+ -- * Conclusion -- $conclusion @@ -125,6 +128,8 @@ -- > x <- input auto "./config.dhall" -- > print (x :: Example) -- +-- __WARNING__: You must not instantiate FromDhall with a recursive type. See [Limitations](#limitations).+-- -- If you compile and run the above example, the program prints the corresponding -- Haskell record: -- @@ -2241,6 +2246,35 @@ -- __Exercise__: Browse the Prelude by running: -- -- > $ dhall <<< 'https://prelude.dhall-lang.org/package.dhall'++-- $limitations+-- #limitations#+--+-- `FromDhall` has a limitiation: It won't work for recursive types.+-- If you instantiate these using their Generic instance you end up with one of+-- the following two cases:+-- +-- If the type appears in it's own definition like+--+-- > data Foo = Foo Foo+-- > deriving Generic+-- >+-- > instance FromDhall Foo+--+-- the resulting Decoder will throw an exception /ON USAGE/.+-- However, if the recursion is indirect like+--+-- > data Foo = Foo Bar+-- > deriving Generic+-- >+-- > instance FromDhall Foo+-- >+-- > data Bar = Bar Foo+-- > deriving Generic+-- >+-- > instance FromDhall Bar+--+-- the resulting Decoder will __NOT TERMINATE__ /ON USAGE/. -- $conclusion --
src/Dhall/TypeCheck.hs view
@@ -725,34 +725,6 @@ return (VOptional _A') - OptionalFold -> do- return- ( VHPi "a" (VConst Type) (\a ->- VOptional a- ~> VHPi "optional" (VConst Type) (\optional ->- VHPi "just" (a ~> optional) (\_just ->- VHPi "nothing" optional (\_nothing ->- optional- )- )- )- )- )-- OptionalBuild -> do- return- ( VHPi "a" (VConst Type) (\a ->- VHPi "optional" (VConst Type) (\optional ->- VHPi "just" (a ~> optional) (\_just ->- VHPi "nothing" optional (\_nothing ->- optional- )- )- )- ~> VOptional a- )- )- Record xTs -> do let process x _T = do tT' <- lift (loop ctx _T)
src/Dhall/Util.hs view
@@ -181,6 +181,7 @@ -- | Convenient utility for retrieving an expression along with its header from -- | text already read from STDIN (so it's not re-read)-getExpressionAndHeaderFromStdinText :: Censor -> Text -> IO (Header, Expr Src Import)+getExpressionAndHeaderFromStdinText+ :: Censor -> Text -> IO (Header, Expr Src Import) getExpressionAndHeaderFromStdinText censor = get Dhall.Parser.exprAndHeaderFromText censor . StdinText
tests/Dhall/Test/Dhall.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-}@@ -18,6 +19,7 @@ import Control.Exception (SomeException, try) import Data.Fix (Fix(..))+import Data.Maybe (isJust) import Data.List.NonEmpty (NonEmpty (..)) import Data.Sequence (Seq) import Data.Scientific (Scientific)@@ -28,6 +30,7 @@ import Dhall.Core (Expr(..)) import GHC.Generics (Generic, Rep) import Numeric.Natural (Natural)+import System.Timeout (timeout) import Test.Tasty import Test.Tasty.HUnit @@ -61,8 +64,8 @@ data MyType = MyType { foo :: String , bar :: Natural } wrongDhallType :: Dhall.Decoder MyType-wrongDhallType = Dhall.Decoder { .. }- where expected =+wrongDhallType = Dhall.Decoder {..}+ where expected = pure $ Dhall.Core.Record ( Dhall.Map.fromList [ ( "bar", Dhall.Core.Natural)@@ -119,6 +122,11 @@ Dhall.embed exampleEncoder () @=? Field (Union (Dhall.Map.singleton "A" Nothing)) "A" +data RecursiveType a = RecursiveType (RecursiveType a)+ deriving Generic++instance FromDhall (RecursiveType a)+ shouldHaveWorkingRecursiveFromDhall :: TestTree shouldHaveWorkingRecursiveFromDhall = testGroup "recursive FromDhall instance" [ testCase "works for a recursive expression" $ do@@ -129,6 +137,16 @@ actual <- Dhall.input Dhall.auto "./tests/recursive/expr1.dhall" expected @=? actual+ , testCase "terminate if type is recursive (monomorphic)" $ do+ actual <- timeout (1 * 1000000) $ do+ !typ <- return $ Dhall.expected (Dhall.auto :: Dhall.Decoder (RecursiveType Void))+ return typ+ assertBool "Does not terminate!" $ isJust actual+ , testCase "terminate if type is recursive (polymorphic)" $ do+ actual <- timeout (1 * 1000000) $ do+ !typ <- return $ Dhall.expected (Dhall.auto :: Dhall.Decoder (RecursiveType a))+ return typ+ assertBool "Does not terminate!" $ isJust actual ] where expected =@@ -318,7 +336,7 @@ :: ( Generic a , Dhall.GenericToDhall (Rep a) , Generic b- , Dhall.GenericFromDhall (Rep b)+ , Dhall.GenericFromDhall b (Rep b) ) => Dhall.InterpretOptions -> Dhall.Decoder (a -> b) functionWithOptions options =@@ -454,9 +472,10 @@ let assertMsg = "The exception message did not match the expected output" case inputEx of- Left (Dhall.ExtractErrors errs) -> case errs of+ Left (Dhall.DhallErrors errs) -> case errs of (err :| []) -> case err of Dhall.TypeMismatch {} -> fail "The extraction using an invalid decoder failed with a type mismatch"+ Dhall.ExpectedTypeError _ -> fail "An error occured while determining the expected Dhall type" Dhall.ExtractError extractError -> assertEqual assertMsg expectedMsg extractError _ -> fail "The extraction using an invalid decoder failed with multiple errors" Right _ -> fail "The extraction using an invalid decoder succeeded"
tests/Dhall/Test/Import.hs view
@@ -3,13 +3,13 @@ module Dhall.Test.Import where import Control.Exception (SomeException)-import Data.Monoid ((<>))-import Data.Text (Text)-import Dhall.Import (MissingImports(..))-import Dhall.Parser (SourcedException(..))-import Prelude hiding (FilePath)-import Test.Tasty (TestTree)-import Turtle (FilePath, (</>))+import Data.Monoid ((<>))+import Data.Text (Text)+import Dhall.Import (MissingImports (..))+import Dhall.Parser (SourcedException (..))+import Prelude hiding (FilePath)+import Test.Tasty (TestTree)+import Turtle (FilePath, (</>)) import qualified Control.Exception as Exception import qualified Control.Monad as Monad@@ -62,9 +62,7 @@ let directoryString = FilePath.takeDirectory pathString - let expectedFailures =- [ importDirectory </> "success/unit/asLocation/HashA.dhall"- ]+ let expectedFailures = [] Test.Util.testCase path expectedFailures (do @@ -72,22 +70,32 @@ actualExpr <- Core.throws (Parser.exprFromText mempty text) - let setCache =- Turtle.export "XDG_CACHE_HOME" "dhall-lang/tests/import/cache"+ let originalCache = "dhall-lang/tests/import/cache" + let setCache = Turtle.export "XDG_CACHE_HOME"+ let unsetCache = Turtle.unset "XDG_CACHE_HOME" let load = State.evalStateT (Test.Util.loadWith actualExpr) (Import.emptyStatus directoryString) - let runTest = do- if Turtle.filename (Turtle.fromText path) `elem`- [ "hashFromCacheA.dhall"- , "unit/asLocation/HashA.dhall"- ]- then do- setCache- _ <- load+ let usesCache = [ "hashFromCacheA.dhall"+ , "unit/asLocation/HashA.dhall"+ , "unit/IgnorePoisonedCacheA.dhall"]++ let endsIn path' = not $ null $ Turtle.match (Turtle.ends path') path++ let buildNewCache = do+ tempdir <- Turtle.mktempdir "/tmp" "dhall-cache"+ Turtle.liftIO $ Turtle.cptree originalCache tempdir+ return tempdir++ let runTest =+ if any endsIn usesCache+ then Turtle.runManaged $ do+ cacheDir <- buildNewCache+ setCache $ Turtle.format Turtle.fp cacheDir+ _ <- Turtle.liftIO load unsetCache else do _ <- load
tests/Dhall/Test/QuickCheck.hs view
@@ -54,6 +54,7 @@ import Text.Megaparsec (SourcePos(..), Pos) import qualified Control.Spoon+import qualified Data.Foldable as Foldable import qualified Data.List import qualified Data.Sequence import qualified Data.SpecialValues@@ -71,6 +72,7 @@ import qualified Dhall.Set import qualified Dhall.TypeCheck import qualified Generic.Random+import qualified Lens.Family as Lens import qualified Numeric.Natural as Nat import qualified Test.QuickCheck import qualified Test.Tasty@@ -307,8 +309,6 @@ % (1 :: W "Optional") % (7 :: W "Some") % (1 :: W "None")- % (1 :: W "OptionalFold")- % (1 :: W "OptionalBuild") % (1 :: W "Record") % (7 :: W "RecordLit") % (1 :: W "Union")@@ -494,6 +494,18 @@ filterOutEmbeds :: Typer a filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression. +noDoubleNotes :: Expr () Import -> Property+noDoubleNotes expression =+ length+ [ ()+ | e <- Foldable.toList parsedExpression+ , Note _ (Note _ _) <- Lens.toListOf Dhall.Core.subExpressions e+ ] === 0+ where+ text = Dhall.Core.pretty expression++ parsedExpression = Parser.exprFromText "" text+ embedThenExtractIsIdentity :: forall a. (ToDhall a, FromDhall a, Eq a, Typeable a, Arbitrary a, Show a) => Proxy a@@ -546,6 +558,10 @@ , ( "Normalizing an expression doesn't change its inferred type" , Test.QuickCheck.property normalizingAnExpressionDoesntChangeItsInferredType , adjustQuickCheckTests 10000+ )+ , ( "Parsing an expression doesn't generated doubly-nested Note constructors"+ , Test.QuickCheck.property noDoubleNotes+ , adjustQuickCheckTests 100 ) , embedThenExtractIsIdentity (Proxy :: Proxy (Text.Text)) , embedThenExtractIsIdentity (Proxy :: Proxy [Nat.Natural])
tests/Dhall/Test/Regression.hs view
@@ -22,6 +22,7 @@ import qualified Test.Tasty import qualified Test.Tasty.HUnit +import Data.Either.Validation (Validation(..)) import Data.Void (Void) import Dhall.Import (Imported, MissingImports(..)) import Dhall.Parser (Src, SourcedException(..))@@ -60,7 +61,7 @@ unnamedFields = Test.Tasty.HUnit.testCase "Unnamed Fields" (do let ty = Dhall.auto :: Dhall.Decoder Foo Test.Tasty.HUnit.assertEqual "Good type" (Dhall.expected ty)- (Dhall.Core.Union+ (Success (Dhall.Core.Union (Dhall.Map.fromList [ ("Foo",Just (Dhall.Core.Record (Dhall.Map.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool)])))@@ -70,17 +71,17 @@ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Integer)]))) ] )- )+ )) let inj = Dhall.inject :: Dhall.Encoder Foo- Test.Tasty.HUnit.assertEqual "Good ToDhall" (Dhall.declared inj) (Dhall.expected ty)+ Test.Tasty.HUnit.assertEqual "Good ToDhall" (Success $ Dhall.declared inj) (Dhall.expected ty) let tu_ty = Dhall.auto :: Dhall.Decoder (Integer, Bool)- Test.Tasty.HUnit.assertEqual "Auto Tuple" (Dhall.expected tu_ty) (Dhall.Core.Record (+ Test.Tasty.HUnit.assertEqual "Auto Tuple" (Dhall.expected tu_ty) (Success $ Dhall.Core.Record ( Dhall.Map.fromList [ ("_1",Dhall.Core.Integer),("_2",Dhall.Core.Bool) ])) let tu_in = Dhall.inject :: Dhall.Encoder (Integer, Bool)- Test.Tasty.HUnit.assertEqual "Inj. Tuple" (Dhall.declared tu_in) (Dhall.expected tu_ty)+ Test.Tasty.HUnit.assertEqual "Inj. Tuple" (Success $ Dhall.declared tu_in) (Dhall.expected tu_ty) return () )
tests/Dhall/Test/Substitution.hs view
@@ -3,10 +3,12 @@ module Dhall.Test.Substitution where +import Control.Exception (throwIO) import Data.Void (Void) import Dhall.Core (Expr(BoolLit, Var)) import Dhall.Src (Src) +import qualified Data.Either.Validation import qualified Dhall import qualified Dhall.Map import qualified Lens.Family as Lens@@ -17,15 +19,18 @@ instance Dhall.FromDhall Result substituteResult :: FilePath -> IO Result-substituteResult fp = let- evaluateSettings = Lens.over Dhall.substitutions (Dhall.Map.insert "Result" resultType) Dhall.defaultEvaluateSettings- in Dhall.inputFileWithSettings evaluateSettings resultDecoder fp+substituteResult fp = do+ rt <- resultType+ let evaluateSettings = Lens.over Dhall.substitutions (Dhall.Map.insert "Result" rt) Dhall.defaultEvaluateSettings+ Dhall.inputFileWithSettings evaluateSettings resultDecoder fp resultDecoder :: Dhall.Decoder Result resultDecoder = Dhall.auto -resultType :: Expr Src Void-resultType = Dhall.expected resultDecoder+resultType :: IO (Expr Src Void)+resultType = case Dhall.expected resultDecoder of+ Data.Either.Validation.Failure e -> throwIO e+ Data.Either.Validation.Success x -> return x substituteFoo :: FilePath -> IO Bool substituteFoo fp = let
tests/Dhall/Test/TypeInference.hs view
@@ -11,6 +11,7 @@ import Turtle (FilePath, (</>)) import qualified Control.Exception as Exception+import qualified Control.Monad as Monad import qualified Data.Text as Text import qualified Data.Text.IO as Text.IO import qualified Dhall.Core as Core@@ -28,8 +29,19 @@ getTests :: IO TestTree getTests = do- let successTestFiles = Turtle.lstree (typeInferenceDirectory </> "success")+ let successTestFiles = do+ path <- Turtle.lstree (typeInferenceDirectory </> "success") + let skip =+ -- This test intermittently fails with:+ -- "Error: Remote host not found"+ [ typeInferenceDirectory </> "success/CacheImportsCanonicalize"+ ]++ Monad.guard (path `notElem` skip)++ return path+ successTests <- Test.Util.discover (Turtle.chars <* "A.dhall") successTest successTestFiles let failureTestFiles = Turtle.lstree (typeInferenceDirectory </> "failure")@@ -47,11 +59,9 @@ successTest prefix = do let expectedFailures = []- #ifdef WITH_HTTP #else ++ [ typeInferenceDirectory </> "success/CacheImports"- , typeInferenceDirectory </> "success/CacheImportsCanonicalize" ] #endif
tests/format/applicationMultilineA.dhall view
@@ -18,7 +18,7 @@ , someList = Some [ aaaaaaaaaaaaaaaaaaaaaaaaaa, bbbbbbbbbbbbbbbbbbbb, cccccccccccccccccccccccc, dddddddddddddd ]-, merge =+, merge1 = merge aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb@@ -27,7 +27,7 @@ a b ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc-, toMap =+, toMap1 = toMap aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa }
tests/format/applicationMultilineB.dhall view
@@ -20,7 +20,7 @@ , cccccccccccccccccccccccc , dddddddddddddd ]-, merge =+, merge1 = merge aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb@@ -29,6 +29,6 @@ a b ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc-, toMap = toMap+, toMap1 = toMap aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa }
+ tests/format/issue1805KeywordRecordFieldShouldBeQuotedA.dhall view
@@ -0,0 +1,1 @@+{ `if` = True }
+ tests/format/issue1805KeywordRecordFieldShouldBeQuotedB.dhall view
@@ -0,0 +1,1 @@+{ `if` = True }
+ tests/format/issue1805SomeQuotedInLetButNotInRecordA.dhall view
@@ -0,0 +1,1 @@+let `Some` = 3 in { `if` = True, Some = 333 }
+ tests/format/issue1805SomeQuotedInLetButNotInRecordB.dhall view
@@ -0,0 +1,1 @@+let `Some` = 3 in { `if` = True, Some = 333 }
tests/format/urlsA.dhall view
@@ -4,10 +4,4 @@ let reserved = http://x/y:z -let quoted = http://x/"y:z"--let quotedPercent = http://x/"y%z"--let snowman = http://x/"y☃z"- in "done"
tests/format/urlsB.dhall view
@@ -4,10 +4,4 @@ let reserved = http://x/y:z -let quoted = http://x/y%3Az--let quotedPercent = http://x/y%25z--let snowman = http://x/y%E2%98%83z- in "done"
− tests/lint/success/optionalFoldBuildA.dhall
@@ -1,4 +0,0 @@-{ example0 = Optional/fold-, example1 = Optional/build-, example2 = Optional/fold Natural (Some 1) Bool Natural/even False-}
− tests/lint/success/optionalFoldBuildB.dhall
@@ -1,18 +0,0 @@-{ example0 =- λ(a : Type) →- λ(o : Optional a) →- λ(optional : Type) →- λ(some : a → optional) →- λ(none : optional) →- merge { Some = some, None = none } o-, example1 =- λ(a : Type) →- λ ( build- : ∀(optional : Type) →- ∀(some : a → optional) →- ∀(none : optional) →- optional- ) →- build (Optional a) (λ(x : a) → Some x) (None a)-, example2 = merge { Some = Natural/even, None = False } (Some 1)-}