{-# 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 {forall a. IM a -> TCMT (InputT IO) a
unIM :: TCMT (Haskeline.InputT IO) a}
  deriving
  ( (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
$cfmap :: forall a b. (a -> b) -> IM a -> IM b
fmap :: forall a b. (a -> b) -> IM a -> IM b
$c<$ :: forall a b. a -> IM b -> IM a
<$ :: forall a b. a -> IM b -> IM a
Functor, Functor IM
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
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
$cpure :: forall a. a -> IM a
pure :: forall a. a -> IM a
$c<*> :: forall a b. IM (a -> b) -> IM a -> IM b
<*> :: forall a b. IM (a -> b) -> IM a -> IM b
$cliftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
liftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
$c*> :: forall a b. IM a -> IM b -> IM b
*> :: forall a b. IM a -> IM b -> IM b
$c<* :: forall a b. IM a -> IM b -> IM a
<* :: forall a b. IM a -> IM b -> IM a
Applicative, Applicative IM
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
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
$c>>= :: forall a b. IM a -> (a -> IM b) -> IM b
>>= :: forall a b. IM a -> (a -> IM b) -> IM b
$c>> :: forall a b. IM a -> IM b -> IM b
>> :: forall a b. IM a -> IM b -> IM b
$creturn :: forall a. a -> IM a
return :: forall a. a -> IM a
Monad, Monad IM
Monad IM -> (forall a. IO a -> IM a) -> MonadIO IM
forall a. IO a -> IM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> IM a
liftIO :: forall a. IO a -> IM a
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
$cpragmaOptions :: IM PragmaOptions
pragmaOptions :: IM PragmaOptions
$ccommandLineOptions :: IM CommandLineOptions
commandLineOptions :: IM CommandLineOptions
HasOptions, Monad IM
IM TCEnv
Monad IM
-> IM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> IM a -> IM a)
-> MonadTCEnv IM
forall a. (TCEnv -> TCEnv) -> IM a -> IM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
$caskTC :: IM TCEnv
askTC :: IM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
localTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
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
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
$cgetTCState :: IM TCState
getTCState :: IM TCState
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
$cwithTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
withTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
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
$cgetTC :: IM TCState
getTC :: IM TCState
$cputTC :: TCState -> IM ()
putTC :: TCState -> IM ()
$cmodifyTC :: (TCState -> TCState) -> IM ()
modifyTC :: (TCState -> TCState) -> 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
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
$cliftTCM :: forall a. TCM a -> IM a
liftTCM :: forall a. TCM a -> IM a
MonadTCM )

runIM :: IM a -> TCM a
runIM :: forall a. IM a -> TCM a
runIM = (forall a1. InputT IO a1 -> IO a1)
-> TCMT (InputT IO) a -> TCMT IO 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 -> TCMT IO a)
-> (IM a -> TCMT (InputT IO) a) -> IM a -> TCMT IO 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 :: forall a. TCErr -> IM a
throwError                = IO a -> IM a
forall a. 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 :: forall a. 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 e a.
Exception e =>
InputT IO a -> (e -> 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 (m :: * -> *) a. Monad m => m a -> TCMT m a
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)