dhall-1.19.1: A configuration language guaranteed to terminate

Safe Haskell | None
Language | Haskell2010

Dhall.Core

Contents

- Syntax
- Normalization
- Pretty-printing
- Miscellaneous

Description

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

Synopsis

- data Const
  - = Type
  - | Kind
  - | Sort
- newtype Directory = Directory {
  - components :: [Text]
  }
- data File = File {
  - directory :: Directory
  - file :: Text
  }
- data FilePrefix
  - = Absolute
  - | Here
  - | Home
- data Import = Import {
  - importHashed :: ImportHashed
  - importMode :: ImportMode
  }
- data ImportHashed = ImportHashed {
  - hash :: Maybe (Digest SHA256)
  - importType :: ImportType
  }
- data ImportMode
  - = Code
  - | RawText
- data ImportType
  - = Local FilePrefix File
  - | Remote URL
  - | Env Text
  - | Missing
- data URL = URL {
  - scheme :: Scheme
  - authority :: Text
  - path :: File
  - query :: Maybe Text
  - fragment :: Maybe Text
  - headers :: Maybe ImportHashed
  }
- type Path = Import
- data Scheme
  - = HTTP
  - | HTTPS
- data Var = V Text !Integer
- data Binding s a = Binding {
  - variable :: Text
  - annotation :: Maybe (Expr s a)
  - value :: Expr s a
  }
- data Chunks s a = Chunks [(Text, Expr s a)] Text
- data Expr s a
  - = Const Const
  - | Var Var
  - | Lam Text (Expr s a) (Expr s a)
  - | Pi Text (Expr s a) (Expr s a)
  - | App (Expr s a) (Expr s a)
  - | Let (NonEmpty (Binding s a)) (Expr s a)
  - | Annot (Expr s a) (Expr s a)
  - | Bool
  - | BoolLit Bool
  - | BoolAnd (Expr s a) (Expr s a)
  - | BoolOr (Expr s a) (Expr s a)
  - | BoolEQ (Expr s a) (Expr s a)
  - | BoolNE (Expr s a) (Expr s a)
  - | BoolIf (Expr s a) (Expr s a) (Expr s a)
  - | Natural
  - | NaturalLit Natural
  - | NaturalFold
  - | NaturalBuild
  - | NaturalIsZero
  - | NaturalEven
  - | NaturalOdd
  - | NaturalToInteger
  - | NaturalShow
  - | NaturalPlus (Expr s a) (Expr s a)
  - | NaturalTimes (Expr s a) (Expr s a)
  - | Integer
  - | IntegerLit Integer
  - | IntegerShow
  - | IntegerToDouble
  - | Double
  - | DoubleLit Double
  - | DoubleShow
  - | Text
  - | TextLit (Chunks s a)
  - | TextAppend (Expr s a) (Expr s a)
  - | List
  - | ListLit (Maybe (Expr s a)) (Seq (Expr s a))
  - | ListAppend (Expr s a) (Expr s a)
  - | ListBuild
  - | ListFold
  - | ListLength
  - | ListHead
  - | ListLast
  - | ListIndexed
  - | ListReverse
  - | Optional
  - | OptionalLit (Expr s a) (Maybe (Expr s a))
  - | Some (Expr s a)
  - | None
  - | OptionalFold
  - | OptionalBuild
  - | Record (Map Text (Expr s a))
  - | RecordLit (Map Text (Expr s a))
  - | Union (Map Text (Expr s a))
  - | UnionLit Text (Expr s a) (Map Text (Expr s a))
  - | Combine (Expr s a) (Expr s a)
  - | CombineTypes (Expr s a) (Expr s a)
  - | Prefer (Expr s a) (Expr s a)
  - | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
  - | Constructors (Expr s a)
  - | Field (Expr s a) Text
  - | Project (Expr s a) (Set Text)
  - | Note s (Expr s a)
  - | ImportAlt (Expr s a) (Expr s a)
  - | Embed a
- alphaNormalize :: Expr s a -> Expr s a
- normalize :: Eq a => Expr s a -> Expr t a
- normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a
- normalizeWithM :: (Eq a, Monad m) => NormalizerM m a -> Expr s a -> m (Expr t a)
- type Normalizer a = NormalizerM Identity a
- type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))
- data ReifiedNormalizer a = ReifiedNormalizer {
  - getReifiedNormalizer :: Normalizer a
  }
- judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
- subst :: Var -> Expr s a -> Expr s a -> Expr s a
- shift :: Integer -> Var -> Expr s a -> Expr s a
- isNormalized :: Eq a => Expr s a -> Bool
- isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
- denote :: Expr s a -> Expr t a
- freeIn :: Eq a => Var -> Expr s a -> Bool
- pretty :: Pretty a => a -> Text
- internalError :: Text -> forall b. b
- reservedIdentifiers :: HashSet Text
- escapeText :: Text -> Text
- subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
- pathCharacter :: Char -> Bool

# Syntax

data Const Source #

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

Constructors

Type |
Kind |
Sort |

Instances

Bounded Const Source # |
Instance details Defined in Dhall.Core Methods minBound :: Const Source # maxBound :: Const Source #
Enum Const Source # |
Instance details Defined in Dhall.Core Methods succ :: Const -> Const Source # pred :: Const -> Const Source # toEnum :: Int -> Const Source # fromEnum :: Const -> Int Source # enumFrom :: Const -> [Const] Source # enumFromThen :: Const -> Const -> [Const] Source # enumFromTo :: Const -> Const -> [Const] Source # enumFromThenTo :: Const -> Const -> Const -> [Const] Source #
Eq Const Source # |
Instance details Defined in Dhall.Core Methods (==) :: Const -> Const -> Bool Source # (/=) :: Const -> Const -> Bool Source #
Data Const Source # |

Instance details

Defined in Dhall.Core

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Const -> c Const Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Const Source #

toConstr :: Const -> Constr Source #

dataTypeOf :: Const -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Const) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Const) Source #

gmapT :: (forall b. Data b => b -> b) -> Const -> Const Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Const -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Const -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Const -> m Const Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const Source #

Show Const Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Const -> ShowS Source # show :: Const -> String Source # showList :: [Const] -> ShowS Source #
Generic Const Source # |
Instance details Defined in Dhall.Core Associated Types type Rep Const :: Type -> Type Source # Methods from :: Const -> Rep Const x Source # to :: Rep Const x -> Const Source #
Pretty Const Source # |
Instance details Defined in Dhall.Core Methods pretty :: Const -> Doc ann Source # prettyList :: [Const] -> Doc ann Source #
type Rep Const Source # |
Instance details Defined in Dhall.Core type Rep Const = D1 (MetaData "Const" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Type" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Kind" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Sort" PrefixI False) (U1 :: Type -> Type)))

newtype Directory Source #

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" ] }`

Constructors

Directory |

Fields

- components :: [Text]

Instances

Eq Directory Source # |
Instance details Defined in Dhall.Core Methods (==) :: Directory -> Directory -> Bool Source # (/=) :: Directory -> Directory -> Bool Source #
Ord Directory Source # |
Instance details Defined in Dhall.Core Methods compare :: Directory -> Directory -> Ordering Source # (<) :: Directory -> Directory -> Bool Source # (<=) :: Directory -> Directory -> Bool Source # (>) :: Directory -> Directory -> Bool Source # (>=) :: Directory -> Directory -> Bool Source # max :: Directory -> Directory -> Directory Source # min :: Directory -> Directory -> Directory Source #
Show Directory Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Directory -> ShowS Source # show :: Directory -> String Source # showList :: [Directory] -> ShowS Source #
Generic Directory Source # |
Instance details Defined in Dhall.Core Associated Types type Rep Directory :: Type -> Type Source # Methods from :: Directory -> Rep Directory x Source # to :: Rep Directory x -> Directory Source #
Semigroup Directory Source # |
Instance details Defined in Dhall.Core Methods (<>) :: Directory -> Directory -> Directory Source # sconcat :: NonEmpty Directory -> Directory Source # stimes :: Integral b => b -> Directory -> Directory Source #
Pretty Directory Source # |
Instance details Defined in Dhall.Core Methods pretty :: Directory -> Doc ann Source # prettyList :: [Directory] -> Doc ann Source #
type Rep Directory Source # |
Instance details Defined in Dhall.Core type Rep Directory = D1 (MetaData "Directory" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" True) (C1 (MetaCons "Directory" PrefixI True) (S1 (MetaSel (Just "components") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Text])))

data File Source #

A `File` is a `directory` followed by one additional path component representing the `file` name

Constructors

File |

Fields

- directory :: Directory
- file :: Text

Instances

Eq File Source # |
Instance details Defined in Dhall.Core Methods (==) :: File -> File -> Bool Source # (/=) :: File -> File -> Bool Source #
Ord File Source # |
Instance details Defined in Dhall.Core Methods compare :: File -> File -> Ordering Source # (<) :: File -> File -> Bool Source # (<=) :: File -> File -> Bool Source # (>) :: File -> File -> Bool Source # (>=) :: File -> File -> Bool Source # max :: File -> File -> File Source # min :: File -> File -> File Source #
Show File Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> File -> ShowS Source # show :: File -> String Source # showList :: [File] -> ShowS Source #
Generic File Source # |
Instance details Defined in Dhall.Core Associated Types type Rep File :: Type -> Type Source # Methods from :: File -> Rep File x Source # to :: Rep File x -> File Source #
Semigroup File Source # |
Instance details Defined in Dhall.Core Methods (<>) :: File -> File -> File Source # sconcat :: NonEmpty File -> File Source # stimes :: Integral b => b -> File -> File Source #
Pretty File Source # |
Instance details Defined in Dhall.Core Methods pretty :: File -> Doc ann Source # prettyList :: [File] -> Doc ann Source #
type Rep File Source # |
Instance details Defined in Dhall.Core type Rep File = D1 (MetaData "File" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "File" PrefixI True) (S1 (MetaSel (Just "directory") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Directory) :*: S1 (MetaSel (Just "file") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text)))

data FilePrefix Source #

The beginning of a file path which anchors subsequent path components

Constructors

Absolute | Absolute path
Here | Path relative to `.`
Home | Path relative to `~`

Instances

Eq FilePrefix Source # |
Instance details Defined in Dhall.Core Methods (==) :: FilePrefix -> FilePrefix -> Bool Source # (/=) :: FilePrefix -> FilePrefix -> Bool Source #
Ord FilePrefix Source # |

Instance details

Defined in Dhall.Core

Methods

compare :: FilePrefix -> FilePrefix -> Ordering Source #

(<) :: FilePrefix -> FilePrefix -> Bool Source #

(<=) :: FilePrefix -> FilePrefix -> Bool Source #

(>) :: FilePrefix -> FilePrefix -> Bool Source #

(>=) :: FilePrefix -> FilePrefix -> Bool Source #

max :: FilePrefix -> FilePrefix -> FilePrefix Source #

min :: FilePrefix -> FilePrefix -> FilePrefix Source #

Show FilePrefix Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> FilePrefix -> ShowS Source # show :: FilePrefix -> String Source # showList :: [FilePrefix] -> ShowS Source #
Generic FilePrefix Source # |
Instance details Defined in Dhall.Core Associated Types type Rep FilePrefix :: Type -> Type Source # Methods from :: FilePrefix -> Rep FilePrefix x Source # to :: Rep FilePrefix x -> FilePrefix Source #
Pretty FilePrefix Source # |
Instance details Defined in Dhall.Core Methods pretty :: FilePrefix -> Doc ann Source # prettyList :: [FilePrefix] -> Doc ann Source #
type Rep FilePrefix Source # |
Instance details Defined in Dhall.Core type Rep FilePrefix = D1 (MetaData "FilePrefix" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Absolute" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Here" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Home" PrefixI False) (U1 :: Type -> Type)))

data Import Source #

Reference to an external resource

Constructors

Import |

Fields

- importHashed :: ImportHashed
- importMode :: ImportMode

Instances

Eq Import Source # |
Instance details Defined in Dhall.Core Methods (==) :: Import -> Import -> Bool Source # (/=) :: Import -> Import -> Bool Source #
Ord Import Source # |
Instance details Defined in Dhall.Core Methods compare :: Import -> Import -> Ordering Source # (<) :: Import -> Import -> Bool Source # (<=) :: Import -> Import -> Bool Source # (>) :: Import -> Import -> Bool Source # (>=) :: Import -> Import -> Bool Source # max :: Import -> Import -> Import Source # min :: Import -> Import -> Import Source #
Show Import Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Import -> ShowS Source # show :: Import -> String Source # showList :: [Import] -> ShowS Source #
Generic Import Source # |
Instance details Defined in Dhall.Core Associated Types type Rep Import :: Type -> Type Source # Methods from :: Import -> Rep Import x Source # to :: Rep Import x -> Import Source #
Semigroup Import Source # |
Instance details Defined in Dhall.Core Methods (<>) :: Import -> Import -> Import Source # sconcat :: NonEmpty Import -> Import Source # stimes :: Integral b => b -> Import -> Import Source #
Pretty Import Source # |
Instance details Defined in Dhall.Core Methods pretty :: Import -> Doc ann Source # prettyList :: [Import] -> Doc ann Source #
type Rep Import Source # |
Instance details Defined in Dhall.Core type Rep Import = D1 (MetaData "Import" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Import" PrefixI True) (S1 (MetaSel (Just "importHashed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ImportHashed) :*: S1 (MetaSel (Just "importMode") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ImportMode)))

data ImportHashed Source #

A `ImportType` extended with an optional hash for semantic integrity checks

Constructors

ImportHashed |

Fields

- hash :: Maybe (Digest SHA256)
- importType :: ImportType

Instances

Eq ImportHashed Source # |
Instance details Defined in Dhall.Core Methods (==) :: ImportHashed -> ImportHashed -> Bool Source # (/=) :: ImportHashed -> ImportHashed -> Bool Source #
Ord ImportHashed Source # |

Instance details

Defined in Dhall.Core

Methods

compare :: ImportHashed -> ImportHashed -> Ordering Source #

(<) :: ImportHashed -> ImportHashed -> Bool Source #

(<=) :: ImportHashed -> ImportHashed -> Bool Source #

(>) :: ImportHashed -> ImportHashed -> Bool Source #

(>=) :: ImportHashed -> ImportHashed -> Bool Source #

max :: ImportHashed -> ImportHashed -> ImportHashed Source #

min :: ImportHashed -> ImportHashed -> ImportHashed Source #

Show ImportHashed Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> ImportHashed -> ShowS Source # show :: ImportHashed -> String Source # showList :: [ImportHashed] -> ShowS Source #
Generic ImportHashed Source # |
Instance details Defined in Dhall.Core Associated Types type Rep ImportHashed :: Type -> Type Source # Methods from :: ImportHashed -> Rep ImportHashed x Source # to :: Rep ImportHashed x -> ImportHashed Source #
Semigroup ImportHashed Source # |
Instance details Defined in Dhall.Core Methods (<>) :: ImportHashed -> ImportHashed -> ImportHashed Source # sconcat :: NonEmpty ImportHashed -> ImportHashed Source # stimes :: Integral b => b -> ImportHashed -> ImportHashed Source #
Pretty ImportHashed Source # |
Instance details Defined in Dhall.Core Methods pretty :: ImportHashed -> Doc ann Source # prettyList :: [ImportHashed] -> Doc ann Source #
type Rep ImportHashed Source # |

Instance details

Defined in Dhall.Core

type Rep ImportHashed = D1 (MetaData "ImportHashed" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "ImportHashed" PrefixI True) (S1 (MetaSel (Just "hash") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Digest SHA256))) :*: S1 (MetaSel (Just "importType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ImportType)))

data ImportMode Source #

How to interpret the import's contents (i.e. as Dhall code or raw text)

Constructors

Code |
RawText |

Instances

Eq ImportMode Source # |
Instance details Defined in Dhall.Core Methods (==) :: ImportMode -> ImportMode -> Bool Source # (/=) :: ImportMode -> ImportMode -> Bool Source #
Ord ImportMode Source # |

Instance details

Defined in Dhall.Core

Methods

compare :: ImportMode -> ImportMode -> Ordering Source #

(<) :: ImportMode -> ImportMode -> Bool Source #

(<=) :: ImportMode -> ImportMode -> Bool Source #

(>) :: ImportMode -> ImportMode -> Bool Source #

(>=) :: ImportMode -> ImportMode -> Bool Source #

max :: ImportMode -> ImportMode -> ImportMode Source #

min :: ImportMode -> ImportMode -> ImportMode Source #

Show ImportMode Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> ImportMode -> ShowS Source # show :: ImportMode -> String Source # showList :: [ImportMode] -> ShowS Source #
Generic ImportMode Source # |
Instance details Defined in Dhall.Core Associated Types type Rep ImportMode :: Type -> Type Source # Methods from :: ImportMode -> Rep ImportMode x Source # to :: Rep ImportMode x -> ImportMode Source #
type Rep ImportMode Source # |
Instance details Defined in Dhall.Core type Rep ImportMode = D1 (MetaData "ImportMode" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Code" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "RawText" PrefixI False) (U1 :: Type -> Type))

data ImportType Source #

The type of import (i.e. local vs. remote vs. environment)

Constructors

Local FilePrefix File | Local path
Remote URL | URL of remote resource and optional headers stored in an import
Env Text | Environment variable
Missing |

Instances

Eq ImportType Source # |
Instance details Defined in Dhall.Core Methods (==) :: ImportType -> ImportType -> Bool Source # (/=) :: ImportType -> ImportType -> Bool Source #
Ord ImportType Source # |

Instance details

Defined in Dhall.Core

Methods

compare :: ImportType -> ImportType -> Ordering Source #

(<) :: ImportType -> ImportType -> Bool Source #

(<=) :: ImportType -> ImportType -> Bool Source #

(>) :: ImportType -> ImportType -> Bool Source #

(>=) :: ImportType -> ImportType -> Bool Source #

max :: ImportType -> ImportType -> ImportType Source #

min :: ImportType -> ImportType -> ImportType Source #

Show ImportType Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> ImportType -> ShowS Source # show :: ImportType -> String Source # showList :: [ImportType] -> ShowS Source #
Generic ImportType Source # |
Instance details Defined in Dhall.Core Associated Types type Rep ImportType :: Type -> Type Source # Methods from :: ImportType -> Rep ImportType x Source # to :: Rep ImportType x -> ImportType Source #
Semigroup ImportType Source # |
Instance details Defined in Dhall.Core Methods (<>) :: ImportType -> ImportType -> ImportType Source # sconcat :: NonEmpty ImportType -> ImportType Source # stimes :: Integral b => b -> ImportType -> ImportType Source #
Pretty ImportType Source # |
Instance details Defined in Dhall.Core Methods pretty :: ImportType -> Doc ann Source # prettyList :: [ImportType] -> Doc ann Source #
type Rep ImportType Source # |

Instance details

Defined in Dhall.Core

type Rep ImportType = D1 (MetaData "ImportType" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) ((C1 (MetaCons "Local" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePrefix) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 File)) :+: C1 (MetaCons "Remote" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 URL))) :+: (C1 (MetaCons "Env" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text)) :+: C1 (MetaCons "Missing" PrefixI False) (U1 :: Type -> Type)))

data URL Source #

Constructors

URL |

Fields

- scheme :: Scheme
- authority :: Text
- path :: File
- query :: Maybe Text
- fragment :: Maybe Text
- headers :: Maybe ImportHashed

Instances

Eq URL Source # |
Instance details Defined in Dhall.Core Methods (==) :: URL -> URL -> Bool Source # (/=) :: URL -> URL -> Bool Source #
Ord URL Source # |
Instance details Defined in Dhall.Core Methods compare :: URL -> URL -> Ordering Source # (<) :: URL -> URL -> Bool Source # (<=) :: URL -> URL -> Bool Source # (>) :: URL -> URL -> Bool Source # (>=) :: URL -> URL -> Bool Source # max :: URL -> URL -> URL Source # min :: URL -> URL -> URL Source #
Show URL Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> URL -> ShowS Source # show :: URL -> String Source # showList :: [URL] -> ShowS Source #
Generic URL Source # |
Instance details Defined in Dhall.Core Associated Types type Rep URL :: Type -> Type Source # Methods from :: URL -> Rep URL x Source # to :: Rep URL x -> URL Source #
type Rep URL Source # |

Instance details

Defined in Dhall.Core

type Rep URL = D1 (MetaData "URL" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "URL" PrefixI True) ((S1 (MetaSel (Just "scheme") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Scheme) :*: (S1 (MetaSel (Just "authority") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: S1 (MetaSel (Just "path") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 File))) :*: (S1 (MetaSel (Just "query") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Text)) :*: (S1 (MetaSel (Just "fragment") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Text)) :*: S1 (MetaSel (Just "headers") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ImportHashed))))))

type Path = Import Source #

Deprecated: Use Dhall.Core.Import instead

Type synonym for `Import`, provided for backwards compatibility

data Scheme Source #

Constructors

HTTP |
HTTPS |

Instances

Eq Scheme Source # |
Instance details Defined in Dhall.Core Methods (==) :: Scheme -> Scheme -> Bool Source # (/=) :: Scheme -> Scheme -> Bool Source #
Ord Scheme Source # |
Instance details Defined in Dhall.Core Methods compare :: Scheme -> Scheme -> Ordering Source # (<) :: Scheme -> Scheme -> Bool Source # (<=) :: Scheme -> Scheme -> Bool Source # (>) :: Scheme -> Scheme -> Bool Source # (>=) :: Scheme -> Scheme -> Bool Source # max :: Scheme -> Scheme -> Scheme Source # min :: Scheme -> Scheme -> Scheme Source #
Show Scheme Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Scheme -> ShowS Source # show :: Scheme -> String Source # showList :: [Scheme] -> ShowS Source #
Generic Scheme Source # |
Instance details Defined in Dhall.Core Associated Types type Rep Scheme :: Type -> Type Source # Methods from :: Scheme -> Rep Scheme x Source # to :: Rep Scheme x -> Scheme Source #
type Rep Scheme Source # |
Instance details Defined in Dhall.Core type Rep Scheme = D1 (MetaData "Scheme" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "HTTP" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "HTTPS" PrefixI False) (U1 :: Type -> Type))

data Var Source #

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 `Var`s and non-zero indices appear as a numeric suffix.

Constructors

V Text !Integer |

Instances

Eq Var Source # |
Instance details Defined in Dhall.Core Methods (==) :: Var -> Var -> Bool Source # (/=) :: Var -> Var -> Bool Source #
Data Var Source # |

Instance details

Defined in Dhall.Core

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var -> c Var Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var Source #

toConstr :: Var -> Constr Source #

dataTypeOf :: Var -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Var) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var) Source #

gmapT :: (forall b. Data b => b -> b) -> Var -> Var Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Var -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var -> m Var Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var Source #

Show Var Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Var -> ShowS Source # show :: Var -> String Source # showList :: [Var] -> ShowS Source #
IsString Var Source # |
Instance details Defined in Dhall.Core Methods fromString :: String -> Var Source #
Generic Var Source # |
Instance details Defined in Dhall.Core Associated Types type Rep Var :: Type -> Type Source # Methods from :: Var -> Rep Var x Source # to :: Rep Var x -> Var Source #
Pretty Var Source # |
Instance details Defined in Dhall.Core Methods pretty :: Var -> Doc ann Source # prettyList :: [Var] -> Doc ann Source #
type Rep Var Source # |
Instance details Defined in Dhall.Core type Rep Var = D1 (MetaData "Var" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "V" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)))

data Binding s a Source #

Constructors

Binding |

Fields

- variable :: Text
- annotation :: Maybe (Expr s a)
- value :: Expr s a

Instances

Bifunctor Binding Source # |
Instance details Defined in Dhall.Core Methods bimap :: (a -> b) -> (c -> d) -> Binding a c -> Binding b d Source # first :: (a -> b) -> Binding a c -> Binding b c Source # second :: (b -> c) -> Binding a b -> Binding a c Source #
Functor (Binding s) Source # |
Instance details Defined in Dhall.Core Methods fmap :: (a -> b) -> Binding s a -> Binding s b Source # (<$) :: a -> Binding s b -> Binding s a Source #
Foldable (Binding s) Source # |

Instance details

Defined in Dhall.Core

Methods

fold :: Monoid m => Binding s m -> m Source #

foldMap :: Monoid m => (a -> m) -> Binding s a -> m Source #

foldr :: (a -> b -> b) -> b -> Binding s a -> b Source #

foldr' :: (a -> b -> b) -> b -> Binding s a -> b Source #

foldl :: (b -> a -> b) -> b -> Binding s a -> b Source #

foldl' :: (b -> a -> b) -> b -> Binding s a -> b Source #

foldr1 :: (a -> a -> a) -> Binding s a -> a Source #

foldl1 :: (a -> a -> a) -> Binding s a -> a Source #

toList :: Binding s a -> [a] Source #

null :: Binding s a -> Bool Source #

length :: Binding s a -> Int Source #

elem :: Eq a => a -> Binding s a -> Bool Source #

maximum :: Ord a => Binding s a -> a Source #

minimum :: Ord a => Binding s a -> a Source #

sum :: Num a => Binding s a -> a Source #

product :: Num a => Binding s a -> a Source #

Traversable (Binding s) Source # |
Instance details Defined in Dhall.Core Methods traverse :: Applicative f => (a -> f b) -> Binding s a -> f (Binding s b) Source # sequenceA :: Applicative f => Binding s (f a) -> f (Binding s a) Source # mapM :: Monad m => (a -> m b) -> Binding s a -> m (Binding s b) Source # sequence :: Monad m => Binding s (m a) -> m (Binding s a) Source #
(Eq s, Eq a) => Eq (Binding s a) Source # |
Instance details Defined in Dhall.Core Methods (==) :: Binding s a -> Binding s a -> Bool Source # (/=) :: Binding s a -> Binding s a -> Bool Source #
(Data s, Data a) => Data (Binding s a) Source # |

Instance details

Defined in Dhall.Core

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binding s a -> c (Binding s a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binding s a) Source #

toConstr :: Binding s a -> Constr Source #

dataTypeOf :: Binding s a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binding s a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binding s a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Binding s a -> Binding s a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binding s a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binding s a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Binding s a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binding s a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) Source #

(Show s, Show a) => Show (Binding s a) Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Binding s a -> ShowS Source # show :: Binding s a -> String Source # showList :: [Binding s a] -> ShowS Source #
Generic (Binding s a) Source # |
Instance details Defined in Dhall.Core Associated Types type Rep (Binding s a) :: Type -> Type Source # Methods from :: Binding s a -> Rep (Binding s a) x Source # to :: Rep (Binding s a) x -> Binding s a Source #
type Rep (Binding s a) Source # |

Instance details

Defined in Dhall.Core

type Rep (Binding s a) = D1 (MetaData "Binding" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Binding" PrefixI True) (S1 (MetaSel (Just "variable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: (S1 (MetaSel (Just "annotation") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr s a))) :*: S1 (MetaSel (Just "value") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))))

data Chunks s a Source #

The body of an interpolated `Text` literal

Constructors

Chunks [(Text, Expr s a)] Text |

Instances

Functor (Chunks s) Source # |
Instance details Defined in Dhall.Core Methods fmap :: (a -> b) -> Chunks s a -> Chunks s b Source # (<$) :: a -> Chunks s b -> Chunks s a Source #
Foldable (Chunks s) Source # |

Instance details

Defined in Dhall.Core

Methods

fold :: Monoid m => Chunks s m -> m Source #

foldMap :: Monoid m => (a -> m) -> Chunks s a -> m Source #

foldr :: (a -> b -> b) -> b -> Chunks s a -> b Source #

foldr' :: (a -> b -> b) -> b -> Chunks s a -> b Source #

foldl :: (b -> a -> b) -> b -> Chunks s a -> b Source #

foldl' :: (b -> a -> b) -> b -> Chunks s a -> b Source #

foldr1 :: (a -> a -> a) -> Chunks s a -> a Source #

foldl1 :: (a -> a -> a) -> Chunks s a -> a Source #

toList :: Chunks s a -> [a] Source #

null :: Chunks s a -> Bool Source #

length :: Chunks s a -> Int Source #

elem :: Eq a => a -> Chunks s a -> Bool Source #

maximum :: Ord a => Chunks s a -> a Source #

minimum :: Ord a => Chunks s a -> a Source #

sum :: Num a => Chunks s a -> a Source #

product :: Num a => Chunks s a -> a Source #

Traversable (Chunks s) Source # |
Instance details Defined in Dhall.Core Methods traverse :: Applicative f => (a -> f b) -> Chunks s a -> f (Chunks s b) Source # sequenceA :: Applicative f => Chunks s (f a) -> f (Chunks s a) Source # mapM :: Monad m => (a -> m b) -> Chunks s a -> m (Chunks s b) Source # sequence :: Monad m => Chunks s (m a) -> m (Chunks s a) Source #
(Eq s, Eq a) => Eq (Chunks s a) Source # |
Instance details Defined in Dhall.Core Methods (==) :: Chunks s a -> Chunks s a -> Bool Source # (/=) :: Chunks s a -> Chunks s a -> Bool Source #
(Data s, Data a) => Data (Chunks s a) Source # |

Instance details

Defined in Dhall.Core

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Chunks s a -> c (Chunks s a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Chunks s a) Source #

toConstr :: Chunks s a -> Constr Source #

dataTypeOf :: Chunks s a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Chunks s a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Chunks s a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Chunks s a -> Chunks s a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Chunks s a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Chunks s a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Chunks s a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Chunks s a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) Source #

(Show s, Show a) => Show (Chunks s a) Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Chunks s a -> ShowS Source # show :: Chunks s a -> String Source # showList :: [Chunks s a] -> ShowS Source #
IsString (Chunks s a) Source # |
Instance details Defined in Dhall.Core Methods fromString :: String -> Chunks s a Source #
Generic (Chunks s a) Source # |
Instance details Defined in Dhall.Core Associated Types type Rep (Chunks s a) :: Type -> Type Source # Methods from :: Chunks s a -> Rep (Chunks s a) x Source # to :: Rep (Chunks s a) x -> Chunks s a Source #
Semigroup (Chunks s a) Source # |
Instance details Defined in Dhall.Core Methods (<>) :: Chunks s a -> Chunks s a -> Chunks s a Source # sconcat :: NonEmpty (Chunks s a) -> Chunks s a Source # stimes :: Integral b => b -> Chunks s a -> Chunks s a Source #
Monoid (Chunks s a) Source # |
Instance details Defined in Dhall.Core Methods mempty :: Chunks s a Source # mappend :: Chunks s a -> Chunks s a -> Chunks s a Source # mconcat :: [Chunks s a] -> Chunks s a Source #
type Rep (Chunks s a) Source # |

Instance details

Defined in Dhall.Core

type Rep (Chunks s a) = D1 (MetaData "Chunks" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) (C1 (MetaCons "Chunks" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Text, Expr s a)]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text)))

data Expr s a Source #

Syntax tree for expressions

Constructors

Const Const

    Const c                                  ~  c

Var Var

    Var (V x 0)                              ~  x
    Var (V x n)                              ~  x@n

Lam Text (Expr s a) (Expr s a)

    Lam x     A b                            ~  λ(x : A) -> b

Pi Text (Expr s a) (Expr s a)

    Pi "_" A B                               ~        A  -> B
    Pi x   A B                               ~  ∀(x : A) -> B

App (Expr s a) (Expr s a)

    App f a                                  ~  f a

Let (NonEmpty (Binding 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

Annot (Expr s a) (Expr s a)

    Annot x t                                ~  x : t

Bool

    Bool                                     ~  Bool

BoolLit Bool

    BoolLit b                                ~  b

BoolAnd (Expr s a) (Expr s a)

    BoolAnd x y                              ~  x && y

BoolOr (Expr s a) (Expr s a)

    BoolOr  x y                              ~  x || y

BoolEQ (Expr s a) (Expr s a)

    BoolEQ  x y                              ~  x == y

BoolNE (Expr s a) (Expr s a)

    BoolNE  x y                              ~  x != y

BoolIf (Expr s a) (Expr s a) (Expr s a)

    BoolIf x y z                             ~  if x then y else z

Natural

    Natural                                  ~  Natural

NaturalLit Natural

    NaturalLit n                             ~  n

NaturalFold

    NaturalFold                              ~  Natural/fold

NaturalBuild

    NaturalBuild                             ~  Natural/build

NaturalIsZero

    NaturalIsZero                            ~  Natural/isZero

NaturalEven

    NaturalEven                              ~  Natural/even

NaturalOdd

    NaturalOdd                               ~  Natural/odd

NaturalToInteger

    NaturalToInteger                         ~  Natural/toInteger

NaturalShow

    NaturalShow                              ~  Natural/show

NaturalPlus (Expr s a) (Expr s a)

    NaturalPlus x y                          ~  x + y

NaturalTimes (Expr s a) (Expr s a)

    NaturalTimes x y                         ~  x * y

Integer

    Integer                                  ~  Integer

IntegerLit Integer

    IntegerLit n                             ~  ±n

IntegerShow

    IntegerShow                              ~  Integer/show

IntegerToDouble

    IntegerToDouble                          ~  Integer/toDouble

Double

    Double                                   ~  Double

DoubleLit Double

    DoubleLit n                              ~  n

DoubleShow

    DoubleShow                               ~  Double/show

Text

    Text                                     ~  Text

TextLit (Chunks s a)

    TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~  "t1${e1}t2${e2}t3"

TextAppend (Expr s a) (Expr s a)

    TextAppend x y                           ~  x ++ y

List

    List                                     ~  List

ListLit (Maybe (Expr s a)) (Seq (Expr s a))

    ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
    ListLit  Nothing  [x, y, z]              ~  [x, y, z]

ListAppend (Expr s a) (Expr s a)

    ListAppend x y                           ~  x # y

ListBuild

    ListBuild                                ~  List/build

ListFold

    ListFold                                 ~  List/fold

ListLength

    ListLength                               ~  List/length

ListHead

    ListHead                                 ~  List/head

ListLast

    ListLast                                 ~  List/last

ListIndexed

    ListIndexed                              ~  List/indexed

ListReverse

    ListReverse                              ~  List/reverse

Optional

    Optional                                 ~  Optional

OptionalLit (Expr s a) (Maybe (Expr s a))

    OptionalLit t (Just e)                   ~  [e] : Optional t
    OptionalLit t Nothing                    ~  []  : Optional t

Some (Expr s a)

    Some e                                   ~  Some e

None

    None                                     ~  None

OptionalFold

    OptionalFold                             ~  Optional/fold

OptionalBuild

    OptionalBuild                            ~  Optional/build

Record (Map Text (Expr s a))

    Record       [(k1, t1), (k2, t2)]        ~  { k1 : t1, k2 : t1 }

RecordLit (Map Text (Expr s a))

    RecordLit    [(k1, v1), (k2, v2)]        ~  { k1 = v1, k2 = v2 }

Union (Map Text (Expr s a))

    Union        [(k1, t1), (k2, t2)]        ~  < k1 : t1 | k2 : t2 >

UnionLit Text (Expr s a) (Map Text (Expr s a))

    UnionLit k v [(k1, t1), (k2, t2)]        ~  < k = v | k1 : t1 | k2 : t2 >

Combine (Expr s a) (Expr s a)

    Combine x y                              ~  x ∧ y

CombineTypes (Expr s a) (Expr s a)

    CombineTypes x y                         ~  x ⩓ y

Prefer (Expr s a) (Expr s a)

    Prefer x y                               ~  x ⫽ y

Merge (Expr s a) (Expr s a) (Maybe (Expr s a))

    Merge x y (Just t )                      ~  merge x y : t
    Merge x y  Nothing                       ~  merge x y

Constructors (Expr s a)

    Constructors e                           ~  constructors e

Field (Expr s a) Text

    Field e x                                ~  e.x

Project (Expr s a) (Set Text)

    Project e xs                             ~  e.{ xs }

Note s (Expr s a)

    Note s x                                 ~  e

ImportAlt (Expr s a) (Expr s a)

    ImportAlt                                ~  e1 ? e2

Embed a

    Embed import                             ~  import

Instances

Bifunctor Expr Source # |
Instance details Defined in Dhall.Core Methods bimap :: (a -> b) -> (c -> d) -> Expr a c -> Expr b d Source # first :: (a -> b) -> Expr a c -> Expr b c Source # second :: (b -> c) -> Expr a b -> Expr a c Source #
Monad (Expr s) Source # |
Instance details Defined in Dhall.Core Methods (>>=) :: Expr s a -> (a -> Expr s b) -> Expr s b Source # (>>) :: Expr s a -> Expr s b -> Expr s b Source # return :: a -> Expr s a Source # fail :: String -> Expr s a Source #
Functor (Expr s) Source # |
Instance details Defined in Dhall.Core Methods fmap :: (a -> b) -> Expr s a -> Expr s b Source # (<$) :: a -> Expr s b -> Expr s a Source #
Applicative (Expr s) Source # |
Instance details Defined in Dhall.Core Methods pure :: a -> Expr s a Source # (<*>) :: Expr s (a -> b) -> Expr s a -> Expr s b Source # liftA2 :: (a -> b -> c) -> Expr s a -> Expr s b -> Expr s c Source # (*>) :: Expr s a -> Expr s b -> Expr s b Source # (<*) :: Expr s a -> Expr s b -> Expr s a Source #
Foldable (Expr s) Source # |

Instance details

Defined in Dhall.Core

Methods

fold :: Monoid m => Expr s m -> m Source #

foldMap :: Monoid m => (a -> m) -> Expr s a -> m Source #

foldr :: (a -> b -> b) -> b -> Expr s a -> b Source #

foldr' :: (a -> b -> b) -> b -> Expr s a -> b Source #

foldl :: (b -> a -> b) -> b -> Expr s a -> b Source #

foldl' :: (b -> a -> b) -> b -> Expr s a -> b Source #

foldr1 :: (a -> a -> a) -> Expr s a -> a Source #

foldl1 :: (a -> a -> a) -> Expr s a -> a Source #

toList :: Expr s a -> [a] Source #

null :: Expr s a -> Bool Source #

length :: Expr s a -> Int Source #

elem :: Eq a => a -> Expr s a -> Bool Source #

maximum :: Ord a => Expr s a -> a Source #

minimum :: Ord a => Expr s a -> a Source #

sum :: Num a => Expr s a -> a Source #

product :: Num a => Expr s a -> a Source #

Traversable (Expr s) Source # |
Instance details Defined in Dhall.Core Methods traverse :: Applicative f => (a -> f b) -> Expr s a -> f (Expr s b) Source # sequenceA :: Applicative f => Expr s (f a) -> f (Expr s a) Source # mapM :: Monad m => (a -> m b) -> Expr s a -> m (Expr s b) Source # sequence :: Monad m => Expr s (m a) -> m (Expr s a) Source #
(Eq s, Eq a) => Eq (Expr s a) Source # |
Instance details Defined in Dhall.Core Methods (==) :: Expr s a -> Expr s a -> Bool Source # (/=) :: Expr s a -> Expr s a -> Bool Source #
(Data s, Data a) => Data (Expr s a) Source # |

Instance details

Defined in Dhall.Core

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr s a -> c (Expr s a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Expr s a) Source #

toConstr :: Expr s a -> Constr Source #

dataTypeOf :: Expr s a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Expr s a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr s a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Expr s a -> Expr s a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr s a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr s a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Expr s a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr s a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr s a -> m (Expr s a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr s a -> m (Expr s a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr s a -> m (Expr s a) Source #

(Show s, Show a) => Show (Expr s a) Source # |
Instance details Defined in Dhall.Core Methods showsPrec :: Int -> Expr s a -> ShowS Source # show :: Expr s a -> String Source # showList :: [Expr s a] -> ShowS Source #
IsString (Expr s a) Source # |
Instance details Defined in Dhall.Core Methods fromString :: String -> Expr s a Source #
Generic (Expr s a) Source # |
Instance details Defined in Dhall.Core Associated Types type Rep (Expr s a) :: Type -> Type Source # Methods from :: Expr s a -> Rep (Expr s a) x Source # to :: Rep (Expr s a) x -> Expr s a Source #
Pretty a => Pretty (Expr s a) Source # | Generates a syntactically valid Dhall program
Instance details Defined in Dhall.Core Methods pretty :: Expr s a -> Doc ann Source # prettyList :: [Expr s a] -> Doc ann Source #
type Rep (Expr s a) Source # |

Instance details

Defined in Dhall.Core

type Rep (Expr s a) = D1 (MetaData "Expr" "Dhall.Core" "dhall-1.19.1-AYtA11MR5MfCiyew2QpWmV" False) ((((((C1 (MetaCons "Const" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Const)) :+: C1 (MetaCons "Var" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Var))) :+: (C1 (MetaCons "Lam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))) :+: C1 (MetaCons "Pi" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))))) :+: ((C1 (MetaCons "App" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "Let" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Binding s a))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))) :+: (C1 (MetaCons "Annot" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "Bool" PrefixI False) (U1 :: Type -> Type)))) :+: (((C1 (MetaCons "BoolLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: C1 (MetaCons "BoolAnd" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))) :+: (C1 (MetaCons "BoolOr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "BoolEQ" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))) :+: ((C1 (MetaCons "BoolNE" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "BoolIf" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))) :+: (C1 (MetaCons "Natural" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NaturalLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Natural)))))) :+: ((((C1 (MetaCons "NaturalFold" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NaturalBuild" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "NaturalIsZero" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NaturalEven" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "NaturalOdd" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NaturalToInteger" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "NaturalShow" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NaturalPlus" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))))) :+: (((C1 (MetaCons "NaturalTimes" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "Integer" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "IntegerLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "IntegerShow" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "IntegerToDouble" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Double" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "DoubleLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Double)) :+: C1 (MetaCons "DoubleShow" PrefixI False) (U1 :: Type -> Type)))))) :+: (((((C1 (MetaCons "Text" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TextLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Chunks s a)))) :+: (C1 (MetaCons "TextAppend" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "List" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "ListLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr s a))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Seq (Expr s a)))) :+: C1 (MetaCons "ListAppend" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))) :+: (C1 (MetaCons "ListBuild" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "ListFold" PrefixI False) (U1 :: Type -> Type)))) :+: (((C1 (MetaCons "ListLength" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "ListHead" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "ListLast" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "ListIndexed" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "ListReverse" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Optional" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "OptionalLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr s a)))) :+: C1 (MetaCons "Some" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))))) :+: ((((C1 (MetaCons "None" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "OptionalFold" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "OptionalBuild" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Record" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Text (Expr s a)))))) :+: ((C1 (MetaCons "RecordLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Text (Expr s a)))) :+: C1 (MetaCons "Union" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Text (Expr s a))))) :+: (C1 (MetaCons "UnionLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Text (Expr s a))))) :+: C1 (MetaCons "Combine" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))))) :+: (((C1 (MetaCons "CombineTypes" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "Prefer" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)))) :+: (C1 (MetaCons "Merge" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr s a))))) :+: C1 (MetaCons "Constructors" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))) :+: ((C1 (MetaCons "Field" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text)) :+: C1 (MetaCons "Project" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Set Text)))) :+: (C1 (MetaCons "Note" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 s) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: (C1 (MetaCons "ImportAlt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "Embed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))))))))

# Normalization

alphaNormalize :: Expr s a -> Expr s a Source #

α-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)

normalize :: Eq a => Expr s a -> Expr t a Source #

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.

normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a Source #

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.

normalizeWithM :: (Eq a, Monad m) => NormalizerM m a -> Expr s a -> m (Expr t a) Source #

type Normalizer a = NormalizerM Identity a Source #

type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a)) Source #

Use this to wrap you embedded functions (see `normalizeWith`) to make them polymorphic enough to be used.

data ReifiedNormalizer a Source #

A reified `Normalizer`, which can be stored in structures without running into impredicative polymorphism.

Constructors

ReifiedNormalizer |

Fields

- getReifiedNormalizer :: Normalizer a

judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool Source #

Returns `True` if two expressions are α-equivalent and β-equivalent and `False` otherwise

subst :: Var -> Expr s a -> Expr s a -> Expr s a Source #

Substitute all occurrences of a variable with an expression

    subst x C B  ~  B[x := C]

shift :: Integer -> Var -> Expr s a -> Expr s a Source #

`shift` is used by both normalization and type-checking to avoid variable capture by shifting variable indices

For example, suppose that you were to normalize the following expression:

    λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x

If you were to substitute `y` with `x` without shifting any variable indices, then you would get the following incorrect result:

    λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form

In order to substitute `x` in place of `y` we need to `shift` `x` by `1` in order to avoid being misinterpreted as the `x` bound by the innermost lambda. If we perform that `shift` then we get the correct result:

    λ(a : Type) → λ(x : a) → λ(x : a) → x@1

As a more worked example, suppose that you were to normalize the following expression:

        λ(a : Type)
    →   λ(f : a → a → a)
    →   λ(x : a)
    →   λ(x : a)
    →   (λ(x : a) → f x x@1) x@1

The correct normalized result would be:

        λ(a : Type)
    →   λ(f : a → a → a)
    →   λ(x : a)
    →   λ(x : a)
    →   f x@1 x

The above example illustrates how we need to both increase and decrease variable indices as part of substitution:

- We need to increase the index of the outer `x@1` to `x@2` before we substitute it into the body of the innermost lambda expression in order to avoid variable capture. This substitution changes the body of the lambda expression to `(f x@2 x@1)`
- We then remove the innermost lambda and therefore decrease the indices of both `x`s in `(f x@2 x@1)` to `(f x@1 x)` in order to reflect that one less `x` variable is now bound within that scope

Formally, `(shift d (V x n) e)` modifies the expression `e` by adding `d` to the indices of all variables named `x` whose indices are greater than `(n + m)`, where `m` is the number of bound variables of the same name within that scope

In practice, `d` is always `1` or `-1` because we either:

- increment variables by `1` to avoid variable capture during substitution
- decrement variables by `1` when deleting lambdas after substitution

`n` starts off at `0` when substitution begins and increments every time we descend into a lambda or let expression that binds a variable of the same name in order to avoid shifting the bound variables by mistake.

isNormalized :: Eq a => Expr s a -> Bool Source #

Quickly check if an expression is in normal form

isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool Source #

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`.

denote :: Expr s a -> Expr t a Source #

Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)

freeIn :: Eq a => Var -> Expr s a -> Bool Source #

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

# Pretty-printing

pretty :: Pretty a => a -> Text Source #

# Miscellaneous

internalError :: Text -> forall b. b Source #

Utility function used to throw internal errors that should never happen (in theory) but that are not enforced by the type system

reservedIdentifiers :: HashSet Text Source #

The set of reserved identifiers for the Dhall language

escapeText :: Text -> Text Source #

subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a) Source #

A traversal over the immediate sub-expressions of an expression.

pathCharacter :: Char -> Bool Source #

Returns `True` if the given `Char` is valid within an unquoted path component

This is exported for reuse within the `Dhall.Parser.Token` module