-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A configuration language guaranteed to terminate
--
-- Dhall is an explicitly typed configuration language that is not Turing
-- complete. Despite being Turing incomplete, Dhall is a real programming
-- language with a type-checker and evaluator.
--
-- Use this library to parse, type-check, evaluate, and pretty-print the
-- Dhall configuration language. This package also includes an executable
-- which type-checks a Dhall file and reduces the file to a fully
-- evaluated normal form.
--
-- Read Dhall.Tutorial to learn how to use this library
@package dhall
@version 1.26.0
-- | This is a utility module that consolidates all Context-related
-- operations
module Dhall.Context
-- | A (Context a) associates Text labels with values of
-- type a. Each Text label can correspond to multiple
-- values of type a
--
-- The Context is used for type-checking when (a = Expr
-- X)
--
--
--
-- The difference between a Context and a Map is that a
-- Context lets you have multiple ordered occurrences of the same
-- key and you can query for the nth occurrence of a given key.
data Context a
-- | An empty context with no key-value pairs
empty :: Context a
-- | Add a key-value pair to the Context
insert :: Text -> a -> Context a -> Context a
-- | "Pattern match" on a Context
--
--
-- match (insert k v ctx) = Just (k, v, ctx)
-- match empty = Nothing
--
match :: Context a -> Maybe (Text, a, Context a)
-- | Look up a key by name and index
--
--
-- lookup _ _ empty = Nothing
-- lookup k 0 (insert k v c) = Just v
-- lookup k n (insert k v c) = lookup k (n - 1) c
-- lookup k n (insert j v c) = lookup k n c -- k /= j
--
lookup :: Text -> Int -> Context a -> Maybe a
-- | Return all key-value associations as a list
--
--
-- toList empty = []
-- toList (insert k v ctx) = (k, v) : toList ctx
--
toList :: Context a -> [(Text, a)]
instance GHC.Base.Functor Dhall.Context.Context
-- | Map type used to represent records and unions
module Dhall.Map
-- | A Map that remembers the original ordering of keys
--
-- This is primarily used so that formatting preserves field order
--
-- This is done primarily to avoid a dependency on
-- insert-ordered-containers and also to improve performance
data Map k v
-- | Create a Map from a single key-value pair
--
--
-- >>> singleton "A" 1
-- fromList [("A",1)]
--
singleton :: k -> v -> Map k v
-- | Create a Map from a list of key-value pairs
--
--
-- >>> fromList [("B",1),("A",2)] -- The map preserves order
-- fromList [("B",1),("A",2)]
--
-- >>> fromList [("A",1),("A",2)] -- For duplicates, later values take precedence
-- fromList [("A",2)]
--
--
-- Note that this handling of duplicates means that fromList is
-- not a monoid homomorphism:
--
--
-- >>> fromList [(1, True)] <> fromList [(1, False)]
-- fromList [(1,True)]
--
-- >>> fromList ([(1, True)] <> [(1, False)])
-- fromList [(1,False)]
--
fromList :: Ord k => [(k, v)] -> Map k v
-- | Create a Map from a list of key-value pairs with a combining
-- function.
--
--
-- >>> fromListWithKey (\k v1 v2 -> k ++ v1 ++ v2) [("B","v1"),("A","v2"),("B","v3")]
-- fromList [("B","Bv3v1"),("A","v2")]
--
fromListWithKey :: Ord k => (k -> v -> v -> v) -> [(k, v)] -> Map k v
-- | Create a Map from a single key-value pair.
--
-- Any further operations on this map will not retain the order of the
-- keys.
--
--
-- >>> unorderedSingleton "A" 1
-- fromList [("A",1)]
--
unorderedSingleton :: k -> v -> Map k v
-- | Create a Map from a list of key-value pairs
--
-- Any further operations on this map will not retain the order of the
-- keys.
--
--
-- >>> unorderedFromList []
-- fromList []
--
-- >>> unorderedFromList [("B",1),("A",2)] -- The map /doesn't/ preserve order
-- fromList [("A",2),("B",1)]
--
-- >>> unorderedFromList [("A",1),("A",2)] -- For duplicates, later values take precedence
-- fromList [("A",2)]
--
unorderedFromList :: Ord k => [(k, v)] -> Map k v
-- | Sort the keys of a Map, forgetting the original ordering
--
--
-- sort (sort x) = sort x
--
--
--
-- >>> sort (fromList [("B",1),("A",2)])
-- fromList [("A",2),("B",1)]
--
sort :: Map k v -> Map k v
-- | Check if the keys of a Map are already sorted
--
--
-- isSorted (sort m) = True
--
--
--
-- >>> isSorted (fromList [("B",1),("A",2)]) -- Sortedness is based only on keys
-- False
--
-- >>> isSorted (fromList [("A",2),("B",1)])
-- True
--
isSorted :: Eq k => Map k v -> Bool
-- | Insert a key-value pair into a Map, overriding any previous
-- value stored underneath the same key, if present
--
--
-- insert = insertWith (\v _ -> v)
--
--
--
-- >>> insert "C" 1 (fromList [("B",2),("A",3)]) -- Values are inserted on left
-- fromList [("C",1),("B",2),("A",3)]
--
-- >>> insert "C" 1 (fromList [("C",2),("A",3)]) -- New value takes precedence
-- fromList [("C",1),("A",3)]
--
insert :: Ord k => k -> v -> Map k v -> Map k v
-- | Insert a key-value pair into a Map, using the supplied function
-- to combine the new value with any old value underneath the same key,
-- if present
--
--
-- >>> insertWith (+) "C" 1 (fromList [("B",2),("A",3)]) -- No collision
-- fromList [("C",1),("B",2),("A",3)]
--
-- >>> insertWith (+) "C" 1 (fromList [("C",2),("A",3)]) -- Collision
-- fromList [("C",3),("A",3)]
--
insertWith :: Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v
-- | Delete a key from a Map if present, otherwise return the
-- original Map
--
--
-- >>> delete "B" (fromList [("C",1),("B",2),("A",3)])
-- fromList [("C",1),("A",3)]
--
-- >>> delete "D" (fromList [("C",1),("B",2),("A",3)])
-- fromList [("C",1),("B",2),("A",3)]
--
delete :: Ord k => k -> Map k v -> Map k v
-- | Keep all values that satisfy the given predicate
--
--
-- >>> filter even (fromList [("C",3),("B",2),("A",1)])
-- fromList [("B",2)]
--
-- >>> filter odd (fromList [("C",3),("B",2),("A",1)])
-- fromList [("C",3),("A",1)]
--
filter :: Ord k => (a -> Bool) -> Map k a -> Map k a
-- | Restrict a Map to only those keys found in a
-- Data.Set.Set.
--
--
-- >>> restrictKeys (fromList [("A",1),("B",2)]) (Data.Set.fromList ["A"])
-- fromList [("A",1)]
--
restrictKeys :: Ord k => Map k a -> Set k -> Map k a
-- | Transform all values in a Map using the supplied function,
-- deleting the key if the function returns Nothing
--
--
-- >>> mapMaybe Data.Maybe.listToMaybe (fromList [("C",[1]),("B",[]),("A",[3])])
-- fromList [("C",1),("A",3)]
--
mapMaybe :: Ord k => (a -> Maybe b) -> Map k a -> Map k b
-- | Retrieve a key from a Map
--
--
-- lookup k mempty = empty
--
-- lookup k (x <> y) = lookup k y <|> lookup k x
--
--
--
-- >>> lookup "A" (fromList [("B",1),("A",2)])
-- Just 2
--
-- >>> lookup "C" (fromList [("B",1),("A",2)])
-- Nothing
--
lookup :: Ord k => k -> Map k v -> Maybe v
-- | Check if a key belongs to a Map
--
--
-- member k mempty = False
--
-- member k (x <> y) = member k x || member k y
--
--
--
-- >>> member "A" (fromList [("B",1),("A",2)])
-- True
--
-- >>> member "C" (fromList [("B",1),("A",2)])
-- False
--
member :: Ord k => k -> Map k v -> Bool
-- | Retrieve the first key, value of the Map, if present, and also
-- returning the rest of the Map.
--
--
-- uncons mempty = empty
--
-- uncons (singleton k v) = (k, v, mempty)
--
--
--
-- >>> uncons (fromList [("C",1),("B",2),("A",3)])
-- Just ("C",1,fromList [("B",2),("A",3)])
--
-- >>> uncons (fromList [])
-- Nothing
--
uncons :: Ord k => Map k v -> Maybe (k, v, Map k v)
-- |
-- >>> size (fromList [("A",1)])
-- 1
--
size :: Map k v -> Int
-- | Combine two Maps, preferring keys from the first Map
--
--
-- union = unionWith (\v _ -> v)
--
--
--
-- >>> union (fromList [("D",1),("C",2)]) (fromList [("B",3),("A",4)])
-- fromList [("D",1),("C",2),("B",3),("A",4)]
--
-- >>> union (fromList [("D",1),("C",2)]) (fromList [("C",3),("A",4)])
-- fromList [("D",1),("C",2),("A",4)]
--
union :: Ord k => Map k v -> Map k v -> Map k v
-- | Combine two Maps using a combining function for colliding keys
--
--
-- >>> unionWith (+) (fromList [("D",1),("C",2)]) (fromList [("B",3),("A",4)])
-- fromList [("D",1),("C",2),("B",3),("A",4)]
--
-- >>> unionWith (+) (fromList [("D",1),("C",2)]) (fromList [("C",3),("A",4)])
-- fromList [("D",1),("C",5),("A",4)]
--
unionWith :: Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
-- | A generalised unionWith.
--
--
-- >>> outerJoin Left Left (\k a b -> Right (k, a, b)) (fromList [("A",1),("B",2)]) (singleton "A" 3)
-- fromList [("A",Right ("A",1,3)),("B",Left 2)]
--
--
-- This function is much inspired by the Data.Semialign.Semialign
-- class.
outerJoin :: Ord k => (a -> c) -> (b -> c) -> (k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
-- | Combine two Map on their shared keys, keeping the value from
-- the first Map
--
--
-- intersection = intersectionWith (\v _ -> v)
--
--
--
-- >>> intersection (fromList [("C",1),("B",2)]) (fromList [("B",3),("A",4)])
-- fromList [("B",2)]
--
intersection :: Ord k => Map k a -> Map k b -> Map k a
-- | Combine two Maps on their shared keys, using the supplied
-- function to combine values from the first and second Map
--
--
-- >>> intersectionWith (+) (fromList [("C",1),("B",2)]) (fromList [("B",3),("A",4)])
-- fromList [("B",5)]
--
intersectionWith :: Ord k => (a -> b -> c) -> Map k a -> Map k b -> Map k c
-- | Compute the difference of two Maps by subtracting all keys from
-- the second Map from the first Map
--
--
-- >>> difference (fromList [("C",1),("B",2)]) (fromList [("B",3),("A",4)])
-- fromList [("C",1)]
--
difference :: Ord k => Map k a -> Map k b -> Map k a
-- | Transform the values of a Map using their corresponding key
--
--
-- mapWithKey (pure id) = id
--
-- mapWithKey (liftA2 (.) f g) = mapWithKey f . mapWithKey g
--
--
--
-- mapWithKey f mempty = mempty
--
-- mapWithKey f (x <> y) = mapWithKey f x <> mapWithKey f y
--
--
--
-- >>> mapWithKey (,) (fromList [("B",1),("A",2)])
-- fromList [("B",("B",1)),("A",("A",2))]
--
mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
-- | Traverse all of the key-value pairs in a Map, in their original
-- order
--
--
-- >>> traverseWithKey (,) (fromList [("B",1),("A",2)])
-- ("BA",fromList [("B",1),("A",2)])
--
traverseWithKey :: Ord k => Applicative f => (k -> a -> f b) -> Map k a -> f (Map k b)
-- | Same as traverseWithKey, except that the order of effects is
-- not necessarily the same as the order of the keys
unorderedTraverseWithKey :: Ord k => Applicative f => (k -> a -> f b) -> Map k a -> f (Map k b)
-- | Traverse all of the key-value pairs in a Map, not preserving
-- their original order, where the result of the computation can be
-- forgotten.
--
-- Note that this is a strict traversal, fully traversing the map even
-- when the Applicative is lazy in the remaining elements.
unorderedTraverseWithKey_ :: Ord k => Applicative f => (k -> a -> f ()) -> Map k a -> f ()
-- | Fold all of the key-value pairs in a Map, in their original
-- order
--
--
-- >>> foldMapWithKey (,) (fromList [("B",[1]),("A",[2])])
-- ("BA",[1,2])
--
foldMapWithKey :: (Monoid m, Ord k) => (k -> a -> m) -> Map k a -> m
-- | Convert a Map to a list of key-value pairs in the original
-- order of keys
--
--
-- >>> toList (fromList [("B",1),("A",2)])
-- [("B",1),("A",2)]
--
toList :: Ord k => Map k v -> [(k, v)]
-- | Convert a Dhall.Map.Map to a
-- Data.Map.Map
--
--
-- >>> toMap (fromList [("B",1),("A",2)]) -- Order is lost upon conversion
-- fromList [("A",2),("B",1)]
--
toMap :: Map k v -> Map k v
-- | Return the keys from a Map in their original order
--
--
-- >>> keys (fromList [("B",1),("A",2)])
-- ["B","A"]
--
keys :: Map k v -> [k]
-- | Return the Data.Set.Set of the keys
--
--
-- >>> keysSet (fromList [("B",1),("A",2)])
-- fromList ["A","B"]
--
keysSet :: Map k v -> Set k
-- | Return the values from a Map in their original order.
--
--
-- >>> elems (fromList [("B",1),("A",2)])
-- [1,2]
--
elems :: Ord k => Map k v -> [v]
instance (Control.DeepSeq.NFData k, Control.DeepSeq.NFData v) => Control.DeepSeq.NFData (Dhall.Map.Map k v)
instance GHC.Generics.Generic (Dhall.Map.Map k v)
instance (Data.Data.Data k, Data.Data.Data v, GHC.Classes.Ord k) => Data.Data.Data (Dhall.Map.Map k v)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Dhall.Map.Keys a)
instance GHC.Generics.Generic (Dhall.Map.Keys a)
instance Data.Data.Data a => Data.Data.Data (Dhall.Map.Keys a)
instance (Data.Data.Data k, Data.Data.Data v, Language.Haskell.TH.Syntax.Lift k, Language.Haskell.TH.Syntax.Lift v, GHC.Classes.Ord k) => Language.Haskell.TH.Syntax.Lift (Dhall.Map.Map k v)
instance (GHC.Classes.Ord k, GHC.Classes.Eq v) => GHC.Classes.Eq (Dhall.Map.Map k v)
instance (GHC.Classes.Ord k, GHC.Classes.Ord v) => GHC.Classes.Ord (Dhall.Map.Map k v)
instance GHC.Base.Functor (Dhall.Map.Map k)
instance GHC.Classes.Ord k => Data.Foldable.Foldable (Dhall.Map.Map k)
instance GHC.Classes.Ord k => Data.Traversable.Traversable (Dhall.Map.Map k)
instance GHC.Classes.Ord k => GHC.Base.Semigroup (Dhall.Map.Map k v)
instance GHC.Classes.Ord k => GHC.Base.Monoid (Dhall.Map.Map k v)
instance (GHC.Show.Show k, GHC.Show.Show v, GHC.Classes.Ord k) => GHC.Show.Show (Dhall.Map.Map k v)
instance GHC.Classes.Ord k => GHC.Exts.IsList (Dhall.Map.Map k v)
instance (Data.Data.Data a, Language.Haskell.TH.Syntax.Lift a) => Language.Haskell.TH.Syntax.Lift (Dhall.Map.Keys a)
-- | This module contains some useful utilities copy-and-pasted from the
-- lens library to avoid a dependency which are used internally
-- and also re-exported for convenience
module Dhall.Optics
-- | Identical to Control.Lens.rewriteOf
rewriteOf :: ASetter a b a b -> (b -> Maybe a) -> a -> b
-- | Identical to Control.Lens.transformOf
transformOf :: ASetter a b a b -> (b -> b) -> a -> b
-- | Identical to Control.Lens.rewriteMOf
rewriteMOf :: Monad m => LensLike (WrappedMonad m) a b a b -> (b -> m (Maybe a)) -> a -> m b
-- | Identical to Control.Lens.transformMOf
transformMOf :: Monad m => LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
-- | Identical to Control.Lens.mapMOf
mapMOf :: LensLike (WrappedMonad m) s t a b -> (a -> m b) -> s -> m t
-- | This module only exports ways of constructing a Set, retrieving List,
-- Set, and Seq representations of the same data, as well as a novel
-- "difference" function. Any other Set-like or List-like functionality
-- should be obtained through toSet and toList, respectively.
module Dhall.Set
data Set a
Set :: Set a -> Seq a -> Set a
toList :: Set a -> [a]
toSet :: Set a -> Set a
toSeq :: Set a -> Seq a
fromList :: Ord a => [a] -> Set a
fromSet :: Set a -> Set a
append :: Ord a => a -> Set a -> Set a
empty :: Set a
-- | Returns, in order, all elements of the first Set not present in the
-- second. (It doesn't matter in what order the elements appear in the
-- second Set.)
difference :: Ord a => Set a -> Set a -> [a]
-- | Sort the set elements, forgetting their original ordering.
--
--
-- >>> sort (fromList [2, 1]) == fromList [1, 2]
-- True
--
sort :: Ord a => Set a -> Set a
-- |
-- >>> isSorted (fromList [2, 1])
-- False
--
-- >>> isSorted (fromList [1, 2])
-- True
--
isSorted :: Ord a => Set a -> Bool
-- |
-- >>> null (fromList [1])
-- False
--
-- >>> null (fromList [])
-- True
--
null :: Set a -> Bool
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Dhall.Set.Set a)
instance (Data.Data.Data a, GHC.Classes.Ord a) => Data.Data.Data (Dhall.Set.Set a)
instance GHC.Show.Show a => GHC.Show.Show (Dhall.Set.Set a)
instance GHC.Generics.Generic (Dhall.Set.Set a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Dhall.Set.Set a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Dhall.Set.Set a)
instance (Data.Data.Data a, Language.Haskell.TH.Syntax.Lift a, GHC.Classes.Ord a) => Language.Haskell.TH.Syntax.Lift (Dhall.Set.Set a)
instance Data.Foldable.Foldable Dhall.Set.Set
-- | This module provides the Src type used for source spans in
-- error messages
module Dhall.Src
-- | Source code extract
data Src
Src :: !SourcePos -> !SourcePos -> Text -> Src
[srcStart] :: Src -> !SourcePos
[srcEnd] :: Src -> !SourcePos
[srcText] :: Src -> Text
instance Control.DeepSeq.NFData Dhall.Src.Src
instance GHC.Show.Show Dhall.Src.Src
instance GHC.Classes.Ord Dhall.Src.Src
instance GHC.Generics.Generic Dhall.Src.Src
instance GHC.Classes.Eq Dhall.Src.Src
instance Data.Data.Data Dhall.Src.Src
instance Language.Haskell.TH.Syntax.Lift Dhall.Src.Src
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Src.Src
-- | This module contains the core calculus for the Dhall language.
--
-- Dhall is essentially a fork of the morte compiler but with
-- more built-in functionality, better error messages, and Haskell
-- integration
module Dhall.Core
-- | Constants for a pure type system
--
-- The axioms are:
--
--
-- ⊦ Type : Kind
-- ⊦ Kind : Sort
--
--
-- ... and the valid rule pairs are:
--
--
-- ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)
-- ⊦ Kind ↝ Type : Type -- Functions from types to terms (type-polymorphic functions)
-- ⊦ Sort ↝ Type : Type -- Functions from kinds to terms
-- ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type-level functions)
-- ⊦ Sort ↝ Kind : Sort -- Functions from kinds to types (kind-polymorphic functions)
-- ⊦ Sort ↝ Sort : Sort -- Functions from kinds to kinds (kind-level functions)
--
--
-- Note that Dhall does not support functions from terms to types and
-- therefore Dhall is not a dependently typed language
data Const
Type :: Const
Kind :: Const
Sort :: Const
-- | Internal representation of a directory that stores the path components
-- in reverse order
--
-- In other words, the directory /foo/bar/baz is encoded as
-- Directory { components = [ "baz", "bar", "foo" ] }
newtype Directory
Directory :: [Text] -> Directory
[components] :: Directory -> [Text]
-- | A File is a directory followed by one additional path
-- component representing the file name
data File
File :: Directory -> Text -> File
[directory] :: File -> Directory
[file] :: File -> Text
-- | The beginning of a file path which anchors subsequent path components
data FilePrefix
-- | Absolute path
Absolute :: FilePrefix
-- | Path relative to .
Here :: FilePrefix
-- | Path relative to ..
Parent :: FilePrefix
-- | Path relative to ~
Home :: FilePrefix
-- | Reference to an external resource
data Import
Import :: ImportHashed -> ImportMode -> Import
[importHashed] :: Import -> ImportHashed
[importMode] :: Import -> ImportMode
-- | A ImportType extended with an optional hash for semantic
-- integrity checks
data ImportHashed
ImportHashed :: Maybe (Digest SHA256) -> ImportType -> ImportHashed
[hash] :: ImportHashed -> Maybe (Digest SHA256)
[importType] :: ImportHashed -> ImportType
-- | How to interpret the import's contents (i.e. as Dhall code or raw
-- text)
data ImportMode
Code :: ImportMode
RawText :: ImportMode
Location :: ImportMode
-- | The type of import (i.e. local vs. remote vs. environment)
data ImportType
-- | Local path
Local :: FilePrefix -> File -> ImportType
-- | URL of remote resource and optional headers stored in an import
Remote :: URL -> ImportType
-- | Environment variable
Env :: Text -> ImportType
Missing :: ImportType
data URL
URL :: Scheme -> Text -> File -> Maybe Text -> Maybe (Expr Src Import) -> URL
[scheme] :: URL -> Scheme
[authority] :: URL -> Text
[path] :: URL -> File
[query] :: URL -> Maybe Text
[headers] :: URL -> Maybe (Expr Src Import)
data Scheme
HTTP :: Scheme
HTTPS :: Scheme
-- | Label for a bound variable
--
-- The Expr field is the variable's name (i.e. "x").
--
-- The Int field disambiguates variables with the same name if
-- there are multiple bound variables of the same name in scope. Zero
-- refers to the nearest bound variable and the index increases by one
-- for each bound variable of the same name going outward. The following
-- diagram may help:
--
--
-- ┌──refers to──┐
-- │ │
-- v │
-- λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0
--
-- ┌─────────────────refers to─────────────────┐
-- │ │
-- v │
-- λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1
--
--
-- This Int behaves like a De Bruijn index in the special case
-- where all variables have the same name.
--
-- You can optionally omit the index if it is 0:
--
--
-- ┌─refers to─┐
-- │ │
-- v │
-- λ(x : Type) → λ(y : Type) → λ(x : Type) → x
--
--
-- Zero indices are omitted when pretty-printing Vars and non-zero
-- indices appear as a numeric suffix.
data Var
V :: Text -> !Int -> Var
-- | The body of an interpolated Text literal
data Chunks s a
Chunks :: [(Text, Expr s a)] -> Text -> Chunks s a
-- | Syntax tree for expressions
--
-- The s type parameter is used to track the presence or absence
-- of Src spans:
--
--
-- - If s = Src then the code may contains Src
-- spans (either in a Noted constructor or inline within another
-- constructor, like Let)
-- - If s = Void then the code has no Src
-- spans
--
--
-- The a type parameter is used to track the presence or absence
-- of imports
--
--
-- - If a = Import then the code may contain unresolved
-- Imports
-- - If a = Void then the code has no
-- Imports
--
data Expr s a
-- |
-- Const c ~ c
--
Const :: Const -> Expr s a
-- |
-- Var (V x 0) ~ x
-- Var (V x n) ~ x@n
--
Var :: Var -> Expr s a
-- |
-- Lam x A b ~ λ(x : A) -> b
--
Lam :: Text -> Expr s a -> Expr s a -> Expr s a
-- |
-- Pi "_" A B ~ A -> B
-- Pi x A B ~ ∀(x : A) -> B
--
Pi :: Text -> Expr s a -> Expr s a -> Expr s a
-- |
-- App f a ~ f a
--
App :: Expr s a -> Expr s a -> Expr s a
-- |
-- Let (Binding _ x _ Nothing _ r) e ~ let x = r in e
-- Let (Binding _ x _ (Just t ) _ r) e ~ let x : t = r in e
--
--
-- The difference between
--
--
-- let x = a let y = b in e
--
--
-- and
--
--
-- let x = a in let y = b in e
--
--
-- is only an additional Note around Let "y" … in
-- the second example.
--
-- See MultiLet for a representation of let-blocks that mirrors
-- the source code more closely.
Let :: Binding s a -> Expr s a -> Expr s a
-- |
-- Annot x t ~ x : t
--
Annot :: Expr s a -> Expr s a -> Expr s a
-- |
-- Bool ~ Bool
--
Bool :: Expr s a
-- |
-- BoolLit b ~ b
--
BoolLit :: Bool -> Expr s a
-- |
-- BoolAnd x y ~ x && y
--
BoolAnd :: Expr s a -> Expr s a -> Expr s a
-- |
-- BoolOr x y ~ x || y
--
BoolOr :: Expr s a -> Expr s a -> Expr s a
-- |
-- BoolEQ x y ~ x == y
--
BoolEQ :: Expr s a -> Expr s a -> Expr s a
-- |
-- BoolNE x y ~ x != y
--
BoolNE :: Expr s a -> Expr s a -> Expr s a
-- |
-- BoolIf x y z ~ if x then y else z
--
BoolIf :: Expr s a -> Expr s a -> Expr s a -> Expr s a
-- |
-- Natural ~ Natural
--
Natural :: Expr s a
-- |
-- NaturalLit n ~ n
--
NaturalLit :: Natural -> Expr s a
-- |
-- NaturalFold ~ Natural/fold
--
NaturalFold :: Expr s a
-- |
-- NaturalBuild ~ Natural/build
--
NaturalBuild :: Expr s a
-- |
-- NaturalIsZero ~ Natural/isZero
--
NaturalIsZero :: Expr s a
-- |
-- NaturalEven ~ Natural/even
--
NaturalEven :: Expr s a
-- |
-- NaturalOdd ~ Natural/odd
--
NaturalOdd :: Expr s a
-- |
-- NaturalToInteger ~ Natural/toInteger
--
NaturalToInteger :: Expr s a
-- |
-- NaturalShow ~ Natural/show
--
NaturalShow :: Expr s a
-- |
-- NaturalSubtract ~ Natural/subtract
--
NaturalSubtract :: Expr s a
-- |
-- NaturalPlus x y ~ x + y
--
NaturalPlus :: Expr s a -> Expr s a -> Expr s a
-- |
-- NaturalTimes x y ~ x * y
--
NaturalTimes :: Expr s a -> Expr s a -> Expr s a
-- |
-- Integer ~ Integer
--
Integer :: Expr s a
-- |
-- IntegerLit n ~ ±n
--
IntegerLit :: Integer -> Expr s a
-- |
-- IntegerShow ~ Integer/show
--
IntegerShow :: Expr s a
-- |
-- IntegerToDouble ~ Integer/toDouble
--
IntegerToDouble :: Expr s a
-- |
-- Double ~ Double
--
Double :: Expr s a
-- |
-- DoubleLit n ~ n
--
DoubleLit :: Double -> Expr s a
-- |
-- DoubleShow ~ Double/show
--
DoubleShow :: Expr s a
-- |
-- Text ~ Text
--
Text :: Expr s a
-- |
-- TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3"
--
TextLit :: Chunks s a -> Expr s a
-- |
-- TextAppend x y ~ x ++ y
--
TextAppend :: Expr s a -> Expr s a -> Expr s a
-- |
-- TextShow ~ Text/show
--
TextShow :: Expr s a
-- |
-- List ~ List
--
List :: Expr s a
-- |
-- ListLit (Just t ) [x, y, z] ~ [x, y, z] : t
-- ListLit Nothing [x, y, z] ~ [x, y, z]
--
ListLit :: Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
-- |
-- ListAppend x y ~ x # y
--
ListAppend :: Expr s a -> Expr s a -> Expr s a
-- |
-- ListBuild ~ List/build
--
ListBuild :: Expr s a
-- |
-- ListFold ~ List/fold
--
ListFold :: Expr s a
-- |
-- ListLength ~ List/length
--
ListLength :: Expr s a
-- |
-- ListHead ~ List/head
--
ListHead :: Expr s a
-- |
-- ListLast ~ List/last
--
ListLast :: Expr s a
-- |
-- ListIndexed ~ List/indexed
--
ListIndexed :: Expr s a
-- |
-- ListReverse ~ List/reverse
--
ListReverse :: Expr s a
-- |
-- Optional ~ Optional
--
Optional :: Expr s a
-- |
-- Some e ~ Some e
--
Some :: Expr s a -> Expr s a
-- |
-- None ~ None
--
None :: Expr s a
-- |
-- OptionalFold ~ Optional/fold
--
OptionalFold :: Expr s a
-- |
-- OptionalBuild ~ Optional/build
--
OptionalBuild :: Expr s a
-- |
-- Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }
--
Record :: Map Text (Expr s a) -> Expr s a
-- |
-- RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }
--
RecordLit :: Map Text (Expr s a) -> Expr s a
-- |
-- Union [(k1, Just t1), (k2, Nothing)] ~ < k1 : t1 | k2 >
--
Union :: Map Text (Maybe (Expr s a)) -> Expr s a
-- |
-- Combine x y ~ x ∧ y
--
Combine :: Expr s a -> Expr s a -> Expr s a
-- |
-- CombineTypes x y ~ x ⩓ y
--
CombineTypes :: Expr s a -> Expr s a -> Expr s a
-- |
-- Prefer x y ~ x ⫽ y
--
Prefer :: Expr s a -> Expr s a -> Expr s a
-- |
-- Merge x y (Just t ) ~ merge x y : t
-- Merge x y Nothing ~ merge x y
--
Merge :: Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
-- |
-- ToMap x (Just t) ~ toMap x : t
-- ToMap x Nothing ~ toMap x
--
ToMap :: Expr s a -> Maybe (Expr s a) -> Expr s a
-- |
-- Field e x ~ e.x
--
Field :: Expr s a -> Text -> Expr s a
-- |
-- Project e (Left xs) ~ e.{ xs }
--
--
-- | > Project e (Right t) ~ e.(t)
Project :: Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
-- |
-- Assert e ~ assert : e
--
Assert :: Expr s a -> Expr s a
-- |
-- Equivalent x y ~ x ≡ y
--
Equivalent :: Expr s a -> Expr s a -> Expr s a
-- |
-- Note s x ~ e
--
Note :: s -> Expr s a -> Expr s a
-- |
-- ImportAlt ~ e1 ? e2
--
ImportAlt :: Expr s a -> Expr s a -> Expr s a
-- |
-- Embed import ~ import
--
Embed :: a -> Expr s a
-- | α-normalize an expression by renaming all bound variables to
-- "_" and using De Bruijn indices to distinguish them
--
--
-- >>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x"))))
-- Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1)))))
--
--
-- α-normalization does not affect free variables:
--
--
-- >>> alphaNormalize "x"
-- Var (V "x" 0)
--
alphaNormalize :: Expr s a -> Expr s a
-- | Reduce an expression to its normal form, performing beta reduction
--
-- normalize does not type-check the expression. You may want to
-- type-check expressions before normalizing them since normalization can
-- convert an ill-typed expression into a well-typed expression.
--
-- normalize can also fail with error if you normalize an
-- ill-typed expression
normalize :: Eq a => Expr s a -> Expr t a
-- | Reduce an expression to its normal form, performing beta reduction and
-- applying any custom definitions.
--
-- normalizeWith is designed to be used with function
-- typeWith. The typeWith function allows typing of
-- Dhall functions in a custom typing context whereas
-- normalizeWith allows evaluating Dhall expressions in a custom
-- context.
--
-- To be more precise normalizeWith applies the given normalizer
-- when it finds an application term that it cannot reduce by other
-- means.
--
-- Note that the context used in normalization will determine the
-- properties of normalization. That is, if the functions in custom
-- context are not total then the Dhall language, evaluated with those
-- functions is not total either.
--
-- normalizeWith can fail with an error if you normalize an
-- ill-typed expression
normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
-- | This function generalizes normalizeWith by allowing the custom
-- normalizer to use an arbitrary Monad
--
-- normalizeWithM can fail with an error if you normalize
-- an ill-typed expression
normalizeWithM :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
type Normalizer a = NormalizerM Identity a
-- | Use this to wrap you embedded functions (see normalizeWith) to
-- make them polymorphic enough to be used.
type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))
-- | A reified Normalizer, which can be stored in structures without
-- running into impredicative polymorphism.
newtype ReifiedNormalizer a
ReifiedNormalizer :: Normalizer a -> ReifiedNormalizer a
[getReifiedNormalizer] :: ReifiedNormalizer a -> Normalizer a
-- | Returns True if two expressions are α-equivalent and
-- β-equivalent and False otherwise
--
-- judgmentallyEqual can fail with an error if you compare
-- ill-typed expressions
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
-- | Substitute all occurrences of a variable with an expression
--
--
-- subst x C B ~ B[x := C]
--
subst :: Var -> Expr s a -> Expr s a -> Expr s a
-- | shift is used by both normalization and type-checking to avoid
-- variable capture by shifting variable indices
--
-- For example, suppose that you were to normalize the following
-- expression:
--
--
-- λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
--
--
-- If you were to substitute y with x without shifting
-- any variable indices, then you would get the following incorrect
-- result:
--
--
-- λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form
--
--
-- In order to substitute x in place of y we need to
-- shift x by 1 in order to avoid being
-- misinterpreted as the x bound by the innermost lambda. If we
-- perform that shift then we get the correct result:
--
--
-- λ(a : Type) → λ(x : a) → λ(x : a) → x@1
--
--
-- As a more worked example, suppose that you were to normalize the
-- following expression:
--
--
-- λ(a : Type)
-- → λ(f : a → a → a)
-- → λ(x : a)
-- → λ(x : a)
-- → (λ(x : a) → f x x@1) x@1
--
--
-- The correct normalized result would be:
--
--
-- λ(a : Type)
-- → λ(f : a → a → a)
-- → λ(x : a)
-- → λ(x : a)
-- → f x@1 x
--
--
-- The above example illustrates how we need to both increase and
-- decrease variable indices as part of substitution:
--
--
-- - We need to increase the index of the outer x@1 to
-- x@2 before we substitute it into the body of the innermost
-- lambda expression in order to avoid variable capture. This
-- substitution changes the body of the lambda expression to (f x@2
-- x@1)
-- - We then remove the innermost lambda and therefore decrease the
-- indices of both xs in (f x@2 x@1) to (f x@1
-- x) in order to reflect that one less x variable is now
-- bound within that scope
--
--
-- Formally, (shift d (V x n) e) modifies the expression
-- e by adding d to the indices of all variables named
-- x whose indices are greater than (n + m), where
-- m is the number of bound variables of the same name within
-- that scope
--
-- In practice, d is always 1 or -1 because we
-- either:
--
--
-- - increment variables by 1 to avoid variable capture during
-- substitution
-- - decrement variables by 1 when deleting lambdas after
-- substitution
--
--
-- n starts off at 0 when substitution begins and
-- increments every time we descend into a lambda or let expression that
-- binds a variable of the same name in order to avoid shifting the bound
-- variables by mistake.
shift :: Int -> Var -> Expr s a -> Expr s a
-- | Quickly check if an expression is in normal form
--
-- Given a well-typed expression e, isNormalized
-- e is equivalent to e == normalize e.
--
-- Given an ill-typed expression, isNormalized may fail with an
-- error, or evaluate to either False or True!
isNormalized :: Eq a => Expr s a -> Bool
-- | Check if an expression is in a normal form given a context of
-- evaluation. Unlike isNormalized, this will fully normalize and
-- traverse through the expression.
--
-- It is much more efficient to use isNormalized.
--
-- isNormalizedWith can fail with an error if you check an
-- ill-typed expression
isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
-- | Remove all Note constructors from an Expr (i.e.
-- de-Note)
denote :: Expr s a -> Expr t a
shallowDenote :: Expr s a -> Expr s a
-- | Detect if the given variable is free within the given expression
--
--
-- >>> "x" `freeIn` "x"
-- True
--
-- >>> "x" `freeIn` "y"
-- False
--
-- >>> "x" `freeIn` Lam "x" (Const Type) "x"
-- False
--
freeIn :: Eq a => Var -> Expr s a -> Bool
pretty :: Pretty a => a -> Text
-- | A traversal over the immediate sub-expressions of an expression.
subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
-- | A traversal over the immediate sub-expressions in Chunks.
chunkExprs :: Applicative f => (Expr s a -> f (Expr t b)) -> Chunks s a -> f (Chunks t b)
-- | Traverse over the immediate Expr children in a Binding.
bindingExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> Binding s a -> f (Binding s b)
-- | Generate a MultiLet from the contents of a Let.
--
-- In the resulting MultiLet bs e, e is
-- guaranteed not to be a Let, but it might be a (Note
-- … (Let …)).
--
-- Given parser output, multiLet consolidates lets that
-- formed a let-block in the original source.
multiLet :: Binding s a -> Expr s a -> MultiLet s a
-- | Wrap let-Bindings around an Expr.
--
-- wrapInLets can be understood as an inverse for multiLet:
--
--
-- let MultiLet bs e1 = multiLet b e0
--
-- wrapInLets bs e1 == Let b e0
--
wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a
data MultiLet s a
MultiLet :: NonEmpty (Binding s a) -> Expr s a -> MultiLet s a
-- | Record the binding part of a let expression.
--
-- For example, > let x : Bool = True in x will be instantiated as
-- follows:
--
--
-- - bindingSrc0 corresponds to the A comment.
-- - variable is "x"
-- - bindingSrc1 corresponds to the B comment.
-- - annotation is Just a pair, corresponding to the
-- C comment and Bool.
-- - bindingSrc2 corresponds to the D comment.
-- - value corresponds to True.
--
data Binding s a
Binding :: Maybe s -> Text -> Maybe s -> Maybe (Maybe s, Expr s a) -> Maybe s -> Expr s a -> Binding s a
[bindingSrc0] :: Binding s a -> Maybe s
[variable] :: Binding s a -> Text
[bindingSrc1] :: Binding s a -> Maybe s
[annotation] :: Binding s a -> Maybe (Maybe s, Expr s a)
[bindingSrc2] :: Binding s a -> Maybe s
[value] :: Binding s a -> Expr s a
-- | Construct a Binding with no source information and no type
-- annotation.
makeBinding :: Text -> Expr s a -> Binding s a
-- | Utility function used to throw internal errors that should never
-- happen (in theory) but that are not enforced by the type system
internalError :: Text -> forall b. b
-- | The set of reserved identifiers for the Dhall language
reservedIdentifiers :: HashSet Text
escapeText :: Text -> Text
-- | Returns True if the given Char is valid within an
-- unquoted path component
--
-- This is exported for reuse within the
-- Dhall.Parser.Token module
pathCharacter :: Char -> Bool
-- | Convenience utility for converting Either-based exceptions to
-- IO-based exceptions
throws :: (Exception e, MonadIO io) => Either e a -> io a
instance Control.DeepSeq.NFData Dhall.Core.ImportType
instance GHC.Show.Show Dhall.Core.ImportType
instance GHC.Classes.Ord Dhall.Core.ImportType
instance GHC.Generics.Generic Dhall.Core.ImportType
instance GHC.Classes.Eq Dhall.Core.ImportType
instance Control.DeepSeq.NFData Dhall.Core.ImportHashed
instance GHC.Show.Show Dhall.Core.ImportHashed
instance GHC.Classes.Ord Dhall.Core.ImportHashed
instance GHC.Generics.Generic Dhall.Core.ImportHashed
instance GHC.Classes.Eq Dhall.Core.ImportHashed
instance Control.DeepSeq.NFData Dhall.Core.Import
instance GHC.Show.Show Dhall.Core.Import
instance GHC.Classes.Ord Dhall.Core.Import
instance GHC.Generics.Generic Dhall.Core.Import
instance GHC.Classes.Eq Dhall.Core.Import
instance Control.DeepSeq.NFData Dhall.Core.URL
instance GHC.Show.Show Dhall.Core.URL
instance GHC.Classes.Ord Dhall.Core.URL
instance GHC.Generics.Generic Dhall.Core.URL
instance GHC.Classes.Eq Dhall.Core.URL
instance (Control.DeepSeq.NFData s, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Dhall.Core.Chunks s a)
instance (Data.Data.Data s, Data.Data.Data a) => Data.Data.Data (Dhall.Core.Chunks s a)
instance (GHC.Classes.Ord s, GHC.Classes.Ord a) => GHC.Classes.Ord (Dhall.Core.Chunks s a)
instance (GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Dhall.Core.Chunks s a)
instance (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Dhall.Core.Chunks s a)
instance Data.Traversable.Traversable (Dhall.Core.Chunks s)
instance GHC.Generics.Generic (Dhall.Core.Chunks s a)
instance Data.Foldable.Foldable (Dhall.Core.Chunks s)
instance GHC.Base.Functor (Dhall.Core.Chunks s)
instance (Control.DeepSeq.NFData s, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Dhall.Core.Expr s a)
instance (Data.Data.Data s, Data.Data.Data a) => Data.Data.Data (Dhall.Core.Expr s a)
instance (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Dhall.Core.Expr s a)
instance Data.Traversable.Traversable (Dhall.Core.Expr s)
instance GHC.Generics.Generic (Dhall.Core.Expr s a)
instance Data.Foldable.Foldable (Dhall.Core.Expr s)
instance Data.Traversable.Traversable (Dhall.Core.Binding s)
instance (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Dhall.Core.Binding s a)
instance (GHC.Classes.Ord s, GHC.Classes.Ord a) => GHC.Classes.Ord (Dhall.Core.Binding s a)
instance (Control.DeepSeq.NFData s, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Dhall.Core.Binding s a)
instance GHC.Generics.Generic (Dhall.Core.Binding s a)
instance GHC.Base.Functor (Dhall.Core.Binding s)
instance Data.Foldable.Foldable (Dhall.Core.Binding s)
instance (GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Dhall.Core.Binding s a)
instance (Data.Data.Data s, Data.Data.Data a) => Data.Data.Data (Dhall.Core.Binding s a)
instance Control.DeepSeq.NFData Dhall.Core.Var
instance GHC.Show.Show Dhall.Core.Var
instance GHC.Classes.Ord Dhall.Core.Var
instance GHC.Classes.Eq Dhall.Core.Var
instance GHC.Generics.Generic Dhall.Core.Var
instance Data.Data.Data Dhall.Core.Var
instance Control.DeepSeq.NFData Dhall.Core.ImportMode
instance GHC.Show.Show Dhall.Core.ImportMode
instance GHC.Classes.Ord Dhall.Core.ImportMode
instance GHC.Generics.Generic Dhall.Core.ImportMode
instance GHC.Classes.Eq Dhall.Core.ImportMode
instance Control.DeepSeq.NFData Dhall.Core.Scheme
instance GHC.Show.Show Dhall.Core.Scheme
instance GHC.Classes.Ord Dhall.Core.Scheme
instance GHC.Generics.Generic Dhall.Core.Scheme
instance GHC.Classes.Eq Dhall.Core.Scheme
instance Control.DeepSeq.NFData Dhall.Core.FilePrefix
instance GHC.Show.Show Dhall.Core.FilePrefix
instance GHC.Classes.Ord Dhall.Core.FilePrefix
instance GHC.Generics.Generic Dhall.Core.FilePrefix
instance GHC.Classes.Eq Dhall.Core.FilePrefix
instance Control.DeepSeq.NFData Dhall.Core.File
instance GHC.Show.Show Dhall.Core.File
instance GHC.Classes.Ord Dhall.Core.File
instance GHC.Generics.Generic Dhall.Core.File
instance GHC.Classes.Eq Dhall.Core.File
instance Control.DeepSeq.NFData Dhall.Core.Directory
instance GHC.Show.Show Dhall.Core.Directory
instance GHC.Classes.Ord Dhall.Core.Directory
instance GHC.Generics.Generic Dhall.Core.Directory
instance GHC.Classes.Eq Dhall.Core.Directory
instance Control.DeepSeq.NFData Dhall.Core.Const
instance GHC.Generics.Generic Dhall.Core.Const
instance GHC.Enum.Enum Dhall.Core.Const
instance GHC.Enum.Bounded Dhall.Core.Const
instance Data.Data.Data Dhall.Core.Const
instance GHC.Classes.Ord Dhall.Core.Const
instance GHC.Classes.Eq Dhall.Core.Const
instance GHC.Show.Show Dhall.Core.Const
instance (GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Dhall.Core.Expr s a)
instance (GHC.Classes.Ord s, GHC.Classes.Ord a) => GHC.Classes.Ord (Dhall.Core.Expr s a)
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.URL
instance GHC.Base.Semigroup Dhall.Core.ImportType
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.ImportType
instance GHC.Base.Semigroup Dhall.Core.ImportHashed
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.ImportHashed
instance GHC.Base.Semigroup Dhall.Core.Import
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Import
instance (Language.Haskell.TH.Syntax.Lift s, Language.Haskell.TH.Syntax.Lift a, Data.Data.Data s, Data.Data.Data a) => Language.Haskell.TH.Syntax.Lift (Dhall.Core.Expr s a)
instance GHC.Base.Functor (Dhall.Core.Expr s)
instance GHC.Base.Applicative (Dhall.Core.Expr s)
instance GHC.Base.Monad (Dhall.Core.Expr s)
instance Data.Bifunctor.Bifunctor Dhall.Core.Expr
instance Data.String.IsString (Dhall.Core.Expr s a)
instance (Language.Haskell.TH.Syntax.Lift s, Language.Haskell.TH.Syntax.Lift a, Data.Data.Data s, Data.Data.Data a) => Language.Haskell.TH.Syntax.Lift (Dhall.Core.Chunks s a)
instance GHC.Base.Semigroup (Dhall.Core.Chunks s a)
instance GHC.Base.Monoid (Dhall.Core.Chunks s a)
instance Data.String.IsString (Dhall.Core.Chunks s a)
instance Data.Text.Prettyprint.Doc.Internal.Pretty a => Data.Text.Prettyprint.Doc.Internal.Pretty (Dhall.Core.Expr s a)
instance Data.Bifunctor.Bifunctor Dhall.Core.Binding
instance Language.Haskell.TH.Syntax.Lift Dhall.Core.Var
instance Data.String.IsString Dhall.Core.Var
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Var
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.FilePrefix
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.File
instance GHC.Base.Semigroup Dhall.Core.File
instance GHC.Base.Semigroup Dhall.Core.Directory
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Directory
instance Language.Haskell.TH.Syntax.Lift Dhall.Core.Const
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Const
-- | This module contains logic for pretty-printing expressions, including
-- support for syntax highlighting
module Dhall.Pretty
-- | Annotation type used to tag elements in a pretty-printed document for
-- syntax highlighting purposes
data Ann
-- | Used for syntactic keywords
Keyword :: Ann
-- | Syntax punctuation such as commas, parenthesis, and braces
Syntax :: Ann
-- | Record labels
Label :: Ann
-- | Literals such as integers and strings
Literal :: Ann
-- | Builtin types and values
Builtin :: Ann
-- | Operators
Operator :: Ann
-- | Convert annotations to their corresponding color for syntax
-- highlighting purposes
annToAnsiStyle :: Ann -> AnsiStyle
-- | Pretty print an expression
prettyExpr :: Pretty a => Expr s a -> Doc Ann
data CharacterSet
ASCII :: CharacterSet
Unicode :: CharacterSet
-- | Pretty-print an Expr using the given CharacterSet.
--
-- prettyCharacterSet largely ignores Notes. Notes
-- do however matter for the layout of let-blocks:
--
--
-- >>> let inner = Let (Binding Nothing "x" Nothing Nothing Nothing (NaturalLit 1)) (Var (V "x" 0)) :: Expr Src ()
--
-- >>> prettyCharacterSet ASCII (Let (Binding Nothing "y" Nothing Nothing Nothing (NaturalLit 2)) inner)
-- let y = 2 let x = 1 in x
--
-- >>> prettyCharacterSet ASCII (Let (Binding Nothing "y" Nothing Nothing Nothing (NaturalLit 2)) (Note (Src unusedSourcePos unusedSourcePos "") inner))
-- let y = 2 in let x = 1 in x
--
--
-- This means the structure of parsed let-blocks is preserved.
prettyCharacterSet :: Pretty a => CharacterSet -> Expr Src a -> Doc Ann
-- | Default layout options
layoutOpts :: LayoutOptions
-- | Parse Dhall tokens. Even though we don't have a tokenizer per-se this
module Dhall.Parser.Token
validCodepoint :: Char -> Bool
whitespace :: Parser ()
nonemptyWhitespace :: Parser ()
bashEnvironmentVariable :: Parser Text
posixEnvironmentVariable :: Parser Text
data ComponentType
URLComponent :: ComponentType
FileComponent :: ComponentType
file_ :: ComponentType -> Parser File
labelOnly :: Parser Text
label :: Parser Text
anyLabel :: Parser Text
labels :: Parser (Set Text)
httpRaw :: Parser URL
hexdig :: Char -> Bool
identifier :: Parser Var
hexNumber :: Parser Int
doubleLiteral :: Parser Double
doubleInfinity :: Parser Double
naturalLiteral :: Parser Natural
integerLiteral :: Parser Integer
_Optional :: Parser ()
_if :: Parser ()
_then :: Parser ()
_else :: Parser ()
_letOnly :: Parser ()
_let :: Parser ()
_in :: Parser ()
_as :: Parser ()
_using :: Parser ()
_merge :: Parser ()
_toMap :: Parser ()
_assert :: Parser ()
_Some :: Parser ()
_None :: Parser ()
_NaturalFold :: Parser ()
_NaturalBuild :: Parser ()
_NaturalIsZero :: Parser ()
_NaturalEven :: Parser ()
_NaturalOdd :: Parser ()
_NaturalToInteger :: Parser ()
_NaturalShow :: Parser ()
_NaturalSubtract :: Parser ()
_IntegerShow :: Parser ()
_IntegerToDouble :: Parser ()
_DoubleShow :: Parser ()
_ListBuild :: Parser ()
_ListFold :: Parser ()
_ListLength :: Parser ()
_ListHead :: Parser ()
_ListLast :: Parser ()
_ListIndexed :: Parser ()
_ListReverse :: Parser ()
_OptionalFold :: Parser ()
_OptionalBuild :: Parser ()
_Bool :: Parser ()
_Natural :: Parser ()
_Integer :: Parser ()
_Double :: Parser ()
_Text :: Parser ()
_TextShow :: Parser ()
_List :: Parser ()
_True :: Parser ()
_False :: Parser ()
_NaN :: Parser ()
_Type :: Parser ()
_Kind :: Parser ()
_Sort :: Parser ()
_Location :: Parser ()
_equalOnly :: Parser ()
_equal :: Parser ()
_or :: Parser ()
_plus :: Parser ()
_textAppend :: Parser ()
_listAppend :: Parser ()
_and :: Parser ()
_times :: Parser ()
_doubleEqual :: Parser ()
_notEqual :: Parser ()
_dot :: Parser ()
_openBrace :: Parser ()
_closeBrace :: Parser ()
_openBracket :: Parser ()
_closeBracket :: Parser ()
_openAngle :: Parser ()
_closeAngle :: Parser ()
_bar :: Parser ()
_comma :: Parser ()
_openParens :: Parser ()
_closeParens :: Parser ()
_colonOnly :: Parser ()
_colon :: Parser ()
_at :: Parser ()
_equivalent :: Parser ()
_missing :: Parser ()
_importAlt :: Parser ()
_combine :: Parser ()
_combineTypes :: Parser ()
_prefer :: Parser ()
_lambda :: Parser ()
_forall :: Parser ()
_arrow :: Parser ()
-- | Parsing Dhall expressions.
module Dhall.Parser.Expression
getSourcePos :: MonadParsec e s m => m SourcePos
getOffset :: MonadParsec e s m => m Int
setOffset :: MonadParsec e s m => Int -> m ()
src :: Parser a -> Parser Src
noted :: Parser (Expr Src a) -> Parser (Expr Src a)
completeExpression :: Parser a -> Parser (Expr Src a)
importExpression :: Parser a -> Parser (Expr Src a)
data Parsers a
Parsers :: Parser (Expr Src a) -> Parser (Expr Src a) -> Parsers a
[completeExpression_] :: Parsers a -> Parser (Expr Src a)
[importExpression_] :: Parsers a -> Parser (Expr Src a)
parsers :: Parser a -> Parsers a
env :: Parser ImportType
localRaw :: Parser ImportType
local :: Parser ImportType
http :: Parser ImportType
missing :: Parser ImportType
importType_ :: Parser ImportType
importHash_ :: Parser (Digest SHA256)
importHashed_ :: Parser ImportHashed
import_ :: Parser Import
-- | Similar to renderChunks except that this doesn't bother to
-- render interpolated expressions to avoid a `Buildable a` constraint.
-- The interpolated contents are not necessary for computing how much to
-- dedent a multi-line string
--
-- This also doesn't include the surrounding quotes since they would
-- interfere with the whitespace detection
renderChunks :: Chunks s a -> Text
splitOn :: Text -> Text -> NonEmpty Text
linesLiteral :: Chunks s a -> NonEmpty (Chunks s a)
unlinesLiteral :: NonEmpty (Chunks s a) -> Chunks s a
emptyLine :: Chunks s a -> Bool
leadingSpaces :: Chunks s a -> Text
dropLiteral :: Int -> Chunks s a -> Chunks s a
toDoubleQuoted :: Chunks Src a -> Chunks Src a
-- | This module contains Dhall's parsing logic
module Dhall.Parser
-- | Parse an expression from Expr containing a Dhall program
exprFromText :: String -> Text -> Either ParseError (Expr Src Import)
-- | Like exprFromText but also returns the leading comments and
-- whitespace (i.e. header) up to the last newline before the code begins
--
-- In other words, if you have a Dhall file of the form:
--
--
-- -- Comment 1
-- 2
--
--
-- Then this will preserve Comment 1, but not Comment 2
--
-- This is used by dhall-format to preserve leading comments and
-- whitespace
exprAndHeaderFromText :: String -> Text -> Either ParseError (Text, Expr Src Import)
-- | Parser for a top-level Dhall expression
expr :: Parser (Expr Src Import)
-- | Parser for a top-level Dhall expression. The expression is
-- parameterized over any parseable type, allowing the language to be
-- extended as needed.
exprA :: Parser a -> Parser (Expr Src a)
-- | Source code extract
data Src
Src :: !SourcePos -> !SourcePos -> Text -> Src
[srcStart] :: Src -> !SourcePos
[srcEnd] :: Src -> !SourcePos
[srcText] :: Src -> Text
data SourcedException e
SourcedException :: Src -> e -> SourcedException e
-- | A parsing error
data ParseError
ParseError :: ParseErrorBundle Text Void -> Text -> ParseError
[unwrap] :: ParseError -> ParseErrorBundle Text Void
[input] :: ParseError -> Text
-- | A Parser that is almost identical to
-- Text.Megaparsec.Parsec except treating
-- Haskell-style comments as whitespace
newtype Parser a
Parser :: Parsec Void Text a -> Parser a
[unParser] :: Parser a -> Parsec Void Text a
instance GHC.Show.Show Dhall.Parser.ParseError
instance GHC.Exception.Type.Exception Dhall.Parser.ParseError
-- | This module contains the implementation of the dhall lint
-- command
module Dhall.Lint
-- | Automatically improve a Dhall expression
--
-- Currently this:
--
--
lint :: Expr s Import -> Expr t Import
removeUnusedBindings :: Eq a => Expr s a -> Maybe (Expr s a)
-- | This module contains the implementation of the dhall format
-- subcommand
module Dhall.Format
-- | Arguments to the format subcommand
data Format
Format :: CharacterSet -> FormatMode -> Format
[characterSet] :: Format -> CharacterSet
[formatMode] :: Format -> FormatMode
-- | The format subcommand can either Modify its input or
-- simply Check that the input is already formatted
data FormatMode
Modify :: Maybe FilePath -> FormatMode
-- | Modify file in-place if present, otherwise read from stdin
-- and write to stdout
[inplace] :: FormatMode -> Maybe FilePath
Check :: Maybe FilePath -> FormatMode
-- | Read from the given file if present, otherwise read from
-- stdin
[path] :: FormatMode -> Maybe FilePath
-- | Implementation of the dhall format subcommand
format :: Format -> IO ()
instance GHC.Exception.Type.Exception Dhall.Format.NotFormatted
instance GHC.Show.Show Dhall.Format.NotFormatted
-- | This module contains logic for converting Dhall expressions to and
-- from CBOR expressions which can in turn be converted to and from a
-- binary representation
module Dhall.Binary
-- | Supported version strings
data StandardVersion
-- | No version string
NoVersion :: StandardVersion
-- | Version "5.0.0"
V_5_0_0 :: StandardVersion
-- | Version "4.0.0"
V_4_0_0 :: StandardVersion
-- | Version "3.0.0"
V_3_0_0 :: StandardVersion
-- | Version "2.0.0"
V_2_0_0 :: StandardVersion
-- | Version "1.0.0"
V_1_0_0 :: StandardVersion
renderStandardVersion :: StandardVersion -> Text
-- | Types that can be encoded as a CBOR Term
class ToTerm a
encode :: ToTerm a => a -> Term
-- | Types that can be decoded from a CBOR Term
class FromTerm a
decode :: FromTerm a => Term -> Maybe a
-- | Encode a Dhall expression as a CBOR Term
--
-- This denotes the expression before encoding it. To encode an
-- already denoted expression, it is more efficient to directly use
-- encode.
encodeExpression :: Expr s Import -> Term
-- | Decode a Dhall expression from a CBOR Term
decodeExpression :: FromTerm a => Term -> Either DecodingFailure (Expr s a)
data DecodingFailure
CBORIsNotDhall :: Term -> DecodingFailure
instance GHC.Classes.Eq Dhall.Binary.DecodingFailure
instance GHC.Enum.Bounded Dhall.Binary.StandardVersion
instance GHC.Enum.Enum Dhall.Binary.StandardVersion
instance GHC.Exception.Type.Exception Dhall.Binary.DecodingFailure
instance GHC.Show.Show Dhall.Binary.DecodingFailure
instance Dhall.Binary.FromTerm a => Dhall.Binary.FromTerm (Dhall.Core.Expr s a)
instance Dhall.Binary.FromTerm Dhall.Core.Import
instance Dhall.Binary.FromTerm Data.Void.Void
instance Dhall.Binary.ToTerm a => Dhall.Binary.ToTerm (Dhall.Core.Expr Data.Void.Void a)
instance Dhall.Binary.ToTerm Dhall.Core.Import
instance Dhall.Binary.ToTerm Data.Void.Void
-- | This module provides functionality for concisely displaying the
-- difference between two expressions
--
-- For example, this is used in type errors to explain why the actual
-- type does not match the expected type
module Dhall.Diff
data Diff
Diff :: Bool -> Doc Ann -> Diff
[same] :: Diff -> Bool
[doc] :: Diff -> Doc Ann
-- | Render the difference between the normal form of two expressions
diffNormalized :: (Eq a, Pretty a, ToTerm a) => Expr s a -> Expr s a -> Diff
-- | Render the difference between two expressions
diff :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff
instance GHC.Base.Semigroup Dhall.Diff.Diff
instance GHC.Base.Monoid Dhall.Diff.Diff
instance Data.String.IsString Dhall.Diff.Diff
-- | Shared utility functions
module Dhall.Util
-- | Utility function to cut out the interior of a large text block
snip :: Text -> Text
-- | Like snip, but for Docs
--
-- Note that this has to be opinionated and render ANSI color codes, but
-- that should be fine because we don't use this in a non-interactive
-- context
snipDoc :: Doc Ann -> Doc a
-- | Function to insert an aligned pretty expression
insert :: Pretty a => a -> Doc Ann
-- | Prefix used for error messages
_ERROR :: IsString string => string
-- | This module contains the logic for type checking Dhall code
module Dhall.TypeCheck
-- | Type-check an expression and return the expression's type if
-- type-checking succeeds or an error if type-checking fails
--
-- typeWith does not necessarily normalize the type since full
-- normalization is not necessary for just type-checking. If you actually
-- care about the returned type then you may want to normalize it
-- afterwards.
--
-- The supplied Context records the types of the names in scope.
-- If these are ill-typed, the return value may be ill-typed.
typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)
-- | typeOf is the same as typeWith with an empty context,
-- meaning that the expression must be closed (i.e. no free variables),
-- otherwise type-checking will fail.
typeOf :: Expr s X -> Either (TypeError s X) (Expr s X)
-- | Generalization of typeWith that allows type-checking the
-- Embed constructor with custom logic
typeWithA :: (Eq a, Pretty a) => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a)
-- | This function verifies that a custom context is well-formed so that
-- type-checking will not loop
--
-- Note that typeWith already calls checkContext for you on
-- the Context that you supply
checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
-- | Function that converts the value inside an Embed constructor
-- into a new expression
type Typer a = forall s. a -> Expr s a
type X = Void
-- | Since Void values logically don't exist, this witnesses the
-- logical reasoning tool of "ex falso quodlibet".
--
--
-- >>> let x :: Either Void Int; x = Right 5
--
-- >>> :{
-- case x of
-- Right r -> r
-- Left l -> absurd l
-- :}
-- 5
--
absurd :: () => Void -> a
-- | A structured type error that includes context
data TypeError s a
TypeError :: Context (Expr s a) -> Expr s a -> TypeMessage s a -> TypeError s a
[context] :: TypeError s a -> Context (Expr s a)
[current] :: TypeError s a -> Expr s a
[typeMessage] :: TypeError s a -> TypeMessage s a
-- | Newtype used to wrap error messages so that they render with a more
-- detailed explanation of what went wrong
newtype DetailedTypeError s a
DetailedTypeError :: TypeError s a -> DetailedTypeError s a
-- | The specific type error
data TypeMessage s a
UnboundVariable :: Text -> TypeMessage s a
InvalidInputType :: Expr s a -> TypeMessage s a
InvalidOutputType :: Expr s a -> TypeMessage s a
NotAFunction :: Expr s a -> Expr s a -> TypeMessage s a
TypeMismatch :: Expr s a -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
AnnotMismatch :: Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
Untyped :: TypeMessage s a
MissingListType :: TypeMessage s a
MismatchedListElements :: Int -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidListElement :: Int -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidListType :: Expr s a -> TypeMessage s a
InvalidSome :: Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidPredicate :: Expr s a -> Expr s a -> TypeMessage s a
IfBranchMismatch :: Expr s a -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
IfBranchMustBeTerm :: Bool -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidFieldType :: Text -> Expr s a -> TypeMessage s a
InvalidAlternativeType :: Text -> Expr s a -> TypeMessage s a
AlternativeAnnotationMismatch :: Text -> Expr s a -> Const -> Text -> Expr s a -> Const -> TypeMessage s a
ListAppendMismatch :: Expr s a -> Expr s a -> TypeMessage s a
MustCombineARecord :: Char -> Expr s a -> Expr s a -> TypeMessage s a
CombineTypesRequiresRecordType :: Expr s a -> Expr s a -> TypeMessage s a
RecordTypeMismatch :: Const -> Const -> Expr s a -> Expr s a -> TypeMessage s a
FieldCollision :: Text -> TypeMessage s a
MustMergeARecord :: Expr s a -> Expr s a -> TypeMessage s a
MustMergeUnion :: Expr s a -> Expr s a -> TypeMessage s a
MustMapARecord :: Expr s a -> Expr s a -> TypeMessage s a
InvalidToMapRecordKind :: Expr s a -> Expr s a -> TypeMessage s a
HeterogenousRecordToMap :: Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidToMapType :: Expr s a -> TypeMessage s a
MapTypeMismatch :: Expr s a -> Expr s a -> TypeMessage s a
MissingToMapType :: TypeMessage s a
UnusedHandler :: Set Text -> TypeMessage s a
MissingHandler :: Set Text -> TypeMessage s a
HandlerInputTypeMismatch :: Text -> Expr s a -> Expr s a -> TypeMessage s a
HandlerOutputTypeMismatch :: Text -> Expr s a -> Text -> Expr s a -> TypeMessage s a
InvalidHandlerOutputType :: Text -> Expr s a -> Expr s a -> TypeMessage s a
MissingMergeType :: TypeMessage s a
HandlerNotAFunction :: Text -> Expr s a -> TypeMessage s a
CantAccess :: Text -> Expr s a -> Expr s a -> TypeMessage s a
CantProject :: Text -> Expr s a -> Expr s a -> TypeMessage s a
CantProjectByExpression :: Expr s a -> TypeMessage s a
MissingField :: Text -> Expr s a -> TypeMessage s a
MissingConstructor :: Text -> Expr s a -> TypeMessage s a
ProjectionTypeMismatch :: Text -> Expr s a -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
AssertionFailed :: Expr s a -> Expr s a -> TypeMessage s a
NotAnEquivalence :: Expr s a -> TypeMessage s a
IncomparableExpression :: Expr s a -> TypeMessage s a
EquivalenceTypeMismatch :: Expr s a -> Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
CantAnd :: Expr s a -> Expr s a -> TypeMessage s a
CantOr :: Expr s a -> Expr s a -> TypeMessage s a
CantEQ :: Expr s a -> Expr s a -> TypeMessage s a
CantNE :: Expr s a -> Expr s a -> TypeMessage s a
CantInterpolate :: Expr s a -> Expr s a -> TypeMessage s a
CantTextAppend :: Expr s a -> Expr s a -> TypeMessage s a
CantListAppend :: Expr s a -> Expr s a -> TypeMessage s a
CantAdd :: Expr s a -> Expr s a -> TypeMessage s a
CantMultiply :: Expr s a -> Expr s a -> TypeMessage s a
instance (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Dhall.TypeCheck.TypeMessage s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a) => GHC.Show.Show (Dhall.TypeCheck.DetailedTypeError s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a, Data.Typeable.Internal.Typeable s, Data.Typeable.Internal.Typeable a) => GHC.Exception.Type.Exception (Dhall.TypeCheck.DetailedTypeError s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a) => Data.Text.Prettyprint.Doc.Internal.Pretty (Dhall.TypeCheck.DetailedTypeError s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a) => GHC.Show.Show (Dhall.TypeCheck.TypeError s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a, Data.Typeable.Internal.Typeable s, Data.Typeable.Internal.Typeable a) => GHC.Exception.Type.Exception (Dhall.TypeCheck.TypeError s a)
instance (GHC.Classes.Eq a, Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Dhall.Binary.ToTerm a) => Data.Text.Prettyprint.Doc.Internal.Pretty (Dhall.TypeCheck.TypeError s a)
-- | Dhall lets you import external expressions located either in local
-- files or hosted on network endpoints.
--
-- To import a local file as an expression, just insert the path to the
-- file, prepending a ./ if the path is relative to the current
-- directory. For example, if you create a file named id with
-- the following contents:
--
--
-- $ cat id
-- λ(a : Type) → λ(x : a) → x
--
--
-- Then you can use the file directly within a dhall program
-- just by referencing the file's path:
--
--
-- $ dhall
-- ./id Bool True
-- <Ctrl-D>
-- Bool
--
-- True
--
--
-- Imported expressions may contain imports of their own, too, which will
-- continue to be resolved. However, Dhall will prevent cyclic imports.
-- For example, if you had these two files:
--
--
-- $ cat foo
-- ./bar
--
--
--
-- $ cat bar
-- ./foo
--
--
-- ... Dhall would throw the following exception if you tried to import
-- foo:
--
--
-- $ dhall
-- ./foo
-- ^D
-- ↳ ./foo
-- ↳ ./bar
--
-- Cyclic import: ./foo
--
--
-- You can also import expressions hosted on network endpoints. Just use
-- the URL
--
--
-- http://host[:port]/path
--
--
-- The compiler expects the downloaded expressions to be in the same
-- format as local files, specifically UTF8-encoded source code text.
--
-- For example, if our id expression were hosted at
-- http://example.com/id, then we would embed the
-- expression within our code using:
--
--
-- http://example.com/id
--
--
-- You can also import expressions stored within environment variables
-- using env:NAME, where NAME is the name of the
-- environment variable. For example:
--
--
-- $ export FOO=1
-- $ export BAR='"Hi"'
-- $ export BAZ='λ(x : Bool) → x == False'
-- $ dhall <<< "{ foo = env:FOO , bar = env:BAR , baz = env:BAZ }"
-- { bar : Text, baz : ∀(x : Bool) → Bool, foo : Integer }
--
-- { bar = "Hi", baz = λ(x : Bool) → x == False, foo = 1 }
--
--
-- If you wish to import the raw contents of an impoert as Text
-- then add as Text to the end of the import:
--
--
-- $ dhall <<< "http://example.com as Text"
-- Text
--
-- "<!doctype html>\n<html>\n<head>\n <title>Example Domain</title>\n\n <meta
-- charset=\"utf-8\" />\n <meta http-equiv=\"Content-type\" content=\"text/html
-- ; charset=utf-8\" />\n <meta name=\"viewport\" content=\"width=device-width,
-- initial-scale=1\" />\n <style type=\"text/css\">\n body {\n backgro
-- und-color: #f0f0f2;\n margin: 0;\n padding: 0;\n font-famil
-- y: \"Open Sans\", \"Helvetica Neue\", Helvetica, Arial, sans-serif;\n \n
-- }\n div {\n width: 600px;\n margin: 5em auto;\n paddi
-- ng: 50px;\n background-color: #fff;\n border-radius: 1em;\n }\n
-- a:link, a:visited {\n color: #38488f;\n text-decoration: none;
-- \n }\n @media (max-width: 700px) {\n body {\n background
-- -color: #fff;\n }\n div {\n width: auto;\n m
-- argin: 0 auto;\n border-radius: 0;\n padding: 1em;\n
-- }\n }\n </style> \n</head>\n\n<body>\n<div>\n <h1>Example Domain</
-- h1>\n <p>This domain is established to be used for illustrative examples in d
-- ocuments. You may use this\n domain in examples without prior coordination or
-- asking for permission.</p>\n <p><a href=\"http://www.iana.org/domains/exampl
-- e\">More information...</a></p>\n</div>\n</body>\n</html>\n"
--
module Dhall.Import
-- | Resolve all imports within an expression
load :: Expr Src Import -> IO (Expr Src X)
-- | Resolve all imports within an expression, importing relative to the
-- given directory.
loadRelativeTo :: FilePath -> SemanticCacheMode -> Expr Src Import -> IO (Expr Src X)
-- | Generalized version of load
--
-- You can configure the desired behavior through the initial
-- Status that you supply
loadWith :: Expr Src Import -> StateT Status IO (Expr Src X)
-- | Construct the file path corresponding to a local import. If the import
-- is _relative_ then the resulting path is also relative.
localToPath :: MonadIO io => FilePrefix -> File -> io FilePath
-- | Hash a fully resolved expression
hashExpression :: Expr s X -> Digest SHA256
-- | Convenience utility to hash a fully resolved expression and return the
-- base-16 encoded hash with the sha256: prefix
--
-- In other words, the output of this function can be pasted into Dhall
-- source code to add an integrity check to an import
hashExpressionToCode :: Expr s X -> Text
-- | Ensure that the given expression is present in the semantic cache. The
-- given expression should be alpha-beta-normal.
writeExpressionToSemanticCache :: Expr Src X -> IO ()
-- | Assert than an expression is import-free
assertNoImports :: MonadIO io => Expr Src Import -> io (Expr Src X)
-- | State threaded throughout the import process
data Status
data SemanticCacheMode
IgnoreSemanticCache :: SemanticCacheMode
UseSemanticCache :: SemanticCacheMode
-- | A fully chained import, i.e. if it contains a relative path
-- that path is relative to the current directory. If it is a remote
-- import with headers those are well-typed (either of type `List {
-- header : Text, value Text}` or `List { mapKey : Text, mapValue Text})`
-- and in normal form. These invariants are preserved by the API exposed
-- by Dhall.Import.
data Chained
chainedImport :: Chained -> Import
-- | Given a Local import construct the corresponding unhashed
-- Chained import (interpreting relative path as relative to the
-- current directory).
chainedFromLocalHere :: FilePrefix -> File -> ImportMode -> Chained
-- | Adjust the import mode of a chained import
chainedChangeMode :: ImportMode -> Chained -> Chained
-- | Default starting Status, importing relative to the given
-- directory.
emptyStatus :: FilePath -> Status
stack :: Functor f => LensLike' f Status (NonEmpty Chained)
cache :: Functor f => LensLike' f Status (Map Chained ImportSemantics)
-- | parent imports (i.e. depends on) child
data Depends
Depends :: Chained -> Chained -> Depends
[parent] :: Depends -> Chained
[child] :: Depends -> Chained
graph :: Functor f => LensLike' f Status [Depends]
remote :: Functor f => LensLike' f Status (URL -> StateT Status IO Text)
-- | Given a well-typed (of type `List { header : Text, value Text }` or
-- `List { mapKey : Text, mapValue Text }`) headers expressions in normal
-- form construct the corresponding binary http headers; otherwise return
-- the empty list.
toHeaders :: Expr s a -> [HTTPHeader]
normalizer :: Functor f => LensLike' f Status (Maybe (ReifiedNormalizer X))
startingContext :: Functor f => LensLike' f Status (Context (Expr Src X))
chainImport :: Chained -> Import -> StateT Status IO Chained
data ImportSemantics
-- | An import failed because of a cycle in the import graph
newtype Cycle
Cycle :: Import -> Cycle
-- | The offending cyclic import
[cyclicImport] :: Cycle -> Import
-- | Dhall tries to ensure that all expressions hosted on network endpoints
-- are weakly referentially transparent, meaning roughly that any two
-- clients will compile the exact same result given the same URL.
--
-- To be precise, a strong interpretaton of referential transparency
-- means that if you compiled a URL you could replace the expression
-- hosted at that URL with the compiled result. Let's call this "static
-- linking". Dhall (very intentionally) does not satisfy this stronger
-- interpretation of referential transparency since "statically linking"
-- an expression (i.e. permanently resolving all imports) means that the
-- expression will no longer update if its dependencies change.
--
-- In general, either interpretation of referential transparency is not
-- enforceable in a networked context since one can easily violate
-- referential transparency with a custom DNS, but Dhall can still try to
-- guard against common unintentional violations. To do this, Dhall
-- enforces that a non-local import may not reference a local import.
--
-- Local imports are defined as:
--
--
-- - A file
-- - A URL with a host of localhost or 127.0.0.1
--
--
-- All other imports are defined to be non-local
newtype ReferentiallyOpaque
ReferentiallyOpaque :: Import -> ReferentiallyOpaque
-- | The offending opaque import
[opaqueImport] :: ReferentiallyOpaque -> Import
-- | Extend another exception with the current import stack
data Imported e
Imported :: NonEmpty Chained -> e -> Imported e
-- | Imports resolved so far, in reverse order
[importStack] :: Imported e -> NonEmpty Chained
-- | The nested exception
[nested] :: Imported e -> e
-- | A call to assertNoImports failed because there was at least one
-- import
data ImportResolutionDisabled
ImportResolutionDisabled :: ImportResolutionDisabled
-- | Wrapper around HttpExceptions with a prettier Show
-- instance.
--
-- In order to keep the library API constant even when the
-- with-http Cabal flag is disabled the pretty error message is
-- pre-rendered and the real HttpExcepion is stored in a
-- Dynamic
data PrettyHttpException
PrettyHttpException :: String -> Dynamic -> PrettyHttpException
-- | Exception thrown when an imported file is missing
data MissingFile
MissingFile :: FilePath -> MissingFile
-- | Exception thrown when an environment variable is missing
newtype MissingEnvironmentVariable
MissingEnvironmentVariable :: Text -> MissingEnvironmentVariable
[name] :: MissingEnvironmentVariable -> Text
-- | List of Exceptions we encounter while resolving Import Alternatives
newtype MissingImports
MissingImports :: [SomeException] -> MissingImports
-- | Exception thrown when an integrity check fails
data HashMismatch
HashMismatch :: Digest SHA256 -> Digest SHA256 -> HashMismatch
[expectedHash] :: HashMismatch -> Digest SHA256
[actualHash] :: HashMismatch -> Digest SHA256
instance GHC.Exception.Type.Exception Dhall.Import.ImportResolutionDisabled
instance GHC.Show.Show Dhall.Import.ImportResolutionDisabled
instance GHC.Exception.Type.Exception Dhall.Import.HashMismatch
instance GHC.Show.Show Dhall.Import.HashMismatch
instance Dhall.Import.Canonicalize Dhall.Core.Directory
instance Dhall.Import.Canonicalize Dhall.Core.File
instance Dhall.Import.Canonicalize Dhall.Core.ImportType
instance Dhall.Import.Canonicalize Dhall.Core.ImportHashed
instance Dhall.Import.Canonicalize Dhall.Core.Import
instance GHC.Exception.Type.Exception Dhall.Import.CannotImportHTTPURL
instance GHC.Show.Show Dhall.Import.CannotImportHTTPURL
instance GHC.Exception.Type.Exception Dhall.Import.MissingImports
instance GHC.Show.Show Dhall.Import.MissingImports
instance GHC.Exception.Type.Exception Dhall.Import.MissingEnvironmentVariable
instance GHC.Show.Show Dhall.Import.MissingEnvironmentVariable
instance GHC.Exception.Type.Exception Dhall.Import.MissingFile
instance GHC.Show.Show Dhall.Import.MissingFile
instance GHC.Exception.Type.Exception e => GHC.Exception.Type.Exception (Dhall.Import.Imported e)
instance GHC.Show.Show e => GHC.Show.Show (Dhall.Import.Imported e)
instance GHC.Exception.Type.Exception Dhall.Import.ReferentiallyOpaque
instance GHC.Show.Show Dhall.Import.ReferentiallyOpaque
instance GHC.Exception.Type.Exception Dhall.Import.Cycle
instance GHC.Show.Show Dhall.Import.Cycle
-- | This module contains the implementation of the dhall hash
-- subcommand
module Dhall.Hash
-- | Implementation of the dhall hash subcommand
hash :: IO ()
-- | This module contains the implementation of the dhall freeze
-- subcommand
module Dhall.Freeze
-- | Implementation of the dhall freeze subcommand
freeze :: Maybe FilePath -> Scope -> Intent -> CharacterSet -> IO ()
-- | Retrieve an Import and update the hash to match the latest
-- contents
freezeImport :: FilePath -> Import -> IO Import
-- | Freeze an import only if the import is a Remote import
freezeRemoteImport :: FilePath -> Import -> IO Import
-- | Specifies which imports to freeze
data Scope
-- | Freeze only remote imports (i.e. URLs)
OnlyRemoteImports :: Scope
-- | Freeze all imports (including paths and environment variables)
AllImports :: Scope
-- | Specifies why we are adding semantic integrity checks
data Intent
-- | Protect imports with an integrity check without a fallback so that
-- import resolution fails if the import changes
Secure :: Intent
-- | Protect imports with an integrity check and also add a fallback import
-- import without an integrity check. This is useful if you only want to
-- cache imports when possible but still gracefully degrade to resolving
-- them if the semantic integrity check has changed.
Cache :: Intent
-- | Please read the Dhall.Tutorial module, which contains a
-- tutorial explaining how to use the language, the compiler, and this
-- library
module Dhall
-- | Type-check and evaluate a Dhall program, decoding the result into
-- Haskell
--
-- The first argument determines the type of value that you decode:
--
--
-- >>> input integer "+2"
-- 2
--
-- >>> input (vector double) "[1.0, 2.0]"
-- [1.0,2.0]
--
--
-- Use auto to automatically select which type to decode based on
-- the inferred return type:
--
--
-- >>> input auto "True" :: IO Bool
-- True
--
--
-- This uses the settings from defaultInputSettings.
input :: Type a -> Text -> IO a
-- | Extend input with a root directory to resolve imports relative
-- to, a file to mention in errors as the source, a custom typing
-- context, and a custom normalization process.
inputWithSettings :: InputSettings -> Type a -> Text -> IO a
-- | Type-check and evaluate a Dhall program that is read from the
-- file-system.
--
-- This uses the settings from defaultEvaluateSettings.
inputFile :: Type a -> FilePath -> IO a
-- | Extend inputFile with a custom typing context and a custom
-- normalization process.
inputFileWithSettings :: EvaluateSettings -> Type a -> FilePath -> IO a
-- | Similar to input, but without interpreting the Dhall
-- Expr into a Haskell type.
--
-- Uses the settings from defaultInputSettings.
inputExpr :: Text -> IO (Expr Src X)
-- | Extend inputExpr with a root directory to resolve imports
-- relative to, a file to mention in errors as the source, a custom
-- typing context, and a custom normalization process.
inputExprWithSettings :: InputSettings -> Text -> IO (Expr Src X)
-- | Access the directory to resolve imports relative to.
rootDirectory :: Functor f => LensLike' f InputSettings FilePath
-- | Access the name of the source to report locations from; this is only
-- used in error messages, so it's okay if this is a best guess or
-- something symbolic.
sourceName :: Functor f => LensLike' f InputSettings FilePath
-- | Access the starting context used for evaluation and type-checking.
startingContext :: (Functor f, HasEvaluateSettings s) => LensLike' f s (Context (Expr Src X))
-- | Access the custom normalizer.
normalizer :: (Functor f, HasEvaluateSettings s) => LensLike' f s (Maybe (ReifiedNormalizer X))
-- | Default input settings: resolves imports relative to . (the
-- current working directory), report errors as coming from
-- (input), and default evaluation settings from
-- defaultEvaluateSettings.
defaultInputSettings :: InputSettings
data InputSettings
-- | Default evaluation settings: no extra entries in the initial context,
-- and no special normalizer behaviour.
defaultEvaluateSettings :: EvaluateSettings
data EvaluateSettings
class HasEvaluateSettings s
-- | Use this to provide more detailed error messages
--
--
-- > input auto "True" :: IO Integer
-- *** Exception: Error: Expression doesn't match annotation
--
-- True : Integer
--
-- (input):1:1
--
--
--
-- > detailed (input auto "True") :: IO Integer
-- *** Exception: Error: Expression doesn't match annotation
--
-- Explanation: You can annotate an expression with its type or kind using the
-- ❰:❱ symbol, like this:
--
--
-- ┌───────┐
-- │ x : t │ ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
-- └───────┘
--
-- The type checker verifies that the expression's type or kind matches the
-- provided annotation
--
-- For example, all of the following are valid annotations that the type checker
-- accepts:
--
--
-- ┌─────────────┐
-- │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type
-- └─────────────┘ checker accepts the annotation
--
--
-- ┌───────────────────────┐
-- │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type
-- └───────────────────────┘ checker accepts the annotation
--
--
-- ┌────────────────────┐
-- │ List : Type → Type │ ❰List❱ is an expression that has kind ❰Type → Type❱,
-- └────────────────────┘ so the type checker accepts the annotation
--
--
-- ┌──────────────────┐
-- │ List Text : Type │ ❰List Text❱ is an expression that has kind ❰Type❱, so
-- └──────────────────┘ the type checker accepts the annotation
--
--
-- However, the following annotations are not valid and the type checker will
-- reject them:
--
--
-- ┌──────────┐
-- │ 1 : Text │ The type checker rejects this because ❰1❱ does not have type
-- └──────────┘ ❰Text❱
--
--
-- ┌─────────────┐
-- │ List : Type │ ❰List❱ does not have kind ❰Type❱
-- └─────────────┘
--
--
-- You or the interpreter annotated this expression:
--
-- ↳ True
--
-- ... with this type or kind:
--
-- ↳ Integer
--
-- ... but the inferred type or kind of the expression is actually:
--
-- ↳ Bool
--
-- Some common reasons why you might get this error:
--
-- ● The Haskell Dhall interpreter implicitly inserts a top-level annotation
-- matching the expected type
--
-- For example, if you run the following Haskell code:
--
--
-- ┌───────────────────────────────┐
-- │ >>> input auto "1" :: IO Text │
-- └───────────────────────────────┘
--
--
-- ... then the interpreter will actually type check the following annotated
-- expression:
--
--
-- ┌──────────┐
-- │ 1 : Text │
-- └──────────┘
--
--
-- ... and then type-checking will fail
--
-- ────────────────────────────────────────────────────────────────────────────────
--
-- True : Integer
--
-- (input):1:1
--
detailed :: IO a -> IO a
-- | A (Type a) represents a way to marshal a value of type
-- 'a' from Dhall into Haskell
--
-- You can produce Types either explicitly:
--
--
-- example :: Type (Vector Text)
-- example = vector text
--
--
-- ... or implicitly using auto:
--
--
-- example :: Type (Vector Text)
-- example = auto
--
--
-- You can consume Types using the input function:
--
--
-- input :: Type a -> Text -> IO a
--
data Type a
Type :: (Expr Src X -> Extractor Src X a) -> Expr Src X -> Type a
-- | Extracts Haskell value from the Dhall expression
[extract] :: Type a -> Expr Src X -> Extractor Src X a
-- | Dhall type of the Haskell value
[expected] :: Type a -> Expr Src X
-- | The RecordType applicative functor allows you to build a
-- Type parser from a Dhall record.
--
-- For example, let's take the following Haskell data type:
--
--
-- >>> :{
-- data Project = Project
-- { projectName :: Text
-- , projectDescription :: Text
-- , projectStars :: Natural
-- }
-- :}
--
--
-- And assume that we have the following Dhall record that we would like
-- to parse as a Project:
--
--
-- { name =
-- "dhall-haskell"
-- , description =
-- "A configuration language guaranteed to terminate"
-- , stars =
-- 289
-- }
--
--
-- Our parser has type Type Project, but we can't build
-- that out of any smaller parsers, as Types cannot be combined
-- (they are only Functors). However, we can use a
-- RecordType to build a Type for Project:
--
--
-- >>> :{
-- project :: Type Project
-- project =
-- record
-- ( Project <$> field "name" strictText
-- <*> field "description" strictText
-- <*> field "stars" natural
-- )
-- :}
--
newtype RecordType a
RecordType :: Product (Const (Map Text (Expr Src X))) (Compose ((->) (Expr Src X)) (Extractor Src X)) a -> RecordType a
-- | The UnionType monoid allows you to build a Type parser
-- from a Dhall union
--
-- For example, let's take the following Haskell data type:
--
--
-- >>> :{
-- data Status = Queued Natural
-- | Result Text
-- | Errored Text
-- :}
--
--
-- And assume that we have the following Dhall union that we would like
-- to parse as a Status:
--
--
-- < Result : Text
-- | Queued : Natural
-- | Errored : Text
-- >.Result "Finish successfully"
--
--
-- Our parser has type Type Status, but we can't build
-- that out of any smaller parsers, as Types cannot be combined
-- (they are only Functors). However, we can use a
-- UnionType to build a Type for Status:
--
--
-- >>> :{
-- status :: Type Status
-- status = union
-- ( ( Queued <$> constructor "Queued" natural )
-- <> ( Result <$> constructor "Result" strictText )
-- <> ( Errored <$> constructor "Errored" strictText )
-- )
-- :}
--
newtype UnionType a
UnionType :: Compose (Map Text) Type a -> UnionType a
-- | An (InputType a) represents a way to marshal a value of type
-- 'a' from Haskell into Dhall
data InputType a
InputType :: (a -> Expr Src X) -> Expr Src X -> InputType a
-- | Embeds a Haskell value as a Dhall expression
[embed] :: InputType a -> a -> Expr Src X
-- | Dhall type of the Haskell value
[declared] :: InputType a -> Expr Src X
-- | Any value that implements Interpret can be automatically
-- decoded based on the inferred return type of input
--
--
-- >>> input auto "[1, 2, 3]" :: IO (Vector Natural)
-- [1,2,3]
--
--
-- This class auto-generates a default implementation for records that
-- implement Generic. This does not auto-generate an instance for
-- recursive types.
class Interpret a
autoWith :: Interpret a => InterpretOptions -> Type a
autoWith :: (Interpret a, Generic a, GenericInterpret (Rep a)) => InterpretOptions -> Type a
-- | Every Type must obey the contract that if an expression's type
-- matches the the expected type then the extract function
-- must not fail with a type error. If not, then this value is returned.
--
-- This value indicates that an invalid Type was provided to the
-- input function
data InvalidType s a
InvalidType :: Expr s a -> Expr s a -> InvalidType s a
[invalidTypeExpected] :: InvalidType s a -> Expr s a
[invalidTypeExpression] :: InvalidType s a -> Expr s a
newtype ExtractErrors s a
ExtractErrors :: NonEmpty (ExtractError s a) -> ExtractErrors s a
[getErrors] :: ExtractErrors s a -> NonEmpty (ExtractError s a)
type Extractor s a = Validation (ExtractErrors s a)
type MonadicExtractor s a = Either (ExtractErrors s a)
typeError :: Expr s a -> Expr s a -> Extractor s a b
extractError :: Text -> Extractor s a b
-- | 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
-- | Switches from a Monad extraction result, able to chain
-- sequential errors, to an Applicative extraction result, able
-- to accumulate errors
fromMonadic :: MonadicExtractor s a b -> Extractor s a b
-- | Use the default options for interpreting a configuration file
--
--
-- auto = autoWith defaultInterpretOptions
--
auto :: Interpret a => Type a
-- | genericAuto is the default implementation for auto if
-- you derive Interpret. The difference is that you can use
-- genericAuto without having to explicitly provide an
-- Interpret instance for a type as long as the type derives
-- Generic
genericAuto :: (Generic a, GenericInterpret (Rep a)) => Type a
-- | Use these options to tweak how Dhall derives a generic implementation
-- of Interpret
data InterpretOptions
InterpretOptions :: (Text -> Text) -> (Text -> Text) -> ReifiedNormalizer X -> InterpretOptions
-- | Function used to transform Haskell field names into their
-- corresponding Dhall field names
[fieldModifier] :: InterpretOptions -> Text -> Text
-- | Function used to transform Haskell constructor names into their
-- corresponding Dhall alternative names
[constructorModifier] :: InterpretOptions -> Text -> Text
-- | This is only used by the Interpret instance for functions in
-- order to normalize the function input before marshaling the input into
-- a Dhall expression
[inputNormalizer] :: InterpretOptions -> ReifiedNormalizer X
-- | Default interpret options, which you can tweak or override, like this:
--
--
-- autoWith
-- (defaultInterpretOptions { fieldModifier = Data.Text.Lazy.dropWhile (== '_') })
--
defaultInterpretOptions :: InterpretOptions
-- | Decode a Expr
--
--
-- >>> input bool "True"
-- True
--
bool :: Type Bool
-- | Decode a Expr
--
--
-- >>> input natural "42"
-- 42
--
natural :: Type Natural
-- | Decode an Expr
--
--
-- >>> input integer "+42"
-- 42
--
integer :: Type Integer
-- | Decode a Scientific
--
--
-- >>> input scientific "1e100"
-- 1.0e100
--
scientific :: Type Scientific
-- | Decode a Expr
--
--
-- >>> input double "42.0"
-- 42.0
--
double :: Type Double
-- | Decode lazy Expr
--
--
-- >>> input lazyText "\"Test\""
-- "Test"
--
lazyText :: Type Text
-- | Decode strict Expr
--
--
-- >>> input strictText "\"Test\""
-- "Test"
--
strictText :: Type Text
-- | Decode a Maybe
--
--
-- >>> input (maybe natural) "Some 1"
-- Just 1
--
maybe :: Type a -> Type (Maybe a)
-- | Decode a Seq
--
--
-- >>> input (sequence natural) "[1, 2, 3]"
-- fromList [1,2,3]
--
sequence :: Type a -> Type (Seq a)
-- | Decode a list
--
--
-- >>> input (list natural) "[1, 2, 3]"
-- [1,2,3]
--
list :: Type a -> Type [a]
-- | Decode a Vector
--
--
-- >>> input (vector natural) "[1, 2, 3]"
-- [1,2,3]
--
vector :: Type a -> Type (Vector a)
-- | Decode () from an empty record.
--
--
-- >>> input unit "{=}" -- GHC doesn't print the result if it is ()
--
unit :: Type ()
-- | Decode a String
--
--
-- >>> input string "\"ABC\""
-- "ABC"
--
string :: Type String
-- | Given a pair of Types, decode a tuple-record into their
-- pairing.
--
--
-- >>> input (pair natural bool) "{ _1 = 42, _2 = False }"
-- (42,False)
--
pair :: Type a -> Type b -> Type (a, b)
-- | Run a RecordType parser to build a Type parser.
record :: RecordType a -> Type a
-- | Parse a single field of a record.
field :: Text -> Type a -> RecordType a
-- | Run a UnionType parser to build a Type parser.
union :: UnionType a -> Type a
-- | Parse a single constructor of a union
constructor :: Text -> Type a -> UnionType a
-- | This is the underlying class that powers the Interpret class's
-- support for automatically deriving a generic implementation
class GenericInterpret f
genericAutoWith :: GenericInterpret f => InterpretOptions -> State Int (Type (f a))
-- | This is the underlying class that powers the Interpret class's
-- support for automatically deriving a generic implementation
class GenericInject f
genericInjectWith :: GenericInject f => InterpretOptions -> State Int (InputType (f a))
-- | This class is used by Interpret instance for functions:
--
--
-- instance (Inject a, Interpret b) => Interpret (a -> b)
--
--
-- You can convert Dhall functions with "simple" inputs (i.e. instances
-- of this class) into Haskell functions. This works by:
--
--
-- - Marshaling the input to the Haskell function into a Dhall
-- expression (i.e. x :: Expr Src X)
-- - Applying the Dhall function (i.e. f :: Expr Src X) to the
-- Dhall input (i.e. App f x)
-- - Normalizing the syntax tree (i.e. normalize (App f
-- x))
-- - Marshaling the resulting Dhall expression back into a Haskell
-- value
--
class Inject a
injectWith :: Inject a => InterpretOptions -> InputType a
injectWith :: (Inject a, Generic a, GenericInject (Rep a)) => InterpretOptions -> InputType a
-- | Use the default options for injecting a value
--
--
-- inject = inject defaultInterpretOptions
--
inject :: Inject a => InputType a
-- | Use the default options for injecting a value, whose structure is
-- determined generically.
--
-- This can be used when you want to use Inject on types that you
-- don't want to define orphan instances for.
genericInject :: (Generic a, GenericInject (Rep a)) => InputType a
newtype RecordInputType a
RecordInputType :: Map Text (InputType a) -> RecordInputType a
inputFieldWith :: Text -> InputType a -> RecordInputType a
inputField :: Inject a => Text -> RecordInputType a
inputRecord :: RecordInputType a -> InputType a
-- | UnionInputType allows you to build an InputType injector
-- for a Dhall record.
--
-- For example, let's take the following Haskell data type:
--
--
-- >>> :{
-- data Status = Queued Natural
-- | Result Text
-- | Errored Text
-- :}
--
--
-- And assume that we have the following Dhall union that we would like
-- to parse as a Status:
--
--
-- < Result : Text
-- | Queued : Natural
-- | Errored : Text
-- >.Result "Finish successfully"
--
--
-- Our injector has type InputType Status, but we can't
-- build that out of any smaller injectors, as InputTypes cannot
-- be combined. However, we can use an UnionInputType to build an
-- InputType for Status:
--
--
-- >>> :{
-- injectStatus :: InputType Status
-- injectStatus = adapt >$< inputUnion
-- ( inputConstructorWith "Queued" inject
-- >|< inputConstructorWith "Result" inject
-- >|< inputConstructorWith "Errored" inject
-- )
-- where
-- adapt (Queued n) = Left n
-- adapt (Result t) = Right (Left t)
-- adapt (Errored e) = Right (Right e)
-- :}
--
--
-- Or, since we are simply using the Inject instance to inject
-- each branch, we could write
--
--
-- >>> :{
-- injectStatus :: InputType Status
-- injectStatus = adapt >$< inputUnion
-- ( inputConstructor "Queued"
-- >|< inputConstructor "Result"
-- >|< inputConstructor "Errored"
-- )
-- where
-- adapt (Queued n) = Left n
-- adapt (Result t) = Right (Left t)
-- adapt (Errored e) = Right (Right e)
-- :}
--
newtype UnionInputType a
UnionInputType :: Product (Const (Map Text (Expr Src X))) (Op (Text, Expr Src X)) a -> UnionInputType a
inputConstructorWith :: Text -> InputType a -> UnionInputType a
inputConstructor :: Inject a => Text -> UnionInputType a
inputUnion :: UnionInputType a -> InputType a
-- | Combines two UnionInputType values. See UnionInputType
-- for usage notes.
--
-- Ideally, this matches chosen; however, this allows
-- UnionInputType to not need a Divisible instance itself
-- (since no instance is possible).
(>|<) :: UnionInputType a -> UnionInputType b -> UnionInputType (Either a b)
infixr 5 >|<
-- | Use this function to extract Haskell values directly from Dhall AST.
-- The intended use case is to allow easy extraction of Dhall values for
-- making the function normalizeWith easier to use.
--
-- For other use cases, use input from Dhall module. It
-- will give you a much better user experience.
rawInput :: Alternative f => Type a -> Expr s X -> f a
-- | This is an infix alias for contramap.
(>$<) :: Contravariant f => (a -> b) -> f b -> f a
infixl 4 >$<
-- | The RecordInputType divisible (contravariant) functor allows
-- you to build an InputType injector for a Dhall record.
--
-- For example, let's take the following Haskell data type:
--
--
-- >>> :{
-- data Project = Project
-- { projectName :: Text
-- , projectDescription :: Text
-- , projectStars :: Natural
-- }
-- :}
--
--
-- And assume that we have the following Dhall record that we would like
-- to parse as a Project:
--
--
-- { name =
-- "dhall-haskell"
-- , description =
-- "A configuration language guaranteed to terminate"
-- , stars =
-- 289
-- }
--
--
-- Our injector has type InputType Project, but we can't
-- build that out of any smaller injectors, as InputTypes cannot
-- be combined (they are only Contravariants). However, we can use
-- an InputRecordType to build an InputType for
-- Project:
--
--
-- >>> :{
-- injectProject :: InputType Project
-- injectProject =
-- inputRecord
-- ( adapt >$< inputFieldWith "name" inject
-- >*< inputFieldWith "description" inject
-- >*< inputFieldWith "stars" inject
-- )
-- where
-- adapt (Project{..}) = (projectName, (projectDescription, projectStars))
-- :}
--
--
-- Or, since we are simply using the Inject instance to inject
-- each field, we could write
--
--
-- >>> :{
-- injectProject :: InputType Project
-- injectProject =
-- inputRecord
-- ( adapt >$< inputField "name"
-- >*< inputField "description"
-- >*< inputField "stars"
-- )
-- where
-- adapt (Project{..}) = (projectName, (projectDescription, projectStars))
-- :}
--
--
-- Infix divided
(>*<) :: Divisible f => f a -> f b -> f (a, b)
infixr 5 >*<
-- | Type representing arbitrary-precision non-negative integers.
--
--
-- >>> 2^100 :: Natural
-- 1267650600228229401496703205376
--
--
-- Operations whose result would be negative throw
-- (Underflow :: ArithException),
--
--
-- >>> -1 :: Natural
-- *** Exception: arithmetic underflow
--
data Natural
-- | General-purpose finite sequences.
data Seq a
-- | A space efficient, packed, unboxed Unicode text type.
data Text
-- | Boxed vectors, supporting efficient slicing.
data Vector a
-- | Representable types of kind *. This class is derivable in GHC
-- with the DeriveGeneric flag on.
--
-- A Generic instance must satisfy the following laws:
--
--
-- from . to ≡ id
-- to . from ≡ id
--
class Generic a
instance Data.Functor.Contravariant.Contravariant Dhall.UnionInputType
instance GHC.Base.Functor Dhall.UnionType
instance GHC.Base.Applicative Dhall.RecordType
instance GHC.Base.Functor Dhall.RecordType
instance GHC.Base.Functor Dhall.Type
instance GHC.Base.Semigroup (Dhall.ExtractErrors s a)
instance Data.Functor.Contravariant.Contravariant Dhall.RecordInputType
instance Data.Functor.Contravariant.Divisible.Divisible Dhall.RecordInputType
instance GHC.Base.Semigroup (Dhall.UnionType a)
instance GHC.Base.Monoid (Dhall.UnionType a)
instance (Dhall.Inject a, Dhall.Interpret b) => Dhall.Interpret (a -> b)
instance Dhall.Inject GHC.Types.Bool
instance Dhall.Inject Data.Text.Internal.Lazy.Text
instance Dhall.Inject Data.Text.Internal.Text
instance Dhall.Inject GHC.Base.String
instance Dhall.Inject GHC.Natural.Natural
instance Dhall.Inject GHC.Integer.Type.Integer
instance Dhall.Inject GHC.Types.Int
instance Dhall.Inject GHC.Word.Word8
instance Dhall.Inject GHC.Word.Word16
instance Dhall.Inject GHC.Word.Word32
instance Dhall.Inject GHC.Word.Word64
instance Dhall.Inject GHC.Types.Double
instance Dhall.Inject Data.Scientific.Scientific
instance Dhall.Inject ()
instance Dhall.Inject a => Dhall.Inject (GHC.Maybe.Maybe a)
instance Dhall.Inject a => Dhall.Inject (Data.Sequence.Internal.Seq a)
instance Dhall.Inject a => Dhall.Inject [a]
instance Dhall.Inject a => Dhall.Inject (Data.Vector.Vector a)
instance Dhall.Inject a => Dhall.Inject (Data.Set.Internal.Set a)
instance (Dhall.Inject a, Dhall.Inject b) => Dhall.Inject (a, b)
instance (GHC.Generics.Selector s, Dhall.Inject a) => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
instance forall k (f :: k -> *) (d :: GHC.Generics.Meta). Dhall.GenericInject f => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.D d f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Dhall.GenericInject f => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.C c f)
instance forall k (c1 :: GHC.Generics.Meta) (c2 :: GHC.Generics.Meta) (f1 :: k -> *) (f2 :: k -> *). (GHC.Generics.Constructor c1, GHC.Generics.Constructor c2, Dhall.GenericInject f1, Dhall.GenericInject f2) => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.C c1 f1 GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c2 f2)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *) (g :: k -> *) (h :: k -> *). (GHC.Generics.Constructor c, Dhall.GenericInject (f GHC.Generics.:+: g), Dhall.GenericInject h) => Dhall.GenericInject ((f GHC.Generics.:+: g) GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c h)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *) (g :: k -> *) (h :: k -> *). (GHC.Generics.Constructor c, Dhall.GenericInject f, Dhall.GenericInject (g GHC.Generics.:+: h)) => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.C c f GHC.Generics.:+: (g GHC.Generics.:+: h))
instance forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *). (Dhall.GenericInject (f GHC.Generics.:+: g), Dhall.GenericInject (h GHC.Generics.:+: i)) => Dhall.GenericInject ((f GHC.Generics.:+: g) GHC.Generics.:+: (h GHC.Generics.:+: i))
instance forall k (f :: k -> *) (g :: k -> *). (Dhall.GenericInject f, Dhall.GenericInject g) => Dhall.GenericInject (f GHC.Generics.:*: g)
instance Dhall.GenericInject GHC.Generics.U1
instance Data.Functor.Contravariant.Contravariant Dhall.InputType
instance Dhall.Interpret GHC.Types.Bool
instance Dhall.Interpret GHC.Natural.Natural
instance Dhall.Interpret GHC.Integer.Type.Integer
instance Dhall.Interpret Data.Scientific.Scientific
instance Dhall.Interpret GHC.Types.Double
instance Dhall.Interpret [GHC.Types.Char]
instance Dhall.Interpret Data.Text.Internal.Lazy.Text
instance Dhall.Interpret Data.Text.Internal.Text
instance Dhall.Interpret a => Dhall.Interpret (GHC.Maybe.Maybe a)
instance Dhall.Interpret a => Dhall.Interpret (Data.Sequence.Internal.Seq a)
instance Dhall.Interpret a => Dhall.Interpret [a]
instance Dhall.Interpret a => Dhall.Interpret (Data.Vector.Vector a)
instance (Dhall.Interpret a, Dhall.Interpret b) => Dhall.Interpret (a, b)
instance Dhall.Interpret (f (Dhall.Result f)) => Dhall.Interpret (Dhall.Result f)
instance (GHC.Base.Functor f, Dhall.Interpret (f (Dhall.Result f))) => Dhall.Interpret (Data.Fix.Fix f)
instance (GHC.Generics.Selector s, Dhall.Interpret a) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
instance forall k (f :: k -> *) (d :: GHC.Generics.Meta). Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.D d f)
instance Dhall.GenericInterpret GHC.Generics.V1
instance forall k (c1 :: GHC.Generics.Meta) (c2 :: GHC.Generics.Meta) (f1 :: k -> *) (f2 :: k -> *). (GHC.Generics.Constructor c1, GHC.Generics.Constructor c2, Dhall.GenericInterpret f1, Dhall.GenericInterpret f2) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c1 f1 GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c2 f2)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *) (g :: k -> *) (h :: k -> *). (GHC.Generics.Constructor c, Dhall.GenericInterpret (f GHC.Generics.:+: g), Dhall.GenericInterpret h) => Dhall.GenericInterpret ((f GHC.Generics.:+: g) GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c h)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *) (g :: k -> *) (h :: k -> *). (GHC.Generics.Constructor c, Dhall.GenericInterpret f, Dhall.GenericInterpret (g GHC.Generics.:+: h)) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c f GHC.Generics.:+: (g GHC.Generics.:+: h))
instance forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *). (Dhall.GenericInterpret (f GHC.Generics.:+: g), Dhall.GenericInterpret (h GHC.Generics.:+: i)) => Dhall.GenericInterpret ((f GHC.Generics.:+: g) GHC.Generics.:+: (h GHC.Generics.:+: i))
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c f)
instance Dhall.GenericInterpret GHC.Generics.U1
instance forall k (f :: k -> *) (g :: k -> *). (Dhall.GenericInterpret f, Dhall.GenericInterpret g) => Dhall.GenericInterpret (f GHC.Generics.:*: g)
instance Dhall.HasEvaluateSettings Dhall.InputSettings
instance Dhall.HasEvaluateSettings Dhall.EvaluateSettings
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.Show.Show (Dhall.ExtractErrors s a)
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)
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.Show.Show (Dhall.ExtractError s a)
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.ExtractError s a)
instance (Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Typeable.Internal.Typeable s, Data.Text.Prettyprint.Doc.Internal.Pretty a, Data.Typeable.Internal.Typeable a) => GHC.Exception.Type.Exception (Dhall.InvalidType s a)
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.Show.Show (Dhall.InvalidType s a)
-- | Dhall is a programming language specialized for configuration files.
-- This module contains a tutorial explaining how to author configuration
-- files using this language
module Dhall.Tutorial
-- | This module provides staticDhallExpression which can be used to
-- resolve all of an expression’s imports at compile time, allowing one
-- to reference Dhall expressions from Haskell without having a runtime
-- dependency on the location of Dhall files.
--
-- For example, given a file "./Some/Type.dhall" containing
--
--
-- < This : Natural | Other : ../Other/Type.dhall >
--
--
-- ... rather than duplicating the AST manually in a Haskell Type,
-- you can do:
--
--
-- Dhall.Type
-- (\case
-- UnionLit "This" _ _ -> ...
-- UnionLit "Other" _ _ -> ...)
-- $(staticDhallExpression "./Some/Type.dhall")
--
--
-- This would create the Dhall Expr AST from the
-- "./Some/Type.dhall" file at compile time with all imports
-- resolved, making it easy to keep your Dhall configs and Haskell
-- interpreters in sync.
module Dhall.TH
-- | This fully resolves, type checks, and normalizes the expression, so
-- the resulting AST is self-contained.
staticDhallExpression :: Text -> Q Exp
-- | This module contains the implementation of the dhall repl
-- subcommand
module Dhall.Repl
-- | Implementation of the dhall repl subcommand
repl :: CharacterSet -> Bool -> IO ()
-- | This module contains the top-level entrypoint and options parsing for
-- the dhall executable
module Dhall.Main
-- | Top-level program options
data Options
Options :: Mode -> Bool -> Bool -> Bool -> Options
[mode] :: Options -> Mode
[explain] :: Options -> Bool
[plain] :: Options -> Bool
[ascii] :: Options -> Bool
-- | The subcommands for the dhall executable
data Mode
Default :: Maybe FilePath -> Bool -> Bool -> SemanticCacheMode -> Mode
[file] :: Mode -> Maybe FilePath
[annotate] :: Mode -> Bool
[alpha] :: Mode -> Bool
[semanticCacheMode] :: Mode -> SemanticCacheMode
Version :: Mode
Resolve :: Maybe FilePath -> Maybe ResolveMode -> Mode
[file] :: Mode -> Maybe FilePath
[resolveMode] :: Mode -> Maybe ResolveMode
Type :: Maybe FilePath -> Mode
[file] :: Mode -> Maybe FilePath
Normalize :: Maybe FilePath -> Bool -> Mode
[file] :: Mode -> Maybe FilePath
[alpha] :: Mode -> Bool
Repl :: Mode
Format :: FormatMode -> Mode
[formatMode] :: Mode -> FormatMode
Freeze :: Maybe FilePath -> Bool -> Bool -> Mode
[inplace] :: Mode -> Maybe FilePath
[all_] :: Mode -> Bool
[cache] :: Mode -> Bool
Hash :: Mode
Diff :: Text -> Text -> Mode
[expr1] :: Mode -> Text
[expr2] :: Mode -> Text
Lint :: Maybe FilePath -> Mode
[inplace] :: Mode -> Maybe FilePath
Encode :: Maybe FilePath -> Bool -> Mode
[file] :: Mode -> Maybe FilePath
[json] :: Mode -> Bool
Decode :: Maybe FilePath -> Bool -> Mode
[file] :: Mode -> Maybe FilePath
[json] :: Mode -> Bool
Text :: Maybe FilePath -> Mode
[file] :: Mode -> Maybe FilePath
-- | Parser for the Options type
parseOptions :: Parser Options
-- | ParserInfo for the Options type
parserInfoOptions :: ParserInfo Options
-- | Run the command specified by the Options type
command :: Options -> IO ()
-- | Entry point for the dhall executable
main :: IO ()