-- | A typeclass collecting all 'pure' typechecking operations
-- | (i.e. ones that do not modify the typechecking state, throw or
-- | catch errors, or do IO other than debug printing).


module Agda.TypeChecking.Monad.Pure where

import Control.Monad.Except ( ExceptT )
import Control.Monad.Trans.Maybe ( MaybeT )
import Control.Monad.Reader ( ReaderT )
import Control.Monad.State ( StateT )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Writer ( WriterT )

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Signature

import Agda.Utils.ListT

class
  ( HasBuiltins m
  , HasConstInfo m
  , MonadAddContext m
  , MonadDebug m
  , MonadReduce m
  , MonadTCEnv m
  , ReadTCState m
  ) => PureTCM m where

instance PureTCM TCM where
instance PureTCM m => PureTCM (BlockT m)
instance PureTCM m => PureTCM (ExceptT e m)
instance PureTCM m => PureTCM (IdentityT m)
instance PureTCM m => PureTCM (ListT m)
instance PureTCM m => PureTCM (MaybeT m)
instance PureTCM m => PureTCM (ReaderT r m)
instance (PureTCM m, Monoid w) => PureTCM (WriterT w m)
instance PureTCM m => PureTCM (StateT s m)