{-# 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.UnionBase
(
UnionBase (..),
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.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.PPrint
( PPrint (pformatPrec),
PPrint1 (liftPFormatPrec),
condEnclose,
pformatPrec1,
)
import Grisette.Internal.Core.Data.Class.PlainUnion
( PlainUnion (ifView, singleView),
)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
SimpleMergeable1 (liftMrgIte),
SymBranching (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),
AllSyms1 (liftAllSymsS),
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 UnionBase a where
UnionSingle :: a -> UnionBase a
UnionIf ::
a ->
!Bool ->
!SymBool ->
UnionBase a ->
UnionBase a ->
UnionBase a
deriving ((forall x. UnionBase a -> Rep (UnionBase a) x)
-> (forall x. Rep (UnionBase a) x -> UnionBase a)
-> Generic (UnionBase a)
forall x. Rep (UnionBase a) x -> UnionBase a
forall x. UnionBase a -> Rep (UnionBase a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (UnionBase a) x -> UnionBase a
forall a x. UnionBase a -> Rep (UnionBase a) x
$cfrom :: forall a x. UnionBase a -> Rep (UnionBase a) x
from :: forall x. UnionBase a -> Rep (UnionBase a) x
$cto :: forall a x. Rep (UnionBase a) x -> UnionBase a
to :: forall x. Rep (UnionBase a) x -> UnionBase a
Generic, UnionBase a -> UnionBase a -> Bool
(UnionBase a -> UnionBase a -> Bool)
-> (UnionBase a -> UnionBase a -> Bool) -> Eq (UnionBase a)
forall a. Eq a => UnionBase a -> UnionBase a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => UnionBase a -> UnionBase a -> Bool
== :: UnionBase a -> UnionBase a -> Bool
$c/= :: forall a. Eq a => UnionBase a -> UnionBase a -> Bool
/= :: UnionBase a -> UnionBase a -> Bool
Eq, (forall (m :: * -> *). Quote m => UnionBase a -> m Exp)
-> (forall (m :: * -> *).
Quote m =>
UnionBase a -> Code m (UnionBase a))
-> Lift (UnionBase a)
forall a (m :: * -> *). (Lift a, Quote m) => UnionBase a -> m Exp
forall a (m :: * -> *).
(Lift a, Quote m) =>
UnionBase a -> Code m (UnionBase a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => UnionBase a -> m Exp
forall (m :: * -> *).
Quote m =>
UnionBase a -> Code m (UnionBase a)
$clift :: forall a (m :: * -> *). (Lift a, Quote m) => UnionBase a -> m Exp
lift :: forall (m :: * -> *). Quote m => UnionBase a -> m Exp
$cliftTyped :: forall a (m :: * -> *).
(Lift a, Quote m) =>
UnionBase a -> Code m (UnionBase a)
liftTyped :: forall (m :: * -> *).
Quote m =>
UnionBase a -> Code m (UnionBase a)
Lift, (forall a. UnionBase a -> Rep1 UnionBase a)
-> (forall a. Rep1 UnionBase a -> UnionBase a)
-> Generic1 UnionBase
forall a. Rep1 UnionBase a -> UnionBase a
forall a. UnionBase a -> Rep1 UnionBase 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. UnionBase a -> Rep1 UnionBase a
from1 :: forall a. UnionBase a -> Rep1 UnionBase a
$cto1 :: forall a. Rep1 UnionBase a -> UnionBase a
to1 :: forall a. Rep1 UnionBase a -> UnionBase a
Generic1)
deriving ((forall a b. (a -> b) -> UnionBase a -> UnionBase b)
-> (forall a b. a -> UnionBase b -> UnionBase a)
-> Functor UnionBase
forall a b. a -> UnionBase b -> UnionBase a
forall a b. (a -> b) -> UnionBase a -> UnionBase 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) -> UnionBase a -> UnionBase b
fmap :: forall a b. (a -> b) -> UnionBase a -> UnionBase b
$c<$ :: forall a b. a -> UnionBase b -> UnionBase a
<$ :: forall a b. a -> UnionBase b -> UnionBase a
Functor)
instance Applicative UnionBase where
pure :: forall a. a -> UnionBase a
pure = a -> UnionBase a
forall a. a -> UnionBase a
UnionSingle
{-# INLINE pure #-}
<*> :: forall a b. UnionBase (a -> b) -> UnionBase a -> UnionBase b
(<*>) = UnionBase (a -> b) -> UnionBase a -> UnionBase b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
{-# INLINE (<*>) #-}
instance Monad UnionBase where
return :: forall a. a -> UnionBase a
return = a -> UnionBase a
forall a. a -> UnionBase a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE return #-}
UnionSingle a
a >>= :: forall a b. UnionBase a -> (a -> UnionBase b) -> UnionBase b
>>= a -> UnionBase b
f = a -> UnionBase b
f a
a
UnionIf a
_ Bool
_ SymBool
c UnionBase a
t UnionBase a
f >>= a -> UnionBase b
f' = Bool -> SymBool -> UnionBase b -> UnionBase b -> UnionBase b
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
False SymBool
c (UnionBase a
t UnionBase a -> (a -> UnionBase b) -> UnionBase b
forall a b. UnionBase a -> (a -> UnionBase b) -> UnionBase b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionBase b
f') (UnionBase a
f UnionBase a -> (a -> UnionBase b) -> UnionBase b
forall a b. UnionBase a -> (a -> UnionBase b) -> UnionBase b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionBase b
f')
{-# INLINE (>>=) #-}
instance Eq1 UnionBase where
liftEq :: forall a b. (a -> b -> Bool) -> UnionBase a -> UnionBase 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 UnionBase a
t1 UnionBase a
f1) (UnionIf b
l2 Bool
i2 SymBool
c2 UnionBase b
t2 UnionBase 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) -> UnionBase a -> UnionBase b -> Bool
forall a b. (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e UnionBase a
t1 UnionBase b
t2 Bool -> Bool -> Bool
&& (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool
forall a b. (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e UnionBase a
f1 UnionBase b
f2
liftEq a -> b -> Bool
_ UnionBase a
_ UnionBase b
_ = Bool
False
instance (NFData a) => NFData (UnionBase a) where
rnf :: UnionBase a -> ()
rnf = UnionBase a -> ()
forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1
instance NFData1 UnionBase where
liftRnf :: forall a. (a -> ()) -> UnionBase a -> ()
liftRnf a -> ()
_a (UnionSingle a
a) = a -> ()
_a a
a
liftRnf a -> ()
_a (UnionIf a
a Bool
bo SymBool
b UnionBase a
l UnionBase 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 -> ()) -> UnionBase a -> ()
forall a. (a -> ()) -> UnionBase a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a UnionBase a
l () -> () -> ()
forall a b. a -> b -> b
`seq`
(a -> ()) -> UnionBase a -> ()
forall a. (a -> ()) -> UnionBase a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a UnionBase a
r
ifWithLeftMost :: Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost :: forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
_ (Con Bool
c) UnionBase a
t UnionBase a
f
| Bool
c = UnionBase a
t
| Bool
otherwise = UnionBase a
f
ifWithLeftMost Bool
inv SymBool
cond UnionBase a
t UnionBase a
f = a -> Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
a -> Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
UnionIf (UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
t) Bool
inv SymBool
cond UnionBase a
t UnionBase a
f
{-# INLINE ifWithLeftMost #-}
instance PlainUnion UnionBase where
singleView :: forall a. UnionBase a -> Maybe a
singleView (UnionSingle a
a) = a -> Maybe a
forall a. a -> Maybe a
Just a
a
singleView UnionBase a
_ = Maybe a
forall a. Maybe a
Nothing
{-# INLINE singleView #-}
ifView :: forall a. UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a)
ifView (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse) = (SymBool, UnionBase a, UnionBase a)
-> Maybe (SymBool, UnionBase a, UnionBase a)
forall a. a -> Maybe a
Just (SymBool
cond, UnionBase a
ifTrue, UnionBase a
ifFalse)
ifView UnionBase a
_ = Maybe (SymBool, UnionBase a, UnionBase a)
forall a. Maybe a
Nothing
{-# INLINE ifView #-}
leftMost :: UnionBase a -> a
leftMost :: forall a. UnionBase a -> a
leftMost (UnionSingle a
a) = a
a
leftMost (UnionIf a
a Bool
_ SymBool
_ UnionBase a
_ UnionBase a
_) = a
a
{-# INLINE leftMost #-}
instance (Mergeable a) => Mergeable (UnionBase a) where
rootStrategy :: MergingStrategy (UnionBase a)
rootStrategy = (SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a))
-> (SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE rootStrategy #-}
instance Mergeable1 UnionBase where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (UnionBase a)
liftRootStrategy MergingStrategy a
ms = (SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a))
-> (SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> MergingStrategy (UnionBase a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy MergingStrategy a
ms
{-# INLINE liftRootStrategy #-}
instance (Mergeable a) => SimpleMergeable (UnionBase a) where
mrgIte :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a
mrgIte = SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance SimpleMergeable1 UnionBase where
liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
liftMrgIte SymBool -> a -> a -> a
m = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall (u :: * -> *) a.
SymBranching 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 UnionBase where
tryMergeWithStrategy :: forall a. MergingStrategy a -> UnionBase a -> UnionBase a
tryMergeWithStrategy = MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct
{-# INLINE tryMergeWithStrategy #-}
instance SymBranching UnionBase where
mrgIfWithStrategy :: forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
mrgIfWithStrategy = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy
{-# INLINE mrgIfWithStrategy #-}
mrgIfPropagatedStrategy :: forall a. SymBool -> UnionBase a -> UnionBase a -> UnionBase a
mrgIfPropagatedStrategy = Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
False
{-# INLINE mrgIfPropagatedStrategy #-}
instance Show1 UnionBase where
liftShowsPrec :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase 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 UnionBase a
t UnionBase 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 -> UnionBase a -> ShowS
sp1 Int
11 UnionBase 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 -> UnionBase a -> ShowS
sp1 Int
11 UnionBase a
f
where
sp1 :: Int -> UnionBase a -> ShowS
sp1 = (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase 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 (UnionBase a) where
showsPrec :: Int -> UnionBase a -> ShowS
showsPrec = Int -> UnionBase a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
instance (PPrint a) => PPrint (UnionBase a) where
pformatPrec :: forall ann. Int -> UnionBase a -> Doc ann
pformatPrec = Int -> UnionBase a -> Doc ann
forall (f :: * -> *) a ann.
(PPrint1 f, PPrint a) =>
Int -> f a -> Doc ann
pformatPrec1
instance PPrint1 UnionBase where
liftPFormatPrec :: forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
_ Int
n (UnionSingle a
a) = Int -> a -> Doc ann
fa Int
n a
a
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
n (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
t UnionBase 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. PPrint a => Int -> a -> Doc ann
pformatPrec Int
11 SymBool
cond,
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall (f :: * -> *) a ann.
PPrint1 f =>
(Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
11 UnionBase a
t,
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall (f :: * -> *) a ann.
PPrint1 f =>
(Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
11 UnionBase a
f
]
instance (Hashable a) => Hashable (UnionBase a) where
Int
s hashWithSalt :: Int -> UnionBase 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 UnionBase a
l UnionBase 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 -> UnionBase a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` UnionBase a
l
Int -> UnionBase a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` UnionBase a
r
instance (AllSyms a) => AllSyms (UnionBase a) where
allSymsS :: UnionBase 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 UnionBase a
t UnionBase 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]
: (UnionBase a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS UnionBase a
t ([SomeSym] -> [SomeSym])
-> ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionBase a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS UnionBase a
f ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall a b. (a -> b) -> a -> b
$ [SomeSym]
l)
instance AllSyms1 UnionBase where
liftAllSymsS :: forall a.
(a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
liftAllSymsS a -> [SomeSym] -> [SomeSym]
fa (UnionSingle a
v) = a -> [SomeSym] -> [SomeSym]
fa a
v
liftAllSymsS a -> [SomeSym] -> [SomeSym]
fa (UnionIf a
_ Bool
_ SymBool
c UnionBase a
t UnionBase 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]
: ((a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall a.
(a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall (f :: * -> *) a.
AllSyms1 f =>
(a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
liftAllSymsS a -> [SomeSym] -> [SomeSym]
fa UnionBase a
t ([SomeSym] -> [SomeSym])
-> ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall a.
(a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall (f :: * -> *) a.
AllSyms1 f =>
(a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
liftAllSymsS a -> [SomeSym] -> [SomeSym]
fa UnionBase a
f ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall a b. (a -> b) -> a -> b
$ [SomeSym]
l)
fullReconstruct :: MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct :: forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct MergingStrategy a
strategy (UnionIf a
_ Bool
False SymBool
cond UnionBase a
t UnionBase a
f) =
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv
MergingStrategy a
strategy
SymBool
cond
(MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct MergingStrategy a
strategy UnionBase a
t)
(MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct MergingStrategy a
strategy UnionBase a
f)
fullReconstruct MergingStrategy a
_ UnionBase a
u = UnionBase a
u
{-# INLINE fullReconstruct #-}
ifWithStrategy ::
MergingStrategy a ->
SymBool ->
UnionBase a ->
UnionBase a ->
UnionBase a
ifWithStrategy :: forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy MergingStrategy a
strategy SymBool
cond t :: UnionBase a
t@(UnionIf a
_ Bool
False SymBool
_ UnionBase a
_ UnionBase a
_) UnionBase a
f =
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy MergingStrategy a
strategy SymBool
cond (MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct MergingStrategy a
strategy UnionBase a
t) UnionBase a
f
ifWithStrategy MergingStrategy a
strategy SymBool
cond UnionBase a
t f :: UnionBase a
f@(UnionIf a
_ Bool
False SymBool
_ UnionBase a
_ UnionBase a
_) =
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy MergingStrategy a
strategy SymBool
cond UnionBase a
t (MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
fullReconstruct MergingStrategy a
strategy UnionBase a
f)
ifWithStrategy MergingStrategy a
strategy SymBool
cond UnionBase a
t UnionBase a
f = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond UnionBase a
t UnionBase a
f
{-# INLINE ifWithStrategy #-}
ifWithStrategyInv ::
MergingStrategy a ->
SymBool ->
UnionBase a ->
UnionBase a ->
UnionBase a
ifWithStrategyInv :: forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
_ (Con Bool
v) UnionBase a
t UnionBase a
f
| Bool
v = UnionBase a
t
| Bool
otherwise = UnionBase a
f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond (UnionIf a
_ Bool
True SymBool
condTrue UnionBase a
tt UnionBase a
_) UnionBase a
f
| SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condTrue = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond UnionBase a
tt UnionBase a
f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond UnionBase a
t (UnionIf a
_ Bool
True SymBool
condFalse UnionBase a
_ UnionBase a
ff)
| SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condFalse = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond UnionBase a
t UnionBase a
ff
ifWithStrategyInv (SimpleStrategy SymBool -> a -> a -> a
m) SymBool
cond (UnionSingle a
l) (UnionSingle a
r) =
a -> UnionBase a
forall a. a -> UnionBase a
UnionSingle (a -> UnionBase a) -> a -> UnionBase 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
UnionBase a
ifTrue
UnionBase a
ifFalse = case (UnionBase a
ifTrue, UnionBase a
ifFalse) of
(UnionSingle a
_, UnionSingle a
_) -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ssUnionIf SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse
(UnionSingle a
_, UnionIf {}) -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
sgUnionIf SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse
(UnionIf {}, UnionSingle a
_) -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
gsUnionIf SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse
(UnionBase a, UnionBase a)
_ -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ggUnionIf SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse
where
ssUnionIf :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ssUnionIf SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf = Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf =
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| Bool
otherwise = Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') UnionBase a
ifFalse' UnionBase a
ifTrue'
where
idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ifTrue'
idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ifFalse'
{-# INLINE ssUnionIf #-}
sgUnionIf :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a
sgUnionIf SymBool
cond' UnionBase a
ifTrue' ifFalse' :: UnionBase a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf UnionBase a
ft UnionBase a
ff)
| idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ssUnionIf SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft = Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxft =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost
Bool
True
(SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool
condf)
(MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' UnionBase a
ifTrue' UnionBase a
ft)
UnionBase a
ff
| Bool
otherwise =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase 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)
UnionBase a
ft
(MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' UnionBase a
ifTrue' UnionBase a
ff)
where
idxft :: idx
idxft = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ft
idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ff
idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ifTrue'
sgUnionIf SymBool
_ UnionBase a
_ UnionBase a
_ = UnionBase a
forall a. HasCallStack => a
undefined
{-# INLINE sgUnionIf #-}
gsUnionIf :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a
gsUnionIf SymBool
cond' ifTrue' :: UnionBase a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt UnionBase a
tt UnionBase a
tf) UnionBase a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ssUnionIf SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) UnionBase a
tt (UnionBase a -> UnionBase a) -> UnionBase a -> UnionBase a
forall a b. (a -> b) -> a -> b
$
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' UnionBase a
tf UnionBase a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase 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 -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxf) SymBool
cond' UnionBase a
tt UnionBase a
ifFalse')
UnionBase a
tf
| Bool
otherwise = Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') UnionBase a
ifFalse' UnionBase a
ifTrue'
where
idxtt :: idx
idxtt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
tt
idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
tf
idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ifFalse'
gsUnionIf SymBool
_ UnionBase a
_ UnionBase a
_ = UnionBase a
forall a. HasCallStack => a
undefined
{-# INLINE gsUnionIf #-}
ggUnionIf :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ggUnionIf
SymBool
cond'
ifTrue' :: UnionBase a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt UnionBase a
tt UnionBase a
tf)
ifFalse' :: UnionBase a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf UnionBase a
ft UnionBase a
ff)
| idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> UnionBase a -> UnionBase a -> UnionBase a
sgUnionIf SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> UnionBase a -> UnionBase a -> UnionBase a
gsUnionIf SymBool
cond' UnionBase a
ifTrue' UnionBase a
ifFalse'
| idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) UnionBase a
tt (UnionBase a -> UnionBase a) -> UnionBase a -> UnionBase a
forall a b. (a -> b) -> a -> b
$
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' UnionBase a
tf UnionBase 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 :: UnionBase a
newUnionIfTrue =
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxtt) SymBool
cond' UnionBase a
tt UnionBase a
ft
newUnionIfFalse :: UnionBase a
newUnionIfFalse = MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' UnionBase a
tf UnionBase a
ff
in Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True SymBool
newCond UnionBase a
newUnionIfTrue UnionBase a
newUnionIfFalse
| Bool
otherwise =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase 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) UnionBase a
ft (UnionBase a -> UnionBase a) -> UnionBase a -> UnionBase a
forall a b. (a -> b) -> a -> b
$
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
MergingStrategy a
-> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' UnionBase a
ifTrue' UnionBase a
ff
where
idxtt :: idx
idxtt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
tt
idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
tf
idxft :: idx
idxft = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ft
idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ UnionBase a -> a
forall a. UnionBase a -> a
leftMost UnionBase a
ff
ggUnionIf SymBool
_ UnionBase a
_ UnionBase a
_ = UnionBase a
forall a. HasCallStack => a
undefined
{-# INLINE ggUnionIf #-}
ifWithStrategyInv MergingStrategy a
NoStrategy SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse =
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
True SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse
ifWithStrategyInv MergingStrategy a
_ SymBool
_ UnionBase a
_ UnionBase a
_ = String -> UnionBase a
forall a. HasCallStack => String -> a
error String
"Invariant violated"
{-# INLINE ifWithStrategyInv #-}