Grisette.Core.Data.Class.SimpleMergeable

Simple mergeable types

class Mergeable a => SimpleMergeable a where

This class indicates that a type has a simple root merge strategy.

Note: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ...
  deriving Generic
  deriving (Mergeable, SimpleMergeable) via (Default X)

Methods

mrgIte :: SymBool -> a -> a -> a

Performs if-then-else with the simple root merge strategy.

>>> mrgIte "a" "b" "c" :: SymInteger
(ite a b c)

Instances

SimpleMergeable AssertionError

Defined in Grisette.Core.Control.Exception

Methods

mrgIte :: SymBool -> AssertionError -> AssertionError -> AssertionError

SimpleMergeable CEGISCondition

Defined in Grisette.Core.Data.Class.CEGISSolver

Methods

mrgIte :: SymBool -> CEGISCondition -> CEGISCondition -> CEGISCondition

SimpleMergeable FreshIndex

Defined in Grisette.Core.Data.Class.GenSym

Methods

mrgIte :: SymBool -> FreshIndex -> FreshIndex -> FreshIndex

SimpleMergeable ()

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> () -> () -> ()

SimpleMergeable a => SimpleMergeable (Identity a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Identity a -> Identity a -> Identity a

(Generic a, Mergeable' (Rep a), SimpleMergeable' (Rep a)) => SimpleMergeable (Default a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Default a -> Default a -> Default a

Mergeable a => SimpleMergeable (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a

Mergeable a => SimpleMergeable (Union a)

Defined in Grisette.Core.Data.Union

Methods

mrgIte :: SymBool -> Union a -> Union a -> Union a

SupportedPrim a => SimpleMergeable (Sym a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Sym a -> Sym a -> Sym a

(UnionLike m, Mergeable a) => SimpleMergeable (FreshT m a)

Defined in Grisette.Core.Data.Class.GenSym

Methods

mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a

(UnionLike m, Mergeable a) => SimpleMergeable (MaybeT m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a

(IsConcrete k, Mergeable t) => SimpleMergeable (HashMap k (UnionM (Maybe t)))

Defined in Grisette.Core.Control.Monad.UnionM

Methods

mrgIte :: SymBool -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t))

SimpleMergeable b => SimpleMergeable (a -> b)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a -> b) -> (a -> b) -> a -> b

(SimpleMergeable a, SimpleMergeable b) => SimpleMergeable (a, b)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b) -> (a, b) -> (a, b)

(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

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

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(UnionLike m, Mergeable a) => SimpleMergeable (IdentityT m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a

(Mergeable a, UnionLike m) => SimpleMergeable (ReaderT s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a

(Mergeable s, Mergeable a, UnionLike m) => SimpleMergeable (StateT s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a

(Mergeable s, Mergeable a, UnionLike m) => SimpleMergeable (StateT s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a

(Mergeable s, Mergeable a, UnionLike m, Monoid s) => SimpleMergeable (WriterT s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

(Mergeable s, Mergeable a, UnionLike m, Monoid s) => SimpleMergeable (WriterT s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c) => SimpleMergeable (a, b, c)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c) -> (a, b, c) -> (a, b, c)

(UnionLike m, Mergeable r) => SimpleMergeable (ContT r m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> ContT r m a -> ContT r m a -> ContT r m a

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d) => SimpleMergeable (a, b, c, d)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

(Mergeable s, Mergeable w, Monoid w, Mergeable a, UnionLike m) => SimpleMergeable (RWST r w s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

(Mergeable s, Mergeable w, Monoid w, Mergeable a, UnionLike m) => SimpleMergeable (RWST r w s m a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e) => SimpleMergeable (a, b, c, d, e)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e, SimpleMergeable f) => SimpleMergeable (a, b, c, d, e, f)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e, SimpleMergeable f, SimpleMergeable g) => SimpleMergeable (a, b, c, d, e, f, g)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e, SimpleMergeable f, SimpleMergeable g, SimpleMergeable h) => SimpleMergeable (a, b, c, d, e, f, g, h)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

class SimpleMergeable1 u where

Lifting of the SimpleMergeable class to unary type constructors.

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a

Lift mrgIte through the type constructor.

>>> liftMrgIte mrgIte "a" (Identity "b") (Identity "c") :: Identity SymInteger
Identity (ite a b c)

Instances

SimpleMergeable1 Identity

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Identity a -> Identity a -> Identity a

SimpleMergeable1 UnionM

Defined in Grisette.Core.Control.Monad.UnionM

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> UnionM a -> UnionM a -> UnionM a

SimpleMergeable1 Union

Defined in Grisette.Core.Data.Union

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Union a -> Union a -> Union a

UnionLike m => SimpleMergeable1 (FreshT m)

Defined in Grisette.Core.Data.Class.GenSym

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> FreshT m a -> FreshT m a -> FreshT m a

UnionLike m => SimpleMergeable1 (MaybeT m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a

SimpleMergeable a => SimpleMergeable1 ((,) a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a0 -> a0 -> a0) -> SymBool -> (a, a0) -> (a, a0) -> (a, a0)

(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) => SimpleMergeable1 (ExceptT e m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> ExceptT e m a -> ExceptT e m a -> ExceptT e m a

UnionLike m => SimpleMergeable1 (IdentityT m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a

UnionLike m => SimpleMergeable1 (ReaderT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a

(Mergeable s, UnionLike m) => SimpleMergeable1 (StateT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a

(Mergeable s, UnionLike m) => SimpleMergeable1 (StateT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a

(Mergeable s, UnionLike m, Monoid s) => SimpleMergeable1 (WriterT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

(Mergeable s, UnionLike m, Monoid s) => SimpleMergeable1 (WriterT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

(UnionLike m, Mergeable r) => SimpleMergeable1 (ContT r m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> ContT r m a -> ContT r m a -> ContT r m a

SimpleMergeable1 ((->) a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a0 -> a0 -> a0) -> SymBool -> (a -> a0) -> (a -> a0) -> a -> a0

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => SimpleMergeable1 (RWST r w s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => SimpleMergeable1 (RWST r w s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a

Lift the standard mrgIte function through the type constructor.

>>> mrgIte1 "a" (Identity "b") (Identity "c") :: Identity SymInteger
Identity (ite a b c)

class Mergeable2 u => SimpleMergeable2 u where

Lifting of the SimpleMergeable class to binary type constructors.

Methods

liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b

Lift mrgIte through the type constructor.

>>> liftMrgIte2 mrgIte mrgIte "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)
((ite a b d),(ite a c e))

Instances

SimpleMergeable2 (,)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a, b) -> (a, b) -> (a, b)

mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b

Lift the standard mrgIte function through the type constructor.

>>> mrgIte2 "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)
((ite a b d),(ite a c e))

UnionLike operations

class (SimpleMergeable1 u, Mergeable1 u) => UnionLike u where

Special case of the Mergeable1 and SimpleMergeable1 class for type constructors that are SimpleMergeable when applied to any Mergeable types.

This type class is used to generalize the mrgIf function to other containers, for example, monad transformer transformed Unions.

Minimal complete definition

single, unionIf, mergeWithStrategy

Methods

single :: a -> u a

Wrap a single value in the union.

Note that this function cannot propagate the Mergeable knowledge.

>>> single "a" :: UnionM SymInteger
<a>
>>> mrgSingle "a" :: UnionM SymInteger
{a}

unionIf :: SymBool -> u a -> u a -> u a

If-then-else on two union values.

Note that this function cannot capture the Mergeable knowledge. However, it may use the merging strategy from the branches to merge the results.

>>> unionIf "a" (single "b") (single "c") :: UnionM SymInteger
<If a b c>
>>> unionIf "a" (mrgSingle "b") (single "c") :: UnionM SymInteger
{(ite a b c)}

mergeWithStrategy :: MergingStrategy a -> u a -> u a

Merge the contents with some merge strategy.

>>> mergeWithStrategy rootStrategy $ unionIf "a" (single "b") (single "c") :: UnionM SymInteger
{(ite a b c)}

Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.

This function is to be called when the Mergeable constraint can not be resolved, e.g., the merge strategy for the contained type is given with Mergeable1. In other cases, merge is usually a better alternative.

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a

Symbolic if control flow with the result merged with some merge strategy.

>>> mrgIfWithStrategy rootStrategy "a" (mrgSingle "b") (single "c") :: UnionM SymInteger
{(ite a b c)}

Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.

This function is to be called when the Mergeable constraint can not be resolved, e.g., the merge strategy for the contained type is given with Mergeable1. In other cases, mrgIf is usually a better alternative.

mrgSingleWithStrategy :: MergingStrategy a -> a -> u a

Wrap a single value in the union and capture the Mergeable knowledge.

>>> mrgSingleWithStrategy rootStrategy "a" :: UnionM SymInteger
{a}

Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.

This function is to be called when the Mergeable constraint can not be resolved, e.g., the merge strategy for the contained type is given with Mergeable1. In other cases, mrgSingle is usually a better alternative.

Instances

UnionLike UnionM

Defined in Grisette.Core.Control.Monad.UnionM

Methods

single :: a -> UnionM a

unionIf :: SymBool -> UnionM a -> UnionM a -> UnionM a

mergeWithStrategy :: MergingStrategy a -> UnionM a -> UnionM a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a

mrgSingleWithStrategy :: MergingStrategy a -> a -> UnionM a

UnionLike Union

Defined in Grisette.Core.Data.Union

Methods

single :: a -> Union a

unionIf :: SymBool -> Union a -> Union a -> Union a

mergeWithStrategy :: MergingStrategy a -> Union a -> Union a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> Union a -> Union a -> Union a

mrgSingleWithStrategy :: MergingStrategy a -> a -> Union a

UnionLike m => UnionLike (FreshT m)

Defined in Grisette.Core.Data.Class.GenSym

Methods

single :: a -> FreshT m a

unionIf :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a

mergeWithStrategy :: MergingStrategy a -> FreshT m a -> FreshT m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> FreshT m a -> FreshT m a -> FreshT m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> FreshT m a

UnionLike m => UnionLike (MaybeT m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> MaybeT m a

unionIf :: SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a

mergeWithStrategy :: MergingStrategy a -> MaybeT m a -> MaybeT m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> MaybeT 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

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

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> ExceptT e m a

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

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

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

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

UnionLike m => UnionLike (IdentityT m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> IdentityT m a

unionIf :: SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a

mergeWithStrategy :: MergingStrategy a -> IdentityT m a -> IdentityT m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> IdentityT m a

UnionLike m => UnionLike (ReaderT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> ReaderT s m a

unionIf :: SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a

mergeWithStrategy :: MergingStrategy a -> ReaderT s m a -> ReaderT s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> ReaderT s m a

(Mergeable s, UnionLike m) => UnionLike (StateT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> StateT s m a

unionIf :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a

mergeWithStrategy :: MergingStrategy a -> StateT s m a -> StateT s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> StateT s m a

(Mergeable s, UnionLike m) => UnionLike (StateT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> StateT s m a

unionIf :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a

mergeWithStrategy :: MergingStrategy a -> StateT s m a -> StateT s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> StateT s m a

(Mergeable s, UnionLike m, Monoid s) => UnionLike (WriterT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> WriterT s m a

unionIf :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

mergeWithStrategy :: MergingStrategy a -> WriterT s m a -> WriterT s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> WriterT s m a

(Mergeable s, UnionLike m, Monoid s) => UnionLike (WriterT s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> WriterT s m a

unionIf :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

mergeWithStrategy :: MergingStrategy a -> WriterT s m a -> WriterT s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> WriterT s m a

(UnionLike m, Mergeable r) => UnionLike (ContT r m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> ContT r m a

unionIf :: SymBool -> ContT r m a -> ContT r m a -> ContT r m a

mergeWithStrategy :: MergingStrategy a -> ContT r m a -> ContT r m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> ContT r m a -> ContT r m a -> ContT r m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> ContT r m a

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => UnionLike (RWST r w s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> RWST r w s m a

unionIf :: SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

mergeWithStrategy :: MergingStrategy a -> RWST r w s m a -> RWST r w s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> RWST r w s m a

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => UnionLike (RWST r w s m)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> RWST r w s m a

unionIf :: SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

mergeWithStrategy :: MergingStrategy a -> RWST r w s m a -> RWST r w s m a

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a

mrgSingleWithStrategy :: MergingStrategy a -> a -> RWST r w s m a

mrgIf :: (UnionLike u, Mergeable a) => SymBool -> u a -> u a -> u a

Symbolic if control flow with the result merged with the type's root merge strategy.

Equivalent to mrgIfWithStrategy rootStrategy.

>>> mrgIf "a" (single "b") (single "c") :: UnionM SymInteger
{(ite a b c)}

merge :: (UnionLike u, Mergeable a) => u a -> u a

Merge the contents with the type's root merge strategy.

Equivalent to mergeWithStrategy rootStrategy.

>>> merge $ unionIf "a" (single "b") (single "c") :: UnionM SymInteger
{(ite a b c)}

mrgSingle :: (UnionLike u, Mergeable a) => a -> u a

Wrap a single value in the type and propagate the type's root merge strategy.

Equivalent to mrgSingleWithStrategy rootStrategy.

>>> mrgSingle "a" :: UnionM SymInteger
{a}

class UnionLike u => UnionPrjOp (u :: Type -> Type) where

Union containers that can be projected back into single value or if-guarded values.

Methods

singleView :: u a -> Maybe a

Pattern match to extract single values.

>>> singleView (single 1 :: UnionM Integer)
Just 1
>>> singleView (unionIf "a" (single 1) (single 2) :: UnionM Integer)
Nothing

ifView :: u a -> Maybe (SymBool, u a, u a)

Pattern match to extract if values.

>>> ifView (single 1 :: UnionM Integer)
Nothing
>>> ifView (unionIf "a" (single 1) (single 2) :: UnionM Integer)
Just (a,<1>,<2>)
>>> ifView (mrgIf "a" (single 1) (single 2) :: UnionM Integer)
Just (a,{1},{2})

leftMost :: u a -> a

The leftmost value in the union.

>>> leftMost (unionIf "a" (single 1) (single 2) :: UnionM Integer)
1

Instances

UnionPrjOp UnionM

Defined in Grisette.Core.Control.Monad.UnionM

Methods

singleView :: UnionM a -> Maybe a

ifView :: UnionM a -> Maybe (SymBool, UnionM a, UnionM a)

leftMost :: UnionM a -> a

UnionPrjOp Union

Defined in Grisette.Core.Data.Union

Methods

singleView :: Union a -> Maybe a

ifView :: Union a -> Maybe (SymBool, Union a, Union a)

leftMost :: Union a -> a

pattern SingleU :: UnionPrjOp u => a -> u a

Pattern match to extract single values with singleView.

>>> case (single 1 :: UnionM Integer) of SingleU v -> v
1

pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a

Pattern match to extract guard values with ifView >>> case (unionIf "a" (single 1) (single 2) :: UnionM Integer) of IfU c t f -> (c,t,f) (a,1,2)

simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a

Merge the simply mergeable values in a union, and extract the merged value.

In the following example, unionIf will not merge the results, and simpleMerge will merge it and extract the single merged value.

>>> unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool
<If a b c>
>>> simpleMerge $ (unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool)
(ite a b c)

onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r

Lift a function to work on union values.

>>> sumU = onUnion sum
>>> sumU (unionIf "cond" (return ["a"]) (return ["b","c"]) :: UnionM [SymInteger])
(ite cond a (+ b c))

onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r

Lift a function to work on union values.

onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r

Lift a function to work on union values.

onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r

Lift a function to work on union values.

(#~) :: (Function f, SimpleMergeable (Ret f), UnionPrjOp u, Functor u) => f -> u (Arg f) -> Ret f infixl 9

Helper for applying functions on UnionPrjOp and SimpleMergeable.

>>> let f :: Integer -> UnionM Integer = \x -> mrgIf (ssym "a") (mrgSingle $ x + 1) (mrgSingle $ x + 2)
>>> f #~ (mrgIf (ssym "b" :: SymBool) (mrgSingle 0) (mrgSingle 2) :: UnionM Integer)
{If (&& b a) 1 (If b 2 (If a 3 4))}