Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.Except

Description

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

Synopsis

- class Error a where
  - noMsg :: a
  - strMsg :: String -> a
- data ExceptT e (m :: Type -> Type) a
- mapExceptT :: (m (Either e a) -> n (Either e' b)) -> ExceptT e m a -> ExceptT e' n b
- mkExceptT :: m (Either e a) -> ExceptT e m a
- class Monad m => MonadError e (m :: Type -> Type) | m -> e where
  - throwError :: e -> m a
  - catchError :: m a -> (e -> m a) -> m a
- runExceptT :: ExceptT e m a -> m (Either e a)

# Documentation

class Error a where Source #

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

Minimal complete definition

Nothing

Methods

noMsg :: a Source #

strMsg :: String -> a Source #

Instances

Error String Source # | A string can be thrown as an error.
Instance details Defined in Agda.Utils.Except Methods noMsg :: String Source # strMsg :: String -> String Source #
Error TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods noMsg :: TCErr Source # strMsg :: String -> TCErr Source #

data ExceptT e (m :: Type -> Type) a Source #

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

Instance details

Defined in Data.Equivalence.Monad

Methods

equivalent :: v -> v -> ExceptT e m Bool Source #

classDesc :: v -> ExceptT e m d Source #

equateAll :: [v] -> ExceptT e m () Source #

equate :: v -> v -> ExceptT e m () Source #

removeClass :: v -> ExceptT e m Bool Source #

getClass :: v -> ExceptT e m c Source #

combineAll :: [c] -> ExceptT e m () Source #

combine :: c -> c -> ExceptT e m c Source #

(===) :: c -> c -> ExceptT e m Bool Source #

desc :: c -> ExceptT e m d Source #

remove :: c -> ExceptT e m Bool Source #

MonadRWS r w s m => MonadRWS r w s (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.RWS.Class
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) Source #
MonadWriter w m => MonadWriter w (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.Writer.Class Methods writer :: (a, w) -> ExceptT e m a Source # tell :: w -> ExceptT e m () Source # listen :: ExceptT e m a -> ExceptT e m (a, w) Source # pass :: ExceptT e m (a, w -> w) -> ExceptT e m a Source #
MonadState s m => MonadState s (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.State.Class Methods get :: ExceptT e m s Source # put :: s -> ExceptT e m () Source # state :: (s -> (a, s)) -> ExceptT e m a Source #
MonadReader r m => MonadReader r (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.Reader.Class Methods ask :: ExceptT e m r Source # local :: (r -> r) -> ExceptT e m a -> ExceptT e m a Source # reader :: (r -> a) -> ExceptT e m a Source #
Monad m => MonadError e (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ExceptT e m a Source # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
MonadTrans (ExceptT e) |
Instance details Defined in Control.Monad.Trans.Except Methods lift :: Monad m => m a -> ExceptT e m a Source #
Monad m => Monad (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods (>>=) :: ExceptT e m a -> (a -> ExceptT e m b) -> ExceptT e m b Source # (>>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b Source # return :: a -> ExceptT e m a Source # fail :: String -> ExceptT e m a Source #
Functor m => Functor (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods fmap :: (a -> b) -> ExceptT e m a -> ExceptT e m b Source # (<$) :: a -> ExceptT e m b -> ExceptT e m a Source #
MonadFix m => MonadFix (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods mfix :: (a -> ExceptT e m a) -> ExceptT e m a Source #
MonadFail m => MonadFail (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods fail :: String -> ExceptT e m a Source #
(Functor m, Monad m) => Applicative (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods pure :: a -> ExceptT e m a Source # (<*>) :: ExceptT e m (a -> b) -> ExceptT e m a -> ExceptT e m b Source # liftA2 :: (a -> b -> c) -> ExceptT e m a -> ExceptT e m b -> ExceptT e m c Source # (*>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b Source # (<*) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m a Source #
Foldable f => Foldable (ExceptT e f) |

Instance details

Defined in Control.Monad.Trans.Except

Methods

fold :: Monoid m => ExceptT e f m -> m Source #

foldMap :: Monoid m => (a -> m) -> ExceptT e f a -> m Source #

foldr :: (a -> b -> b) -> b -> ExceptT e f a -> b Source #

foldr' :: (a -> b -> b) -> b -> ExceptT e f a -> b Source #

foldl :: (b -> a -> b) -> b -> ExceptT e f a -> b Source #

foldl' :: (b -> a -> b) -> b -> ExceptT e f a -> b Source #

foldr1 :: (a -> a -> a) -> ExceptT e f a -> a Source #

foldl1 :: (a -> a -> a) -> ExceptT e f a -> a Source #

toList :: ExceptT e f a -> [a] Source #

null :: ExceptT e f a -> Bool Source #

length :: ExceptT e f a -> Int Source #

elem :: Eq a => a -> ExceptT e f a -> Bool Source #

maximum :: Ord a => ExceptT e f a -> a Source #

minimum :: Ord a => ExceptT e f a -> a Source #

sum :: Num a => ExceptT e f a -> a Source #

product :: Num a => ExceptT e f a -> a Source #

Traversable f => Traversable (ExceptT e f) |
Instance details Defined in Control.Monad.Trans.Except Methods traverse :: Applicative f0 => (a -> f0 b) -> ExceptT e f a -> f0 (ExceptT e f b) Source # sequenceA :: Applicative f0 => ExceptT e f (f0 a) -> f0 (ExceptT e f a) Source # mapM :: Monad m => (a -> m b) -> ExceptT e f a -> m (ExceptT e f b) Source # sequence :: Monad m => ExceptT e f (m a) -> m (ExceptT e f a) Source #
Contravariant m => Contravariant (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods contramap :: (a -> b) -> ExceptT e m b -> ExceptT e m a Source # (>$) :: b -> ExceptT e m b -> ExceptT e m a Source #
(Eq e, Eq1 m) => Eq1 (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods liftEq :: (a -> b -> Bool) -> ExceptT e m a -> ExceptT e m b -> Bool Source #
(Ord e, Ord1 m) => Ord1 (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods liftCompare :: (a -> b -> Ordering) -> ExceptT e m a -> ExceptT e m b -> Ordering Source #
(Read e, Read1 m) => Read1 (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ExceptT e m a) Source # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ExceptT e m a] Source # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (ExceptT e m a) Source # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [ExceptT e m a] Source #
(Show e, Show1 m) => Show1 (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ExceptT e m a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ExceptT e m a] -> ShowS Source #
MonadZip m => MonadZip (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods mzip :: ExceptT e m a -> ExceptT e m b -> ExceptT e m (a, b) Source # mzipWith :: (a -> b -> c) -> ExceptT e m a -> ExceptT e m b -> ExceptT e m c Source # munzip :: ExceptT e m (a, b) -> (ExceptT e m a, ExceptT e m b) Source #
MonadIO m => MonadIO (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods liftIO :: IO a -> ExceptT e m a Source #
(Functor m, Monad m, Monoid e) => Alternative (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods empty :: ExceptT e m a Source # (<|>) :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source # some :: ExceptT e m a -> ExceptT e m [a] Source # many :: ExceptT e m a -> ExceptT e m [a] Source #
(Monad m, Monoid e) => MonadPlus (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods mzero :: ExceptT e m a Source # mplus :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #
MonadThrow m => MonadThrow (ExceptT e m) | Throws exceptions into the base monad.
Instance details Defined in Control.Monad.Catch Methods throwM :: Exception e0 => e0 -> ExceptT e m a Source #
MonadCatch m => MonadCatch (ExceptT e m) | Catches exceptions from the base monad.
Instance details Defined in Control.Monad.Catch Methods catch :: Exception e0 => ExceptT e m a -> (e0 -> ExceptT e m a) -> ExceptT e m a Source #
MonadMask m => MonadMask (ExceptT e m) | Since: exceptions-0.9.0
Instance details Defined in Control.Monad.Catch Methods mask :: ((forall a. ExceptT e m a -> ExceptT e m a) -> ExceptT e m b) -> ExceptT e m b Source # uninterruptibleMask :: ((forall a. ExceptT e m a -> ExceptT e m a) -> ExceptT e m b) -> ExceptT e m b Source # generalBracket :: ExceptT e m a -> (a -> ExitCase b -> ExceptT e m c) -> (a -> ExceptT e m b) -> ExceptT e m (b, c) Source #
PrimMonad m => PrimMonad (ExceptT e m) |
Instance details Defined in Control.Monad.Primitive Associated Types type PrimState (ExceptT e m) :: Type Methods primitive :: (State# (PrimState (ExceptT e m)) -> (#State# (PrimState (ExceptT e m)), a#)) -> ExceptT e m a
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ExceptT err tcm a Source #
MonadTCState m => MonadTCState (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: ExceptT err m TCState Source # putTC :: TCState -> ExceptT err m () Source # modifyTC :: (TCState -> TCState) -> ExceptT err m () Source #
MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ExceptT err m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ExceptT err m a -> ExceptT err m a Source #
MonadReduce m => MonadReduce (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ExceptT err m a Source #
HasOptions m => HasOptions (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source #
ReadTCState m => ReadTCState (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ExceptT err m TCState Source # withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #
MonadDebug m => MonadDebug (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug 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 # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ExceptT err m Definition Source # getConstInfo' :: QName -> ExceptT err m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ExceptT err m RewriteRules Source #
HasBuiltins m => HasBuiltins (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun)) Source #
(Eq e, Eq1 m, Eq a) => Eq (ExceptT e m a) |
Instance details Defined in Control.Monad.Trans.Except Methods (==) :: ExceptT e m a -> ExceptT e m a -> Bool Source # (/=) :: ExceptT e m a -> ExceptT e m a -> Bool Source #
(Ord e, Ord1 m, Ord a) => Ord (ExceptT e m a) |

Instance details

Defined in Control.Monad.Trans.Except

Methods

compare :: ExceptT e m a -> ExceptT e m a -> Ordering Source #

(<) :: ExceptT e m a -> ExceptT e m a -> Bool Source #

(<=) :: ExceptT e m a -> ExceptT e m a -> Bool Source #

(>) :: ExceptT e m a -> ExceptT e m a -> Bool Source #

(>=) :: ExceptT e m a -> ExceptT e m a -> Bool Source #

max :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #

min :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #

(Read e, Read1 m, Read a) => Read (ExceptT e m a) |
Instance details Defined in Control.Monad.Trans.Except Methods readsPrec :: Int -> ReadS (ExceptT e m a) Source # readList :: ReadS [ExceptT e m a] Source # readPrec :: ReadPrec (ExceptT e m a) Source # readListPrec :: ReadPrec [ExceptT e m a] Source #
(Show e, Show1 m, Show a) => Show (ExceptT e m a) |
Instance details Defined in Control.Monad.Trans.Except Methods showsPrec :: Int -> ExceptT e m a -> ShowS Source # show :: ExceptT e m a -> String Source # showList :: [ExceptT e m a] -> ShowS Source #
type PrimState (ExceptT e m) |
Instance details Defined in Control.Monad.Primitive type PrimState (ExceptT e m) = PrimState m

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

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 :: Type -> Type) | m -> e where Source #

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 `MonadError` class. (If you are using the deprecated Control.Monad.Error or Control.Monad.Trans.Error, you may also have to define an `Error` instance.)

Methods

throwError :: e -> m a Source #

Is used within a monadic computation to begin exception processing.

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

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 () Maybe | Since: mtl-2.2.2
Instance details Defined in Control.Monad.Error.Class Methods throwError :: () -> Maybe a Source # catchError :: Maybe a -> (() -> Maybe a) -> Maybe a Source #
MonadError IOException IO |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: IOException -> IO a Source # catchError :: IO a -> (IOException -> IO a) -> IO a Source #
MonadError ParseError Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a Source # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a Source #
MonadError ParseError PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods throwError :: ParseError -> PM a Source # catchError :: PM a -> (ParseError -> PM a) -> PM a Source #
MonadError DeclarationException Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods throwError :: DeclarationException -> Nice a Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a Source #
MonadError TCErr IM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> IM a Source # catchError :: IM a -> (TCErr -> IM a) -> IM a Source #
MonadError TCErr TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods throwError :: TCErr -> TerM a Source # catchError :: TerM a -> (TCErr -> TerM a) -> TerM a Source #
MonadError e m => MonadError e (MaybeT m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> MaybeT m a Source # catchError :: MaybeT m a -> (e -> MaybeT m a) -> MaybeT m a Source #
MonadError e m => MonadError e (ListT m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ListT m a Source # catchError :: ListT m a -> (e -> ListT m a) -> ListT m a Source #
MonadError e (Either e) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> Either e a Source # catchError :: Either e a -> (e -> Either e a) -> Either e a Source #
MonadError TCErr (TCMT IO) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a Source # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a Source #
(Monoid w, MonadError e m) => MonadError e (WriterT w m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> WriterT w m a Source # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a Source #
(Monoid w, MonadError e m) => MonadError e (WriterT w m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> WriterT w m a Source # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a Source #
MonadError e m => MonadError e (StateT s m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> StateT s m a Source # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a Source #
MonadError e m => MonadError e (StateT s m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> StateT s m a Source # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a Source #
MonadError e m => MonadError e (ReaderT r m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ReaderT r m a Source # catchError :: ReaderT r m a -> (e -> ReaderT r m a) -> ReaderT r m a Source #
MonadError e m => MonadError e (IdentityT m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> IdentityT m a Source # catchError :: IdentityT m a -> (e -> IdentityT m a) -> IdentityT m a Source #
Monad m => MonadError e (ExceptT e m) | Since: mtl-2.2
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ExceptT e m a Source # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a Source #
(Monad m, Error e) => MonadError e (ErrorT e m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ErrorT e m a Source # catchError :: ErrorT e m a -> (e -> ErrorT e m a) -> ErrorT e m a Source #
MonadError e m => MonadError e (EquivT s c v m) |
Instance details Defined in Data.Equivalence.Monad Methods throwError :: e -> EquivT s c v m a Source # catchError :: EquivT s c v m a -> (e -> EquivT s c v m a) -> EquivT s c v m a Source #
(Monoid w, MonadError e m) => MonadError e (RWST r w s m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> RWST r w s m a Source # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a Source #
(Monoid w, MonadError e m) => MonadError e (RWST r w s m) |
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> RWST r w s m a Source # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a Source #

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

The inverse of `ExceptT`.