{-# LANGUAGE BangPatterns #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UnicodeSyntax #-} {-| This module contains the core syntax types and optics for them. 'reservedIdentifiers', 'denote' and friends are included because they are involved in a dependency circle with "Dhall.Pretty.Internal". -} module Dhall.Syntax ( -- * 'Expr' Const(..) , Var(..) , Binding(..) , makeBinding , Chunks(..) , DhallDouble(..) , Expr(..) -- ** 'Let'-blocks , MultiLet(..) , multiLet , wrapInLets -- ** Optics , subExpressions , chunkExprs , bindingExprs -- ** Handling 'Note's , denote , renote , shallowDenote -- * 'Import' , Directory(..) , File(..) , FilePrefix(..) , Import(..) , ImportHashed(..) , ImportMode(..) , ImportType(..) , URL(..) , Scheme(..) , pathCharacter -- * Reserved identifiers , reservedIdentifiers ) where import Control.DeepSeq (NFData) import Data.Bifunctor (Bifunctor(..)) import Data.Bits (xor) import Data.Data (Data) import Data.Foldable import Data.HashSet (HashSet) import Data.List.NonEmpty (NonEmpty(..)) import Data.String (IsString(..)) import Data.Semigroup (Semigroup(..)) import Data.Sequence (Seq) import Data.Text (Text) import Data.Text.Prettyprint.Doc (Doc, Pretty) import Data.Traversable import Data.Void (Void) import Dhall.Map (Map) import Dhall.Set (Set) import Dhall.Src (Src(..)) import {-# SOURCE #-} Dhall.Pretty.Internal import GHC.Generics (Generic) import Instances.TH.Lift () import Language.Haskell.TH.Syntax (Lift) import Numeric.Natural (Natural) import Prelude hiding (succ) import Unsafe.Coerce (unsafeCoerce) import qualified Control.Monad import qualified Data.HashSet import qualified Data.List.NonEmpty import qualified Data.Text import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Dhall.Crypto import qualified Network.URI as URI {-| Constants for a pure type system The axioms are: > ⊦ Type : Kind > ⊦ Kind : Sort ... and the valid rule pairs are: > ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions) > ⊦ Kind ↝ Type : Type -- Functions from types to terms (type-polymorphic functions) > ⊦ Sort ↝ Type : Type -- Functions from kinds to terms > ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type-level functions) > ⊦ Sort ↝ Kind : Sort -- Functions from kinds to types (kind-polymorphic functions) > ⊦ Sort ↝ Sort : Sort -- Functions from kinds to kinds (kind-level functions) Note that Dhall does not support functions from terms to types and therefore Dhall is not a dependently typed language -} data Const = Type | Kind | Sort deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, NFData) instance Lift Const instance Pretty Const where pretty = Pretty.unAnnotate . prettyConst {-| 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. -} data Var = V Text !Int deriving (Data, Generic, Eq, Ord, Show, NFData) instance Lift Var instance IsString Var where fromString str = V (fromString str) 0 instance Pretty Var where pretty = Pretty.unAnnotate . prettyVar {- | 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 the @A@ comment. * @variable@ is @"x"@ * @bindingSrc1@ corresponds to the @B@ comment. * @annotation@ is 'Just' a pair, corresponding to the @C@ comment and @Bool@. * @bindingSrc2@ corresponds to the @D@ comment. * @value@ corresponds to @True@. -} 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 } deriving (Data, Eq, Foldable, Functor, Generic, NFData, Ord, Show, Traversable) instance Bifunctor Binding where first k (Binding src0 a src1 b src2 c) = Binding (fmap k src0) a (fmap k src1) (fmap adapt0 b) (fmap k src2) (first k c) where adapt0 (src3, d) = (fmap k src3, first k d) second = fmap {-| Construct a 'Binding' with no source information and no type annotation. -} makeBinding :: Text -> Expr s a -> Binding s a makeBinding name = Binding Nothing name Nothing Nothing Nothing -- | This wrapper around 'Prelude.Double' exists for its 'Eq' instance which is -- defined via the binary encoding of Dhall @Double@s. newtype DhallDouble = DhallDouble { getDhallDouble :: Double } deriving (Show, Data, NFData, Generic) -- | This instance satisfies all the customary 'Eq' laws except substitutivity. -- -- In particular: -- -- >>> nan = DhallDouble (0/0) -- >>> nan == nan -- True -- -- This instance is also consistent with with the binary encoding of Dhall @Double@s: -- -- >>> toBytes n = Dhall.Binary.encodeExpression (DoubleLit n :: Expr Void Import) -- -- prop> \a b -> (a == b) == (toBytes a == toBytes b) instance Eq DhallDouble where DhallDouble a == DhallDouble b | isNaN a && isNaN b = True | isNegativeZero a `xor` isNegativeZero b = False | otherwise = a == b -- | This instance relies on the 'Eq' instance for 'DhallDouble' but cannot -- satisfy the customary 'Ord' laws when @NaN@ is involved. instance Ord DhallDouble where compare a@(DhallDouble a') b@(DhallDouble b') = if a == b then EQ else compare a' b' -- | The body of an interpolated @Text@ literal data Chunks s a = Chunks [(Text, Expr s a)] Text deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData) instance (Lift s, Lift a, Data s, Data a) => Lift (Chunks s a) instance Data.Semigroup.Semigroup (Chunks s a) where Chunks xysL zL <> Chunks [] zR = Chunks xysL (zL <> zR) Chunks xysL zL <> Chunks ((x, y):xysR) zR = Chunks (xysL ++ (zL <> x, y):xysR) zR instance Monoid (Chunks s a) where mempty = Chunks [] mempty #if !(MIN_VERSION_base(4,11,0)) mappend = (<>) #endif instance IsString (Chunks s a) where fromString str = Chunks [] (fromString str) {-| Syntax tree for expressions The @s@ type parameter is used to track the presence or absence of `Src` spans: * If @s = `Src`@ then the code may contains `Src` spans (either in a `Noted` constructor or inline within another constructor, like `Let`) * If @s = `Void`@ then the code has no `Src` spans The @a@ type parameter is used to track the presence or absence of imports * If @a = `Import`@ then the code may contain unresolved `Import`s * If @a = `Void`@ then the code has no `Import`s -} data Expr s a -- | > Const c ~ c = Const Const -- | > Var (V x 0) ~ x -- > Var (V x n) ~ x@n | Var Var -- | > Lam x A b ~ λ(x : A) -> b | Lam Text (Expr s a) (Expr s a) -- | > Pi "_" A B ~ A -> B -- > Pi x A B ~ ∀(x : A) -> B | Pi Text (Expr s a) (Expr s a) -- | > App f a ~ f a | App (Expr s a) (Expr s a) -- | > Let (Binding _ x _ Nothing _ r) e ~ let x = r in e -- > Let (Binding _ x _ (Just t ) _ r) e ~ let x : t = r in e -- -- The difference between -- -- > let x = a let y = b in e -- -- and -- -- > let x = a in let y = b in e -- -- is only an additional 'Note' around @'Let' "y" …@ in the second -- example. -- -- See 'MultiLet' for a representation of let-blocks that mirrors the -- source code more closely. | Let (Binding s a) (Expr s a) -- | > Annot x t ~ x : t | Annot (Expr s a) (Expr s a) -- | > Bool ~ Bool | Bool -- | > BoolLit b ~ b | BoolLit Bool -- | > BoolAnd x y ~ x && y | BoolAnd (Expr s a) (Expr s a) -- | > BoolOr x y ~ x || y | BoolOr (Expr s a) (Expr s a) -- | > BoolEQ x y ~ x == y | BoolEQ (Expr s a) (Expr s a) -- | > BoolNE x y ~ x != y | BoolNE (Expr s a) (Expr s a) -- | > BoolIf x y z ~ if x then y else z | BoolIf (Expr s a) (Expr s a) (Expr s a) -- | > Natural ~ Natural | Natural -- | > NaturalLit n ~ n | NaturalLit Natural -- | > NaturalFold ~ Natural/fold | NaturalFold -- | > NaturalBuild ~ Natural/build | NaturalBuild -- | > NaturalIsZero ~ Natural/isZero | NaturalIsZero -- | > NaturalEven ~ Natural/even | NaturalEven -- | > NaturalOdd ~ Natural/odd | NaturalOdd -- | > NaturalToInteger ~ Natural/toInteger | NaturalToInteger -- | > NaturalShow ~ Natural/show | NaturalShow -- | > NaturalSubtract ~ Natural/subtract | NaturalSubtract -- | > NaturalPlus x y ~ x + y | NaturalPlus (Expr s a) (Expr s a) -- | > NaturalTimes x y ~ x * y | NaturalTimes (Expr s a) (Expr s a) -- | > Integer ~ Integer | Integer -- | > IntegerLit n ~ ±n | IntegerLit Integer -- | IntegerClamp ~ Integer/clamp | IntegerClamp -- | IntegerNegate ~ Integer/negate | IntegerNegate -- | > IntegerShow ~ Integer/show | IntegerShow -- | > IntegerToDouble ~ Integer/toDouble | IntegerToDouble -- | > Double ~ Double | Double -- | > DoubleLit n ~ n | DoubleLit DhallDouble -- | > DoubleShow ~ Double/show | DoubleShow -- | > Text ~ Text | Text -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3" | TextLit (Chunks s a) -- | > TextAppend x y ~ x ++ y | TextAppend (Expr s a) (Expr s a) -- | > TextShow ~ Text/show | TextShow -- | > List ~ List | List -- | > ListLit (Just t ) [] ~ [] : t -- > ListLit Nothing [x, y, z] ~ [x, y, z] -- -- Invariant: A non-empty list literal is always represented as -- @ListLit Nothing xs@. -- -- When an annotated, non-empty list literal is parsed, it is represented -- as -- -- > Annot (ListLit Nothing [x, y, z]) t ~ [x, y, z] : t -- Eventually we should have separate constructors for empty and non-empty -- list literals. For now it's easier to check the invariant in @infer@. -- See https://github.com/dhall-lang/dhall-haskell/issues/1359#issuecomment-537087234. | ListLit (Maybe (Expr s a)) (Seq (Expr s a)) -- | > ListAppend x y ~ x # y | ListAppend (Expr s a) (Expr s a) -- | > ListBuild ~ List/build | ListBuild -- | > ListFold ~ List/fold | ListFold -- | > ListLength ~ List/length | ListLength -- | > ListHead ~ List/head | ListHead -- | > ListLast ~ List/last | ListLast -- | > ListIndexed ~ List/indexed | ListIndexed -- | > ListReverse ~ List/reverse | ListReverse -- | > Optional ~ Optional | Optional -- | > Some e ~ Some e | Some (Expr s a) -- | > None ~ None | None -- | > OptionalFold ~ Optional/fold | OptionalFold -- | > OptionalBuild ~ Optional/build | OptionalBuild -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 } | Record (Map Text (Expr s a)) -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 } | RecordLit (Map Text (Expr s a)) -- | > Union [(k1, Just t1), (k2, Nothing)] ~ < k1 : t1 | k2 > | Union (Map Text (Maybe (Expr s a))) -- | > Combine x y ~ x ∧ y | Combine (Expr s a) (Expr s a) -- | > CombineTypes x y ~ x ⩓ y | CombineTypes (Expr s a) (Expr s a) -- | > Prefer x y ~ x ⫽ y | Prefer (Expr s a) (Expr s a) -- | > RecordCompletion x y ~ x::y | RecordCompletion (Expr s a) (Expr s a) -- | > Merge x y (Just t ) ~ merge x y : t -- > Merge x y Nothing ~ merge x y | Merge (Expr s a) (Expr s a) (Maybe (Expr s a)) -- | > ToMap x (Just t) ~ toMap x : t -- > ToMap x Nothing ~ toMap x | ToMap (Expr s a) (Maybe (Expr s a)) -- | > Field e x ~ e.x | Field (Expr s a) Text -- | > Project e (Left xs) ~ e.{ xs } -- | > Project e (Right t) ~ e.(t) | Project (Expr s a) (Either (Set Text) (Expr s a)) -- | > Assert e ~ assert : e | Assert (Expr s a) -- | > Equivalent x y ~ x ≡ y | Equivalent (Expr s a) (Expr s a) -- | > Note s x ~ e | Note s (Expr s a) -- | > ImportAlt ~ e1 ? e2 | ImportAlt (Expr s a) (Expr s a) -- | > Embed import ~ import | Embed a deriving (Foldable, Generic, Traversable, Show, Data, NFData) -- NB: If you add a constructor to Expr, please also update the Arbitrary -- instance in Dhall.Test.QuickCheck. -- | This instance encodes what the Dhall standard calls an \"exact match\" -- between two expressions. -- -- Note that -- -- >>> nan = DhallDouble (0/0) -- >>> DoubleLit nan == DoubleLit nan -- True deriving instance (Eq s, Eq a) => Eq (Expr s a) -- | Note that this 'Ord' instance inherits `DhallDouble`'s defects. deriving instance (Ord s, Ord a) => Ord (Expr s a) instance (Lift s, Lift a, Data s, Data a) => Lift (Expr s a) -- This instance is hand-written due to the fact that deriving -- it does not give us an INLINABLE pragma. We annotate this fmap -- implementation with this pragma below to allow GHC to, possibly, -- inline the implementation for performance improvements. instance Functor (Expr s) where fmap _ (Const c) = Const c fmap _ (Var v) = Var v fmap f (Lam v e1 e2) = Lam v (fmap f e1) (fmap f e2) fmap f (Pi v e1 e2) = Pi v (fmap f e1) (fmap f e2) fmap f (App e1 e2) = App (fmap f e1) (fmap f e2) fmap f (Let b e2) = Let (fmap f b) (fmap f e2) fmap f (Annot e1 e2) = Annot (fmap f e1) (fmap f e2) fmap _ Bool = Bool fmap _ (BoolLit b) = BoolLit b fmap f (BoolAnd e1 e2) = BoolAnd (fmap f e1) (fmap f e2) fmap f (BoolOr e1 e2) = BoolOr (fmap f e1) (fmap f e2) fmap f (BoolEQ e1 e2) = BoolEQ (fmap f e1) (fmap f e2) fmap f (BoolNE e1 e2) = BoolNE (fmap f e1) (fmap f e2) fmap f (BoolIf e1 e2 e3) = BoolIf (fmap f e1) (fmap f e2) (fmap f e3) fmap _ Natural = Natural fmap _ (NaturalLit n) = NaturalLit n fmap _ NaturalFold = NaturalFold fmap _ NaturalBuild = NaturalBuild fmap _ NaturalIsZero = NaturalIsZero fmap _ NaturalEven = NaturalEven fmap _ NaturalOdd = NaturalOdd fmap _ NaturalToInteger = NaturalToInteger fmap _ NaturalShow = NaturalShow fmap _ NaturalSubtract = NaturalSubtract fmap f (NaturalPlus e1 e2) = NaturalPlus (fmap f e1) (fmap f e2) fmap f (NaturalTimes e1 e2) = NaturalTimes (fmap f e1) (fmap f e2) fmap _ Integer = Integer fmap _ (IntegerLit i) = IntegerLit i fmap _ IntegerClamp = IntegerClamp fmap _ IntegerNegate = IntegerNegate fmap _ IntegerShow = IntegerShow fmap _ IntegerToDouble = IntegerToDouble fmap _ Double = Double fmap _ (DoubleLit d) = DoubleLit d fmap _ DoubleShow = DoubleShow fmap _ Text = Text fmap f (TextLit cs) = TextLit (fmap f cs) fmap f (TextAppend e1 e2) = TextAppend (fmap f e1) (fmap f e2) fmap _ TextShow = TextShow fmap _ List = List fmap f (ListLit maybeE seqE) = ListLit (fmap (fmap f) maybeE) (fmap (fmap f) seqE) fmap f (ListAppend e1 e2) = ListAppend (fmap f e1) (fmap f e2) fmap _ ListBuild = ListBuild fmap _ ListFold = ListFold fmap _ ListLength = ListLength fmap _ ListHead = ListHead fmap _ ListLast = ListLast fmap _ ListIndexed = ListIndexed fmap _ ListReverse = ListReverse fmap _ Optional = Optional fmap f (Some e) = Some (fmap f e) fmap _ None = None fmap _ OptionalFold = OptionalFold fmap _ OptionalBuild = OptionalBuild fmap f (Record r) = Record (fmap (fmap f) r) fmap f (RecordLit r) = RecordLit (fmap (fmap f) r) fmap f (Union u) = Union (fmap (fmap (fmap f)) u) fmap f (Combine e1 e2) = Combine (fmap f e1) (fmap f e2) fmap f (CombineTypes e1 e2) = CombineTypes (fmap f e1) (fmap f e2) fmap f (Prefer e1 e2) = Prefer (fmap f e1) (fmap f e2) fmap f (RecordCompletion e1 e2) = RecordCompletion (fmap f e1) (fmap f e2) fmap f (Merge e1 e2 maybeE) = Merge (fmap f e1) (fmap f e2) (fmap (fmap f) maybeE) fmap f (ToMap e maybeE) = ToMap (fmap f e) (fmap (fmap f) maybeE) fmap f (Field e1 v) = Field (fmap f e1) v fmap f (Project e1 vs) = Project (fmap f e1) (fmap (fmap f) vs) fmap f (Assert t) = Assert (fmap f t) fmap f (Equivalent e1 e2) = Equivalent (fmap f e1) (fmap f e2) fmap f (Note s e1) = Note s (fmap f e1) fmap f (ImportAlt e1 e2) = ImportAlt (fmap f e1) (fmap f e2) fmap f (Embed a) = Embed (f a) {-# INLINABLE fmap #-} instance Applicative (Expr s) where pure = Embed (<*>) = Control.Monad.ap instance Monad (Expr s) where return = pure Const a >>= _ = Const a Var a >>= _ = Var a Lam a b c >>= k = Lam a (b >>= k) (c >>= k) Pi a b c >>= k = Pi a (b >>= k) (c >>= k) App a b >>= k = App (a >>= k) (b >>= k) Let a b >>= k = Let (adapt0 a) (b >>= k) where adapt0 (Binding src0 c src1 d src2 e) = Binding src0 c src1 (fmap adapt1 d) src2 (e >>= k) adapt1 (src3, f) = (src3, f >>= k) Annot a b >>= k = Annot (a >>= k) (b >>= k) Bool >>= _ = Bool BoolLit a >>= _ = BoolLit a BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k) BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k) BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k) BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k) BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k) Natural >>= _ = Natural NaturalLit a >>= _ = NaturalLit a NaturalFold >>= _ = NaturalFold NaturalBuild >>= _ = NaturalBuild NaturalIsZero >>= _ = NaturalIsZero NaturalEven >>= _ = NaturalEven NaturalOdd >>= _ = NaturalOdd NaturalToInteger >>= _ = NaturalToInteger NaturalShow >>= _ = NaturalShow NaturalSubtract >>= _ = NaturalSubtract NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k) NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k) Integer >>= _ = Integer IntegerLit a >>= _ = IntegerLit a IntegerClamp >>= _ = IntegerClamp IntegerNegate >>= _ = IntegerNegate IntegerShow >>= _ = IntegerShow IntegerToDouble >>= _ = IntegerToDouble Double >>= _ = Double DoubleLit a >>= _ = DoubleLit a DoubleShow >>= _ = DoubleShow Text >>= _ = Text TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b) TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k) TextShow >>= _ = TextShow List >>= _ = List ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b) ListAppend a b >>= k = ListAppend (a >>= k) (b >>= k) ListBuild >>= _ = ListBuild ListFold >>= _ = ListFold ListLength >>= _ = ListLength ListHead >>= _ = ListHead ListLast >>= _ = ListLast ListIndexed >>= _ = ListIndexed ListReverse >>= _ = ListReverse Optional >>= _ = Optional Some a >>= k = Some (a >>= k) None >>= _ = None OptionalFold >>= _ = OptionalFold OptionalBuild >>= _ = OptionalBuild Record a >>= k = Record (fmap (>>= k) a) RecordLit a >>= k = RecordLit (fmap (>>= k) a) Union a >>= k = Union (fmap (fmap (>>= k)) a) Combine a b >>= k = Combine (a >>= k) (b >>= k) CombineTypes a b >>= k = CombineTypes (a >>= k) (b >>= k) Prefer a b >>= k = Prefer (a >>= k) (b >>= k) RecordCompletion a b >>= k = RecordCompletion (a >>= k) (b >>= k) Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c) ToMap a b >>= k = ToMap (a >>= k) (fmap (>>= k) b) Field a b >>= k = Field (a >>= k) b Project a b >>= k = Project (a >>= k) (fmap (>>= k) b) Assert a >>= k = Assert (a >>= k) Equivalent a b >>= k = Equivalent (a >>= k) (b >>= k) Note a b >>= k = Note a (b >>= k) ImportAlt a b >>= k = ImportAlt (a >>= k) (b >>= k) Embed a >>= k = k a instance Bifunctor Expr where first _ (Const a ) = Const a first _ (Var a ) = Var a first k (Lam a b c ) = Lam a (first k b) (first k c) first k (Pi a b c ) = Pi a (first k b) (first k c) first k (App a b ) = App (first k a) (first k b) first k (Let a b ) = Let (first k a) (first k b) first k (Annot a b ) = Annot (first k a) (first k b) first _ Bool = Bool first _ (BoolLit a ) = BoolLit a first k (BoolAnd a b ) = BoolAnd (first k a) (first k b) first k (BoolOr a b ) = BoolOr (first k a) (first k b) first k (BoolEQ a b ) = BoolEQ (first k a) (first k b) first k (BoolNE a b ) = BoolNE (first k a) (first k b) first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c) first _ Natural = Natural first _ (NaturalLit a ) = NaturalLit a first _ NaturalFold = NaturalFold first _ NaturalBuild = NaturalBuild first _ NaturalIsZero = NaturalIsZero first _ NaturalEven = NaturalEven first _ NaturalOdd = NaturalOdd first _ NaturalToInteger = NaturalToInteger first _ NaturalShow = NaturalShow first _ NaturalSubtract = NaturalSubtract first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b) first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b) first _ Integer = Integer first _ (IntegerLit a ) = IntegerLit a first _ IntegerClamp = IntegerClamp first _ IntegerNegate = IntegerNegate first _ IntegerShow = IntegerShow first _ IntegerToDouble = IntegerToDouble first _ Double = Double first _ (DoubleLit a ) = DoubleLit a first _ DoubleShow = DoubleShow first _ Text = Text first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b) first k (TextAppend a b ) = TextAppend (first k a) (first k b) first _ TextShow = TextShow first _ List = List first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b) first k (ListAppend a b ) = ListAppend (first k a) (first k b) first _ ListBuild = ListBuild first _ ListFold = ListFold first _ ListLength = ListLength first _ ListHead = ListHead first _ ListLast = ListLast first _ ListIndexed = ListIndexed first _ ListReverse = ListReverse first _ Optional = Optional first k (Some a ) = Some (first k a) first _ None = None first _ OptionalFold = OptionalFold first _ OptionalBuild = OptionalBuild first k (Record a ) = Record (fmap (first k) a) first k (RecordLit a ) = RecordLit (fmap (first k) a) first k (Union a ) = Union (fmap (fmap (first k)) a) first k (Combine a b ) = Combine (first k a) (first k b) first k (CombineTypes a b ) = CombineTypes (first k a) (first k b) first k (Prefer a b ) = Prefer (first k a) (first k b) first k (RecordCompletion a b) = RecordCompletion (first k a) (first k b) first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c) first k (ToMap a b ) = ToMap (first k a) (fmap (first k) b) first k (Field a b ) = Field (first k a) b first k (Assert a ) = Assert (first k a) first k (Equivalent a b ) = Equivalent (first k a) (first k b) first k (Project a b ) = Project (first k a) (fmap (first k) b) first k (Note a b ) = Note (k a) (first k b) first k (ImportAlt a b ) = ImportAlt (first k a) (first k b) first _ (Embed a ) = Embed a second = fmap instance IsString (Expr s a) where fromString str = Var (fromString str) -- | Generates a syntactically valid Dhall program instance Pretty a => Pretty (Expr s a) where pretty = Pretty.unAnnotate . prettyExpr {- Instead of converting explicitly between 'Expr's and 'MultiLet', it might be nicer to use a pattern synonym: > pattern MultiLet' :: NonEmpty (Binding s a) -> Expr s a -> Expr s a > pattern MultiLet' as b <- (multiLetFromExpr -> Just (MultiLet as b)) where > MultiLet' as b = wrapInLets as b > > multiLetFromExpr :: Expr s a -> Maybe (MultiLet s a) > multiLetFromExpr = \case > Let x mA a b -> Just (multiLet x mA a b) > _ -> Nothing This works in principle, but GHC as of v8.8.1 doesn't handle it well: https://gitlab.haskell.org/ghc/ghc/issues/17096 This should be fixed by GHC-8.10, so it might be worth revisiting then. -} {-| Generate a 'MultiLet' from the contents of a 'Let'. In the resulting @'MultiLet' bs e@, @e@ is guaranteed not to be a 'Let', but it might be a @('Note' … ('Let' …))@. Given parser output, 'multiLet' consolidates @let@s that formed a let-block in the original source. -} multiLet :: Binding s a -> Expr s a -> MultiLet s a multiLet b0 = \case Let b1 e1 -> let MultiLet bs e = multiLet b1 e1 in MultiLet (Data.List.NonEmpty.cons b0 bs) e e -> MultiLet (b0 :| []) e {-| 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 -} wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a wrapInLets bs e = foldr Let e bs {-| This type represents 1 or more nested `Let` bindings that have been coalesced together for ease of manipulation -} data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a) -- | A traversal over the immediate sub-expressions of an expression. subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a) subExpressions _ (Const c) = pure (Const c) subExpressions _ (Var v) = pure (Var v) subExpressions f (Lam a b c) = Lam a <$> f b <*> f c subExpressions f (Pi a b c) = Pi a <$> f b <*> f c subExpressions f (App a b) = App <$> f a <*> f b subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b subExpressions f (Annot a b) = Annot <$> f a <*> f b subExpressions _ Bool = pure Bool subExpressions _ (BoolLit b) = pure (BoolLit b) subExpressions f (BoolAnd a b) = BoolAnd <$> f a <*> f b subExpressions f (BoolOr a b) = BoolOr <$> f a <*> f b subExpressions f (BoolEQ a b) = BoolEQ <$> f a <*> f b subExpressions f (BoolNE a b) = BoolNE <$> f a <*> f b subExpressions f (BoolIf a b c) = BoolIf <$> f a <*> f b <*> f c subExpressions _ Natural = pure Natural subExpressions _ (NaturalLit n) = pure (NaturalLit n) subExpressions _ NaturalFold = pure NaturalFold subExpressions _ NaturalBuild = pure NaturalBuild subExpressions _ NaturalIsZero = pure NaturalIsZero subExpressions _ NaturalEven = pure NaturalEven subExpressions _ NaturalOdd = pure NaturalOdd subExpressions _ NaturalToInteger = pure NaturalToInteger subExpressions _ NaturalShow = pure NaturalShow subExpressions _ NaturalSubtract = pure NaturalSubtract subExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b subExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b subExpressions _ Integer = pure Integer subExpressions _ (IntegerLit n) = pure (IntegerLit n) subExpressions _ IntegerClamp = pure IntegerClamp subExpressions _ IntegerNegate = pure IntegerNegate subExpressions _ IntegerShow = pure IntegerShow subExpressions _ IntegerToDouble = pure IntegerToDouble subExpressions _ Double = pure Double subExpressions _ (DoubleLit n) = pure (DoubleLit n) subExpressions _ DoubleShow = pure DoubleShow subExpressions _ Text = pure Text subExpressions f (TextLit chunks) = TextLit <$> chunkExprs f chunks subExpressions f (TextAppend a b) = TextAppend <$> f a <*> f b subExpressions _ TextShow = pure TextShow subExpressions _ List = pure List subExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b subExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b subExpressions _ ListBuild = pure ListBuild subExpressions _ ListFold = pure ListFold subExpressions _ ListLength = pure ListLength subExpressions _ ListHead = pure ListHead subExpressions _ ListLast = pure ListLast subExpressions _ ListIndexed = pure ListIndexed subExpressions _ ListReverse = pure ListReverse subExpressions _ Optional = pure Optional subExpressions f (Some a) = Some <$> f a subExpressions _ None = pure None subExpressions _ OptionalFold = pure OptionalFold subExpressions _ OptionalBuild = pure OptionalBuild subExpressions f (Record a) = Record <$> traverse f a subExpressions f ( RecordLit a ) = RecordLit <$> traverse f a subExpressions f (Union a) = Union <$> traverse (traverse f) a subExpressions f (Combine a b) = Combine <$> f a <*> f b subExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b subExpressions f (Prefer a b) = Prefer <$> f a <*> f b subExpressions f (RecordCompletion a b) = RecordCompletion <$> f a <*> f b subExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t subExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t subExpressions f (Field a b) = Field <$> f a <*> pure b subExpressions f (Project a b) = Project <$> f a <*> traverse f b subExpressions f (Assert a) = Assert <$> f a subExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b subExpressions f (Note a b) = Note a <$> f b subExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r subExpressions _ (Embed a) = pure (Embed a) {-| Traverse over the immediate 'Expr' children in a 'Binding'. -} bindingExprs :: (Applicative f) => (Expr s a -> f (Expr s b)) -> Binding s a -> f (Binding s b) bindingExprs f (Binding s0 n s1 t s2 v) = Binding <$> pure s0 <*> pure n <*> pure s1 <*> traverse (traverse f) t <*> pure s2 <*> f v -- | A traversal over the immediate sub-expressions in 'Chunks'. chunkExprs :: Applicative f => (Expr s a -> f (Expr t b)) -> Chunks s a -> f (Chunks t b) chunkExprs f (Chunks chunks final) = flip Chunks final <$> traverse (traverse f) chunks {-| Internal representation of a directory that stores the path components in reverse order In other words, the directory @\/foo\/bar\/baz@ is encoded as @Directory { components = [ "baz", "bar", "foo" ] }@ -} newtype Directory = Directory { components :: [Text] } deriving (Eq, Generic, Ord, Show, NFData) instance Semigroup Directory where Directory components₀ <> Directory components₁ = Directory (components₁ <> components₀) instance Pretty Directory where pretty (Directory {..}) = foldMap prettyPathComponent (reverse components) prettyPathComponent :: Text -> Doc ann prettyPathComponent text | Data.Text.all pathCharacter text = "/" <> Pretty.pretty text | otherwise = "/\"" <> Pretty.pretty text <> "\"" {-| A `File` is a `directory` followed by one additional path component representing the `file` name -} data File = File { directory :: Directory , file :: Text } deriving (Eq, Generic, Ord, Show, NFData) instance Pretty File where pretty (File {..}) = Pretty.pretty directory <> prettyPathComponent file instance Semigroup File where File directory₀ _ <> File directory₁ file = File (directory₀ <> directory₁) file -- | The beginning of a file path which anchors subsequent path components data FilePrefix = Absolute -- ^ Absolute path | Here -- ^ Path relative to @.@ | Parent -- ^ Path relative to @..@ | Home -- ^ Path relative to @~@ deriving (Eq, Generic, Ord, Show, NFData) instance Pretty FilePrefix where pretty Absolute = "" pretty Here = "." pretty Parent = ".." pretty Home = "~" -- | The URI scheme data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData) -- | This type stores all of the components of a remote import data URL = URL { scheme :: Scheme , authority :: Text , path :: File , query :: Maybe Text , headers :: Maybe (Expr Src Import) } deriving (Eq, Generic, Ord, Show, NFData) instance Pretty URL where pretty (URL {..}) = schemeDoc <> "://" <> Pretty.pretty authority <> pathDoc <> queryDoc <> foldMap prettyHeaders headers where prettyHeaders h = " using " <> Pretty.pretty h File {..} = path Directory {..} = directory pathDoc = foldMap prettyURIComponent (reverse components) <> prettyURIComponent file schemeDoc = case scheme of HTTP -> "http" HTTPS -> "https" queryDoc = case query of Nothing -> "" Just q -> "?" <> Pretty.pretty q prettyURIComponent :: Text -> Doc ann prettyURIComponent text = Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text -- | The type of import (i.e. local vs. remote vs. environment) data ImportType = Local FilePrefix File -- ^ Local path | Remote URL -- ^ URL of remote resource and optional headers stored in an import | Env Text -- ^ Environment variable | Missing deriving (Eq, Generic, Ord, Show, NFData) parent :: File parent = File { directory = Directory { components = [ ".." ] }, file = "" } instance Semigroup ImportType where Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁) Remote (URL { path = path₀, ..}) <> Local Here path₁ = Remote (URL { path = path₀ <> path₁, ..}) Local prefix file₀ <> Local Parent file₁ = Local prefix (file₀ <> parent <> file₁) Remote (URL { path = path₀, .. }) <> Local Parent path₁ = Remote (URL { path = path₀ <> parent <> path₁, .. }) import₀ <> Remote (URL { headers = headers₀, .. }) = Remote (URL { headers = headers₁, .. }) where importHashed₀ = Import (ImportHashed Nothing import₀) Code headers₁ = fmap (fmap (importHashed₀ <>)) headers₀ _ <> import₁ = import₁ instance Pretty ImportType where pretty (Local prefix file) = Pretty.pretty prefix <> Pretty.pretty file pretty (Remote url) = Pretty.pretty url pretty (Env env) = "env:" <> prettyEnvironmentVariable env pretty Missing = "missing" -- | How to interpret the import's contents (i.e. as Dhall code or raw text) data ImportMode = Code | RawText | Location deriving (Eq, Generic, Ord, Show, NFData) -- | A `ImportType` extended with an optional hash for semantic integrity checks data ImportHashed = ImportHashed { hash :: Maybe Dhall.Crypto.SHA256Digest , importType :: ImportType } deriving (Eq, Generic, Ord, Show, NFData) instance Semigroup ImportHashed where ImportHashed _ importType₀ <> ImportHashed hash importType₁ = ImportHashed hash (importType₀ <> importType₁) instance Pretty ImportHashed where pretty (ImportHashed Nothing p) = Pretty.pretty p pretty (ImportHashed (Just h) p) = Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h) -- | Reference to an external resource data Import = Import { importHashed :: ImportHashed , importMode :: ImportMode } deriving (Eq, Generic, Ord, Show, NFData) instance Semigroup Import where Import importHashed₀ _ <> Import importHashed₁ code = Import (importHashed₀ <> importHashed₁) code instance Pretty Import where pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix where suffix :: Text suffix = case importMode of RawText -> " as Text" Location -> " as Location" Code -> "" {-| Returns `True` if the given `Char` is valid within an unquoted path component This is exported for reuse within the @"Dhall.Parser.Token"@ module -} pathCharacter :: Char -> Bool pathCharacter c = '\x21' == c || ('\x24' <= c && c <= '\x27') || ('\x2A' <= c && c <= '\x2B') || ('\x2D' <= c && c <= '\x2E') || ('\x30' <= c && c <= '\x3B') || c == '\x3D' || ('\x40' <= c && c <= '\x5A') || ('\x5E' <= c && c <= '\x7A') || c == '\x7C' || c == '\x7E' -- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`) denote :: Expr s a -> Expr t a denote (Note _ b ) = denote b denote (Const a ) = Const a denote (Var a ) = Var a denote (Lam a b c ) = Lam a (denote b) (denote c) denote (Pi a b c ) = Pi a (denote b) (denote c) denote (App a b ) = App (denote a) (denote b) denote (Let a b ) = Let (adapt0 a) (denote b) where adapt0 (Binding _ c _ d _ e) = Binding Nothing c Nothing (fmap adapt1 d) Nothing (denote e) adapt1 (_, f) = (Nothing, denote f) denote (Annot a b ) = Annot (denote a) (denote b) denote Bool = Bool denote (BoolLit a ) = BoolLit a denote (BoolAnd a b ) = BoolAnd (denote a) (denote b) denote (BoolOr a b ) = BoolOr (denote a) (denote b) denote (BoolEQ a b ) = BoolEQ (denote a) (denote b) denote (BoolNE a b ) = BoolNE (denote a) (denote b) denote (BoolIf a b c ) = BoolIf (denote a) (denote b) (denote c) denote Natural = Natural denote (NaturalLit a ) = NaturalLit a denote NaturalFold = NaturalFold denote NaturalBuild = NaturalBuild denote NaturalIsZero = NaturalIsZero denote NaturalEven = NaturalEven denote NaturalOdd = NaturalOdd denote NaturalToInteger = NaturalToInteger denote NaturalShow = NaturalShow denote NaturalSubtract = NaturalSubtract denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b) denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b) denote Integer = Integer denote (IntegerLit a ) = IntegerLit a denote IntegerClamp = IntegerClamp denote IntegerNegate = IntegerNegate denote IntegerShow = IntegerShow denote IntegerToDouble = IntegerToDouble denote Double = Double denote (DoubleLit a ) = DoubleLit a denote DoubleShow = DoubleShow denote Text = Text denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b) denote (TextAppend a b ) = TextAppend (denote a) (denote b) denote TextShow = TextShow denote List = List denote (ListLit a b ) = ListLit (fmap denote a) (fmap denote b) denote (ListAppend a b ) = ListAppend (denote a) (denote b) denote ListBuild = ListBuild denote ListFold = ListFold denote ListLength = ListLength denote ListHead = ListHead denote ListLast = ListLast denote ListIndexed = ListIndexed denote ListReverse = ListReverse denote Optional = Optional denote (Some a ) = Some (denote a) denote None = None denote OptionalFold = OptionalFold denote OptionalBuild = OptionalBuild denote (Record a ) = Record (fmap denote a) denote (RecordLit a ) = RecordLit (fmap denote a) denote (Union a ) = Union (fmap (fmap denote) a) denote (Combine a b ) = Combine (denote a) (denote b) denote (CombineTypes a b ) = CombineTypes (denote a) (denote b) denote (Prefer a b ) = Prefer (denote a) (denote b) denote (RecordCompletion a b) = RecordCompletion (denote a) (denote b) denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c) denote (ToMap a b ) = ToMap (denote a) (fmap denote b) denote (Field a b ) = Field (denote a) b denote (Project a b ) = Project (denote a) (fmap denote b) denote (Assert a ) = Assert (denote a) denote (Equivalent a b ) = Equivalent (denote a) (denote b) denote (ImportAlt a b ) = ImportAlt (denote a) (denote b) denote (Embed a ) = Embed a -- | The \"opposite\" of `denote`, like @first absurd@ but faster renote :: Expr Void a -> Expr s a renote = unsafeCoerce {-# INLINE renote #-} {-| Remove any outermost `Note` constructors This is typically used when you want to get the outermost non-`Note` constructor without removing internal `Note` constructors -} shallowDenote :: Expr s a -> Expr s a shallowDenote (Note _ e) = shallowDenote e shallowDenote e = e -- | The set of reserved identifiers for the Dhall language reservedIdentifiers :: HashSet Text reservedIdentifiers = Data.HashSet.fromList [ -- Keywords according to the `keyword` rule in the grammar "if" , "then" , "else" , "let" , "in" , "using" , "missing" , "as" , "Infinity" , "NaN" , "merge" , "Some" , "toMap" , "assert" , "forall" -- Builtins according to the `builtin` rule in the grammar , "Natural/fold" , "Natural/build" , "Natural/isZero" , "Natural/even" , "Natural/odd" , "Natural/toInteger" , "Natural/show" , "Natural/subtract" , "Integer" , "Integer/clamp" , "Integer/negate" , "Integer/show" , "Integer/toDouble" , "Integer/show" , "Natural/subtract" , "Double/show" , "List/build" , "List/fold" , "List/length" , "List/head" , "List/last" , "List/indexed" , "List/reverse" , "Optional/fold" , "Optional/build" , "Text/show" , "Bool" , "True" , "False" , "Optional" , "None" , "Natural" , "Integer" , "Double" , "Text" , "List" , "Type" , "Kind" , "Sort" ]