{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Use <&>" #-}

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Control.Monad.Union
-- 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.Control.Monad.Union
  ( -- * Union and helpers
    Union (..),
    unionBase,
  )
where

import Data.String (IsString (fromString))
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( PlainUnion (ifView, singleView, toGuardedList),
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, sym),
    pattern Con,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy, sortIndices),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (SimpleStrategy),
    resolveStrategy,
    rootStrategy1,
  )
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),
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.Internal.Decl.Core.Data.UnionBase
  ( UnionBase (UnionIf, UnionSingle),
    ifWithLeftMost,
  )

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | 'Union' is the 'UnionBase' container (hidden) enhanced with
-- 'MergingStrategy'
-- [knowledge propagation](https://okmij.org/ftp/Haskell/set-monad.html#PE).
--
-- The 'UnionBase' models the underlying semantics evaluation semantics for
-- unsolvable types with the nested if-then-else tree semantics, and can be
-- viewed as the following structure:
--
-- > data UnionBase a
-- >   = UnionSingle a
-- >   | UnionIf bool (Union a) (Union a)
--
-- The 'UnionSingle' constructor is for a single value with the path condition
-- @true@, and the 'UnionIf' constructor is the if operator in an if-then-else
-- tree.
-- For clarity, when printing a 'Union' value, we will omit the 'UnionSingle'
-- constructor. The following two representations has the same semantics.
--
-- > If      c1    (If c11 v11 (If c12 v12 v13))
-- >   (If   c2    v2
-- >               v3)
--
-- \[
--   \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right.
-- \]
--
-- To reduce the size of the if-then-else tree to reduce the number of paths to
-- execute, Grisette would merge the branches in a 'UnionBase' container and
-- maintain a representation invariant for them. To perform this merging
-- procedure, Grisette relies on a type class called 'Mergeable' and the
-- merging strategy defined by it.
--
-- 'UnionBase' is a monad, so we can easily write code with the do-notation and
-- monadic combinators. However, the standard monadic operators cannot
-- resolve any extra constraints, including the 'Mergeable' constraint (see
-- [The constrained-monad
-- problem](https://dl.acm.org/doi/10.1145/2500365.2500602)
-- by Sculthorpe et al.).
-- This prevents the standard do-notations to merge the results automatically,
-- and would result in bad performance or very verbose code.
--
-- To reduce this boilerplate, Grisette provide another monad, 'Union' that
-- would try to cache the merging strategy.
-- The 'Union' has two data constructors (hidden intentionally), 'UAny' and
-- 'UMrg'. The 'UAny' data constructor (printed as @<@@...@@>@) wraps an
-- arbitrary (probably unmerged) 'UnionBase'. It is constructed when no
-- 'Mergeable' knowledge is available (for example, when constructed with
-- Haskell\'s 'return'). The 'UMrg' data constructor (printed as @{...}@) wraps
-- a merged 'UnionBase' along with the 'Mergeable' constraint. This constraint
-- can be propagated to the contexts without 'Mergeable' knowledge, and helps
-- the system to merge the resulting 'UnionBase'.
--
-- __/Examples:/__
--
-- 'return' cannot resolve the 'Mergeable' constraint.
--
-- >>> return 1 :: Union Integer
-- <1>
--
-- 'Grisette.Lib.Control.Monad.mrgReturn' can resolve the 'Mergeable' constraint.
--
-- >>> import Grisette.Lib.Base
-- >>> mrgReturn 1 :: Union Integer
-- {1}
--
-- 'mrgIfPropagatedStrategy' does not try to 'Mergeable' constraint.
--
-- >>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: Union Integer
-- <If a 1 (If b 1 2)>
--
-- But 'mrgIfPropagatedStrategy' is able to merge the result if some of the
-- branches are merged and have a cached merging strategy:
--
-- >>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (mrgReturn 1) (return 2)) :: Union Integer
-- {If (|| a b) 1 2}
--
-- The '>>=' operator uses 'mrgIfPropagatedStrategy' internally. When the final
-- statement in a do-block merges the values, the system can then merge the
-- final result.
--
-- >>> :{
--   do
--     x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))
--     mrgSingle $ x + 1 :: Union Integer
-- :}
-- {If (|| a b) 2 3}
--
-- Calling a function that merges a result at the last line of a do-notation
-- will also merge the whole block. If you stick to these @mrg*@ combinators and
-- all the functions will merge the results, the whole program can be
-- symbolically evaluated efficiently.
--
-- >>> f x y = mrgIf "c" x y :: Union Integer
-- >>> :{
--   do
--     x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))
--     f x (x + 1)
-- :}
-- {If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}
--
-- In "Grisette.Lib.Base", "Grisette.Lib.Mtl", we also provided more @mrg*@
-- variants of other combinators. You should stick to these combinators to
-- ensure efficient merging by Grisette.
data Union a where
  -- | 'Union' with no 'Mergeable' knowledge.
  UAny ::
    -- | Original 'UnionBase'.
    UnionBase a ->
    Union a
  -- | 'Union' with 'Mergeable' knowledge.
  UMrg ::
    -- | Cached merging strategy.
    MergingStrategy a ->
    -- | Merged 'UnionBase'
    UnionBase a ->
    Union a

-- | Extract the underlying Union. May be unmerged.
unionBase :: Union a -> UnionBase a
unionBase :: forall a. Union a -> UnionBase a
unionBase (UAny UnionBase a
a) = UnionBase a
a
unionBase (UMrg MergingStrategy a
_ UnionBase a
a) = UnionBase a
a
{-# INLINE unionBase #-}

instance Functor Union where
  fmap :: forall a b. (a -> b) -> Union a -> Union b
fmap a -> b
f Union a
fa = Union a
fa 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
>>= b -> Union b
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Union b) -> (a -> b) -> a -> Union b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
  {-# INLINE fmap #-}

instance Applicative Union where
  pure :: forall a. a -> Union a
pure = UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny (UnionBase a -> Union a) -> (a -> UnionBase a) -> a -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> UnionBase a
forall a. a -> UnionBase a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE pure #-}
  Union (a -> b)
f <*> :: forall a b. Union (a -> b) -> Union a -> Union b
<*> Union a
a = Union (a -> b)
f Union (a -> b) -> ((a -> b) -> 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 -> b
xf -> Union a
a 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
>>= (b -> Union b
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Union b) -> (a -> b) -> a -> Union b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
xf))
  {-# INLINE (<*>) #-}

bindUnionBase :: UnionBase a -> (a -> Union b) -> Union b
bindUnionBase :: forall a b. UnionBase a -> (a -> Union b) -> Union b
bindUnionBase (UnionSingle a
a') a -> Union b
f' = a -> Union b
f' a
a'
bindUnionBase (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
ifTrue UnionBase a
ifFalse) a -> Union b
f' =
  SymBool -> Union b -> Union b -> Union b
forall a. SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
SymBranching u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy
    SymBool
cond
    (UnionBase a -> (a -> Union b) -> Union b
forall a b. UnionBase a -> (a -> Union b) -> Union b
bindUnionBase UnionBase a
ifTrue a -> Union b
f')
    (UnionBase a -> (a -> Union b) -> Union b
forall a b. UnionBase a -> (a -> Union b) -> Union b
bindUnionBase UnionBase a
ifFalse a -> Union b
f')
{-# INLINE bindUnionBase #-}

instance Monad Union where
  Union a
a >>= :: forall a b. Union a -> (a -> Union b) -> Union b
>>= a -> Union b
f = UnionBase a -> (a -> Union b) -> Union b
forall a b. UnionBase a -> (a -> Union b) -> Union b
bindUnionBase (Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
a) a -> Union b
f
  {-# INLINE (>>=) #-}

instance TryMerge Union where
  tryMergeWithStrategy :: forall a. MergingStrategy a -> Union a -> Union a
tryMergeWithStrategy MergingStrategy a
_ m :: Union a
m@(UMrg MergingStrategy a
_ UnionBase a
_) = Union a
m
  tryMergeWithStrategy MergingStrategy a
s (UAny UnionBase a
u) = MergingStrategy a -> UnionBase a -> Union a
forall a. MergingStrategy a -> UnionBase a -> Union a
UMrg MergingStrategy a
s (UnionBase a -> Union a) -> UnionBase a -> Union a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> UnionBase a -> UnionBase a
forall a. MergingStrategy a -> UnionBase a -> UnionBase a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy a
s UnionBase a
u
  {-# INLINE tryMergeWithStrategy #-}

instance (IsString a, Mergeable a) => IsString (Union a) where
  fromString :: String -> Union a
fromString = a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> Union a) -> (String -> a) -> String -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> a
forall a. IsString a => String -> a
fromString

instance (Solvable c t, Mergeable t) => Solvable c (Union t) where
  con :: c -> Union t
con = t -> Union t
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (t -> Union t) -> (c -> t) -> c -> Union t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> t
forall c t. Solvable c t => c -> t
con
  {-# INLINE con #-}
  sym :: Symbol -> Union t
sym = t -> Union t
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (t -> Union t) -> (Symbol -> t) -> Symbol -> Union t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> t
forall c t. Solvable c t => Symbol -> t
sym
  {-# INLINE sym #-}
  conView :: Union t -> Maybe c
conView Union t
v = do
    c <- Union t -> Maybe t
forall a. Union a -> Maybe a
forall (u :: * -> *) a. PlainUnion u => u a -> Maybe a
singleView (Union t -> Maybe t) -> Union t -> Maybe t
forall a b. (a -> b) -> a -> b
$ Union t -> Union t
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge Union t
v
    conView c
  {-# INLINE conView #-}

instance (Mergeable a) => Mergeable (Union a) where
  rootStrategy :: MergingStrategy (Union a)
rootStrategy = MergingStrategy (Union a)
forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1
  {-# INLINE rootStrategy #-}
  sortIndices :: Union a -> [DynamicSortedIdx]
sortIndices = ([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx]
forall a b. (a, b) -> a
fst (([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx])
-> (Union a -> ([DynamicSortedIdx], MergingStrategy a))
-> Union a
-> [DynamicSortedIdx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MergingStrategy a -> a -> ([DynamicSortedIdx], MergingStrategy a)
forall x.
MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy (a -> ([DynamicSortedIdx], MergingStrategy a))
-> (Union a -> a)
-> Union a
-> ([DynamicSortedIdx], MergingStrategy a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymBool, a) -> a
forall a b. (a, b) -> b
snd ((SymBool, a) -> a) -> (Union a -> (SymBool, a)) -> Union a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SymBool, a)] -> (SymBool, a)
forall a. HasCallStack => [a] -> a
head ([(SymBool, a)] -> (SymBool, a))
-> (Union a -> [(SymBool, a)]) -> Union a -> (SymBool, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> [(SymBool, a)]
forall a. Union a -> [(SymBool, a)]
forall (u :: * -> *) a. PlainUnion u => u a -> [(SymBool, a)]
toGuardedList

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.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
  {-# INLINE mrgIte #-}

instance Mergeable1 Union where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (Union a)
liftRootStrategy MergingStrategy a
m = (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
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy MergingStrategy a
m
  {-# INLINE liftRootStrategy #-}

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.
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)
  {-# INLINE liftMrgIte #-}

instance SymBranching Union where
  mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
mrgIfWithStrategy MergingStrategy a
s (Con Bool
c) Union a
l Union a
r =
    if Bool
c then MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy a
s Union a
l else MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy a
s Union a
r
  mrgIfWithStrategy MergingStrategy a
s SymBool
cond Union a
l Union a
r =
    MergingStrategy a -> UnionBase a -> Union a
forall a. MergingStrategy a -> UnionBase a -> Union a
UMrg MergingStrategy a
s (UnionBase a -> Union a) -> UnionBase a -> Union 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
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy
        MergingStrategy a
s
        SymBool
cond
        (Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
l)
        (Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
r)
  {-# INLINE mrgIfWithStrategy #-}
  mrgIfPropagatedStrategy :: forall a. SymBool -> Union a -> Union a -> Union a
mrgIfPropagatedStrategy SymBool
cond (UAny UnionBase a
t) (UAny UnionBase a
f) =
    UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny (UnionBase a -> Union a) -> UnionBase a -> Union a
forall a b. (a -> b) -> a -> b
$ Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
forall a.
Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost Bool
False SymBool
cond UnionBase a
t UnionBase a
f
  mrgIfPropagatedStrategy SymBool
cond t :: Union a
t@(UMrg MergingStrategy a
m UnionBase a
_) Union a
f = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy MergingStrategy a
m SymBool
cond Union a
t Union a
f
  mrgIfPropagatedStrategy SymBool
cond Union a
t f :: Union a
f@(UMrg MergingStrategy a
m UnionBase a
_) = MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy MergingStrategy a
m SymBool
cond Union a
t Union a
f
  {-# INLINE mrgIfPropagatedStrategy #-}

instance PlainUnion Union where
  singleView :: forall a. Union a -> Maybe a
singleView = UnionBase a -> Maybe a
forall a. UnionBase a -> Maybe a
forall (u :: * -> *) a. PlainUnion u => u a -> Maybe a
singleView (UnionBase a -> Maybe a)
-> (Union a -> UnionBase a) -> Union a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase
  {-# INLINE singleView #-}
  ifView :: forall a. Union a -> Maybe (SymBool, Union a, Union a)
ifView (UAny UnionBase a
u) = case UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a)
forall a. UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a)
forall (u :: * -> *) a.
PlainUnion u =>
u a -> Maybe (SymBool, u a, u a)
ifView UnionBase a
u of
    Just (SymBool
c, UnionBase a
t, UnionBase a
f) -> (SymBool, Union a, Union a) -> Maybe (SymBool, Union a, Union a)
forall a. a -> Maybe a
Just (SymBool
c, UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny UnionBase a
t, UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny UnionBase a
f)
    Maybe (SymBool, UnionBase a, UnionBase a)
Nothing -> Maybe (SymBool, Union a, Union a)
forall a. Maybe a
Nothing
  ifView (UMrg MergingStrategy a
m UnionBase a
u) = case UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a)
forall a. UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a)
forall (u :: * -> *) a.
PlainUnion u =>
u a -> Maybe (SymBool, u a, u a)
ifView UnionBase a
u of
    Just (SymBool
c, UnionBase a
t, UnionBase a
f) -> (SymBool, Union a, Union a) -> Maybe (SymBool, Union a, Union a)
forall a. a -> Maybe a
Just (SymBool
c, MergingStrategy a -> UnionBase a -> Union a
forall a. MergingStrategy a -> UnionBase a -> Union a
UMrg MergingStrategy a
m UnionBase a
t, MergingStrategy a -> UnionBase a -> Union a
forall a. MergingStrategy a -> UnionBase a -> Union a
UMrg MergingStrategy a
m UnionBase a
f)
    Maybe (SymBool, UnionBase a, UnionBase a)
Nothing -> Maybe (SymBool, Union a, Union a)
forall a. Maybe a
Nothing
  {-# INLINE ifView #-}