Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Control.Monad.CBMCExcept

Contents

CBMC-like error handling

Description

Synopsis

newtype CBMCEither a b = CBMCEither {
- runCBMCEither :: Either a b
}
newtype CBMCExceptT e m a = CBMCExceptT {
- runCBMCExceptT :: m (CBMCEither e a)
}
cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a
mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b
withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT 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

CBMC-like error handling

newtype CBMCEither a b Source #

A wrapper type for Either. Uses different merging strategies.

Constructors

CBMCEither
Fields runCBMCEither :: Either a b

Instances

Instances details

(GenSym () a, Mergeable a, GenSym () b, Mergeable b) => GenSym () (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fresh :: MonadFresh m => () -> m (UnionM (CBMCEither a b)) Source #
Eq a => Eq1 (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftEq :: (a0 -> b -> Bool) -> CBMCEither a a0 -> CBMCEither a b -> Bool #
Ord a => Ord1 (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftCompare :: (a0 -> b -> Ordering) -> CBMCEither a a0 -> CBMCEither a b -> Ordering #
Read a => Read1 (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftReadsPrec :: (Int -> ReadS a0) -> ReadS [a0] -> Int -> ReadS (CBMCEither a a0) # liftReadList :: (Int -> ReadS a0) -> ReadS [a0] -> ReadS [CBMCEither a a0] # liftReadPrec :: ReadPrec a0 -> ReadPrec [a0] -> ReadPrec (CBMCEither a a0) # liftReadListPrec :: ReadPrec a0 -> ReadPrec [a0] -> ReadPrec [CBMCEither a a0] #
Show a => Show1 (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftShowsPrec :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> Int -> CBMCEither a a0 -> ShowS # liftShowList :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> [CBMCEither a a0] -> ShowS #
Applicative (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods pure :: a0 -> CBMCEither a a0 # (<>) :: CBMCEither a (a0 -> b) -> CBMCEither a a0 -> CBMCEither a b # liftA2 :: (a0 -> b -> c) -> CBMCEither a a0 -> CBMCEither a b -> CBMCEither a c # (>) :: CBMCEither a a0 -> CBMCEither a b -> CBMCEither a b # (<*) :: CBMCEither a a0 -> CBMCEither a b -> CBMCEither a a0 #
Functor (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fmap :: (a0 -> b) -> CBMCEither a a0 -> CBMCEither a b # (<$) :: a0 -> CBMCEither a b -> CBMCEither a a0 #
Monad (CBMCEither a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (>>=) :: CBMCEither a a0 -> (a0 -> CBMCEither a b) -> CBMCEither a b # (>>) :: CBMCEither a a0 -> CBMCEither a b -> CBMCEither a b # return :: a0 -> CBMCEither a a0 #
Mergeable e => Mergeable1 (CBMCEither e) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftRootStrategy :: MergingStrategy a -> MergingStrategy (CBMCEither e a) Source #
UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v) Source #
(Lift a, Lift b) => Lift (CBMCEither a b :: TYPE LiftedRep) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods lift :: Quote m => CBMCEither a b -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => CBMCEither a b -> Code m (CBMCEither a b) #
Generic (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Associated Types type Rep (CBMCEither a b) :: Type -> Type # Methods from :: CBMCEither a b -> Rep (CBMCEither a b) x # to :: Rep (CBMCEither a b) x -> CBMCEither a b #
(Read a, Read b) => Read (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods readsPrec :: Int -> ReadS (CBMCEither a b) # readList :: ReadS [CBMCEither a b] # readPrec :: ReadPrec (CBMCEither a b) # readListPrec :: ReadPrec [CBMCEither a b] #
(Show a, Show b) => Show (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods showsPrec :: Int -> CBMCEither a b -> ShowS # show :: CBMCEither a b -> String # showList :: [CBMCEither a b] -> ShowS #
(NFData a, NFData b) => NFData (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods rnf :: CBMCEither a b -> () #
(Eq a, Eq b) => Eq (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (==) :: CBMCEither a b -> CBMCEither a b -> Bool # (/=) :: CBMCEither a b -> CBMCEither a b -> Bool #
(Ord a, Ord b) => Ord (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods compare :: CBMCEither a b -> CBMCEither a b -> Ordering # (<) :: CBMCEither a b -> CBMCEither a b -> Bool # (<=) :: CBMCEither a b -> CBMCEither a b -> Bool # (>) :: CBMCEither a b -> CBMCEither a b -> Bool # (>=) :: CBMCEither a b -> CBMCEither a b -> Bool # max :: CBMCEither a b -> CBMCEither a b -> CBMCEither a b # min :: CBMCEither a b -> CBMCEither a b -> CBMCEither a b #
(SEq e, SEq a) => SEq (CBMCEither e a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (==~) :: CBMCEither e a -> CBMCEither e a -> SymBool Source # (/=~) :: CBMCEither e a -> CBMCEither e a -> SymBool Source #
(EvaluateSym a, EvaluateSym b) => EvaluateSym (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods evaluateSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b Source #
(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractSymbolics :: CBMCEither a b -> SymbolSet Source #
(Mergeable e, Mergeable a) => Mergeable (CBMCEither e a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods rootStrategy :: MergingStrategy (CBMCEither e a) Source #
(SOrd a, SOrd b) => SOrd (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (<~) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (<=~) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (>~) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (>=~) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # symCompare :: CBMCEither a b -> CBMCEither a b -> UnionM Ordering Source #
(Hashable a, Hashable b) => Hashable (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods hashWithSalt :: Int -> CBMCEither a b -> Int # hash :: CBMCEither a b -> Int #
(GenSymSimple a a, Mergeable a, GenSymSimple b b, Mergeable b) => GenSym (CBMCEither a b) (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fresh :: MonadFresh m => CBMCEither a b -> m (UnionM (CBMCEither a b)) Source #
(GenSymSimple a a, GenSymSimple b b) => GenSymSimple (CBMCEither a b) (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods simpleFresh :: MonadFresh m => CBMCEither a b -> m (CBMCEither a b) Source #
(ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (CBMCEither e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toCon :: Either e1 a1 -> Maybe (CBMCEither e2 a2) Source #
(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (Either e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCEither e1 a1 -> Maybe (Either e2 a2) Source #
(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (CBMCEither e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCEither e1 a1 -> Maybe (CBMCEither e2 a2) Source #
(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toSym :: Either e1 a1 -> CBMCEither e2 a2 Source #
(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCEither e1 a1 -> Either e2 a2 Source #
(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (CBMCEither e2 a2) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source #
type Rep (CBMCEither a b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept type Rep (CBMCEither a b) = D1 ('MetaData "CBMCEither" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "CBMCEither" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCEither") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either a b))))

newtype CBMCExceptT e m a Source #

Similar to ExceptT, but with different error handling mechanism.

Constructors

CBMCExceptT
Fields runCBMCExceptT :: m (CBMCEither e a)

Instances

Instances details

Functor m => Generic1 (CBMCExceptT e m :: Type -> Type) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Associated Types type Rep1 (CBMCExceptT e m) :: k -> Type # Methods from1 :: forall (a :: k). CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a # to1 :: forall (a :: k). Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a #
Monad m => MonadError e (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods throwError :: e -> CBMCExceptT e m a # catchError :: CBMCExceptT e m a -> (e -> CBMCExceptT e m a) -> CBMCExceptT e m a #
(GenSym spec (m (CBMCEither a b)), Mergeable1 m, Mergeable a, Mergeable b) => GenSym spec (CBMCExceptT a m b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fresh :: MonadFresh m0 => spec -> m0 (UnionM (CBMCExceptT a m b)) Source #
GenSymSimple spec (m (CBMCEither a b)) => GenSymSimple spec (CBMCExceptT a m b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods simpleFresh :: MonadFresh m0 => spec -> m0 (CBMCExceptT a m b) Source #
MonadTrans (CBMCExceptT e) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods lift :: Monad m => m a -> CBMCExceptT e m a #
MonadFail m => MonadFail (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fail :: String -> CBMCExceptT e m a #
MonadFix m => MonadFix (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods mfix :: (a -> CBMCExceptT e m a) -> CBMCExceptT e m a #
MonadIO m => MonadIO (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftIO :: IO a -> CBMCExceptT e m a #
MonadZip m => MonadZip (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods mzip :: CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m (a, b) # mzipWith :: (a -> b -> c) -> CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m c # munzip :: CBMCExceptT e m (a, b) -> (CBMCExceptT e m a, CBMCExceptT e m b) #
Foldable f => Foldable (CBMCExceptT e f) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fold :: Monoid m => CBMCExceptT e f m -> m # foldMap :: Monoid m => (a -> m) -> CBMCExceptT e f a -> m # foldMap' :: Monoid m => (a -> m) -> CBMCExceptT e f a -> m # foldr :: (a -> b -> b) -> b -> CBMCExceptT e f a -> b # foldr' :: (a -> b -> b) -> b -> CBMCExceptT e f a -> b # foldl :: (b -> a -> b) -> b -> CBMCExceptT e f a -> b # foldl' :: (b -> a -> b) -> b -> CBMCExceptT e f a -> b # foldr1 :: (a -> a -> a) -> CBMCExceptT e f a -> a # foldl1 :: (a -> a -> a) -> CBMCExceptT e f a -> a # toList :: CBMCExceptT e f a -> [a] # null :: CBMCExceptT e f a -> Bool # length :: CBMCExceptT e f a -> Int # elem :: Eq a => a -> CBMCExceptT e f a -> Bool # maximum :: Ord a => CBMCExceptT e f a -> a # minimum :: Ord a => CBMCExceptT e f a -> a # sum :: Num a => CBMCExceptT e f a -> a # product :: Num a => CBMCExceptT e f a -> a #
(Eq e, Eq1 m) => Eq1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftEq :: (a -> b -> Bool) -> CBMCExceptT e m a -> CBMCExceptT e m b -> Bool #
(Ord e, Ord1 m) => Ord1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftCompare :: (a -> b -> Ordering) -> CBMCExceptT e m a -> CBMCExceptT e m b -> Ordering #
(Read e, Read1 m) => Read1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCExceptT e m a) # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCExceptT e m a] # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (CBMCExceptT e m a) # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [CBMCExceptT e m a] #
(Show e, Show1 m) => Show1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> CBMCExceptT e m a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCExceptT e m a] -> ShowS #
Contravariant m => Contravariant (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods contramap :: (a' -> a) -> CBMCExceptT e m a -> CBMCExceptT e m a' # (>$) :: b -> CBMCExceptT e m b -> CBMCExceptT e m a #
Traversable f => Traversable (CBMCExceptT e f) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods traverse :: Applicative f0 => (a -> f0 b) -> CBMCExceptT e f a -> f0 (CBMCExceptT e f b) # sequenceA :: Applicative f0 => CBMCExceptT e f (f0 a) -> f0 (CBMCExceptT e f a) # mapM :: Monad m => (a -> m b) -> CBMCExceptT e f a -> m (CBMCExceptT e f b) # sequence :: Monad m => CBMCExceptT e f (m a) -> m (CBMCExceptT e f a) #
(Functor m, Monad m, Monoid e) => Alternative (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods empty :: CBMCExceptT e m a # (<\|>) :: CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a # some :: CBMCExceptT e m a -> CBMCExceptT e m [a] # many :: CBMCExceptT e m a -> CBMCExceptT e m [a] #
(Functor m, Monad m) => Applicative (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods pure :: a -> CBMCExceptT e m a # (<>) :: CBMCExceptT e m (a -> b) -> CBMCExceptT e m a -> CBMCExceptT e m b # liftA2 :: (a -> b -> c) -> CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m c # (>) :: CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m b # (<*) :: CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m a #
Functor m => Functor (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fmap :: (a -> b) -> CBMCExceptT e m a -> CBMCExceptT e m b # (<$) :: a -> CBMCExceptT e m b -> CBMCExceptT e m a #
Monad m => Monad (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (>>=) :: CBMCExceptT e m a -> (a -> CBMCExceptT e m b) -> CBMCExceptT e m b # (>>) :: CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m b # return :: a -> CBMCExceptT e m a #
(Monad m, Monoid e) => MonadPlus (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods mzero :: CBMCExceptT e m a # mplus :: CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a #
(Mergeable1 m, Mergeable e) => Mergeable1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftRootStrategy :: MergingStrategy a -> MergingStrategy (CBMCExceptT e m a) Source #
(UnionLike m, Mergeable e) => SimpleMergeable1 (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source #
(UnionLike m, Mergeable e) => UnionLike (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods single :: a -> CBMCExceptT e m a Source # unionIf :: SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source # mergeWithStrategy :: MergingStrategy a -> CBMCExceptT e m a -> CBMCExceptT e m a Source # mrgIfWithStrategy :: MergingStrategy a -> SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source # mrgSingleWithStrategy :: MergingStrategy a -> a -> CBMCExceptT e m a Source #
Generic (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Associated Types type Rep (CBMCExceptT e m a) :: Type -> Type # Methods from :: CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x # to :: Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a #
(Read e, Read1 m, Read a) => Read (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods readsPrec :: Int -> ReadS (CBMCExceptT e m a) # readList :: ReadS [CBMCExceptT e m a] # readPrec :: ReadPrec (CBMCExceptT e m a) # readListPrec :: ReadPrec [CBMCExceptT e m a] #
(Show e, Show1 m, Show a) => Show (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods showsPrec :: Int -> CBMCExceptT e m a -> ShowS # show :: CBMCExceptT e m a -> String # showList :: [CBMCExceptT e m a] -> ShowS #
(Eq e, Eq1 m, Eq a) => Eq (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (==) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool # (/=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool #
(Ord e, Ord1 m, Ord a) => Ord (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods compare :: CBMCExceptT e m a -> CBMCExceptT e m a -> Ordering # (<) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool # (<=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool # (>) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool # (>=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool # max :: CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a # min :: CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a #
SEq (m (CBMCEither e a)) => SEq (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (==~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (/=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source #
EvaluateSym (m (CBMCEither e a)) => EvaluateSym (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods evaluateSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a Source #
ExtractSymbolics (m (CBMCEither e a)) => ExtractSymbolics (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractSymbolics :: CBMCExceptT e m a -> SymbolSet Source #
(Mergeable1 m, Mergeable e, Mergeable a) => Mergeable (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods rootStrategy :: MergingStrategy (CBMCExceptT e m a) Source #
SOrd (m (CBMCEither e a)) => SOrd (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods (<~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (<=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (>~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (>=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> UnionM Ordering Source #
(UnionLike m, Mergeable e, Mergeable a) => SimpleMergeable (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods mrgIte :: SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source #
(Monad u, UnionLike u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: CBMCExceptT e u v -> u (Either e v) Source #
ToCon (m1 (CBMCEither e1 a)) (Either e2 b) => ToCon (CBMCExceptT e1 m1 a) (Either e2 b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCExceptT e1 m1 a -> Maybe (Either e2 b) Source #
(GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSym (CBMCExceptT e m a) (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods fresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (UnionM (CBMCExceptT e m a)) Source #
GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)) => GenSymSimple (CBMCExceptT e m a) (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods simpleFresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (CBMCExceptT e m a) Source #
ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCExceptT e1 m1 a -> Maybe (CBMCExceptT e2 m2 b) Source #
ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b Source #
type Rep1 (CBMCExceptT e m :: Type -> Type) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept type Rep1 (CBMCExceptT e m :: Type -> Type) = D1 ('MetaData "CBMCExceptT" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "CBMCExceptT" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCExceptT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (m :.: Rec1 (CBMCEither e))))
type Rep (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept type Rep (CBMCExceptT e m a) = D1 ('MetaData "CBMCExceptT" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "CBMCExceptT" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCExceptT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (m (CBMCEither e a)))))

cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a Source #

Wrap an Either value in CBMCExceptT

mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b Source #

Map the error and values in a CBMCExceptT

withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a Source #

Map the error in a CBMCExceptT

class Monad m => MonadError e (m :: Type -> Type) | 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 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 #

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

Instances details

MonadError IOException IO
Instance details Defined in Control.Monad.Error.Class Methods throwError :: IOException -> IO a # catchError :: IO a -> (IOException -> IO a) -> IO a #
MonadError () Maybe	Since: mtl-2.2.2
Instance details Defined in Control.Monad.Error.Class Methods throwError :: () -> Maybe a # catchError :: Maybe a -> (() -> Maybe a) -> Maybe a #
MonadError e (Either e)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> Either e a # catchError :: Either e a -> (e -> Either e a) -> Either e a #
MonadError e m => MonadError e (FreshT m) Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods throwError :: e -> FreshT m a # catchError :: FreshT m a -> (e -> FreshT m a) -> FreshT m a #
MonadError e m => MonadError e (QueryT m)
Instance details Defined in Data.SBV.Core.Symbolic Methods throwError :: e -> QueryT m a # catchError :: QueryT m a -> (e -> QueryT m a) -> QueryT m a #
MonadError e m => MonadError e (SymbolicT m)
Instance details Defined in Data.SBV.Core.Symbolic Methods throwError :: e -> SymbolicT m a # catchError :: SymbolicT m a -> (e -> SymbolicT m a) -> SymbolicT m a #
MonadError e m => MonadError e (ListT m)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ListT m a # catchError :: ListT m a -> (e -> ListT m a) -> ListT m a #
MonadError e m => MonadError e (MaybeT m)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> MaybeT m a # catchError :: MaybeT m a -> (e -> MaybeT m a) -> MaybeT m a #
Monad m => MonadError e (CBMCExceptT e m) Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods throwError :: e -> CBMCExceptT e m a # catchError :: CBMCExceptT e m a -> (e -> CBMCExceptT e m a) -> CBMCExceptT e m a #
(Monad m, Error e) => MonadError e (ErrorT e m)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> ErrorT e m a # catchError :: ErrorT e m a -> (e -> ErrorT e m a) -> ErrorT e m a #
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 # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a #
MonadError e m => MonadError e (IdentityT m)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> IdentityT m a # catchError :: IdentityT m a -> (e -> IdentityT m a) -> IdentityT m a #
MonadError e m => MonadError e (ReaderT r m)
Instance details Defined in Control.Monad.Error.Class 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 (StateT s m)
Instance details Defined in Control.Monad.Error.Class 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)
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> StateT s m a # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a #
(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 # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a #
(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 # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a #
(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 # 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)
Instance details Defined in Control.Monad.Error.Class 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 #