content: {-# LANGUAGE DeriveGeneric            #-}
  {-# LANGUAGE StandaloneKindSignatures #-}
  
  module Dhall.Syntax.Expr
      ( Expr(..)
      ) where
  
  import                Data.ByteString              (ByteString)
  import                Data.Kind                    (Type)
  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
  -}
  type Expr :: Type -> Type -> Type
  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 (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 str = Var (fromString str)
  