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.Control.Monad.Union

Contents

Union and helpers

Description

Synopsis

data Union a where
- UAny :: forall a. UnionBase a -> Union a
- UMrg :: forall a. MergingStrategy a -> UnionBase a -> Union a
unionUnaryOp :: (a -> a) -> Union a -> Union a
unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a
liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a
liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a
unionBase :: Union a -> UnionBase a
unionMergingStrategy :: Union a -> Maybe (MergingStrategy a)
isMerged :: Union a -> Bool
unionSize :: Union a -> Int
class (Eq t, Ord t, Hashable t) => IsConcrete t

Union and helpers

data Union a where Source #

Union is the UnionBase container (hidden) enhanced with MergingStrategy knowledge propagation.

The UnionBase models the underlying semantics evaluation semantics for unsolvable types with the nested if-then-else tree semantics, and can be viewed as the following structure:

data UnionBase a
  = UnionSingle a
  | UnionIf bool (Union a) (Union a)

The UnionSingle constructor is for a single value with the path condition true, and the UnionIf constructor is the if operator in an if-then-else tree. For clarity, when printing a Union value, we will omit the UnionSingle constructor. The following two representations has the same semantics.

If      c1    (If c11 v11 (If c12 v12 v13))
  (If   c2    v2
              v3)

\[ \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right. \]

To reduce the size of the if-then-else tree to reduce the number of paths to execute, Grisette would merge the branches in a UnionBase container and maintain a representation invariant for them. To perform this merging procedure, Grisette relies on a type class called Mergeable and the merging strategy defined by it.

UnionBase is a monad, so we can easily write code with the do-notation and monadic combinators. However, the standard monadic operators cannot resolve any extra constraints, including the Mergeable constraint (see The constrained-monad problem by Sculthorpe et al.). This prevents the standard do-notations to merge the results automatically, and would result in bad performance or very verbose code.

To reduce this boilerplate, Grisette provide another monad, Union that would try to cache the merging strategy. The Union has two data constructors (hidden intentionally), UAny and UMrg. The UAny data constructor (printed as <...>) wraps an arbitrary (probably unmerged) UnionBase. It is constructed when no Mergeable knowledge is available (for example, when constructed with Haskell's return). The UMrg data constructor (printed as {...}) wraps a merged UnionBase along with the Mergeable constraint. This constraint can be propagated to the contexts without Mergeable knowledge, and helps the system to merge the resulting UnionBase.

Examples:

return cannot resolve the Mergeable constraint.

>>> return 1 :: Union Integer
<1>

mrgReturn can resolve the Mergeable constraint.

>>> import Grisette.Lib.Base
>>> mrgReturn 1 :: Union Integer
{1}

mrgIfPropagatedStrategy does not try to Mergeable constraint.

>>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: Union Integer
<If a 1 (If b 1 2)>

But mrgIfPropagatedStrategy is able to merge the result if some of the branches are merged and have a cached merging strategy:

>>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (mrgReturn 1) (return 2)) :: Union Integer
{If (|| a b) 1 2}

The >>= operator uses mrgIfPropagatedStrategy internally. When the final statement in a do-block merges the values, the system can then merge the final result.

>>> :{
  do
    x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))
    mrgSingle $ x + 1 :: Union Integer
:}
{If (|| a b) 2 3}

Calling a function that merges a result at the last line of a do-notation will also merge the whole block. If you stick to these mrg* combinators and all the functions will merge the results, the whole program can be symbolically evaluated efficiently.

>>> f x y = mrgIf "c" x y :: Union Integer
>>> :{
  do
    x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))
    f x (x + 1)
:}
{If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}

In Grisette.Lib.Base, Grisette.Lib.Mtl, we also provided more mrg* variants of other combinators. You should stick to these combinators to ensure efficient merging by Grisette.

Constructors

UAny	`Union` with no `Mergeable` knowledge.
Fields :: forall a. UnionBase a Original `UnionBase`. -> Union a
UMrg	`Union` with `Mergeable` knowledge.
Fields :: forall a. MergingStrategy a Cached merging strategy. -> UnionBase a Merged `UnionBase` -> Union a

Instances

Instances details

Eq1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftEq :: (a -> b -> Bool) -> Union a -> Union b -> Bool #
Show1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Union a] -> ShowS #
NFData1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftRnf :: (a -> ()) -> Union a -> () #
Applicative Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods pure :: a -> Union a # (<>) :: Union (a -> b) -> Union a -> Union b # liftA2 :: (a -> b -> c) -> Union a -> Union b -> Union c # (>) :: Union a -> Union b -> Union b # (<*) :: Union a -> Union b -> Union a #
Functor Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods fmap :: (a -> b) -> Union a -> Union b # (<$) :: a -> Union b -> Union a #
Monad Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods (>>=) :: Union a -> (a -> Union b) -> Union b # (>>) :: Union a -> Union b -> Union b # return :: a -> Union a #
MonadParallelUnion Union Source #
Instance details Defined in Grisette.Experimental.MonadParallelUnion Methods parBindUnion :: (Mergeable b, NFData b) => Union a -> (a -> Union b) -> Union b Source #
PlainUnion Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods singleView :: Union a -> Maybe a Source # ifView :: Union a -> Maybe (SymBool, Union a, Union a) Source # toGuardedList :: Union a -> [(SymBool, a)] Source # overestimateUnionValues :: Mergeable a => Union a -> [a] Source #
EvalSym1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Union a -> Union a Source #
ExtractSym1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftExtractSymMaybe :: forall (knd :: SymbolKind) a. IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> Union a -> Maybe (SymbolSet knd) Source #
Mergeable1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods liftRootStrategy :: MergingStrategy a -> MergingStrategy (Union a) Source #
PPrint1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftPFormatPrec :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> Union a -> Doc ann Source # liftPFormatList :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> [Union a] -> Doc ann 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 #
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 #
SubstSym1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Union a -> Union a Source #
SymEq1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftSymEq :: (a -> b -> SymBool) -> Union a -> Union b -> SymBool Source #
SymOrd1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods liftSymCompare :: (a -> b -> Union Ordering) -> Union a -> Union b -> Union Ordering Source #
TryMerge Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods tryMergeWithStrategy :: MergingStrategy a -> Union a -> Union a Source #
AllSyms1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Union a -> [SomeSym] -> [SomeSym] Source #
Hashable1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Union a -> Int #
ToCon1 Union Identity Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftToCon :: (a -> Maybe b) -> Union a -> Maybe (Identity b) Source #
ToCon1 Union Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftToCon :: (a -> Maybe b) -> Union a -> Maybe (Union b) Source #
ToSym1 Identity Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftToSym :: (a -> b) -> Identity a -> Union b Source #
ToSym1 Union Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftToSym :: (a -> b) -> Union a -> Union b Source #
(GenSym spec a, Mergeable a) => GenSym spec (Union a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => spec -> m (Union (Union a)) Source #
GenSym spec a => GenSymSimple spec (Union a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => spec -> m (Union a) Source #
(Solvable c t, Mergeable t) => Solvable c (Union t) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods con :: c -> Union t Source # conView :: Union t -> Maybe c Source # sym :: Symbol -> Union t Source # ssym :: Identifier -> Union t Source # isym :: Identifier -> Int -> Union t Source #
ToSym AssertionError (Union AssertionError) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: AssertionError -> Union AssertionError Source #
ToSym VerificationConditions (Union VerificationConditions) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: VerificationConditions -> Union VerificationConditions Source #
ToSym NotRepresentableFPError (Union NotRepresentableFPError) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: NotRepresentableFPError -> Union NotRepresentableFPError Source #
ToSym () (Union ()) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: () -> Union () Source #
(UnifiedITEOp 'S v, Mergeable v) => UnifiedITEOp 'S (Union v) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp Methods withBaseITEOp :: (If (IsConMode 'S) () (ITEOp (Union v)) => r) -> r Source #
UnifiedSymEq 'S v => UnifiedSymEq 'S (Union v) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq Methods withBaseSymEq :: (If (IsConMode 'S) (Eq (Union v)) (SymEq (Union v)) => r) -> r Source #
UnifiedSymOrd 'S v => UnifiedSymOrd 'S (Union v) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd Methods withBaseSymOrd :: (If (IsConMode 'S) (Ord (Union v)) (SymOrd (Union v)) => r) -> r Source #
Lift a => Lift (Union a :: Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods lift :: Quote m => Union a -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Union a -> Code m (Union a) #
(Mergeable a, Serial a) => Binary (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods put :: Union a -> Put # get :: Get (Union a) # putList :: [Union a] -> Put #
(Mergeable a, Serial a) => Serial (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods serialize :: MonadPut m => Union a -> m () # deserialize :: MonadGet m => m (Union a) #
(Mergeable a, Serial a) => Serialize (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods put :: Putter (Union a) # get :: Get (Union a) #
NFData a => NFData (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods rnf :: Union a -> () #
(IsString a, Mergeable a) => IsString (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods fromString :: String -> Union a #
(Num a, Mergeable a) => Num (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (+) :: Union a -> Union a -> Union a # (-) :: Union a -> Union a -> Union a # (*) :: Union a -> Union a -> Union a # negate :: Union a -> Union a # abs :: Union a -> Union a # signum :: Union a -> Union a # fromInteger :: Integer -> Union a #
Show a => Show (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods showsPrec :: Int -> Union a -> ShowS # show :: Union a -> String # showList :: [Union a] -> ShowS #
Eq a => Eq (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (==) :: Union a -> Union a -> Bool # (/=) :: Union a -> Union a -> Bool #
(ITEOp a, Mergeable a) => ITEOp (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods symIte :: SymBool -> Union a -> Union a -> Union a Source #
(LogicalOp a, Mergeable a) => LogicalOp (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods true :: Union a Source # false :: Union a Source # (.\|\|) :: Union a -> Union a -> Union a Source # (.&&) :: Union a -> Union a -> Union a Source # symNot :: Union a -> Union a Source # symXor :: Union a -> Union a -> Union a Source # symImplies :: Union a -> Union a -> Union a Source #
EvalSym a => EvalSym (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods evalSym :: Bool -> Model -> Union a -> Union a Source #
ExtractSym a => ExtractSym (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods extractSym :: Union a -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => Union a -> Maybe (SymbolSet knd) Source #
Mergeable a => Mergeable (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods rootStrategy :: MergingStrategy (Union a) Source # sortIndices :: Union a -> [DynamicSortedIdx] Source #
PPrint a => PPrint (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods pformat :: Union a -> Doc ann Source # pformatPrec :: Int -> Union a -> Doc ann Source # pformatList :: [Union a] -> Doc ann 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 #
SubstSym a => SubstSym (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Union a -> Union a Source #
SymEq a => SymEq (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (.==) :: Union a -> Union a -> SymBool Source # (./=) :: Union a -> Union a -> SymBool Source # symDistinct :: [Union a] -> SymBool Source #
SymOrd a => SymOrd (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: Union a -> Union a -> SymBool Source # (.<=) :: Union a -> Union a -> SymBool Source # (.>) :: Union a -> Union a -> SymBool Source # (.>=) :: Union a -> Union a -> SymBool Source # symCompare :: Union a -> Union a -> Union Ordering Source #
AllSyms a => AllSyms (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods allSymsS :: Union a -> [SomeSym] -> [SomeSym] Source # allSyms :: Union a -> [SomeSym] Source #
Hashable a => Hashable (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods hashWithSalt :: Int -> Union a -> Int # hash :: Union a -> Int #
(GenSym a a, Mergeable a) => GenSym (Union a) a Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => Union a -> m (Union a) Source #
ToCon (Union AssertionError) AssertionError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union AssertionError -> Maybe AssertionError Source #
ToCon (Union VerificationConditions) VerificationConditions Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union VerificationConditions -> Maybe VerificationConditions Source #
ToCon (Union NotRepresentableFPError) NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union NotRepresentableFPError -> Maybe NotRepresentableFPError Source #
ToCon (Union ()) () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union () -> Maybe () Source #
ToSym (Union Integer) SymInteger Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union Integer -> SymInteger Source #
ToSym (Union Bool) SymBool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union Bool -> SymBool Source #
UnionWithExcept (Union (Either e v)) Union e v Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods extractUnionExcept :: Union (Either e v) -> Union (Either e v) Source #
UnionWithExcept (Union (CBMCEither e v)) Union e v Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: Union (CBMCEither e v) -> Union (Either e v) Source #
(Function f arg ret, Mergeable f, Mergeable ret) => Function (Union f) arg (Union ret) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (#) :: Union f -> arg -> Union ret Source #
ToCon a1 a2 => ToCon (Union (First a1)) (First a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (First a1) -> Maybe (First a2) Source #
ToCon a1 a2 => ToCon (Union (Last a1)) (Last a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Last a1) -> Maybe (Last a2) Source #
ToCon a1 a2 => ToCon (Union (Down a1)) (Down a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Down a1) -> Maybe (Down a2) Source #
ToCon a1 a2 => ToCon (Union (Dual a1)) (Dual a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Dual a1) -> Maybe (Dual a2) Source #
ToCon a1 a2 => ToCon (Union (Product a1)) (Product a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Product a1) -> Maybe (Product a2) Source #
ToCon a1 a2 => ToCon (Union (Sum a1)) (Sum a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Sum a1) -> Maybe (Sum a2) Source #
ToCon a1 a2 => ToCon (Union (Maybe a1)) (Maybe a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Maybe a1) -> Maybe (Maybe a2) Source #
ToCon a1 a2 => ToCon (Union [a1]) [a2] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union [a1] -> Maybe [a2] Source #
ToCon a b => ToCon (Union a) (Identity b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toCon :: Union a -> Maybe (Identity b) Source #
ToCon a b => ToCon (Union a) (Union b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toCon :: Union a -> Maybe (Union b) Source #
ToSym a b => ToSym (Identity a) (Union b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Identity a -> Union b Source #
(Mergeable a1, ToSym a2 a1) => ToSym (First a2) (Union (First a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: First a2 -> Union (First a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Last a2) (Union (Last a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Last a2 -> Union (Last a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Down a2) (Union (Down a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Down a2 -> Union (Down a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Dual a2) (Union (Dual a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Dual a2 -> Union (Dual a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Product a2) (Union (Product a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Product a2 -> Union (Product a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Sum a2) (Union (Sum a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Sum a2 -> Union (Sum a1) Source #
(KnownNat n, 1 <= n) => ToSym (Union (IntN n)) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (WordN n) -> SymWordN n Source #
ToSym a b => ToSym (Union a) (Union b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union a -> Union b Source #
(Mergeable a1, ToSym a2 a1) => ToSym (Maybe a2) (Union (Maybe a1)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Maybe a2 -> Union (Maybe a1) Source #
(Mergeable a1, ToSym a2 a1) => ToSym [a2] (Union [a1]) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: [a2] -> Union [a1] Source #
(ToCon a1 a2, ToCon a3 a4) => ToCon (Union (Either a1 a3)) (Either a2 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (Either a1 a3) -> Maybe (Either a2 a4) Source #
(ToCon1 a1 a2, ToCon a3 a4) => ToCon (Union (MaybeT a1 a3)) (MaybeT a2 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (MaybeT a1 a3) -> Maybe (MaybeT a2 a4) Source #
(ToCon a1 a2, ToCon a3 a4) => ToCon (Union (a1, a3)) (a2, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3) -> Maybe (a2, a4) Source #
(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca --> cb)) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (ca --> cb) -> sa -~> sb Source #
(SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca =-> cb)) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (ca =-> cb) -> sa =~> sb Source #
(ToCon a1 a2, ToCon1 a3 a4, ToCon a5 a6) => ToCon (Union (ExceptT a1 a3 a5)) (ExceptT a2 a4 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (ExceptT a1 a3 a5) -> Maybe (ExceptT a2 a4 a6) Source #
(ToCon a1 a2, ToCon1 a3 a4, ToCon a5 a6) => ToCon (Union (WriterT a1 a3 a5)) (WriterT a2 a4 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (WriterT a1 a3 a5) -> Maybe (WriterT a2 a4 a6) Source #
(ToCon a1 a2, ToCon1 a3 a4, ToCon a5 a6) => ToCon (Union (WriterT a1 a3 a5)) (WriterT a2 a4 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (WriterT a1 a3 a5) -> Maybe (WriterT a2 a4 a6) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6) => ToCon (Union (a1, a3, a5)) (a2, a4, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5) -> Maybe (a2, a4, a6) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8) => ToCon (Union (a1, a3, a5, a7)) (a2, a4, a6, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7) -> Maybe (a2, a4, a6, a8) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10) => ToCon (Union (a1, a3, a5, a7, a9)) (a2, a4, a6, a8, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9) -> Maybe (a2, a4, a6, a8, a10) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12) => ToCon (Union (a1, a3, a5, a7, a9, a11)) (a2, a4, a6, a8, a10, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11) -> Maybe (a2, a4, a6, a8, a10, a12) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13)) (a2, a4, a6, a8, a10, a12, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13) -> Maybe (a2, a4, a6, a8, a10, a12, a14) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15)) (a2, a4, a6, a8, a10, a12, a14, a16) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17)) (a2, a4, a6, a8, a10, a12, a14, a16, a18) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20, ToCon a21 a22) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20, ToCon a21 a22, ToCon a23 a24) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20, ToCon a21 a22, ToCon a23 a24, ToCon a25 a26) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20, ToCon a21 a22, ToCon a23 a24, ToCon a25 a26, ToCon a27 a28) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25, a27)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26, a28) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25, a27) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26, a28) Source #
(ToCon a1 a2, ToCon a3 a4, ToCon a5 a6, ToCon a7 a8, ToCon a9 a10, ToCon a11 a12, ToCon a13 a14, ToCon a15 a16, ToCon a17 a18, ToCon a19 a20, ToCon a21 a22, ToCon a23 a24, ToCon a25 a26, ToCon a27 a28, ToCon a29 a30) => ToCon (Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25, a27, a29)) (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26, a28, a30) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union (a1, a3, a5, a7, a9, a11, a13, a15, a17, a19, a21, a23, a25, a27, a29) -> Maybe (a2, a4, a6, a8, a10, a12, a14, a16, a18, a20, a22, a24, a26, a28, a30) Source #
(IsConcrete k, Mergeable t) => Mergeable (HashMap k (Union (Maybe t))) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods rootStrategy :: MergingStrategy (HashMap k (Union (Maybe t))) Source # sortIndices :: HashMap k (Union (Maybe t)) -> [DynamicSortedIdx] 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 #
(Mergeable a1, Mergeable a2, ToSym a3 a1, ToSym a4 a2) => ToSym (Either a3 a4) (Union (Either a1 a2)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Either a3 a4 -> Union (Either a1 a2) Source #
(Mergeable1 a1, Mergeable a2, ToSym1 a3 a1, ToSym a4 a2) => ToSym (MaybeT a3 a4) (Union (MaybeT a1 a2)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: MaybeT a3 a4 -> Union (MaybeT a1 a2) Source #
(Mergeable a1, Mergeable a2, ToSym a3 a1, ToSym a4 a2) => ToSym (a3, a4) (Union (a1, a2)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a3, a4) -> Union (a1, a2) Source #
(Mergeable a1, Mergeable1 a2, Mergeable a3, ToSym a4 a1, ToSym1 a5 a2, ToSym a6 a3) => ToSym (ExceptT a4 a5 a6) (Union (ExceptT a1 a2 a3)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: ExceptT a4 a5 a6 -> Union (ExceptT a1 a2 a3) Source #
(Mergeable a1, Mergeable1 a2, Mergeable a3, ToSym a4 a1, ToSym1 a5 a2, ToSym a6 a3) => ToSym (WriterT a4 a5 a6) (Union (WriterT a1 a2 a3)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: WriterT a4 a5 a6 -> Union (WriterT a1 a2 a3) Source #
(Mergeable a1, Mergeable1 a2, Mergeable a3, ToSym a4 a1, ToSym1 a5 a2, ToSym a6 a3) => ToSym (WriterT a4 a5 a6) (Union (WriterT a1 a2 a3)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: WriterT a4 a5 a6 -> Union (WriterT a1 a2 a3) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, ToSym a4 a1, ToSym a5 a2, ToSym a6 a3) => ToSym (a4, a5, a6) (Union (a1, a2, a3)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a4, a5, a6) -> Union (a1, a2, a3) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, ToSym a5 a1, ToSym a6 a2, ToSym a7 a3, ToSym a8 a4) => ToSym (a5, a6, a7, a8) (Union (a1, a2, a3, a4)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a5, a6, a7, a8) -> Union (a1, a2, a3, a4) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, ToSym a6 a1, ToSym a7 a2, ToSym a8 a3, ToSym a9 a4, ToSym a10 a5) => ToSym (a6, a7, a8, a9, a10) (Union (a1, a2, a3, a4, a5)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a6, a7, a8, a9, a10) -> Union (a1, a2, a3, a4, a5) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, ToSym a7 a1, ToSym a8 a2, ToSym a9 a3, ToSym a10 a4, ToSym a11 a5, ToSym a12 a6) => ToSym (a7, a8, a9, a10, a11, a12) (Union (a1, a2, a3, a4, a5, a6)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a7, a8, a9, a10, a11, a12) -> Union (a1, a2, a3, a4, a5, a6) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, ToSym a8 a1, ToSym a9 a2, ToSym a10 a3, ToSym a11 a4, ToSym a12 a5, ToSym a13 a6, ToSym a14 a7) => ToSym (a8, a9, a10, a11, a12, a13, a14) (Union (a1, a2, a3, a4, a5, a6, a7)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a8, a9, a10, a11, a12, a13, a14) -> Union (a1, a2, a3, a4, a5, a6, a7) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, ToSym a9 a1, ToSym a10 a2, ToSym a11 a3, ToSym a12 a4, ToSym a13 a5, ToSym a14 a6, ToSym a15 a7, ToSym a16 a8) => ToSym (a9, a10, a11, a12, a13, a14, a15, a16) (Union (a1, a2, a3, a4, a5, a6, a7, a8)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a9, a10, a11, a12, a13, a14, a15, a16) -> Union (a1, a2, a3, a4, a5, a6, a7, a8) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, ToSym a10 a1, ToSym a11 a2, ToSym a12 a3, ToSym a13 a4, ToSym a14 a5, ToSym a15 a6, ToSym a16 a7, ToSym a17 a8, ToSym a18 a9) => ToSym (a10, a11, a12, a13, a14, a15, a16, a17, a18) (Union (a1, a2, a3, a4, a5, a6, a7, a8, a9)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a10, a11, a12, a13, a14, a15, a16, a17, a18) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, ToSym a11 a1, ToSym a12 a2, ToSym a13 a3, ToSym a14 a4, ToSym a15 a5, ToSym a16 a6, ToSym a17 a7, ToSym a18 a8, ToSym a19 a9, ToSym a20 a10) => ToSym (a11, a12, a13, a14, a15, a16, a17, a18, a19, a20) (Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a11, a12, a13, a14, a15, a16, a17, a18, a19, a20) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, Mergeable a11, ToSym a12 a1, ToSym a13 a2, ToSym a14 a3, ToSym a15 a4, ToSym a16 a5, ToSym a17 a6, ToSym a18 a7, ToSym a19 a8, ToSym a20 a9, ToSym a21 a10, ToSym a22 a11) => ToSym (a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22) (Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, Mergeable a11, Mergeable a12, ToSym a13 a1, ToSym a14 a2, ToSym a15 a3, ToSym a16 a4, ToSym a17 a5, ToSym a18 a6, ToSym a19 a7, ToSym a20 a8, ToSym a21 a9, ToSym a22 a10, ToSym a23 a11, ToSym a24 a12) => ToSym (a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24) (Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, Mergeable a11, Mergeable a12, Mergeable a13, ToSym a14 a1, ToSym a15 a2, ToSym a16 a3, ToSym a17 a4, ToSym a18 a5, ToSym a19 a6, ToSym a20 a7, ToSym a21 a8, ToSym a22 a9, ToSym a23 a10, ToSym a24 a11, ToSym a25 a12, ToSym a26 a13) => ToSym (a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26) (Union (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.ToSym Methods toSym :: (a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, Mergeable a11, Mergeable a12, Mergeable a13, Mergeable a14, ToSym a15 a1, ToSym a16 a2, ToSym a17 a3, ToSym a18 a4, ToSym a19 a5, ToSym a20 a6, ToSym a21 a7, ToSym a22 a8, ToSym a23 a9, ToSym a24 a10, ToSym a25 a11, ToSym a26 a12, ToSym a27 a13, ToSym a28 a14) => ToSym (a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28) (Union (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.ToSym Methods toSym :: (a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
(Mergeable a1, Mergeable a2, Mergeable a3, Mergeable a4, Mergeable a5, Mergeable a6, Mergeable a7, Mergeable a8, Mergeable a9, Mergeable a10, Mergeable a11, Mergeable a12, Mergeable a13, Mergeable a14, Mergeable a15, ToSym a16 a1, ToSym a17 a2, ToSym a18 a3, ToSym a19 a4, ToSym a20 a5, ToSym a21 a6, ToSym a22 a7, ToSym a23 a8, ToSym a24 a9, ToSym a25 a10, ToSym a26 a11, ToSym a27 a12, ToSym a28 a13, ToSym a29 a14, ToSym a30 a15) => ToSym (a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30) (Union (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.ToSym Methods toSym :: (a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30) -> Union (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #

unionUnaryOp :: (a -> a) -> Union a -> Union a Source #

Lift a unary operation to Union.

unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a Source #

Lift a binary operation to Union.

liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a Source #

Lift the Union to any Applicative SymBranching.

liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a Source #

Alias for liftUnion, but for monads.

unionBase :: Union a -> UnionBase a Source #

Extract the underlying Union. May be unmerged.

unionMergingStrategy :: Union a -> Maybe (MergingStrategy a) Source #

Get the (possibly empty) cached merging strategy.

isMerged :: Union a -> Bool Source #

Check if a Union is already merged.

unionSize :: Union a -> Int Source #

The size of a union is defined as the number of branches. For example,

>>> unionSize (return True)
1
>>> unionSize (mrgIf "a" (return 1) (return 2) :: Union Integer)
2
>>> unionSize (choose [1..7] "a" :: Union Integer)
7

class (Eq t, Ord t, Hashable t) => IsConcrete t Source #

Tag for concrete types. Useful for specifying the merge strategy for some parametrized types where we should have different merge strategy for symbolic and concrete ones.

Instances

Instances details

IsConcrete Integer Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union
IsConcrete Bool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union