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

-- | Encoding stuff into JSON values in TCM

module Agda.Interaction.JSON
  ( EncodeTCM(..)
  , obj, kind, kind'
  , (@=), (#=)
  , (>=>), (<=<)
  -- , ToRep(..), rep
  ) where

import Control.Monad ((>=>), (<=<), sequence, liftM2)
import Data.Aeson
import Data.Aeson.Types (Pair)
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.TypeChecking.Pretty (PrettyTCM(..))
import Agda.Utils.Pretty
import qualified Agda.Utils.FileName as File
import qualified Agda.Utils.Maybe.Strict as Strict

---------------------------------------------------------------------------
-- * 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

-- | Pairs a key with a value wrapped in TCM
(#=) :: (ToJSON a) => Text -> TCM a -> TCM Pair
#= :: 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= a -> Value
forall a. ToJSON a => a -> Value
toJSON a
value

-- | Abbreviation of `_ #= encodeTCM _`
(@=) :: (EncodeTCM a) => Text -> a -> TCM Pair
@= :: 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 :: [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