{-# 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 -> 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
<$ :: forall a b. a -> IM b -> IM a
$c<$ :: forall a b. a -> IM b -> IM a
fmap :: forall a b. (a -> b) -> IM a -> IM b
$cfmap :: forall a b. (a -> b) -> IM a -> IM b
Functor, Functor 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
<* :: forall a b. IM a -> IM b -> IM a
$c<* :: forall a b. IM a -> IM b -> IM a
*> :: forall a b. IM a -> IM b -> IM b
$c*> :: forall a b. IM a -> IM b -> IM b
liftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
$cliftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
<*> :: forall a b. IM (a -> b) -> IM a -> IM b
$c<*> :: forall a b. IM (a -> b) -> IM a -> IM b
pure :: forall a. a -> IM a
$cpure :: forall a. a -> IM a
Applicative, Applicative 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
return :: forall a. a -> IM a
$creturn :: forall a. a -> IM a
>> :: forall a b. IM a -> IM b -> IM b
$c>> :: forall a b. IM a -> IM b -> IM b
>>= :: forall a b. IM a -> (a -> IM b) -> IM b
$c>>= :: forall a b. IM a -> (a -> IM b) -> IM b
Monad, Monad IM
forall a. IO a -> IM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> IM a
$cliftIO :: forall a. IO a -> IM a
MonadIO
  , Monad IM
Functor IM
Applicative IM
IM PragmaOptions
IM CommandLineOptions
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
HasOptions, Monad IM
IM TCEnv
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 :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
askTC :: IM TCEnv
$caskTC :: IM TCEnv
MonadTCEnv, Monad IM
IM TCState
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 :: forall a. (TCState -> TCState) -> IM a -> IM a
$cwithTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
locallyTCState :: forall a b. 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
ReadTCState, Monad IM
IM TCState
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
MonadTCState, Applicative IM
MonadIO IM
HasOptions IM
MonadTCState IM
MonadTCEnv 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
liftTCM :: forall a. TCM a -> IM a
$cliftTCM :: forall a. TCM a -> IM a
MonadTCM )

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

instance MonadError TCErr IM where
  throwError :: forall a. TCErr -> IM a
throwError                = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. TCMT (InputT IO) a -> IM a
IM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. (IORef TCState -> TCEnv -> m a) -> TCMT m a
TCM forall a b. (a -> b) -> a -> b
$ \IORef TCState
s TCEnv
e ->
    IORef TCState -> TCEnv -> InputT IO a
m IORef TCState
s TCEnv
e forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Haskeline.catch` \TCErr
err -> forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (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 = forall a. TCMT (InputT IO) a -> IM a
IM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
Haskeline.getInputLine String
s)