Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Dhall.Core
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
- newtype Directory = Directory {
- components :: [Text]
- data File = File {}
- data FilePrefix
- data Import = Import {}
- data ImportHashed = ImportHashed {
- hash :: Maybe SHA256Digest
- importType :: ImportType
- data ImportMode
- data ImportType
- data URL = URL {}
- data Scheme
- newtype DhallDouble = DhallDouble {
- getDhallDouble :: Double
- data Var = V Text !Int
- data Binding s a = Binding {
- bindingSrc0 :: Maybe s
- variable :: Text
- bindingSrc1 :: Maybe s
- annotation :: Maybe (Maybe s, Expr s a)
- bindingSrc2 :: Maybe s
- value :: Expr s a
- makeBinding :: Text -> Expr s a -> Binding s a
- data Chunks s a = Chunks [(Text, Expr s a)] Text
- data PreferAnnotation
- data RecordField s a = RecordField {
- recordFieldSrc0 :: Maybe s
- recordFieldValue :: Expr s a
- recordFieldSrc1 :: Maybe s
- recordFieldSrc2 :: Maybe s
- makeRecordField :: Expr s a -> RecordField s a
- data FunctionBinding s a = FunctionBinding {
- functionBindingSrc0 :: Maybe s
- functionBindingVariable :: Text
- functionBindingSrc1 :: Maybe s
- functionBindingSrc2 :: Maybe s
- functionBindingAnnotation :: Expr s a
- makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a
- data FieldSelection s = FieldSelection {
- fieldSelectionSrc0 :: Maybe s
- fieldSelectionLabel :: !Text
- fieldSelectionSrc1 :: Maybe s
- makeFieldSelection :: Text -> FieldSelection s
- data WithComponent
- data Expr s a
- = Const Const
- | Var Var
- | Lam (Maybe CharacterSet) (FunctionBinding s a) (Expr s a)
- | Pi (Maybe CharacterSet) Text (Expr s a) (Expr s a)
- | App (Expr s a) (Expr s a)
- | Let (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)
- | Bytes
- | BytesLit ByteString
- | Natural
- | NaturalLit Natural
- | NaturalFold
- | NaturalBuild
- | NaturalIsZero
- | NaturalEven
- | NaturalOdd
- | NaturalToInteger
- | NaturalShow
- | NaturalSubtract
- | NaturalPlus (Expr s a) (Expr s a)
- | NaturalTimes (Expr s a) (Expr s a)
- | Integer
- | IntegerLit Integer
- | IntegerClamp
- | IntegerNegate
- | IntegerShow
- | IntegerToDouble
- | Double
- | DoubleLit DhallDouble
- | DoubleShow
- | Text
- | TextLit (Chunks s a)
- | TextAppend (Expr s a) (Expr s a)
- | TextReplace
- | TextShow
- | Date
- | DateLiteral Day
- | DateShow
- | Time
- | TimeLiteral TimeOfDay Word
- | TimeShow
- | TimeZone
- | TimeZoneLiteral TimeZone
- | TimeZoneShow
- | 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
- | Some (Expr s a)
- | None
- | Record (Map Text (RecordField s a))
- | RecordLit (Map Text (RecordField s a))
- | Union (Map Text (Maybe (Expr s a)))
- | Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a)
- | CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a)
- | Prefer (Maybe CharacterSet) PreferAnnotation (Expr s a) (Expr s a)
- | RecordCompletion (Expr s a) (Expr s a)
- | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
- | ToMap (Expr s a) (Maybe (Expr s a))
- | ShowConstructor (Expr s a)
- | Field (Expr s a) (FieldSelection s)
- | Project (Expr s a) (Either [Text] (Expr s a))
- | Assert (Expr s a)
- | Equivalent (Maybe CharacterSet) (Expr s a) (Expr s a)
- | With (Expr s a) (NonEmpty WithComponent) (Expr s a)
- | 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 => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
- normalizeWithM :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
- type Normalizer a = NormalizerM Identity a
- type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))
- newtype ReifiedNormalizer a = ReifiedNormalizer {}
- judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
- subst :: Var -> Expr s a -> Expr s a -> Expr s a
- shift :: Int -> 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
- renote :: Expr Void a -> Expr s a
- shallowDenote :: Expr s a -> Expr s a
- freeIn :: Eq a => Var -> Expr s a -> Bool
- pretty :: Pretty a => a -> Text
- subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
- subExpressionsWith :: Applicative f => (a -> f (Expr s b)) -> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
- chunkExprs :: Applicative f => (Expr s a -> f (Expr t b)) -> Chunks s a -> f (Chunks t b)
- bindingExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> Binding s a -> f (Binding s b)
- recordFieldExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> RecordField s a -> f (RecordField s b)
- functionBindingExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> FunctionBinding s a -> f (FunctionBinding s b)
- multiLet :: Binding s a -> Expr s a -> MultiLet s a
- wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a
- data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a)
- internalError :: Text -> forall b. b
- reservedIdentifiers :: HashSet Text
- escapeText :: Text -> Text
- pathCharacter :: Char -> Bool
- throws :: (Exception e, MonadIO io) => Either e a -> io a
- textShow :: Text -> Text
- censorExpression :: Expr Src a -> Expr Src a
- censorText :: Text -> Text
Syntax
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
Instances
Data Const | |
Defined in Dhall.Syntax.Instances.Data 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 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 :: forall r r'. (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 | |
Bounded Const Source # | |
Defined in Dhall.Syntax.Const | |
Enum Const Source # | |
Generic Const Source # | |
Show Const | |
NFData Const | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq Const | |
Ord Const | |
Pretty Const | |
Defined in Dhall.Syntax.Instances.Pretty | |
Lift Const | |
type Rep Const Source # | |
Defined in Dhall.Syntax.Const type Rep Const = D1 ('MetaData "Const" "Dhall.Syntax.Const" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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))) |
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
Data Directory Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Directory -> c Directory gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Directory toConstr :: Directory -> Constr dataTypeOf :: Directory -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Directory) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Directory) gmapT :: (forall b. Data b => b -> b) -> Directory -> Directory gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Directory -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Directory -> r gmapQ :: (forall d. Data d => d -> u) -> Directory -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Directory -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Directory -> m Directory gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Directory -> m Directory gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Directory -> m Directory | |
Semigroup Directory Source # | |
Generic Directory Source # | |
Show Directory | |
NFData Directory | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq Directory | |
Ord Directory | |
Defined in Dhall.Syntax.Instances.Ord | |
Pretty Directory | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep Directory Source # | |
Defined in Dhall.Syntax.Import |
Instances
Data File Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> File -> c File gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c File dataTypeOf :: File -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c File) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c File) gmapT :: (forall b. Data b => b -> b) -> File -> File gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> File -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> File -> r gmapQ :: (forall d. Data d => d -> u) -> File -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> File -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> File -> m File gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> File -> m File gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> File -> m File | |
Semigroup File Source # | |
Generic File Source # | |
Show File | |
NFData File | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq File | |
Ord File | |
Pretty File | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep File Source # | |
Defined in Dhall.Syntax.Import type Rep File = D1 ('MetaData "File" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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
Data FilePrefix Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FilePrefix -> c FilePrefix gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FilePrefix toConstr :: FilePrefix -> Constr dataTypeOf :: FilePrefix -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FilePrefix) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FilePrefix) gmapT :: (forall b. Data b => b -> b) -> FilePrefix -> FilePrefix gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FilePrefix -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FilePrefix -> r gmapQ :: (forall d. Data d => d -> u) -> FilePrefix -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FilePrefix -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FilePrefix -> m FilePrefix gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FilePrefix -> m FilePrefix gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FilePrefix -> m FilePrefix | |
Generic FilePrefix Source # | |
Defined in Dhall.Syntax.Import Associated Types type Rep FilePrefix :: Type -> Type | |
Show FilePrefix | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> FilePrefix -> ShowS show :: FilePrefix -> String showList :: [FilePrefix] -> ShowS | |
NFData FilePrefix | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: FilePrefix -> () | |
Eq FilePrefix | |
Defined in Dhall.Syntax.Instances.Eq | |
Ord FilePrefix | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: FilePrefix -> FilePrefix -> Ordering (<) :: FilePrefix -> FilePrefix -> Bool (<=) :: FilePrefix -> FilePrefix -> Bool (>) :: FilePrefix -> FilePrefix -> Bool (>=) :: FilePrefix -> FilePrefix -> Bool max :: FilePrefix -> FilePrefix -> FilePrefix min :: FilePrefix -> FilePrefix -> FilePrefix | |
Pretty FilePrefix | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep FilePrefix Source # | |
Defined in Dhall.Syntax.Import type Rep FilePrefix = D1 ('MetaData "FilePrefix" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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))) |
Reference to an external resource
Constructors
Import | |
Fields |
Instances
Data Import Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Import -> c Import gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Import dataTypeOf :: Import -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Import) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Import) gmapT :: (forall b. Data b => b -> b) -> Import -> Import gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Import -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Import -> r gmapQ :: (forall d. Data d => d -> u) -> Import -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Import -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Import -> m Import gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Import -> m Import gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Import -> m Import | |
Semigroup Import Source # | |
Generic Import Source # | |
Show Import | |
NFData Import | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq Import | |
Ord Import | |
Pretty Import | |
Defined in Dhall.Syntax.Instances.Pretty | |
Serialise (Expr Void Import) | |
Defined in Dhall.Binary | |
type Rep Import Source # | |
Defined in Dhall.Syntax.Import type Rep Import = D1 ('MetaData "Import" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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
|
Instances
Data ImportHashed Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportHashed -> c ImportHashed gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImportHashed toConstr :: ImportHashed -> Constr dataTypeOf :: ImportHashed -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ImportHashed) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImportHashed) gmapT :: (forall b. Data b => b -> b) -> ImportHashed -> ImportHashed gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportHashed -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportHashed -> r gmapQ :: (forall d. Data d => d -> u) -> ImportHashed -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportHashed -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImportHashed -> m ImportHashed gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportHashed -> m ImportHashed gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportHashed -> m ImportHashed | |
Semigroup ImportHashed Source # | |
Defined in Dhall.Syntax.Import Methods (<>) :: ImportHashed -> ImportHashed -> ImportHashed sconcat :: NonEmpty ImportHashed -> ImportHashed stimes :: Integral b => b -> ImportHashed -> ImportHashed | |
Generic ImportHashed Source # | |
Defined in Dhall.Syntax.Import Associated Types type Rep ImportHashed :: Type -> Type | |
Show ImportHashed | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> ImportHashed -> ShowS show :: ImportHashed -> String showList :: [ImportHashed] -> ShowS | |
NFData ImportHashed | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: ImportHashed -> () | |
Eq ImportHashed | |
Defined in Dhall.Syntax.Instances.Eq | |
Ord ImportHashed | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: ImportHashed -> ImportHashed -> Ordering (<) :: ImportHashed -> ImportHashed -> Bool (<=) :: ImportHashed -> ImportHashed -> Bool (>) :: ImportHashed -> ImportHashed -> Bool (>=) :: ImportHashed -> ImportHashed -> Bool max :: ImportHashed -> ImportHashed -> ImportHashed min :: ImportHashed -> ImportHashed -> ImportHashed | |
Pretty ImportHashed | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep ImportHashed Source # | |
Defined in Dhall.Syntax.Import type Rep ImportHashed = D1 ('MetaData "ImportHashed" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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)
Instances
Data ImportMode Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportMode -> c ImportMode gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImportMode toConstr :: ImportMode -> Constr dataTypeOf :: ImportMode -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ImportMode) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImportMode) gmapT :: (forall b. Data b => b -> b) -> ImportMode -> ImportMode gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportMode -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportMode -> r gmapQ :: (forall d. Data d => d -> u) -> ImportMode -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportMode -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImportMode -> m ImportMode gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportMode -> m ImportMode gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportMode -> m ImportMode | |
Generic ImportMode Source # | |
Defined in Dhall.Syntax.Import Associated Types type Rep ImportMode :: Type -> Type | |
Show ImportMode | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> ImportMode -> ShowS show :: ImportMode -> String showList :: [ImportMode] -> ShowS | |
NFData ImportMode | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: ImportMode -> () | |
Eq ImportMode | |
Defined in Dhall.Syntax.Instances.Eq | |
Ord ImportMode | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: ImportMode -> ImportMode -> Ordering (<) :: ImportMode -> ImportMode -> Bool (<=) :: ImportMode -> ImportMode -> Bool (>) :: ImportMode -> ImportMode -> Bool (>=) :: ImportMode -> ImportMode -> Bool max :: ImportMode -> ImportMode -> ImportMode min :: ImportMode -> ImportMode -> ImportMode | |
type Rep ImportMode Source # | |
Defined in Dhall.Syntax.Import type Rep ImportMode = D1 ('MetaData "ImportMode" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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) :+: C1 ('MetaCons "RawBytes" '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
Data ImportType Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportType -> c ImportType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImportType toConstr :: ImportType -> Constr dataTypeOf :: ImportType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ImportType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImportType) gmapT :: (forall b. Data b => b -> b) -> ImportType -> ImportType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportType -> r gmapQ :: (forall d. Data d => d -> u) -> ImportType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImportType -> m ImportType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportType -> m ImportType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportType -> m ImportType | |
Semigroup ImportType Source # | |
Defined in Dhall.Syntax.Import Methods (<>) :: ImportType -> ImportType -> ImportType sconcat :: NonEmpty ImportType -> ImportType stimes :: Integral b => b -> ImportType -> ImportType | |
Generic ImportType Source # | |
Defined in Dhall.Syntax.Import Associated Types type Rep ImportType :: Type -> Type | |
Show ImportType | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> ImportType -> ShowS show :: ImportType -> String showList :: [ImportType] -> ShowS | |
NFData ImportType | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: ImportType -> () | |
Eq ImportType | |
Defined in Dhall.Syntax.Instances.Eq | |
Ord ImportType | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: ImportType -> ImportType -> Ordering (<) :: ImportType -> ImportType -> Bool (<=) :: ImportType -> ImportType -> Bool (>) :: ImportType -> ImportType -> Bool (>=) :: ImportType -> ImportType -> Bool max :: ImportType -> ImportType -> ImportType min :: ImportType -> ImportType -> ImportType | |
Pretty ImportType | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep ImportType Source # | |
Defined in Dhall.Syntax.Import type Rep ImportType = D1 ('MetaData "ImportType" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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))) |
This type stores all of the components of a remote import
Constructors
URL | |
Instances
Data URL Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> URL -> c URL gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c URL dataTypeOf :: URL -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c URL) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c URL) gmapT :: (forall b. Data b => b -> b) -> URL -> URL gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> URL -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> URL -> r gmapQ :: (forall d. Data d => d -> u) -> URL -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> URL -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> URL -> m URL gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> URL -> m URL gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> URL -> m URL | |
Generic URL Source # | |
Show URL | |
NFData URL | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq URL | |
Ord URL | |
Pretty URL | |
Defined in Dhall.Syntax.Instances.Pretty | |
type Rep URL Source # | |
Defined in Dhall.Syntax.Import type Rep URL = D1 ('MetaData "URL" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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 "headers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Expr Src Import))))))) |
The URI scheme
Instances
Data Scheme Source # | |
Defined in Dhall.Syntax.Import Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scheme -> c Scheme gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Scheme dataTypeOf :: Scheme -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Scheme) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scheme) gmapT :: (forall b. Data b => b -> b) -> Scheme -> Scheme gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r gmapQ :: (forall d. Data d => d -> u) -> Scheme -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Scheme -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scheme -> m Scheme gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scheme -> m Scheme gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scheme -> m Scheme | |
Generic Scheme Source # | |
Show Scheme | |
NFData Scheme | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq Scheme | |
Ord Scheme | |
type Rep Scheme Source # | |
Defined in Dhall.Syntax.Import type Rep Scheme = D1 ('MetaData "Scheme" "Dhall.Syntax.Import" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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 Double
s.
Constructors
DhallDouble | |
Fields
|
Instances
Data DhallDouble | |
Defined in Dhall.Syntax.Instances.Data 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 :: forall r r'. (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 | |
Generic DhallDouble Source # | |
Defined in Dhall.Syntax.Types Associated Types type Rep DhallDouble :: Type -> Type | |
Show DhallDouble | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> DhallDouble -> ShowS show :: DhallDouble -> String showList :: [DhallDouble] -> ShowS | |
NFData DhallDouble | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: DhallDouble -> () | |
Eq DhallDouble | This instance satisfies all the customary In particular:
This instance is also consistent with with the binary encoding of Dhall
\a b -> (a == b) == (toBytes a == toBytes b) |
Defined in Dhall.Syntax.Instances.Eq | |
Ord DhallDouble | This instance relies on the |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: DhallDouble -> DhallDouble -> Ordering (<) :: DhallDouble -> DhallDouble -> Bool (<=) :: DhallDouble -> DhallDouble -> Bool (>) :: DhallDouble -> DhallDouble -> Bool (>=) :: DhallDouble -> DhallDouble -> Bool max :: DhallDouble -> DhallDouble -> DhallDouble min :: DhallDouble -> DhallDouble -> DhallDouble | |
Lift DhallDouble | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => DhallDouble -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => DhallDouble -> Code m DhallDouble | |
type Rep DhallDouble Source # | |
Defined in Dhall.Syntax.Types type Rep DhallDouble = D1 ('MetaData "DhallDouble" "Dhall.Syntax.Types" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'True) (C1 ('MetaCons "DhallDouble" 'PrefixI 'True) (S1 ('MetaSel ('Just "getDhallDouble") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Double))) |
Label for a bound variable
The Text
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.
Instances
Data Var | |
Defined in Dhall.Syntax.Instances.Data 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 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 :: forall r r'. (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 | |
IsString Var Source # | |
Defined in Dhall.Syntax.Var Methods fromString :: String -> Var | |
Generic Var Source # | |
Show Var | |
NFData Var | |
Defined in Dhall.Syntax.Instances.NFData | |
Eq Var | |
Ord Var | |
Pretty Var | |
Defined in Dhall.Syntax.Instances.Pretty | |
Lift Var | |
type Rep Var Source # | |
Defined in Dhall.Syntax.Var type Rep Var = D1 ('MetaData "Var" "Dhall.Syntax.Var" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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 Int))) |
Record the binding part of a let
expression.
For example,
let {- A -} x {- B -} : {- C -} Bool = {- D -} True in x
… will be instantiated as follows:
bindingSrc0
corresponds to theA
comment.variable
is"x"
bindingSrc1
corresponds to theB
comment.annotation
isJust
a pair, corresponding to theC
comment andBool
.bindingSrc2
corresponds to theD
comment.value
corresponds toTrue
.
Constructors
Binding | |
Fields
|
Instances
Bifunctor Binding | |
(Lift s, Lift a) => Lift (Binding s a :: Type) | |
Foldable (Binding s) | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => Binding s m -> m foldMap :: Monoid m => (a -> m) -> Binding s a -> 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 elem :: Eq a => a -> Binding s a -> Bool maximum :: Ord a => Binding s a -> a minimum :: Ord a => Binding s a -> a | |
Traversable (Binding s) | |
Defined in Dhall.Syntax.Instances.Traversable | |
Functor (Binding s) | |
(Data a, Data s) => Data (Binding s a) | |
Defined in Dhall.Syntax.Instances.Data 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 :: forall r r'. (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) | |
Generic (Binding s a) Source # | |
(Show s, Show a) => Show (Binding s a) | |
(NFData s, NFData a) => NFData (Binding s a) | |
Defined in Dhall.Syntax.Instances.NFData | |
(Eq s, Eq a) => Eq (Binding s a) | |
(Ord s, Ord a) => Ord (Binding s a) | |
Defined in Dhall.Syntax.Instances.Ord | |
type Rep (Binding s a) Source # | |
Defined in Dhall.Syntax.Binding type Rep (Binding s a) = D1 ('MetaData "Binding" "Dhall.Syntax.Binding" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "Binding" 'PrefixI 'True) ((S1 ('MetaSel ('Just "bindingSrc0") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: (S1 ('MetaSel ('Just "variable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "bindingSrc1") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)))) :*: (S1 ('MetaSel ('Just "annotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Maybe s, Expr s a))) :*: (S1 ('MetaSel ('Just "bindingSrc2") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: S1 ('MetaSel ('Just "value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr s a)))))) |
makeBinding :: Text -> Expr s a -> Binding s a Source #
Construct a Binding
with no source information and no type annotation.
The body of an interpolated Text
literal
Instances
(Lift s, Lift a) => Lift (Chunks s a :: Type) | |
Foldable (Chunks s) | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => Chunks s m -> m foldMap :: Monoid m => (a -> m) -> Chunks s a -> 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 elem :: Eq a => a -> Chunks s a -> Bool maximum :: Ord a => Chunks s a -> a minimum :: Ord a => Chunks s a -> a | |
Traversable (Chunks s) | |
Defined in Dhall.Syntax.Instances.Traversable | |
Functor (Chunks s) | |
(Data a, Data s) => Data (Chunks s a) | |
Defined in Dhall.Syntax.Instances.Data 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 :: forall r r'. (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) | |
IsString (Chunks s a) Source # | |
Defined in Dhall.Syntax.Chunks Methods fromString :: String -> Chunks s a | |
Monoid (Chunks s a) Source # | |
Semigroup (Chunks s a) Source # | |
Generic (Chunks s a) Source # | |
(Show s, Show a) => Show (Chunks s a) | |
(NFData s, NFData a) => NFData (Chunks s a) | |
Defined in Dhall.Syntax.Instances.NFData | |
(Eq s, Eq a) => Eq (Chunks s a) | |
(Ord s, Ord a) => Ord (Chunks s a) | |
type Rep (Chunks s a) Source # | |
Defined in Dhall.Syntax.Chunks type Rep (Chunks s a) = D1 ('MetaData "Chunks" "Dhall.Syntax.Chunks" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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 Source #
Used to record the origin of a //
operator (i.e. from source code or a
product of desugaring)
Constructors
PreferFromSource | |
PreferFromCompletion |
Instances
Data PreferAnnotation | |
Defined in Dhall.Syntax.Instances.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PreferAnnotation -> c PreferAnnotation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PreferAnnotation toConstr :: PreferAnnotation -> Constr dataTypeOf :: PreferAnnotation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PreferAnnotation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PreferAnnotation) gmapT :: (forall b. Data b => b -> b) -> PreferAnnotation -> PreferAnnotation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PreferAnnotation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PreferAnnotation -> r gmapQ :: (forall d. Data d => d -> u) -> PreferAnnotation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PreferAnnotation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PreferAnnotation -> m PreferAnnotation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PreferAnnotation -> m PreferAnnotation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PreferAnnotation -> m PreferAnnotation | |
Generic PreferAnnotation Source # | |
Defined in Dhall.Syntax.Types Associated Types type Rep PreferAnnotation :: Type -> Type Methods from :: PreferAnnotation -> Rep PreferAnnotation x to :: Rep PreferAnnotation x -> PreferAnnotation | |
Show PreferAnnotation | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> PreferAnnotation -> ShowS show :: PreferAnnotation -> String showList :: [PreferAnnotation] -> ShowS | |
NFData PreferAnnotation | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: PreferAnnotation -> () | |
Eq PreferAnnotation | |
Defined in Dhall.Syntax.Instances.Eq Methods (==) :: PreferAnnotation -> PreferAnnotation -> Bool (/=) :: PreferAnnotation -> PreferAnnotation -> Bool | |
Ord PreferAnnotation | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: PreferAnnotation -> PreferAnnotation -> Ordering (<) :: PreferAnnotation -> PreferAnnotation -> Bool (<=) :: PreferAnnotation -> PreferAnnotation -> Bool (>) :: PreferAnnotation -> PreferAnnotation -> Bool (>=) :: PreferAnnotation -> PreferAnnotation -> Bool max :: PreferAnnotation -> PreferAnnotation -> PreferAnnotation min :: PreferAnnotation -> PreferAnnotation -> PreferAnnotation | |
Lift PreferAnnotation | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => PreferAnnotation -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => PreferAnnotation -> Code m PreferAnnotation | |
type Rep PreferAnnotation Source # | |
Defined in Dhall.Syntax.Types type Rep PreferAnnotation = D1 ('MetaData "PreferAnnotation" "Dhall.Syntax.Types" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "PreferFromSource" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreferFromCompletion" 'PrefixI 'False) (U1 :: Type -> Type)) |
data RecordField s a Source #
Record the field of a record-type and record-literal expression. The reason why we use the same ADT for both of them is because they store the same information.
For example,
{ {- A -} x {- B -} : {- C -} T }
... or
{ {- A -} x {- B -} = {- C -} T }
will be instantiated as follows:
recordFieldSrc0
corresponds to theA
comment.recordFieldValue
isT
recordFieldSrc1
corresponds to theB
comment.recordFieldSrc2
corresponds to theC
comment.
Although the A
comment isn't annotating the T
Record Field,
this is the best place to keep these comments.
Note that recordFieldSrc2
is always Nothing
when the RecordField
is for
a punned entry, because there is no =
sign. For example,
{ {- A -} x {- B -} }
will be instantiated as follows:
recordFieldSrc0
corresponds to theA
comment.recordFieldValue
corresponds to(Var "x")
recordFieldSrc1
corresponds to theB
comment.recordFieldSrc2
will beNothing
The labels involved in a record using dot-syntax like in this example:
{ {- A -} a {- B -} . {- C -} b {- D -} . {- E -} c {- F -} = {- G -} e }
will be instantiated as follows:
- For both the
a
andb
field,recordfieldSrc2
isNothing
- For the
a
field: recordFieldSrc0
corresponds to theA
commentrecordFieldSrc1
corresponds to theB
comment- For the
b
field: recordFieldSrc0
corresponds to theC
commentrecordFieldSrc1
corresponds to theD
comment- For the
c
field: recordFieldSrc0
corresponds to theE
commentrecordFieldSrc1
corresponds to theF
commentrecordFieldSrc2
corresponds to theG
comment
That is, for every label except the last one the semantics of
recordFieldSrc0
and recordFieldSrc1
are the same from a regular record
label but recordFieldSrc2
is always Nothing
. For the last keyword, all
srcs are Just
Constructors
RecordField | |
Fields
|
Instances
Bifunctor RecordField | |
Defined in Dhall.Syntax.Instances.Bifunctor Methods bimap :: (a -> b) -> (c -> d) -> RecordField a c -> RecordField b d first :: (a -> b) -> RecordField a c -> RecordField b c second :: (b -> c) -> RecordField a b -> RecordField a c | |
(Lift s, Lift a) => Lift (RecordField s a :: Type) | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => RecordField s a -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => RecordField s a -> Code m (RecordField s a) | |
Foldable (RecordField s) | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => RecordField s m -> m foldMap :: Monoid m => (a -> m) -> RecordField s a -> m foldMap' :: Monoid m => (a -> m) -> RecordField s a -> m foldr :: (a -> b -> b) -> b -> RecordField s a -> b foldr' :: (a -> b -> b) -> b -> RecordField s a -> b foldl :: (b -> a -> b) -> b -> RecordField s a -> b foldl' :: (b -> a -> b) -> b -> RecordField s a -> b foldr1 :: (a -> a -> a) -> RecordField s a -> a foldl1 :: (a -> a -> a) -> RecordField s a -> a toList :: RecordField s a -> [a] null :: RecordField s a -> Bool length :: RecordField s a -> Int elem :: Eq a => a -> RecordField s a -> Bool maximum :: Ord a => RecordField s a -> a minimum :: Ord a => RecordField s a -> a sum :: Num a => RecordField s a -> a product :: Num a => RecordField s a -> a | |
Traversable (RecordField s) | |
Defined in Dhall.Syntax.Instances.Traversable Methods traverse :: Applicative f => (a -> f b) -> RecordField s a -> f (RecordField s b) sequenceA :: Applicative f => RecordField s (f a) -> f (RecordField s a) mapM :: Monad m => (a -> m b) -> RecordField s a -> m (RecordField s b) sequence :: Monad m => RecordField s (m a) -> m (RecordField s a) | |
Functor (RecordField s) | |
Defined in Dhall.Syntax.Instances.Functor Methods fmap :: (a -> b) -> RecordField s a -> RecordField s b (<$) :: a -> RecordField s b -> RecordField s a | |
(Data a, Data s) => Data (RecordField s a) | |
Defined in Dhall.Syntax.Instances.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RecordField s a -> c (RecordField s a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RecordField s a) toConstr :: RecordField s a -> Constr dataTypeOf :: RecordField s a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RecordField s a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RecordField s a)) gmapT :: (forall b. Data b => b -> b) -> RecordField s a -> RecordField s a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RecordField s a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RecordField s a -> r gmapQ :: (forall d. Data d => d -> u) -> RecordField s a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RecordField s a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RecordField s a -> m (RecordField s a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordField s a -> m (RecordField s a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordField s a -> m (RecordField s a) | |
Generic (RecordField s a) Source # | |
Defined in Dhall.Syntax.RecordField Associated Types type Rep (RecordField s a) :: Type -> Type Methods from :: RecordField s a -> Rep (RecordField s a) x to :: Rep (RecordField s a) x -> RecordField s a | |
(Show s, Show a) => Show (RecordField s a) | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> RecordField s a -> ShowS show :: RecordField s a -> String showList :: [RecordField s a] -> ShowS | |
(NFData s, NFData a) => NFData (RecordField s a) | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: RecordField s a -> () | |
(Eq s, Eq a) => Eq (RecordField s a) | |
Defined in Dhall.Syntax.Instances.Eq Methods (==) :: RecordField s a -> RecordField s a -> Bool (/=) :: RecordField s a -> RecordField s a -> Bool | |
(Ord s, Ord a) => Ord (RecordField s a) | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: RecordField s a -> RecordField s a -> Ordering (<) :: RecordField s a -> RecordField s a -> Bool (<=) :: RecordField s a -> RecordField s a -> Bool (>) :: RecordField s a -> RecordField s a -> Bool (>=) :: RecordField s a -> RecordField s a -> Bool max :: RecordField s a -> RecordField s a -> RecordField s a min :: RecordField s a -> RecordField s a -> RecordField s a | |
type Rep (RecordField s a) Source # | |
Defined in Dhall.Syntax.RecordField type Rep (RecordField s a) = D1 ('MetaData "RecordField" "Dhall.Syntax.RecordField" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "RecordField" 'PrefixI 'True) ((S1 ('MetaSel ('Just "recordFieldSrc0") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: S1 ('MetaSel ('Just "recordFieldValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr s a))) :*: (S1 ('MetaSel ('Just "recordFieldSrc1") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: S1 ('MetaSel ('Just "recordFieldSrc2") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s))))) |
makeRecordField :: Expr s a -> RecordField s a Source #
Construct a RecordField
with no src information
data FunctionBinding s a Source #
Record the label of a function or a function-type expression
For example,
λ({- A -} a {- B -} : {- C -} T) -> e
… will be instantiated as follows:
functionBindingSrc0
corresponds to theA
commentfunctionBindingVariable
isa
functionBindingSrc1
corresponds to theB
commentfunctionBindingSrc2
corresponds to theC
commentfunctionBindingAnnotation
isT
Constructors
FunctionBinding | |
Fields
|
Instances
Bifunctor FunctionBinding | |
Defined in Dhall.Syntax.Instances.Bifunctor Methods bimap :: (a -> b) -> (c -> d) -> FunctionBinding a c -> FunctionBinding b d first :: (a -> b) -> FunctionBinding a c -> FunctionBinding b c second :: (b -> c) -> FunctionBinding a b -> FunctionBinding a c | |
(Lift s, Lift a) => Lift (FunctionBinding s a :: Type) | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => FunctionBinding s a -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => FunctionBinding s a -> Code m (FunctionBinding s a) | |
Foldable (FunctionBinding s) | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => FunctionBinding s m -> m foldMap :: Monoid m => (a -> m) -> FunctionBinding s a -> m foldMap' :: Monoid m => (a -> m) -> FunctionBinding s a -> m foldr :: (a -> b -> b) -> b -> FunctionBinding s a -> b foldr' :: (a -> b -> b) -> b -> FunctionBinding s a -> b foldl :: (b -> a -> b) -> b -> FunctionBinding s a -> b foldl' :: (b -> a -> b) -> b -> FunctionBinding s a -> b foldr1 :: (a -> a -> a) -> FunctionBinding s a -> a foldl1 :: (a -> a -> a) -> FunctionBinding s a -> a toList :: FunctionBinding s a -> [a] null :: FunctionBinding s a -> Bool length :: FunctionBinding s a -> Int elem :: Eq a => a -> FunctionBinding s a -> Bool maximum :: Ord a => FunctionBinding s a -> a minimum :: Ord a => FunctionBinding s a -> a sum :: Num a => FunctionBinding s a -> a product :: Num a => FunctionBinding s a -> a | |
Traversable (FunctionBinding s) | |
Defined in Dhall.Syntax.Instances.Traversable Methods traverse :: Applicative f => (a -> f b) -> FunctionBinding s a -> f (FunctionBinding s b) sequenceA :: Applicative f => FunctionBinding s (f a) -> f (FunctionBinding s a) mapM :: Monad m => (a -> m b) -> FunctionBinding s a -> m (FunctionBinding s b) sequence :: Monad m => FunctionBinding s (m a) -> m (FunctionBinding s a) | |
Functor (FunctionBinding s) | |
Defined in Dhall.Syntax.Instances.Functor Methods fmap :: (a -> b) -> FunctionBinding s a -> FunctionBinding s b (<$) :: a -> FunctionBinding s b -> FunctionBinding s a | |
(Data a, Data s) => Data (FunctionBinding s a) | |
Defined in Dhall.Syntax.Instances.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctionBinding s a -> c (FunctionBinding s a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FunctionBinding s a) toConstr :: FunctionBinding s a -> Constr dataTypeOf :: FunctionBinding s a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FunctionBinding s a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FunctionBinding s a)) gmapT :: (forall b. Data b => b -> b) -> FunctionBinding s a -> FunctionBinding s a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionBinding s a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionBinding s a -> r gmapQ :: (forall d. Data d => d -> u) -> FunctionBinding s a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionBinding s a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionBinding s a -> m (FunctionBinding s a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionBinding s a -> m (FunctionBinding s a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionBinding s a -> m (FunctionBinding s a) | |
Generic (FunctionBinding s a) Source # | |
Defined in Dhall.Syntax.FunctionBinding Associated Types type Rep (FunctionBinding s a) :: Type -> Type Methods from :: FunctionBinding s a -> Rep (FunctionBinding s a) x to :: Rep (FunctionBinding s a) x -> FunctionBinding s a | |
(Show s, Show a) => Show (FunctionBinding s a) | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> FunctionBinding s a -> ShowS show :: FunctionBinding s a -> String showList :: [FunctionBinding s a] -> ShowS | |
(NFData s, NFData a) => NFData (FunctionBinding s a) | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: FunctionBinding s a -> () | |
(Eq s, Eq a) => Eq (FunctionBinding s a) | |
Defined in Dhall.Syntax.Instances.Eq Methods (==) :: FunctionBinding s a -> FunctionBinding s a -> Bool (/=) :: FunctionBinding s a -> FunctionBinding s a -> Bool | |
(Ord s, Ord a) => Ord (FunctionBinding s a) | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: FunctionBinding s a -> FunctionBinding s a -> Ordering (<) :: FunctionBinding s a -> FunctionBinding s a -> Bool (<=) :: FunctionBinding s a -> FunctionBinding s a -> Bool (>) :: FunctionBinding s a -> FunctionBinding s a -> Bool (>=) :: FunctionBinding s a -> FunctionBinding s a -> Bool max :: FunctionBinding s a -> FunctionBinding s a -> FunctionBinding s a min :: FunctionBinding s a -> FunctionBinding s a -> FunctionBinding s a | |
type Rep (FunctionBinding s a) Source # | |
Defined in Dhall.Syntax.FunctionBinding type Rep (FunctionBinding s a) = D1 ('MetaData "FunctionBinding" "Dhall.Syntax.FunctionBinding" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "FunctionBinding" 'PrefixI 'True) ((S1 ('MetaSel ('Just "functionBindingSrc0") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: S1 ('MetaSel ('Just "functionBindingVariable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :*: (S1 ('MetaSel ('Just "functionBindingSrc1") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: (S1 ('MetaSel ('Just "functionBindingSrc2") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: S1 ('MetaSel ('Just "functionBindingAnnotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr s a)))))) |
makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a Source #
Smart constructor for FunctionBinding
with no src information
data FieldSelection s Source #
Record the field on a selector-expression
For example,
e . {- A -} x {- B -}
… will be instantiated as follows:
fieldSelectionSrc0
corresponds to theA
commentfieldSelectionLabel
corresponds tox
fieldSelectionSrc1
corresponds to theB
comment
Given our limitation that not all expressions recover their whitespaces, the
purpose of fieldSelectionSrc1
is to save the SourcePos
where the fieldSelectionLabel
ends, but we still use a
'Maybe Dhall.Src.Src' (s =
) to be consistent with similar
data types such as Src
Binding
, for example.
Constructors
FieldSelection | |
Fields
|
Instances
Foldable FieldSelection | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => FieldSelection m -> m foldMap :: Monoid m => (a -> m) -> FieldSelection a -> m foldMap' :: Monoid m => (a -> m) -> FieldSelection a -> m foldr :: (a -> b -> b) -> b -> FieldSelection a -> b foldr' :: (a -> b -> b) -> b -> FieldSelection a -> b foldl :: (b -> a -> b) -> b -> FieldSelection a -> b foldl' :: (b -> a -> b) -> b -> FieldSelection a -> b foldr1 :: (a -> a -> a) -> FieldSelection a -> a foldl1 :: (a -> a -> a) -> FieldSelection a -> a toList :: FieldSelection a -> [a] null :: FieldSelection a -> Bool length :: FieldSelection a -> Int elem :: Eq a => a -> FieldSelection a -> Bool maximum :: Ord a => FieldSelection a -> a minimum :: Ord a => FieldSelection a -> a sum :: Num a => FieldSelection a -> a product :: Num a => FieldSelection a -> a | |
Traversable FieldSelection | |
Defined in Dhall.Syntax.Instances.Traversable Methods traverse :: Applicative f => (a -> f b) -> FieldSelection a -> f (FieldSelection b) sequenceA :: Applicative f => FieldSelection (f a) -> f (FieldSelection a) mapM :: Monad m => (a -> m b) -> FieldSelection a -> m (FieldSelection b) sequence :: Monad m => FieldSelection (m a) -> m (FieldSelection a) | |
Functor FieldSelection | |
Defined in Dhall.Syntax.Instances.Functor Methods fmap :: (a -> b) -> FieldSelection a -> FieldSelection b (<$) :: a -> FieldSelection b -> FieldSelection a | |
Lift s => Lift (FieldSelection s :: Type) | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => FieldSelection s -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => FieldSelection s -> Code m (FieldSelection s) | |
Data s => Data (FieldSelection s) | |
Defined in Dhall.Syntax.Instances.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FieldSelection s -> c (FieldSelection s) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FieldSelection s) toConstr :: FieldSelection s -> Constr dataTypeOf :: FieldSelection s -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FieldSelection s)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FieldSelection s)) gmapT :: (forall b. Data b => b -> b) -> FieldSelection s -> FieldSelection s gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FieldSelection s -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FieldSelection s -> r gmapQ :: (forall d. Data d => d -> u) -> FieldSelection s -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FieldSelection s -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FieldSelection s -> m (FieldSelection s) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldSelection s -> m (FieldSelection s) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldSelection s -> m (FieldSelection s) | |
Generic (FieldSelection s) Source # | |
Defined in Dhall.Syntax.Types Associated Types type Rep (FieldSelection s) :: Type -> Type Methods from :: FieldSelection s -> Rep (FieldSelection s) x to :: Rep (FieldSelection s) x -> FieldSelection s | |
Show s => Show (FieldSelection s) | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> FieldSelection s -> ShowS show :: FieldSelection s -> String showList :: [FieldSelection s] -> ShowS | |
NFData s => NFData (FieldSelection s) | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: FieldSelection s -> () | |
Eq s => Eq (FieldSelection s) | |
Defined in Dhall.Syntax.Instances.Eq Methods (==) :: FieldSelection s -> FieldSelection s -> Bool (/=) :: FieldSelection s -> FieldSelection s -> Bool | |
Ord s => Ord (FieldSelection s) | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: FieldSelection s -> FieldSelection s -> Ordering (<) :: FieldSelection s -> FieldSelection s -> Bool (<=) :: FieldSelection s -> FieldSelection s -> Bool (>) :: FieldSelection s -> FieldSelection s -> Bool (>=) :: FieldSelection s -> FieldSelection s -> Bool max :: FieldSelection s -> FieldSelection s -> FieldSelection s min :: FieldSelection s -> FieldSelection s -> FieldSelection s | |
type Rep (FieldSelection s) Source # | |
Defined in Dhall.Syntax.Types type Rep (FieldSelection s) = D1 ('MetaData "FieldSelection" "Dhall.Syntax.Types" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "FieldSelection" 'PrefixI 'True) (S1 ('MetaSel ('Just "fieldSelectionSrc0") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s)) :*: (S1 ('MetaSel ('Just "fieldSelectionLabel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Just "fieldSelectionSrc1") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe s))))) |
makeFieldSelection :: Text -> FieldSelection s Source #
Smart constructor for FieldSelection
with no src information
data WithComponent Source #
A path component for a with
expression
Constructors
WithLabel Text | |
WithQuestion |
Instances
Data WithComponent | |
Defined in Dhall.Syntax.Instances.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithComponent -> c WithComponent gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WithComponent toConstr :: WithComponent -> Constr dataTypeOf :: WithComponent -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WithComponent) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WithComponent) gmapT :: (forall b. Data b => b -> b) -> WithComponent -> WithComponent gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithComponent -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithComponent -> r gmapQ :: (forall d. Data d => d -> u) -> WithComponent -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> WithComponent -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithComponent -> m WithComponent gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithComponent -> m WithComponent gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithComponent -> m WithComponent | |
Generic WithComponent Source # | |
Defined in Dhall.Syntax.Types Associated Types type Rep WithComponent :: Type -> Type | |
Show WithComponent | |
Defined in Dhall.Syntax.Instances.Show Methods showsPrec :: Int -> WithComponent -> ShowS show :: WithComponent -> String showList :: [WithComponent] -> ShowS | |
NFData WithComponent | |
Defined in Dhall.Syntax.Instances.NFData Methods rnf :: WithComponent -> () | |
Eq WithComponent | |
Defined in Dhall.Syntax.Instances.Eq | |
Ord WithComponent | |
Defined in Dhall.Syntax.Instances.Ord Methods compare :: WithComponent -> WithComponent -> Ordering (<) :: WithComponent -> WithComponent -> Bool (<=) :: WithComponent -> WithComponent -> Bool (>) :: WithComponent -> WithComponent -> Bool (>=) :: WithComponent -> WithComponent -> Bool max :: WithComponent -> WithComponent -> WithComponent min :: WithComponent -> WithComponent -> WithComponent | |
Lift WithComponent | |
Defined in Dhall.Syntax.Instances.Lift Methods lift :: Quote m => WithComponent -> m Exp liftTyped :: forall (m :: Type -> Type). Quote m => WithComponent -> Code m WithComponent | |
type Rep WithComponent Source # | |
Defined in Dhall.Syntax.Types type Rep WithComponent = D1 ('MetaData "WithComponent" "Dhall.Syntax.Types" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" 'False) (C1 ('MetaCons "WithLabel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "WithQuestion" 'PrefixI 'False) (U1 :: Type -> Type)) |
Syntax tree for expressions
The s
type parameter is used to track the presence or absence of
Src
spans:
- If
s =
then the code may containsSrc
Src
spans (either in aNote
constructor or inline within another constructor, likeLet
) - If
s =
then the code has noVoid
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 (Maybe CharacterSet) (FunctionBinding s a) (Expr s a) | Lam _ (FunctionBinding _ "x" _ _ A) b ~ λ(x : A) -> b |
Pi (Maybe CharacterSet) 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 See |
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 |
Bytes | Bytes ~ Bytes |
BytesLit ByteString | BytesLit "\x00\xFF" ~ 0x"00FF" |
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 |
TextReplace | TextReplace ~ Text/replace |
TextShow | TextShow ~ Text/show |
Date | Date ~ Date |
DateLiteral Day | DateLiteral (fromGregorian _YYYY _MM _DD) ~ YYYY-MM-DD |
DateShow | DateShow ~ Date/show |
Time | Time ~ Time |
TimeLiteral | TimeLiteral (TimeOfDay hh mm ss) _ ~ hh:mm:ss |
Fields
| |
TimeShow | |
TimeZone | TimeZone ~ TimeZone |
TimeZoneLiteral TimeZone | TimeZoneLiteral (TimeZone ( 60 * _HH + _MM) _ _) ~ +HH:MM | > TimeZoneLiteral (TimeZone (-60 * _HH + _MM) _ _) ~ -HH:MM |
TimeZoneShow | TimeZoneShow ~ TimeZone/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
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 (RecordField s a)) | Record [ (k1, RecordField _ t1) ~ { k1 : t1, k2 : t1 } , (k2, RecordField _ t2) ] |
RecordLit (Map Text (RecordField s a)) | RecordLit [ (k1, RecordField _ v1) ~ { k1 = v1, k2 = v2 } , (k2, RecordField _ v2) ] |
Union (Map Text (Maybe (Expr s a))) | Union [(k1, Just t1), (k2, Nothing)] ~ < k1 : t1 | k2 > |
Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a) | Combine _ Nothing x y ~ x ∧ y The first field is a RecordLit [ ( k ~ { k = x, k = y } , RecordField _ (Combine (Just k) x y) )] |
CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a) | CombineTypes _ x y ~ x ⩓ y |
Prefer (Maybe CharacterSet) PreferAnnotation (Expr s a) (Expr s a) | Prefer _ _ x y ~ x ⫽ y |
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 |
ShowConstructor (Expr s a) | ShowConstructor x ~ showConstructor x |
Field (Expr s a) (FieldSelection s) | Field e (FieldSelection _ x _) ~ e.x |
Project (Expr s a) (Either [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 (Maybe CharacterSet) (Expr s a) (Expr s a) | Equivalent _ x y ~ x ≡ y |
With (Expr s a) (NonEmpty WithComponent) (Expr s a) | With x y e ~ x with y = e |
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 | |
(Lift s, Lift a) => Lift (Expr s a :: Type) | |
Foldable (Expr s) | |
Defined in Dhall.Syntax.Instances.Foldable Methods fold :: Monoid m => Expr s m -> m foldMap :: Monoid m => (a -> m) -> Expr s a -> 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 elem :: Eq a => a -> Expr s a -> Bool maximum :: Ord a => Expr s a -> a | |
Traversable (Expr s) | |
Applicative (Expr s) | |
Functor (Expr s) | |
Monad (Expr s) | |
(Data a, Data s) => Data (Expr s a) | |
Defined in Dhall.Syntax.Instances.Data 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 :: forall r r'. (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) | |
IsString (Expr s a) Source # | |
Defined in Dhall.Syntax.Expr Methods fromString :: String -> Expr s a | |
Generic (Expr s a) Source # | |
(Show s, Show a) => Show (Expr s a) | |
(NFData s, NFData a) => NFData (Expr s a) | |
Defined in Dhall.Syntax.Instances.NFData | |
(Eq s, Eq a) => Eq (Expr s a) | This instance encodes what the Dhall standard calls an "exact match" between two expressions. Note that
|
(Ord s, Ord a) => Ord (Expr s a) | Note that this |
Defined in Dhall.Syntax.Instances.Ord | |
Pretty a => Pretty (Expr s a) | Generates a syntactically valid Dhall program |
Defined in Dhall.Syntax.Instances.Pretty | |
Serialise (Expr Void Void) | |
Defined in Dhall.Binary Methods encode :: Expr Void Void -> Encoding decode :: Decoder s (Expr Void Void) encodeList :: [Expr Void Void] -> Encoding decodeList :: Decoder s [Expr Void Void] | |
Serialise (Expr Void Import) | |
Defined in Dhall.Binary | |
type Rep (Expr s a) Source # | |
Defined in Dhall.Syntax.Expr type Rep (Expr s a) = D1 ('MetaData "Expr" "Dhall.Syntax.Expr" "dhall-1.42.1-7Gn60Ylzvt3KI4yZM8Lxo" '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 (Maybe CharacterSet)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FunctionBinding 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 (Maybe CharacterSet)) :*: 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 "Bytes" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BytesLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ByteString)) :+: 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 "TextReplace" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "TextShow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Date" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DateLiteral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Day)) :+: (C1 ('MetaCons "DateShow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Time" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TimeLiteral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeOfDay) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word)) :+: C1 ('MetaCons "TimeShow" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TimeZone" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TimeZoneLiteral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeZone)) :+: C1 ('MetaCons "TimeZoneShow" '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 (RecordField s a)))) :+: C1 ('MetaCons "RecordLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Text (RecordField 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 CharacterSet)) :*: 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 (Maybe CharacterSet)) :*: (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 (Maybe CharacterSet)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PreferAnnotation)) :*: (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 "ShowConstructor" '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 (FieldSelection s))) :+: 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 [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 (Maybe CharacterSet)) :*: (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 WithComponent)) :*: 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
>>>
mfb = Syntax.makeFunctionBinding
>>>
alphaNormalize (Lam mempty (mfb "a" (Const Type)) (Lam mempty (mfb "b" (Const Type)) (Lam mempty (mfb "x" "a") (Lam mempty (mfb "y" "b") "x"))))
Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = 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.
Constructors
ReifiedNormalizer | |
Fields |
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
tox@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 lessx
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
,
is equivalent to
isNormalized
ee ==
.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
shallowDenote :: Expr s a -> Expr s a Source #
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 mempty (Syntax.makeFunctionBinding "x" (Const Type)) "x"
False
Pretty-printing
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.
subExpressionsWith :: Applicative f => (a -> f (Expr s b)) -> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b) Source #
A traversal over the immediate sub-expressions of an expression which allows mapping embedded values
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 #
recordFieldExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> RecordField s a -> f (RecordField s b) Source #
Traverse over the immediate Expr
children in a RecordField
.
functionBindingExprs :: Applicative f => (Expr s a -> f (Expr s b)) -> FunctionBinding s a -> f (FunctionBinding s b) Source #
Traverse over the immediate Expr
children in a FunctionBinding
.
Let-blocks
wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a Source #
Wrap let-Binding
s 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
This type represents 1 or more nested Let
bindings that have been
coalesced together for ease of manipulation
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 Text
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