| 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.Control.Monad.Union
Contents
Description
Synopsis
- data Union a where
- unionUnaryOp :: (a -> a) -> Union a -> Union a
- unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a
- liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a
- liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a
- unionBase :: Union a -> UnionBase a
- unionMergingStrategy :: Union a -> Maybe (MergingStrategy a)
- isMerged :: Union a -> Bool
- unionSize :: Union a -> Int
- class (Eq t, Ord t, Hashable t) => IsConcrete t
Union and helpers
Union is the UnionBase container (hidden) enhanced with
MergingStrategy
knowledge propagation.
The UnionBase models the underlying semantics evaluation semantics for
unsolvable types with the nested if-then-else tree semantics, and can be
viewed as the following structure:
data UnionBase a = UnionSingle a | UnionIf bool (Union a) (Union a)
The UnionSingle constructor is for a single value with the path condition
true, and the UnionIf constructor is the if operator in an if-then-else
tree.
For clarity, when printing a Union value, we will omit the UnionSingle
constructor. The following two representations has the same semantics.
If c1 (If c11 v11 (If c12 v12 v13))
(If c2 v2
v3)\[ \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right. \]
To reduce the size of the if-then-else tree to reduce the number of paths to
execute, Grisette would merge the branches in a UnionBase container and
maintain a representation invariant for them. To perform this merging
procedure, Grisette relies on a type class called Mergeable and the
merging strategy defined by it.
UnionBase is a monad, so we can easily write code with the do-notation and
monadic combinators. However, the standard monadic operators cannot
resolve any extra constraints, including the Mergeable constraint (see
The constrained-monad
problem
by Sculthorpe et al.).
This prevents the standard do-notations to merge the results automatically,
and would result in bad performance or very verbose code.
To reduce this boilerplate, Grisette provide another monad, Union that
would try to cache the merging strategy.
The Union has two data constructors (hidden intentionally), UAny and
UMrg. The UAny data constructor (printed as <...>) wraps an
arbitrary (probably unmerged) UnionBase. It is constructed when no
Mergeable knowledge is available (for example, when constructed with
Haskell's return). The UMrg data constructor (printed as {...}) wraps
a merged UnionBase along with the Mergeable constraint. This constraint
can be propagated to the contexts without Mergeable knowledge, and helps
the system to merge the resulting UnionBase.
Examples:
return cannot resolve the Mergeable constraint.
>>>return 1 :: Union Integer<1>
mrgReturn can resolve the Mergeable constraint.
>>>import Grisette.Lib.Base>>>mrgReturn 1 :: Union Integer{1}
mrgIfPropagatedStrategy does not try to Mergeable constraint.
>>>mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: Union Integer<If a 1 (If b 1 2)>
But mrgIfPropagatedStrategy is able to merge the result if some of the
branches are merged and have a cached merging strategy:
>>>mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (mrgReturn 1) (return 2)) :: Union Integer{If (|| a b) 1 2}
The >>= operator uses mrgIfPropagatedStrategy internally. When the final
statement in a do-block merges the values, the system can then merge the
final result.
>>>:{do x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2)) mrgSingle $ x + 1 :: Union Integer :} {If (|| a b) 2 3}
Calling a function that merges a result at the last line of a do-notation
will also merge the whole block. If you stick to these mrg* combinators and
all the functions will merge the results, the whole program can be
symbolically evaluated efficiently.
>>>f x y = mrgIf "c" x y :: Union Integer>>>:{do x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2)) f x (x + 1) :} {If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}
In Grisette.Lib.Base, Grisette.Lib.Mtl, we also provided more mrg*
variants of other combinators. You should stick to these combinators to
ensure efficient merging by Grisette.
Constructors
| UAny | |
| UMrg | |
Fields
| |
Instances
unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a Source #
Lift a binary operation to Union.
liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a Source #
Lift the Union to any Applicative SymBranching.
liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a Source #
Alias for liftUnion, but for monads.
unionMergingStrategy :: Union a -> Maybe (MergingStrategy a) Source #
Get the (possibly empty) cached merging strategy.
unionSize :: Union a -> Int Source #
The size of a union is defined as the number of branches. For example,
>>>unionSize (return True)1>>>unionSize (mrgIf "a" (return 1) (return 2) :: Union Integer)2>>>unionSize (choose [1..7] "a" :: Union Integer)7