    {-# LANGUAGE CPP               #-}
    {-# LANGUAGE OverloadedStrings #-}

    -- | Encoding stuff into JSON values in TCM

    module Agda.Interaction.JSON
      ( module Export
      , EncodeTCM(..)
      , obj, kind, kind'
      , (.=)
      , (@=), (#=)
      ) where

    import Control.Monad as Export ((>=>), (<=<))
    import Data.Aeson    as Export hiding (Result(..), (.=))

    import qualified Data.Aeson
    import Data.Aeson.Types ( Pair )
    #if MIN_VERSION_aeson(2,0,0)
    import qualified Data.Aeson.Key as Key
    #endif

    import Data.Text (Text)
    import GHC.Int (Int32)

    -- import qualified Agda.Syntax.Translation.InternalToAbstract as I2A
    -- import qualified Agda.Syntax.Translation.AbstractToConcrete as A2C

    -- import qualified Agda.Syntax.Concrete as C
    -- import qualified Agda.Syntax.Internal as I
    import Agda.TypeChecking.Monad
    import Agda.Utils.Pretty
    import qualified Agda.Utils.FileName as File
    import qualified Agda.Utils.Maybe.Strict as Strict

    #if MIN_VERSION_aeson(2,0,0)
    toKey :: Text -> Key
    toKey :: Text -> Key
    toKey = Text -> Key
    Key.fromText
    #else
    type Key = Text

    toKey :: Text -> Key
    toKey = id
    #endif

    ---------------------------------------------------------------------------
    -- * The EncodeTCM class

    -- | The JSON version of`PrettyTCM`, for encoding JSON value in TCM
    class EncodeTCM a where
      encodeTCM :: a -> TCM Value
      default encodeTCM :: ToJSON a => a -> TCM Value
      encodeTCM = Value -> TCM Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> TCM Value) -> (a -> Value) -> a -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Value
    forall a. ToJSON a => a -> Value
    toJSON

    -- | TCM monadic version of object
    obj :: [TCM Pair] -> TCM Value
    obj :: [TCM Pair] -> TCM Value
    obj = ([Pair] -> Value
    object ([Pair] -> Value) -> TCMT IO [Pair] -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (TCMT IO [Pair] -> TCM Value)
    -> ([TCM Pair] -> TCMT IO [Pair]) -> [TCM Pair] -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TCM Pair] -> TCMT IO [Pair]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence

    -- | A key-value pair for encoding a JSON object.
    (.=) :: ToJSON a => Text -> a -> Pair
    .= :: forall a. ToJSON a => Text -> a -> Pair
    (.=) = Key -> a -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    (Data.Aeson..=) (Key -> a -> Pair) -> (Text -> Key) -> Text -> a -> Pair
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Key
    toKey

    -- | Pairs a key with a value wrapped in TCM
    (#=) :: (ToJSON a) => Text -> TCM a -> TCM Pair
    #= :: forall a. ToJSON a => Text -> TCM a -> TCM Pair
    (#=) Text
    key TCM a
    boxed = do
      a
    value <- TCM a
    boxed
      Pair -> TCM Pair
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pair -> TCM Pair) -> Pair -> TCM Pair
    forall a b. (a -> b) -> a -> b
    $ Text
    key Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= a -> Value
    forall a. ToJSON a => a -> Value
    toJSON a
    value

    -- | Abbreviation of `_ #= encodeTCM _`
    (@=) :: (EncodeTCM a) => Text -> a -> TCM Pair
    @= :: forall a. EncodeTCM a => Text -> a -> TCM Pair
    (@=) Text
    key a
    value = do
      Value
    encoded <- a -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM a
    value
      Pair -> TCM Pair
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pair -> TCM Pair) -> Pair -> TCM Pair
    forall a b. (a -> b) -> a -> b
    $ Text
    key Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Value
    encoded

    -- | A handy alternative of `obj` with kind specified
    kind :: Text -> [TCM Pair] -> TCM Value
    kind :: Text -> [TCM Pair] -> TCM Value
    kind Text
    k = [TCM Pair] -> TCM Value
    obj ([TCM Pair] -> TCM Value)
    -> ([TCM Pair] -> [TCM Pair]) -> [TCM Pair] -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Text
    "kind" Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Text -> Value
    String Text
    k) TCM Pair -> [TCM Pair] -> [TCM Pair]
    forall a. a -> [a] -> [a]
    :)

    -- | A handy alternative of `object` with kind specified
    kind' :: Text -> [Pair] -> Value
    kind' :: Text -> [Pair] -> Value
    kind' Text
    k = [Pair] -> Value
    object ([Pair] -> Value) -> ([Pair] -> [Pair]) -> [Pair] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Text
    "kind" Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Text -> Value
    String Text
    k) Pair -> [Pair] -> [Pair]
    forall a. a -> [a] -> [a]
    :)

    -- ---------------------------------------------------------------------------
    -- -- * The Rep & ToRep class
    --
    -- -- | Translates internal types to concrete types
    -- class ToRep i c | i -> c where
    --   toRep :: i -> TCM c
    --
    -- instance ToRep I.Term C.Expr where
    --   toRep internal = I2A.reify internal >>= A2C.abstractToConcrete_
    --
    -- instance ToRep I.Type C.Expr where
    --   toRep internal = I2A.reify internal >>= A2C.abstractToConcrete_
    --
    -- data Rep internal concrete = Rep
    --   { internalRep :: internal
    --   , concreteRep :: concrete
    --   }
    --
    -- instance (ToJSON i, ToJSON c) => ToJSON (Rep i c) where
    --   toJSON (Rep i c) = object
    --     [ "internal" .= i
    --     , "concrete" .= c
    --     ]
    --
    -- rep :: (ToRep i c) => i -> TCM (Rep i c)
    -- rep internal = do
    --   concrete <- toRep internal
    --   return $ Rep
    --     { internalRep = internal
    --     , concreteRep = concrete
    --     }

    --------------------------------------------------------------------------------
    -- Instances of ToJSON or EncodeTCM

    encodeListTCM :: EncodeTCM a => [a] -> TCM Value
    encodeListTCM :: forall a. EncodeTCM a => [a] -> TCM Value
    encodeListTCM = (a -> TCM Value) -> [a] -> TCMT IO [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM a -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([a] -> TCMT IO [Value])
    -> ([Value] -> TCM Value) -> [a] -> TCM Value
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Value -> TCM Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> TCM Value) -> ([Value] -> Value) -> [Value] -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Value] -> Value
    forall a. ToJSON a => [a] -> Value
    toJSONList

    instance EncodeTCM a => EncodeTCM [a] where
      encodeTCM :: [a] -> TCM Value
    encodeTCM = (a -> TCM Value) -> [a] -> TCMT IO [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM a -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([a] -> TCMT IO [Value])
    -> ([Value] -> TCM Value) -> [a] -> TCM Value
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Value -> TCM Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> TCM Value) -> ([Value] -> Value) -> [Value] -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Value] -> Value
    forall a. ToJSON a => [a] -> Value
    toJSONList

    -- overlaps with the instance declared above
    instance {-# OVERLAPPING #-} EncodeTCM String

    instance EncodeTCM Bool where
    instance EncodeTCM Int where
    instance EncodeTCM Int32 where
    instance EncodeTCM Value where
    instance EncodeTCM Doc where

    instance ToJSON Doc where
      toJSON :: Doc -> Value
    toJSON = String -> Value
    forall a. ToJSON a => a -> Value
    toJSON (String -> Value) -> (Doc -> String) -> Doc -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> String
    render

    instance EncodeTCM a => EncodeTCM (Maybe a) where
      encodeTCM :: Maybe a -> TCM Value
    encodeTCM Maybe a
    Nothing   = Value -> TCM Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return Value
    Null
      encodeTCM (Just a
    a)  = a -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM a
    a

    instance ToJSON File.AbsolutePath where
      toJSON :: AbsolutePath -> Value
    toJSON (File.AbsolutePath Text
    path) = Text -> Value
    forall a. ToJSON a => a -> Value
    toJSON Text
    path

    #if !(MIN_VERSION_aeson(1,5,3))
    instance ToJSON a => ToJSON (Strict.Maybe a) where
      toJSON (Strict.Just a) = toJSON a
      toJSON Strict.Nothing  = Null
    #endif