{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Internal.Internal.Decl.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.Internal.Decl.Core.Data.UnionBase
  ( -- * The union data structure.

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

import Control.Monad (ap)
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.PlainUnion
  ( PlainUnion (ifView, singleView),
  )
import Grisette.Internal.Core.Data.Class.Solvable (pattern Con)
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    SymBranching (mrgIfPropagatedStrategy, mrgIfWithStrategy),
    mrgIf,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.TryMerge
  ( TryMerge (tryMergeWithStrategy),
  )
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 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 #-}

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

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

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

-- | 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
_ = [Char] -> UnionBase a
forall a. HasCallStack => [Char] -> a
error [Char]
"Invariant violated"
{-# INLINE ifWithStrategyInv #-}

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