{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Core.Data.Union
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Core.Data.Union
  ( -- * The union data structure.

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

import Control.DeepSeq
import Data.Functor.Classes
import Data.Hashable
import GHC.Generics
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
import Language.Haskell.TH.Syntax

-- | The default union implementation.
data Union a
  = -- | A single value
    Single a
  | -- | A if value
    If
      a
      -- ^ Cached leftmost value
      !Bool
      -- ^ Is merged invariant already maintained?
      !SymBool
      -- ^ If condition
      (Union a)
      -- ^ True branch
      (Union a)
      -- ^ False branch
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Union a) x -> Union a
forall a x. Union a -> Rep (Union a) x
$cto :: forall a x. Rep (Union a) x -> Union a
$cfrom :: forall a x. Union a -> Rep (Union a) x
Generic, Union a -> Union a -> Bool
forall a. Eq a => Union a -> Union a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Union a -> Union a -> Bool
$c/= :: forall a. Eq a => Union a -> Union a -> Bool
== :: Union a -> Union a -> Bool
$c== :: forall a. Eq a => Union a -> Union a -> Bool
Eq, forall a (m :: * -> *). (Lift a, Quote m) => Union a -> m Exp
forall a (m :: * -> *).
(Lift a, Quote m) =>
Union a -> Code m (Union a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Union a -> m Exp
forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
liftTyped :: forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
$cliftTyped :: forall a (m :: * -> *).
(Lift a, Quote m) =>
Union a -> Code m (Union a)
lift :: forall (m :: * -> *). Quote m => Union a -> m Exp
$clift :: forall a (m :: * -> *). (Lift a, Quote m) => Union a -> m Exp
Lift, forall a. Rep1 Union a -> Union a
forall a. Union a -> Rep1 Union a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Union a -> Union a
$cfrom1 :: forall a. Union a -> Rep1 Union a
Generic1)

instance Eq1 Union where
  liftEq :: forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
liftEq a -> b -> Bool
e (Single a
a) (Single b
b) = a -> b -> Bool
e a
a b
b
  liftEq a -> b -> Bool
e (If a
l1 Bool
i1 SymBool
c1 Union a
t1 Union a
f1) (If b
l2 Bool
i2 SymBool
c2 Union b
t2 Union b
f2) =
    a -> b -> Bool
e a
l1 b
l2 Bool -> Bool -> Bool
&& Bool
i1 forall a. Eq a => a -> a -> Bool
== Bool
i2 Bool -> Bool -> Bool
&& SymBool
c1 forall a. Eq a => a -> a -> Bool
== SymBool
c2 Bool -> Bool -> Bool
&& forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e Union a
t1 Union b
t2 Bool -> Bool -> Bool
&& forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e Union a
f1 Union b
f2
  liftEq a -> b -> Bool
_ Union a
_ Union b
_ = Bool
False

instance (NFData a) => NFData (Union a) where
  rnf :: Union a -> ()
rnf = forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1

instance NFData1 Union where
  liftRnf :: forall a. (a -> ()) -> Union a -> ()
liftRnf a -> ()
_a (Single a
a) = a -> ()
_a a
a
  liftRnf a -> ()
_a (If a
a Bool
bo SymBool
b Union a
l Union a
r) = a -> ()
_a a
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Bool
bo seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SymBool
b seq :: forall a b. a -> b -> b
`seq` forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
l seq :: forall a b. a -> b -> b
`seq` forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
r

-- | Build 'If' with leftmost cache correctly maintained.
--
-- Usually you should never directly try to build a 'If' with its constructor.
ifWithLeftMost :: Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost :: forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
_ (Con Bool
c) Union a
t Union a
f
  | Bool
c = Union a
t
  | Bool
otherwise = Union a
f
ifWithLeftMost Bool
inv SymBool
cond Union a
t Union a
f = forall a. a -> Bool -> SymBool -> Union a -> Union a -> Union a
If (forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
t) Bool
inv SymBool
cond Union a
t Union a
f
{-# INLINE ifWithLeftMost #-}

instance UnionPrjOp Union where
  singleView :: forall a. Union a -> Maybe a
singleView (Single a
a) = forall a. a -> Maybe a
Just a
a
  singleView Union a
_ = forall a. Maybe a
Nothing
  {-# INLINE singleView #-}
  ifView :: forall a. Union a -> Maybe (SymBool, Union a, Union a)
ifView (If a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) = forall a. a -> Maybe a
Just (SymBool
cond, Union a
ifTrue, Union a
ifFalse)
  ifView Union a
_ = forall a. Maybe a
Nothing
  {-# INLINE ifView #-}
  leftMost :: forall a. Union a -> a
leftMost (Single a
a) = a
a
  leftMost (If a
a Bool
_ SymBool
_ Union a
_ Union a
_) = a
a
  {-# INLINE leftMost #-}

instance (Mergeable a) => Mergeable (Union a) where
  rootStrategy :: MergingStrategy (Union a)
rootStrategy = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy forall a. Mergeable a => MergingStrategy a
rootStrategy
  {-# INLINE rootStrategy #-}

instance Mergeable1 Union where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (Union a)
liftRootStrategy MergingStrategy a
ms = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
ms
  {-# INLINE liftRootStrategy #-}

instance (Mergeable a) => SimpleMergeable (Union a) where
  mrgIte :: SymBool -> Union a -> Union a -> Union a
mrgIte = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf

instance SimpleMergeable1 Union where
  liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> Union a -> Union a -> Union a
liftMrgIte SymBool -> a -> a -> a
m = forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)

instance UnionLike Union where
  mergeWithStrategy :: forall a. MergingStrategy a -> Union a -> Union a
mergeWithStrategy = forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct
  {-# INLINE mergeWithStrategy #-}
  single :: forall a. a -> Union a
single = forall a. a -> Union a
Single
  {-# INLINE single #-}
  unionIf :: forall a. SymBool -> Union a -> Union a -> Union a
unionIf = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
False
  {-# INLINE unionIf #-}
  mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
mrgIfWithStrategy = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy
  {-# INLINE mrgIfWithStrategy #-}
  mrgSingleWithStrategy :: forall a. MergingStrategy a -> a -> Union a
mrgSingleWithStrategy MergingStrategy a
_ = forall a. a -> Union a
Single
  {-# INLINE mrgSingleWithStrategy #-}

instance Show1 Union where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ Int
i (Single a
a) = 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 (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
    Bool -> ShowS -> ShowS
showParen (Int
i forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"If" forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
f
    where
      sp1 :: Int -> Union a -> ShowS
sp1 = forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl

instance (Show a) => Show (Union a) where
  showsPrec :: Int -> Union a -> ShowS
showsPrec = forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (Hashable a) => Hashable (Union a) where
  Int
s hashWithSalt :: Int -> Union a -> Int
`hashWithSalt` (Single a
a) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
a
  Int
s `hashWithSalt` (If a
_ Bool
_ SymBool
c Union a
l Union a
r) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` SymBool
c forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
l forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
r

instance AllSyms a => AllSyms (Union a) where
  allSymsS :: Union a -> [SomeSym] -> [SomeSym]
allSymsS (Single a
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
v
  allSymsS (If a
_ Bool
_ SymBool
c Union a
t Union a
f) = \[SomeSym]
l -> forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymBool
c forall a. a -> [a] -> [a]
: (forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
f forall a b. (a -> b) -> a -> b
$ [SomeSym]
l)

-- | Fully reconstruct a 'Union' to maintain the merged invariant.
fullReconstruct :: MergingStrategy a -> Union a -> Union a
fullReconstruct :: forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy (If a
_ Bool
False SymBool
cond Union a
t Union a
f) =
  forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond (forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
t) (forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
f)
fullReconstruct MergingStrategy a
_ Union a
u = Union a
u
{-# INLINE fullReconstruct #-}

-- | Use a specific strategy to build a 'If' value.
--
-- The merged invariant will be maintained in the result.
ifWithStrategy ::
  MergingStrategy a ->
  SymBool ->
  Union a ->
  Union a ->
  Union a
ifWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond t :: Union a
t@(If a
_ Bool
False SymBool
_ Union a
_ Union a
_) Union a
f = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond (forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
t) Union a
f
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t f :: Union a
f@(If a
_ Bool
False SymBool
_ Union a
_ Union a
_) = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t (forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
f)
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t Union a
f = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t Union a
f
{-# INLINE ifWithStrategy #-}

ifWithStrategyInv ::
  MergingStrategy a ->
  SymBool ->
  Union a ->
  Union a ->
  Union a
ifWithStrategyInv :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
_ (Con Bool
v) Union a
t Union a
f
  | Bool
v = Union a
t
  | Bool
otherwise = Union a
f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond (If a
_ Bool
True SymBool
condTrue Union a
tt Union a
_) Union a
f
  | SymBool
cond forall a. Eq a => a -> a -> Bool
== SymBool
condTrue = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
tt Union a
f
-- {| nots cond == condTrue || cond == nots condTrue = ifWithStrategyInv strategy cond ft f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t (If a
_ Bool
True SymBool
condFalse Union a
_ Union a
ff)
  | SymBool
cond forall a. Eq a => a -> a -> Bool
== SymBool
condFalse = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t Union a
ff
-- {| nots cond == condTrue || cond == nots condTrue = ifWithStrategyInv strategy cond t tf -- buggy here condTrue
ifWithStrategyInv (SimpleStrategy SymBool -> a -> a -> a
m) SymBool
cond (Single a
l) (Single a
r) = forall a. a -> Union a
Single forall a b. (a -> b) -> a -> b
$ SymBool -> a -> a -> a
m SymBool
cond a
l a
r
ifWithStrategyInv strategy :: MergingStrategy a
strategy@(SortedStrategy a -> idx
idxFun idx -> MergingStrategy a
substrategy) SymBool
cond Union a
ifTrue Union a
ifFalse = case (Union a
ifTrue, Union a
ifFalse) of
  (Single a
_, Single a
_) -> SymBool -> Union a -> Union a -> Union a
ssIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (Single a
_, If {}) -> SymBool -> Union a -> Union a -> Union a
sgIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (If {}, Single a
_) -> SymBool -> Union a -> Union a -> Union a
gsIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (Union a, Union a)
_ -> SymBool -> Union a -> Union a -> Union a
ggIf SymBool
cond Union a
ifTrue Union a
ifFalse
  where
    ssIf :: SymBool -> Union a -> Union a -> Union a
ssIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt forall a. Ord a => a -> a -> Bool
< idx
idxf = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt forall a. Eq a => a -> a -> Bool
== idx
idxf = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | Bool
otherwise = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (forall b. LogicalOp b => b -> b
nots SymBool
cond') Union a
ifFalse' Union a
ifTrue'
      where
        idxt :: idx
idxt = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ifTrue'
        idxf :: idx
idxf = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ifFalse'
    {-# INLINE ssIf #-}
    sgIf :: SymBool -> Union a -> Union a -> Union a
sgIf SymBool
cond' Union a
ifTrue' ifFalse' :: Union a
ifFalse'@(If a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
      | idx
idxft forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
ssIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt forall a. Ord a => a -> a -> Bool
< idx
idxft = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt forall a. Eq a => a -> a -> Bool
== idx
idxft = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' forall b. LogicalOp b => b -> b -> b
||~ SymBool
condf) (forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxt) SymBool
cond' Union a
ifTrue' Union a
ft) Union a
ff
      | Bool
otherwise = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (forall b. LogicalOp b => b -> b
nots SymBool
cond' forall b. LogicalOp b => b -> b -> b
&&~ SymBool
condf) Union a
ft (forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
ifTrue' Union a
ff)
      where
        idxft :: idx
idxft = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ft
        idxff :: idx
idxff = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ff
        idxt :: idx
idxt = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ifTrue'
    sgIf SymBool
_ Union a
_ Union a
_ = forall a. HasCallStack => a
undefined
    {-# INLINE sgIf #-}
    gsIf :: SymBool -> Union a -> Union a -> Union a
gsIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(If a
_ Bool
True SymBool
condt Union a
tt Union a
tf) Union a
ifFalse'
      | idx
idxtt forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
ssIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxtt forall a. Ord a => a -> a -> Bool
< idx
idxf = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' forall b. LogicalOp b => b -> b -> b
&&~ SymBool
condt) Union a
tt forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ifFalse'
      | idx
idxtt forall a. Eq a => a -> a -> Bool
== idx
idxf = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (forall b. LogicalOp b => b -> b
nots SymBool
cond' forall b. LogicalOp b => b -> b -> b
||~ SymBool
condt) (forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxf) SymBool
cond' Union a
tt Union a
ifFalse') Union a
tf
      | Bool
otherwise = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (forall b. LogicalOp b => b -> b
nots SymBool
cond') Union a
ifFalse' Union a
ifTrue'
      where
        idxtt :: idx
idxtt = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
tt
        idxtf :: idx
idxtf = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
tf
        idxf :: idx
idxf = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ifFalse'
    gsIf SymBool
_ Union a
_ Union a
_ = forall a. HasCallStack => a
undefined
    {-# INLINE gsIf #-}
    ggIf :: SymBool -> Union a -> Union a -> Union a
ggIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(If a
_ Bool
True SymBool
condt Union a
tt Union a
tf) ifFalse' :: Union a
ifFalse'@(If a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
      | idx
idxtt forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
sgIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxft forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
gsIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxtt forall a. Ord a => a -> a -> Bool
< idx
idxft = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' forall b. LogicalOp b => b -> b -> b
&&~ SymBool
condt) Union a
tt forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ifFalse'
      | idx
idxtt forall a. Eq a => a -> a -> Bool
== idx
idxft =
          let newCond :: SymBool
newCond = forall v. ITEOp v => SymBool -> v -> v -> v
ites SymBool
cond' SymBool
condt SymBool
condf
              newIfTrue :: Union a
newIfTrue = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv (idx -> MergingStrategy a
substrategy idx
idxtt) SymBool
cond' Union a
tt Union a
ft
              newIfFalse :: Union a
newIfFalse = forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ff
           in forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
newCond Union a
newIfTrue Union a
newIfFalse
      | Bool
otherwise = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (forall b. LogicalOp b => b -> b
nots SymBool
cond' forall b. LogicalOp b => b -> b -> b
&&~ SymBool
condf) Union a
ft forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
ifTrue' Union a
ff
      where
        idxtt :: idx
idxtt = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
tt
        idxtf :: idx
idxtf = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
tf
        idxft :: idx
idxft = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ft
        idxff :: idx
idxff = a -> idx
idxFun forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost Union a
ff
    ggIf SymBool
_ Union a
_ Union a
_ = forall a. HasCallStack => a
undefined
    {-# INLINE ggIf #-}
ifWithStrategyInv MergingStrategy a
NoStrategy SymBool
cond Union a
ifTrue Union a
ifFalse = forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond Union a
ifTrue Union a
ifFalse
ifWithStrategyInv MergingStrategy a
_ SymBool
_ Union a
_ Union a
_ = forall a. HasCallStack => String -> a
error String
"Invariant violated"
{-# INLINE ifWithStrategyInv #-}