Grisette.Core.Control.Monad.CBMCExcept

CBMC-like error handling

newtype CBMCEither a b

A wrapper type for Either. Uses different merging strategies.

Constructors

CBMCEither

Fields

• runCBMCEither :: Either a b

Instances

(GenSym () a, Mergeable a, GenSym () b, Mergeable b) => GenSym () (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => () -> m (UnionM (CBMCEither a b))

(Lift a, Lift b) => Lift (CBMCEither a b :: Type)

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)

Eq a => Eq1 (CBMCEither a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

liftEq :: (a0 -> b -> Bool) -> CBMCEither a a0 -> CBMCEither a b -> Bool

Ord a => Ord1 (CBMCEither a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

liftCompare :: (a0 -> b -> Ordering) -> CBMCEither a a0 -> CBMCEither a b -> Ordering

Read a => Read1 (CBMCEither a)

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)

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)

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)

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)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

liftRootStrategy :: MergingStrategy a -> MergingStrategy (CBMCEither e a)

UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v

Defined in Grisette.Core.Control.Monad.UnionM

Methods

extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v)

Generic (CBMCEither a b)

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)

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)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

rnf :: CBMCEither a b -> ()

(Eq a, Eq b) => Eq (CBMCEither a b)

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)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(==~) :: CBMCEither e a -> CBMCEither e a -> SymBool

(/=~) :: CBMCEither e a -> CBMCEither e a -> SymBool

(EvaluateSym a, EvaluateSym b) => EvaluateSym (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

evaluateSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b

(ExtractSymbolics a, ExtractSymbolics b) => ExtractSymbolics (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

extractSymbolics :: CBMCEither a b -> SymbolSet

(Mergeable e, Mergeable a) => Mergeable (CBMCEither e a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

rootStrategy :: MergingStrategy (CBMCEither e a)

(SOrd a, SOrd b) => SOrd (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(<~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(<=~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(>~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(>=~) :: CBMCEither a b -> CBMCEither a b -> SymBool

symCompare :: CBMCEither a b -> CBMCEither a b -> UnionM Ordering

(Hashable a, Hashable b) => Hashable (CBMCEither a b)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => CBMCEither a b -> m (UnionM (CBMCEither a b))

(GenSymSimple a a, GenSymSimple b b) => GenSymSimple (CBMCEither a b) (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m => CBMCEither a b -> m (CBMCEither a b)

(ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: Either e1 a1 -> Maybe (CBMCEither e2 a2)

(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (Either e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCEither e1 a1 -> Maybe (Either e2 a2)

(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCEither e1 a1 -> Maybe (CBMCEither e2 a2)

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: Either e1 a1 -> CBMCEither e2 a2

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> Either e2 a2

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2

type Rep (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

type Rep (CBMCEither a b) = D1 ('MetaData "CBMCEither" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "CBMCEither" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCEither") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either a b))))

newtype CBMCExceptT e m a

Similar to ExceptT, but with different error handling mechanism.

Constructors

CBMCExceptT

Fields

• runCBMCExceptT :: m (CBMCEither e a)

Instances

Monad m => MonadError e (CBMCExceptT e m)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => spec -> m0 (UnionM (CBMCExceptT a m b))

GenSymSimple spec (m (CBMCEither a b)) => GenSymSimple spec (CBMCExceptT a m b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m0 => spec -> m0 (CBMCExceptT a m b)

MonadTrans (CBMCExceptT e)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

lift :: Monad m => m a -> CBMCExceptT e m a

Functor m => Generic1 (CBMCExceptT e m :: Type -> Type)

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

MonadFail m => MonadFail (CBMCExceptT e m)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fail :: String -> CBMCExceptT e m a

MonadFix m => MonadFix (CBMCExceptT e m)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

mfix :: (a -> CBMCExceptT e m a) -> CBMCExceptT e m a

MonadIO m => MonadIO (CBMCExceptT e m)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

liftIO :: IO a -> CBMCExceptT e m a

MonadZip m => MonadZip (CBMCExceptT e m)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

liftRootStrategy :: MergingStrategy a -> MergingStrategy (CBMCExceptT e m a)

(UnionLike m, Mergeable e) => SimpleMergeable1 (CBMCExceptT e m)

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

(UnionLike m, Mergeable e) => UnionLike (CBMCExceptT e m)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

single :: a -> CBMCExceptT e m a

unionIf :: SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a

mergeWithStrategy :: MergingStrategy a -> CBMCExceptT e m a -> CBMCExceptT e m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> CBMCExceptT e m a

Generic (CBMCExceptT e m a)

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)

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)

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)

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)

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)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(==~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(/=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

EvaluateSym (m (CBMCEither e a)) => EvaluateSym (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

evaluateSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a

ExtractSymbolics (m (CBMCEither e a)) => ExtractSymbolics (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

extractSymbolics :: CBMCExceptT e m a -> SymbolSet

(Mergeable1 m, Mergeable e, Mergeable a) => Mergeable (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

rootStrategy :: MergingStrategy (CBMCExceptT e m a)

SOrd (m (CBMCEither e a)) => SOrd (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(<~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(<=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(>~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(>=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> UnionM Ordering

(UnionLike m, Mergeable e, Mergeable a) => SimpleMergeable (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

mrgIte :: SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a

(Monad u, UnionLike u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

extractUnionExcept :: CBMCExceptT e u v -> u (Either e v)

ToCon (m1 (CBMCEither e1 a)) (Either e2 b) => ToCon (CBMCExceptT e1 m1 a) (Either e2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCExceptT e1 m1 a -> Maybe (Either e2 b)

(GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSym (CBMCExceptT e m a) (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (UnionM (CBMCExceptT e m a))

GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)) => GenSymSimple (CBMCExceptT e m a) (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (CBMCExceptT e m a)

ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCExceptT e1 m1 a -> Maybe (CBMCExceptT e2 m2 b)

ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b

type Rep1 (CBMCExceptT e m :: Type -> Type)

Defined in Grisette.Core.Control.Monad.CBMCExcept

type Rep1 (CBMCExceptT e m :: Type -> Type) = D1 ('MetaData "CBMCExceptT" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "CBMCExceptT" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCExceptT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (m :.: Rec1 (CBMCEither e))))

type Rep (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

type Rep (CBMCExceptT e m a) = D1 ('MetaData "CBMCExceptT" "Grisette.Core.Control.Monad.CBMCExcept" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" '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

Wrap an Either value in CBMCExceptT

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

Map the error and values in a CBMCExceptT

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

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

MonadError IOException IO

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

Defined in Control.Monad.Error.Class

Methods

throwError :: () -> Maybe a

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

MonadError e (Either e)

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)

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)

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)

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)

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)

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)

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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