grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Mergeable

Description

 
Synopsis

Merging strategy

data MergingStrategy a where Source #

Merging strategies.

You probably do not need to know the details of this type if you are only going to use algebraic data types. You can get merging strategies for them with type derivation.

In Grisette, a merged union (if-then-else tree) follows the hierarchical sorted representation invariant with regards to some merging strategy.

A merging strategy encodes how to merge a subset of the values of a given type. We have three types of merging strategies:

  • Simple strategy
  • Sorted strategy
  • No strategy

The SimpleStrategy merges values with a simple merge function. For example,

  • the symbolic boolean values can be directly merged with ites.
  • the set {1}, which is a subset of the values of the type Integer, can be simply merged as the set contains only a single value.
  • all the Just values of the type Maybe SymBool can be simply merged by merging the wrapped symbolic boolean with ites.

The SortedStrategy merges values by first grouping the values with an indexing function, and the values with the same index will be organized as a sub-tree in the if-then-else structure of UnionBase. Each group (sub-tree) will be further merged with a sub-strategy for the index. The index type should be a totally ordered type (with the Ord type class). Grisette will use the indexing function to partition the values into sub-trees, and organize them in a sorted way. The sub-trees will further be merged with the sub-strategies. For example,

  • all the integers can be merged with SortedStrategy by indexing with the identity function and use the SimpleStrategy shown before as the sub-strategies.
  • all the Maybe SymBool values can be merged with SortedStrategy by indexing with isJust, the Nothing and Just values can then then be merged with different simple strategies as sub-strategies.

The NoStrategy does not perform any merging. For example, we cannot merge values with function types that returns concrete lists.

For ADTs, we can automatically derive the Mergeable type class, which provides a merging strategy.

If the derived version does not work for you, you should determine if your type can be directly merged with a merging function. If so, you can implement the merging strategy as a SimpleStrategy. If the type cannot be directly merged with a merging function, but could be partitioned into subsets of values that can be simply merged with a function, you should implement the merging strategy as a SortedStrategy. For easier building of the merging strategies, check out the combinators like wrapStrategy.

For more details, please see the documents of the constructors, or refer to Grisette's paper.

Constructors

SimpleStrategy

Simple mergeable strategy.

For symbolic booleans, we can implement its merge strategy as follows:

SimpleStrategy ites :: MergingStrategy SymBool

Fields

SortedStrategy

Sorted mergeable strategy.

For Integers, we can implement its merge strategy as follows:

SortedStrategy id (\_ -> SimpleStrategy $ \_ t _ -> t)

For Maybe SymBool, we can implement its merge strategy as follows:

SortedStrategy
  (\case; Nothing -> False; Just _ -> True)
  (\idx ->
     if idx
       then SimpleStrategy $ \_ t _ -> t
       else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ ites cond l r)

Fields

NoStrategy :: MergingStrategy a

For preventing the merging intentionally. This could be useful for keeping some value concrete and may help generate more efficient formulas.

See Grisette's paper for details.

Mergeable

class Mergeable a where Source #

Each type is associated with a root merge strategy given by rootStrategy. The root merge strategy should be able to merge every value of the type. Grisette will use the root merge strategy to merge the values of the type in a union.

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

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

Methods

rootStrategy :: MergingStrategy a Source #

The root merging strategy for the type.

Instances

Instances details
Mergeable ArithException Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Ordering Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Mergeable VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Mergeable BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable CEGISCondition Source # 
Instance details

Defined in Grisette.Core.Data.Class.CEGISSolver

Mergeable FreshIndex Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Mergeable SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable () Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable a => Mergeable (Sum a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Control.Monad.UnionM

(KnownNat n, 1 <= n) => Mergeable (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(KnownNat n, 1 <= n) => Mergeable (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Union

(KnownNat n, 1 <= n) => Mergeable (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(KnownNat n, 1 <= n) => Mergeable (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable a => Mergeable (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable a => Mergeable [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable e, Mergeable a) => Mergeable (Either e a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable (U1 x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable (V1 x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Control.Monad.CBMCExcept

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

Defined in Grisette.Core.Data.Class.GenSym

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa -~> sb) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa =~> sb) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Control.Monad.UnionM

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Control.Monad.CBMCExcept

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable s, Mergeable a, Mergeable1 m) => Mergeable (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable s, Mergeable a, Mergeable1 m) => Mergeable (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c) Source #

(Mergeable1 l, Mergeable1 r, Mergeable x) => Mergeable (Sum l r x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable (a x), Mergeable (b x)) => Mergeable ((a :*: b) x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable (a x), Mergeable (b x)) => Mergeable ((a :+: b) x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable c => Mergeable (K1 i c x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c, d) Source #

Mergeable (a x) => Mergeable (M1 i c a x) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (M1 i c a x) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (RWST r w s m a) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (RWST r w s m a) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c, d, e) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c, d, e, f) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c, d, e, f, g) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (a, b, c, d, e, f, g, h) Source #

class Mergeable1 (u :: Type -> Type) where Source #

Lifting of the Mergeable class to unary type constructors.

Methods

liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a) Source #

Lift merge strategy through the type constructor.

Instances

Instances details
Mergeable1 Identity Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable1 Sum Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Mergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Mergeable1 Maybe Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable1 [] Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable e => Mergeable1 (Either e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Generic1 u, Mergeable1' (Rep1 u)) => Mergeable1 (Default1 u) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable e => Mergeable1 (CBMCEither e) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

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

Defined in Grisette.Core.Data.Class.GenSym

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

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable a => Mergeable1 ((,) a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Control.Monad.CBMCExcept

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable a, Mergeable b) => Mergeable1 ((,,) a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable1 l, Mergeable1 r) => Mergeable1 (Sum l r) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

liftRootStrategy :: MergingStrategy a0 -> MergingStrategy (a, b, c, d, a0) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

liftRootStrategy :: MergingStrategy a0 -> MergingStrategy (a, b, c, d, e, a0) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

liftRootStrategy :: MergingStrategy a0 -> MergingStrategy (a, b, c, d, e, f, a0) Source #

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

Defined in Grisette.Core.Data.Class.Mergeable

Methods

liftRootStrategy :: MergingStrategy a0 -> MergingStrategy (a, b, c, d, e, f, g, a0) Source #

rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a) Source #

Lift the root merge strategy through the unary type constructor.

class Mergeable2 (u :: Type -> Type -> Type) where Source #

Lifting of the Mergeable class to binary type constructors.

Methods

liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b) Source #

Lift merge strategy through the type constructor.

rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b) Source #

Lift the root merge strategy through the binary type constructor.

class Mergeable3 (u :: Type -> Type -> Type -> Type) where Source #

Lifting of the Mergeable class to ternary type constructors.

Methods

liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c) Source #

Lift merge strategy through the type constructor.

Instances

Instances details
Mergeable3 (,,) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c) Source #

Lift the root merge strategy through the binary type constructor.

class Mergeable' f where Source #

Auxiliary class for the generic derivation for the Mergeable class.

Instances

Instances details
Mergeable' (U1 :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable' (V1 :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable' a, Mergeable' b) => Mergeable' (a :*: b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(Mergeable' a, Mergeable' b) => Mergeable' (a :+: b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable c => Mergeable' (K1 i c :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Mergeable' a => Mergeable' (M1 i c a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy' :: MergingStrategy (M1 i c a a0) Source #

derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a Source #

Generic derivation for the Mergeable class.

Usually you can derive the merging strategy with the DerivingVia and DerivingStrategies extension.

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

Combinators for manually building merging strategies

wrapStrategy Source #

Arguments

:: MergingStrategy a

The merge strategy to be wrapped

-> (a -> b)

The wrap function

-> (b -> a)

The unwrap function, which does not have to be defined for every value

-> MergingStrategy b 

Useful utility function for building merge strategies manually.

For example, to build the merge strategy for the just branch of Maybe a, one could write

wrapStrategy Just fromMaybe rootStrategy :: MergingStrategy (Maybe a)

product2Strategy Source #

Arguments

:: (a -> b -> r)

The wrap function

-> (r -> (a, b))

The unwrap function, which does not have to be defined for every value

-> MergingStrategy a

The first merge strategy to be wrapped

-> MergingStrategy b

The second merge strategy to be wrapped

-> MergingStrategy r 

Useful utility function for building merge strategies for product types manually.

For example, to build the merge strategy for the following product type, one could write

data X = X { x1 :: Int, x2 :: Bool }
product2Strategy X (\(X a b) -> (a, b)) rootStrategy rootStrategy
  :: MergingStrategy X

data DynamicSortedIdx where Source #

Helper type for combining arbitrary number of indices into one. Useful when trying to write efficient merge strategy for lists/vectors.

Constructors

DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx 

data StrategyList container where Source #

Helper type for building efficient merge strategy for list-like containers.

Constructors

StrategyList :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container 

Instances

Instances details
Show1 container => Show (StrategyList container) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Methods

showsPrec :: Int -> StrategyList container -> ShowS #

show :: StrategyList container -> String #

showList :: [StrategyList container] -> ShowS #

Eq1 container => Eq (StrategyList container) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Methods

(==) :: StrategyList container -> StrategyList container -> Bool #

(/=) :: StrategyList container -> StrategyList container -> Bool #

Ord1 container => Ord (StrategyList container) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

Methods

compare :: StrategyList container -> StrategyList container -> Ordering #

(<) :: StrategyList container -> StrategyList container -> Bool #

(<=) :: StrategyList container -> StrategyList container -> Bool #

(>) :: StrategyList container -> StrategyList container -> Bool #

(>=) :: StrategyList container -> StrategyList container -> Bool #

max :: StrategyList container -> StrategyList container -> StrategyList container #

min :: StrategyList container -> StrategyList container -> StrategyList container #

buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container Source #

Helper function for building efficient merge strategy for list-like containers.

resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x) Source #

Resolves the indices and the terminal merge strategy for a value of some Mergeable type.

resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x) Source #

Resolves the indices and the terminal merge strategy for a value given a merge strategy for its type.