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.Internal.Core.Control.Monad.CBMCExcept

Contents

CBMC-like error handling

Description

Synopsis

newtype CBMCEither a b = CBMCEither {
- runCBMCEither :: Either a b
}
newtype CBMCExceptT e (m :: Type -> Type) a = CBMCExceptT {
- runCBMCExceptT :: m (CBMCEither e a)
}
cbmcExcept :: forall (m :: Type -> Type) e a. 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 :: forall (m :: Type -> Type) e e' a. 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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => () -> m (Union (CBMCEither a b)) Source #

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

Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

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

UnionWithExcept (Union (CBMCEither e v)) Union e v Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

extractUnionExcept :: Union (CBMCEither e v) -> Union (Either e v) Source #

(NFData a, NFData b) => NFData (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

rnf :: CBMCEither a b -> () #

Generic (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Associated Types

type Rep (CBMCEither a b)
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept type Rep (CBMCEither a b) = D1 ('MetaData "CBMCEither" "Grisette.Internal.Core.Control.Monad.CBMCExcept" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "CBMCEither" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCEither") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either a b))))

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.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

showsPrec :: Int -> CBMCEither a b -> ShowS #

show :: CBMCEither a b -> String #

showList :: [CBMCEither a b] -> ShowS #

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

Instance details

Defined in Grisette.Internal.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.Internal.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 #

(EvalSym a, EvalSym b) => EvalSym (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

evalSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b Source #

(ExtractSym a, ExtractSym b) => ExtractSym (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

extractSym :: CBMCEither a b -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => CBMCEither a b -> Maybe (SymbolSet knd) Source #

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

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

rootStrategy :: MergingStrategy (CBMCEither e a) Source #

sortIndices :: CBMCEither e a -> [DynamicSortedIdx] Source #

(SymEq e, SymEq a) => SymEq (CBMCEither e a) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

(.==) :: CBMCEither e a -> CBMCEither e a -> SymBool Source #

(./=) :: CBMCEither e a -> CBMCEither e a -> SymBool Source #

symDistinct :: [CBMCEither e a] -> SymBool Source #

(SymOrd a, SymOrd b) => SymOrd (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.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 -> Union Ordering Source #

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

Instance details

Defined in Grisette.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => CBMCEither a b -> m (Union (CBMCEither a b)) Source #

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

Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source #

type Rep (CBMCEither a b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

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

newtype CBMCExceptT e (m :: Type -> Type) 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.Internal.Core.Control.Monad.CBMCExcept

Associated Types

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

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

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

Methods

from1 :: CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a #

to1 :: Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a #

Monad m => MonadError e (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => spec -> m0 (Union (CBMCExceptT a m b)) Source #

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

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

MonadTrans (CBMCExceptT e) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

MonadIO m => MonadIO (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

liftIO :: IO a -> CBMCExceptT e m a #

MonadZip m => MonadZip (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.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) #

(Eq e, Eq1 m) => Eq1 (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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 #

(Functor m, Monad m, Monoid e) => Alternative (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

mzero :: CBMCExceptT e m a #

mplus :: CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a #

MonadFail m => MonadFail (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

fail :: String -> CBMCExceptT e m a #

MonadFix m => MonadFix (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

Foldable f => Foldable (CBMCExceptT e f) Source #

Instance details

Defined in Grisette.Internal.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 #

Traversable f => Traversable (CBMCExceptT e f) Source #

Instance details

Defined in Grisette.Internal.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) #

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

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

(SymBranching m, Mergeable e) => SimpleMergeable1 (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source #

(SymBranching m, Mergeable e) => SymBranching (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

mrgIfPropagatedStrategy :: SymBool -> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a Source #

(TryMerge m, Mergeable e) => TryMerge (CBMCExceptT e m) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

tryMergeWithStrategy :: MergingStrategy a -> CBMCExceptT e m a -> CBMCExceptT e m a Source #

Generic (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Associated Types

type Rep (CBMCExceptT e m a)

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

type Rep (CBMCExceptT e m a) = D1 ('MetaData "CBMCExceptT" "Grisette.Internal.Core.Control.Monad.CBMCExcept" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "CBMCExceptT" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCExceptT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (m (CBMCEither e a)))))

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.Internal.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.Internal.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.Internal.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.Internal.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 #

EvalSym (m (CBMCEither e a)) => EvalSym (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

evalSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a Source #

ExtractSym (m (CBMCEither e a)) => ExtractSym (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

extractSym :: CBMCExceptT e m a -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => CBMCExceptT e m a -> Maybe (SymbolSet knd) Source #

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

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

rootStrategy :: MergingStrategy (CBMCExceptT e m a) Source #

sortIndices :: CBMCExceptT e m a -> [DynamicSortedIdx] Source #

(SymBranching m, Mergeable e, Mergeable a) => SimpleMergeable (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

SymEq (m (CBMCEither e a)) => SymEq (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.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 #

symDistinct :: [CBMCExceptT e m a] -> SymBool Source #

SymOrd (m (CBMCEither e a)) => SymOrd (CBMCExceptT e m a) Source #

Instance details

Defined in Grisette.Internal.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 -> Union Ordering Source #

(Monad u, TryMerge u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source #

Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (Union (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.Internal.Core.Control.Monad.CBMCExcept

Methods

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

(ToCon1 m1 m2, ToCon e1 e2, ToCon a b) => ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source #

Instance details

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

(ToSym e1 e2, ToSym a b, ToSym1 m1 m2) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source #

Instance details

Defined in Grisette.Internal.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.Internal.Core.Control.Monad.CBMCExcept

type Rep1 (CBMCExceptT e m :: Type -> Type) = D1 ('MetaData "CBMCExceptT" "Grisette.Internal.Core.Control.Monad.CBMCExcept" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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.Internal.Core.Control.Monad.CBMCExcept

type Rep (CBMCExceptT e m a) = D1 ('MetaData "CBMCExceptT" "Grisette.Internal.Core.Control.Monad.CBMCExcept" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "CBMCExceptT" 'PrefixI 'True) (S1 ('MetaSel ('Just "runCBMCExceptT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (m (CBMCEither e a)))))

cbmcExcept :: forall (m :: Type -> Type) e a. 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 :: forall (m :: Type -> Type) e e' a. 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 String Alloc
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Alloc a # catchError :: Alloc a -> (String -> Alloc a) -> Alloc a #
MonadError String Eval
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Eval a # catchError :: Eval a -> (String -> Eval a) -> Eval a #
MonadError String Q
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods throwError :: String -> Q a # catchError :: Q a -> (String -> Q a) -> Q 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.Internal.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 (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.Internal.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 #
(Monoid w, MonadError e m) => MonadError e (AccumT w m)	Since: mtl-2.3
Instance details Defined in Control.Monad.Error.Class Methods throwError :: e -> AccumT w m a # catchError :: AccumT w m a -> (e -> AccumT w m a) -> AccumT w 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)	Since: mtl-2.3
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 (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)	Since: mtl-2.3
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 #
(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 #

Key	Shortcut
s	Open this search box
esc	Close this search box
↓,ctrl + j	Move down in search results
↑,ctrl + k	Move up in search results
↵	Go to active search result