{-# 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.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.Internal.Core.Data.Union
  ( -- * The union data structure.

    -- | Please consider using 'Grisette.Internal.Core.Control.Monad.UnionM' instead.
    Union (..),
    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.GPretty
  ( GPretty (gprettyPrec),
    condEnclose,
  )
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.PlainUnion
  ( PlainUnion (ifView, singleView),
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    UnionMergeable1 (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),
    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 default union implementation.
data Union a where
  -- | A single value
  UnionSingle :: a -> Union a
  -- | A if value
  UnionIf ::
    -- | Cached leftmost value
    a ->
    -- | Is merged invariant already maintained?
    !Bool ->
    -- | If condition
    !SymBool ->
    -- | True branch
    Union a ->
    -- | False branch
    Union a ->
    Union a
  deriving ((forall x. Union a -> Rep (Union a) x)
-> (forall x. Rep (Union a) x -> Union a) -> Generic (Union a)
forall x. Rep (Union a) x -> Union a
forall x. Union a -> Rep (Union a) x
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
$cfrom :: forall a x. Union a -> Rep (Union a) x
from :: forall x. Union a -> Rep (Union a) x
$cto :: forall a x. Rep (Union a) x -> Union a
to :: forall x. Rep (Union a) x -> Union a
Generic, Union a -> Union a -> Bool
(Union a -> Union a -> Bool)
-> (Union a -> Union a -> Bool) -> Eq (Union a)
forall a. Eq a => Union a -> Union a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Union a -> Union a -> Bool
Eq, (forall (m :: * -> *). Quote m => Union a -> m Exp)
-> (forall (m :: * -> *). Quote m => Union a -> Code m (Union a))
-> Lift (Union a)
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)
$clift :: forall a (m :: * -> *). (Lift a, Quote m) => Union a -> m Exp
lift :: forall (m :: * -> *). Quote m => Union a -> m Exp
$cliftTyped :: forall a (m :: * -> *).
(Lift a, Quote m) =>
Union a -> Code m (Union a)
liftTyped :: forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
Lift, (forall a. Union a -> Rep1 Union a)
-> (forall a. Rep1 Union a -> Union a) -> Generic1 Union
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
$cfrom1 :: forall a. Union a -> Rep1 Union a
from1 :: forall a. Union a -> Rep1 Union a
$cto1 :: forall a. Rep1 Union a -> Union a
to1 :: forall a. Rep1 Union a -> Union a
Generic1)
  deriving ((forall a b. (a -> b) -> Union a -> Union b)
-> (forall a b. a -> Union b -> Union a) -> Functor Union
forall a b. a -> Union b -> Union a
forall a b. (a -> b) -> Union a -> Union 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) -> Union a -> Union b
fmap :: forall a b. (a -> b) -> Union a -> Union b
$c<$ :: forall a b. a -> Union b -> Union a
<$ :: forall a b. a -> Union b -> Union a
Functor)

instance Applicative Union where
  pure :: forall a. a -> Union a
pure = a -> Union a
forall a. a -> Union a
UnionSingle
  {-# INLINE pure #-}
  <*> :: forall a b. Union (a -> b) -> Union a -> Union b
(<*>) = Union (a -> b) -> Union a -> Union b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
  {-# INLINE (<*>) #-}

instance Monad Union where
  return :: forall a. a -> Union a
return = a -> Union a
forall a. a -> Union a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE return #-}
  UnionSingle a
a >>= :: forall a b. Union a -> (a -> Union b) -> Union b
>>= a -> Union b
f = a -> Union b
f a
a
  UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f >>= a -> Union b
f' = Bool -> SymBool -> Union b -> Union b -> Union b
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
False SymBool
c (Union a
t Union a -> (a -> Union b) -> Union b
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Union b
f') (Union a
f Union a -> (a -> Union b) -> Union b
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Union b
f')
  {-# INLINE (>>=) #-}

instance Eq1 Union where
  liftEq :: forall a b. (a -> b -> Bool) -> Union a -> Union 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 Union a
t1 Union a
f1) (UnionIf 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 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) -> Union a -> Union b -> Bool
forall a b. (a -> b -> Bool) -> Union a -> Union b -> 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
&& (a -> b -> Bool) -> Union a -> Union b -> Bool
forall a b. (a -> b -> Bool) -> Union a -> Union b -> 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 = Union a -> ()
forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1

instance NFData1 Union where
  liftRnf :: forall a. (a -> ()) -> Union a -> ()
liftRnf a -> ()
_a (UnionSingle a
a) = a -> ()
_a a
a
  liftRnf a -> ()
_a (UnionIf a
a Bool
bo SymBool
b Union a
l Union 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 -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
l () -> () -> ()
forall a b. a -> b -> b
`seq`
            (a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union 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 -> 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 = a -> Bool -> SymBool -> Union a -> Union a -> Union a
forall a. a -> Bool -> SymBool -> Union a -> Union a -> Union a
UnionIf (Union a -> a
forall a. Union a -> a
leftMost Union a
t) Bool
inv SymBool
cond Union a
t Union a
f
{-# INLINE ifWithLeftMost #-}

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

leftMost :: Union a -> a
leftMost :: forall a. Union a -> a
leftMost (UnionSingle a
a) = a
a
leftMost (UnionIf a
a Bool
_ SymBool
_ Union a
_ Union a
_) = a
a
{-# INLINE leftMost #-}

instance (Mergeable a) => Mergeable (Union a) where
  rootStrategy :: MergingStrategy (Union a)
rootStrategy = (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Union a -> Union a -> Union a)
 -> MergingStrategy (Union a))
-> (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
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 = (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Union a -> Union a -> Union a)
 -> MergingStrategy (Union a))
-> (SymBool -> Union a -> Union a -> Union a)
-> MergingStrategy (Union a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 = SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
(UnionMergeable1 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 = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
UnionMergeable1 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 Union where
  tryMergeWithStrategy :: forall a. MergingStrategy a -> Union a -> Union a
tryMergeWithStrategy = MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct
  {-# INLINE tryMergeWithStrategy #-}

instance UnionMergeable1 Union where
  mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
mrgIfWithStrategy = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy
  {-# INLINE mrgIfWithStrategy #-}

  mrgIfPropagatedStrategy :: forall a. SymBool -> Union a -> Union a -> Union a
mrgIfPropagatedStrategy = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
False
  {-# INLINE mrgIfPropagatedStrategy #-}

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 (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 Union a
t Union 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 -> Union a -> ShowS
sp1 Int
11 Union 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 -> Union a -> ShowS
sp1 Int
11 Union a
f
    where
      sp1 :: Int -> Union a -> ShowS
sp1 = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union 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 (Union a) where
  showsPrec :: Int -> Union a -> ShowS
showsPrec = Int -> Union a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (GPretty a) => GPretty (Union a) where
  gprettyPrec :: forall ann. Int -> Union a -> Doc ann
gprettyPrec Int
n (UnionSingle a
a) = Int -> a -> Doc ann
forall ann. Int -> a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
n a
a
  gprettyPrec Int
n (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union 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. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 SymBool
cond,
                Int -> Union a -> Doc ann
forall ann. Int -> Union a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 Union a
t,
                Int -> Union a -> Doc ann
forall ann. Int -> Union a -> Doc ann
forall a ann. GPretty a => Int -> a -> Doc ann
gprettyPrec Int
11 Union a
f
              ]

instance (Hashable a) => Hashable (Union a) where
  Int
s hashWithSalt :: Int -> Union 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 Union a
l Union 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 -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
l
      Int -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
r

instance (AllSyms a) => AllSyms (Union a) where
  allSymsS :: Union 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 Union a
t Union 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]
: (Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
t ([SomeSym] -> [SomeSym])
-> ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS Union a
f ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
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 (UnionIf a
_ Bool
False SymBool
cond Union a
t Union a
f) =
  MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv
    MergingStrategy a
strategy
    SymBool
cond
    (MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
strategy Union a
t)
    (MergingStrategy a -> Union a -> Union a
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 'UnionIf' 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@(UnionIf a
_ Bool
False SymBool
_ Union a
_ Union a
_) Union a
f =
  MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond (MergingStrategy a -> Union a -> Union a
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@(UnionIf a
_ Bool
False SymBool
_ Union a
_ Union a
_) =
  MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
strategy SymBool
cond Union a
t (MergingStrategy a -> Union a -> Union a
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 = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 (UnionIf a
_ Bool
True SymBool
condTrue Union a
tt Union a
_) Union a
f
  | SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condTrue = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
tt Union a
f
-- {| symNot cond == condTrue || cond == symNot condTrue = ifWithStrategyInv strategy cond ft f
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t (UnionIf a
_ Bool
True SymBool
condFalse Union a
_ Union a
ff)
  | SymBool
cond SymBool -> SymBool -> Bool
forall a. Eq a => a -> a -> Bool
== SymBool
condFalse = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond Union a
t Union 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 -> Union a
forall a. a -> Union a
UnionSingle (a -> Union a) -> a -> Union 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 Union a
ifTrue Union a
ifFalse = case (Union a
ifTrue, Union a
ifFalse) of
  (UnionSingle a
_, UnionSingle a
_) -> SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (UnionSingle a
_, UnionIf {}) -> SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (UnionIf {}, UnionSingle a
_) -> SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
  (Union a, Union a)
_ -> SymBool -> Union a -> Union a -> Union a
ggUnionIf SymBool
cond Union a
ifTrue Union a
ifFalse
  where
    ssUnionIf :: SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') Union a
ifFalse' Union a
ifTrue'
      where
        idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifTrue'
        idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifFalse'
    {-# INLINE ssUnionIf #-}
    sgUnionIf :: SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond' Union a
ifTrue' ifFalse' :: Union a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
      | idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool
condf) (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union 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) Union a
ft (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ft
        idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ff
        idxt :: idx
idxt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifTrue'
    sgUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
    {-# INLINE sgUnionIf #-}
    gsUnionIf :: SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt Union a
tt Union a
tf) Union a
ifFalse'
      | idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
ssUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) Union a
tt (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxf = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union 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 -> Union a -> Union a -> Union a
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 = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
cond') Union a
ifFalse' Union a
ifTrue'
      where
        idxtt :: idx
idxtt = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tt
        idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tf
        idxf :: idx
idxf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ifFalse'
    gsUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
    {-# INLINE gsUnionIf #-}
    ggUnionIf :: SymBool -> Union a -> Union a -> Union a
ggUnionIf SymBool
cond' ifTrue' :: Union a
ifTrue'@(UnionIf a
_ Bool
True SymBool
condt Union a
tt Union a
tf) ifFalse' :: Union a
ifFalse'@(UnionIf a
_ Bool
True SymBool
condf Union a
ft Union a
ff)
      | idx
idxtt idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxtf = SymBool -> Union a -> Union a -> Union a
sgUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxft idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idxff = SymBool -> Union a -> Union a -> Union a
gsUnionIf SymBool
cond' Union a
ifTrue' Union a
ifFalse'
      | idx
idxtt idx -> idx -> Bool
forall a. Ord a => a -> a -> Bool
< idx
idxft = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True (SymBool
cond' SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
condt) Union a
tt (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 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 :: Union a
newUnionIfTrue = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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
              newUnionIfFalse :: Union a
newUnionIfFalse = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategyInv MergingStrategy a
strategy SymBool
cond' Union a
tf Union a
ff
           in Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union a
ifWithLeftMost Bool
True SymBool
newCond Union a
newUnionIfTrue Union a
newUnionIfFalse
      | Bool
otherwise = Bool -> SymBool -> Union a -> Union a -> Union a
forall a. Bool -> SymBool -> Union a -> Union a -> Union 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) Union a
ft (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
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 (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tt
        idxtf :: idx
idxtf = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
tf
        idxft :: idx
idxft = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ft
        idxff :: idx
idxff = a -> idx
idxFun (a -> idx) -> a -> idx
forall a b. (a -> b) -> a -> b
$ Union a -> a
forall a. Union a -> a
leftMost Union a
ff
    ggUnionIf SymBool
_ Union a
_ Union a
_ = Union a
forall a. HasCallStack => a
undefined
    {-# INLINE ggUnionIf #-}
ifWithStrategyInv MergingStrategy a
NoStrategy SymBool
cond Union a
ifTrue Union a
ifFalse = Bool -> SymBool -> Union a -> Union a -> Union a
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
_ = String -> Union a
forall a. HasCallStack => String -> a
error String
"Invariant violated"
{-# INLINE ifWithStrategyInv #-}