| 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 | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Internal.Core.Data.Class.Mergeable
Description
Synopsis
- data MergingStrategy a where
- SimpleStrategy :: forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
- SortedStrategy :: forall idx a. (Ord idx, Typeable idx, Show idx) => (a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
- NoStrategy :: forall a. MergingStrategy a
- class Mergeable a where
- rootStrategy :: MergingStrategy a
- sortIndices :: a -> [DynamicSortedIdx]
- class (forall a. Mergeable a => Mergeable (u a)) => Mergeable1 (u :: Type -> Type) where
- liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)
- rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)
- class (forall a. Mergeable a => Mergeable1 (u a)) => 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 (forall a. Mergeable a => Mergeable2 (u a)) => 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)
- data family MergeableArgs arity a
- class GMergeable arity (f :: Type -> Type) where
- grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a)
- genericRootStrategy :: (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a
- genericLiftRootStrategy :: (Generic1 f, GMergeable Arity1 (Rep1 f)) => MergingStrategy a -> MergingStrategy (f 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 :: Type -> Type) where
- StrategyList :: forall a (container :: Type -> Type). container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- resolveStrategy :: MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
- resolveStrategy' :: x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
- resolveMergeable1 :: (Mergeable1 f, Mergeable a) => (Mergeable (f a) => r) -> r
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
symIte. - 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 withsymIte.
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 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 symIte :: 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 $ symIte cond l r) |
Fields
| |
| NoStrategy :: forall a. 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)
Minimal complete definition
Methods
rootStrategy :: MergingStrategy a Source #
The root merging strategy for the type.
sortIndices :: a -> [DynamicSortedIdx] Source #
Instances
class (forall a. Mergeable a => Mergeable (u a)) => 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 (forall a. Mergeable a => Mergeable1 (u a)) => 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
rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b) Source #
Lift the root merge strategy through the binary type constructor.
class (forall a. Mergeable a => Mergeable2 (u a)) => 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
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.
Generic Mergeable
data family MergeableArgs arity a Source #
The arguments to the generic merging strategy function.
Instances
| data MergeableArgs Arity0 _ Source # | |
| newtype MergeableArgs Arity1 a Source # | |
class GMergeable arity (f :: Type -> Type) where Source #
The class of types that can be generically merged.
Methods
grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a) Source #
Instances
genericRootStrategy :: (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a Source #
Generic rootStrategy.
genericLiftRootStrategy :: (Generic1 f, GMergeable Arity1 (Rep1 f)) => MergingStrategy a -> MergingStrategy (f a) Source #
Generic liftRootStrategy.
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.Internal.Internal.Decl.Core.Data.Class.Mergeable Methods showsPrec :: Int -> DynamicSortedIdx -> ShowS # show :: DynamicSortedIdx -> String # showList :: [DynamicSortedIdx] -> ShowS # | |
| Eq DynamicSortedIdx Source # | |
Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable Methods (==) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (/=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # | |
| Ord DynamicSortedIdx Source # | |
Defined in Grisette.Internal.Internal.Decl.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 :: Type -> Type) where Source #
Helper type for building efficient merge strategy for list-like containers.
Constructors
| StrategyList :: forall a (container :: Type -> Type). container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container |
Instances
buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container Source #
Helper function for building efficient merge strategy for list-like containers.
resolveStrategy :: MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x) Source #
Resolves the indices and the terminal merge strategy for a value of some
Mergeable type.
resolveStrategy' :: 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.
resolveMergeable1 :: (Mergeable1 f, Mergeable a) => (Mergeable (f a) => r) -> r Source #
Workaround as GHC prior to 9.6 doesn't support quantified constraints reliably.
Similar to https://github.com/haskell/core-libraries-committee/issues/10, which is only available with 9.6 or higher.