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.Data.Class.SimpleMergeable

Description

 
Synopsis

Simple mergeable types

class Mergeable a => SimpleMergeable a where Source #

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

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

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

Instances

Instances details
SimpleMergeable AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SimpleMergeable CEGISCondition Source # 
Instance details

Defined in Grisette.Core.Data.Class.CEGISSolver

SimpleMergeable FreshIndex Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

SimpleMergeable () Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> () -> () -> () Source #

SimpleMergeable a => SimpleMergeable (Identity a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Identity a -> Identity a -> Identity a Source #

(Generic a, Mergeable' (Rep a), SimpleMergeable' (Rep a)) => SimpleMergeable (Default a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Default a -> Default a -> Default a Source #

Mergeable a => SimpleMergeable (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a Source #

Mergeable a => SimpleMergeable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

mrgIte :: SymBool -> Union a -> Union a -> Union a Source #

SupportedPrim a => SimpleMergeable (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Sym a -> Sym a -> Sym a Source #

(UnionLike m, Mergeable a) => SimpleMergeable (FreshT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

(UnionLike m, Mergeable a) => SimpleMergeable (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(IsConcrete k, Mergeable t) => SimpleMergeable (HashMap k (UnionM (Maybe t))) Source # 
Instance details

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)) Source #

SimpleMergeable b => SimpleMergeable (a -> b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(SimpleMergeable a, SimpleMergeable b) => SimpleMergeable (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

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

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

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

(UnionLike m, Mergeable e, Mergeable a) => SimpleMergeable (ExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(UnionLike m, Mergeable a) => SimpleMergeable (IdentityT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable a, UnionLike m) => SimpleMergeable (ReaderT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable a, UnionLike m) => SimpleMergeable (StateT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable a, UnionLike m) => SimpleMergeable (StateT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable a, UnionLike m, Monoid s) => SimpleMergeable (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable a, UnionLike m, Monoid s) => SimpleMergeable (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c) => SimpleMergeable (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(UnionLike m, Mergeable r) => SimpleMergeable (ContT r m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d) => SimpleMergeable (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable w, Monoid w, Mergeable a, UnionLike m) => SimpleMergeable (RWST r w s m a) Source # 
Instance details

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

(Mergeable s, Mergeable w, Monoid w, Mergeable a, UnionLike m) => SimpleMergeable (RWST r w s m a) Source # 
Instance details

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

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e) => SimpleMergeable (a, b, c, d, e) Source # 
Instance details

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) Source #

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e, SimpleMergeable f) => SimpleMergeable (a, b, c, d, e, f) Source # 
Instance details

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) Source #

(SimpleMergeable a, SimpleMergeable b, SimpleMergeable c, SimpleMergeable d, SimpleMergeable e, SimpleMergeable f, SimpleMergeable g) => SimpleMergeable (a, b, c, d, e, f, g) Source # 
Instance details

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) Source #

(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) Source # 
Instance details

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) Source #

class SimpleMergeable1 u where Source #

Lifting of the SimpleMergeable class to unary type constructors.

Methods

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

Lift mrgIte through the type constructor.

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

Instances

Instances details
SimpleMergeable1 Identity Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

SimpleMergeable1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

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

SimpleMergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

UnionLike m => SimpleMergeable1 (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

UnionLike m => SimpleMergeable1 (MaybeT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

SimpleMergeable a => SimpleMergeable1 ((,) a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(UnionLike m, Mergeable e) => SimpleMergeable1 (CBMCExceptT e m) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

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

(UnionLike m, Mergeable e) => SimpleMergeable1 (ExceptT e m) Source # 
Instance details

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

UnionLike m => SimpleMergeable1 (IdentityT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

UnionLike m => SimpleMergeable1 (ReaderT s m) Source # 
Instance details

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

(Mergeable s, UnionLike m) => SimpleMergeable1 (StateT s m) Source # 
Instance details

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

(Mergeable s, UnionLike m) => SimpleMergeable1 (StateT s m) Source # 
Instance details

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

(Mergeable s, UnionLike m, Monoid s) => SimpleMergeable1 (WriterT s m) Source # 
Instance details

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

(Mergeable s, UnionLike m, Monoid s) => SimpleMergeable1 (WriterT s m) Source # 
Instance details

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

(UnionLike m, Mergeable r) => SimpleMergeable1 (ContT r m) Source # 
Instance details

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

SimpleMergeable1 ((->) a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => SimpleMergeable1 (RWST r w s m) Source # 
Instance details

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

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => SimpleMergeable1 (RWST r w s m) Source # 
Instance details

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

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

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

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

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

Instances details
SimpleMergeable2 (,) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

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

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

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

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

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

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

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

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

Instances details
UnionLike UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

UnionLike Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

UnionLike m => UnionLike (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

UnionLike m => UnionLike (MaybeT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

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

Defined in Grisette.Core.Control.Monad.CBMCExcept

(UnionLike m, Mergeable e) => UnionLike (ExceptT e m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

UnionLike m => UnionLike (IdentityT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

UnionLike m => UnionLike (ReaderT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

(Mergeable s, UnionLike m) => UnionLike (StateT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> StateT s m a Source #

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

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

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

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

(Mergeable s, UnionLike m) => UnionLike (StateT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> StateT s m a Source #

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

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

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

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

(Mergeable s, UnionLike m, Monoid s) => UnionLike (WriterT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

(Mergeable s, UnionLike m, Monoid s) => UnionLike (WriterT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

(UnionLike m, Mergeable r) => UnionLike (ContT r m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

single :: a -> ContT r m a Source #

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

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

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

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

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => UnionLike (RWST r w s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

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

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

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

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

(Mergeable s, Mergeable w, Monoid w, UnionLike m) => UnionLike (RWST r w s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

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

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

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

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

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

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

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

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

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

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

Methods

singleView :: u a -> Maybe a Source #

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) Source #

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

The leftmost value in the union.

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

Instances

Instances details
UnionPrjOp UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

UnionPrjOp Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

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

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

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

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

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

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

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

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

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))}