{-# 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
(.=) = forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
(Data.Aeson..=) 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
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Text
key forall a. ToJSON a => Text -> a -> Pair
.= 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 <- forall a. EncodeTCM a => a -> TCM Value
encodeTCM a
value
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Text
key 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Text
"kind" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Text -> Value
String Text
k) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Text
"kind" forall a. ToJSON a => Text -> a -> Pair
.= Text -> Value
String Text
k) 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. EncodeTCM a => a -> TCM Value
encodeTCM forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToJSON a => [a] -> Value
toJSONList

instance EncodeTCM a => EncodeTCM [a] where
  encodeTCM :: [a] -> TCM Value
encodeTCM = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. EncodeTCM a => a -> TCM Value
encodeTCM forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. ToJSON a => a -> Value
toJSON 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   = forall (m :: * -> *) a. Monad m => a -> m a
return Value
Null
  encodeTCM (Just a
a)  = forall a. EncodeTCM a => a -> TCM Value
encodeTCM a
a

instance ToJSON File.AbsolutePath where
  toJSON :: AbsolutePath -> Value
toJSON (File.AbsolutePath Text
path) = 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