Agda.Utils.Except

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

Documentation

class Error a where

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

Methods

noMsg :: a

strMsg :: String -> a

Instances

Error String

A string can be thrown as an error.

Methods

noMsg :: String

strMsg :: String -> String

Error TCErr

Methods

noMsg :: TCErr

strMsg :: String -> TCErr

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

Methods

convert :: Exp O -> MOT Type

Conversion MOT (Exp O) Term

Methods

convert :: Exp O -> MOT Term

Conversion MOT a b => Conversion MOT (Abs a) (Abs b)

Methods

convert :: Abs a -> MOT (Abs b)

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

Methods

convert :: MM a (RefInfo O) -> MOT b

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)

Methods

liftTCM :: TCM a -> ExceptT err tcm a

HasOptions m => HasOptions (ExceptT e m)

Methods

pragmaOptions :: ExceptT e m PragmaOptions

commandLineOptions :: ExceptT e m CommandLineOptions

MonadDebug m => MonadDebug (ExceptT e m)

Methods

displayDebugMessage :: Int -> String -> ExceptT e m ()

traceDebugMessage :: Int -> String -> ExceptT e m a -> ExceptT e m a

formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ExceptT e m String

HasConstInfo m => HasConstInfo (ExceptT err m)

Methods

getConstInfo :: QName -> ExceptT err m Definition

getConstInfo' :: QName -> ExceptT err m (Either SigError Definition)

getRewriteRulesFor :: QName -> ExceptT err m RewriteRules

(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

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 () Maybe

Methods

throwError :: () -> Maybe a

catchError :: Maybe a -> (() -> Maybe a) -> Maybe a

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.