Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.Core.Data.Class.UnionView

Description

Synopsis

class (Applicative u, TryMerge u) => UnionView (u :: Type -> Type) where
- singleView :: u a -> Maybe a
- ifView :: u a -> Maybe (IfViewResult u a)
- toGuardedList :: u a -> [(SymBool, a)]
- overestimateUnionValues :: Mergeable a => u a -> [a]
data IfViewResult (u :: Type -> Type) a where
- IfViewResult :: forall (u :: Type -> Type) a. SymBranching u => SymBool -> u a -> u a -> IfViewResult u a
pattern Single :: (UnionView u, Mergeable a) => a -> u a
pattern If :: (UnionView u, Mergeable a) => SymBranching u => SymBool -> u a -> u a -> u a
simpleMerge :: forall u a. (SimpleMergeable a, UnionView u) => u a -> a
symIteMerge :: (ITEOp a, Mergeable a, UnionView u) => u a -> a
(.#) :: (Function f a r, SimpleMergeable r, UnionView u) => f -> u a -> r
onUnion :: forall u a r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a) => (a -> r) -> u a -> r
onUnion2 :: forall u a b r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b) => (a -> b -> r) -> u a -> u b -> r
onUnion3 :: forall u a b c r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b, Mergeable c) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
onUnion4 :: forall u a b c d r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b, Mergeable c, Mergeable d) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
unionToCon :: (ToCon a b, UnionView u) => u a -> Maybe b
liftUnion :: (Mergeable a, UnionView u, Applicative m, SymBranching m) => u a -> m a
liftToMonadUnion :: (Mergeable a, UnionView u, Monad m, SymBranching m) => u a -> m a

Documentation

class (Applicative u, TryMerge u) => UnionView (u :: Type -> Type) where Source #

Containers that can be projected back into single value or if-guarded values. Identity is an instance of this class as we can always project to single value.

Minimal complete definition

singleView, ifView

Methods

singleView :: u a -> Maybe a Source #

Pattern match to extract single values.

>>> singleView (return 1 :: Union Integer)
Just 1
>>> singleView (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer)
Nothing

ifView :: u a -> Maybe (IfViewResult u a) Source #

Pattern match to extract if values.

>>> ifView (return 1 :: Union Integer)
Nothing
>>> ifView (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer)
Just (IfViewResult a <1> <2>)
>>> ifView (mrgIf "a" (return 1) (return 2) :: Union Integer)
Just (IfViewResult a {1} {2})

toGuardedList :: u a -> [(SymBool, a)] Source #

Convert the union to a guarded list.

>>> toGuardedList (mrgIf "a" (return 1) (mrgIf "b" (return 2) (return 3)) :: Union Integer)
[(a,1),((&& b (! a)),2),((! (|| b a)),3)]

overestimateUnionValues :: Mergeable a => u a -> [a] Source #

Return all possible values in the union. Drop the path conditions.

>>> overestimateUnionValues (return 1 :: Union Integer)
[1]

>>> overestimateUnionValues (mrgIf "a" (return 1) (return 2) :: Union Integer)
[1,2]

Instances

Instances details

UnionView Identity Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.UnionView Methods singleView :: Identity a -> Maybe a Source # ifView :: Identity a -> Maybe (IfViewResult Identity a) Source # toGuardedList :: Identity a -> [(SymBool, a)] Source # overestimateUnionValues :: Mergeable a => Identity a -> [a] Source #
UnionView Union Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods singleView :: Union a -> Maybe a Source # ifView :: Union a -> Maybe (IfViewResult Union a) Source # toGuardedList :: Union a -> [(SymBool, a)] Source # overestimateUnionValues :: Mergeable a => Union a -> [a] Source #
UnionView UnionBase Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase Methods singleView :: UnionBase a -> Maybe a Source # ifView :: UnionBase a -> Maybe (IfViewResult UnionBase a) Source # toGuardedList :: UnionBase a -> [(SymBool, a)] Source # overestimateUnionValues :: Mergeable a => UnionBase a -> [a] Source #
UnionView u => UnionView (AsKey1 u) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.UnionView Methods singleView :: AsKey1 u a -> Maybe a Source # ifView :: AsKey1 u a -> Maybe (IfViewResult (AsKey1 u) a) Source # toGuardedList :: AsKey1 u a -> [(SymBool, a)] Source # overestimateUnionValues :: Mergeable a => AsKey1 u a -> [a] Source #

data IfViewResult (u :: Type -> Type) a where Source #

The result of ifView.

Constructors

IfViewResult :: forall (u :: Type -> Type) a. SymBranching u => SymBool -> u a -> u a -> IfViewResult u a

Instances

Instances details

Show (u a) => Show (IfViewResult u a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.UnionView Methods showsPrec :: Int -> IfViewResult u a -> ShowS # show :: IfViewResult u a -> String # showList :: [IfViewResult u a] -> ShowS #

pattern Single :: (UnionView u, Mergeable a) => a -> u a Source #

Pattern match to extract single values with singleView.

>>> case (return 1 :: Union Integer) of Single v -> v
1

pattern If :: (UnionView u, Mergeable a) => SymBranching u => SymBool -> u a -> u a -> u a Source #

Pattern match to extract guard values with ifView

>>> case (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer) of If c t f -> (c,t,f)
(a,<1>,<2>)

simpleMerge :: forall u a. (SimpleMergeable a, UnionView u) => u a -> a Source #

Merge the simply mergeable values in a union, and extract the merged value.

In the following example, mrgIfPropagatedStrategy will not merge the results, and simpleMerge will merge it and extract the single merged value.

>>> mrgIfPropagatedStrategy (ssym "a") (return $ ssym "b") (return $ ssym "c") :: Union SymBool
<If a b c>
>>> simpleMerge $ (mrgIfPropagatedStrategy (ssym "a") (return $ ssym "b") (return $ ssym "c") :: Union SymBool)
(ite a b c)

symIteMerge :: (ITEOp a, Mergeable a, UnionView u) => u a -> a Source #

Merge the mergeable values in a union, using symIte, and extract the merged value.

The reason why we provide this class is that for some types, we only have ITEOp (which may throw an error), and we don't have a SimpleMergeable instance. In this case, we can use symIteMerge to merge the values.

(.#) :: (Function f a r, SimpleMergeable r, UnionView u) => f -> u a -> r infixl 9 Source #

Helper for applying functions on UnionView and SimpleMergeable.

>>> let f :: Integer -> Union Integer = \x -> mrgIf (ssym "a") (mrgSingle $ x + 1) (mrgSingle $ x + 2)
>>> f .# (mrgIf (ssym "b" :: SymBool) (mrgSingle 0) (mrgSingle 2) :: Union Integer)
{If (&& b a) 1 (If b 2 (If a 3 4))}

onUnion :: forall u a r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a) => (a -> r) -> u a -> r Source #

Lift a function to work on union values.

>>> sumU = onUnion sum :: Union [SymInteger] -> SymInteger
>>> sumU (mrgIfPropagatedStrategy "cond" (return ["a"]) (return ["b","c"]) :: Union [SymInteger])
(ite cond a (+ b c))

onUnion2 :: forall u a b r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b) => (a -> b -> r) -> u a -> u b -> r Source #

Lift a function to work on union values.

onUnion3 :: forall u a b c r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b, Mergeable c) => (a -> b -> c -> r) -> u a -> u b -> u c -> r Source #

Lift a function to work on union values.

onUnion4 :: forall u a b c d r. (SimpleMergeable r, SymBranching u, UnionView u, Mergeable a, Mergeable b, Mergeable c, Mergeable d) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r Source #

Lift a function to work on union values.

unionToCon :: (ToCon a b, UnionView u) => u a -> Maybe b Source #

Convert a plain union to concrete values.

>>> unionToCon (return 1 :: Union SymInteger) :: Maybe Integer
Just 1
>>> unionToCon (mrgIf "a" (return 1) (return 2) :: Union SymInteger) :: Maybe Integer
Nothing
>>> unionToCon (return "a" :: Union SymInteger) :: Maybe Integer
Nothing

liftUnion :: (Mergeable a, UnionView u, Applicative m, SymBranching m) => u a -> m a Source #

Lift the UnionView value to any Applicative SymBranching.

liftToMonadUnion :: (Mergeable a, UnionView u, Monad m, SymBranching m) => u a -> m a Source #

Alias for liftUnion, but for monads.