1{-# LANGUAGE DeriveAnyClass #-} 2{-# LANGUAGE DeriveDataTypeable #-} 3{-# LANGUAGE DeriveGeneric #-} 4{-# LANGUAGE DeriveLift #-} 5{-# LANGUAGE DeriveTraversable #-} 6{-# LANGUAGE DerivingStrategies #-} 7{-# LANGUAGE GeneralizedNewtypeDeriving #-} 8{-# LANGUAGE LambdaCase #-} 9{-# LANGUAGE OverloadedLists #-} 10{-# LANGUAGE OverloadedStrings #-} 11{-# LANGUAGE RankNTypes #-} 12{-# LANGUAGE RecordWildCards #-} 13{-# LANGUAGE StandaloneDeriving #-} 14{-# LANGUAGE UnicodeSyntax #-} 15 16{-| This module contains the core syntax types and optics for them. 17 18'reservedIdentifiers', 'denote' and friends are included because they are 19involved in a dependency circle with "Dhall.Pretty.Internal". 20-} 21 22module Dhall.Syntax ( 23 -- * 'Expr' 24 Const(..) 25 , Var(..) 26 , Binding(..) 27 , makeBinding 28 , CharacterSet(..) 29 , Chunks(..) 30 , DhallDouble(..) 31 , PreferAnnotation(..) 32 , Expr(..) 33 , RecordField(..) 34 , makeRecordField 35 , FunctionBinding(..) 36 , makeFunctionBinding 37 , FieldSelection(..) 38 , makeFieldSelection 39 40 -- ** 'Let'-blocks 41 , MultiLet(..) 42 , multiLet 43 , wrapInLets 44 45 -- ** Optics 46 , subExpressions 47 , unsafeSubExpressions 48 , chunkExprs 49 , bindingExprs 50 , recordFieldExprs 51 , functionBindingExprs 52 53 -- ** Handling 'Note's 54 , denote 55 , renote 56 , shallowDenote 57 58 -- * 'Import' 59 , Directory(..) 60 , File(..) 61 , FilePrefix(..) 62 , Import(..) 63 , ImportHashed(..) 64 , ImportMode(..) 65 , ImportType(..) 66 , URL(..) 67 , Scheme(..) 68 , pathCharacter 69 70 -- * Reserved identifiers 71 , reservedIdentifiers 72 , reservedKeywords 73 74 -- * `Data.Text.Text` manipulation 75 , toDoubleQuoted 76 , longestSharedWhitespacePrefix 77 , linesLiteral 78 , unlinesLiteral 79 80 -- * Desugaring 81 , desugarWith 82 83 -- * Utilities 84 , internalError 85 -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a 86 -- module cycle 87 , shift 88 ) where 89 90import Control.DeepSeq (NFData) 91import Data.Bifunctor (Bifunctor (..)) 92import Data.Bits (xor) 93import Data.Data (Data) 94import Data.Foldable 95import Data.HashSet (HashSet) 96import Data.List.NonEmpty (NonEmpty (..)) 97import Data.Sequence (Seq) 98import Data.String (IsString (..)) 99import Data.Text (Text) 100import Data.Text.Prettyprint.Doc (Doc, Pretty) 101import Data.Traversable () 102import Data.Void (Void) 103import Dhall.Map (Map) 104import {-# SOURCE #-} Dhall.Pretty.Internal 105import Dhall.Src (Src (..)) 106import GHC.Generics (Generic) 107import Instances.TH.Lift () 108import Language.Haskell.TH.Syntax (Lift) 109import Numeric.Natural (Natural) 110import Unsafe.Coerce (unsafeCoerce) 111 112import qualified Control.Monad 113import qualified Data.HashSet 114import qualified Data.List.NonEmpty as NonEmpty 115import qualified Data.Text 116import qualified Data.Text.Prettyprint.Doc as Pretty 117import qualified Dhall.Crypto 118import qualified Dhall.Optics as Optics 119import qualified Lens.Family as Lens 120import qualified Network.URI as URI 121 122-- $setup 123-- >>> import Dhall.Binary () -- For the orphan instance for `Serialise (Expr Void Import)` 124 125{-| Constants for a pure type system 126 127 The axioms are: 128 129> ⊦ Type : Kind 130> ⊦ Kind : Sort 131 132 ... and the valid rule pairs are: 133 134> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions) 135> ⊦ Kind ↝ Type : Type -- Functions from types to terms (type-polymorphic functions) 136> ⊦ Sort ↝ Type : Type -- Functions from kinds to terms 137> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type-level functions) 138> ⊦ Sort ↝ Kind : Sort -- Functions from kinds to types (kind-polymorphic functions) 139> ⊦ Sort ↝ Sort : Sort -- Functions from kinds to kinds (kind-level functions) 140 141 Note that Dhall does not support functions from terms to types and therefore 142 Dhall is not a dependently typed language 143-} 144data Const = Type | Kind | Sort 145 deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, Lift, NFData) 146 147instance Pretty Const where 148 pretty = Pretty.unAnnotate . prettyConst 149 150{-| Label for a bound variable 151 152 The `Data.Text.Text` field is the variable's name (i.e. \"@x@\"). 153 154 The `Int` field disambiguates variables with the same name if there are 155 multiple bound variables of the same name in scope. Zero refers to the 156 nearest bound variable and the index increases by one for each bound 157 variable of the same name going outward. The following diagram may help: 158 159> ┌──refers to──┐ 160> │ │ 161> v │ 162> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0 163> 164> ┌─────────────────refers to─────────────────┐ 165> │ │ 166> v │ 167> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1 168 169 This `Int` behaves like a De Bruijn index in the special case where all 170 variables have the same name. 171 172 You can optionally omit the index if it is @0@: 173 174> ┌─refers to─┐ 175> │ │ 176> v │ 177> λ(x : Type) → λ(y : Type) → λ(x : Type) → x 178 179 Zero indices are omitted when pretty-printing @Var@s and non-zero indices 180 appear as a numeric suffix. 181-} 182data Var = V Text !Int 183 deriving (Data, Generic, Eq, Ord, Show, Lift, NFData) 184 185instance IsString Var where 186 fromString str = V (fromString str) 0 187 188instance Pretty Var where 189 pretty = Pretty.unAnnotate . prettyVar 190 191-- | Record the binding part of a @let@ expression. 192-- 193-- For example, 194-- 195-- > let {- A -} x {- B -} : {- C -} Bool = {- D -} True in x 196-- 197-- … will be instantiated as follows: 198-- 199-- * @bindingSrc0@ corresponds to the @A@ comment. 200-- * @variable@ is @"x"@ 201-- * @bindingSrc1@ corresponds to the @B@ comment. 202-- * @annotation@ is 'Just' a pair, corresponding to the @C@ comment and @Bool@. 203-- * @bindingSrc2@ corresponds to the @D@ comment. 204-- * @value@ corresponds to @True@. 205data Binding s a = Binding 206 { bindingSrc0 :: Maybe s 207 , variable :: Text 208 , bindingSrc1 :: Maybe s 209 , annotation :: Maybe (Maybe s, Expr s a) 210 , bindingSrc2 :: Maybe s 211 , value :: Expr s a 212 } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) 213 214instance Bifunctor Binding where 215 first k (Binding src0 a src1 b src2 c) = 216 Binding (fmap k src0) a (fmap k src1) (fmap adapt0 b) (fmap k src2) (first k c) 217 where 218 adapt0 (src3, d) = (fmap k src3, first k d) 219 220 second = fmap 221 222{-| Construct a 'Binding' with no source information and no type annotation. 223-} 224makeBinding :: Text -> Expr s a -> Binding s a 225makeBinding name = Binding Nothing name Nothing Nothing Nothing 226 227-- | This wrapper around 'Prelude.Double' exists for its 'Eq' instance which is 228-- defined via the binary encoding of Dhall @Double@s. 229newtype DhallDouble = DhallDouble { getDhallDouble :: Double } 230 deriving stock (Show, Data, Lift, Generic) 231 deriving anyclass NFData 232 233-- | This instance satisfies all the customary 'Eq' laws except substitutivity. 234-- 235-- In particular: 236-- 237-- >>> nan = DhallDouble (0/0) 238-- >>> nan == nan 239-- True 240-- 241-- This instance is also consistent with with the binary encoding of Dhall @Double@s: 242-- 243-- >>> toBytes n = Dhall.Binary.encodeExpression (DoubleLit n :: Expr Void Import) 244-- 245-- prop> \a b -> (a == b) == (toBytes a == toBytes b) 246instance Eq DhallDouble where 247 DhallDouble a == DhallDouble b 248 | isNaN a && isNaN b = True 249 | isNegativeZero a `xor` isNegativeZero b = False 250 | otherwise = a == b 251 252-- | This instance relies on the 'Eq' instance for 'DhallDouble' but cannot 253-- satisfy the customary 'Ord' laws when @NaN@ is involved. 254instance Ord DhallDouble where 255 compare a@(DhallDouble a') b@(DhallDouble b') = 256 if a == b 257 then EQ 258 else compare a' b' 259 260-- | The body of an interpolated @Text@ literal 261data Chunks s a = Chunks [(Text, Expr s a)] Text 262 deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, Lift, NFData) 263 264instance Semigroup (Chunks s a) where 265 Chunks xysL zL <> Chunks [] zR = 266 Chunks xysL (zL <> zR) 267 Chunks xysL zL <> Chunks ((x, y):xysR) zR = 268 Chunks (xysL ++ (zL <> x, y):xysR) zR 269 270instance Monoid (Chunks s a) where 271 mempty = Chunks [] mempty 272 273instance IsString (Chunks s a) where 274 fromString str = Chunks [] (fromString str) 275 276-- | Used to record the origin of a @//@ operator (i.e. from source code or a 277-- product of desugaring) 278data PreferAnnotation s a 279 = PreferFromSource 280 | PreferFromWith (Expr s a) 281 -- ^ Stores the original @with@ expression 282 | PreferFromCompletion 283 deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) 284 285instance Bifunctor PreferAnnotation where 286 first _ PreferFromSource = PreferFromSource 287 first f (PreferFromWith e ) = PreferFromWith (first f e) 288 first _ PreferFromCompletion = PreferFromCompletion 289 290 second = fmap 291 292-- | Record the field of a record-type and record-literal expression. 293-- The reason why we use the same ADT for both of them is because they store 294-- the same information. 295-- 296-- For example, 297-- 298-- > { {- A -} x {- B -} : {- C -} T } 299-- 300-- ... or 301-- 302-- > { {- A -} x {- B -} = {- C -} T } 303-- 304-- will be instantiated as follows: 305-- 306-- * @recordFieldSrc0@ corresponds to the @A@ comment. 307-- * @recordFieldValue@ is @"T"@ 308-- * @recordFieldSrc1@ corresponds to the @B@ comment. 309-- * @recordFieldSrc2@ corresponds to the @C@ comment. 310-- 311-- Although the @A@ comment isn't annotating the @"T"@ Record Field, 312-- this is the best place to keep these comments. 313-- 314-- Note that @recordFieldSrc2@ is always 'Nothing' when the 'RecordField' is for 315-- a punned entry, because there is no @=@ sign. For example, 316-- 317-- > { {- A -} x {- B -} } 318-- 319-- will be instantiated as follows: 320-- 321-- * @recordFieldSrc0@ corresponds to the @A@ comment. 322-- * @recordFieldValue@ corresponds to @(Var "x")@ 323-- * @recordFieldSrc1@ corresponds to the @B@ comment. 324-- * @recordFieldSrc2@ will be 'Nothing' 325-- 326-- The labels involved in a record using dot-syntax like in this example: 327-- 328-- > { {- A -} a {- B -} . {- C -} b {- D -} . {- E -} c {- F -} = {- G -} e } 329-- 330-- will be instantiated as follows: 331-- 332-- * For both the @a@ and @b@ field, @recordfieldSrc2@ is 'Nothing' 333-- * For the @a@ field: 334-- * @recordFieldSrc0@ corresponds to the @A@ comment 335-- * @recordFieldSrc1@ corresponds to the @B@ comment 336-- * For the @b@ field: 337-- * @recordFieldSrc0@ corresponds to the @C@ comment 338-- * @recordFieldSrc1@ corresponds to the @D@ comment 339-- * For the @c@ field: 340-- * @recordFieldSrc0@ corresponds to the @E@ comment 341-- * @recordFieldSrc1@ corresponds to the @F@ comment 342-- * @recordFieldSrc2@ corresponds to the @G@ comment 343-- 344-- That is, for every label except the last one the semantics of 345-- @recordFieldSrc0@ and @recordFieldSrc1@ are the same from a regular record 346-- label but @recordFieldSrc2@ is always 'Nothing'. For the last keyword, all 347-- srcs are 'Just' 348data RecordField s a = RecordField 349 { recordFieldSrc0 :: Maybe s 350 , recordFieldValue :: Expr s a 351 , recordFieldSrc1 :: Maybe s 352 , recordFieldSrc2 :: Maybe s 353 } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) 354 355-- | Construct a 'RecordField' with no src information 356makeRecordField :: Expr s a -> RecordField s a 357makeRecordField e = RecordField Nothing e Nothing Nothing 358 359 360instance Bifunctor RecordField where 361 first k (RecordField s0 value s1 s2) = 362 RecordField (k <$> s0) (first k value) (k <$> s1) (k <$> s2) 363 second = fmap 364 365{-| Record the label of a function or a function-type expression 366 367For example, 368 369> λ({- A -} a {- B -} : {- C -} T) -> e 370 371will be instantiated as follows: 372* @functionBindingSrc0@ corresponds to the @A@ comment 373* @functionBindingVariable@ is @a@ 374* @functionBindingSrc1@ corresponds to the @B@ comment 375* @functionBindingSrc2@ corresponds to the @C@ comment 376* @functionBindingAnnotation@ is @T@ 377-} 378data FunctionBinding s a = FunctionBinding 379 { functionBindingSrc0 :: Maybe s 380 , functionBindingVariable :: Text 381 , functionBindingSrc1 :: Maybe s 382 , functionBindingSrc2 :: Maybe s 383 , functionBindingAnnotation :: Expr s a 384 } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) 385 386-- | Smart constructor for 'FunctionBinding' with no src information 387makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a 388makeFunctionBinding l t = FunctionBinding Nothing l Nothing Nothing t 389 390instance Bifunctor FunctionBinding where 391 first k (FunctionBinding src0 label src1 src2 type_) = 392 FunctionBinding (k <$> src0) label (k <$> src1) (k <$> src2) (first k type_) 393 394 second = fmap 395 396-- | Record the field on a selector-expression 397-- 398-- For example, 399-- 400-- > e . {- A -} x {- B -} 401-- 402-- … will be instantiated as follows: 403-- 404-- * @fieldSelectionSrc0@ corresponds to the @A@ comment 405-- * @fieldSelectionLabel@ corresponds to @x@ 406-- * @fieldSelectionSrc1@ corresponds to the @B@ comment 407-- 408-- Given our limitation that not all expressions recover their whitespaces, the 409-- purpose of @fieldSelectionSrc1@ is to save the 'Text.Megaparsec.SourcePos' 410-- where the @fieldSelectionLabel@ ends, but we /still/ use a 'Maybe Src' 411-- (@s = 'Src'@) to be consistent with similar data types such as 'Binding', for 412-- example. 413data FieldSelection s = FieldSelection 414 { fieldSelectionSrc0 :: Maybe s 415 , fieldSelectionLabel :: !Text 416 , fieldSelectionSrc1 :: Maybe s 417 } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) 418 419-- | Smart constructor for 'FieldSelection' with no src information 420makeFieldSelection :: Text -> FieldSelection s 421makeFieldSelection t = FieldSelection Nothing t Nothing 422 423{-| Syntax tree for expressions 424 425 The @s@ type parameter is used to track the presence or absence of `Src` 426 spans: 427 428 * If @s = `Src`@ then the code may contains `Src` spans (either in a `Note` 429 constructor or inline within another constructor, like `Let`) 430 * If @s = `Void`@ then the code has no `Src` spans 431 432 The @a@ type parameter is used to track the presence or absence of imports 433 434 * If @a = `Import`@ then the code may contain unresolved `Import`s 435 * If @a = `Void`@ then the code has no `Import`s 436-} 437data Expr s a 438 -- | > Const c ~ c 439 = Const Const 440 -- | > Var (V x 0) ~ x 441 -- > Var (V x n) ~ x@n 442 | Var Var 443 -- | > Lam (FunctionBinding _ "x" _ _ A) b ~ λ(x : A) -> b 444 | Lam (Maybe CharacterSet) (FunctionBinding s a) (Expr s a) 445 -- | > Pi "_" A B ~ A -> B 446 -- > Pi x A B ~ ∀(x : A) -> B 447 | Pi (Maybe CharacterSet) Text (Expr s a) (Expr s a) 448 -- | > App f a ~ f a 449 | App (Expr s a) (Expr s a) 450 -- | > Let (Binding _ x _ Nothing _ r) e ~ let x = r in e 451 -- > Let (Binding _ x _ (Just t ) _ r) e ~ let x : t = r in e 452 -- 453 -- The difference between 454 -- 455 -- > let x = a let y = b in e 456 -- 457 -- and 458 -- 459 -- > let x = a in let y = b in e 460 -- 461 -- is only an additional 'Note' around @'Let' "y" …@ in the second 462 -- example. 463 -- 464 -- See 'MultiLet' for a representation of let-blocks that mirrors the 465 -- source code more closely. 466 | Let (Binding s a) (Expr s a) 467 -- | > Annot x t ~ x : t 468 | Annot (Expr s a) (Expr s a) 469 -- | > Bool ~ Bool 470 | Bool 471 -- | > BoolLit b ~ b 472 | BoolLit Bool 473 -- | > BoolAnd x y ~ x && y 474 | BoolAnd (Expr s a) (Expr s a) 475 -- | > BoolOr x y ~ x || y 476 | BoolOr (Expr s a) (Expr s a) 477 -- | > BoolEQ x y ~ x == y 478 | BoolEQ (Expr s a) (Expr s a) 479 -- | > BoolNE x y ~ x != y 480 | BoolNE (Expr s a) (Expr s a) 481 -- | > BoolIf x y z ~ if x then y else z 482 | BoolIf (Expr s a) (Expr s a) (Expr s a) 483 -- | > Natural ~ Natural 484 | Natural 485 -- | > NaturalLit n ~ n 486 | NaturalLit Natural 487 -- | > NaturalFold ~ Natural/fold 488 | NaturalFold 489 -- | > NaturalBuild ~ Natural/build 490 | NaturalBuild 491 -- | > NaturalIsZero ~ Natural/isZero 492 | NaturalIsZero 493 -- | > NaturalEven ~ Natural/even 494 | NaturalEven 495 -- | > NaturalOdd ~ Natural/odd 496 | NaturalOdd 497 -- | > NaturalToInteger ~ Natural/toInteger 498 | NaturalToInteger 499 -- | > NaturalShow ~ Natural/show 500 | NaturalShow 501 -- | > NaturalSubtract ~ Natural/subtract 502 | NaturalSubtract 503 -- | > NaturalPlus x y ~ x + y 504 | NaturalPlus (Expr s a) (Expr s a) 505 -- | > NaturalTimes x y ~ x * y 506 | NaturalTimes (Expr s a) (Expr s a) 507 -- | > Integer ~ Integer 508 | Integer 509 -- | > IntegerLit n ~ ±n 510 | IntegerLit Integer 511 -- | > IntegerClamp ~ Integer/clamp 512 | IntegerClamp 513 -- | > IntegerNegate ~ Integer/negate 514 | IntegerNegate 515 -- | > IntegerShow ~ Integer/show 516 | IntegerShow 517 -- | > IntegerToDouble ~ Integer/toDouble 518 | IntegerToDouble 519 -- | > Double ~ Double 520 | Double 521 -- | > DoubleLit n ~ n 522 | DoubleLit DhallDouble 523 -- | > DoubleShow ~ Double/show 524 | DoubleShow 525 -- | > Text ~ Text 526 | Text 527 -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~ "t1${e1}t2${e2}t3" 528 | TextLit (Chunks s a) 529 -- | > TextAppend x y ~ x ++ y 530 | TextAppend (Expr s a) (Expr s a) 531 -- | > TextReplace ~ Text/replace 532 | TextReplace 533 -- | > TextShow ~ Text/show 534 | TextShow 535 -- | > List ~ List 536 | List 537 -- | > ListLit (Just t ) [] ~ [] : t 538 -- > ListLit Nothing [x, y, z] ~ [x, y, z] 539 -- 540 -- Invariant: A non-empty list literal is always represented as 541 -- @ListLit Nothing xs@. 542 -- 543 -- When an annotated, non-empty list literal is parsed, it is represented 544 -- as 545 -- 546 -- > Annot (ListLit Nothing [x, y, z]) t ~ [x, y, z] : t 547 548 -- Eventually we should have separate constructors for empty and non-empty 549 -- list literals. For now it's easier to check the invariant in @infer@. 550 -- See https://github.com/dhall-lang/dhall-haskell/issues/1359#issuecomment-537087234. 551 | ListLit (Maybe (Expr s a)) (Seq (Expr s a)) 552 -- | > ListAppend x y ~ x # y 553 | ListAppend (Expr s a) (Expr s a) 554 -- | > ListBuild ~ List/build 555 | ListBuild 556 -- | > ListFold ~ List/fold 557 | ListFold 558 -- | > ListLength ~ List/length 559 | ListLength 560 -- | > ListHead ~ List/head 561 | ListHead 562 -- | > ListLast ~ List/last 563 | ListLast 564 -- | > ListIndexed ~ List/indexed 565 | ListIndexed 566 -- | > ListReverse ~ List/reverse 567 | ListReverse 568 -- | > Optional ~ Optional 569 | Optional 570 -- | > Some e ~ Some e 571 | Some (Expr s a) 572 -- | > None ~ None 573 | None 574 -- | > Record [ (k1, RecordField _ t1) ~ { k1 : t1, k2 : t1 } 575 -- > , (k2, RecordField _ t2) 576 -- > ] 577 | Record (Map Text (RecordField s a)) 578 -- | > RecordLit [ (k1, RecordField _ v1) ~ { k1 = v1, k2 = v2 } 579 -- > , (k2, RecordField _ v2) 580 -- > ] 581 | RecordLit (Map Text (RecordField s a)) 582 -- | > Union [(k1, Just t1), (k2, Nothing)] ~ < k1 : t1 | k2 > 583 | Union (Map Text (Maybe (Expr s a))) 584 -- | > Combine Nothing x y ~ x ∧ y 585 -- 586 -- The first field is a `Just` when the `Combine` operator is introduced 587 -- as a result of desugaring duplicate record fields: 588 -- 589 -- > RecordLit [ ( k ~ { k = x, k = y } 590 -- > , RecordField 591 -- > _ 592 -- > (Combine (Just k) x y) 593 -- > )] 594 | Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a) 595 -- | > CombineTypes x y ~ x ⩓ y 596 | CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a) 597 -- | > Prefer False x y ~ x ⫽ y 598 -- 599 -- The first field is a `True` when the `Prefer` operator is introduced as a 600 -- result of desugaring a @with@ expression 601 | Prefer (Maybe CharacterSet) (PreferAnnotation s a) (Expr s a) (Expr s a) 602 -- | > RecordCompletion x y ~ x::y 603 | RecordCompletion (Expr s a) (Expr s a) 604 -- | > Merge x y (Just t ) ~ merge x y : t 605 -- > Merge x y Nothing ~ merge x y 606 | Merge (Expr s a) (Expr s a) (Maybe (Expr s a)) 607 -- | > ToMap x (Just t) ~ toMap x : t 608 -- > ToMap x Nothing ~ toMap x 609 | ToMap (Expr s a) (Maybe (Expr s a)) 610 -- | > Field e (FieldSelection _ x _) ~ e.x 611 | Field (Expr s a) (FieldSelection s) 612 -- | > Project e (Left xs) ~ e.{ xs } 613 -- > Project e (Right t) ~ e.(t) 614 | Project (Expr s a) (Either [Text] (Expr s a)) 615 -- | > Assert e ~ assert : e 616 | Assert (Expr s a) 617 -- | > Equivalent x y ~ x ≡ y 618 | Equivalent (Expr s a) (Expr s a) 619 -- | > With x y e ~ x with y = e 620 | With (Expr s a) (NonEmpty Text) (Expr s a) 621 -- | > Note s x ~ e 622 | Note s (Expr s a) 623 -- | > ImportAlt ~ e1 ? e2 624 | ImportAlt (Expr s a) (Expr s a) 625 -- | > Embed import ~ import 626 | Embed a 627 deriving (Foldable, Generic, Traversable, Show, Data, Lift, NFData) 628-- NB: If you add a constructor to Expr, please also update the Arbitrary 629-- instance in Dhall.Test.QuickCheck. 630 631-- | This instance encodes what the Dhall standard calls an \"exact match\" 632-- between two expressions. 633-- 634-- Note that 635-- 636-- >>> nan = DhallDouble (0/0) 637-- >>> DoubleLit nan == DoubleLit nan 638-- True 639deriving instance (Eq s, Eq a) => Eq (Expr s a) 640 641-- | Note that this 'Ord' instance inherits `DhallDouble`'s defects. 642deriving instance (Ord s, Ord a) => Ord (Expr s a) 643 644-- This instance is hand-written due to the fact that deriving 645-- it does not give us an INLINABLE pragma. We annotate this fmap 646-- implementation with this pragma below to allow GHC to, possibly, 647-- inline the implementation for performance improvements. 648instance Functor (Expr s) where 649 fmap f (Embed a) = Embed (f a) 650 fmap f (Let b e2) = Let (fmap f b) (fmap f e2) 651 fmap f (Note s e1) = Note s (fmap f e1) 652 fmap f (Record a) = Record $ fmap f <$> a 653 fmap f (RecordLit a) = RecordLit $ fmap f <$> a 654 fmap f (Lam cs fb e) = Lam cs (f <$> fb) (f <$> e) 655 fmap f (Field a b) = Field (f <$> a) b 656 fmap f expression = Lens.over unsafeSubExpressions (fmap f) expression 657 {-# INLINABLE fmap #-} 658 659instance Applicative (Expr s) where 660 pure = Embed 661 662 (<*>) = Control.Monad.ap 663 664instance Monad (Expr s) where 665 return = pure 666 667 expression >>= k = case expression of 668 Embed a -> k a 669 Let a b -> Let (adaptBinding a) (b >>= k) 670 Note a b -> Note a (b >>= k) 671 Record a -> Record $ bindRecordKeyValues <$> a 672 RecordLit a -> RecordLit $ bindRecordKeyValues <$> a 673 Lam cs a b -> Lam cs (adaptFunctionBinding a) (b >>= k) 674 Field a b -> Field (a >>= k) b 675 _ -> Lens.over unsafeSubExpressions (>>= k) expression 676 where 677 bindRecordKeyValues (RecordField s0 e s1 s2) = 678 RecordField s0 (e >>= k) s1 s2 679 680 adaptBinding (Binding src0 c src1 d src2 e) = 681 Binding src0 c src1 (fmap adaptBindingAnnotation d) src2 (e >>= k) 682 683 adaptFunctionBinding (FunctionBinding src0 label src1 src2 type_) = 684 FunctionBinding src0 label src1 src2 (type_ >>= k) 685 686 adaptBindingAnnotation (src3, f) = (src3, f >>= k) 687 688instance Bifunctor Expr where 689 first k (Note a b ) = Note (k a) (first k b) 690 first _ (Embed a ) = Embed a 691 first k (Let a b ) = Let (first k a) (first k b) 692 first k (Record a ) = Record $ first k <$> a 693 first k (RecordLit a) = RecordLit $ first k <$> a 694 first k (Lam cs a b ) = Lam cs (first k a) (first k b) 695 first k (Field a b ) = Field (first k a) (k <$> b) 696 first k expression = Lens.over unsafeSubExpressions (first k) expression 697 698 second = fmap 699 700instance IsString (Expr s a) where 701 fromString str = Var (fromString str) 702 703-- | Generates a syntactically valid Dhall program 704instance Pretty a => Pretty (Expr s a) where 705 pretty = Pretty.unAnnotate . prettyExpr 706 707{- 708Instead of converting explicitly between 'Expr's and 'MultiLet', it might 709be nicer to use a pattern synonym: 710 711> pattern MultiLet' :: NonEmpty (Binding s a) -> Expr s a -> Expr s a 712> pattern MultiLet' as b <- (multiLetFromExpr -> Just (MultiLet as b)) where 713> MultiLet' as b = wrapInLets as b 714> 715> multiLetFromExpr :: Expr s a -> Maybe (MultiLet s a) 716> multiLetFromExpr = \case 717> Let x mA a b -> Just (multiLet x mA a b) 718> _ -> Nothing 719 720This works in principle, but GHC as of v8.8.1 doesn't handle it well: 721https://gitlab.haskell.org/ghc/ghc/issues/17096 722 723This should be fixed by GHC-8.10, so it might be worth revisiting then. 724-} 725 726{-| Generate a 'MultiLet' from the contents of a 'Let'. 727 728 In the resulting @'MultiLet' bs e@, @e@ is guaranteed not to be a 'Let', 729 but it might be a @('Note' … ('Let' …))@. 730 731 Given parser output, 'multiLet' consolidates @let@s that formed a 732 let-block in the original source. 733-} 734multiLet :: Binding s a -> Expr s a -> MultiLet s a 735multiLet b0 = \case 736 Let b1 e1 -> 737 let MultiLet bs e = multiLet b1 e1 738 in MultiLet (NonEmpty.cons b0 bs) e 739 e -> MultiLet (b0 :| []) e 740 741{-| Wrap let-'Binding's around an 'Expr'. 742 743'wrapInLets' can be understood as an inverse for 'multiLet': 744 745> let MultiLet bs e1 = multiLet b e0 746> 747> wrapInLets bs e1 == Let b e0 748-} 749wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a 750wrapInLets bs e = foldr Let e bs 751 752{-| This type represents 1 or more nested `Let` bindings that have been 753 coalesced together for ease of manipulation 754-} 755data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a) 756 757-- | A traversal over the immediate sub-expressions of an expression. 758subExpressions 759 :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a) 760subExpressions _ (Embed a) = pure (Embed a) 761subExpressions f (Note a b) = Note a <$> f b 762subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b 763subExpressions f (Record a) = Record <$> traverse (recordFieldExprs f) a 764subExpressions f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a 765subExpressions f (Lam cs fb e) = Lam cs <$> functionBindingExprs f fb <*> f e 766subExpressions f (Field a b) = Field <$> f a <*> pure b 767subExpressions f expression = unsafeSubExpressions f expression 768{-# INLINABLE subExpressions #-} 769 770{-| An internal utility used to implement transformations that require changing 771 one of the type variables of the `Expr` type 772 773 This utility only works because the implementation is partial, not 774 handling the `Let`, `Note`, or `Embed` cases, which need to be handled by 775 the caller. 776-} 777unsafeSubExpressions 778 :: Applicative f => (Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b) 779unsafeSubExpressions _ (Const c) = pure (Const c) 780unsafeSubExpressions _ (Var v) = pure (Var v) 781unsafeSubExpressions f (Pi cs a b c) = Pi cs a <$> f b <*> f c 782unsafeSubExpressions f (App a b) = App <$> f a <*> f b 783unsafeSubExpressions f (Annot a b) = Annot <$> f a <*> f b 784unsafeSubExpressions _ Bool = pure Bool 785unsafeSubExpressions _ (BoolLit b) = pure (BoolLit b) 786unsafeSubExpressions f (BoolAnd a b) = BoolAnd <$> f a <*> f b 787unsafeSubExpressions f (BoolOr a b) = BoolOr <$> f a <*> f b 788unsafeSubExpressions f (BoolEQ a b) = BoolEQ <$> f a <*> f b 789unsafeSubExpressions f (BoolNE a b) = BoolNE <$> f a <*> f b 790unsafeSubExpressions f (BoolIf a b c) = BoolIf <$> f a <*> f b <*> f c 791unsafeSubExpressions _ Natural = pure Natural 792unsafeSubExpressions _ (NaturalLit n) = pure (NaturalLit n) 793unsafeSubExpressions _ NaturalFold = pure NaturalFold 794unsafeSubExpressions _ NaturalBuild = pure NaturalBuild 795unsafeSubExpressions _ NaturalIsZero = pure NaturalIsZero 796unsafeSubExpressions _ NaturalEven = pure NaturalEven 797unsafeSubExpressions _ NaturalOdd = pure NaturalOdd 798unsafeSubExpressions _ NaturalToInteger = pure NaturalToInteger 799unsafeSubExpressions _ NaturalShow = pure NaturalShow 800unsafeSubExpressions _ NaturalSubtract = pure NaturalSubtract 801unsafeSubExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b 802unsafeSubExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b 803unsafeSubExpressions _ Integer = pure Integer 804unsafeSubExpressions _ (IntegerLit n) = pure (IntegerLit n) 805unsafeSubExpressions _ IntegerClamp = pure IntegerClamp 806unsafeSubExpressions _ IntegerNegate = pure IntegerNegate 807unsafeSubExpressions _ IntegerShow = pure IntegerShow 808unsafeSubExpressions _ IntegerToDouble = pure IntegerToDouble 809unsafeSubExpressions _ Double = pure Double 810unsafeSubExpressions _ (DoubleLit n) = pure (DoubleLit n) 811unsafeSubExpressions _ DoubleShow = pure DoubleShow 812unsafeSubExpressions _ Text = pure Text 813unsafeSubExpressions f (TextLit chunks) = 814 TextLit <$> chunkExprs f chunks 815unsafeSubExpressions f (TextAppend a b) = TextAppend <$> f a <*> f b 816unsafeSubExpressions _ TextReplace = pure TextReplace 817unsafeSubExpressions _ TextShow = pure TextShow 818unsafeSubExpressions _ List = pure List 819unsafeSubExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b 820unsafeSubExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b 821unsafeSubExpressions _ ListBuild = pure ListBuild 822unsafeSubExpressions _ ListFold = pure ListFold 823unsafeSubExpressions _ ListLength = pure ListLength 824unsafeSubExpressions _ ListHead = pure ListHead 825unsafeSubExpressions _ ListLast = pure ListLast 826unsafeSubExpressions _ ListIndexed = pure ListIndexed 827unsafeSubExpressions _ ListReverse = pure ListReverse 828unsafeSubExpressions _ Optional = pure Optional 829unsafeSubExpressions f (Some a) = Some <$> f a 830unsafeSubExpressions _ None = pure None 831unsafeSubExpressions f (Union a) = Union <$> traverse (traverse f) a 832unsafeSubExpressions f (Combine cs a b c) = Combine cs a <$> f b <*> f c 833unsafeSubExpressions f (CombineTypes cs a b) = CombineTypes cs <$> f a <*> f b 834unsafeSubExpressions f (Prefer cs a b c) = Prefer cs <$> a' <*> f b <*> f c 835 where 836 a' = case a of 837 PreferFromSource -> pure PreferFromSource 838 PreferFromWith d -> PreferFromWith <$> f d 839 PreferFromCompletion -> pure PreferFromCompletion 840unsafeSubExpressions f (RecordCompletion a b) = RecordCompletion <$> f a <*> f b 841unsafeSubExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t 842unsafeSubExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t 843unsafeSubExpressions f (Project a b) = Project <$> f a <*> traverse f b 844unsafeSubExpressions f (Assert a) = Assert <$> f a 845unsafeSubExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b 846unsafeSubExpressions f (With a b c) = With <$> f a <*> pure b <*> f c 847unsafeSubExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r 848unsafeSubExpressions _ (Let {}) = unhandledConstructor "Let" 849unsafeSubExpressions _ (Note {}) = unhandledConstructor "Note" 850unsafeSubExpressions _ (Embed {}) = unhandledConstructor "Embed" 851unsafeSubExpressions _ (Record {}) = unhandledConstructor "Record" 852unsafeSubExpressions _ (RecordLit {}) = unhandledConstructor "RecordLit" 853unsafeSubExpressions _ (Lam {}) = unhandledConstructor "Lam" 854unsafeSubExpressions _ (Field {}) = unhandledConstructor "Field" 855{-# INLINABLE unsafeSubExpressions #-} 856 857unhandledConstructor :: Text -> a 858unhandledConstructor constructor = 859 internalError 860 ( "Dhall.Syntax.unsafeSubExpressions: Unhandled " 861 <> constructor 862 <> " construtor" 863 ) 864 865{-| Traverse over the immediate 'Expr' children in a 'Binding'. 866-} 867bindingExprs 868 :: (Applicative f) 869 => (Expr s a -> f (Expr s b)) 870 -> Binding s a -> f (Binding s b) 871bindingExprs f (Binding s0 n s1 t s2 v) = 872 Binding 873 <$> pure s0 874 <*> pure n 875 <*> pure s1 876 <*> traverse (traverse f) t 877 <*> pure s2 878 <*> f v 879{-# INLINABLE bindingExprs #-} 880 881{-| Traverse over the immediate 'Expr' children in a 'RecordField'. 882-} 883recordFieldExprs 884 :: Applicative f 885 => (Expr s a -> f (Expr s b)) 886 -> RecordField s a -> f (RecordField s b) 887recordFieldExprs f (RecordField s0 e s1 s2) = 888 RecordField 889 <$> pure s0 890 <*> f e 891 <*> pure s1 892 <*> pure s2 893{-# INLINABLE recordFieldExprs #-} 894 895{-| Traverse over the immediate 'Expr' children in a 'FunctionBinding'. 896-} 897functionBindingExprs 898 :: Applicative f 899 => (Expr s a -> f (Expr s b)) 900 -> FunctionBinding s a -> f (FunctionBinding s b) 901functionBindingExprs f (FunctionBinding s0 label s1 s2 type_) = 902 FunctionBinding 903 <$> pure s0 904 <*> pure label 905 <*> pure s1 906 <*> pure s2 907 <*> f type_ 908{-# INLINABLE functionBindingExprs #-} 909 910-- | A traversal over the immediate sub-expressions in 'Chunks'. 911chunkExprs 912 :: Applicative f 913 => (Expr s a -> f (Expr t b)) 914 -> Chunks s a -> f (Chunks t b) 915chunkExprs f (Chunks chunks final) = 916 flip Chunks final <$> traverse (traverse f) chunks 917{-# INLINABLE chunkExprs #-} 918 919{-| Internal representation of a directory that stores the path components in 920 reverse order 921 922 In other words, the directory @\/foo\/bar\/baz@ is encoded as 923 @Directory { components = [ "baz", "bar", "foo" ] }@ 924-} 925newtype Directory = Directory { components :: [Text] } 926 deriving stock (Eq, Generic, Ord, Show) 927 deriving anyclass NFData 928 929instance Semigroup Directory where 930 Directory components₀ <> Directory components₁ = 931 Directory (components₁ <> components₀) 932 933instance Pretty Directory where 934 pretty (Directory {..}) = foldMap prettyPathComponent (reverse components) 935 936prettyPathComponent :: Text -> Doc ann 937prettyPathComponent text 938 | Data.Text.all pathCharacter text = 939 "/" <> Pretty.pretty text 940 | otherwise = 941 "/\"" <> Pretty.pretty text <> "\"" 942 943{-| A `File` is a `directory` followed by one additional path component 944 representing the `file` name 945-} 946data File = File 947 { directory :: Directory 948 , file :: Text 949 } deriving (Eq, Generic, Ord, Show, NFData) 950 951instance Pretty File where 952 pretty (File {..}) = 953 Pretty.pretty directory 954 <> prettyPathComponent file 955 956instance Semigroup File where 957 File directory₀ _ <> File directory₁ file = 958 File (directory₀ <> directory₁) file 959 960-- | The beginning of a file path which anchors subsequent path components 961data FilePrefix 962 = Absolute 963 -- ^ Absolute path 964 | Here 965 -- ^ Path relative to @.@ 966 | Parent 967 -- ^ Path relative to @..@ 968 | Home 969 -- ^ Path relative to @~@ 970 deriving (Eq, Generic, Ord, Show, NFData) 971 972instance Pretty FilePrefix where 973 pretty Absolute = "" 974 pretty Here = "." 975 pretty Parent = ".." 976 pretty Home = "~" 977 978-- | The URI scheme 979data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData) 980 981-- | This type stores all of the components of a remote import 982data URL = URL 983 { scheme :: Scheme 984 , authority :: Text 985 , path :: File 986 , query :: Maybe Text 987 , headers :: Maybe (Expr Src Import) 988 } deriving (Eq, Generic, Ord, Show, NFData) 989 990instance Pretty URL where 991 pretty (URL {..}) = 992 schemeDoc 993 <> "://" 994 <> Pretty.pretty authority 995 <> pathDoc 996 <> queryDoc 997 <> foldMap prettyHeaders headers 998 where 999 prettyHeaders h = 1000 " using " <> Pretty.unAnnotate (prettyImportExpression h) 1001 1002 File {..} = path 1003 1004 Directory {..} = directory 1005 1006 pathDoc = 1007 foldMap prettyURIComponent (reverse components) 1008 <> prettyURIComponent file 1009 1010 schemeDoc = case scheme of 1011 HTTP -> "http" 1012 HTTPS -> "https" 1013 1014 queryDoc = case query of 1015 Nothing -> "" 1016 Just q -> "?" <> Pretty.pretty q 1017 1018prettyURIComponent :: Text -> Doc ann 1019prettyURIComponent text = 1020 Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text 1021 1022-- | The type of import (i.e. local vs. remote vs. environment) 1023data ImportType 1024 = Local FilePrefix File 1025 -- ^ Local path 1026 | Remote URL 1027 -- ^ URL of remote resource and optional headers stored in an import 1028 | Env Text 1029 -- ^ Environment variable 1030 | Missing 1031 deriving (Eq, Generic, Ord, Show, NFData) 1032 1033parent :: File 1034parent = File { directory = Directory { components = [ ".." ] }, file = "" } 1035 1036instance Semigroup ImportType where 1037 Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁) 1038 1039 Remote (URL { path = path₀, ..}) <> Local Here path₁ = 1040 Remote (URL { path = path₀ <> path₁, ..}) 1041 1042 Local prefix file₀ <> Local Parent file₁ = 1043 Local prefix (file₀ <> parent <> file₁) 1044 1045 Remote (URL { path = path₀, .. }) <> Local Parent path₁ = 1046 Remote (URL { path = path₀ <> parent <> path₁, .. }) 1047 1048 import₀ <> Remote (URL { headers = headers₀, .. }) = 1049 Remote (URL { headers = headers₁, .. }) 1050 where 1051 importHashed₀ = Import (ImportHashed Nothing import₀) Code 1052 1053 headers₁ = fmap (fmap (importHashed₀ <>)) headers₀ 1054 1055 _ <> import₁ = 1056 import₁ 1057 1058instance Pretty ImportType where 1059 pretty (Local prefix file) = 1060 Pretty.pretty prefix <> Pretty.pretty file 1061 1062 pretty (Remote url) = Pretty.pretty url 1063 1064 pretty (Env env) = "env:" <> prettyEnvironmentVariable env 1065 1066 pretty Missing = "missing" 1067 1068-- | How to interpret the import's contents (i.e. as Dhall code or raw text) 1069data ImportMode = Code | RawText | Location 1070 deriving (Eq, Generic, Ord, Show, NFData) 1071 1072-- | A `ImportType` extended with an optional hash for semantic integrity checks 1073data ImportHashed = ImportHashed 1074 { hash :: Maybe Dhall.Crypto.SHA256Digest 1075 , importType :: ImportType 1076 } deriving (Eq, Generic, Ord, Show, NFData) 1077 1078instance Semigroup ImportHashed where 1079 ImportHashed _ importType₀ <> ImportHashed hash importType₁ = 1080 ImportHashed hash (importType₀ <> importType₁) 1081 1082instance Pretty ImportHashed where 1083 pretty (ImportHashed Nothing p) = 1084 Pretty.pretty p 1085 pretty (ImportHashed (Just h) p) = 1086 Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h) 1087 1088-- | Reference to an external resource 1089data Import = Import 1090 { importHashed :: ImportHashed 1091 , importMode :: ImportMode 1092 } deriving (Eq, Generic, Ord, Show, NFData) 1093 1094instance Semigroup Import where 1095 Import importHashed₀ _ <> Import importHashed₁ code = 1096 Import (importHashed₀ <> importHashed₁) code 1097 1098instance Pretty Import where 1099 pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix 1100 where 1101 suffix :: Text 1102 suffix = case importMode of 1103 RawText -> " as Text" 1104 Location -> " as Location" 1105 Code -> "" 1106 1107{-| Returns `True` if the given `Char` is valid within an unquoted path 1108 component 1109 1110 This is exported for reuse within the @"Dhall.Parser.Token"@ module 1111-} 1112pathCharacter :: Char -> Bool 1113pathCharacter c = 1114 '\x21' == c 1115 || ('\x24' <= c && c <= '\x27') 1116 || ('\x2A' <= c && c <= '\x2B') 1117 || ('\x2D' <= c && c <= '\x2E') 1118 || ('\x30' <= c && c <= '\x3B') 1119 || c == '\x3D' 1120 || ('\x40' <= c && c <= '\x5A') 1121 || ('\x5E' <= c && c <= '\x7A') 1122 || c == '\x7C' 1123 || c == '\x7E' 1124 1125-- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`) 1126-- 1127-- This also remove CharacterSet annotations. 1128denote :: Expr s a -> Expr t a 1129denote = \case 1130 Note _ b -> denote b 1131 Let a b -> Let (denoteBinding a) (denote b) 1132 Embed a -> Embed a 1133 Combine _ _ b c -> Combine Nothing Nothing (denote b) (denote c) 1134 CombineTypes _ b c -> CombineTypes Nothing (denote b) (denote c) 1135 Prefer _ a b c -> Lens.over unsafeSubExpressions denote $ Prefer Nothing a b c 1136 Record a -> Record $ denoteRecordField <$> a 1137 RecordLit a -> RecordLit $ denoteRecordField <$> a 1138 Lam _ a b -> Lam Nothing (denoteFunctionBinding a) (denote b) 1139 Pi _ t a b -> Pi Nothing t (denote a) (denote b) 1140 Field a (FieldSelection _ b _) -> Field (denote a) (FieldSelection Nothing b Nothing) 1141 expression -> Lens.over unsafeSubExpressions denote expression 1142 where 1143 denoteRecordField (RecordField _ e _ _) = RecordField Nothing (denote e) Nothing Nothing 1144 denoteBinding (Binding _ c _ d _ e) = 1145 Binding Nothing c Nothing (fmap denoteBindingAnnotation d) Nothing (denote e) 1146 1147 denoteBindingAnnotation (_, f) = (Nothing, denote f) 1148 1149 denoteFunctionBinding (FunctionBinding _ l _ _ t) = 1150 FunctionBinding Nothing l Nothing Nothing (denote t) 1151 1152-- | The \"opposite\" of `denote`, like @first absurd@ but faster 1153renote :: Expr Void a -> Expr s a 1154renote = unsafeCoerce 1155{-# INLINE renote #-} 1156 1157{-| Remove any outermost `Note` constructors 1158 1159 This is typically used when you want to get the outermost non-`Note` 1160 constructor without removing internal `Note` constructors 1161-} 1162shallowDenote :: Expr s a -> Expr s a 1163shallowDenote (Note _ e) = shallowDenote e 1164shallowDenote e = e 1165 1166-- | The set of reserved keywords according to the @keyword@ rule in the grammar 1167reservedKeywords :: HashSet Text 1168reservedKeywords = 1169 Data.HashSet.fromList 1170 [ 1171 "if" 1172 , "then" 1173 , "else" 1174 , "let" 1175 , "in" 1176 , "using" 1177 , "missing" 1178 , "as" 1179 , "Infinity" 1180 , "NaN" 1181 , "merge" 1182 , "Some" 1183 , "toMap" 1184 , "assert" 1185 , "forall" 1186 , "with" 1187 ] 1188 1189-- | The set of reserved identifiers for the Dhall language 1190-- | Contains also all keywords from "reservedKeywords" 1191reservedIdentifiers :: HashSet Text 1192reservedIdentifiers = reservedKeywords <> 1193 Data.HashSet.fromList 1194 [ -- Builtins according to the `builtin` rule in the grammar 1195 "Natural/fold" 1196 , "Natural/build" 1197 , "Natural/isZero" 1198 , "Natural/even" 1199 , "Natural/odd" 1200 , "Natural/toInteger" 1201 , "Natural/show" 1202 , "Natural/subtract" 1203 , "Integer" 1204 , "Integer/clamp" 1205 , "Integer/negate" 1206 , "Integer/show" 1207 , "Integer/toDouble" 1208 , "Integer/show" 1209 , "Natural/subtract" 1210 , "Double/show" 1211 , "List/build" 1212 , "List/fold" 1213 , "List/length" 1214 , "List/head" 1215 , "List/last" 1216 , "List/indexed" 1217 , "List/reverse" 1218 , "Text/replace" 1219 , "Text/show" 1220 , "Bool" 1221 , "True" 1222 , "False" 1223 , "Optional" 1224 , "None" 1225 , "Natural" 1226 , "Integer" 1227 , "Double" 1228 , "Text" 1229 , "List" 1230 , "Type" 1231 , "Kind" 1232 , "Sort" 1233 ] 1234 1235-- | Same as @Data.Text.splitOn@, except always returning a `NonEmpty` result 1236splitOn :: Text -> Text -> NonEmpty Text 1237splitOn needle haystack = 1238 case Data.Text.splitOn needle haystack of 1239 [] -> "" :| [] 1240 t : ts -> t :| ts 1241 1242-- | Split `Chunks` by lines 1243linesLiteral :: Chunks s a -> NonEmpty (Chunks s a) 1244linesLiteral (Chunks [] suffix) = 1245 fmap (Chunks []) (splitOn "\n" suffix) 1246linesLiteral (Chunks ((prefix, interpolation) : pairs₀) suffix₀) = 1247 foldr 1248 NonEmpty.cons 1249 (Chunks ((lastLine, interpolation) : pairs₁) suffix₁ :| chunks) 1250 (fmap (Chunks []) initLines) 1251 where 1252 splitLines = splitOn "\n" prefix 1253 1254 initLines = NonEmpty.init splitLines 1255 lastLine = NonEmpty.last splitLines 1256 1257 Chunks pairs₁ suffix₁ :| chunks = linesLiteral (Chunks pairs₀ suffix₀) 1258 1259-- | Flatten several `Chunks` back into a single `Chunks` by inserting newlines 1260unlinesLiteral :: NonEmpty (Chunks s a) -> Chunks s a 1261unlinesLiteral chunks = 1262 Data.Foldable.fold (NonEmpty.intersperse "\n" chunks) 1263 1264-- | Returns `True` if the `Chunks` represents a blank line 1265emptyLine :: Chunks s a -> Bool 1266emptyLine (Chunks [] "" ) = True 1267emptyLine (Chunks [] "\r") = True -- So that `\r\n` is treated as a blank line 1268emptyLine _ = False 1269 1270-- | Return the leading whitespace for a `Chunks` literal 1271leadingSpaces :: Chunks s a -> Text 1272leadingSpaces chunks = Data.Text.takeWhile isSpace firstText 1273 where 1274 isSpace c = c == ' ' || c == '\t' 1275 1276 firstText = 1277 case chunks of 1278 Chunks [] suffix -> suffix 1279 Chunks ((prefix, _) : _ ) _ -> prefix 1280 1281{-| Compute the longest shared whitespace prefix for the purposes of stripping 1282 leading indentation 1283-} 1284longestSharedWhitespacePrefix :: NonEmpty (Chunks s a) -> Text 1285longestSharedWhitespacePrefix literals = 1286 case fmap leadingSpaces filteredLines of 1287 l : ls -> Data.Foldable.foldl' sharedPrefix l ls 1288 [] -> "" 1289 where 1290 sharedPrefix ab ac = 1291 case Data.Text.commonPrefixes ab ac of 1292 Just (a, _b, _c) -> a 1293 Nothing -> "" 1294 1295 -- The standard specifies to filter out blank lines for all lines *except* 1296 -- for the last line 1297 filteredLines = newInit <> pure oldLast 1298 where 1299 oldInit = NonEmpty.init literals 1300 1301 oldLast = NonEmpty.last literals 1302 1303 newInit = filter (not . emptyLine) oldInit 1304 1305-- | Drop the first @n@ characters for a `Chunks` literal 1306dropLiteral :: Int -> Chunks s a -> Chunks s a 1307dropLiteral n (Chunks [] suffix) = 1308 Chunks [] (Data.Text.drop n suffix) 1309dropLiteral n (Chunks ((prefix, interpolation) : rest) suffix) = 1310 Chunks ((Data.Text.drop n prefix, interpolation) : rest) suffix 1311 1312{-| Convert a single-quoted `Chunks` literal to the equivalent double-quoted 1313 `Chunks` literal 1314-} 1315toDoubleQuoted :: Chunks Src a -> Chunks Src a 1316toDoubleQuoted literal = 1317 unlinesLiteral (fmap (dropLiteral indent) literals) 1318 where 1319 literals = linesLiteral literal 1320 1321 longestSharedPrefix = longestSharedWhitespacePrefix literals 1322 1323 indent = Data.Text.length longestSharedPrefix 1324 1325{-| `shift` is used by both normalization and type-checking to avoid variable 1326 capture by shifting variable indices 1327 1328 For example, suppose that you were to normalize the following expression: 1329 1330> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x 1331 1332 If you were to substitute @y@ with @x@ without shifting any variable 1333 indices, then you would get the following incorrect result: 1334 1335> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form 1336 1337 In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in 1338 order to avoid being misinterpreted as the @x@ bound by the innermost 1339 lambda. If we perform that `shift` then we get the correct result: 1340 1341> λ(a : Type) → λ(x : a) → λ(x : a) → x@1 1342 1343 As a more worked example, suppose that you were to normalize the following 1344 expression: 1345 1346> λ(a : Type) 1347> → λ(f : a → a → a) 1348> → λ(x : a) 1349> → λ(x : a) 1350> → (λ(x : a) → f x x@1) x@1 1351 1352 The correct normalized result would be: 1353 1354> λ(a : Type) 1355> → λ(f : a → a → a) 1356> → λ(x : a) 1357> → λ(x : a) 1358> → f x@1 x 1359 1360 The above example illustrates how we need to both increase and decrease 1361 variable indices as part of substitution: 1362 1363 * We need to increase the index of the outer @x\@1@ to @x\@2@ before we 1364 substitute it into the body of the innermost lambda expression in order 1365 to avoid variable capture. This substitution changes the body of the 1366 lambda expression to @(f x\@2 x\@1)@ 1367 1368 * We then remove the innermost lambda and therefore decrease the indices of 1369 both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one 1370 less @x@ variable is now bound within that scope 1371 1372 Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to 1373 the indices of all variables named @x@ whose indices are greater than 1374 @(n + m)@, where @m@ is the number of bound variables of the same name 1375 within that scope 1376 1377 In practice, @d@ is always @1@ or @-1@ because we either: 1378 1379 * increment variables by @1@ to avoid variable capture during substitution 1380 * decrement variables by @1@ when deleting lambdas after substitution 1381 1382 @n@ starts off at @0@ when substitution begins and increments every time we 1383 descend into a lambda or let expression that binds a variable of the same 1384 name in order to avoid shifting the bound variables by mistake. 1385-} 1386shift :: Int -> Var -> Expr s a -> Expr s a 1387shift d (V x n) (Var (V x' n')) = Var (V x' n'') 1388 where 1389 n'' = if x == x' && n <= n' then n' + d else n' 1390shift d (V x n) (Lam cs (FunctionBinding src0 x' src1 src2 _A) b) = 1391 Lam cs (FunctionBinding src0 x' src1 src2 _A') b' 1392 where 1393 _A' = shift d (V x n ) _A 1394 b' = shift d (V x n') b 1395 where 1396 n' = if x == x' then n + 1 else n 1397shift d (V x n) (Pi cs x' _A _B) = Pi cs x' _A' _B' 1398 where 1399 _A' = shift d (V x n ) _A 1400 _B' = shift d (V x n') _B 1401 where 1402 n' = if x == x' then n + 1 else n 1403shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) = 1404 Let (Binding src0 f src1 mt' src2 r') e' 1405 where 1406 e' = shift d (V x n') e 1407 where 1408 n' = if x == f then n + 1 else n 1409 1410 mt' = fmap (fmap (shift d (V x n))) mt 1411 r' = shift d (V x n) r 1412shift d v expression = Lens.over subExpressions (shift d v) expression 1413 1414-- | Desugar all @with@ expressions 1415desugarWith :: Expr s a -> Expr s a 1416desugarWith = Optics.rewriteOf subExpressions rewrite 1417 where 1418 rewrite e@(With record (key :| []) value) = 1419 Just 1420 (Prefer 1421 mempty 1422 (PreferFromWith e) 1423 record 1424 (RecordLit [ (key, makeRecordField value) ]) 1425 ) 1426 rewrite e@(With record (key0 :| key1 : keys) value) = 1427 Just 1428 (Let 1429 (makeBinding "_" record) 1430 (Prefer mempty (PreferFromWith e) "_" 1431 (RecordLit 1432 [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ] 1433 ) 1434 ) 1435 ) 1436 rewrite _ = Nothing 1437 1438_ERROR :: String 1439_ERROR = "\ESC[1;31mError\ESC[0m" 1440 1441{-| Utility function used to throw internal errors that should never happen 1442 (in theory) but that are not enforced by the type system 1443-} 1444internalError :: Data.Text.Text -> forall b . b 1445internalError text = error (unlines 1446 [ _ERROR <> ": Compiler bug " 1447 , " " 1448 , "Explanation: This error message means that there is a bug in the Dhall compiler." 1449 , "You didn't do anything wrong, but if you would like to see this problem fixed " 1450 , "then you should report the bug at: " 1451 , " " 1452 , "https://github.com/dhall-lang/dhall-haskell/issues " 1453 , " " 1454 , "Please include the following text in your bug report: " 1455 , " " 1456 , "``` " 1457 , Data.Text.unpack text <> " " 1458 , "``` " 1459 ] ) 1460