{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.Internal.Core.Data.Union
(
Union (..),
ifWithLeftMost,
ifWithStrategy,
fullReconstruct,
)
where
import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)
import Control.Monad (ap)
import Data.Functor.Classes
( Eq1 (liftEq),
Show1 (liftShowsPrec),
showsPrec1,
showsUnaryWith,
)
import Data.Hashable (Hashable (hashWithSalt))
import GHC.Generics (Generic, Generic1)
import Grisette.Internal.Core.Data.Class.GPretty
( GPretty (gprettyPrec),
condEnclose,
)
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 (rootStrategy),
Mergeable1 (liftRootStrategy),
MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
)
import Grisette.Internal.Core.Data.Class.PlainUnion
( PlainUnion (ifView, singleView),
)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
SimpleMergeable1 (liftMrgIte),
UnionMergeable1 (mrgIfPropagatedStrategy, mrgIfWithStrategy),
mrgIf,
)
import Grisette.Internal.Core.Data.Class.Solvable (pattern Con)
import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge (tryMergeWithStrategy))
import Grisette.Internal.SymPrim.AllSyms
( AllSyms (allSymsS),
SomeSym (SomeSym),
)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Language.Haskell.TH.Syntax (Lift)
#if MIN_VERSION_prettyprinter(1,7,0)
import Prettyprinter (align, group, nest, vsep)
#else
import Data.Text.Prettyprint.Doc (align, group, nest, vsep)
#endif
data Union a where
UnionSingle :: a -> Union a
UnionIf ::
a ->
!Bool ->
!SymBool ->
Union a ->
Union a ->
Union a
deriving ((forall x. Union a -> Rep (Union a) x)
-> (forall x. Rep (Union a) x -> Union a) -> Generic (Union a)
forall x. Rep (Union a) x -> Union a
forall x. Union a -> Rep (Union a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Union a) x -> Union a
forall a x. Union a -> Rep (Union a) x
$cfrom :: forall a x. Union a -> Rep (Union a) x
from :: forall x. Union a -> Rep (Union a) x
$cto :: forall a x. Rep (Union a) x -> Union a
to :: forall x. Rep (Union a) x -> Union a
Generic, Union a -> Union a -> Bool
(Union a -> Union a -> Bool)
-> (Union a -> Union a -> Bool) -> Eq (Union a)
forall a. Eq a => Union a -> Union a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Union a -> Union a -> Bool
== :: Union a -> Union a -> Bool
$c/= :: forall a. Eq a => Union a -> Union a -> Bool
/= :: Union a -> Union a -> Bool
Eq, (forall (m :: * -> *). Quote m => Union a -> m Exp)
-> (forall (m :: * -> *). Quote m => Union a -> Code m (Union a))
-> Lift (Union a)
forall a (m :: * -> *). (Lift a, Quote m) => Union a -> m Exp
forall a (m :: * -> *).
(Lift a, Quote m) =>
Union a -> Code m (Union a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Union a -> m Exp
forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
$clift :: forall a (m :: * -> *). (Lift a, Quote m) => Union a -> m Exp
lift :: forall (m :: * -> *). Quote m => Union a -> m Exp
$cliftTyped :: forall a (m :: * -> *).
(Lift a, Quote m) =>
Union a -> Code m (Union a)
liftTyped :: forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
Lift, (forall a. Union a -> Rep1 Union a)
-> (forall a. Rep1 Union a -> Union a) -> Generic1 Union
forall a. Rep1 Union a -> Union a
forall a. Union a -> Rep1 Union a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a. Union a -> Rep1 Union a
from1 :: forall a. Union a -> Rep1 Union a
$cto1 :: forall a. Rep1 Union a -> Union a
to1 :: forall a. Rep1 Union a -> Union a
Generic1)
deriving ((forall a b. (a -> b) -> Union a -> Union b)
-> (forall a b. a -> Union b -> Union a) -> Functor Union
forall a b. a -> Union b -> Union a
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Union a -> Union b
fmap :: forall a b. (a -> b) -> Union a -> Union b
$c<$ :: forall a b. a -> Union b -> Union a
<$ :: forall a b. a -> Union b -> Union a
Functor)
instance Applicative Union where
pure :: forall a. a -> Union a
pure = a -> Union a
forall a. a -> Union a
UnionSingle
{-# INLINE pure #-}
<*> :: forall a b. Union (a -> b) -> Union a -> Union b
(<*>) = Union (a -> b) -> Union a -> Union b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
{-# INLINE (<*>) #-}
instance Monad Union where
return :: forall a. a -> Union a
return = a -> Union a
forall a. a -> Union a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE return #-}
UnionSingle a
a >>= :: forall a b. Union a -> (a -> Union b) -> Union b
>>= a -> Union b
f = a -> Union b
f a
a
UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f >>= a -> Union b
f' = Bool -> SymBool -> Union b -> Union b -> Union b
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
False SymBool
c (Union a
t Union a -> (a -> Union b) -> Union b
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Union b
f') (Union a
f Union a -> (a -> Union b) -> Union b
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Union b
f')
{-# INLINE (>>=) #-}
instance Eq1 Union where
liftEq :: forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
liftEq a -> b -> Bool
e (UnionSingle a
a) (UnionSingle b
b) = a -> b -> Bool
e a
a b
b
liftEq a -> b -> Bool
e (UnionIf a
l1 Bool
i1 SymBool
c1 Union a
t1 Union a
f1) (UnionIf b
l2 Bool
i2 SymBool
c2 Union b
t2 Union b
f2) =
a -> b -> Bool
e a
l1 b
l2 Bool -> Bool -> Bool
&& Bool
i1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
i2 Bool -> Bool -> Bool
&& SymBool
c1 SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
c2 Bool -> Bool -> Bool
&& (a -> b -> Bool) -> Union a -> Union b -> Bool
forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e Union a
t1 Union b
t2 Bool -> Bool -> Bool
&& (a -> b -> Bool) -> Union a -> Union b -> Bool
forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e Union a
f1 Union b
f2
liftEq a -> b -> Bool
_ Union a
_ Union b
_ = Bool
False
instance (NFData a) => NFData (Union a) where
rnf :: Union a -> ()
rnf = Union a -> ()
forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1
instance NFData1 Union where
liftRnf :: forall a. (a -> ()) -> Union a -> ()
liftRnf a -> ()
_a (UnionSingle a
a) = a -> ()
_a a
a
liftRnf a -> ()
_a (UnionIf a
a Bool
bo SymBool
b Union a
l Union a
r) =
a -> ()
_a a
a () -> () -> ()
forall a b. a -> b -> b
`seq`
Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
bo () -> () -> ()
forall a b. a -> b -> b
`seq`
SymBool -> ()
forall a. NFData a => a -> ()
rnf SymBool
b () -> () -> ()
forall a b. a -> b -> b
`seq`
(a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
l () -> () -> ()
forall a b. a -> b -> b
`seq`
(a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
r
ifWithLeftMost :: Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost :: forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
_ (Con Bool
c) Union a
t Union a
f
| Bool
c = Union a
t
| Bool
otherwise = Union a
f
ifWithLeftMost Bool
inv SymBool
cond Union a
t Union a
f = a -> Bool -> SymBool -> Union a -> Union a -> Union a
forall a. a -> Bool -> SymBool -> Union a -> Union a -> Union a
UnionIf (Union a -> a
forall a. Union a -> a
leftMost Union a
t) Bool
inv SymBool
cond Union a
t Union a
f
{-# INLINE ifWithLeftMost #-}
instance PlainUnion Union where
singleView :: forall a. Union a -> Maybe a
singleView (UnionSingle a
a) = a -> Maybe a
forall a. a -> Maybe a
Just a
a
singleView Union a
_ = Maybe a
forall a. Maybe a
Nothing
{-# INLINE singleView #-}
ifView :: forall a. Union a -> Maybe (SymBool, Union a, Union a)
ifView (UnionIf a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) = (SymBool, Union a, Union a) -> Maybe (SymBool, Union a, Union a)
forall a. a -> Maybe a
Just (SymBool
cond, Union a
ifTrue, Union a
ifFalse)
ifView Union a
_ = Maybe (SymBool, Union a, Union a)
forall a. Maybe a
Nothing
{-# INLINE ifView #-}
leftMost :: Union a -> a
leftMost :: forall a. Union a -> a
leftMost (UnionSingle a
a) = a
a
leftMost (UnionIf a
a Bool
_ SymBool
_ Union a
_ Union a
_) = a
a
{-# INLINE leftMost #-}
instance (Mergeable a) => Mergeable (Union a) where
rootStrategy :: MergingStrategy (Union a)
rootStrategy = (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a))
-> (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE rootStrategy #-}
instance Mergeable1 Union where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (Union a)
liftRootStrategy MergingStrategy a
ms = (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a))
-> (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
ms
{-# INLINE liftRootStrategy #-}
instance (Mergeable a) => SimpleMergeable (Union a) where
mrgIte :: SymBool -> Union a -> Union a -> Union a
mrgIte = SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance SimpleMergeable1 Union where
liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> Union a -> Union a -> Union a
liftMrgIte SymBool -> a -> a -> a
m = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
UnionMergeable1 u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
instance TryMerge Union where
tryMergeWithStrategy :: forall a. MergingStrategy a -> Union a -> Union a
tryMergeWithStrategy = MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct
{-# INLINE tryMergeWithStrategy #-}
instance UnionMergeable1 Union where
mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
mrgIfWithStrategy = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy
{-# INLINE mrgIfWithStrategy #-}
mrgIfPropagatedStrategy :: forall a. SymBool -> Union a -> Union a -> Union a
mrgIfPropagatedStrategy = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
False
{-# INLINE mrgIfPropagatedStrategy #-}
instance Show1 Union where
liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ Int
i (UnionSingle a
a) = (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> a -> ShowS
sp String
"Single" Int
i a
a
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
Bool -> ShowS -> ShowS
showParen (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"If"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SymBool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
f
where
sp1 :: Int -> Union a -> ShowS
sp1 = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl
instance (Show a) => Show (Union a) where
showsPrec :: Int -> Union a -> ShowS
showsPrec = Int -> Union a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
instance (GPretty a) => GPretty (Union a) where
gprettyPrec :: forall ann. Int -> Union a -> Doc ann
gprettyPrec Int
n (UnionSingle a
a) = Int -> a -> Doc ann
forall ann. Int -> a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
n a
a
gprettyPrec Int
n (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
group (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
condEnclose (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) Doc ann
"(" Doc ann
")" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
[ Doc ann
"If",
Int -> SymBool -> Doc ann
forall ann. Int -> SymBool -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 SymBool
cond,
Int -> Union a -> Doc ann
forall ann. Int -> Union a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 Union a
t,
Int -> Union a -> Doc ann
forall ann. Int -> Union a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 Union a
f
]
instance (Hashable a) => Hashable (Union a) where
Int
s hashWithSalt :: Int -> Union a -> Int
`hashWithSalt` (UnionSingle a
a) =
Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
a
Int
s `hashWithSalt` (UnionIf a
_ Bool
_ SymBool
c Union a
l Union a
r) =
Int
s
Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int)
Int -> SymBool -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` SymBool
c
Int -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
l
Int -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
r
instance (AllSyms a) => AllSyms (Union a) where
allSymsS :: Union a -> [SomeSym] -> [SomeSym]
allSymsS (UnionSingle a
v) = a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
v
allSymsS (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = \[SomeSym]
l -> SymBool -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymBool
c SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
: (Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
t ([SomeSym] -> [SomeSym])
-> ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
f ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall a b. (a -> b) -> a -> b
$ [SomeSym]
l)
fullReconstruct :: MergingStrategy a -> Union a -> Union a
fullReconstruct :: forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy (UnionIf a
_ Bool
False SymBool
cond Union a
t Union a
f) =
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv
MergingStrategy a
strategy
SymBool
cond
(MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
t)
(MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
f)
fullReconstruct MergingStrategy a
_ Union a
u = Union a
u
{-# INLINE fullReconstruct #-}
ifWithStrategy ::
MergingStrategy a ->
SymBool ->
Union a ->
Union a ->
Union a
ifWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond t :: Union a
t@(UnionIf a
_ Bool
False SymBool
_ Union a
_ Union a
_) Union a
f =
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond (MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
t) Union a
f
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t f :: Union a
f@(UnionIf a
_ Bool
False SymBool
_ Union a
_ Union a
_) =
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t (MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
f)
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t Union a
f = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t Union a
f
{-# INLINE ifWithStrategy #-}
ifWithStrategyInv ::
MergingStrategy a ->
SymBool ->
Union a ->
Union a ->
Union a
ifWithStrategyInv :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
_ (Con Bool
v) Union a
t Union a
f
| Bool
v = Union a
t
| Bool
otherwise = Union a
f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond (UnionIf a
_ Bool
True SymBool
condTrue Union a
tt Union a
_) Union a
f
| SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condTrue = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
tt Union a
f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t (UnionIf a
_ Bool
True SymBool
condFalse Union a
_ Union a
ff)
| SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condFalse = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t Union a
ff
ifWithStrategyInv (SimpleStrategy SymBool -> a -> a -> a
m) SymBool
cond (UnionSingle a
l) (UnionSingle a
r) = a -> Union a
forall a. a -> Union a
UnionSingle (a -> Union a) -> a -> Union a
forall a b. (a -> b) -> a -> b
$ SymBool -> a -> a -> a
m SymBool
cond a
l a
r
ifWithStrategyInv strategy :: MergingStrategy a
strategy@(SortedStrategy a -> idx
idxFun idx -> MergingStrategy a
substrategy) SymBool
cond Union a
ifTrue Union a
ifFalse = case (Union a
ifTrue, Union a
ifFalse) of
(UnionSingle a
_, UnionSingle a
_) -> SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
(UnionSingle a
_, UnionIf {}) -> SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
(UnionIf {}, UnionSingle a
_) -> SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
(Union a, Union a)
_ -> SymBool -> Union a -> Union a -> Union a
ggUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
where
ssUnionIf :: SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| Bool
otherwise = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') Union a
ifFalse' Union a
ifTrue'
where
idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifTrue'
idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifFalse'
{-# INLINE ssUnionIf #-}
sgUnionIf :: SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond' Union a
ifTrue' ifFalse' :: Union a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
| idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool
condf) (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' Union a
ifTrue' Union a
ft) Union a
ff
| Bool
otherwise = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condf) Union a
ft (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
ifTrue' Union a
ff)
where
idxft :: idx
idxft = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ft
idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ff
idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifTrue'
sgUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
{-# INLINE sgUnionIf #-}
gsUnionIf :: SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt Union a
tt Union a
tf) Union a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) Union a
tt (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool
condt) (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxf) SymBool
cond' Union a
tt Union a
ifFalse') Union a
tf
| Bool
otherwise = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') Union a
ifFalse' Union a
ifTrue'
where
idxtt :: idx
idxtt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tt
idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tf
idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifFalse'
gsUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
{-# INLINE gsUnionIf #-}
ggUnionIf :: SymBool -> Union a -> Union a -> Union a
ggUnionIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt Union a
tt Union a
tf) ifFalse' :: Union a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) Union a
tt (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxft =
let newCond :: SymBool
newCond = SymBool -> SymBool -> SymBool -> SymBool
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
cond' SymBool
condt SymBool
condf
newUnionIfTrue :: Union a
newUnionIfTrue = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxtt) SymBool
cond' Union a
tt Union a
ft
newUnionIfFalse :: Union a
newUnionIfFalse = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ff
in Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
newCond Union a
newUnionIfTrue Union a
newUnionIfFalse
| Bool
otherwise = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condf) Union a
ft (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
ifTrue' Union a
ff
where
idxtt :: idx
idxtt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tt
idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tf
idxft :: idx
idxft = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ft
idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ff
ggUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
{-# INLINE ggUnionIf #-}
ifWithStrategyInv MergingStrategy a
NoStrategy SymBool
cond Union a
ifTrue Union a
ifFalse = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond Union a
ifTrue Union a
ifFalse
ifWithStrategyInv MergingStrategy a
_ SymBool
_ Union a
_ Union a
_ = String -> Union a
forall a. HasCallStack => String -> a
error String
"Invariant violated"
{-# INLINE ifWithStrategyInv #-}