{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.UnionBase
  ( -- * The union data structure.

    -- | Please consider using 'Grisette.Core.Union' instead.
    UnionBase (..),
    ifWithLeftMost,
    ifWithStrategy,
    fullReconstruct,
  )
where

#if MIN_VERSION_prettyprinter(1,7,0)
import Prettyprinter (align, group, nest, vsep)
#else
import Data.Text.Prettyprint.Doc (align, group, nest, vsep)
#endif

import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)
import Control.Monad (ap)
import qualified Data.Binary as Binary
import Data.Bytes.Get (MonadGet (getWord8))
import Data.Bytes.Put (MonadPut (putWord8))
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Functor.Classes
  ( Eq1 (liftEq),
    Show1 (liftShowsPrec),
    showsPrec1,
    showsUnaryWith,
  )
import Data.Hashable (Hashable (hashWithSalt))
import qualified Data.Serialize as Cereal
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)

-- | The base union implementation, which is an if-then-else tree structure.
data UnionBase a where
  -- | A single value
  UnionSingle :: a -> UnionBase a
  -- | A if value
  UnionIf ::
    -- | Cached leftmost value
    a ->
    -- | Is merged invariant already maintained?
    !Bool ->
    -- | If condition
    !SymBool ->
    -- | True branch
    UnionBase a ->
    -- | False branch
    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

-- | Build 'UnionIf' with leftmost cache correctly maintained.
--
-- Usually you should never directly try to build a 'UnionIf' with its
-- constructor.
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 (Mergeable a, Serial a) => Serial (UnionBase a) where
  serialize :: forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize (UnionSingle a
a) = Word8 -> m ()
forall (m :: * -> *). MonadPut m => Word8 -> m ()
putWord8 Word8
0 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => a -> m ()
serialize a
a
  serialize (UnionIf a
_ Bool
_ SymBool
c UnionBase a
a UnionBase a
b) =
    Word8 -> m ()
forall (m :: * -> *). MonadPut m => Word8 -> m ()
putWord8 Word8
1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SymBool -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymBool -> m ()
serialize SymBool
c m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UnionBase a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize UnionBase a
a m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UnionBase a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize UnionBase a
b
  deserialize :: forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize = do
    Word8
tag <- m Word8
forall (m :: * -> *). MonadGet m => m Word8
getWord8
    case Word8
tag of
      Word8
0 -> a -> UnionBase a
forall a. a -> UnionBase a
UnionSingle (a -> UnionBase a) -> m a -> m (UnionBase a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m a
deserialize
      Word8
1 ->
        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
          (SymBool -> UnionBase a -> UnionBase a -> UnionBase a)
-> m SymBool -> m (UnionBase a -> UnionBase a -> UnionBase a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SymBool
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m SymBool
deserialize
          m (UnionBase a -> UnionBase a -> UnionBase a)
-> m (UnionBase a) -> m (UnionBase a -> UnionBase a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize
          m (UnionBase a -> UnionBase a)
-> m (UnionBase a) -> m (UnionBase a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize
      Word8
_ -> String -> m (UnionBase a)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid tag"

instance (Mergeable a, Serial a) => Cereal.Serialize (UnionBase a) where
  put :: Putter (UnionBase a)
put = Putter (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize
  get :: Get (UnionBase a)
get = Get (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize

instance (Mergeable a, Serial a) => Binary.Binary (UnionBase a) where
  put :: UnionBase a -> Put
put = UnionBase a -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize
  get :: Get (UnionBase a)
get = Get (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize

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)

-- | Fully reconstruct a 'Grisette.Core.Union' to maintain the merged invariant.
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 #-}

-- | Use a specific strategy to build a 'UnionIf' value.
--
-- The merged invariant will be maintained in the result.
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
-- {| symNot cond == condTrue || cond == symNot condTrue = ifWithStrategyInv strategy cond ft 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
-- {| symNot cond == condTrue || cond == symNot condTrue = ifWithStrategyInv strategy cond t tf -- buggy here condTrue
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 #-}