| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Core.Data.Class.Mergeable
Description
Synopsis
- data MergingStrategy a where
- SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a
- SortedStrategy :: (Ord idx, Typeable idx, Show idx) => (a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
- NoStrategy :: MergingStrategy a
- class Mergeable a where
- class Mergeable1 (u :: Type -> Type) where
- liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)
- rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)
- class Mergeable2 (u :: Type -> Type -> Type) where
- liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
- rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b)
- class Mergeable3 (u :: Type -> Type -> Type -> Type) where
- liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c)
- rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c)
- class Mergeable' f where
- rootStrategy' :: MergingStrategy (f a)
- derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a
- wrapStrategy :: MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
- product2Strategy :: (a -> b -> r) -> (r -> (a, b)) -> MergingStrategy a -> MergingStrategy b -> MergingStrategy r
- data DynamicSortedIdx where
- DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx
- data StrategyList container where
- StrategyList :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
- resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
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 typeInteger, can be simply merged as the set contains only a single value. - all the
Justvalues of the typeMaybe SymBoolcan be simply merged by merging the wrapped symbolic boolean withites.
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
SortedStrategyby indexing with the identity function and use theSimpleStrategyshown before as the sub-strategies. - all the
Maybe SymBoolvalues can be merged withSortedStrategyby indexing withisJust, theNothingandJustvalues 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 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)
Instances
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
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.
Instances
| Mergeable2 Either Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (Either a b) Source # | |
| Mergeable2 (,) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b) Source # | |
| Mergeable a => Mergeable2 ((,,) a) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a0 -> MergingStrategy b -> MergingStrategy (a, a0, b) Source # | |
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
| Mergeable3 (,,) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (a, b, c) Source # | |
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.
Methods
rootStrategy' :: MergingStrategy (f a) Source #
Instances
| Mergeable' (U1 :: Type -> Type) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy' :: MergingStrategy (U1 a) Source # | |
| Mergeable' (V1 :: Type -> Type) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy' :: MergingStrategy (V1 a) Source # | |
| (Mergeable' a, Mergeable' b) => Mergeable' (a :*: b) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy' :: MergingStrategy ((a :*: b) a0) Source # | |
| (Mergeable' a, Mergeable' b) => Mergeable' (a :+: b) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy' :: MergingStrategy ((a :+: b) a0) Source # | |
| Mergeable c => Mergeable' (K1 i c :: Type -> Type) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy' :: MergingStrategy (K1 i c a) Source # | |
| Mergeable' a => Mergeable' (M1 i c a) Source # | |
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
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)
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 Xdata 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 |
Instances
| Show DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods showsPrec :: Int -> DynamicSortedIdx -> ShowS # show :: DynamicSortedIdx -> String # showList :: [DynamicSortedIdx] -> ShowS # | |
| Eq DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods (==) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (/=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # | |
| Ord DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods compare :: DynamicSortedIdx -> DynamicSortedIdx -> Ordering # (<) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (<=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # max :: DynamicSortedIdx -> DynamicSortedIdx -> DynamicSortedIdx # min :: DynamicSortedIdx -> DynamicSortedIdx -> 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
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.