| 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.SimpleMergeable
Description
Synopsis
- class Mergeable a => SimpleMergeable a where
- class 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 => 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
- class (SimpleMergeable1 u, Mergeable1 u) => UnionLike u where
- single :: a -> u a
- unionIf :: SymBool -> u a -> u a -> u a
- mergeWithStrategy :: MergingStrategy a -> u a -> u a
- mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a
- mrgSingleWithStrategy :: MergingStrategy a -> a -> u a
- mrgIf :: (UnionLike u, Mergeable a) => SymBool -> u a -> u a -> u a
- merge :: (UnionLike u, Mergeable a) => u a -> u a
- mrgSingle :: (UnionLike u, Mergeable a) => a -> u a
- class UnionLike u => UnionPrjOp (u :: Type -> Type) where
- pattern SingleU :: UnionPrjOp u => a -> u a
- pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a
- simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
- onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
- onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
- onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
- onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
- (#~) :: (Function f, SimpleMergeable (Ret f), UnionPrjOp u, Functor u) => f -> u (Arg f) -> Ret f
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 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 => 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
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))
UnionLike operations
class (SimpleMergeable1 u, Mergeable1 u) => UnionLike u 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.
Minimal complete definition
Methods
Wrap a single value in the union.
Note that this function cannot propagate the Mergeable knowledge.
>>>single "a" :: UnionM SymInteger<a>>>>mrgSingle "a" :: UnionM SymInteger{a}
unionIf :: SymBool -> u a -> u a -> u a Source #
If-then-else on two union values.
Note that this function cannot capture the Mergeable knowledge. However,
it may use the merging strategy from the branches to merge the results.
>>>unionIf "a" (single "b") (single "c") :: UnionM SymInteger<If a b c>>>>unionIf "a" (mrgSingle "b") (single "c") :: UnionM SymInteger{(ite a b c)}
mergeWithStrategy :: MergingStrategy a -> u a -> u a Source #
Merge the contents with some merge strategy.
>>>mergeWithStrategy rootStrategy $ unionIf "a" (single "b") (single "c") :: UnionM 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, merge is usually a better alternative.
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") (single "c") :: UnionM 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.
mrgSingleWithStrategy :: MergingStrategy a -> a -> u a Source #
Wrap a single value in the union and capture the Mergeable knowledge.
>>>mrgSingleWithStrategy rootStrategy "a" :: UnionM SymInteger{a}
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, mrgSingle is usually a better alternative.
Instances
mrgIf :: (UnionLike 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" (single "b") (single "c") :: UnionM SymInteger{(ite a b c)}
merge :: (UnionLike u, Mergeable a) => u a -> u a Source #
Merge the contents with the type's root merge strategy.
Equivalent to mergeWithStrategy rootStrategy
>>>merge $ unionIf "a" (single "b") (single "c") :: UnionM SymInteger{(ite a b c)}
mrgSingle :: (UnionLike u, Mergeable a) => a -> u a Source #
Wrap a single value in the type and propagate the type's root merge strategy.
Equivalent to mrgSingleWithStrategy rootStrategy
>>>mrgSingle "a" :: UnionM SymInteger{a}
class UnionLike u => UnionPrjOp (u :: Type -> Type) where Source #
Union containers that can be projected back into single value or if-guarded values.
Methods
singleView :: u a -> Maybe a Source #
Pattern match to extract single values.
>>>singleView (single 1 :: UnionM Integer)Just 1>>>singleView (unionIf "a" (single 1) (single 2) :: UnionM Integer)Nothing
ifView :: u a -> Maybe (SymBool, u a, u a) Source #
Pattern match to extract if values.
>>>ifView (single 1 :: UnionM Integer)Nothing>>>ifView (unionIf "a" (single 1) (single 2) :: UnionM Integer)Just (a,<1>,<2>)>>>ifView (mrgIf "a" (single 1) (single 2) :: UnionM Integer)Just (a,{1},{2})
The leftmost value in the union.
>>>leftMost (unionIf "a" (single 1) (single 2) :: UnionM Integer)1
Instances
pattern SingleU :: UnionPrjOp u => a -> u a Source #
Pattern match to extract single values with singleView.
>>>case (single 1 :: UnionM Integer) of SingleU v -> v1
pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a Source #
simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a Source #
Merge the simply mergeable values in a union, and extract the merged value.
In the following example, unionIf will not merge the results, and
simpleMerge will merge it and extract the single merged value.
>>>unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool<If a b c>>>>simpleMerge $ (unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool)(ite a b c)
onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r Source #
Lift a function to work on union values.
>>>sumU = onUnion sum>>>sumU (unionIf "cond" (return ["a"]) (return ["b","c"]) :: UnionM [SymInteger])(ite cond a (+ b c))
onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r Source #
Lift a function to work on union values.
onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r Source #
Lift a function to work on union values.
onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r Source #
Lift a function to work on union values.
(#~) :: (Function f, SimpleMergeable (Ret f), UnionPrjOp u, Functor u) => f -> u (Arg f) -> Ret f infixl 9 Source #
Helper for applying functions on UnionPrjOp and SimpleMergeable.
>>>let f :: Integer -> UnionM Integer = \x -> mrgIf (ssym "a") (mrgSingle $ x + 1) (mrgSingle $ x + 2)>>>f #~ (mrgIf (ssym "b" :: SymBool) (mrgSingle 0) (mrgSingle 2) :: UnionM Integer){If (&& b a) 1 (If b 2 (If a 3 4))}