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	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.Class.PlainUnion

Description

Synopsis

class (Applicative u, UnionMergeable1 u) => PlainUnion (u :: Type -> Type) where
- singleView :: u a -> Maybe a
- ifView :: u a -> Maybe (SymBool, u a, u a)
- toGuardedList :: u a -> [(SymBool, a)]
pattern Single :: (PlainUnion u, Mergeable a) => a -> u a
pattern If :: (PlainUnion u, Mergeable a) => SymBool -> u a -> u a -> u a
simpleMerge :: forall u a. (SimpleMergeable a, PlainUnion u) => u a -> a
symIteMerge :: (ITEOp a, Mergeable a, PlainUnion u) => u a -> a
(.#) :: (Function f a r, SimpleMergeable r, PlainUnion u) => f -> u a -> r
onUnion :: forall u a r. (SimpleMergeable r, UnionMergeable1 u, PlainUnion u, Mergeable a) => (a -> r) -> u a -> r
onUnion2 :: forall u a b r. (SimpleMergeable r, UnionMergeable1 u, PlainUnion u, Mergeable a, Mergeable b) => (a -> b -> r) -> u a -> u b -> r
onUnion3 :: forall u a b c r. (SimpleMergeable r, UnionMergeable1 u, PlainUnion 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, UnionMergeable1 u, PlainUnion u, Mergeable a, Mergeable b, Mergeable c, Mergeable d) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r

Documentation

class (Applicative u, UnionMergeable1 u) => PlainUnion (u :: Type -> Type) where Source #

Plain union containers that can be projected back into single value or if-guarded values.

Minimal complete definition

singleView, ifView

Methods

singleView :: u a -> Maybe a Source #

Pattern match to extract single values.

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

ifView :: u a -> Maybe (SymBool, u a, u a) Source #

Pattern match to extract if values.

>>> ifView (return 1 :: UnionM Integer)
Nothing
>>> ifView (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: UnionM Integer)
Just (a,<1>,<2>)
>>> ifView (mrgIf "a" (return 1) (return 2) :: UnionM Integer)
Just (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)) :: UnionM Integer)
[(a,1),((&& b (! a)),2),((! (|| b a)),3)]

Instances

Instances details

PlainUnion UnionM Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods singleView :: UnionM a -> Maybe a Source # ifView :: UnionM a -> Maybe (SymBool, UnionM a, UnionM a) Source # toGuardedList :: UnionM a -> [(SymBool, a)] Source #
PlainUnion Union Source #
Instance details Defined in Grisette.Internal.Core.Data.Union Methods singleView :: Union a -> Maybe a Source # ifView :: Union a -> Maybe (SymBool, Union a, Union a) Source # toGuardedList :: Union a -> [(SymBool, a)] Source #

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

Pattern match to extract single values with singleView.

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

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

Pattern match to extract guard values with ifView >>> case (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: UnionM Integer) of If c t f -> (c,t,f) (a,1,2)

simpleMerge :: forall u a. (SimpleMergeable a, PlainUnion 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") :: UnionM SymBool
<If a b c>
>>> simpleMerge $ (mrgIfPropagatedStrategy (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool)
(ite a b c)

symIteMerge :: (ITEOp a, Mergeable a, PlainUnion 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, PlainUnion u) => f -> u a -> r infixl 9 Source #

Helper for applying functions on UnionLike 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))}

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

Lift a function to work on union values.

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

onUnion2 :: forall u a b r. (SimpleMergeable r, UnionMergeable1 u, PlainUnion 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, UnionMergeable1 u, PlainUnion 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, UnionMergeable1 u, PlainUnion 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.