| 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 | Trustworthy |
| Language | Haskell2010 |
Grisette.Internal.Core.Data.Class.SimpleMergeable
Description
Synopsis
- class Mergeable a => SimpleMergeable a where
- class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 u where
- liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a
- mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a
- class (Mergeable2 u, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 u where
- liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b
- mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b
- data family SimpleMergeableArgs arity a :: Type
- class GSimpleMergeable arity f where
- gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a
- genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a
- genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a
- class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) where
- mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a
- mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a
- mrgIf :: (SymBranching u, Mergeable a) => SymBool -> u a -> u a -> u a
- mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a
- merge :: (SymBranching m, Mergeable a) => m a -> m a
Simple mergeable types
class Mergeable a => SimpleMergeable a where Source #
This class indicates that a type has a simple root merge strategy.
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving (Mergeable, SimpleMergeable) via (Default X)
Methods
mrgIte :: SymBool -> a -> a -> a Source #
Performs if-then-else with the simple root merge strategy.
>>>mrgIte "a" "b" "c" :: SymInteger(ite a b c)
Instances
class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 u where Source #
Lifting of the SimpleMergeable class to unary type constructors.
Methods
liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte mrgIte "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
Instances
mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte1 "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
class (Mergeable2 u, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 u where Source #
Lifting of the SimpleMergeable class to binary type constructors.
Methods
liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte2 mrgIte mrgIte "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
Instances
| SimpleMergeable2 (,) Source # | |
| SimpleMergeable a => SimpleMergeable2 ((,,) a) Source # | |
| (SimpleMergeable a, SimpleMergeable b) => SimpleMergeable2 ((,,,) a b) Source # | |
| SimpleMergeable2 (->) Source # | |
mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte2 "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
Generic SimpleMergeable
data family SimpleMergeableArgs arity a :: Type Source #
The arguments to the generic simple merging function.
Instances
| data SimpleMergeableArgs Arity0 _ Source # | |
| newtype SimpleMergeableArgs Arity1 a Source # | |
class GSimpleMergeable arity f where Source #
Generic SimpleMergeable class.
Methods
gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a Source #
Instances
| GSimpleMergeable Arity1 Par1 Source # | |
| GSimpleMergeable arity (U1 :: Type -> Type) Source # | |
| GSimpleMergeable arity (V1 :: Type -> Type) Source # | |
| SimpleMergeable1 f => GSimpleMergeable Arity1 (Rec1 f) Source # | |
| (GSimpleMergeable arity a, GSimpleMergeable arity b) => GSimpleMergeable arity (a :*: b) Source # | |
| SimpleMergeable c => GSimpleMergeable arity (K1 i c :: Type -> Type) Source # | |
| (SimpleMergeable1 f, GSimpleMergeable Arity1 g) => GSimpleMergeable Arity1 (f :.: g) Source # | |
| GSimpleMergeable arity a => GSimpleMergeable arity (M1 i c a) Source # | |
genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a Source #
Generic mrgIte function.
genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a Source #
Generic liftMrgIte function.
Symbolic branching
class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) where Source #
Special case of the Mergeable1 and SimpleMergeable1 class for type
constructors that are SimpleMergeable when applied to any Mergeable
types.
This type class is used to generalize the mrgIf function to other
containers, for example, monad transformer transformed Unions.
Methods
mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with some merge
strategy.
>>>mrgIfWithStrategy rootStrategy "a" (mrgSingle "b") (return "c") :: Union SymInteger{(ite a b c)}
Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be
resolved, e.g., the merge strategy for the contained type is given with
Mergeable1. In other cases, mrgIf is usually a better alternative.
mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result.
This function does not need a merging strategy, and it will merge the result only if any of the branches is merged.
Instances
mrgIf :: (SymBranching u, Mergeable a) => SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with the type's root
merge strategy.
Equivalent to mrgIfWithStrategy rootStrategy
>>>mrgIf "a" (return "b") (return "c") :: Union SymInteger{(ite a b c)}
mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a Source #
Try to merge the container with a given merge strategy.
merge :: (SymBranching m, Mergeable a) => m a -> m a Source #
Try to merge the container with the root strategy.