dhall-1.33.1: A configuration language guaranteed to terminate

Safe HaskellNone
LanguageHaskell2010

Dhall.Core

Contents

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

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

Enum Const Source # 
Instance details

Defined in Dhall.Syntax

Eq Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Const -> Const -> Bool #

(/=) :: Const -> Const -> Bool #

Data Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

toConstr :: Const -> Constr #

dataTypeOf :: Const -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: Const -> Const -> Ordering #

(<) :: Const -> Const -> Bool #

(<=) :: Const -> Const -> Bool #

(>) :: Const -> Const -> Bool #

(>=) :: Const -> Const -> Bool #

max :: Const -> Const -> Const #

min :: Const -> Const -> Const #

Show Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> Const -> ShowS #

show :: Const -> String #

showList :: [Const] -> ShowS #

Generic Const Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep Const :: Type -> Type #

Methods

from :: Const -> Rep Const x #

to :: Rep Const x -> Const #

Lift Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: Const -> Q Exp #

NFData Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Const -> () #

Pretty Const Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: Const -> Doc ann #

prettyList :: [Const] -> Doc ann #

type Rep Const Source # 
Instance details

Defined in Dhall.Syntax

type Rep Const = D1 (MetaData "Const" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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

Instances
Eq Directory Source # 
Instance details

Defined in Dhall.Syntax

Ord Directory Source # 
Instance details

Defined in Dhall.Syntax

Show Directory Source # 
Instance details

Defined in Dhall.Syntax

Generic Directory Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep Directory :: Type -> Type #

Semigroup Directory Source # 
Instance details

Defined in Dhall.Syntax

NFData Directory Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Directory -> () #

Pretty Directory Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: Directory -> Doc ann #

prettyList :: [Directory] -> Doc ann #

type Rep Directory Source # 
Instance details

Defined in Dhall.Syntax

type Rep Directory = D1 (MetaData "Directory" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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

Instances
Eq File Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: File -> File -> Bool #

(/=) :: File -> File -> Bool #

Ord File Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: File -> File -> Ordering #

(<) :: File -> File -> Bool #

(<=) :: File -> File -> Bool #

(>) :: File -> File -> Bool #

(>=) :: File -> File -> Bool #

max :: File -> File -> File #

min :: File -> File -> File #

Show File Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> File -> ShowS #

show :: File -> String #

showList :: [File] -> ShowS #

Generic File Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep File :: Type -> Type #

Methods

from :: File -> Rep File x #

to :: Rep File x -> File #

Semigroup File Source # 
Instance details

Defined in Dhall.Syntax

Methods

(<>) :: File -> File -> File #

sconcat :: NonEmpty File -> File #

stimes :: Integral b => b -> File -> File #

NFData File Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: File -> () #

Pretty File Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: File -> Doc ann #

prettyList :: [File] -> Doc ann #

type Rep File Source # 
Instance details

Defined in Dhall.Syntax

type Rep File = D1 (MetaData "File" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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 .

Parent

Path relative to ..

Home

Path relative to ~

Instances
Eq FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Ord FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Show FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Generic FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep FilePrefix :: Type -> Type #

NFData FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: FilePrefix -> () #

Pretty FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: FilePrefix -> Doc ann #

prettyList :: [FilePrefix] -> Doc ann #

type Rep FilePrefix Source # 
Instance details

Defined in Dhall.Syntax

type Rep FilePrefix = D1 (MetaData "FilePrefix" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" False) ((C1 (MetaCons "Absolute" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Here" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Parent" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Home" PrefixI False) (U1 :: Type -> Type)))

data Import Source #

Reference to an external resource

Instances
Eq Import Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Import -> Import -> Bool #

(/=) :: Import -> Import -> Bool #

Ord Import Source # 
Instance details

Defined in Dhall.Syntax

Show Import Source # 
Instance details

Defined in Dhall.Syntax

Generic Import Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep Import :: Type -> Type #

Methods

from :: Import -> Rep Import x #

to :: Rep Import x -> Import #

Semigroup Import Source # 
Instance details

Defined in Dhall.Syntax

NFData Import Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Import -> () #

Pretty Import Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: Import -> Doc ann #

prettyList :: [Import] -> Doc ann #

Serialise (Expr Void Import) Source # 
Instance details

Defined in Dhall.Binary

type Rep Import Source # 
Instance details

Defined in Dhall.Syntax

type Rep Import = D1 (MetaData "Import" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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

Instances
Eq ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Ord ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Show ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Generic ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep ImportHashed :: Type -> Type #

Semigroup ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

NFData ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: ImportHashed -> () #

Pretty ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: ImportHashed -> Doc ann #

prettyList :: [ImportHashed] -> Doc ann #

type Rep ImportHashed Source # 
Instance details

Defined in Dhall.Syntax

type Rep ImportHashed = D1 (MetaData "ImportHashed" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" False) (C1 (MetaCons "ImportHashed" PrefixI True) (S1 (MetaSel (Just "hash") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe SHA256Digest)) :*: 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 
Location 
Instances
Eq ImportMode Source # 
Instance details

Defined in Dhall.Syntax

Ord ImportMode Source # 
Instance details

Defined in Dhall.Syntax

Show ImportMode Source # 
Instance details

Defined in Dhall.Syntax

Generic ImportMode Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep ImportMode :: Type -> Type #

NFData ImportMode Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: ImportMode -> () #

type Rep ImportMode Source # 
Instance details

Defined in Dhall.Syntax

type Rep ImportMode = D1 (MetaData "ImportMode" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" False) (C1 (MetaCons "Code" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "RawText" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Location" 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.Syntax

Ord ImportType Source # 
Instance details

Defined in Dhall.Syntax

Show ImportType Source # 
Instance details

Defined in Dhall.Syntax

Generic ImportType Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep ImportType :: Type -> Type #

Semigroup ImportType Source # 
Instance details

Defined in Dhall.Syntax

NFData ImportType Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: ImportType -> () #

Pretty ImportType Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: ImportType -> Doc ann #

prettyList :: [ImportType] -> Doc ann #

type Rep ImportType Source # 
Instance details

Defined in Dhall.Syntax

data URL Source #

This type stores all of the components of a remote import

Constructors

URL 
Instances
Eq URL Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: URL -> URL -> Bool #

(/=) :: URL -> URL -> Bool #

Ord URL Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: URL -> URL -> Ordering #

(<) :: URL -> URL -> Bool #

(<=) :: URL -> URL -> Bool #

(>) :: URL -> URL -> Bool #

(>=) :: URL -> URL -> Bool #

max :: URL -> URL -> URL #

min :: URL -> URL -> URL #

Show URL Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> URL -> ShowS #

show :: URL -> String #

showList :: [URL] -> ShowS #

Generic URL Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep URL :: Type -> Type #

Methods

from :: URL -> Rep URL x #

to :: Rep URL x -> URL #

NFData URL Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: URL -> () #

Pretty URL Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: URL -> Doc ann #

prettyList :: [URL] -> Doc ann #

type Rep URL Source # 
Instance details

Defined in Dhall.Syntax

data Scheme Source #

The URI scheme

Constructors

HTTP 
HTTPS 
Instances
Eq Scheme Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Scheme -> Scheme -> Bool #

(/=) :: Scheme -> Scheme -> Bool #

Ord Scheme Source # 
Instance details

Defined in Dhall.Syntax

Show Scheme Source # 
Instance details

Defined in Dhall.Syntax

Generic Scheme Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep Scheme :: Type -> Type #

Methods

from :: Scheme -> Rep Scheme x #

to :: Rep Scheme x -> Scheme #

NFData Scheme Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Scheme -> () #

type Rep Scheme Source # 
Instance details

Defined in Dhall.Syntax

type Rep Scheme = D1 (MetaData "Scheme" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" False) (C1 (MetaCons "HTTP" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "HTTPS" PrefixI False) (U1 :: Type -> Type))

newtype DhallDouble Source #

This wrapper around Double exists for its Eq instance which is defined via the binary encoding of Dhall Doubles.

Constructors

DhallDouble 
Instances
Eq DhallDouble Source #

This instance satisfies all the customary Eq laws except substitutivity.

In particular:

>>> nan = DhallDouble (0/0)
>>> nan == nan
True

This instance is also consistent with with the binary encoding of Dhall Doubles:

>>> toBytes n = Dhall.Binary.encodeExpression (DoubleLit n :: Expr Void Import)
\a b -> (a == b) == (toBytes a == toBytes b)
Instance details

Defined in Dhall.Syntax

Data DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

toConstr :: DhallDouble -> Constr #

dataTypeOf :: DhallDouble -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord DhallDouble Source #

This instance relies on the Eq instance for DhallDouble but cannot satisfy the customary Ord laws when NaN is involved.

Instance details

Defined in Dhall.Syntax

Show DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

Generic DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep DhallDouble :: Type -> Type #

Lift DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: DhallDouble -> Q Exp #

NFData DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: DhallDouble -> () #

type Rep DhallDouble Source # 
Instance details

Defined in Dhall.Syntax

type Rep DhallDouble = D1 (MetaData "DhallDouble" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" True) (C1 (MetaCons "DhallDouble" PrefixI True) (S1 (MetaSel (Just "getDhallDouble") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Double)))

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

Constructors

V Text !Int 
Instances
Eq Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Data Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

toConstr :: Var -> Constr #

dataTypeOf :: Var -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: Var -> Var -> Ordering #

(<) :: Var -> Var -> Bool #

(<=) :: Var -> Var -> Bool #

(>) :: Var -> Var -> Bool #

(>=) :: Var -> Var -> Bool #

max :: Var -> Var -> Var #

min :: Var -> Var -> Var #

Show Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

IsString Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

fromString :: String -> Var #

Generic Var Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep Var :: Type -> Type #

Methods

from :: Var -> Rep Var x #

to :: Rep Var x -> Var #

Lift Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: Var -> Q Exp #

NFData Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Var -> () #

Pretty Var Source # 
Instance details

Defined in Dhall.Syntax

Methods

pretty :: Var -> Doc ann #

prettyList :: [Var] -> Doc ann #

type Rep Var Source # 
Instance details

Defined in Dhall.Syntax

data Binding s a Source #

Record the binding part of a let expression.

For example,

let  x  :  Bool =  True in x

will be instantiated as follows:

  • bindingSrc0 corresponds to the A comment.
  • variable is "x"
  • bindingSrc1 corresponds to the B comment.
  • annotation is Just a pair, corresponding to the C comment and Bool.
  • bindingSrc2 corresponds to the D comment.
  • value corresponds to True.

Constructors

Binding 

Fields

Instances
Bifunctor Binding Source # 
Instance details

Defined in Dhall.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Binding a c -> Binding b d #

first :: (a -> b) -> Binding a c -> Binding b c #

second :: (b -> c) -> Binding a b -> Binding a c #

Functor (Binding s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fmap :: (a -> b) -> Binding s a -> Binding s b #

(<$) :: a -> Binding s b -> Binding s a #

Foldable (Binding s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

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

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

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

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

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

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

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

null :: Binding s a -> Bool #

length :: Binding s a -> Int #

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

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

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

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

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

Traversable (Binding s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Binding s a -> f (Binding s b) #

sequenceA :: Applicative f => Binding s (f a) -> f (Binding s a) #

mapM :: Monad m => (a -> m b) -> Binding s a -> m (Binding s b) #

sequence :: Monad m => Binding s (m a) -> m (Binding s a) #

(Eq s, Eq a) => Eq (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Binding s a -> Binding s a -> Bool #

(/=) :: Binding s a -> Binding s a -> Bool #

(Data s, Data a) => Data (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

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

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

toConstr :: Binding s a -> Constr #

dataTypeOf :: Binding s a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Ord s, Ord a) => Ord (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: Binding s a -> Binding s a -> Ordering #

(<) :: Binding s a -> Binding s a -> Bool #

(<=) :: Binding s a -> Binding s a -> Bool #

(>) :: Binding s a -> Binding s a -> Bool #

(>=) :: Binding s a -> Binding s a -> Bool #

max :: Binding s a -> Binding s a -> Binding s a #

min :: Binding s a -> Binding s a -> Binding s a #

(Show s, Show a) => Show (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> Binding s a -> ShowS #

show :: Binding s a -> String #

showList :: [Binding s a] -> ShowS #

Generic (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep (Binding s a) :: Type -> Type #

Methods

from :: Binding s a -> Rep (Binding s a) x #

to :: Rep (Binding s a) x -> Binding s a #

(Lift s, Lift a) => Lift (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: Binding s a -> Q Exp #

(NFData s, NFData a) => NFData (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Binding s a -> () #

type Rep (Binding s a) Source # 
Instance details

Defined in Dhall.Syntax

makeBinding :: Text -> Expr s a -> Binding s a Source #

Construct a Binding with no source information and no type annotation.

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

Methods

fmap :: (a -> b) -> Chunks s a -> Chunks s b #

(<$) :: a -> Chunks s b -> Chunks s a #

Foldable (Chunks s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

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

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

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

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

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

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

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

null :: Chunks s a -> Bool #

length :: Chunks s a -> Int #

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

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

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

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

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

Traversable (Chunks s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Chunks s a -> f (Chunks s b) #

sequenceA :: Applicative f => Chunks s (f a) -> f (Chunks s a) #

mapM :: Monad m => (a -> m b) -> Chunks s a -> m (Chunks s b) #

sequence :: Monad m => Chunks s (m a) -> m (Chunks s a) #

(Eq s, Eq a) => Eq (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Chunks s a -> Chunks s a -> Bool #

(/=) :: Chunks s a -> Chunks s a -> Bool #

(Data s, Data a) => Data (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

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

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

toConstr :: Chunks s a -> Constr #

dataTypeOf :: Chunks s a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Ord s, Ord a) => Ord (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

compare :: Chunks s a -> Chunks s a -> Ordering #

(<) :: Chunks s a -> Chunks s a -> Bool #

(<=) :: Chunks s a -> Chunks s a -> Bool #

(>) :: Chunks s a -> Chunks s a -> Bool #

(>=) :: Chunks s a -> Chunks s a -> Bool #

max :: Chunks s a -> Chunks s a -> Chunks s a #

min :: Chunks s a -> Chunks s a -> Chunks s a #

(Show s, Show a) => Show (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> Chunks s a -> ShowS #

show :: Chunks s a -> String #

showList :: [Chunks s a] -> ShowS #

IsString (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fromString :: String -> Chunks s a #

Generic (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep (Chunks s a) :: Type -> Type #

Methods

from :: Chunks s a -> Rep (Chunks s a) x #

to :: Rep (Chunks s a) x -> Chunks s a #

Semigroup (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

(<>) :: Chunks s a -> Chunks s a -> Chunks s a #

sconcat :: NonEmpty (Chunks s a) -> Chunks s a #

stimes :: Integral b => b -> Chunks s a -> Chunks s a #

Monoid (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

mempty :: Chunks s a #

mappend :: Chunks s a -> Chunks s a -> Chunks s a #

mconcat :: [Chunks s a] -> Chunks s a #

(Lift s, Lift a) => Lift (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: Chunks s a -> Q Exp #

(NFData s, NFData a) => NFData (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Chunks s a -> () #

type Rep (Chunks s a) Source # 
Instance details

Defined in Dhall.Syntax

type Rep (Chunks s a) = D1 (MetaData "Chunks" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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 PreferAnnotation s a Source #

Used to record the origin of a // operator (i.e. from source code or a product of desugaring)

Constructors

PreferFromSource 
PreferFromWith (Expr s a)

Stores the original with expression

PreferFromCompletion 
Instances
Bifunctor PreferAnnotation Source # 
Instance details

Defined in Dhall.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> PreferAnnotation a c -> PreferAnnotation b d #

first :: (a -> b) -> PreferAnnotation a c -> PreferAnnotation b c #

second :: (b -> c) -> PreferAnnotation a b -> PreferAnnotation a c #

Functor (PreferAnnotation s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fmap :: (a -> b) -> PreferAnnotation s a -> PreferAnnotation s b #

(<$) :: a -> PreferAnnotation s b -> PreferAnnotation s a #

Foldable (PreferAnnotation s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fold :: Monoid m => PreferAnnotation s m -> m #

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

foldr :: (a -> b -> b) -> b -> PreferAnnotation s a -> b #

foldr' :: (a -> b -> b) -> b -> PreferAnnotation s a -> b #

foldl :: (b -> a -> b) -> b -> PreferAnnotation s a -> b #

foldl' :: (b -> a -> b) -> b -> PreferAnnotation s a -> b #

foldr1 :: (a -> a -> a) -> PreferAnnotation s a -> a #

foldl1 :: (a -> a -> a) -> PreferAnnotation s a -> a #

toList :: PreferAnnotation s a -> [a] #

null :: PreferAnnotation s a -> Bool #

length :: PreferAnnotation s a -> Int #

elem :: Eq a => a -> PreferAnnotation s a -> Bool #

maximum :: Ord a => PreferAnnotation s a -> a #

minimum :: Ord a => PreferAnnotation s a -> a #

sum :: Num a => PreferAnnotation s a -> a #

product :: Num a => PreferAnnotation s a -> a #

Traversable (PreferAnnotation s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> PreferAnnotation s a -> f (PreferAnnotation s b) #

sequenceA :: Applicative f => PreferAnnotation s (f a) -> f (PreferAnnotation s a) #

mapM :: Monad m => (a -> m b) -> PreferAnnotation s a -> m (PreferAnnotation s b) #

sequence :: Monad m => PreferAnnotation s (m a) -> m (PreferAnnotation s a) #

(Eq s, Eq a) => Eq (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

(Data s, Data a) => Data (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

toConstr :: PreferAnnotation s a -> Constr #

dataTypeOf :: PreferAnnotation s a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Ord s, Ord a) => Ord (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

(Show s, Show a) => Show (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

Generic (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep (PreferAnnotation s a) :: Type -> Type #

(Lift s, Lift a) => Lift (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: PreferAnnotation s a -> Q Exp #

(NFData s, NFData a) => NFData (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: PreferAnnotation s a -> () #

type Rep (PreferAnnotation s a) Source # 
Instance details

Defined in Dhall.Syntax

type Rep (PreferAnnotation s a) = D1 (MetaData "PreferAnnotation" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" False) (C1 (MetaCons "PreferFromSource" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "PreferFromWith" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))) :+: C1 (MetaCons "PreferFromCompletion" PrefixI False) (U1 :: Type -> Type)))

data Expr s a Source #

Syntax tree for expressions

The s type parameter is used to track the presence or absence of Src spans:

  • If s = Src then the code may contains Src spans (either in a Noted constructor or inline within another constructor, like Let)
  • If s = Void then the code has no Src spans

The a type parameter is used to track the presence or absence of imports

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 (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

The difference between

let x = a    let y = b in e

and

let x = a in let y = b in e

is only an additional Note around Let "y" … in the second example.

See MultiLet for a representation of let-blocks that mirrors the source code more closely.

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
NaturalSubtract
NaturalSubtract                          ~  Natural/subtract
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
IntegerClamp
IntegerClamp                               ~  Integer/clamp
IntegerNegate
IntegerNegate                              ~  Integer/negate
IntegerShow
IntegerShow                              ~  Integer/show
IntegerToDouble
IntegerToDouble                          ~  Integer/toDouble
Double
Double                                   ~  Double
DoubleLit DhallDouble
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
TextShow
TextShow                                 ~  Text/show
List
List                                     ~  List
ListLit (Maybe (Expr s a)) (Seq (Expr s a))
ListLit (Just t ) []                     ~  [] : t
ListLit  Nothing  [x, y, z]              ~  [x, y, z]

Invariant: A non-empty list literal is always represented as ListLit Nothing xs.

When an annotated, non-empty list literal is parsed, it is represented as

Annot (ListLit Nothing [x, y, z]) t      ~ [x, y, z] : t
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
Some (Expr s a)
Some e                                   ~  Some e
None
None                                     ~  None
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 (Maybe (Expr s a)))
Union        [(k1, Just t1), (k2, Nothing)] ~  < k1 : t1 | k2 >
Combine (Maybe Text) (Expr s a) (Expr s a)
Combine Nothing x y                      ~  x ∧ y

The first field is a Just when the Combine operator is introduced as a result of desugaring duplicate record fields:

RecordLit [ (k, Combine (Just k) x y) ]  ~ { k = x, k = y }
CombineTypes (Expr s a) (Expr s a)
CombineTypes x y                         ~  x ⩓ y
Prefer (PreferAnnotation s a) (Expr s a) (Expr s a)
Prefer False x y                         ~  x ⫽ y

The first field is a True when the Prefer operator is introduced as a result of desugaring a with expression

RecordCompletion (Expr s a) (Expr s a)
RecordCompletion 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
ToMap (Expr s a) (Maybe (Expr s a))
ToMap x (Just t)                         ~  toMap x : t
ToMap x  Nothing                         ~  toMap x
Field (Expr s a) Text
Field e x                                ~  e.x
Project (Expr s a) (Either (Set Text) (Expr s a))
Project e (Left xs)                      ~  e.{ xs }
Project e (Right t)                      ~  e.(t)
Assert (Expr s a)
Assert e                                 ~  assert : e
Equivalent (Expr s a) (Expr s a)
Equivalent x y                           ~  x ≡ y
With (Expr s a) (NonEmpty Text) (Expr s a)
With x y                                 ~  x with y
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.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Expr a c -> Expr b d #

first :: (a -> b) -> Expr a c -> Expr b c #

second :: (b -> c) -> Expr a b -> Expr a c #

Monad (Expr s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

(>>=) :: Expr s a -> (a -> Expr s b) -> Expr s b #

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

return :: a -> Expr s a #

fail :: String -> Expr s a #

Functor (Expr s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fmap :: (a -> b) -> Expr s a -> Expr s b #

(<$) :: a -> Expr s b -> Expr s a #

Applicative (Expr s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

pure :: a -> Expr s a #

(<*>) :: Expr s (a -> b) -> Expr s a -> Expr s b #

liftA2 :: (a -> b -> c) -> Expr s a -> Expr s b -> Expr s c #

(*>) :: Expr s a -> Expr s b -> Expr s b #

(<*) :: Expr s a -> Expr s b -> Expr s a #

Foldable (Expr s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

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

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

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

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

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

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

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

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

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

null :: Expr s a -> Bool #

length :: Expr s a -> Int #

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

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

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

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

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

Traversable (Expr s) Source # 
Instance details

Defined in Dhall.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Expr s a -> f (Expr s b) #

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

mapM :: Monad m => (a -> m b) -> Expr s a -> m (Expr s b) #

sequence :: Monad m => Expr s (m a) -> m (Expr s a) #

(Eq s, Eq a) => Eq (Expr s a) Source #

This instance encodes what the Dhall standard calls an "exact match" between two expressions.

Note that

>>> nan = DhallDouble (0/0)
>>> DoubleLit nan == DoubleLit nan
True
Instance details

Defined in Dhall.Syntax

Methods

(==) :: Expr s a -> Expr s a -> Bool #

(/=) :: Expr s a -> Expr s a -> Bool #

(Data s, Data a) => Data (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

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

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

toConstr :: Expr s a -> Constr #

dataTypeOf :: Expr s a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Ord s, Ord a) => Ord (Expr s a) Source #

Note that this Ord instance inherits DhallDouble's defects.

Instance details

Defined in Dhall.Syntax

Methods

compare :: Expr s a -> Expr s a -> Ordering #

(<) :: Expr s a -> Expr s a -> Bool #

(<=) :: Expr s a -> Expr s a -> Bool #

(>) :: Expr s a -> Expr s a -> Bool #

(>=) :: Expr s a -> Expr s a -> Bool #

max :: Expr s a -> Expr s a -> Expr s a #

min :: Expr s a -> Expr s a -> Expr s a #

(Show s, Show a) => Show (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

showsPrec :: Int -> Expr s a -> ShowS #

show :: Expr s a -> String #

showList :: [Expr s a] -> ShowS #

IsString (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

fromString :: String -> Expr s a #

Generic (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

Associated Types

type Rep (Expr s a) :: Type -> Type #

Methods

from :: Expr s a -> Rep (Expr s a) x #

to :: Rep (Expr s a) x -> Expr s a #

(Lift s, Lift a) => Lift (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

lift :: Expr s a -> Q Exp #

(NFData s, NFData a) => NFData (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

Methods

rnf :: Expr s a -> () #

Pretty a => Pretty (Expr s a) Source #

Generates a syntactically valid Dhall program

Instance details

Defined in Dhall.Syntax

Methods

pretty :: Expr s a -> Doc ann #

prettyList :: [Expr s a] -> Doc ann #

Serialise (Expr Void Void) Source # 
Instance details

Defined in Dhall.Binary

Serialise (Expr Void Import) Source # 
Instance details

Defined in Dhall.Binary

type Rep (Expr s a) Source # 
Instance details

Defined in Dhall.Syntax

type Rep (Expr s a) = D1 (MetaData "Expr" "Dhall.Syntax" "dhall-1.33.1-DOBPU4XX8CX7s0IhWgRrGJ" 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 (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 "NaturalSubtract" 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 "IntegerClamp" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "IntegerNegate" PrefixI False) (U1 :: Type -> Type) :+: 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 DhallDouble)))))))) :+: (((((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 "TextShow" PrefixI False) (U1 :: Type -> Type) :+: 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 "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 "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 (Maybe (Expr s a))))))) :+: ((C1 (MetaCons "Combine" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe 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 "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 (PreferAnnotation 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 "RecordCompletion" 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 "ToMap" 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 "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 (Either (Set Text) (Expr s a)))) :+: C1 (MetaCons "Assert" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))) :+: ((C1 (MetaCons "Equivalent" 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 "With" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty Text)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr s a))))) :+: (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.

normalize can also fail with error if you normalize an ill-typed expression

normalizeWith :: Eq a => Maybe (ReifiedNormalizer 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.

normalizeWith can fail with an error if you normalize an ill-typed expression

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

This function generalizes normalizeWith by allowing the custom normalizer to use an arbitrary Monad

normalizeWithM can fail with an error if you normalize an ill-typed expression

type Normalizer a = NormalizerM Identity a Source #

An variation on NormalizerM for pure normalizers

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.

newtype ReifiedNormalizer a Source #

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

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

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

judgmentallyEqual can fail with an error if you compare ill-typed expressions

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 :: Int -> 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 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.

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

Quickly check if an expression is in normal form

Given a well-typed expression e, isNormalized e is equivalent to e == normalize e.

Given an ill-typed expression, isNormalized may fail with an error, or evaluate to either False or True!

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.

isNormalizedWith can fail with an error if you check an ill-typed expression

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

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

renote :: Expr Void a -> Expr s a Source #

The "opposite" of denote, like first absurd but faster

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

Remove any outermost Note constructors

This is typically used when you want to get the outermost non-Note constructor without removing internal Note constructors

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 #

Pretty-print a value

Optics

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.

chunkExprs :: Applicative f => (Expr s a -> f (Expr t b)) -> Chunks s a -> f (Chunks t b) Source #

A traversal over the immediate sub-expressions in Chunks.

bindingExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> Binding s a -> f (Binding s b) Source #

Traverse over the immediate Expr children in a Binding.

Let-blocks

multiLet :: Binding s a -> Expr s a -> MultiLet s a Source #

Generate a MultiLet from the contents of a Let.

In the resulting MultiLet bs e, e is guaranteed not to be a Let, but it might be a (Note … (Let …)).

Given parser output, multiLet consolidates lets that formed a let-block in the original source.

wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a Source #

Wrap let-Bindings around an Expr.

wrapInLets can be understood as an inverse for multiLet:

let MultiLet bs e1 = multiLet b e0

wrapInLets bs e1 == Let b e0

data MultiLet s a Source #

This type represents 1 or more nested Let bindings that have been coalesced together for ease of manipulation

Constructors

MultiLet (NonEmpty (Binding s a)) (Expr s a) 

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 | Contains also all keywords from "reservedKeywords"

escapeText :: Text -> Text Source #

Escape a Expr literal using Dhall's escaping rules

Note that the result does not include surrounding quotes

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

throws :: (Exception e, MonadIO io) => Either e a -> io a Source #

Convenience utility for converting Either-based exceptions to IO-based exceptions

textShow :: Text -> Text Source #

Utility that powers the Text/show built-in

censorExpression :: Expr Src a -> Expr Src a Source #

Utility used to implement the --censor flag, by:

  • Replacing all Src text with spaces
  • Replacing all Expr literals inside type errors with spaces

censorText :: Text -> Text Source #

Utility used to censor Expr by replacing all characters with a space

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

Desugar all with expressions