{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FunctionalDependencies #-}

-- | Intermediate Representation for Agda's types
module Agda.IR where

import qualified Agda.Interaction.Response as Agda
import Agda.TypeChecking.Monad (TCM)
import Data.Aeson
import GHC.Generics (Generic)
import Render

--------------------------------------------------------------------------------

-- | Typeclass for converting Agda values into IR
class FromAgda a b | a -> b where
  fromAgda :: a -> b

class FromAgdaTCM a b | a -> b where
  fromAgdaTCM :: a -> TCM b

--------------------------------------------------------------------------------
-- | IR for IOCTM
data Response
  = -- non-last responses
    ResponseHighlightingInfoDirect HighlightingInfos
  | ResponseHighlightingInfoIndirect FilePath
  | ResponseDisplayInfo DisplayInfo
  | ResponseStatus Bool Bool
  | ResponseClearHighlightingTokenBased
  | ResponseClearHighlightingNotOnlyTokenBased
  | ResponseRunningInfo Int String
  | ResponseClearRunningInfo
  | ResponseDoneAborting
  | ResponseDoneExiting
  | ResponseGiveAction Int GiveResult
  | -- priority: 1
    ResponseInteractionPoints [Int]
  | -- priority: 2
    ResponseMakeCaseFunction [String]
  | ResponseMakeCaseExtendedLambda [String]
  | ResponseSolveAll [(Int, String)]
  | -- priority: 3
    ResponseJumpToError FilePath Int
  | ResponseEnd
  deriving (forall x. Rep Response x -> Response
forall x. Response -> Rep Response x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Response x -> Response
$cfrom :: forall x. Response -> Rep Response x
Generic)

instance ToJSON Response

--------------------------------------------------------------------------------

-- | IR for DisplayInfo
data DisplayInfo
  = DisplayInfoGeneric String [Block]
  | DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]
  | DisplayInfoCurrentGoal Block
  | DisplayInfoInferredType Block
  | DisplayInfoCompilationOk [String] [String]
  | DisplayInfoAuto String
  | DisplayInfoError String
  | DisplayInfoTime String
  | DisplayInfoNormalForm String
  deriving (forall x. Rep DisplayInfo x -> DisplayInfo
forall x. DisplayInfo -> Rep DisplayInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DisplayInfo x -> DisplayInfo
$cfrom :: forall x. DisplayInfo -> Rep DisplayInfo x
Generic)

instance ToJSON DisplayInfo

--------------------------------------------------------------------------------

-- | GiveResult
data GiveResult
  = GiveString String
  | GiveParen
  | GiveNoParen
  deriving (forall x. Rep GiveResult x -> GiveResult
forall x. GiveResult -> Rep GiveResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GiveResult x -> GiveResult
$cfrom :: forall x. GiveResult -> Rep GiveResult x
Generic)

instance FromAgda Agda.GiveResult GiveResult where
  fromAgda :: GiveResult -> GiveResult
fromAgda (Agda.Give_String FilePath
s) = FilePath -> GiveResult
GiveString FilePath
s
  fromAgda GiveResult
Agda.Give_Paren = GiveResult
GiveParen
  fromAgda GiveResult
Agda.Give_NoParen = GiveResult
GiveNoParen

instance ToJSON GiveResult

--------------------------------------------------------------------------------

-- | IR for HighlightingInfo
data HighlightingInfo
  = HighlightingInfo
      Int -- starting offset
      Int -- ending offset
      [String] -- list of names of aspects
      Bool -- is token based?
      String -- note
      (Maybe (FilePath, Int)) -- the defining module of the token and its position in that module
  deriving (forall x. Rep HighlightingInfo x -> HighlightingInfo
forall x. HighlightingInfo -> Rep HighlightingInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep HighlightingInfo x -> HighlightingInfo
$cfrom :: forall x. HighlightingInfo -> Rep HighlightingInfo x
Generic, Int -> HighlightingInfo -> ShowS
[HighlightingInfo] -> ShowS
HighlightingInfo -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [HighlightingInfo] -> ShowS
$cshowList :: [HighlightingInfo] -> ShowS
show :: HighlightingInfo -> FilePath
$cshow :: HighlightingInfo -> FilePath
showsPrec :: Int -> HighlightingInfo -> ShowS
$cshowsPrec :: Int -> HighlightingInfo -> ShowS
Show)

instance ToJSON HighlightingInfo

data HighlightingInfos = HighlightingInfos Bool [HighlightingInfo]
  deriving (forall x. Rep HighlightingInfos x -> HighlightingInfos
forall x. HighlightingInfos -> Rep HighlightingInfos x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep HighlightingInfos x -> HighlightingInfos
$cfrom :: forall x. HighlightingInfos -> Rep HighlightingInfos x
Generic, Int -> HighlightingInfos -> ShowS
[HighlightingInfos] -> ShowS
HighlightingInfos -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [HighlightingInfos] -> ShowS
$cshowList :: [HighlightingInfos] -> ShowS
show :: HighlightingInfos -> FilePath
$cshow :: HighlightingInfos -> FilePath
showsPrec :: Int -> HighlightingInfos -> ShowS
$cshowsPrec :: Int -> HighlightingInfos -> ShowS
Show)

instance ToJSON HighlightingInfos