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 symIte.
• 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 symIte.

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.

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)

Lifting of the Mergeable class to unary type constructors.

Lift the root merge strategy through the unary type constructor.

Lifting of the Mergeable class to binary type constructors.

Lift the root merge strategy through the binary type constructor.

Lifting of the Mergeable class to ternary type constructors.

Lift the root merge strategy through the binary type constructor.

Auxiliary class for the generic derivation for the Mergeable class.

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)

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)

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

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

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

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

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

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