{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Grisette.Internal.Core.Data.Class.PlainUnion
( PlainUnion (..),
pattern Single,
pattern If,
simpleMerge,
symIteMerge,
(.#),
onUnion,
onUnion2,
onUnion3,
onUnion4,
)
where
import Data.Bifunctor (Bifunctor (first))
import Data.Kind (Type)
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.LogicalOp
( LogicalOp (symNot, (.&&)),
)
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
( SimpleMergeable,
UnionMergeable1,
mrgIf,
)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.TryMerge
( mrgSingle,
tryMerge,
)
import Grisette.Internal.SymPrim.SymBool (SymBool)
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)]
toGuardedList u a
u =
case (u a -> Maybe a
forall a. u a -> Maybe a
forall (u :: * -> *) a. PlainUnion u => u a -> Maybe a
singleView u a
u, u a -> Maybe (SymBool, u a, u a)
forall a. u a -> Maybe (SymBool, u a, u a)
forall (u :: * -> *) a.
PlainUnion u =>
u a -> Maybe (SymBool, u a, u a)
ifView u a
u) of
(Just a
x, Maybe (SymBool, u a, u a)
_) -> [(Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True, a
x)]
(Maybe a
_, Just (SymBool
c, u a
l, u a
r)) ->
((SymBool, a) -> (SymBool, a)) -> [(SymBool, a)] -> [(SymBool, a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SymBool -> SymBool) -> (SymBool, a) -> (SymBool, a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
c)) (u a -> [(SymBool, a)]
forall a. u a -> [(SymBool, a)]
forall (u :: * -> *) a. PlainUnion u => u a -> [(SymBool, a)]
toGuardedList u a
l)
[(SymBool, a)] -> [(SymBool, a)] -> [(SymBool, a)]
forall a. [a] -> [a] -> [a]
++ ((SymBool, a) -> (SymBool, a)) -> [(SymBool, a)] -> [(SymBool, a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SymBool -> SymBool) -> (SymBool, a) -> (SymBool, a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
c)) (u a -> [(SymBool, a)]
forall a. u a -> [(SymBool, a)]
forall (u :: * -> *) a. PlainUnion u => u a -> [(SymBool, a)]
toGuardedList u a
r)
(Maybe a, Maybe (SymBool, u a, u a))
_ -> [Char] -> [(SymBool, a)]
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
overestimateUnionValues :: (Mergeable a) => u a -> [a]
overestimateUnionValues (Single a
v) = [a
v]
overestimateUnionValues (If SymBool
_ u a
l u a
r) =
u a -> [a]
forall a. Mergeable a => u a -> [a]
forall (u :: * -> *) a. (PlainUnion u, Mergeable a) => u a -> [a]
overestimateUnionValues u a
l [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ u a -> [a]
forall a. Mergeable a => u a -> [a]
forall (u :: * -> *) a. (PlainUnion u, Mergeable a) => u a -> [a]
overestimateUnionValues u a
r
pattern Single :: (PlainUnion u, Mergeable a) => a -> u a
pattern $mSingle :: forall {r} {u :: * -> *} {a}.
(PlainUnion u, Mergeable a) =>
u a -> (a -> r) -> ((# #) -> r) -> r
$bSingle :: forall (u :: * -> *) a. (PlainUnion u, Mergeable a) => a -> u a
Single x <-
(singleView -> Just x)
where
Single a
x = a -> u a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
x
pattern If :: (PlainUnion u, Mergeable a) => SymBool -> u a -> u a -> u a
pattern $mIf :: forall {r} {u :: * -> *} {a}.
(PlainUnion u, Mergeable a) =>
u a -> (SymBool -> u a -> u a -> r) -> ((# #) -> r) -> r
$bIf :: forall (u :: * -> *) a.
(PlainUnion u, Mergeable a) =>
SymBool -> u a -> u a -> u a
If c t f <-
(ifView -> Just (c, t, f))
where
If SymBool
c u a
t u a
f = SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c u a
t u a
f
#if MIN_VERSION_base(4, 16, 4)
{-# COMPLETE Single, If #-}
#endif
simpleMerge :: forall u a. (SimpleMergeable a, PlainUnion u) => u a -> a
simpleMerge :: forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge u a
u = case u a -> u a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u a
u of
Single a
x -> a
x
u a
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
{-# INLINE simpleMerge #-}
symIteMerge :: (ITEOp a, Mergeable a, PlainUnion u) => u a -> a
symIteMerge :: forall a (u :: * -> *).
(ITEOp a, Mergeable a, PlainUnion u) =>
u a -> a
symIteMerge (Single a
x) = a
x
symIteMerge (If SymBool
cond u a
l u a
r) = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
cond (u a -> a
forall a (u :: * -> *).
(ITEOp a, Mergeable a, PlainUnion u) =>
u a -> a
symIteMerge u a
l) (u a -> a
forall a (u :: * -> *).
(ITEOp a, Mergeable a, PlainUnion u) =>
u a -> a
symIteMerge u a
r)
{-# INLINE symIteMerge #-}
(.#) ::
(Function f a r, SimpleMergeable r, PlainUnion u) =>
f ->
u a ->
r
.# :: forall f a r (u :: * -> *).
(Function f a r, SimpleMergeable r, PlainUnion u) =>
f -> u a -> r
(.#) f
f u a
u = u r -> r
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u r -> r) -> u r -> r
forall a b. (a -> b) -> a -> b
$ (a -> r) -> u a -> u r
forall a b. (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f
f f -> a -> r
forall f arg ret. Function f arg ret => f -> arg -> ret
#) u a
u
{-# INLINE (.#) #-}
infixl 9 .#
onUnion ::
forall u a r.
(SimpleMergeable r, UnionMergeable1 u, PlainUnion u, Mergeable a) =>
(a -> r) ->
(u a -> r)
onUnion :: forall (u :: * -> *) a r.
(SimpleMergeable r, UnionMergeable1 u, PlainUnion u,
Mergeable a) =>
(a -> r) -> u a -> r
onUnion a -> r
f = u r -> r
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u r -> r) -> (u a -> u r) -> u a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> r) -> u a -> u r
forall a b. (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> r
f (u a -> u r) -> (u a -> u a) -> u a -> u r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u a -> u a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge
onUnion2 ::
forall u a b r.
( SimpleMergeable r,
UnionMergeable1 u,
PlainUnion u,
Mergeable a,
Mergeable b
) =>
(a -> b -> r) ->
(u a -> u b -> 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
onUnion2 a -> b -> r
f u a
ua u b
ub = u r -> r
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u r -> r) -> u r -> r
forall a b. (a -> b) -> a -> b
$ a -> b -> r
f (a -> b -> r) -> u a -> u (b -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u a -> u a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u a
ua u (b -> r) -> u b -> u r
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u b -> u b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u b
ub
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)
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
onUnion3 a -> b -> c -> r
f u a
ua u b
ub u c
uc =
u r -> r
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u r -> r) -> u r -> r
forall a b. (a -> b) -> a -> b
$ a -> b -> c -> r
f (a -> b -> c -> r) -> u a -> u (b -> c -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u a -> u a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u a
ua u (b -> c -> r) -> u b -> u (c -> r)
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u b -> u b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u b
ub u (c -> r) -> u c -> u r
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u c -> u c
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u c
uc
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)
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
onUnion4 a -> b -> c -> d -> r
f u a
ua u b
ub u c
uc u d
ud =
u r -> r
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (u r -> r) -> u r -> r
forall a b. (a -> b) -> a -> b
$
a -> b -> c -> d -> r
f (a -> b -> c -> d -> r) -> u a -> u (b -> c -> d -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u a -> u a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u a
ua u (b -> c -> d -> r) -> u b -> u (c -> d -> r)
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u b -> u b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u b
ub u (c -> d -> r) -> u c -> u (d -> r)
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u c -> u c
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u c
uc u (d -> r) -> u d -> u r
forall a b. u (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u d -> u d
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge u d
ud