-- 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.22.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 -> Integer -> 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 empty = mempty
--
-- fromList (x <|> y) = fromList x <> fromList y
--
--
--
-- >>> 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)]
--
fromList :: 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 :: Ord k => 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
-- | 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)
-- | 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
-- | 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)
-- | Traverse all of the key-value pairs in a Map, in their original
-- order where the result of the computation can be forgotten.
--
--
-- >>> traverseWithKey_ (\k v -> print (k, v)) (fromList [("B",1),("A",2)])
-- ("B",1)
-- ("A",2)
--
traverseWithKey_ :: Ord k => Applicative f => (k -> a -> f ()) -> Map k a -> f ()
-- | Travese 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 an optimisation over traverseWithKey_ since
-- we do not care in what order we traverse the pairs.
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]
instance (Data.Data.Data k, Data.Data.Data v, GHC.Classes.Ord k) => Data.Data.Data (Dhall.Map.Map k v)
instance (GHC.Classes.Eq k, GHC.Classes.Eq v) => GHC.Classes.Eq (Dhall.Map.Map k v)
instance GHC.Base.Functor (Dhall.Map.Map k)
instance Data.Foldable.Foldable (Dhall.Map.Map k)
instance 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)
-- | 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
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]
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.Classes.Ord a => GHC.Classes.Ord (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 Data.Foldable.Foldable Dhall.Set.Set
-- | 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
-- | 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 ImportHashed -> URL
[scheme] :: URL -> Scheme
[authority] :: URL -> Text
[path] :: URL -> File
[query] :: URL -> Maybe Text
[headers] :: URL -> Maybe ImportHashed
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 -> !Integer -> Var
data Binding s a
Binding :: Text -> Maybe (Expr s a) -> Expr s a -> Binding s a
[variable] :: Binding s a -> Text
[annotation] :: Binding s a -> Maybe (Expr s a)
[value] :: Binding s a -> Expr s a
-- | The body of an interpolated Text literal
data Chunks s a
Chunks :: [(Text, Expr s a)] -> Text -> Chunks s a
-- | Syntax tree for expressions
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
--
Let :: NonEmpty (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
-- |
-- 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] : List 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
-- |
-- OptionalLit t (Just e) ~ [e] : Optional t
-- OptionalLit t Nothing ~ [] : Optional t
--
OptionalLit :: Expr s a -> Maybe (Expr s a) -> 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
-- |
-- UnionLit k v [(k1, Just t1), (k2, Nothing)] ~ < k = v | k1 : t1 | k2 >
--
UnionLit :: Text -> Expr s a -> 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
-- |
-- Field e x ~ e.x
--
Field :: Expr s a -> Text -> Expr s a
-- |
-- Project e xs ~ e.{ xs }
--
Project :: Expr s a -> Set Text -> 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.
--
-- However, normalize will not fail if the expression is ill-typed
-- and will leave ill-typed sub-expressions unevaluated.
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 :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
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 :: 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 :: Integer -> Var -> Expr s a -> Expr s a
-- | Quickly check if an expression is in normal form
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 :: (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
-- | 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
-- | 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
-- | 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)
-- | 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 (Data.Data.Data s, Data.Data.Data a) => Data.Data.Data (Dhall.Core.Binding s a)
instance (GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Dhall.Core.Binding s a)
instance (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Dhall.Core.Binding s a)
instance Data.Traversable.Traversable (Dhall.Core.Binding s)
instance GHC.Generics.Generic (Dhall.Core.Binding s a)
instance Data.Foldable.Foldable (Dhall.Core.Binding s)
instance GHC.Base.Functor (Dhall.Core.Binding s)
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 (GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Dhall.Core.Expr s a)
instance (Data.Data.Data s, Data.Data.Data a) => Data.Data.Data (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 GHC.Show.Show 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 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 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 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 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 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 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 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 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 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 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.Eq Dhall.Core.Const
instance GHC.Show.Show Dhall.Core.Const
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 Data.Bifunctor.Bifunctor Dhall.Core.Binding
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.String.IsString Dhall.Core.Var
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Var
instance GHC.Base.Semigroup Dhall.Core.Import
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.Core.Import
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 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 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
prettyCharacterSet :: Pretty a => CharacterSet -> Expr s a -> Doc Ann
-- | Default layout options
layoutOpts :: LayoutOptions
-- | 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
removeLetInLet :: Eq a => Expr s a -> Maybe (Expr s a)
removeUnusedBindings :: Eq a => Expr s a -> Maybe (Expr s a)
optionalLitToSomeNone :: Expr s a -> Maybe (Expr s a)
-- | 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
defaultStandardVersion :: StandardVersion
parseStandardVersion :: Parser 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
encodeExpression :: Expr s Import -> Term
-- | Decode a Dhall expression from a CBOR Term
decodeExpression :: Term -> Either DecodingFailure (Expr s Import)
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.ToTerm a => Dhall.Binary.ToTerm (Dhall.Core.Expr s a)
instance Dhall.Binary.ToTerm Dhall.Core.Import
-- | 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
diffExpression :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Diff
-- | Render the difference between the normal form of two expressions
diffNormalized :: (Eq a, Pretty a, ToTerm a) => Expr s a -> Expr s a -> Doc Ann
-- | Render the difference between two expressions
diff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann
instance GHC.Base.Semigroup Dhall.Diff.Diff
instance GHC.Base.Monoid Dhall.Diff.Diff
instance Data.String.IsString Dhall.Diff.Diff
-- | 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 => 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
-- | Like Void, except with a shorter inferred type
newtype X
X :: (forall a. a) -> X
[absurd] :: X -> forall a. 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
InvalidOptionalElement :: Expr s a -> Expr s a -> Expr s a -> TypeMessage s a
InvalidOptionalType :: 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
InvalidField :: Text -> Expr s a -> TypeMessage s a
InvalidFieldType :: Text -> Expr s a -> TypeMessage s a
FieldAnnotationMismatch :: Text -> Expr s a -> Const -> Text -> Expr s a -> Const -> TypeMessage s a
FieldMismatch :: Text -> Expr s a -> Const -> Text -> Expr s a -> Const -> TypeMessage s a
InvalidAlternative :: 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
DuplicateAlternative :: Text -> TypeMessage s a
MustCombineARecord :: Char -> Expr s a -> Expr s a -> TypeMessage s a
RecordMismatch :: Char -> Expr s a -> Expr s a -> Const -> Const -> 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
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
ConstructorsRequiresAUnionType :: Expr s a -> 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
MissingField :: Text -> 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
NoDependentTypes :: 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)
instance GHC.Show.Show Dhall.TypeCheck.X
instance GHC.Classes.Eq Dhall.TypeCheck.X
instance Data.Data.Data Dhall.TypeCheck.X
instance Data.Text.Prettyprint.Doc.Internal.Pretty Dhall.TypeCheck.X
instance Dhall.Binary.FromTerm Dhall.TypeCheck.X
instance Dhall.Binary.ToTerm Dhall.TypeCheck.X
-- | 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
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 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
-- | 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
-- | Parse an expression from a Import containing a Dhall program
exprFromImport :: Import -> StateT (Status IO) IO (Expr Src Import)
-- | Save an expression to the specified Import
--
-- Currently this only works for cached imports and ignores other types
-- of imports, but could conceivably work for uncached imports in the
-- future
--
-- The main reason for this more general type is for symmetry with
-- exprFromImport and to support doing more clever things in the
-- future, like doing "the right thing" for uncached imports (i.e.
-- exporting environment variables or creating files)
exprToImport :: Import -> Expr Src X -> StateT (Status IO) IO ()
-- | Resolve all imports within an expression
load :: 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 :: MonadCatch m => Expr Src Import -> StateT (Status m) m (Expr Src X)
-- | Hash a fully resolved expression
hashExpression :: StandardVersion -> 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 :: StandardVersion -> Expr s X -> Text
-- | 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 m
-- | Default starting Status, importing relative to the given
-- directory.
emptyStatus :: FilePath -> Status IO
stack :: Functor f => LensLike' f (Status m) (NonEmpty Import)
cache :: Functor f => LensLike' f (Status m) (Map Import (NodeId, Expr Src X))
manager :: Functor f => LensLike' f (Status m) (Maybe Dynamic)
standardVersion :: Functor f => LensLike' f (Status m) StandardVersion
normalizer :: Functor f => LensLike' f (Status m) (Maybe (ReifiedNormalizer X))
startingContext :: Functor f => LensLike' f (Status m) (Context (Expr Src X))
resolver :: Functor f => LensLike' f (Status m) (Import -> StateT (Status m) m (Expr Src Import))
cacher :: Functor f => LensLike' f (Status m) (Import -> Expr Src X -> StateT (Status m) m ())
-- | 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 Import -> e -> Imported e
-- | Imports resolved so far, in reverse order
[importStack] :: Imported e -> NonEmpty Import
-- | 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
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 :: StandardVersion -> IO ()
-- | This module contains the implementation of the dhall freeze
-- subcommand
module Dhall.Freeze
-- | Implementation of the dhall freeze subcommand
freeze :: Maybe FilePath -> Bool -> StandardVersion -> IO ()
-- | Retrieve an Import and update the hash to match the latest
-- contents
freezeImport :: FilePath -> StandardVersion -> Import -> IO Import
-- | Freeze an import only if the import is a Remote import
freezeRemoteImport :: FilePath -> StandardVersion -> Import -> IO Import
-- | 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))
-- | Access the standard version (used primarily when encoding or decoding
-- Dhall expressions to and from a binary representation)
standardVersion :: (Functor f, HasEvaluateSettings s) => LensLike' f s StandardVersion
-- | 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 -> Maybe a) -> Expr Src X -> Type a
-- | Extracts Haskell value from the Dhall expression
[extract] :: Type a -> Expr Src X -> Maybe 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" string
-- <*> field "description" string
-- <*> field "stars" natural
-- )
--
newtype RecordType a
RecordType :: Product (Const (Map Text (Expr Src X))) (Compose ((->) (Expr Src X)) Maybe) 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 = "Finish succesfully"
-- | Queued : Natural
-- | Errored : Text
-- >
--
--
-- 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" string
-- <> Errored <$> constructor "Errored" string
-- )
--
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 succeed. If not, then this exception is thrown
--
-- This exception 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
-- | 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
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
-- | The UnionInputType monoid 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 = "Finish succesfully"
-- | Queued : Natural
-- | Errored : Text
-- >
--
--
-- 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 InputUnionType to build
-- an InputType for Status:
--
--
-- injectStatus :: InputType Status
-- injectStatus =
-- adapt
-- >$< inputConstructorWith "Queued" inject
-- >|< inputConstructorWith "Result" inject
-- >|< inputConstructorWith "Errored" inject
-- where
-- adapt (Queued n) = Left (Left n)
-- adapt (Result t) = Left (Right t)
-- adapt (Errored e) = Right e
--
--
-- Or, since we are simply using the Inject instance to inject
-- each branch, we could write
--
--
-- injectStatus :: InputType Status
-- injectStatus =
-- adapt
-- >$< inputConstructor "Queued"
-- >|< inputConstructor "Result"
-- >|< inputConstructor "Errored"
-- where
-- adapt (Queued n) = Left (Left n)
-- adapt (Result t) = Left (Right t)
-- adapt (Errored e) = 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 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.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 ()
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 Dhall.GenericInject f => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.D d f)
instance Dhall.GenericInject f => Dhall.GenericInject (GHC.Generics.M1 GHC.Generics.C c f)
instance (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 (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 (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 (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 (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 (GHC.Generics.Selector s, Dhall.Interpret a) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a))
instance Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.D d f)
instance Dhall.GenericInterpret GHC.Generics.V1
instance (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 (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 (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 (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 Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c f)
instance Dhall.GenericInterpret GHC.Generics.U1
instance (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.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.Exception.Type.Exception (Dhall.InvalidType s a)
-- | Dhall is a programming language specialized for configuration files.
-- This module contains a tutorial explaning 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 -> StandardVersion -> 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 -> StandardVersion -> Options
[mode] :: Options -> Mode
[explain] :: Options -> Bool
[plain] :: Options -> Bool
[ascii] :: Options -> Bool
[standardVersion] :: Options -> StandardVersion
-- | The subcommands for the dhall executable
data Mode
Default :: Bool -> Bool -> Mode
[annotate] :: Mode -> Bool
[alpha] :: Mode -> Bool
Version :: Mode
Resolve :: Maybe ResolveMode -> Mode
[resolveMode] :: Mode -> Maybe ResolveMode
Type :: Mode
Normalize :: Bool -> Mode
[alpha] :: Mode -> Bool
Repl :: Mode
Format :: FormatMode -> Mode
[formatMode] :: Mode -> FormatMode
Freeze :: Maybe FilePath -> Bool -> Mode
[inplace] :: Mode -> Maybe FilePath
[all_] :: Mode -> Bool
Hash :: Mode
Diff :: Text -> Text -> Mode
[expr1] :: Mode -> Text
[expr2] :: Mode -> Text
Lint :: Maybe FilePath -> Mode
[inplace] :: Mode -> Maybe FilePath
Encode :: Bool -> Mode
[json] :: Mode -> Bool
Decode :: Bool -> Mode
[json] :: Mode -> Bool
-- | 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 ()