{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}

module Cornelis.Types
  ( module Cornelis.Types
  , InteractionId
  , Buffer
  , Window
  , Text
  , traceMX
  , HasCallStack
  ) where

import Control.Concurrent.Chan.Unagi (InChan)
import Control.Monad.State.Class
import Cornelis.Debug
import Cornelis.Offsets (Pos(..), Interval(..), AgdaIndex, AgdaPos, AgdaInterval, VimIndex, LineNumber, Indexing(..))
import Cornelis.Types.Agda (InteractionId)
import Data.Aeson hiding (Error)
import Data.Char (toLower)
import Data.Functor.Identity
import Data.Generics.Labels ()
import Data.IORef
import Data.IntervalMap.FingerTree (IntervalMap)
import Data.Map (Map)
import Data.Maybe (listToMaybe)
import Data.Text (Text)
import DiffLoc (Diff, Colline)
import GHC.Generics
import GHC.Stack
import Neovim hiding (err)
import Neovim.API.Text (Buffer(..), Window)
import System.Process (ProcessHandle)

deriving stock instance Ord Buffer

data Agda = Agda
  { Agda -> Buffer
a_buffer :: Buffer
  , Agda -> IORef Bool
a_ready  :: IORef Bool
  , Agda -> InChan [Char]
a_req    :: InChan String
  , Agda -> ProcessHandle
a_hdl    :: ProcessHandle
  }
  deriving (forall x. Agda -> Rep Agda x)
-> (forall x. Rep Agda x -> Agda) -> Generic Agda
forall x. Rep Agda x -> Agda
forall x. Agda -> Rep Agda x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Agda -> Rep Agda x
from :: forall x. Agda -> Rep Agda x
$cto :: forall x. Rep Agda x -> Agda
to :: forall x. Rep Agda x -> Agda
Generic

data BufferStuff = BufferStuff
  { BufferStuff -> Agda
bs_agda_proc  :: Agda
  , BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips        :: Map InteractionId (InteractionPoint Identity)
  , BufferStuff -> Map InteractionId Extmark
bs_ip_exts    :: Map InteractionId Extmark
  , BufferStuff -> Map Extmark DefinitionSite
bs_goto_sites :: Map Extmark DefinitionSite
  , BufferStuff -> DisplayInfo
bs_goals      :: DisplayInfo
  , BufferStuff -> InfoBuffer
bs_info_win   :: InfoBuffer
  , BufferStuff -> LineIntervals
bs_code_map   :: LineIntervals
  }
  deriving (forall x. BufferStuff -> Rep BufferStuff x)
-> (forall x. Rep BufferStuff x -> BufferStuff)
-> Generic BufferStuff
forall x. Rep BufferStuff x -> BufferStuff
forall x. BufferStuff -> Rep BufferStuff x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BufferStuff -> Rep BufferStuff x
from :: forall x. BufferStuff -> Rep BufferStuff x
$cto :: forall x. Rep BufferStuff x -> BufferStuff
to :: forall x. Rep BufferStuff x -> BufferStuff
Generic

newtype InfoBuffer = InfoBuffer
  { InfoBuffer -> Buffer
iw_buffer :: Buffer
  }
  deriving (forall x. InfoBuffer -> Rep InfoBuffer x)
-> (forall x. Rep InfoBuffer x -> InfoBuffer) -> Generic InfoBuffer
forall x. Rep InfoBuffer x -> InfoBuffer
forall x. InfoBuffer -> Rep InfoBuffer x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. InfoBuffer -> Rep InfoBuffer x
from :: forall x. InfoBuffer -> Rep InfoBuffer x
$cto :: forall x. Rep InfoBuffer x -> InfoBuffer
to :: forall x. Rep InfoBuffer x -> InfoBuffer
Generic

data CornelisState = CornelisState
  { CornelisState -> Map Buffer BufferStuff
cs_buffers :: Map Buffer BufferStuff
  , CornelisState -> Map BufferNum Diff0
cs_diff :: Map BufferNum Diff0
  }
  deriving (forall x. CornelisState -> Rep CornelisState x)
-> (forall x. Rep CornelisState x -> CornelisState)
-> Generic CornelisState
forall x. Rep CornelisState x -> CornelisState
forall x. CornelisState -> Rep CornelisState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CornelisState -> Rep CornelisState x
from :: forall x. CornelisState -> Rep CornelisState x
$cto :: forall x. Rep CornelisState x -> CornelisState
to :: forall x. Rep CornelisState x -> CornelisState
Generic

data SplitLocation
  = Vertical
  | Horizontal
  | OnLeft
  | OnRight
  | OnTop
  | OnBottom
  deriving (SplitLocation -> SplitLocation -> Bool
(SplitLocation -> SplitLocation -> Bool)
-> (SplitLocation -> SplitLocation -> Bool) -> Eq SplitLocation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SplitLocation -> SplitLocation -> Bool
== :: SplitLocation -> SplitLocation -> Bool
$c/= :: SplitLocation -> SplitLocation -> Bool
/= :: SplitLocation -> SplitLocation -> Bool
Eq, Eq SplitLocation
Eq SplitLocation =>
(SplitLocation -> SplitLocation -> Ordering)
-> (SplitLocation -> SplitLocation -> Bool)
-> (SplitLocation -> SplitLocation -> Bool)
-> (SplitLocation -> SplitLocation -> Bool)
-> (SplitLocation -> SplitLocation -> Bool)
-> (SplitLocation -> SplitLocation -> SplitLocation)
-> (SplitLocation -> SplitLocation -> SplitLocation)
-> Ord SplitLocation
SplitLocation -> SplitLocation -> Bool
SplitLocation -> SplitLocation -> Ordering
SplitLocation -> SplitLocation -> SplitLocation
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SplitLocation -> SplitLocation -> Ordering
compare :: SplitLocation -> SplitLocation -> Ordering
$c< :: SplitLocation -> SplitLocation -> Bool
< :: SplitLocation -> SplitLocation -> Bool
$c<= :: SplitLocation -> SplitLocation -> Bool
<= :: SplitLocation -> SplitLocation -> Bool
$c> :: SplitLocation -> SplitLocation -> Bool
> :: SplitLocation -> SplitLocation -> Bool
$c>= :: SplitLocation -> SplitLocation -> Bool
>= :: SplitLocation -> SplitLocation -> Bool
$cmax :: SplitLocation -> SplitLocation -> SplitLocation
max :: SplitLocation -> SplitLocation -> SplitLocation
$cmin :: SplitLocation -> SplitLocation -> SplitLocation
min :: SplitLocation -> SplitLocation -> SplitLocation
Ord, Int -> SplitLocation
SplitLocation -> Int
SplitLocation -> [SplitLocation]
SplitLocation -> SplitLocation
SplitLocation -> SplitLocation -> [SplitLocation]
SplitLocation -> SplitLocation -> SplitLocation -> [SplitLocation]
(SplitLocation -> SplitLocation)
-> (SplitLocation -> SplitLocation)
-> (Int -> SplitLocation)
-> (SplitLocation -> Int)
-> (SplitLocation -> [SplitLocation])
-> (SplitLocation -> SplitLocation -> [SplitLocation])
-> (SplitLocation -> SplitLocation -> [SplitLocation])
-> (SplitLocation
    -> SplitLocation -> SplitLocation -> [SplitLocation])
-> Enum SplitLocation
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: SplitLocation -> SplitLocation
succ :: SplitLocation -> SplitLocation
$cpred :: SplitLocation -> SplitLocation
pred :: SplitLocation -> SplitLocation
$ctoEnum :: Int -> SplitLocation
toEnum :: Int -> SplitLocation
$cfromEnum :: SplitLocation -> Int
fromEnum :: SplitLocation -> Int
$cenumFrom :: SplitLocation -> [SplitLocation]
enumFrom :: SplitLocation -> [SplitLocation]
$cenumFromThen :: SplitLocation -> SplitLocation -> [SplitLocation]
enumFromThen :: SplitLocation -> SplitLocation -> [SplitLocation]
$cenumFromTo :: SplitLocation -> SplitLocation -> [SplitLocation]
enumFromTo :: SplitLocation -> SplitLocation -> [SplitLocation]
$cenumFromThenTo :: SplitLocation -> SplitLocation -> SplitLocation -> [SplitLocation]
enumFromThenTo :: SplitLocation -> SplitLocation -> SplitLocation -> [SplitLocation]
Enum, SplitLocation
SplitLocation -> SplitLocation -> Bounded SplitLocation
forall a. a -> a -> Bounded a
$cminBound :: SplitLocation
minBound :: SplitLocation
$cmaxBound :: SplitLocation
maxBound :: SplitLocation
Bounded)

instance Show SplitLocation where
  show :: SplitLocation -> [Char]
show SplitLocation
Vertical   = [Char]
"vertical"
  show SplitLocation
Horizontal = [Char]
"horizontal"
  show SplitLocation
OnLeft     = [Char]
"left"
  show SplitLocation
OnRight    = [Char]
"right"
  show SplitLocation
OnTop      = [Char]
"top"
  show SplitLocation
OnBottom   = [Char]
"bottom"

readSplitLocation :: String -> Maybe SplitLocation
readSplitLocation :: [Char] -> Maybe SplitLocation
readSplitLocation [Char]
s = case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Char
toLower [Char]
s of
  [Char]
"vertical"   -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
Vertical
  [Char]
"horizontal" -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
Horizontal
  [Char]
"left"       -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
OnLeft
  [Char]
"right"      -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
OnRight
  [Char]
"top"        -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
OnTop
  [Char]
"bottom"     -> SplitLocation -> Maybe SplitLocation
forall a. a -> Maybe a
Just SplitLocation
OnBottom
  [Char]
_            -> Maybe SplitLocation
forall a. Maybe a
Nothing


data CornelisConfig = CornelisConfig
  { CornelisConfig -> BufferNum
cc_max_height :: Int64
  , CornelisConfig -> BufferNum
cc_max_width :: Int64
  , CornelisConfig -> SplitLocation
cc_split_location :: SplitLocation
  }
  deriving (Int -> CornelisConfig -> ShowS
[CornelisConfig] -> ShowS
CornelisConfig -> [Char]
(Int -> CornelisConfig -> ShowS)
-> (CornelisConfig -> [Char])
-> ([CornelisConfig] -> ShowS)
-> Show CornelisConfig
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CornelisConfig -> ShowS
showsPrec :: Int -> CornelisConfig -> ShowS
$cshow :: CornelisConfig -> [Char]
show :: CornelisConfig -> [Char]
$cshowList :: [CornelisConfig] -> ShowS
showList :: [CornelisConfig] -> ShowS
Show, (forall x. CornelisConfig -> Rep CornelisConfig x)
-> (forall x. Rep CornelisConfig x -> CornelisConfig)
-> Generic CornelisConfig
forall x. Rep CornelisConfig x -> CornelisConfig
forall x. CornelisConfig -> Rep CornelisConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CornelisConfig -> Rep CornelisConfig x
from :: forall x. CornelisConfig -> Rep CornelisConfig x
$cto :: forall x. Rep CornelisConfig x -> CornelisConfig
to :: forall x. Rep CornelisConfig x -> CornelisConfig
Generic)

data CornelisEnv = CornelisEnv
  { CornelisEnv -> IORef CornelisState
ce_state :: IORef CornelisState
  , CornelisEnv -> InChan AgdaResp
ce_stream :: InChan AgdaResp
  , CornelisEnv -> BufferNum
ce_namespace :: Int64
  , CornelisEnv -> CornelisConfig
ce_config :: CornelisConfig
  }
  deriving (forall x. CornelisEnv -> Rep CornelisEnv x)
-> (forall x. Rep CornelisEnv x -> CornelisEnv)
-> Generic CornelisEnv
forall x. Rep CornelisEnv x -> CornelisEnv
forall x. CornelisEnv -> Rep CornelisEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CornelisEnv -> Rep CornelisEnv x
from :: forall x. CornelisEnv -> Rep CornelisEnv x
$cto :: forall x. Rep CornelisEnv x -> CornelisEnv
to :: forall x. Rep CornelisEnv x -> CornelisEnv
Generic

data AgdaResp = AgdaResp
  { AgdaResp -> Buffer
ar_buffer :: Buffer
  , AgdaResp -> Response
ar_message :: Response
  }
  deriving (forall x. AgdaResp -> Rep AgdaResp x)
-> (forall x. Rep AgdaResp x -> AgdaResp) -> Generic AgdaResp
forall x. Rep AgdaResp x -> AgdaResp
forall x. AgdaResp -> Rep AgdaResp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AgdaResp -> Rep AgdaResp x
from :: forall x. AgdaResp -> Rep AgdaResp x
$cto :: forall x. Rep AgdaResp x -> AgdaResp
to :: forall x. Rep AgdaResp x -> AgdaResp
Generic

instance MonadState CornelisState (Neovim CornelisEnv) where
  get :: Neovim CornelisEnv CornelisState
get = do
    IORef CornelisState
mv <- (CornelisEnv -> IORef CornelisState)
-> Neovim CornelisEnv (IORef CornelisState)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> IORef CornelisState
ce_state
    IO CornelisState -> Neovim CornelisEnv CornelisState
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CornelisState -> Neovim CornelisEnv CornelisState)
-> IO CornelisState -> Neovim CornelisEnv CornelisState
forall a b. (a -> b) -> a -> b
$ IORef CornelisState -> IO CornelisState
forall a. IORef a -> IO a
readIORef IORef CornelisState
mv
  put :: CornelisState -> Neovim CornelisEnv ()
put CornelisState
a = do
    IORef CornelisState
mv <- (CornelisEnv -> IORef CornelisState)
-> Neovim CornelisEnv (IORef CornelisState)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> IORef CornelisState
ce_state
    IO () -> Neovim CornelisEnv ()
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Neovim CornelisEnv ()) -> IO () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ IORef CornelisState -> CornelisState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef CornelisState
mv CornelisState
a

data Response
  = DisplayInfo DisplayInfo
  | ClearHighlighting -- TokenBased
  | HighlightingInfo Bool [Highlight]
  | ClearRunningInfo
  | RunningInfo Int Text
  | Status
    { Response -> Bool
status_checked :: Bool
    , Response -> Bool
status_showIrrelevant :: Bool
    , Response -> Bool
status_showImplicits :: Bool
    }
  | JumpToError FilePath AgdaIndex
  | InteractionPoints [InteractionPoint Maybe]
  | GiveAction Text (InteractionPoint (Const ()))
  | MakeCase MakeCase
  | SolveAll [Solution]
  | Unknown Text Value
  deriving (Response -> Response -> Bool
(Response -> Response -> Bool)
-> (Response -> Response -> Bool) -> Eq Response
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Response -> Response -> Bool
== :: Response -> Response -> Bool
$c/= :: Response -> Response -> Bool
/= :: Response -> Response -> Bool
Eq, Eq Response
Eq Response =>
(Response -> Response -> Ordering)
-> (Response -> Response -> Bool)
-> (Response -> Response -> Bool)
-> (Response -> Response -> Bool)
-> (Response -> Response -> Bool)
-> (Response -> Response -> Response)
-> (Response -> Response -> Response)
-> Ord Response
Response -> Response -> Bool
Response -> Response -> Ordering
Response -> Response -> Response
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Response -> Response -> Ordering
compare :: Response -> Response -> Ordering
$c< :: Response -> Response -> Bool
< :: Response -> Response -> Bool
$c<= :: Response -> Response -> Bool
<= :: Response -> Response -> Bool
$c> :: Response -> Response -> Bool
> :: Response -> Response -> Bool
$c>= :: Response -> Response -> Bool
>= :: Response -> Response -> Bool
$cmax :: Response -> Response -> Response
max :: Response -> Response -> Response
$cmin :: Response -> Response -> Response
min :: Response -> Response -> Response
Ord, Int -> Response -> ShowS
[Response] -> ShowS
Response -> [Char]
(Int -> Response -> ShowS)
-> (Response -> [Char]) -> ([Response] -> ShowS) -> Show Response
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Response -> ShowS
showsPrec :: Int -> Response -> ShowS
$cshow :: Response -> [Char]
show :: Response -> [Char]
$cshowList :: [Response] -> ShowS
showList :: [Response] -> ShowS
Show)

data DefinitionSite = DefinitionSite
  { DefinitionSite -> Text
ds_filepath :: Text
  , DefinitionSite -> AgdaIndex
ds_position :: AgdaIndex
  }
  deriving (DefinitionSite -> DefinitionSite -> Bool
(DefinitionSite -> DefinitionSite -> Bool)
-> (DefinitionSite -> DefinitionSite -> Bool) -> Eq DefinitionSite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DefinitionSite -> DefinitionSite -> Bool
== :: DefinitionSite -> DefinitionSite -> Bool
$c/= :: DefinitionSite -> DefinitionSite -> Bool
/= :: DefinitionSite -> DefinitionSite -> Bool
Eq, Eq DefinitionSite
Eq DefinitionSite =>
(DefinitionSite -> DefinitionSite -> Ordering)
-> (DefinitionSite -> DefinitionSite -> Bool)
-> (DefinitionSite -> DefinitionSite -> Bool)
-> (DefinitionSite -> DefinitionSite -> Bool)
-> (DefinitionSite -> DefinitionSite -> Bool)
-> (DefinitionSite -> DefinitionSite -> DefinitionSite)
-> (DefinitionSite -> DefinitionSite -> DefinitionSite)
-> Ord DefinitionSite
DefinitionSite -> DefinitionSite -> Bool
DefinitionSite -> DefinitionSite -> Ordering
DefinitionSite -> DefinitionSite -> DefinitionSite
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DefinitionSite -> DefinitionSite -> Ordering
compare :: DefinitionSite -> DefinitionSite -> Ordering
$c< :: DefinitionSite -> DefinitionSite -> Bool
< :: DefinitionSite -> DefinitionSite -> Bool
$c<= :: DefinitionSite -> DefinitionSite -> Bool
<= :: DefinitionSite -> DefinitionSite -> Bool
$c> :: DefinitionSite -> DefinitionSite -> Bool
> :: DefinitionSite -> DefinitionSite -> Bool
$c>= :: DefinitionSite -> DefinitionSite -> Bool
>= :: DefinitionSite -> DefinitionSite -> Bool
$cmax :: DefinitionSite -> DefinitionSite -> DefinitionSite
max :: DefinitionSite -> DefinitionSite -> DefinitionSite
$cmin :: DefinitionSite -> DefinitionSite -> DefinitionSite
min :: DefinitionSite -> DefinitionSite -> DefinitionSite
Ord, Int -> DefinitionSite -> ShowS
[DefinitionSite] -> ShowS
DefinitionSite -> [Char]
(Int -> DefinitionSite -> ShowS)
-> (DefinitionSite -> [Char])
-> ([DefinitionSite] -> ShowS)
-> Show DefinitionSite
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefinitionSite -> ShowS
showsPrec :: Int -> DefinitionSite -> ShowS
$cshow :: DefinitionSite -> [Char]
show :: DefinitionSite -> [Char]
$cshowList :: [DefinitionSite] -> ShowS
showList :: [DefinitionSite] -> ShowS
Show)

instance FromJSON DefinitionSite where
  parseJSON :: Value -> Parser DefinitionSite
parseJSON = [Char]
-> (Object -> Parser DefinitionSite)
-> Value
-> Parser DefinitionSite
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"DefinitionSite" ((Object -> Parser DefinitionSite)
 -> Value -> Parser DefinitionSite)
-> (Object -> Parser DefinitionSite)
-> Value
-> Parser DefinitionSite
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    Text -> AgdaIndex -> DefinitionSite
DefinitionSite (Text -> AgdaIndex -> DefinitionSite)
-> Parser Text -> Parser (AgdaIndex -> DefinitionSite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"filepath" Parser (AgdaIndex -> DefinitionSite)
-> Parser AgdaIndex -> Parser DefinitionSite
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser AgdaIndex
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"position"

data Highlight = Highlight
  { Highlight -> [Text]
hl_atoms          :: [Text]
  , Highlight -> Maybe DefinitionSite
hl_definitionSite :: Maybe DefinitionSite
  , Highlight -> AgdaIndex
hl_start          :: AgdaIndex
  , Highlight -> AgdaIndex
hl_end            :: AgdaIndex
  }
  deriving (Highlight -> Highlight -> Bool
(Highlight -> Highlight -> Bool)
-> (Highlight -> Highlight -> Bool) -> Eq Highlight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Highlight -> Highlight -> Bool
== :: Highlight -> Highlight -> Bool
$c/= :: Highlight -> Highlight -> Bool
/= :: Highlight -> Highlight -> Bool
Eq, Eq Highlight
Eq Highlight =>
(Highlight -> Highlight -> Ordering)
-> (Highlight -> Highlight -> Bool)
-> (Highlight -> Highlight -> Bool)
-> (Highlight -> Highlight -> Bool)
-> (Highlight -> Highlight -> Bool)
-> (Highlight -> Highlight -> Highlight)
-> (Highlight -> Highlight -> Highlight)
-> Ord Highlight
Highlight -> Highlight -> Bool
Highlight -> Highlight -> Ordering
Highlight -> Highlight -> Highlight
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Highlight -> Highlight -> Ordering
compare :: Highlight -> Highlight -> Ordering
$c< :: Highlight -> Highlight -> Bool
< :: Highlight -> Highlight -> Bool
$c<= :: Highlight -> Highlight -> Bool
<= :: Highlight -> Highlight -> Bool
$c> :: Highlight -> Highlight -> Bool
> :: Highlight -> Highlight -> Bool
$c>= :: Highlight -> Highlight -> Bool
>= :: Highlight -> Highlight -> Bool
$cmax :: Highlight -> Highlight -> Highlight
max :: Highlight -> Highlight -> Highlight
$cmin :: Highlight -> Highlight -> Highlight
min :: Highlight -> Highlight -> Highlight
Ord, Int -> Highlight -> ShowS
[Highlight] -> ShowS
Highlight -> [Char]
(Int -> Highlight -> ShowS)
-> (Highlight -> [Char])
-> ([Highlight] -> ShowS)
-> Show Highlight
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Highlight -> ShowS
showsPrec :: Int -> Highlight -> ShowS
$cshow :: Highlight -> [Char]
show :: Highlight -> [Char]
$cshowList :: [Highlight] -> ShowS
showList :: [Highlight] -> ShowS
Show)

instance FromJSON Highlight where
  parseJSON :: Value -> Parser Highlight
parseJSON = [Char] -> (Object -> Parser Highlight) -> Value -> Parser Highlight
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Highlight" ((Object -> Parser Highlight) -> Value -> Parser Highlight)
-> (Object -> Parser Highlight) -> Value -> Parser Highlight
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    [Text]
-> Maybe DefinitionSite -> AgdaIndex -> AgdaIndex -> Highlight
Highlight
      ([Text]
 -> Maybe DefinitionSite -> AgdaIndex -> AgdaIndex -> Highlight)
-> Parser [Text]
-> Parser
     (Maybe DefinitionSite -> AgdaIndex -> AgdaIndex -> Highlight)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser [Text]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"atoms"
      Parser
  (Maybe DefinitionSite -> AgdaIndex -> AgdaIndex -> Highlight)
-> Parser (Maybe DefinitionSite)
-> Parser (AgdaIndex -> AgdaIndex -> Highlight)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser (Maybe DefinitionSite)
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"definitionSite"
      Parser (AgdaIndex -> AgdaIndex -> Highlight)
-> Parser AgdaIndex -> Parser (AgdaIndex -> Highlight)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([AgdaIndex] -> AgdaIndex)
-> Parser [AgdaIndex] -> Parser AgdaIndex
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([AgdaIndex] -> Int -> AgdaIndex
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Object
obj Object -> Key -> Parser [AgdaIndex]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"range")
      Parser (AgdaIndex -> Highlight)
-> Parser AgdaIndex -> Parser Highlight
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([AgdaIndex] -> AgdaIndex)
-> Parser [AgdaIndex] -> Parser AgdaIndex
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([AgdaIndex] -> Int -> AgdaIndex
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) (Object
obj Object -> Key -> Parser [AgdaIndex]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"range")

data MakeCase
  = RegularCase MakeCaseVariant [Text] (InteractionPoint Identity)
  deriving (MakeCase -> MakeCase -> Bool
(MakeCase -> MakeCase -> Bool)
-> (MakeCase -> MakeCase -> Bool) -> Eq MakeCase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MakeCase -> MakeCase -> Bool
== :: MakeCase -> MakeCase -> Bool
$c/= :: MakeCase -> MakeCase -> Bool
/= :: MakeCase -> MakeCase -> Bool
Eq, Eq MakeCase
Eq MakeCase =>
(MakeCase -> MakeCase -> Ordering)
-> (MakeCase -> MakeCase -> Bool)
-> (MakeCase -> MakeCase -> Bool)
-> (MakeCase -> MakeCase -> Bool)
-> (MakeCase -> MakeCase -> Bool)
-> (MakeCase -> MakeCase -> MakeCase)
-> (MakeCase -> MakeCase -> MakeCase)
-> Ord MakeCase
MakeCase -> MakeCase -> Bool
MakeCase -> MakeCase -> Ordering
MakeCase -> MakeCase -> MakeCase
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MakeCase -> MakeCase -> Ordering
compare :: MakeCase -> MakeCase -> Ordering
$c< :: MakeCase -> MakeCase -> Bool
< :: MakeCase -> MakeCase -> Bool
$c<= :: MakeCase -> MakeCase -> Bool
<= :: MakeCase -> MakeCase -> Bool
$c> :: MakeCase -> MakeCase -> Bool
> :: MakeCase -> MakeCase -> Bool
$c>= :: MakeCase -> MakeCase -> Bool
>= :: MakeCase -> MakeCase -> Bool
$cmax :: MakeCase -> MakeCase -> MakeCase
max :: MakeCase -> MakeCase -> MakeCase
$cmin :: MakeCase -> MakeCase -> MakeCase
min :: MakeCase -> MakeCase -> MakeCase
Ord, Int -> MakeCase -> ShowS
[MakeCase] -> ShowS
MakeCase -> [Char]
(Int -> MakeCase -> ShowS)
-> (MakeCase -> [Char]) -> ([MakeCase] -> ShowS) -> Show MakeCase
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MakeCase -> ShowS
showsPrec :: Int -> MakeCase -> ShowS
$cshow :: MakeCase -> [Char]
show :: MakeCase -> [Char]
$cshowList :: [MakeCase] -> ShowS
showList :: [MakeCase] -> ShowS
Show, (forall x. MakeCase -> Rep MakeCase x)
-> (forall x. Rep MakeCase x -> MakeCase) -> Generic MakeCase
forall x. Rep MakeCase x -> MakeCase
forall x. MakeCase -> Rep MakeCase x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MakeCase -> Rep MakeCase x
from :: forall x. MakeCase -> Rep MakeCase x
$cto :: forall x. Rep MakeCase x -> MakeCase
to :: forall x. Rep MakeCase x -> MakeCase
Generic)

data MakeCaseVariant = Function | ExtendedLambda
  deriving stock (MakeCaseVariant -> MakeCaseVariant -> Bool
(MakeCaseVariant -> MakeCaseVariant -> Bool)
-> (MakeCaseVariant -> MakeCaseVariant -> Bool)
-> Eq MakeCaseVariant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MakeCaseVariant -> MakeCaseVariant -> Bool
== :: MakeCaseVariant -> MakeCaseVariant -> Bool
$c/= :: MakeCaseVariant -> MakeCaseVariant -> Bool
/= :: MakeCaseVariant -> MakeCaseVariant -> Bool
Eq, Eq MakeCaseVariant
Eq MakeCaseVariant =>
(MakeCaseVariant -> MakeCaseVariant -> Ordering)
-> (MakeCaseVariant -> MakeCaseVariant -> Bool)
-> (MakeCaseVariant -> MakeCaseVariant -> Bool)
-> (MakeCaseVariant -> MakeCaseVariant -> Bool)
-> (MakeCaseVariant -> MakeCaseVariant -> Bool)
-> (MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant)
-> (MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant)
-> Ord MakeCaseVariant
MakeCaseVariant -> MakeCaseVariant -> Bool
MakeCaseVariant -> MakeCaseVariant -> Ordering
MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MakeCaseVariant -> MakeCaseVariant -> Ordering
compare :: MakeCaseVariant -> MakeCaseVariant -> Ordering
$c< :: MakeCaseVariant -> MakeCaseVariant -> Bool
< :: MakeCaseVariant -> MakeCaseVariant -> Bool
$c<= :: MakeCaseVariant -> MakeCaseVariant -> Bool
<= :: MakeCaseVariant -> MakeCaseVariant -> Bool
$c> :: MakeCaseVariant -> MakeCaseVariant -> Bool
> :: MakeCaseVariant -> MakeCaseVariant -> Bool
$c>= :: MakeCaseVariant -> MakeCaseVariant -> Bool
>= :: MakeCaseVariant -> MakeCaseVariant -> Bool
$cmax :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant
max :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant
$cmin :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant
min :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant
Ord, Int -> MakeCaseVariant -> ShowS
[MakeCaseVariant] -> ShowS
MakeCaseVariant -> [Char]
(Int -> MakeCaseVariant -> ShowS)
-> (MakeCaseVariant -> [Char])
-> ([MakeCaseVariant] -> ShowS)
-> Show MakeCaseVariant
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MakeCaseVariant -> ShowS
showsPrec :: Int -> MakeCaseVariant -> ShowS
$cshow :: MakeCaseVariant -> [Char]
show :: MakeCaseVariant -> [Char]
$cshowList :: [MakeCaseVariant] -> ShowS
showList :: [MakeCaseVariant] -> ShowS
Show, (forall x. MakeCaseVariant -> Rep MakeCaseVariant x)
-> (forall x. Rep MakeCaseVariant x -> MakeCaseVariant)
-> Generic MakeCaseVariant
forall x. Rep MakeCaseVariant x -> MakeCaseVariant
forall x. MakeCaseVariant -> Rep MakeCaseVariant x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MakeCaseVariant -> Rep MakeCaseVariant x
from :: forall x. MakeCaseVariant -> Rep MakeCaseVariant x
$cto :: forall x. Rep MakeCaseVariant x -> MakeCaseVariant
to :: forall x. Rep MakeCaseVariant x -> MakeCaseVariant
Generic)
  deriving anyclass (Maybe MakeCaseVariant
Value -> Parser [MakeCaseVariant]
Value -> Parser MakeCaseVariant
(Value -> Parser MakeCaseVariant)
-> (Value -> Parser [MakeCaseVariant])
-> Maybe MakeCaseVariant
-> FromJSON MakeCaseVariant
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser MakeCaseVariant
parseJSON :: Value -> Parser MakeCaseVariant
$cparseJSONList :: Value -> Parser [MakeCaseVariant]
parseJSONList :: Value -> Parser [MakeCaseVariant]
$comittedField :: Maybe MakeCaseVariant
omittedField :: Maybe MakeCaseVariant
FromJSON)

instance FromJSON MakeCase where
  parseJSON :: Value -> Parser MakeCase
parseJSON = [Char] -> (Object -> Parser MakeCase) -> Value -> Parser MakeCase
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"MakeCase" ((Object -> Parser MakeCase) -> Value -> Parser MakeCase)
-> (Object -> Parser MakeCase) -> Value -> Parser MakeCase
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    MakeCaseVariant -> [Text] -> InteractionPoint Identity -> MakeCase
RegularCase (MakeCaseVariant
 -> [Text] -> InteractionPoint Identity -> MakeCase)
-> Parser MakeCaseVariant
-> Parser ([Text] -> InteractionPoint Identity -> MakeCase)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser MakeCaseVariant
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"variant" Parser ([Text] -> InteractionPoint Identity -> MakeCase)
-> Parser [Text] -> Parser (InteractionPoint Identity -> MakeCase)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser [Text]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"clauses" Parser (InteractionPoint Identity -> MakeCase)
-> Parser (InteractionPoint Identity) -> Parser MakeCase
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser (InteractionPoint Identity)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"interactionPoint"


data Solution = Solution
  { Solution -> InteractionId
s_ip :: InteractionId
  , Solution -> Text
s_expression :: Text
  }
  deriving (Solution -> Solution -> Bool
(Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool) -> Eq Solution
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Solution -> Solution -> Bool
== :: Solution -> Solution -> Bool
$c/= :: Solution -> Solution -> Bool
/= :: Solution -> Solution -> Bool
Eq, Eq Solution
Eq Solution =>
(Solution -> Solution -> Ordering)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Solution)
-> (Solution -> Solution -> Solution)
-> Ord Solution
Solution -> Solution -> Bool
Solution -> Solution -> Ordering
Solution -> Solution -> Solution
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Solution -> Solution -> Ordering
compare :: Solution -> Solution -> Ordering
$c< :: Solution -> Solution -> Bool
< :: Solution -> Solution -> Bool
$c<= :: Solution -> Solution -> Bool
<= :: Solution -> Solution -> Bool
$c> :: Solution -> Solution -> Bool
> :: Solution -> Solution -> Bool
$c>= :: Solution -> Solution -> Bool
>= :: Solution -> Solution -> Bool
$cmax :: Solution -> Solution -> Solution
max :: Solution -> Solution -> Solution
$cmin :: Solution -> Solution -> Solution
min :: Solution -> Solution -> Solution
Ord, Int -> Solution -> ShowS
[Solution] -> ShowS
Solution -> [Char]
(Int -> Solution -> ShowS)
-> (Solution -> [Char]) -> ([Solution] -> ShowS) -> Show Solution
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Solution -> ShowS
showsPrec :: Int -> Solution -> ShowS
$cshow :: Solution -> [Char]
show :: Solution -> [Char]
$cshowList :: [Solution] -> ShowS
showList :: [Solution] -> ShowS
Show)

data InteractionPoint f = InteractionPoint
  { forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id :: InteractionId
  , forall (f :: * -> *). InteractionPoint f -> f AgdaInterval
ip_intervalM :: f AgdaInterval
  } deriving (forall x. InteractionPoint f -> Rep (InteractionPoint f) x)
-> (forall x. Rep (InteractionPoint f) x -> InteractionPoint f)
-> Generic (InteractionPoint f)
forall x. Rep (InteractionPoint f) x -> InteractionPoint f
forall x. InteractionPoint f -> Rep (InteractionPoint f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: * -> *) x.
Rep (InteractionPoint f) x -> InteractionPoint f
forall (f :: * -> *) x.
InteractionPoint f -> Rep (InteractionPoint f) x
$cfrom :: forall (f :: * -> *) x.
InteractionPoint f -> Rep (InteractionPoint f) x
from :: forall x. InteractionPoint f -> Rep (InteractionPoint f) x
$cto :: forall (f :: * -> *) x.
Rep (InteractionPoint f) x -> InteractionPoint f
to :: forall x. Rep (InteractionPoint f) x -> InteractionPoint f
Generic

deriving instance Eq (f AgdaInterval) => Eq (InteractionPoint f)
deriving instance Ord (f AgdaInterval) => Ord (InteractionPoint f)
deriving instance Show (f AgdaInterval) => Show (InteractionPoint f)

ip_interval' :: InteractionPoint Identity -> AgdaInterval
ip_interval' :: InteractionPoint Identity -> AgdaInterval
ip_interval' (InteractionPoint InteractionId
_ (Identity AgdaInterval
i)) = AgdaInterval
i

sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity)
sequenceInteractionPoint :: forall (f :: * -> *).
Applicative f =>
InteractionPoint f -> f (InteractionPoint Identity)
sequenceInteractionPoint (InteractionPoint InteractionId
n f AgdaInterval
f) = (Identity AgdaInterval -> InteractionPoint Identity)
-> f (Identity AgdaInterval -> InteractionPoint Identity)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InteractionId -> Identity AgdaInterval -> InteractionPoint Identity
forall (f :: * -> *).
InteractionId -> f AgdaInterval -> InteractionPoint f
InteractionPoint InteractionId
n) f (Identity AgdaInterval -> InteractionPoint Identity)
-> f (Identity AgdaInterval) -> f (InteractionPoint Identity)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (AgdaInterval -> Identity AgdaInterval)
-> f AgdaInterval -> f (Identity AgdaInterval)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AgdaInterval -> Identity AgdaInterval
forall a. a -> Identity a
Identity f AgdaInterval
f


data NamedPoint = NamedPoint
  { NamedPoint -> Text
np_name :: Text
  , NamedPoint -> Maybe AgdaInterval
np_interval :: Maybe AgdaInterval
  }
  deriving (NamedPoint -> NamedPoint -> Bool
(NamedPoint -> NamedPoint -> Bool)
-> (NamedPoint -> NamedPoint -> Bool) -> Eq NamedPoint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NamedPoint -> NamedPoint -> Bool
== :: NamedPoint -> NamedPoint -> Bool
$c/= :: NamedPoint -> NamedPoint -> Bool
/= :: NamedPoint -> NamedPoint -> Bool
Eq, Eq NamedPoint
Eq NamedPoint =>
(NamedPoint -> NamedPoint -> Ordering)
-> (NamedPoint -> NamedPoint -> Bool)
-> (NamedPoint -> NamedPoint -> Bool)
-> (NamedPoint -> NamedPoint -> Bool)
-> (NamedPoint -> NamedPoint -> Bool)
-> (NamedPoint -> NamedPoint -> NamedPoint)
-> (NamedPoint -> NamedPoint -> NamedPoint)
-> Ord NamedPoint
NamedPoint -> NamedPoint -> Bool
NamedPoint -> NamedPoint -> Ordering
NamedPoint -> NamedPoint -> NamedPoint
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: NamedPoint -> NamedPoint -> Ordering
compare :: NamedPoint -> NamedPoint -> Ordering
$c< :: NamedPoint -> NamedPoint -> Bool
< :: NamedPoint -> NamedPoint -> Bool
$c<= :: NamedPoint -> NamedPoint -> Bool
<= :: NamedPoint -> NamedPoint -> Bool
$c> :: NamedPoint -> NamedPoint -> Bool
> :: NamedPoint -> NamedPoint -> Bool
$c>= :: NamedPoint -> NamedPoint -> Bool
>= :: NamedPoint -> NamedPoint -> Bool
$cmax :: NamedPoint -> NamedPoint -> NamedPoint
max :: NamedPoint -> NamedPoint -> NamedPoint
$cmin :: NamedPoint -> NamedPoint -> NamedPoint
min :: NamedPoint -> NamedPoint -> NamedPoint
Ord, Int -> NamedPoint -> ShowS
[NamedPoint] -> ShowS
NamedPoint -> [Char]
(Int -> NamedPoint -> ShowS)
-> (NamedPoint -> [Char])
-> ([NamedPoint] -> ShowS)
-> Show NamedPoint
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NamedPoint -> ShowS
showsPrec :: Int -> NamedPoint -> ShowS
$cshow :: NamedPoint -> [Char]
show :: NamedPoint -> [Char]
$cshowList :: [NamedPoint] -> ShowS
showList :: [NamedPoint] -> ShowS
Show)

instance FromJSON AgdaInterval where
  parseJSON :: Value -> Parser AgdaInterval
parseJSON = [Char]
-> (Object -> Parser AgdaInterval) -> Value -> Parser AgdaInterval
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"IntervalWithoutFile" ((Object -> Parser AgdaInterval) -> Value -> Parser AgdaInterval)
-> (Object -> Parser AgdaInterval) -> Value -> Parser AgdaInterval
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    AgdaPos' -> AgdaPos' -> AgdaInterval
mkInterval (AgdaPos' -> AgdaPos' -> AgdaInterval)
-> Parser AgdaPos' -> Parser (AgdaPos' -> AgdaInterval)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser AgdaPos'
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"start" Parser (AgdaPos' -> AgdaInterval)
-> Parser AgdaPos' -> Parser AgdaInterval
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser AgdaPos'
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"end"
    where
      mkInterval :: AgdaPos' -> AgdaPos' -> AgdaInterval
mkInterval (AgdaPos Pos 'CodePoint 'OneIndexed 'OneIndexed
p) (AgdaPos Pos 'CodePoint 'OneIndexed 'OneIndexed
q) = Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed -> AgdaInterval
forall p. p -> p -> Interval p
Interval Pos 'CodePoint 'OneIndexed 'OneIndexed
p Pos 'CodePoint 'OneIndexed 'OneIndexed
q

newtype AgdaPos' = AgdaPos AgdaPos

instance FromJSON AgdaPos' where
  parseJSON :: Value -> Parser AgdaPos'
parseJSON = [Char] -> (Object -> Parser AgdaPos') -> Value -> Parser AgdaPos'
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Position" ((Object -> Parser AgdaPos') -> Value -> Parser AgdaPos')
-> (Object -> Parser AgdaPos') -> Value -> Parser AgdaPos'
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Pos 'CodePoint 'OneIndexed 'OneIndexed -> AgdaPos'
AgdaPos (Pos 'CodePoint 'OneIndexed 'OneIndexed -> AgdaPos')
-> Parser (Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Parser AgdaPos'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Index 'Line 'OneIndexed
-> AgdaIndex -> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos (Index 'Line 'OneIndexed
 -> AgdaIndex -> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Parser (Index 'Line 'OneIndexed)
-> Parser (AgdaIndex -> Pos 'CodePoint 'OneIndexed 'OneIndexed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser (Index 'Line 'OneIndexed)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"line" Parser (AgdaIndex -> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Parser AgdaIndex
-> Parser (Pos 'CodePoint 'OneIndexed 'OneIndexed)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser AgdaIndex
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"col")

instance FromJSON (InteractionPoint Maybe) where
  parseJSON :: Value -> Parser (InteractionPoint Maybe)
parseJSON = [Char]
-> (Object -> Parser (InteractionPoint Maybe))
-> Value
-> Parser (InteractionPoint Maybe)
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"InteractionPoint" ((Object -> Parser (InteractionPoint Maybe))
 -> Value -> Parser (InteractionPoint Maybe))
-> (Object -> Parser (InteractionPoint Maybe))
-> Value
-> Parser (InteractionPoint Maybe)
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    InteractionId -> Maybe AgdaInterval -> InteractionPoint Maybe
forall (f :: * -> *).
InteractionId -> f AgdaInterval -> InteractionPoint f
InteractionPoint (InteractionId -> Maybe AgdaInterval -> InteractionPoint Maybe)
-> Parser InteractionId
-> Parser (Maybe AgdaInterval -> InteractionPoint Maybe)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser InteractionId
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"id" Parser (Maybe AgdaInterval -> InteractionPoint Maybe)
-> Parser (Maybe AgdaInterval) -> Parser (InteractionPoint Maybe)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([AgdaInterval] -> Maybe AgdaInterval)
-> Parser [AgdaInterval] -> Parser (Maybe AgdaInterval)
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [AgdaInterval] -> Maybe AgdaInterval
forall a. [a] -> Maybe a
listToMaybe (Object
obj Object -> Key -> Parser [AgdaInterval]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"range")

instance FromJSON (InteractionPoint Identity) where
  parseJSON :: Value -> Parser (InteractionPoint Identity)
parseJSON = [Char]
-> (Object -> Parser (InteractionPoint Identity))
-> Value
-> Parser (InteractionPoint Identity)
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"InteractionPoint" ((Object -> Parser (InteractionPoint Identity))
 -> Value -> Parser (InteractionPoint Identity))
-> (Object -> Parser (InteractionPoint Identity))
-> Value
-> Parser (InteractionPoint Identity)
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    InteractionId -> Identity AgdaInterval -> InteractionPoint Identity
forall (f :: * -> *).
InteractionId -> f AgdaInterval -> InteractionPoint f
InteractionPoint (InteractionId
 -> Identity AgdaInterval -> InteractionPoint Identity)
-> Parser InteractionId
-> Parser (Identity AgdaInterval -> InteractionPoint Identity)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser InteractionId
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"id" Parser (Identity AgdaInterval -> InteractionPoint Identity)
-> Parser (Identity AgdaInterval)
-> Parser (InteractionPoint Identity)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Identity AgdaInterval] -> Identity AgdaInterval)
-> Parser [Identity AgdaInterval] -> Parser (Identity AgdaInterval)
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Identity AgdaInterval] -> Identity AgdaInterval
forall a. HasCallStack => [a] -> a
head (Object
obj Object -> Key -> Parser [Identity AgdaInterval]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"range")

instance FromJSON (InteractionPoint (Const ())) where
  parseJSON :: Value -> Parser (InteractionPoint (Const ()))
parseJSON = [Char]
-> (Object -> Parser (InteractionPoint (Const ())))
-> Value
-> Parser (InteractionPoint (Const ()))
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"InteractionPoint" ((Object -> Parser (InteractionPoint (Const ())))
 -> Value -> Parser (InteractionPoint (Const ())))
-> (Object -> Parser (InteractionPoint (Const ())))
-> Value
-> Parser (InteractionPoint (Const ()))
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    InteractionId
-> Const () AgdaInterval -> InteractionPoint (Const ())
forall (f :: * -> *).
InteractionId -> f AgdaInterval -> InteractionPoint f
InteractionPoint (InteractionId
 -> Const () AgdaInterval -> InteractionPoint (Const ()))
-> Parser InteractionId
-> Parser (Const () AgdaInterval -> InteractionPoint (Const ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser InteractionId
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"id" Parser (Const () AgdaInterval -> InteractionPoint (Const ()))
-> Parser (Const () AgdaInterval)
-> Parser (InteractionPoint (Const ()))
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Const () AgdaInterval -> Parser (Const () AgdaInterval)
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Const () AgdaInterval
forall {k} a (b :: k). a -> Const a b
Const ())

instance FromJSON NamedPoint where
  parseJSON :: Value -> Parser NamedPoint
parseJSON = [Char]
-> (Object -> Parser NamedPoint) -> Value -> Parser NamedPoint
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"InteractionPoint" ((Object -> Parser NamedPoint) -> Value -> Parser NamedPoint)
-> (Object -> Parser NamedPoint) -> Value -> Parser NamedPoint
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Text -> Maybe AgdaInterval -> NamedPoint
NamedPoint (Text -> Maybe AgdaInterval -> NamedPoint)
-> Parser Text -> Parser (Maybe AgdaInterval -> NamedPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"name" Parser (Maybe AgdaInterval -> NamedPoint)
-> Parser (Maybe AgdaInterval) -> Parser NamedPoint
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([AgdaInterval] -> Maybe AgdaInterval)
-> Parser [AgdaInterval] -> Parser (Maybe AgdaInterval)
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [AgdaInterval] -> Maybe AgdaInterval
forall a. [a] -> Maybe a
listToMaybe (Object
obj Object -> Key -> Parser [AgdaInterval]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"range")

instance FromJSON Solution where
  parseJSON :: Value -> Parser Solution
parseJSON = [Char] -> (Object -> Parser Solution) -> Value -> Parser Solution
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Solution" ((Object -> Parser Solution) -> Value -> Parser Solution)
-> (Object -> Parser Solution) -> Value -> Parser Solution
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    InteractionId -> Text -> Solution
Solution (InteractionId -> Text -> Solution)
-> Parser InteractionId -> Parser (Text -> Solution)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser InteractionId
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"interactionPoint" Parser (Text -> Solution) -> Parser Text -> Parser Solution
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expression"

data GoalInfo a = GoalInfo
  { forall a. GoalInfo a -> a
gi_ip :: a
  , forall a. GoalInfo a -> Type
gi_type :: Type
  }
  deriving (GoalInfo a -> GoalInfo a -> Bool
(GoalInfo a -> GoalInfo a -> Bool)
-> (GoalInfo a -> GoalInfo a -> Bool) -> Eq (GoalInfo a)
forall a. Eq a => GoalInfo a -> GoalInfo a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => GoalInfo a -> GoalInfo a -> Bool
== :: GoalInfo a -> GoalInfo a -> Bool
$c/= :: forall a. Eq a => GoalInfo a -> GoalInfo a -> Bool
/= :: GoalInfo a -> GoalInfo a -> Bool
Eq, Eq (GoalInfo a)
Eq (GoalInfo a) =>
(GoalInfo a -> GoalInfo a -> Ordering)
-> (GoalInfo a -> GoalInfo a -> Bool)
-> (GoalInfo a -> GoalInfo a -> Bool)
-> (GoalInfo a -> GoalInfo a -> Bool)
-> (GoalInfo a -> GoalInfo a -> Bool)
-> (GoalInfo a -> GoalInfo a -> GoalInfo a)
-> (GoalInfo a -> GoalInfo a -> GoalInfo a)
-> Ord (GoalInfo a)
GoalInfo a -> GoalInfo a -> Bool
GoalInfo a -> GoalInfo a -> Ordering
GoalInfo a -> GoalInfo a -> GoalInfo a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (GoalInfo a)
forall a. Ord a => GoalInfo a -> GoalInfo a -> Bool
forall a. Ord a => GoalInfo a -> GoalInfo a -> Ordering
forall a. Ord a => GoalInfo a -> GoalInfo a -> GoalInfo a
$ccompare :: forall a. Ord a => GoalInfo a -> GoalInfo a -> Ordering
compare :: GoalInfo a -> GoalInfo a -> Ordering
$c< :: forall a. Ord a => GoalInfo a -> GoalInfo a -> Bool
< :: GoalInfo a -> GoalInfo a -> Bool
$c<= :: forall a. Ord a => GoalInfo a -> GoalInfo a -> Bool
<= :: GoalInfo a -> GoalInfo a -> Bool
$c> :: forall a. Ord a => GoalInfo a -> GoalInfo a -> Bool
> :: GoalInfo a -> GoalInfo a -> Bool
$c>= :: forall a. Ord a => GoalInfo a -> GoalInfo a -> Bool
>= :: GoalInfo a -> GoalInfo a -> Bool
$cmax :: forall a. Ord a => GoalInfo a -> GoalInfo a -> GoalInfo a
max :: GoalInfo a -> GoalInfo a -> GoalInfo a
$cmin :: forall a. Ord a => GoalInfo a -> GoalInfo a -> GoalInfo a
min :: GoalInfo a -> GoalInfo a -> GoalInfo a
Ord, Int -> GoalInfo a -> ShowS
[GoalInfo a] -> ShowS
GoalInfo a -> [Char]
(Int -> GoalInfo a -> ShowS)
-> (GoalInfo a -> [Char])
-> ([GoalInfo a] -> ShowS)
-> Show (GoalInfo a)
forall a. Show a => Int -> GoalInfo a -> ShowS
forall a. Show a => [GoalInfo a] -> ShowS
forall a. Show a => GoalInfo a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> GoalInfo a -> ShowS
showsPrec :: Int -> GoalInfo a -> ShowS
$cshow :: forall a. Show a => GoalInfo a -> [Char]
show :: GoalInfo a -> [Char]
$cshowList :: forall a. Show a => [GoalInfo a] -> ShowS
showList :: [GoalInfo a] -> ShowS
Show, (forall a b. (a -> b) -> GoalInfo a -> GoalInfo b)
-> (forall a b. a -> GoalInfo b -> GoalInfo a) -> Functor GoalInfo
forall a b. a -> GoalInfo b -> GoalInfo a
forall a b. (a -> b) -> GoalInfo a -> GoalInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GoalInfo a -> GoalInfo b
fmap :: forall a b. (a -> b) -> GoalInfo a -> GoalInfo b
$c<$ :: forall a b. a -> GoalInfo b -> GoalInfo a
<$ :: forall a b. a -> GoalInfo b -> GoalInfo a
Functor)

instance FromJSON a => FromJSON (GoalInfo a) where
  parseJSON :: Value -> Parser (GoalInfo a)
parseJSON = [Char]
-> (Object -> Parser (GoalInfo a)) -> Value -> Parser (GoalInfo a)
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"GoalInfo" ((Object -> Parser (GoalInfo a)) -> Value -> Parser (GoalInfo a))
-> (Object -> Parser (GoalInfo a)) -> Value -> Parser (GoalInfo a)
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    (Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"kind") Parser Text -> (Text -> Parser (GoalInfo a)) -> Parser (GoalInfo a)
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Text
"OfType" -> a -> Type -> GoalInfo a
forall a. a -> Type -> GoalInfo a
GoalInfo (a -> Type -> GoalInfo a)
-> Parser a -> Parser (Type -> GoalInfo a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser a
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintObj" Parser (Type -> GoalInfo a) -> Parser Type -> Parser (GoalInfo a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Type
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"type"
      Text
"JustSort" -> a -> Type -> GoalInfo a
forall a. a -> Type -> GoalInfo a
GoalInfo (a -> Type -> GoalInfo a)
-> Parser a -> Parser (Type -> GoalInfo a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser a
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintObj" Parser (Type -> GoalInfo a) -> Parser Type -> Parser (GoalInfo a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Parser Type
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Type
Type Text
"Sort")
      (Text
_ :: Text) -> Parser (GoalInfo a)
forall a. Parser a
forall (f :: * -> *) a. Alternative f => f a
empty

newtype Type = Type Text
  deriving newtype (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
/= :: Type -> Type -> Bool
Eq, Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Type -> Type -> Ordering
compare :: Type -> Type -> Ordering
$c< :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
>= :: Type -> Type -> Bool
$cmax :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
min :: Type -> Type -> Type
Ord, Int -> Type -> ShowS
[Type] -> ShowS
Type -> [Char]
(Int -> Type -> ShowS)
-> (Type -> [Char]) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Type -> ShowS
showsPrec :: Int -> Type -> ShowS
$cshow :: Type -> [Char]
show :: Type -> [Char]
$cshowList :: [Type] -> ShowS
showList :: [Type] -> ShowS
Show, Maybe Type
Value -> Parser [Type]
Value -> Parser Type
(Value -> Parser Type)
-> (Value -> Parser [Type]) -> Maybe Type -> FromJSON Type
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser Type
parseJSON :: Value -> Parser Type
$cparseJSONList :: Value -> Parser [Type]
parseJSONList :: Value -> Parser [Type]
$comittedField :: Maybe Type
omittedField :: Maybe Type
FromJSON)

data InScope = InScope
  { InScope -> Text
is_refied_name :: Text
  , InScope -> Text
is_original_name :: Text
  , InScope -> Bool
is_in_scope :: Bool
  , InScope -> Type
is_type :: Type
  }
  deriving (InScope -> InScope -> Bool
(InScope -> InScope -> Bool)
-> (InScope -> InScope -> Bool) -> Eq InScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InScope -> InScope -> Bool
== :: InScope -> InScope -> Bool
$c/= :: InScope -> InScope -> Bool
/= :: InScope -> InScope -> Bool
Eq, Eq InScope
Eq InScope =>
(InScope -> InScope -> Ordering)
-> (InScope -> InScope -> Bool)
-> (InScope -> InScope -> Bool)
-> (InScope -> InScope -> Bool)
-> (InScope -> InScope -> Bool)
-> (InScope -> InScope -> InScope)
-> (InScope -> InScope -> InScope)
-> Ord InScope
InScope -> InScope -> Bool
InScope -> InScope -> Ordering
InScope -> InScope -> InScope
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InScope -> InScope -> Ordering
compare :: InScope -> InScope -> Ordering
$c< :: InScope -> InScope -> Bool
< :: InScope -> InScope -> Bool
$c<= :: InScope -> InScope -> Bool
<= :: InScope -> InScope -> Bool
$c> :: InScope -> InScope -> Bool
> :: InScope -> InScope -> Bool
$c>= :: InScope -> InScope -> Bool
>= :: InScope -> InScope -> Bool
$cmax :: InScope -> InScope -> InScope
max :: InScope -> InScope -> InScope
$cmin :: InScope -> InScope -> InScope
min :: InScope -> InScope -> InScope
Ord, Int -> InScope -> ShowS
[InScope] -> ShowS
InScope -> [Char]
(Int -> InScope -> ShowS)
-> (InScope -> [Char]) -> ([InScope] -> ShowS) -> Show InScope
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InScope -> ShowS
showsPrec :: Int -> InScope -> ShowS
$cshow :: InScope -> [Char]
show :: InScope -> [Char]
$cshowList :: [InScope] -> ShowS
showList :: [InScope] -> ShowS
Show)

instance FromJSON InScope where
  parseJSON :: Value -> Parser InScope
parseJSON = [Char] -> (Object -> Parser InScope) -> Value -> Parser InScope
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"InScope" ((Object -> Parser InScope) -> Value -> Parser InScope)
-> (Object -> Parser InScope) -> Value -> Parser InScope
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    Text -> Text -> Bool -> Type -> InScope
InScope (Text -> Text -> Bool -> Type -> InScope)
-> Parser Text -> Parser (Text -> Bool -> Type -> InScope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"reifiedName" Parser (Text -> Bool -> Type -> InScope)
-> Parser Text -> Parser (Bool -> Type -> InScope)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"originalName" Parser (Bool -> Type -> InScope)
-> Parser Bool -> Parser (Type -> InScope)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Bool
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"inScope" Parser (Type -> InScope) -> Parser Type -> Parser InScope
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Type
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"binding"

newtype Message = Message { Message -> Text
getMessage :: Text }
  deriving (Message -> Message -> Bool
(Message -> Message -> Bool)
-> (Message -> Message -> Bool) -> Eq Message
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Message -> Message -> Bool
== :: Message -> Message -> Bool
$c/= :: Message -> Message -> Bool
/= :: Message -> Message -> Bool
Eq, Eq Message
Eq Message =>
(Message -> Message -> Ordering)
-> (Message -> Message -> Bool)
-> (Message -> Message -> Bool)
-> (Message -> Message -> Bool)
-> (Message -> Message -> Bool)
-> (Message -> Message -> Message)
-> (Message -> Message -> Message)
-> Ord Message
Message -> Message -> Bool
Message -> Message -> Ordering
Message -> Message -> Message
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Message -> Message -> Ordering
compare :: Message -> Message -> Ordering
$c< :: Message -> Message -> Bool
< :: Message -> Message -> Bool
$c<= :: Message -> Message -> Bool
<= :: Message -> Message -> Bool
$c> :: Message -> Message -> Bool
> :: Message -> Message -> Bool
$c>= :: Message -> Message -> Bool
>= :: Message -> Message -> Bool
$cmax :: Message -> Message -> Message
max :: Message -> Message -> Message
$cmin :: Message -> Message -> Message
min :: Message -> Message -> Message
Ord, Int -> Message -> ShowS
[Message] -> ShowS
Message -> [Char]
(Int -> Message -> ShowS)
-> (Message -> [Char]) -> ([Message] -> ShowS) -> Show Message
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Message -> ShowS
showsPrec :: Int -> Message -> ShowS
$cshow :: Message -> [Char]
show :: Message -> [Char]
$cshowList :: [Message] -> ShowS
showList :: [Message] -> ShowS
Show)

instance FromJSON Message where
  parseJSON :: Value -> Parser Message
parseJSON = [Char] -> (Object -> Parser Message) -> Value -> Parser Message
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Message" ((Object -> Parser Message) -> Value -> Parser Message)
-> (Object -> Parser Message) -> Value -> Parser Message
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    Text -> Message
Message (Text -> Message) -> Parser Text -> Parser Message
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"message"


data DisplayInfo
  = AllGoalsWarnings
      { DisplayInfo -> [GoalInfo (InteractionPoint Identity)]
di_all_visible :: [GoalInfo (InteractionPoint Identity)]
      , DisplayInfo -> [GoalInfo NamedPoint]
di_all_invisible :: [GoalInfo NamedPoint]
      , DisplayInfo -> [Message]
di_errors :: [Message]
      , DisplayInfo -> [Message]
di_warnings :: [Message]
      }
  | GoalSpecific
      { DisplayInfo -> InteractionPoint Identity
di_ips :: InteractionPoint Identity
      , DisplayInfo -> [InScope]
di_in_scope :: [InScope]
      , DisplayInfo -> Type
di_type :: Type
      , DisplayInfo -> Maybe Type
di_type_aux :: Maybe Type
      , DisplayInfo -> Maybe [Text]
di_boundary :: Maybe [Text]
      , DisplayInfo -> Maybe [Text]
di_output_forms :: Maybe [Text]
      }
  | HelperFunction Text
  | InferredType Type
  | DisplayError Text
  | WhyInScope Text
  | NormalForm Text
  | UnknownDisplayInfo Value
  deriving (DisplayInfo -> DisplayInfo -> Bool
(DisplayInfo -> DisplayInfo -> Bool)
-> (DisplayInfo -> DisplayInfo -> Bool) -> Eq DisplayInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DisplayInfo -> DisplayInfo -> Bool
== :: DisplayInfo -> DisplayInfo -> Bool
$c/= :: DisplayInfo -> DisplayInfo -> Bool
/= :: DisplayInfo -> DisplayInfo -> Bool
Eq, Eq DisplayInfo
Eq DisplayInfo =>
(DisplayInfo -> DisplayInfo -> Ordering)
-> (DisplayInfo -> DisplayInfo -> Bool)
-> (DisplayInfo -> DisplayInfo -> Bool)
-> (DisplayInfo -> DisplayInfo -> Bool)
-> (DisplayInfo -> DisplayInfo -> Bool)
-> (DisplayInfo -> DisplayInfo -> DisplayInfo)
-> (DisplayInfo -> DisplayInfo -> DisplayInfo)
-> Ord DisplayInfo
DisplayInfo -> DisplayInfo -> Bool
DisplayInfo -> DisplayInfo -> Ordering
DisplayInfo -> DisplayInfo -> DisplayInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DisplayInfo -> DisplayInfo -> Ordering
compare :: DisplayInfo -> DisplayInfo -> Ordering
$c< :: DisplayInfo -> DisplayInfo -> Bool
< :: DisplayInfo -> DisplayInfo -> Bool
$c<= :: DisplayInfo -> DisplayInfo -> Bool
<= :: DisplayInfo -> DisplayInfo -> Bool
$c> :: DisplayInfo -> DisplayInfo -> Bool
> :: DisplayInfo -> DisplayInfo -> Bool
$c>= :: DisplayInfo -> DisplayInfo -> Bool
>= :: DisplayInfo -> DisplayInfo -> Bool
$cmax :: DisplayInfo -> DisplayInfo -> DisplayInfo
max :: DisplayInfo -> DisplayInfo -> DisplayInfo
$cmin :: DisplayInfo -> DisplayInfo -> DisplayInfo
min :: DisplayInfo -> DisplayInfo -> DisplayInfo
Ord, Int -> DisplayInfo -> ShowS
[DisplayInfo] -> ShowS
DisplayInfo -> [Char]
(Int -> DisplayInfo -> ShowS)
-> (DisplayInfo -> [Char])
-> ([DisplayInfo] -> ShowS)
-> Show DisplayInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DisplayInfo -> ShowS
showsPrec :: Int -> DisplayInfo -> ShowS
$cshow :: DisplayInfo -> [Char]
show :: DisplayInfo -> [Char]
$cshowList :: [DisplayInfo] -> ShowS
showList :: [DisplayInfo] -> ShowS
Show, (forall x. DisplayInfo -> Rep DisplayInfo x)
-> (forall x. Rep DisplayInfo x -> DisplayInfo)
-> Generic DisplayInfo
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
$cfrom :: forall x. DisplayInfo -> Rep DisplayInfo x
from :: forall x. DisplayInfo -> Rep DisplayInfo x
$cto :: forall x. Rep DisplayInfo x -> DisplayInfo
to :: forall x. Rep DisplayInfo x -> DisplayInfo
Generic)

newtype TypeAux = TypeAux
  { TypeAux -> Type
ta_expr :: Type
  }

instance FromJSON TypeAux where
  parseJSON :: Value -> Parser TypeAux
parseJSON = [Char] -> (Object -> Parser TypeAux) -> Value -> Parser TypeAux
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"TypeAux" ((Object -> Parser TypeAux) -> Value -> Parser TypeAux)
-> (Object -> Parser TypeAux) -> Value -> Parser TypeAux
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    Type -> TypeAux
TypeAux (Type -> TypeAux) -> (Text -> Type) -> Text -> TypeAux
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Type
Type (Text -> TypeAux) -> Parser Text -> Parser TypeAux
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expr"

instance FromJSON DisplayInfo where
  parseJSON :: Value -> Parser DisplayInfo
parseJSON Value
v = ((Object -> Parser DisplayInfo) -> Value -> Parser DisplayInfo)
-> Value -> (Object -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Char]
-> (Object -> Parser DisplayInfo) -> Value -> Parser DisplayInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"DisplayInfo") Value
v ((Object -> Parser DisplayInfo) -> Parser DisplayInfo)
-> (Object -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"kind" Parser Text -> (Text -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Text
"AllGoalsWarnings" ->
        [GoalInfo (InteractionPoint Identity)]
-> [GoalInfo NamedPoint] -> [Message] -> [Message] -> DisplayInfo
AllGoalsWarnings
          ([GoalInfo (InteractionPoint Identity)]
 -> [GoalInfo NamedPoint] -> [Message] -> [Message] -> DisplayInfo)
-> Parser [GoalInfo (InteractionPoint Identity)]
-> Parser
     ([GoalInfo NamedPoint] -> [Message] -> [Message] -> DisplayInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser [GoalInfo (InteractionPoint Identity)]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"visibleGoals"
          Parser
  ([GoalInfo NamedPoint] -> [Message] -> [Message] -> DisplayInfo)
-> Parser [GoalInfo NamedPoint]
-> Parser ([Message] -> [Message] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser [GoalInfo NamedPoint]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"invisibleGoals"
          Parser ([Message] -> [Message] -> DisplayInfo)
-> Parser [Message] -> Parser ([Message] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
obj Object -> Key -> Parser [Message]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"errors"   Parser [Message] -> Parser [Message] -> Parser [Message]
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Message -> [Message]) -> Parser Message -> Parser [Message]
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Message -> [Message]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Object
obj Object -> Key -> Parser Message
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"errors"))
          Parser ([Message] -> DisplayInfo)
-> Parser [Message] -> Parser DisplayInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
obj Object -> Key -> Parser [Message]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"warnings" Parser [Message] -> Parser [Message] -> Parser [Message]
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Message -> [Message]) -> Parser Message -> Parser [Message]
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Message -> [Message]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Object
obj Object -> Key -> Parser Message
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"warnings"))
      Text
"Error" ->
        Object
obj Object -> Key -> Parser Object
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"error" Parser Object
-> (Object -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Object
err ->
          Text -> DisplayInfo
DisplayError (Text -> DisplayInfo) -> Parser Text -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
err Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"message"
      Text
"InferredType" ->
        Type -> DisplayInfo
InferredType (Type -> DisplayInfo) -> Parser Type -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Type
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expr"
      Text
"WhyInScope" ->
        Text -> DisplayInfo
WhyInScope (Text -> DisplayInfo) -> Parser Text -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"message"
      Text
"NormalForm" ->
        Text -> DisplayInfo
NormalForm (Text -> DisplayInfo) -> Parser Text -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expr"
      Text
"GoalSpecific" ->
        (Object
obj Object -> Key -> Parser Object
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"goalInfo") Parser Object
-> (Object -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Object
info ->
          (Object
info Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"kind") Parser Text -> (Text -> Parser DisplayInfo) -> Parser DisplayInfo
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Text
"HelperFunction" ->
              Text -> DisplayInfo
HelperFunction (Text -> DisplayInfo) -> Parser Text -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
info Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"signature"
            Text
"GoalType" ->
              InteractionPoint Identity
-> [InScope]
-> Type
-> Maybe Type
-> Maybe [Text]
-> Maybe [Text]
-> DisplayInfo
GoalSpecific
                (InteractionPoint Identity
 -> [InScope]
 -> Type
 -> Maybe Type
 -> Maybe [Text]
 -> Maybe [Text]
 -> DisplayInfo)
-> Parser (InteractionPoint Identity)
-> Parser
     ([InScope]
      -> Type
      -> Maybe Type
      -> Maybe [Text]
      -> Maybe [Text]
      -> DisplayInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser (InteractionPoint Identity)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"interactionPoint"
                Parser
  ([InScope]
   -> Type
   -> Maybe Type
   -> Maybe [Text]
   -> Maybe [Text]
   -> DisplayInfo)
-> Parser [InScope]
-> Parser
     (Type -> Maybe Type -> Maybe [Text] -> Maybe [Text] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
info Object -> Key -> Parser [InScope]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"entries"
                Parser
  (Type -> Maybe Type -> Maybe [Text] -> Maybe [Text] -> DisplayInfo)
-> Parser Type
-> Parser
     (Maybe Type -> Maybe [Text] -> Maybe [Text] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
info Object -> Key -> Parser Type
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"type"
                Parser (Maybe Type -> Maybe [Text] -> Maybe [Text] -> DisplayInfo)
-> Parser (Maybe Type)
-> Parser (Maybe [Text] -> Maybe [Text] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Maybe TypeAux -> Maybe Type)
-> Parser (Maybe TypeAux) -> Parser (Maybe Type)
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeAux -> Type) -> Maybe TypeAux -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeAux -> Type
ta_expr) (Object
info Object -> Key -> Parser (Maybe TypeAux)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"typeAux") Parser (Maybe Type) -> Parser (Maybe Type) -> Parser (Maybe Type)
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Type -> Parser (Maybe Type)
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing)
                Parser (Maybe [Text] -> Maybe [Text] -> DisplayInfo)
-> Parser (Maybe [Text]) -> Parser (Maybe [Text] -> DisplayInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
info Object -> Key -> Parser (Maybe [Text])
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"boundary"
                Parser (Maybe [Text] -> DisplayInfo)
-> Parser (Maybe [Text]) -> Parser DisplayInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
info Object -> Key -> Parser (Maybe [Text])
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"outputForms"
            Text
"NormalForm" -> Text -> DisplayInfo
NormalForm (Text -> DisplayInfo) -> Parser Text -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
info Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expr"
            Text
"InferredType" ->
              Type -> DisplayInfo
InferredType (Type -> DisplayInfo) -> Parser Type -> Parser DisplayInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
info Object -> Key -> Parser Type
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"expr"
            (Text
_ :: Text) ->
              DisplayInfo -> Parser DisplayInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DisplayInfo -> Parser DisplayInfo)
-> DisplayInfo -> Parser DisplayInfo
forall a b. (a -> b) -> a -> b
$ Value -> DisplayInfo
UnknownDisplayInfo Value
v
      (Text
_ :: Text) -> DisplayInfo -> Parser DisplayInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DisplayInfo -> Parser DisplayInfo)
-> DisplayInfo -> Parser DisplayInfo
forall a b. (a -> b) -> a -> b
$ Value -> DisplayInfo
UnknownDisplayInfo Value
v

instance FromJSON Response where
  parseJSON :: Value -> Parser Response
parseJSON Value
v = ((Object -> Parser Response) -> Value -> Parser Response)
-> Value -> (Object -> Parser Response) -> Parser Response
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Char] -> (Object -> Parser Response) -> Value -> Parser Response
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Response") Value
v ((Object -> Parser Response) -> Parser Response)
-> (Object -> Parser Response) -> Parser Response
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"kind" Parser Text -> (Text -> Parser Response) -> Parser Response
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Text
"MakeCase" ->
        MakeCase -> Response
MakeCase (MakeCase -> Response) -> Parser MakeCase -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser MakeCase
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
      Text
"ClearRunningInfo" ->
        Response -> Parser Response
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response
ClearRunningInfo
      Text
"HighlightingInfo" ->
        (Object
obj Object -> Key -> Parser Object
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"info") Parser Object -> (Object -> Parser Response) -> Parser Response
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Object
info ->
          Bool -> [Highlight] -> Response
HighlightingInfo (Bool -> [Highlight] -> Response)
-> Parser Bool -> Parser ([Highlight] -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
info Object -> Key -> Parser Bool
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"remove" Parser ([Highlight] -> Response)
-> Parser [Highlight] -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
info Object -> Key -> Parser [Highlight]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"payload"
      Text
"ClearHighlighting" ->
        Response -> Parser Response
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response
ClearHighlighting
      Text
"RunningInfo" ->
        Int -> Text -> Response
RunningInfo (Int -> Text -> Response)
-> Parser Int -> Parser (Text -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"debugLevel" Parser (Text -> Response) -> Parser Text -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"message"
      Text
"InteractionPoints" ->
        [InteractionPoint Maybe] -> Response
InteractionPoints ([InteractionPoint Maybe] -> Response)
-> Parser [InteractionPoint Maybe] -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser [InteractionPoint Maybe]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"interactionPoints"
      Text
"SolveAll" ->
        [Solution] -> Response
SolveAll ([Solution] -> Response) -> Parser [Solution] -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser [Solution]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"solutions"
      Text
"GiveAction" ->
        (Object
obj Object -> Key -> Parser Object
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"giveResult") Parser Object -> (Object -> Parser Response) -> Parser Response
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Object
result ->
          Text -> InteractionPoint (Const ()) -> Response
GiveAction (Text -> InteractionPoint (Const ()) -> Response)
-> Parser Text -> Parser (InteractionPoint (Const ()) -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
result Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"str" Parser (InteractionPoint (Const ()) -> Response)
-> Parser (InteractionPoint (Const ())) -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser (InteractionPoint (Const ()))
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"interactionPoint"
      Text
"DisplayInfo" ->
        DisplayInfo -> Response
DisplayInfo (DisplayInfo -> Response) -> Parser DisplayInfo -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser DisplayInfo
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"info"
      Text
"JumpToError" ->
        [Char] -> AgdaIndex -> Response
JumpToError ([Char] -> AgdaIndex -> Response)
-> Parser [Char] -> Parser (AgdaIndex -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser [Char]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"filepath" Parser (AgdaIndex -> Response)
-> Parser AgdaIndex -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser AgdaIndex
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"position"
      Text
"Status" -> do
        (Object
obj Object -> Key -> Parser Value
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"status" >>=) ((Value -> Parser Response) -> Parser Response)
-> (Value -> Parser Response) -> Parser Response
forall a b. (a -> b) -> a -> b
$ [Char] -> (Object -> Parser Response) -> Value -> Parser Response
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"Status" ((Object -> Parser Response) -> Value -> Parser Response)
-> (Object -> Parser Response) -> Value -> Parser Response
forall a b. (a -> b) -> a -> b
$ \Object
s ->
          Bool -> Bool -> Bool -> Response
Status (Bool -> Bool -> Bool -> Response)
-> Parser Bool -> Parser (Bool -> Bool -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
s Object -> Key -> Parser Bool
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"checked"
                  Parser (Bool -> Bool -> Response)
-> Parser Bool -> Parser (Bool -> Response)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
s Object -> Key -> Parser Bool
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"showIrrelevantArguments"Parser Bool -> Parser Bool -> Parser Bool
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Parser Bool
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)
                  Parser (Bool -> Response) -> Parser Bool -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
s Object -> Key -> Parser Bool
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"showImplicitArguments"
      (Text
_ :: Text) -> Text -> Value -> Response
Unknown (Text -> Value -> Response)
-> Parser Text -> Parser (Value -> Response)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"kind" Parser (Value -> Response) -> Parser Value -> Parser Response
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser Value
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v

newtype Extmark = Extmark Int64
  deriving (Extmark -> Extmark -> Bool
(Extmark -> Extmark -> Bool)
-> (Extmark -> Extmark -> Bool) -> Eq Extmark
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Extmark -> Extmark -> Bool
== :: Extmark -> Extmark -> Bool
$c/= :: Extmark -> Extmark -> Bool
/= :: Extmark -> Extmark -> Bool
Eq, Eq Extmark
Eq Extmark =>
(Extmark -> Extmark -> Ordering)
-> (Extmark -> Extmark -> Bool)
-> (Extmark -> Extmark -> Bool)
-> (Extmark -> Extmark -> Bool)
-> (Extmark -> Extmark -> Bool)
-> (Extmark -> Extmark -> Extmark)
-> (Extmark -> Extmark -> Extmark)
-> Ord Extmark
Extmark -> Extmark -> Bool
Extmark -> Extmark -> Ordering
Extmark -> Extmark -> Extmark
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Extmark -> Extmark -> Ordering
compare :: Extmark -> Extmark -> Ordering
$c< :: Extmark -> Extmark -> Bool
< :: Extmark -> Extmark -> Bool
$c<= :: Extmark -> Extmark -> Bool
<= :: Extmark -> Extmark -> Bool
$c> :: Extmark -> Extmark -> Bool
> :: Extmark -> Extmark -> Bool
$c>= :: Extmark -> Extmark -> Bool
>= :: Extmark -> Extmark -> Bool
$cmax :: Extmark -> Extmark -> Extmark
max :: Extmark -> Extmark -> Extmark
$cmin :: Extmark -> Extmark -> Extmark
min :: Extmark -> Extmark -> Extmark
Ord, Int -> Extmark -> ShowS
[Extmark] -> ShowS
Extmark -> [Char]
(Int -> Extmark -> ShowS)
-> (Extmark -> [Char]) -> ([Extmark] -> ShowS) -> Show Extmark
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Extmark -> ShowS
showsPrec :: Int -> Extmark -> ShowS
$cshow :: Extmark -> [Char]
show :: Extmark -> [Char]
$cshowList :: [Extmark] -> ShowS
showList :: [Extmark] -> ShowS
Show)

data ExtmarkStuff = ExtmarkStuff
  { ExtmarkStuff -> Extmark
es_mark     :: Extmark
  , ExtmarkStuff -> Text
es_hlgroup  :: Text
  , ExtmarkStuff -> AgdaInterval
es_interval :: AgdaInterval
  }
  deriving (ExtmarkStuff -> ExtmarkStuff -> Bool
(ExtmarkStuff -> ExtmarkStuff -> Bool)
-> (ExtmarkStuff -> ExtmarkStuff -> Bool) -> Eq ExtmarkStuff
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExtmarkStuff -> ExtmarkStuff -> Bool
== :: ExtmarkStuff -> ExtmarkStuff -> Bool
$c/= :: ExtmarkStuff -> ExtmarkStuff -> Bool
/= :: ExtmarkStuff -> ExtmarkStuff -> Bool
Eq, Eq ExtmarkStuff
Eq ExtmarkStuff =>
(ExtmarkStuff -> ExtmarkStuff -> Ordering)
-> (ExtmarkStuff -> ExtmarkStuff -> Bool)
-> (ExtmarkStuff -> ExtmarkStuff -> Bool)
-> (ExtmarkStuff -> ExtmarkStuff -> Bool)
-> (ExtmarkStuff -> ExtmarkStuff -> Bool)
-> (ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff)
-> (ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff)
-> Ord ExtmarkStuff
ExtmarkStuff -> ExtmarkStuff -> Bool
ExtmarkStuff -> ExtmarkStuff -> Ordering
ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ExtmarkStuff -> ExtmarkStuff -> Ordering
compare :: ExtmarkStuff -> ExtmarkStuff -> Ordering
$c< :: ExtmarkStuff -> ExtmarkStuff -> Bool
< :: ExtmarkStuff -> ExtmarkStuff -> Bool
$c<= :: ExtmarkStuff -> ExtmarkStuff -> Bool
<= :: ExtmarkStuff -> ExtmarkStuff -> Bool
$c> :: ExtmarkStuff -> ExtmarkStuff -> Bool
> :: ExtmarkStuff -> ExtmarkStuff -> Bool
$c>= :: ExtmarkStuff -> ExtmarkStuff -> Bool
>= :: ExtmarkStuff -> ExtmarkStuff -> Bool
$cmax :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff
max :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff
$cmin :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff
min :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff
Ord, Int -> ExtmarkStuff -> ShowS
[ExtmarkStuff] -> ShowS
ExtmarkStuff -> [Char]
(Int -> ExtmarkStuff -> ShowS)
-> (ExtmarkStuff -> [Char])
-> ([ExtmarkStuff] -> ShowS)
-> Show ExtmarkStuff
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExtmarkStuff -> ShowS
showsPrec :: Int -> ExtmarkStuff -> ShowS
$cshow :: ExtmarkStuff -> [Char]
show :: ExtmarkStuff -> [Char]
$cshowList :: [ExtmarkStuff] -> ShowS
showList :: [ExtmarkStuff] -> ShowS
Show)


data DebugCommand
  = DumpIPs
  deriving (DebugCommand -> DebugCommand -> Bool
(DebugCommand -> DebugCommand -> Bool)
-> (DebugCommand -> DebugCommand -> Bool) -> Eq DebugCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DebugCommand -> DebugCommand -> Bool
== :: DebugCommand -> DebugCommand -> Bool
$c/= :: DebugCommand -> DebugCommand -> Bool
/= :: DebugCommand -> DebugCommand -> Bool
Eq, Eq DebugCommand
Eq DebugCommand =>
(DebugCommand -> DebugCommand -> Ordering)
-> (DebugCommand -> DebugCommand -> Bool)
-> (DebugCommand -> DebugCommand -> Bool)
-> (DebugCommand -> DebugCommand -> Bool)
-> (DebugCommand -> DebugCommand -> Bool)
-> (DebugCommand -> DebugCommand -> DebugCommand)
-> (DebugCommand -> DebugCommand -> DebugCommand)
-> Ord DebugCommand
DebugCommand -> DebugCommand -> Bool
DebugCommand -> DebugCommand -> Ordering
DebugCommand -> DebugCommand -> DebugCommand
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DebugCommand -> DebugCommand -> Ordering
compare :: DebugCommand -> DebugCommand -> Ordering
$c< :: DebugCommand -> DebugCommand -> Bool
< :: DebugCommand -> DebugCommand -> Bool
$c<= :: DebugCommand -> DebugCommand -> Bool
<= :: DebugCommand -> DebugCommand -> Bool
$c> :: DebugCommand -> DebugCommand -> Bool
> :: DebugCommand -> DebugCommand -> Bool
$c>= :: DebugCommand -> DebugCommand -> Bool
>= :: DebugCommand -> DebugCommand -> Bool
$cmax :: DebugCommand -> DebugCommand -> DebugCommand
max :: DebugCommand -> DebugCommand -> DebugCommand
$cmin :: DebugCommand -> DebugCommand -> DebugCommand
min :: DebugCommand -> DebugCommand -> DebugCommand
Ord, Int -> DebugCommand -> ShowS
[DebugCommand] -> ShowS
DebugCommand -> [Char]
(Int -> DebugCommand -> ShowS)
-> (DebugCommand -> [Char])
-> ([DebugCommand] -> ShowS)
-> Show DebugCommand
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DebugCommand -> ShowS
showsPrec :: Int -> DebugCommand -> ShowS
$cshow :: DebugCommand -> [Char]
show :: DebugCommand -> [Char]
$cshowList :: [DebugCommand] -> ShowS
showList :: [DebugCommand] -> ShowS
Show, ReadPrec [DebugCommand]
ReadPrec DebugCommand
Int -> ReadS DebugCommand
ReadS [DebugCommand]
(Int -> ReadS DebugCommand)
-> ReadS [DebugCommand]
-> ReadPrec DebugCommand
-> ReadPrec [DebugCommand]
-> Read DebugCommand
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS DebugCommand
readsPrec :: Int -> ReadS DebugCommand
$creadList :: ReadS [DebugCommand]
readList :: ReadS [DebugCommand]
$creadPrec :: ReadPrec DebugCommand
readPrec :: ReadPrec DebugCommand
$creadListPrec :: ReadPrec [DebugCommand]
readListPrec :: ReadPrec [DebugCommand]
Read, Int -> DebugCommand
DebugCommand -> Int
DebugCommand -> [DebugCommand]
DebugCommand -> DebugCommand
DebugCommand -> DebugCommand -> [DebugCommand]
DebugCommand -> DebugCommand -> DebugCommand -> [DebugCommand]
(DebugCommand -> DebugCommand)
-> (DebugCommand -> DebugCommand)
-> (Int -> DebugCommand)
-> (DebugCommand -> Int)
-> (DebugCommand -> [DebugCommand])
-> (DebugCommand -> DebugCommand -> [DebugCommand])
-> (DebugCommand -> DebugCommand -> [DebugCommand])
-> (DebugCommand -> DebugCommand -> DebugCommand -> [DebugCommand])
-> Enum DebugCommand
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: DebugCommand -> DebugCommand
succ :: DebugCommand -> DebugCommand
$cpred :: DebugCommand -> DebugCommand
pred :: DebugCommand -> DebugCommand
$ctoEnum :: Int -> DebugCommand
toEnum :: Int -> DebugCommand
$cfromEnum :: DebugCommand -> Int
fromEnum :: DebugCommand -> Int
$cenumFrom :: DebugCommand -> [DebugCommand]
enumFrom :: DebugCommand -> [DebugCommand]
$cenumFromThen :: DebugCommand -> DebugCommand -> [DebugCommand]
enumFromThen :: DebugCommand -> DebugCommand -> [DebugCommand]
$cenumFromTo :: DebugCommand -> DebugCommand -> [DebugCommand]
enumFromTo :: DebugCommand -> DebugCommand -> [DebugCommand]
$cenumFromThenTo :: DebugCommand -> DebugCommand -> DebugCommand -> [DebugCommand]
enumFromThenTo :: DebugCommand -> DebugCommand -> DebugCommand -> [DebugCommand]
Enum, DebugCommand
DebugCommand -> DebugCommand -> Bounded DebugCommand
forall a. a -> a -> Bounded a
$cminBound :: DebugCommand
minBound :: DebugCommand
$cmaxBound :: DebugCommand
maxBound :: DebugCommand
Bounded)

-- * Translating Agda indices to Vim indices
--
-- Agda sometimes takes a while to process. We want to be able to modify the
-- buffer in the meantime. But then, Agda's highlighting instructions
-- will be out of sync.
--
-- We record the LineIntervals mapping (in field 'bs_code_map') at the time
-- when we reloaded, to translate old AgdaIndex to old VimPos, and then use the
-- 'Diff0' data structure (in field 'cs_diff') to translate (intervals of) old
-- VimPos to new VimPos.

-- | Data for mapping code point indices to byte indices
newtype LineIntervals = LineIntervals
  { LineIntervals
-> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
li_intervalMap :: IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
    -- ^ Mapping from positions to line numbers
  } deriving newtype (NonEmpty LineIntervals -> LineIntervals
LineIntervals -> LineIntervals -> LineIntervals
(LineIntervals -> LineIntervals -> LineIntervals)
-> (NonEmpty LineIntervals -> LineIntervals)
-> (forall b. Integral b => b -> LineIntervals -> LineIntervals)
-> Semigroup LineIntervals
forall b. Integral b => b -> LineIntervals -> LineIntervals
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: LineIntervals -> LineIntervals -> LineIntervals
<> :: LineIntervals -> LineIntervals -> LineIntervals
$csconcat :: NonEmpty LineIntervals -> LineIntervals
sconcat :: NonEmpty LineIntervals -> LineIntervals
$cstimes :: forall b. Integral b => b -> LineIntervals -> LineIntervals
stimes :: forall b. Integral b => b -> LineIntervals -> LineIntervals
Semigroup, Semigroup LineIntervals
LineIntervals
Semigroup LineIntervals =>
LineIntervals
-> (LineIntervals -> LineIntervals -> LineIntervals)
-> ([LineIntervals] -> LineIntervals)
-> Monoid LineIntervals
[LineIntervals] -> LineIntervals
LineIntervals -> LineIntervals -> LineIntervals
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: LineIntervals
mempty :: LineIntervals
$cmappend :: LineIntervals -> LineIntervals -> LineIntervals
mappend :: LineIntervals -> LineIntervals -> LineIntervals
$cmconcat :: [LineIntervals] -> LineIntervals
mconcat :: [LineIntervals] -> LineIntervals
Monoid)

-- | Buffer update events give us this instead of a proper Buffer
-- There is  buffer_get_number :: Buffer -> Neovim env BufferNum
-- but nothing the other way???
type BufferNum = Int64

-- Data structures from the diff-loc library
type DPos = Colline (LineNumber 'ZeroIndexed) VimIndex
type Diff0 = Diff DPos