{-# OPTIONS_GHC -fwarn-orphans #-}
{-# LANGUAGE CPP               #-}

module Agda.Interaction.Monad
  ( IM
  , runIM
  , readline
  ) where

import Agda.TypeChecking.Monad
  ( HasOptions
  , MonadTCEnv
  , MonadTCM
  , MonadTCState
  , ReadTCState
  , TCErr
  , TCM, TCMT(..)
  , mapTCMT
  )
import Control.Exception (throwIO)
import Control.Monad.Except (MonadError (..))
import Control.Monad.Trans (MonadIO, lift, liftIO)
import qualified System.Console.Haskeline as Haskeline

-- MonadException is replaced by MonadCatch in haskeline 0.8
#if MIN_VERSION_haskeline(0,8,0)
import qualified Control.Monad.Catch as Haskeline (catch)
#endif

-- | Interaction monad.
newtype IM a = IM {IM a -> TCMT (InputT IO) a
unIM :: TCMT (Haskeline.InputT IO) a}
  deriving
  ( a -> IM b -> IM a
(a -> b) -> IM a -> IM b
(forall a b. (a -> b) -> IM a -> IM b)
-> (forall a b. a -> IM b -> IM a) -> Functor IM
forall a b. a -> IM b -> IM a
forall a b. (a -> b) -> IM a -> IM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> IM b -> IM a
$c<$ :: forall a b. a -> IM b -> IM a
fmap :: (a -> b) -> IM a -> IM b
$cfmap :: forall a b. (a -> b) -> IM a -> IM b
Functor, Functor IM
a -> IM a
Functor IM
-> (forall a. a -> IM a)
-> (forall a b. IM (a -> b) -> IM a -> IM b)
-> (forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c)
-> (forall a b. IM a -> IM b -> IM b)
-> (forall a b. IM a -> IM b -> IM a)
-> Applicative IM
IM a -> IM b -> IM b
IM a -> IM b -> IM a
IM (a -> b) -> IM a -> IM b
(a -> b -> c) -> IM a -> IM b -> IM c
forall a. a -> IM a
forall a b. IM a -> IM b -> IM a
forall a b. IM a -> IM b -> IM b
forall a b. IM (a -> b) -> IM a -> IM b
forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: IM a -> IM b -> IM a
$c<* :: forall a b. IM a -> IM b -> IM a
*> :: IM a -> IM b -> IM b
$c*> :: forall a b. IM a -> IM b -> IM b
liftA2 :: (a -> b -> c) -> IM a -> IM b -> IM c
$cliftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
<*> :: IM (a -> b) -> IM a -> IM b
$c<*> :: forall a b. IM (a -> b) -> IM a -> IM b
pure :: a -> IM a
$cpure :: forall a. a -> IM a
$cp1Applicative :: Functor IM
Applicative, Applicative IM
a -> IM a
Applicative IM
-> (forall a b. IM a -> (a -> IM b) -> IM b)
-> (forall a b. IM a -> IM b -> IM b)
-> (forall a. a -> IM a)
-> Monad IM
IM a -> (a -> IM b) -> IM b
IM a -> IM b -> IM b
forall a. a -> IM a
forall a b. IM a -> IM b -> IM b
forall a b. IM a -> (a -> IM b) -> IM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> IM a
$creturn :: forall a. a -> IM a
>> :: IM a -> IM b -> IM b
$c>> :: forall a b. IM a -> IM b -> IM b
>>= :: IM a -> (a -> IM b) -> IM b
$c>>= :: forall a b. IM a -> (a -> IM b) -> IM b
$cp1Monad :: Applicative IM
Monad, Monad IM
Monad IM -> (forall a. IO a -> IM a) -> MonadIO IM
IO a -> IM a
forall a. IO a -> IM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> IM a
$cliftIO :: forall a. IO a -> IM a
$cp1MonadIO :: Monad IM
MonadIO
  , Monad IM
Functor IM
Applicative IM
IM PragmaOptions
IM CommandLineOptions
Functor IM
-> Applicative IM
-> Monad IM
-> IM PragmaOptions
-> IM CommandLineOptions
-> HasOptions IM
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
commandLineOptions :: IM CommandLineOptions
$ccommandLineOptions :: IM CommandLineOptions
pragmaOptions :: IM PragmaOptions
$cpragmaOptions :: IM PragmaOptions
$cp3HasOptions :: Monad IM
$cp2HasOptions :: Applicative IM
$cp1HasOptions :: Functor IM
HasOptions, Monad IM
IM TCEnv
Monad IM
-> IM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> IM a -> IM a)
-> MonadTCEnv IM
(TCEnv -> TCEnv) -> IM a -> IM a
forall a. (TCEnv -> TCEnv) -> IM a -> IM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: (TCEnv -> TCEnv) -> IM a -> IM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
askTC :: IM TCEnv
$caskTC :: IM TCEnv
$cp1MonadTCEnv :: Monad IM
MonadTCEnv, Monad IM
IM TCState
Monad IM
-> IM TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b)
-> (forall a. (TCState -> TCState) -> IM a -> IM a)
-> ReadTCState IM
(TCState -> TCState) -> IM a -> IM a
Lens' a TCState -> (a -> a) -> IM b -> IM b
forall a. (TCState -> TCState) -> IM a -> IM a
forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: (TCState -> TCState) -> IM a -> IM a
$cwithTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
locallyTCState :: Lens' a TCState -> (a -> a) -> IM b -> IM b
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
getTCState :: IM TCState
$cgetTCState :: IM TCState
$cp1ReadTCState :: Monad IM
ReadTCState, Monad IM
IM TCState
Monad IM
-> IM TCState
-> (TCState -> IM ())
-> ((TCState -> TCState) -> IM ())
-> MonadTCState IM
TCState -> IM ()
(TCState -> TCState) -> IM ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
modifyTC :: (TCState -> TCState) -> IM ()
$cmodifyTC :: (TCState -> TCState) -> IM ()
putTC :: TCState -> IM ()
$cputTC :: TCState -> IM ()
getTC :: IM TCState
$cgetTC :: IM TCState
$cp1MonadTCState :: Monad IM
MonadTCState, Applicative IM
MonadIO IM
HasOptions IM
MonadTCState IM
MonadTCEnv IM
Applicative IM
-> MonadIO IM
-> MonadTCEnv IM
-> MonadTCState IM
-> HasOptions IM
-> (forall a. TCM a -> IM a)
-> MonadTCM IM
TCM a -> IM a
forall a. TCM a -> IM a
forall (tcm :: * -> *).
Applicative tcm
-> MonadIO tcm
-> MonadTCEnv tcm
-> MonadTCState tcm
-> HasOptions tcm
-> (forall a. TCM a -> tcm a)
-> MonadTCM tcm
liftTCM :: TCM a -> IM a
$cliftTCM :: forall a. TCM a -> IM a
$cp5MonadTCM :: HasOptions IM
$cp4MonadTCM :: MonadTCState IM
$cp3MonadTCM :: MonadTCEnv IM
$cp2MonadTCM :: MonadIO IM
$cp1MonadTCM :: Applicative IM
MonadTCM )

runIM :: IM a -> TCM a
runIM :: IM a -> TCM a
runIM = (forall a1. InputT IO a1 -> IO a1) -> TCMT (InputT IO) a -> TCM a
forall (m :: * -> *) (n :: * -> *) a.
(forall a1. m a1 -> n a1) -> TCMT m a -> TCMT n a
mapTCMT (Settings IO -> InputT IO a1 -> IO a1
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
Haskeline.runInputT Settings IO
forall (m :: * -> *). MonadIO m => Settings m
Haskeline.defaultSettings) (TCMT (InputT IO) a -> TCM a)
-> (IM a -> TCMT (InputT IO) a) -> IM a -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IM a -> TCMT (InputT IO) a
forall a. IM a -> TCMT (InputT IO) a
unIM

instance MonadError TCErr IM where
  throwError :: TCErr -> IM a
throwError                = IO a -> IM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> IM a) -> (TCErr -> IO a) -> TCErr -> IM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> IO a
forall e a. Exception e => e -> IO a
throwIO
  catchError :: IM a -> (TCErr -> IM a) -> IM a
catchError (IM (TCM IORef TCState -> TCEnv -> InputT IO a
m)) TCErr -> IM a
h = TCMT (InputT IO) a -> IM a
forall a. TCMT (InputT IO) a -> IM a
IM (TCMT (InputT IO) a -> IM a)
-> ((IORef TCState -> TCEnv -> InputT IO a) -> TCMT (InputT IO) a)
-> (IORef TCState -> TCEnv -> InputT IO a)
-> IM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IORef TCState -> TCEnv -> InputT IO a) -> TCMT (InputT IO) a
forall (m :: * -> *) a. (IORef TCState -> TCEnv -> m a) -> TCMT m a
TCM ((IORef TCState -> TCEnv -> InputT IO a) -> IM a)
-> (IORef TCState -> TCEnv -> InputT IO a) -> IM a
forall a b. (a -> b) -> a -> b
$ \IORef TCState
s TCEnv
e ->
    IORef TCState -> TCEnv -> InputT IO a
m IORef TCState
s TCEnv
e InputT IO a -> (TCErr -> InputT IO a) -> InputT IO a
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Haskeline.catch` \TCErr
err -> TCMT (InputT IO) a -> IORef TCState -> TCEnv -> InputT IO a
forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (IM a -> TCMT (InputT IO) a
forall a. IM a -> TCMT (InputT IO) a
unIM (TCErr -> IM a
h TCErr
err)) IORef TCState
s TCEnv
e

-- | Line reader. The line reader history is not stored between
-- sessions.
readline :: String -> IM (Maybe String)
readline :: String -> IM (Maybe String)
readline String
s = TCMT (InputT IO) (Maybe String) -> IM (Maybe String)
forall a. TCMT (InputT IO) a -> IM a
IM (TCMT (InputT IO) (Maybe String) -> IM (Maybe String))
-> TCMT (InputT IO) (Maybe String) -> IM (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT IO (Maybe String) -> TCMT (InputT IO) (Maybe String)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> InputT IO (Maybe String)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
Haskeline.getInputLine String
s)