module Agda.Interaction.Command
  ( CommandM, localStateCommandM, liftLocalState, revLift, revLiftTC
  ) where

import Control.Monad.State ( MonadState(..), execStateT, lift )

import Agda.TypeChecking.Monad.Base ( TCM,MonadTCState, TCState, getTC, putTC )
import Agda.TypeChecking.Monad.State ( localTCState )

import Agda.Interaction.Base ( CommandM' )

------------------------------------------------------------------------
-- The CommandM monad

type CommandM  = CommandM' TCM

-- | Restore both 'TCState' and 'CommandState'.

localStateCommandM :: CommandM a -> CommandM a
localStateCommandM :: forall a. CommandM a -> CommandM a
localStateCommandM CommandM a
m = do
  CommandState
cSt <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
  TCState
tcSt <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  a
x <- CommandM a
m
  TCState -> StateT CommandState TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcSt
  CommandState -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
cSt
  a -> CommandM a
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- | Restore 'TCState', do not touch 'CommandState'.

liftLocalState :: TCM a -> CommandM a
liftLocalState :: forall a. TCM a -> CommandM a
liftLocalState = TCM a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM a -> StateT CommandState TCM a)
-> (TCM a -> TCM a) -> TCM a -> StateT CommandState TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM a -> TCM a
forall a. TCM a -> TCM a
localTCState

-- | Build an opposite action to 'lift' for state monads.

revLift
    :: MonadState st m
    => (forall c . m c -> st -> k (c, st))      -- ^ run
    -> (forall b . k b -> m b)                  -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a  -- ^ reverse lift in double negative position
revLift :: forall st (m :: * -> *) (k :: * -> *) a.
MonadState st m =>
(forall c. m c -> st -> k (c, st))
-> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLift forall c. m c -> st -> k (c, st)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    st
st <- m st
forall s (m :: * -> *). MonadState s m => m s
get
    (a
a, st
st') <- k (a, st) -> m (a, st)
forall b. k b -> m b
lift' (k (a, st) -> m (a, st)) -> k (a, st) -> m (a, st)
forall a b. (a -> b) -> a -> b
$ (m a -> k (a, st)) -> k (a, st)
forall x. (m a -> k x) -> k x
f (m a -> st -> k (a, st)
forall c. m c -> st -> k (c, st)
`run` st
st)
    st -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put st
st'
    a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

revLiftTC
    :: MonadTCState m
    => (forall c . m c -> TCState -> k (c, TCState))  -- ^ run
    -> (forall b . k b -> m b)                        -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a        -- ^ reverse lift in double negative position
revLiftTC :: forall (m :: * -> *) (k :: * -> *) a.
MonadTCState m =>
(forall c. m c -> TCState -> k (c, TCState))
-> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLiftTC forall c. m c -> TCState -> k (c, TCState)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    TCState
st <- m TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    (a
a, TCState
st') <- k (a, TCState) -> m (a, TCState)
forall b. k b -> m b
lift' (k (a, TCState) -> m (a, TCState))
-> k (a, TCState) -> m (a, TCState)
forall a b. (a -> b) -> a -> b
$ (m a -> k (a, TCState)) -> k (a, TCState)
forall x. (m a -> k x) -> k x
f (m a -> TCState -> k (a, TCState)
forall c. m c -> TCState -> k (c, TCState)
`run` TCState
st)
    TCState -> m ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st'
    a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a