Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SimpleMergeable

Contents

Simple mergeable types
Generic SimpleMergeable
Symbolic branching

Description

Synopsis

class Mergeable a => SimpleMergeable a where
- mrgIte :: SymBool -> a -> a -> a
class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 (u :: Type -> Type) where
- liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a
mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a
class (Mergeable2 u, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 (u :: Type -> Type -> Type) where
- liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b
mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b
data family SimpleMergeableArgs arity a
class GSimpleMergeable arity (f :: Type -> Type) where
- gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a
genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a
genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a
class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) where
- mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a
- mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a
mrgIf :: (SymBranching u, Mergeable a) => SymBool -> u a -> u a -> u a
mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a
merge :: (SymBranching m, Mergeable a) => m a -> m a

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.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> AssertionError -> AssertionError -> AssertionError Source #
SimpleMergeable CEGISCondition Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.CEGISSolver Methods mrgIte :: SymBool -> CEGISCondition -> CEGISCondition -> CEGISCondition Source #
SimpleMergeable FreshIndex Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods mrgIte :: SymBool -> FreshIndex -> FreshIndex -> FreshIndex Source #
SimpleMergeable SymAlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #
SimpleMergeable SymBool Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymBool -> SymBool -> SymBool Source #
SimpleMergeable SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #
SimpleMergeable SymInteger Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source #
SimpleMergeable () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> () -> () -> () Source #
(Generic a, GSimpleMergeable Arity0 (Rep a), GMergeable Arity0 (Rep a)) => SimpleMergeable (Default a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Default a -> Default a -> Default a Source #
SimpleMergeable a => SimpleMergeable (Identity a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Identity a -> Identity a -> Identity a Source #
SimpleMergeable a => SimpleMergeable (Down a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Down a -> Down a -> Down a Source #
SimpleMergeable a => SimpleMergeable (Dual a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Dual a -> Dual a -> Dual a Source #
SimpleMergeable a => SimpleMergeable (Endo a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Endo a -> Endo a -> Endo a Source #
SimpleMergeable a => SimpleMergeable (Product a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Product a -> Product a -> Product a Source #
SimpleMergeable a => SimpleMergeable (Sum a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Sum a -> Sum a -> Sum a Source #
SimpleMergeable p => SimpleMergeable (Par1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Par1 p -> Par1 p -> Par1 p Source #
Mergeable a => SimpleMergeable (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods mrgIte :: SymBool -> Union a -> Union a -> Union a Source #
Mergeable a => SimpleMergeable (UnionBase a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase Methods mrgIte :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
(Generic1 f, GSimpleMergeable Arity1 (Rep1 f), GMergeable Arity1 (Rep1 f), SimpleMergeable a) => SimpleMergeable (Default1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Default1 f a -> Default1 f a -> Default1 f a Source #
SimpleMergeable (Proxy a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Proxy a -> Proxy a -> Proxy a Source #
SimpleMergeable (U1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> U1 p -> U1 p -> U1 p Source #
SimpleMergeable (V1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> V1 p -> V1 p -> V1 p Source #
(SymBranching m, Mergeable a) => SimpleMergeable (FreshT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source #
SimpleMergeable (a --> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a --> b) -> (a --> b) -> a --> b Source #
ValidFP eb sb => SimpleMergeable (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #
SimpleMergeable (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb Source #
SimpleMergeable (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb Source #
(SymBranching m, Mergeable a) => SimpleMergeable (MaybeT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a Source #
(IsConcrete k, Mergeable t) => SimpleMergeable (HashMap k (Union (Maybe t))) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods mrgIte :: SymBool -> HashMap k (Union (Maybe t)) -> HashMap k (Union (Maybe t)) -> HashMap k (Union (Maybe t)) Source #
(SimpleMergeable a1, SimpleMergeable a2) => SimpleMergeable (a1, a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2) -> (a1, a2) -> (a1, a2) Source #
SimpleMergeable b => SimpleMergeable (a -> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a -> b) -> (a -> b) -> a -> b Source #
SimpleMergeable a => SimpleMergeable (Const a b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Const a b -> Const a b -> Const a b Source #
SimpleMergeable (f a) => SimpleMergeable (Ap f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Ap f a -> Ap f a -> Ap f a Source #
SimpleMergeable (f a) => SimpleMergeable (Alt f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Alt f a -> Alt f a -> Alt f a Source #
SimpleMergeable (f p) => SimpleMergeable (Rec1 f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Rec1 f p -> Rec1 f p -> Rec1 f p 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 #
(SymBranching m, Mergeable e, Mergeable a) => SimpleMergeable (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #
(SymBranching m, Mergeable a) => SimpleMergeable (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a Source #
(Mergeable a, SymBranching m) => SimpleMergeable (ReaderT s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a Source #
(Mergeable s, Mergeable a, SymBranching m) => SimpleMergeable (StateT s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source #
(Mergeable s, Mergeable a, SymBranching m) => SimpleMergeable (StateT s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source #
(Mergeable s, Mergeable a, SymBranching m, Monoid s) => SimpleMergeable (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source #
(Mergeable s, Mergeable a, SymBranching m, Monoid s) => SimpleMergeable (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3) => SimpleMergeable (a1, a2, a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3) -> (a1, a2, a3) -> (a1, a2, a3) Source #
(SimpleMergeable (l a), SimpleMergeable (r a)) => SimpleMergeable (Product l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Product l r a -> Product l r a -> Product l r a Source #
(SimpleMergeable (f p), SimpleMergeable (g p)) => SimpleMergeable ((f :*: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (f :: g) p -> (f :: g) p -> (f :*: g) p Source #
SimpleMergeable c => SimpleMergeable (K1 i c p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> K1 i c p -> K1 i c p -> K1 i c p Source #
(SymBranching m, Mergeable r) => SimpleMergeable (ContT r m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> ContT r m a -> ContT r m a -> ContT r m a Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4) => SimpleMergeable (a1, a2, a3, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> (a1, a2, a3, a4) Source #
SimpleMergeable (f (g a)) => SimpleMergeable (Compose f g a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> Compose f g a -> Compose f g a -> Compose f g a Source #
SimpleMergeable (f (g p)) => SimpleMergeable ((f :.: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (f :.: g) p -> (f :.: g) p -> (f :.: g) p Source #
SimpleMergeable (f p) => SimpleMergeable (M1 i c f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> M1 i c f p -> M1 i c f p -> M1 i c f p Source #
(Mergeable s, Mergeable w, Monoid w, Mergeable a, SymBranching m) => SimpleMergeable (RWST r w s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m) => SimpleMergeable (RWST r w s m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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 a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5) => SimpleMergeable (a1, a2, a3, a4, a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6) => SimpleMergeable (a1, a2, a3, a4, a5, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13, SimpleMergeable a14) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13, SimpleMergeable a14, SimpleMergeable a15) => SimpleMergeable (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #

class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 (u :: Type -> Type) 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.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Identity a -> Identity a -> Identity a Source #
SimpleMergeable1 Down Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Down a -> Down a -> Down a Source #
SimpleMergeable1 Dual Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Dual a -> Dual a -> Dual a Source #
SimpleMergeable1 Endo Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Endo a -> Endo a -> Endo a Source #
SimpleMergeable1 Product Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Product a -> Product a -> Product a Source #
SimpleMergeable1 Sum Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Sum a -> Sum a -> Sum a Source #
SimpleMergeable1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Union a -> Union a -> Union a Source #
SimpleMergeable1 UnionBase Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #
(Generic1 f, GSimpleMergeable Arity1 (Rep1 f), GMergeable Arity1 (Rep1 f)) => SimpleMergeable1 (Default1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Default1 f a -> Default1 f a -> Default1 f a Source #
SimpleMergeable1 (Proxy :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Proxy a -> Proxy a -> Proxy a Source #
SymBranching m => SimpleMergeable1 (FreshT m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source #
SymBranching m => SimpleMergeable1 (MaybeT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a0 -> a0 -> a0) -> SymBool -> (a, a0) -> (a, a0) -> (a, a0) Source #
SimpleMergeable a => SimpleMergeable1 (Const a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a0 -> a0 -> a0) -> SymBool -> Const a a0 -> Const a a0 -> Const a a0 Source #
SimpleMergeable1 f => SimpleMergeable1 (Ap f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Ap f a -> Ap f a -> Ap f a Source #
SimpleMergeable1 f => SimpleMergeable1 (Alt f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Alt f a -> Alt f a -> Alt f 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) => SimpleMergeable1 (ExceptT e m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #
SymBranching m => SimpleMergeable1 (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a Source #
SymBranching m => SimpleMergeable1 (ReaderT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m) => SimpleMergeable1 (StateT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m) => SimpleMergeable1 (StateT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m, Monoid s) => SimpleMergeable1 (WriterT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m, Monoid s) => SimpleMergeable1 (WriterT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source #
(SimpleMergeable a1, SimpleMergeable a2) => SimpleMergeable1 ((,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a) -> (a1, a2, a) -> (a1, a2, a) Source #
(SimpleMergeable1 l, SimpleMergeable1 r) => SimpleMergeable1 (Product l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Product l r a -> Product l r a -> Product l r a Source #
(SymBranching m, Mergeable r) => SimpleMergeable1 (ContT r m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> ContT r m a -> ContT r m a -> ContT r m a Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3) => SimpleMergeable1 ((,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a) -> (a1, a2, a3, a) -> (a1, a2, a3, a) Source #
SimpleMergeable1 ((->) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a0 -> a0 -> a0) -> SymBool -> (a -> a0) -> (a -> a0) -> a -> a0 Source #
(SimpleMergeable1 f, SimpleMergeable1 g) => SimpleMergeable1 (Compose f g) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Compose f g a -> Compose f g a -> Compose f g a Source #
(Mergeable s, Mergeable w, Monoid w, SymBranching m) => SimpleMergeable1 (RWST r w s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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, SymBranching m) => SimpleMergeable1 (RWST r w s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.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 #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4) => SimpleMergeable1 ((,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a) -> (a1, a2, a3, a4, a) -> (a1, a2, a3, a4, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5) => SimpleMergeable1 ((,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a) -> (a1, a2, a3, a4, a5, a) -> (a1, a2, a3, a4, a5, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6) => SimpleMergeable1 ((,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a) -> (a1, a2, a3, a4, a5, a6, a) -> (a1, a2, a3, a4, a5, a6, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7) => SimpleMergeable1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a) -> (a1, a2, a3, a4, a5, a6, a7, a) -> (a1, a2, a3, a4, a5, a6, a7, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8) => SimpleMergeable1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9) => SimpleMergeable1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10) => SimpleMergeable1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11) => SimpleMergeable1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12) => SimpleMergeable1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13) => SimpleMergeable1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13, SimpleMergeable a14) => SimpleMergeable1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, 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, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 (u :: Type -> Type -> Type) 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.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a, b) -> (a, b) -> (a, b) Source #
SimpleMergeable a => SimpleMergeable2 ((,,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a0 -> a0 -> a0) -> (SymBool -> b -> b -> b) -> SymBool -> (a, a0, b) -> (a, a0, b) -> (a, a0, b) Source #
(SimpleMergeable a1, SimpleMergeable a2) => SimpleMergeable2 ((,,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a, b) -> (a1, a2, a, b) -> (a1, a2, a, b) Source #
SimpleMergeable2 (->) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a -> b) -> (a -> b) -> a -> b Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3) => SimpleMergeable2 ((,,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a, b) -> (a1, a2, a3, a, b) -> (a1, a2, a3, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4) => SimpleMergeable2 ((,,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a, b) -> (a1, a2, a3, a4, a, b) -> (a1, a2, a3, a4, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5) => SimpleMergeable2 ((,,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a, b) -> (a1, a2, a3, a4, a5, a, b) -> (a1, a2, a3, a4, a5, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6) => SimpleMergeable2 ((,,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a, b) -> (a1, a2, a3, a4, a5, a6, a, b) -> (a1, a2, a3, a4, a5, a6, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7) => SimpleMergeable2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8) => SimpleMergeable2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9) => SimpleMergeable2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10) => SimpleMergeable2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11) => SimpleMergeable2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12) => SimpleMergeable2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) Source #
(SimpleMergeable a1, SimpleMergeable a2, SimpleMergeable a3, SimpleMergeable a4, SimpleMergeable a5, SimpleMergeable a6, SimpleMergeable a7, SimpleMergeable a8, SimpleMergeable a9, SimpleMergeable a10, SimpleMergeable a11, SimpleMergeable a12, SimpleMergeable a13) => SimpleMergeable2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, 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))

Generic `SimpleMergeable`

data family SimpleMergeableArgs arity a Source #

The arguments to the generic simple merging function.

Instances

Instances details

data SimpleMergeableArgs Arity0 _ Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable data SimpleMergeableArgs Arity0 _ = SimpleMergeableArgs0
newtype SimpleMergeableArgs Arity1 a Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable newtype SimpleMergeableArgs Arity1 a = SimpleMergeableArgs1 (SymBool -> a -> a -> a)

class GSimpleMergeable arity (f :: Type -> Type) where Source #

Generic SimpleMergeable class.

Methods

gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a Source #

Instances

Instances details

GSimpleMergeable Arity1 Par1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs Arity1 a -> SymBool -> Par1 a -> Par1 a -> Par1 a Source #
GSimpleMergeable arity (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> U1 a -> U1 a -> U1 a Source #
GSimpleMergeable arity (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> V1 a -> V1 a -> V1 a Source #
SimpleMergeable1 f => GSimpleMergeable Arity1 (Rec1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs Arity1 a -> SymBool -> Rec1 f a -> Rec1 f a -> Rec1 f a Source #
(GSimpleMergeable arity a, GSimpleMergeable arity b) => GSimpleMergeable arity (a :*: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs arity a0 -> SymBool -> (a :: b) a0 -> (a :: b) a0 -> (a :*: b) a0 Source #
SimpleMergeable c => GSimpleMergeable arity (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> K1 i c a -> K1 i c a -> K1 i c a Source #
(SimpleMergeable1 f, GSimpleMergeable Arity1 g) => GSimpleMergeable Arity1 (f :.: g) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs Arity1 a -> SymBool -> (f :.: g) a -> (f :.: g) a -> (f :.: g) a Source #
GSimpleMergeable arity a => GSimpleMergeable arity (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods gmrgIte :: SimpleMergeableArgs arity a0 -> SymBool -> M1 i c a a0 -> M1 i c a a0 -> M1 i c a a0 Source #

genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a Source #

Generic mrgIte function.

genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a Source #

Generic liftMrgIte function.

Symbolic branching

class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) 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.

Methods

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") (return "c") :: Union 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.

mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a Source #

Symbolic if control flow with the result.

This function does not need a merging strategy, and it will merge the result only if any of the branches is merged.

Instances

Instances details

SymBranching Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> Union a -> Union a -> Union a Source # mrgIfPropagatedStrategy :: SymBool -> Union a -> Union a -> Union a Source #
SymBranching UnionBase Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source # mrgIfPropagatedStrategy :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #
SymBranching m => SymBranching (FreshT m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source # mrgIfPropagatedStrategy :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source #
SymBranching m => SymBranching (MaybeT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> MaybeT m a -> MaybeT m a -> MaybeT m a Source # mrgIfPropagatedStrategy :: SymBool -> MaybeT m a -> MaybeT m a -> MaybeT 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 #
(SymBranching m, Mergeable e) => SymBranching (ExceptT e m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source # mrgIfPropagatedStrategy :: SymBool -> ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #
SymBranching m => SymBranching (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a Source # mrgIfPropagatedStrategy :: SymBool -> IdentityT m a -> IdentityT m a -> IdentityT m a Source #
SymBranching m => SymBranching (ReaderT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a Source # mrgIfPropagatedStrategy :: SymBool -> ReaderT s m a -> ReaderT s m a -> ReaderT s m a Source #
(Mergeable s, SymBranching m) => SymBranching (StateT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source # mrgIfPropagatedStrategy :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source #
(Mergeable s, SymBranching m) => SymBranching (StateT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source # mrgIfPropagatedStrategy :: SymBool -> StateT s m a -> StateT s m a -> StateT s m a Source #
(Mergeable s, SymBranching m, Monoid s) => SymBranching (WriterT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source # mrgIfPropagatedStrategy :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source #
(Mergeable s, SymBranching m, Monoid s) => SymBranching (WriterT s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source # mrgIfPropagatedStrategy :: SymBool -> WriterT s m a -> WriterT s m a -> WriterT s m a Source #
(SymBranching m, Mergeable r) => SymBranching (ContT r m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> ContT r m a -> ContT r m a -> ContT r m a Source # mrgIfPropagatedStrategy :: SymBool -> ContT r m a -> ContT r m a -> ContT r m a Source #
(Mergeable s, Mergeable w, Monoid w, SymBranching m) => SymBranching (RWST r w s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source # mrgIfPropagatedStrategy :: 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, SymBranching m) => SymBranching (RWST r w s m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIfWithStrategy :: MergingStrategy a -> SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source # mrgIfPropagatedStrategy :: SymBool -> RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source #

mrgIf :: (SymBranching 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" (return "b") (return "c") :: Union SymInteger
{(ite a b c)}

mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a Source #

Try to merge the container with a given merge strategy.

merge :: (SymBranching m, Mergeable a) => m a -> m a Source #

Try to merge the container with the root strategy.

Simple mergeable types

Instances

Instances

Instances

Generic SimpleMergeable

Instances

Instances

Symbolic branching

Instances

Generic `SimpleMergeable`