| Safe Haskell | None |
|---|---|
| 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 {}
- data ImportMode
- data ImportType
- data URL = URL {}
- data Scheme
- newtype DhallDouble = DhallDouble {}
- 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 Expr s a
- = Const Const
- | Var Var
- | Lam Text (Expr s a) (Expr s a)
- | Pi Text (Expr s a) (Expr s a)
- | App (Expr s a) (Expr s a)
- | Let (Binding s a) (Expr s a)
- | Annot (Expr s a) (Expr s a)
- | Bool
- | BoolLit Bool
- | BoolAnd (Expr s a) (Expr s a)
- | BoolOr (Expr s a) (Expr s a)
- | BoolEQ (Expr s a) (Expr s a)
- | BoolNE (Expr s a) (Expr s a)
- | BoolIf (Expr s a) (Expr s a) (Expr s a)
- | Natural
- | NaturalLit Natural
- | NaturalFold
- | NaturalBuild
- | NaturalIsZero
- | NaturalEven
- | NaturalOdd
- | NaturalToInteger
- | NaturalShow
- | NaturalSubtract
- | NaturalPlus (Expr s a) (Expr s a)
- | NaturalTimes (Expr s a) (Expr s a)
- | Integer
- | IntegerLit Integer
- | IntegerShow
- | IntegerToDouble
- | Double
- | DoubleLit DhallDouble
- | DoubleShow
- | Text
- | TextLit (Chunks s a)
- | TextAppend (Expr s a) (Expr s a)
- | TextShow
- | 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
- | OptionalFold
- | OptionalBuild
- | Record (Map Text (Expr s a))
- | RecordLit (Map Text (Expr s a))
- | Union (Map Text (Maybe (Expr s a)))
- | Combine (Expr s a) (Expr s a)
- | CombineTypes (Expr s a) (Expr s a)
- | Prefer (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))
- | Field (Expr s a) Text
- | Project (Expr s a) (Either (Set Text) (Expr s a))
- | Assert (Expr s a)
- | Equivalent (Expr s a) (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)
- 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)
- 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
| Bounded Const Source # | |
| Enum Const Source # | |
| Eq Const Source # | |
| Data Const Source # | |
Defined in Dhall.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Const -> c Const # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Const # dataTypeOf :: Const -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Const) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Const) # gmapT :: (forall b. Data b => b -> b) -> Const -> Const # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r # gmapQ :: (forall d. Data d => d -> u) -> Const -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Const -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Const -> m Const # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const # | |
| Ord Const Source # | |
| Show Const Source # | |
| Generic Const Source # | |
| Lift Const Source # | |
| NFData Const Source # | |
Defined in Dhall.Syntax | |
| Pretty Const Source # | |
Defined in Dhall.Syntax | |
| type Rep Const Source # | |
Defined in Dhall.Syntax | |
Internal representation of a directory that stores the path components in reverse order
In other words, the directory /foo/bar/baz is encoded as
Directory { components = [ "baz", "bar", "foo" ] }
Constructors
| Directory | |
Fields
| |
Instances
| Eq Directory Source # | |
| Ord Directory Source # | |
| Show Directory Source # | |
| Generic Directory Source # | |
| Semigroup Directory Source # | |
| NFData Directory Source # | |
Defined in Dhall.Syntax | |
| Pretty Directory Source # | |
Defined in Dhall.Syntax | |
| type Rep Directory Source # | |
Defined in Dhall.Syntax | |
Instances
| Eq File Source # | |
| Ord File Source # | |
| Show File Source # | |
| Generic File Source # | |
| Semigroup File Source # | |
| NFData File Source # | |
Defined in Dhall.Syntax | |
| Pretty File Source # | |
Defined in Dhall.Syntax | |
| type Rep File Source # | |
Defined in Dhall.Syntax type Rep File = D1 (MetaData "File" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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
Reference to an external resource
Constructors
| Import | |
Fields | |
Instances
| Eq Import Source # | |
| Ord Import Source # | |
| Show Import Source # | |
| Generic Import Source # | |
| Semigroup Import Source # | |
| NFData Import Source # | |
Defined in Dhall.Syntax | |
| Pretty Import Source # | |
Defined in Dhall.Syntax | |
| FromTerm Import Source # | |
| ToTerm Import Source # | |
| type Rep Import Source # | |
Defined in Dhall.Syntax type Rep Import = D1 (MetaData "Import" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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 ImportMode Source #
How to interpret the import's contents (i.e. as Dhall code or raw text)
Instances
| Eq ImportMode Source # | |
Defined in Dhall.Syntax | |
| Ord ImportMode Source # | |
Defined in Dhall.Syntax 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 # | |
| Show ImportMode Source # | |
Defined in Dhall.Syntax Methods showsPrec :: Int -> ImportMode -> ShowS # show :: ImportMode -> String # showList :: [ImportMode] -> ShowS # | |
| Generic ImportMode Source # | |
Defined in Dhall.Syntax Associated Types type Rep ImportMode :: Type -> Type # | |
| NFData ImportMode Source # | |
Defined in Dhall.Syntax Methods rnf :: ImportMode -> () # | |
| type Rep ImportMode Source # | |
Defined in Dhall.Syntax | |
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
This type stores all of the components of a remote import
Constructors
| URL | |
Instances
| Eq URL Source # | |
| Ord URL Source # | |
| Show URL Source # | |
| Generic URL Source # | |
| NFData URL Source # | |
Defined in Dhall.Syntax | |
| Pretty URL Source # | |
Defined in Dhall.Syntax | |
| type Rep URL Source # | |
Defined in Dhall.Syntax type Rep URL = D1 (MetaData "URL" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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
newtype DhallDouble Source #
This wrapper around Double exists for its Eq instance which is
defined via the binary encoding of Dhall Doubles.
Constructors
| DhallDouble | |
Fields | |
Instances
| Eq DhallDouble Source # | 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 | |
| Data DhallDouble Source # | |
Defined in Dhall.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DhallDouble -> c DhallDouble # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DhallDouble # toConstr :: DhallDouble -> Constr # dataTypeOf :: DhallDouble -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DhallDouble) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DhallDouble) # gmapT :: (forall b. Data b => b -> b) -> DhallDouble -> DhallDouble # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DhallDouble -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DhallDouble -> r # gmapQ :: (forall d. Data d => d -> u) -> DhallDouble -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DhallDouble -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DhallDouble -> m DhallDouble # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DhallDouble -> m DhallDouble # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DhallDouble -> m DhallDouble # | |
| Ord DhallDouble Source # | This instance relies on the |
Defined in Dhall.Syntax 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 # | |
| Show DhallDouble Source # | |
Defined in Dhall.Syntax Methods showsPrec :: Int -> DhallDouble -> ShowS # show :: DhallDouble -> String # showList :: [DhallDouble] -> ShowS # | |
| Generic DhallDouble Source # | |
Defined in Dhall.Syntax Associated Types type Rep DhallDouble :: Type -> Type # | |
| NFData DhallDouble Source # | |
Defined in Dhall.Syntax Methods rnf :: DhallDouble -> () # | |
| ToTerm DhallDouble Source # | |
Defined in Dhall.Binary Methods encode :: DhallDouble -> Term Source # | |
| type Rep DhallDouble Source # | |
Defined in Dhall.Syntax type Rep DhallDouble = D1 (MetaData "DhallDouble" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" True) (C1 (MetaCons "DhallDouble" PrefixI True) (S1 (MetaSel (Just "getDhallDouble") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Double))) | |
Label for a bound variable
The Expr field is the variable's name (i.e. "x").
The Int field disambiguates variables with the same name if there are
multiple bound variables of the same name in scope. Zero refers to the
nearest bound variable and the index increases by one for each bound
variable of the same name going outward. The following diagram may help:
┌──refers to──┐
│ │
v │
λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0
┌─────────────────refers to─────────────────┐
│ │
v │
λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1This 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) → xZero indices are omitted when pretty-printing Vars and non-zero indices
appear as a numeric suffix.
Instances
| Eq Var Source # | |
| Data Var Source # | |
Defined in Dhall.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var -> c Var # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var # dataTypeOf :: Var -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Var) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var) # gmapT :: (forall b. Data b => b -> b) -> Var -> Var # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r # gmapQ :: (forall d. Data d => d -> u) -> Var -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var -> m Var # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var # | |
| Ord Var Source # | |
| Show Var Source # | |
| IsString Var Source # | |
Defined in Dhall.Syntax Methods fromString :: String -> Var # | |
| Generic Var Source # | |
| Lift Var Source # | |
| NFData Var Source # | |
Defined in Dhall.Syntax | |
| Pretty Var Source # | |
Defined in Dhall.Syntax | |
| type Rep Var Source # | |
Defined in Dhall.Syntax type Rep Var = D1 (MetaData "Var" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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 x : Bool = True in x will be instantiated as follows:
bindingSrc0corresponds to theAcomment.variableis"x"bindingSrc1corresponds to theBcomment.annotationisJusta pair, corresponding to theCcomment andBool.bindingSrc2corresponds to theDcomment.valuecorresponds toTrue.
Constructors
| Binding | |
Fields
| |
Instances
| Bifunctor Binding Source # | |
| Functor (Binding s) Source # | |
| Foldable (Binding s) Source # | |
Defined in Dhall.Syntax Methods fold :: Monoid m => Binding s m -> m # foldMap :: Monoid m => (a -> m) -> Binding s a -> m # foldr :: (a -> b -> b) -> b -> Binding s a -> b # foldr' :: (a -> b -> b) -> b -> Binding s a -> b # foldl :: (b -> a -> b) -> b -> Binding s a -> b # foldl' :: (b -> a -> b) -> b -> Binding s a -> b # foldr1 :: (a -> a -> a) -> Binding s a -> a # foldl1 :: (a -> a -> a) -> Binding s a -> a # toList :: Binding s a -> [a] # length :: Binding s a -> Int # elem :: Eq a => a -> Binding s a -> Bool # maximum :: Ord a => Binding s a -> a # minimum :: Ord a => Binding s a -> a # | |
| Traversable (Binding s) Source # | |
| (Eq s, Eq a) => Eq (Binding s a) Source # | |
| (Data s, Data a) => Data (Binding s a) Source # | |
Defined in Dhall.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binding s a -> c (Binding s a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binding s a) # toConstr :: Binding s a -> Constr # dataTypeOf :: Binding s a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binding s a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binding s a)) # gmapT :: (forall b. Data b => b -> b) -> Binding s a -> Binding s a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binding s a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binding s a -> r # gmapQ :: (forall d. Data d => d -> u) -> Binding s a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binding s a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding s a -> m (Binding s a) # | |
| (Ord s, Ord a) => Ord (Binding s a) Source # | |
Defined in Dhall.Syntax | |
| (Show s, Show a) => Show (Binding s a) Source # | |
| Generic (Binding s a) Source # | |
| (NFData s, NFData a) => NFData (Binding s a) Source # | |
Defined in Dhall.Syntax | |
| type Rep (Binding s a) Source # | |
Defined in Dhall.Syntax type Rep (Binding s a) = D1 (MetaData "Binding" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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
| Functor (Chunks s) Source # | |
| Foldable (Chunks s) Source # | |
Defined in Dhall.Syntax Methods fold :: Monoid m => Chunks s m -> m # foldMap :: Monoid m => (a -> m) -> Chunks s a -> m # foldr :: (a -> b -> b) -> b -> Chunks s a -> b # foldr' :: (a -> b -> b) -> b -> Chunks s a -> b # foldl :: (b -> a -> b) -> b -> Chunks s a -> b # foldl' :: (b -> a -> b) -> b -> Chunks s a -> b # foldr1 :: (a -> a -> a) -> Chunks s a -> a # foldl1 :: (a -> a -> a) -> Chunks s a -> a # 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) Source # | |
| (Eq s, Eq a) => Eq (Chunks s a) Source # | |
| (Data s, Data a) => Data (Chunks s a) Source # | |
Defined in Dhall.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Chunks s a -> c (Chunks s a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Chunks s a) # toConstr :: Chunks s a -> Constr # dataTypeOf :: Chunks s a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Chunks s a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Chunks s a)) # gmapT :: (forall b. Data b => b -> b) -> Chunks s a -> Chunks s a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Chunks s a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Chunks s a -> r # gmapQ :: (forall d. Data d => d -> u) -> Chunks s a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Chunks s a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Chunks s a -> m (Chunks s a) # | |
| (Ord s, Ord a) => Ord (Chunks s a) Source # | |
| (Show s, Show a) => Show (Chunks s a) Source # | |
| IsString (Chunks s a) Source # | |
Defined in Dhall.Syntax Methods fromString :: String -> Chunks s a # | |
| Generic (Chunks s a) Source # | |
| Semigroup (Chunks s a) Source # | |
| Monoid (Chunks s a) Source # | |
| (Lift s, Lift a, Data s, Data a) => Lift (Chunks s a) Source # | |
| (NFData s, NFData a) => NFData (Chunks s a) Source # | |
Defined in Dhall.Syntax | |
| type Rep (Chunks s a) Source # | |
Defined in Dhall.Syntax type Rep (Chunks s a) = D1 (MetaData "Chunks" "Dhall.Syntax" "dhall-1.27.0-JmSUw037kSChLDht9wrsx" 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))) | |
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 containsSrcSrcspans (either in aNotedconstructor or inline within another constructor, likeLet) - If
s =then the code has noVoidSrcspans
The a type parameter is used to track the presence or absence of imports
Constructors
| Const Const | Const c ~ c |
| Var Var | Var (V x 0) ~ x Var (V x n) ~ x@n |
| Lam Text (Expr s a) (Expr s a) | Lam x A b ~ λ(x : A) -> b |
| Pi Text (Expr s a) (Expr s a) | Pi "_" A B ~ A -> B Pi x A B ~ ∀(x : A) -> B |
| App (Expr s a) (Expr s a) | App f a ~ f a |
| Let (Binding s a) (Expr s a) | Let (Binding _ x _ Nothing _ r) e ~ let x = r in e Let (Binding _ x _ (Just t ) _ r) e ~ let x : t = r in e The difference between let x = a let y = b in e and let x = a in let y = b in e is only an additional 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 |
| 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 |
| IntegerShow | IntegerShow ~ Integer/show |
| IntegerToDouble | IntegerToDouble ~ Integer/toDouble |
| Double | Double ~ Double |
| DoubleLit DhallDouble | DoubleLit n ~ n |
| DoubleShow | DoubleShow ~ Double/show |
| Text | Text ~ Text |
| TextLit (Chunks s a) | TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3" |
| TextAppend (Expr s a) (Expr s a) | TextAppend x y ~ x ++ y |
| TextShow | TextShow ~ Text/show |
| List | List ~ List |
| ListLit (Maybe (Expr s a)) (Seq (Expr s a)) | ListLit (Just t ) [] ~ [] : t ListLit Nothing [x, y, z] ~ [x, y, z] Invariant: A non-empty list literal is always represented as
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 |
| OptionalFold | OptionalFold ~ Optional/fold |
| OptionalBuild | OptionalBuild ~ Optional/build |
| Record (Map Text (Expr s a)) | Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 } |
| RecordLit (Map Text (Expr s a)) | RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 } |
| Union (Map Text (Maybe (Expr s a))) | Union [(k1, Just t1), (k2, Nothing)] ~ < k1 : t1 | k2 > |
| Combine (Expr s a) (Expr s a) | Combine x y ~ x ∧ y |
| CombineTypes (Expr s a) (Expr s a) | CombineTypes x y ~ x ⩓ y |
| Prefer (Expr s a) (Expr s a) | Prefer x y ~ x ⫽ y |
| RecordCompletion (Expr s a) (Expr s a) | RecordCompletion x y ~ x::y |
| Merge (Expr s a) (Expr s a) (Maybe (Expr s a)) | Merge x y (Just t ) ~ merge x y : t Merge x y Nothing ~ merge x y |
| ToMap (Expr s a) (Maybe (Expr s a)) | ToMap x (Just t) ~ toMap x : t ToMap x Nothing ~ toMap x |
| Field (Expr s a) Text | Field e x ~ e.x |
| Project (Expr s a) (Either (Set Text) (Expr s a)) | Project e (Left xs) ~ e.{ xs }| > Project e (Right t) ~ e.(t) |
| Assert (Expr s a) | Assert e ~ assert : e |
| Equivalent (Expr s a) (Expr s a) | Equivalent x y ~ x ≡ y |
| 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
Normalization
alphaNormalize :: Expr s a -> Expr s a Source #
α-normalize an expression by renaming all bound variables to "_" and
using De Bruijn indices to distinguish them
>>>alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x"))))Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1)))))
α-normalization does not affect free variables:
>>>alphaNormalize "x"Var (V "x" 0)
normalize :: Eq a => Expr s a -> Expr t a Source #
Reduce an expression to its normal form, performing beta reduction
normalize does not type-check the expression. You may want to type-check
expressions before normalizing them since normalization can convert an
ill-typed expression into a well-typed expression.
normalize can also fail with error if you normalize an ill-typed
expression
normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a Source #
Reduce an expression to its normal form, performing beta reduction and applying any custom definitions.
normalizeWith is designed to be used with function typeWith. The typeWith
function allows typing of Dhall functions in a custom typing context whereas
normalizeWith allows evaluating Dhall expressions in a custom context.
To be more precise normalizeWith applies the given normalizer when it finds an
application term that it cannot reduce by other means.
Note that the context used in normalization will determine the properties of normalization. That is, if the functions in custom context are not total then the Dhall language, evaluated with those functions is not total either.
normalizeWith can fail with an error if you normalize an ill-typed
expression
normalizeWithM :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a) Source #
This function generalizes normalizeWith by allowing the custom normalizer
to use an arbitrary Monad
normalizeWithM can fail with an error if you normalize an ill-typed
expression
type Normalizer a = NormalizerM Identity a Source #
An variation on NormalizerM for pure normalizers
type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a)) Source #
Use this to wrap you embedded functions (see normalizeWith) to make them
polymorphic enough to be used.
newtype ReifiedNormalizer a Source #
A reified Normalizer, which can be stored in structures without
running into impredicative polymorphism.
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@1tox@2before we substitute it into the body of the innermost lambda expression in order to avoid variable capture. This substitution changes the body of the lambda expression to(f x@2 x@1) - We then remove the innermost lambda and therefore decrease the indices of
both
xs in(f x@2 x@1)to(f x@1 x)in order to reflect that one lessxvariable 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
1to avoid variable capture during substitution - decrement variables by
1when deleting lambdas after substitution
n starts off at 0 when substitution begins and increments every time we
descend into a lambda or let expression that binds a variable of the same
name in order to avoid shifting the bound variables by mistake.
isNormalized :: Eq a => Expr s a -> Bool Source #
Quickly check if an expression is in normal form
Given a well-typed expression e, isNormalized 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 "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.
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 #
Let-blocks
wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a Source #
Wrap let-Bindings around an Expr.
wrapInLets can be understood as an inverse for multiLet:
let MultiLet bs e1 = multiLet b e0 wrapInLets bs e1 == Let b e0
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
escapeText :: Text -> Text Source #
Escape a Expr literal using Dhall's escaping rules
Note that the result does not include surrounding quotes
pathCharacter :: Char -> Bool Source #
Returns True if the given Char is valid within an unquoted path
component
This is exported for reuse within the Dhall.Parser.Token module