Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.Except

Description

Wrapper for Control.Monad.Except from the mtl library (>= 2.2.1)

Synopsis

Documentation

class Error a where Source #

Error class for backward compatibility (from Control.Monad.Trans.Error in transformers 0.3.0.0).

Methods

noMsg :: a Source #

strMsg :: String -> a Source #

Instances

Error String Source #	A string can be thrown as an error.
Methods noMsg :: String Source # strMsg :: String -> String Source #
Error TCErr Source #
Methods noMsg :: TCErr Source # strMsg :: String -> TCErr Source #

data ExceptT e m a :: * -> (* -> *) -> * -> * #

A monad transformer that adds exceptions to other monads.

ExceptT constructs a monad parameterized over two things:

e - The exception type.
m - The inner monad.

The return function yields a computation that produces the given value, while >>= sequences two subcomputations, exiting on the first exception.

Instances

MonadEquiv c v d m => MonadEquiv c v d (ExceptT e m)
Methods equivalent :: v -> v -> ExceptT e m Bool # classDesc :: v -> ExceptT e m d # equateAll :: [v] -> ExceptT e m () # equate :: v -> v -> ExceptT e m () # removeClass :: v -> ExceptT e m Bool # getClass :: v -> ExceptT e m c # combineAll :: [c] -> ExceptT e m () # combine :: c -> c -> ExceptT e m c # (===) :: c -> c -> ExceptT e m Bool # desc :: c -> ExceptT e m d # remove :: c -> ExceptT e m Bool #
Conversion MOT (Exp O) Type Source #
Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source #
Methods convert :: Exp O -> MOT Term Source #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source #
Methods convert :: Abs a -> MOT (Abs b) Source #
MonadWriter w m => MonadWriter w (ExceptT e m)
Methods writer :: (a, w) -> ExceptT e m a tell :: w -> ExceptT e m () listen :: ExceptT e m a -> ExceptT e m (a, w) pass :: ExceptT e m (a, w -> w) -> ExceptT e m a
MonadReader r m => MonadReader r (ExceptT e m)
Methods ask :: ExceptT e m r local :: (r -> r) -> ExceptT e m a -> ExceptT e m a reader :: (r -> a) -> ExceptT e m a
MonadState s m => MonadState s (ExceptT e m)
Methods get :: ExceptT e m s put :: s -> ExceptT e m () state :: (s -> (a, s)) -> ExceptT e m a
Monad m => MonadError e (ExceptT e m)
Methods throwError :: e -> ExceptT e m a # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #
Methods convert :: MM a (RefInfo O) -> MOT b Source #
MonadTrans (ExceptT e)
Methods lift :: Monad m => m a -> ExceptT e m a #
Monad m => Monad (ExceptT e m)
Methods (>>=) :: ExceptT e m a -> (a -> ExceptT e m b) -> ExceptT e m b # (>>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b # return :: a -> ExceptT e m a # fail :: String -> ExceptT e m a #
Functor m => Functor (ExceptT e m)
Methods fmap :: (a -> b) -> ExceptT e m a -> ExceptT e m b # (<$) :: a -> ExceptT e m b -> ExceptT e m a #
MonadFix m => MonadFix (ExceptT e m)
Methods mfix :: (a -> ExceptT e m a) -> ExceptT e m a #
MonadFail m => MonadFail (ExceptT e m)
Methods fail :: String -> ExceptT e m a #
(Functor m, Monad m) => Applicative (ExceptT e m)
Methods pure :: a -> ExceptT e m a # (<>) :: ExceptT e m (a -> b) -> ExceptT e m a -> ExceptT e m b # (>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b # (<*) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m a #
Foldable f => Foldable (ExceptT e f)
Methods fold :: Monoid m => ExceptT e f m -> m # foldMap :: Monoid m => (a -> m) -> ExceptT e f a -> m # foldr :: (a -> b -> b) -> b -> ExceptT e f a -> b # foldr' :: (a -> b -> b) -> b -> ExceptT e f a -> b # foldl :: (b -> a -> b) -> b -> ExceptT e f a -> b # foldl' :: (b -> a -> b) -> b -> ExceptT e f a -> b # foldr1 :: (a -> a -> a) -> ExceptT e f a -> a # foldl1 :: (a -> a -> a) -> ExceptT e f a -> a # toList :: ExceptT e f a -> [a] # null :: ExceptT e f a -> Bool # length :: ExceptT e f a -> Int # elem :: Eq a => a -> ExceptT e f a -> Bool # maximum :: Ord a => ExceptT e f a -> a # minimum :: Ord a => ExceptT e f a -> a # sum :: Num a => ExceptT e f a -> a # product :: Num a => ExceptT e f a -> a #
Traversable f => Traversable (ExceptT e f)
Methods traverse :: Applicative f => (a -> f b) -> ExceptT e f a -> f (ExceptT e f b) # sequenceA :: Applicative f => ExceptT e f (f a) -> f (ExceptT e f a) # mapM :: Monad m => (a -> m b) -> ExceptT e f a -> m (ExceptT e f b) # sequence :: Monad m => ExceptT e f (m a) -> m (ExceptT e f a) #
(Eq e, Eq1 m) => Eq1 (ExceptT e m)
Methods liftEq :: (a -> b -> Bool) -> ExceptT e m a -> ExceptT e m b -> Bool #
(Ord e, Ord1 m) => Ord1 (ExceptT e m)
Methods liftCompare :: (a -> b -> Ordering) -> ExceptT e m a -> ExceptT e m b -> Ordering #
(Read e, Read1 m) => Read1 (ExceptT e m)
Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ExceptT e m a) # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ExceptT e m a] #
(Show e, Show1 m) => Show1 (ExceptT e m)
Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ExceptT e m a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ExceptT e m a] -> ShowS #
MonadZip m => MonadZip (ExceptT e m)
Methods mzip :: ExceptT e m a -> ExceptT e m b -> ExceptT e m (a, b) # mzipWith :: (a -> b -> c) -> ExceptT e m a -> ExceptT e m b -> ExceptT e m c # munzip :: ExceptT e m (a, b) -> (ExceptT e m a, ExceptT e m b) #
MonadIO m => MonadIO (ExceptT e m)
Methods liftIO :: IO a -> ExceptT e m a #
(Functor m, Monad m, Monoid e) => Alternative (ExceptT e m)
Methods empty :: ExceptT e m a # (<\|>) :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a # some :: ExceptT e m a -> ExceptT e m [a] # many :: ExceptT e m a -> ExceptT e m [a] #
(Monad m, Monoid e) => MonadPlus (ExceptT e m)
Methods mzero :: ExceptT e m a # mplus :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a #
PrimMonad m => PrimMonad (ExceptT e m)
Associated Types type PrimState (ExceptT e m :: * -> ) :: Methods primitive :: (State# (PrimState (ExceptT e m)) -> (#VoidRep, PtrRepLifted, State# (PrimState (ExceptT e m)), a#)) -> ExceptT e m a
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source #
Methods liftTCM :: TCM a -> ExceptT err tcm a Source #
HasOptions m => HasOptions (ExceptT e m) Source #
Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source #
MonadDebug m => MonadDebug (ExceptT e m) Source #
Methods displayDebugMessage :: Int -> String -> ExceptT e m () Source # traceDebugMessage :: Int -> String -> ExceptT e m a -> ExceptT e m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ExceptT e m String Source #
HasConstInfo m => HasConstInfo (ExceptT err m) Source #
Methods getConstInfo :: QName -> ExceptT err m Definition Source # getConstInfo' :: QName -> ExceptT err m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ExceptT err m RewriteRules Source #
(Eq e, Eq1 m, Eq a) => Eq (ExceptT e m a)
Methods (==) :: ExceptT e m a -> ExceptT e m a -> Bool # (/=) :: ExceptT e m a -> ExceptT e m a -> Bool #
(Ord e, Ord1 m, Ord a) => Ord (ExceptT e m a)
Methods compare :: ExceptT e m a -> ExceptT e m a -> Ordering # (<) :: ExceptT e m a -> ExceptT e m a -> Bool # (<=) :: ExceptT e m a -> ExceptT e m a -> Bool # (>) :: ExceptT e m a -> ExceptT e m a -> Bool # (>=) :: ExceptT e m a -> ExceptT e m a -> Bool # max :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a # min :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a #
(Read e, Read1 m, Read a) => Read (ExceptT e m a)
Methods readsPrec :: Int -> ReadS (ExceptT e m a) # readList :: ReadS [ExceptT e m a] # readPrec :: ReadPrec (ExceptT e m a) # readListPrec :: ReadPrec [ExceptT e m a] #
(Show e, Show1 m, Show a) => Show (ExceptT e m a)
Methods showsPrec :: Int -> ExceptT e m a -> ShowS # show :: ExceptT e m a -> String # showList :: [ExceptT e m a] -> ShowS #
type PrimState (ExceptT e m)
type PrimState (ExceptT e m) = PrimState m

mapExceptT :: (m (Either e a) -> n (Either e' b)) -> ExceptT e m a -> ExceptT e' n b #

Map the unwrapped computation using the given function.

runExceptT (mapExceptT f m) = f (runExceptT m)

mkExceptT :: m (Either e a) -> ExceptT e m a Source #

We cannot define data constructors synonymous, so we define the mkExceptT function to be used instead of the data constructor ExceptT.

class Monad m => MonadError e m | m -> e where #

Minimal complete definition

throwError, catchError

Methods

throwError :: e -> m a #

catchError :: m a -> (e -> m a) -> m a #

Instances

MonadError IOException IO
Methods throwError :: IOException -> IO a # catchError :: IO a -> (IOException -> IO a) -> IO a #
MonadError ParseError Parser #
Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a #
MonadError ParseError PM #
Methods throwError :: ParseError -> PM a # catchError :: PM a -> (ParseError -> PM a) -> PM a #
MonadError DeclarationException Nice #
Methods throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a #
MonadError TCErr IM #
Methods throwError :: TCErr -> IM a # catchError :: IM a -> (TCErr -> IM a) -> IM a #
MonadError TCErr TerM #
Methods throwError :: TCErr -> TerM a # catchError :: TerM a -> (TCErr -> TerM a) -> TerM a #
MonadError e m => MonadError e (MaybeT m)
Methods throwError :: e -> MaybeT m a # catchError :: MaybeT m a -> (e -> MaybeT m a) -> MaybeT m a #
MonadError e m => MonadError e (ListT m)
Methods throwError :: e -> ListT m a # catchError :: ListT m a -> (e -> ListT m a) -> ListT m a #
MonadError e (Either e)
Methods throwError :: e -> Either e a # catchError :: Either e a -> (e -> Either e a) -> Either e a #
MonadError TCErr (TCMT IO) #
Methods throwError :: TCErr -> TCMT IO a # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a #
MonadError e m => MonadError e (STT s m)
Methods throwError :: e -> STT s m a # catchError :: STT s m a -> (e -> STT s m a) -> STT s m a #
(Monoid w, MonadError e m) => MonadError e (WriterT w m)
Methods throwError :: e -> WriterT w m a # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a #
(Monoid w, MonadError e m) => MonadError e (WriterT w m)
Methods throwError :: e -> WriterT w m a # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a #
MonadError e m => MonadError e (StateT s m)
Methods throwError :: e -> StateT s m a # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a #
MonadError e m => MonadError e (StateT s m)
Methods throwError :: e -> StateT s m a # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a #
MonadError e m => MonadError e (IdentityT * m)
Methods throwError :: e -> IdentityT * m a # catchError :: IdentityT * m a -> (e -> IdentityT * m a) -> IdentityT * m a #
Monad m => MonadError e (ExceptT e m)
Methods throwError :: e -> ExceptT e m a # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a #
(Monad m, Error e) => MonadError e (ErrorT e m)
Methods throwError :: e -> ErrorT e m a # catchError :: ErrorT e m a -> (e -> ErrorT e m a) -> ErrorT e m a #
MonadError e m => MonadError e (ReaderT * r m)
Methods throwError :: e -> ReaderT * r m a # catchError :: ReaderT * r m a -> (e -> ReaderT * r m a) -> ReaderT * r m a #
MonadError e m => MonadError e (ParsecT s u m)
Methods throwError :: e -> ParsecT s u m a # catchError :: ParsecT s u m a -> (e -> ParsecT s u m a) -> ParsecT s u m a #
MonadError e m => MonadError e (EquivT s c v m)
Methods throwError :: e -> EquivT s c v m a # catchError :: EquivT s c v m a -> (e -> EquivT s c v m a) -> EquivT s c v m a #
(Monoid w, MonadError e m) => MonadError e (RWST r w s m)
Methods throwError :: e -> RWST r w s m a # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a #
(Monoid w, MonadError e m) => MonadError e (RWST r w s m)
Methods throwError :: e -> RWST r w s m a # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a #

runExceptT :: ExceptT e m a -> m (Either e a) #

The inverse of ExceptT.