    {-# LANGUAGE DeriveGeneric #-}

    module Dhall.Syntax.Expr
        ( Expr(..)
        ) where

    import                Data.ByteString              (ByteString)
    import                Data.List.NonEmpty           (NonEmpty (..))
    import                Data.Sequence                (Seq)
    import                Data.String                  (IsString (..))
    import                Data.Text                    (Text)
    import                Data.Traversable             ()
    import                Dhall.Map                    (Map)
    import {-# SOURCE #-} Dhall.Pretty.Internal        (CharacterSet (..))
    import                Dhall.Syntax.Binding
    import                Dhall.Syntax.Chunks
    import                Dhall.Syntax.Const
    import                Dhall.Syntax.FunctionBinding
    import                Dhall.Syntax.RecordField
    import                Dhall.Syntax.Types
    import                Dhall.Syntax.Var
    import                GHC.Generics                 (Generic)
    import                Numeric.Natural              (Natural)

    import qualified Data.Time as Time

    {-| Syntax tree for expressions

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

        * If @s = `Dhall.Src.Src`@ then the code may contains `Dhall.Src.Src` spans
          (either in a `Note` constructor or inline within another constructor, like
          `Let`)
        * If @s = `Data.Void.Void`@ then the code has no `Dhall.Src.Src` spans

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

        * If @a = `Dhall.Syntax.Import.Import`@ then the code may contain unresolved
          `Dhall.Syntax.Import.Import`s
        * If @a = `Data.Void.Void`@ then the code has no
          `Dhall.Syntax.Import.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 _ (FunctionBinding _ "x" _ _ A) b    ~  λ(x : A) -> b
        | Lam (Maybe CharacterSet) (FunctionBinding s a) (Expr s a)
        -- | > Pi _ "_" A B                               ~        A  -> B
        --   > Pi _ x   A B                               ~  ∀(x : A) -> B
        | Pi  (Maybe CharacterSet) 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 `Dhall.Syntax.MultiLet.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)
        -- | > Bytes                                    ~ Bytes
        | Bytes
        -- | > BytesLit "\x00\xFF"                      ~ 0x"00FF"
        | BytesLit ByteString
        -- | > 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)
        -- | > TextReplace                              ~ Text/replace
        | TextReplace
        -- | > TextShow                                 ~  Text/show
        | TextShow
        -- | > Date                                     ~  Date
        | Date
        -- | > DateLiteral (fromGregorian _YYYY _MM _DD) ~ YYYY-MM-DD
        | DateLiteral Time.Day
        -- | > DateShow                                 ~  Date/show
        | DateShow
        -- | > Time                                     ~  Time
        | Time
        -- | > TimeLiteral (TimeOfDay hh mm ss) _       ~  hh:mm:ss
        | TimeLiteral
            Time.TimeOfDay
            Word
            -- ^ Precision
        -- | > TimeShow                                 ~  Time/show
        | TimeShow
        -- | > TimeZone                                 ~  TimeZone
        | TimeZone
        -- | > TimeZoneLiteral (TimeZone ( 60 * _HH + _MM) _ _) ~ +HH:MM
        -- | > TimeZoneLiteral (TimeZone (-60 * _HH + _MM) _ _) ~ -HH:MM
        | TimeZoneLiteral Time.TimeZone
        -- | > TimeZoneShow                             ~  TimeZone/Show
        | TimeZoneShow
        -- | > 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
        -- | > Record [ (k1, RecordField _ t1)          ~  { k1 : t1, k2 : t1 }
        --   >        , (k2, RecordField _ t2)
        --   >        ]
        | Record    (Map Text (RecordField s a))
        -- | > RecordLit [ (k1, RecordField _ v1)       ~  { k1 = v1, k2 = v2 }
        --   >           , (k2, RecordField _ v2)
        --   >           ]
        | RecordLit (Map Text (RecordField s a))
        -- | > Union        [(k1, Just t1), (k2, Nothing)] ~  < k1 : t1 | k2 >
        | Union     (Map Text (Maybe (Expr s a)))
        -- | > Combine _ Nothing x y                    ~  x ∧ y
        --
        -- The first field is a `Just` when the `Combine` operator is introduced
        -- as a result of desugaring duplicate record fields:
        --
        --   > RecordLit [ ( k                          ~ { k = x, k = y }
        --   >           , RecordField
        --   >              _
        --   >              (Combine (Just k) x y)
        --   >            )]
        | Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a)
        -- | > CombineTypes _ x y                       ~  x ⩓ y
        | CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a)
        -- | > Prefer _ _ x y                           ~  x ⫽ y
        | Prefer (Maybe CharacterSet) PreferAnnotation (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))
        -- | > ShowConstructor x                        ~  showConstructor x
        | ShowConstructor (Expr s a)
        -- | > Field e (FieldSelection _ x _)              ~  e.x
        | Field (Expr s a) (FieldSelection s)
        -- | > Project e (Left xs)                      ~  e.{ xs }
        --   > Project e (Right t)                      ~  e.(t)
        | Project (Expr s a) (Either [Text] (Expr s a))
        -- | > Assert e                                 ~  assert : e
        | Assert (Expr s a)
        -- | > Equivalent _ x y                           ~  x ≡ y
        | Equivalent (Maybe CharacterSet) (Expr s a) (Expr s a)
        -- | > With x y e                               ~  x with y = e
        | With (Expr s a) (NonEmpty WithComponent) (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 ((forall x. Expr s a -> Rep (Expr s a) x)
    -> (forall x. Rep (Expr s a) x -> Expr s a) -> Generic (Expr s a)
    forall x. Rep (Expr s a) x -> Expr s a
    forall x. Expr s a -> Rep (Expr s a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall s a x. Rep (Expr s a) x -> Expr s a
    forall s a x. Expr s a -> Rep (Expr s a) x
    $cfrom :: forall s a x. Expr s a -> Rep (Expr s a) x
    from :: forall x. Expr s a -> Rep (Expr s a) x
    $cto :: forall s a x. Rep (Expr s a) x -> Expr s a
    to :: forall x. Rep (Expr s a) x -> Expr s a
    Generic)
    -- NB: If you add a constructor to Expr, please also update the Arbitrary
    -- instance in Dhall.Test.QuickCheck.

    instance IsString (Expr s a) where
        fromString :: String -> Expr s a
    fromString String
    str = Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (String -> Var
    forall a. IsString a => String -> a
    fromString String
    str)