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 |
Synopsis
- data Union a
- ifWithLeftMost :: Bool -> SymBool -> Union a -> Union a -> Union a
- ifWithStrategy :: MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
- fullReconstruct :: MergingStrategy a -> Union a -> Union a
- data UnionM a where
- underlyingUnion :: UnionM a -> Union a
- isMerged :: UnionM a -> Bool
The UnionBase type
The default union implementation.
UnionSingle a | A single value |
UnionIf | A if value |
Instances
ifWithStrategy :: MergingStrategy a -> SymBool -> Union a -> Union a -> Union a Source #
Use a specific strategy to build a UnionIf
value.
The merged invariant will be maintained in the result.
fullReconstruct :: MergingStrategy a -> Union a -> Union a Source #
Fully reconstruct a Union
to maintain the merged invariant.
The UnionMBase type
UnionM
is the Union
container (hidden) enhanced with
MergingStrategy
knowledge propagation.
The Union
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 Union a = Single a | If bool (Union a) (Union a)
The Single
constructor is for a single value with the path condition
true
, and the If
constructor is the if operator in an if-then-else
tree.
For clarity, when printing a UnionM
value, we will omit the Single
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 Union
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.
Union
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, UnionM
that
would try to cache the merging strategy.
The UnionM
has two data constructors (hidden intentionally), UAny
and UMrg
.
The UAny
data constructor (printed as <
...
>
) wraps an arbitrary (probably
unmerged) Union
. 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 UnionM
along with the
Mergeable
constraint. This constraint can be propagated to the contexts
without Mergeable
knowledge, and helps the system to merge the resulting
Union
.
Examples:
return
cannot resolve the Mergeable
constraint.
>>>
return 1 :: UnionM Integer
<1>
mrgReturn
can resolve the Mergeable
constraint.
>>>
import Grisette.Lib.Base
>>>
mrgReturn 1 :: UnionM Integer
{1}
unionIf
cannot resolve the Mergeable
constraint.
>>>
unionIf "a" (return 1) (unionIf "b" (return 1) (return 2)) :: UnionM Integer
<If a 1 (If b 1 2)>
But unionIf
is able to merge the result if some of the branches are merged:
>>>
unionIf "a" (return 1) (unionIf "b" (mrgReturn 1) (return 2)) :: UnionM Integer
{If (|| a b) 1 2}
The >>=
operator uses unionIf
internally. When the final statement in a do-block
merges the values, the system can then merge the final result.
>>>
:{
do x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2)) mrgSingle $ x + 1 :: UnionM 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
>>>
:{
do x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2)) f x (x + 1) :: UnionM Integer :} {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.
UAny | |
UMrg | |
|
Instances
underlyingUnion :: UnionM a -> Union a Source #
Extract the underlying Union. May be unmerged.