{-# 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 )
import qualified Data.Aeson.Key as Key

import Data.Text (Text)
import Data.Word (Word32)

-- 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.Syntax.Common.Pretty

import Agda.Utils.DocTree qualified as DocTree
import qualified Agda.Utils.FileName as File
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Interaction.Highlighting.Common (toAtoms)
import qualified Data.Aeson.KeyMap as KeyMap

toKey :: Text -> Key
toKey :: Text -> Key
toKey = Text -> Key
Key.fromText

---------------------------------------------------------------------------
-- * 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 a. a -> TCMT IO a
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e 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
  value <- TCM a
boxed
  pure $ key .= toJSON value

-- | Abbreviation of `_ #= encodeTCM _`
(@=) :: (EncodeTCM a) => Text -> a -> TCM Pair
@= :: forall a. EncodeTCM a => Text -> a -> TCM Pair
(@=) Text
key a
value = do
  encoded <- a -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM a
value
  pure $ key .= 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> TCMT IO a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> TCMT IO a
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
instance EncodeTCM Int
instance EncodeTCM Word32
instance EncodeTCM Value
instance EncodeTCM Doc
instance EncodeTCM DocTree

instance ToJSON DocTree where
  toJSON :: DocTree Aspects -> Value
toJSON = Text -> Value
forall a. ToJSON a => a -> Value
toJSON (Text -> Value)
-> (DocTree Aspects -> Text) -> DocTree Aspects -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DocTree Aspects -> Text
forall ann. DocTree ann -> Text
DocTree.treeToTextNoAnn
  -- toJSON = toJsonDocTree  -- TODO: communicate annotations to JSON client

-- UNUSED code taken from
-- https://github.com/plt-amy/agda/blob/9fd50b883f14a05792ed79a0b693fbecb2165bf5/src/full/Agda/LSP/Output.hs#L29-L35
toJsonDocTree :: DocTree -> Value
toJsonDocTree :: DocTree Aspects -> Value
toJsonDocTree = \case
    DocTree.Node Aspects
tt [DocTree Aspects]
ds -> Object -> Value
Object (Object -> Value) -> Object -> Value
forall a b. (a -> b) -> a -> b
$ [Pair] -> Object
forall v. [(Key, v)] -> KeyMap v
KeyMap.fromList
      [ (Key
"style", [String] -> Value
forall a. ToJSON a => a -> Value
toJSON (Aspects -> [String]
toAtoms Aspects
tt))
      , (Key
"children", [DocTree Aspects] -> Value
forall a. ToJSON a => [a] -> Value
toJSONList [DocTree Aspects]
ds)
      ]
    DocTree.Text Text
t -> Text -> Value
forall a. ToJSON a => a -> Value
toJSON Text
t

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
forall a. Doc a -> String
render

instance EncodeTCM a => EncodeTCM (Maybe a) where
  encodeTCM :: Maybe a -> TCM Value
encodeTCM Maybe a
Nothing   = Value -> TCM Value
forall a. a -> TCMT IO a
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