grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Control.Monad.CBMCExcept

Description

 
Synopsis

CBMC-like error handling

newtype CBMCEither a b Source #

A wrapper type for Either. Uses different merging strategies.

Constructors

CBMCEither 

Fields

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 #

(Lift a, Lift b) => Lift (CBMCEither a b :: Type) 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) #

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

UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

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

(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

(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

(Mergeable e, Mergeable a) => Mergeable (CBMCEither e a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

(SOrd a, SOrd b) => SOrd (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

(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.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 Source #

Similar to ExceptT, but with different error handling mechanism.

Constructors

CBMCExceptT 

Fields

Instances

Instances details
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 #

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 #

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

(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

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

(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

(Mergeable1 m, Mergeable e, Mergeable a) => Mergeable (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

SOrd (m (CBMCEither e a)) => SOrd (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

(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.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) 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.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 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 #