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 #
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 #
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 #
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 # liftA2 :: (a -> b -> c) -> ExceptT e m a -> ExceptT e m b -> ExceptT e m c # (>) :: 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] # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (ExceptT e m a) # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [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)) -> (#TupleRep [RuntimeRep], LiftedRep, 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 #

The strategy of combining computations that can throw exceptions by bypassing bound functions from the point an exception is thrown to the point that it is handled.

Is parameterized over the type of error information and the monad type constructor. It is common to use Either String as the monad type constructor for an error monad in which error descriptions take the form of strings. In that case and many other common cases the resulting monad is already defined as an instance of the MonadError class. You can also define your own error type and/or use a monad type constructor other than Either String or Either IOError. In these cases you will have to explicitly define instances of the Error and/or MonadError classes.

Minimal complete definition

throwError, catchError

Methods

throwError :: e -> m a #

Is used within a monadic computation to begin exception processing.

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

A handler function to handle previous errors and return to normal execution. A common idiom is:

do { action1; action2; action3 } `catchError` handler

where the action functions can call throwError. Note that handler and the do-block must have the same return type.

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 #
(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 (STT s m)
Methods throwError :: e -> STT s m a # catchError :: STT s m a -> (e -> STT s m a) -> STT s 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 #
(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 #
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 #

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

The inverse of ExceptT.