{-# 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

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

-- | 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 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 #-}