{-# LANGUAGE OverloadedStrings #-}
module Agda.Interaction.JSON
( EncodeTCM(..)
, obj, kind, kind'
, (@=), (#=)
, (>=>), (<=<)
) where
import Control.Monad ((>=>), (<=<), sequence, liftM2)
import Data.Aeson
import Data.Aeson.Types (Pair)
import Data.Text (Text)
import GHC.Int (Int32)
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
class EncodeTCM a where
encodeTCM :: a -> TCM Value
default encodeTCM :: ToJSON a => a -> TCM Value
encodeTCM = pure . toJSON
obj :: [TCM Pair] -> TCM Value
obj = (object <$>) . sequence
(#=) :: (ToJSON a) => Text -> TCM a -> TCM Pair
(#=) key boxed = do
value <- boxed
pure $ key .= toJSON value
(@=) :: (EncodeTCM a) => Text -> a -> TCM Pair
(@=) key value = do
encoded <- encodeTCM value
pure $ key .= encoded
kind :: Text -> [TCM Pair] -> TCM Value
kind k = obj . (("kind" @= String k) :)
kind' :: Text -> [Pair] -> Value
kind' k = object . (("kind" .= String k) :)
encodeListTCM :: EncodeTCM a => [a] -> TCM Value
encodeListTCM = mapM encodeTCM >=> return . toJSONList
instance EncodeTCM a => EncodeTCM [a] where
encodeTCM = mapM encodeTCM >=> return . toJSONList
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 = toJSON . render
instance EncodeTCM a => EncodeTCM (Maybe a) where
encodeTCM Nothing = return Null
encodeTCM (Just a) = encodeTCM a
instance ToJSON File.AbsolutePath where
toJSON (File.AbsolutePath path) = toJSON path
instance ToJSON a => ToJSON (Strict.Maybe a) where
toJSON (Strict.Just a) = toJSON a
toJSON Strict.Nothing = Null