{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# HLINT ignore "Use <&>" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.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.Core.Control.Monad.Union
  ( -- * Union and helpers
    Union (..),
    unionUnaryOp,
    unionBinOp,
    liftUnion,
    liftToMonadUnion,
    unionBase,
    unionMergingStrategy,
    isMerged,
    unionSize,
    IsConcrete,
  )
where

import Control.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)
import Data.Functor.Classes
  ( Eq1 (liftEq),
    Show1 (liftShowsPrec),
    showsPrec1,
  )
import qualified Data.HashMap.Lazy as HML
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.EvalSym
  ( EvalSym (evalSym),
    EvalSym1 (liftEvalSym),
    evalSym1,
  )
import Grisette.Internal.Core.Data.Class.ExtractSym
  ( ExtractSym (extractSymMaybe),
    ExtractSym1 (liftExtractSymMaybe),
    extractSymMaybe1,
  )
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (false, symImplies, symNot, symXor, true, (.&&), (.||)),
  )
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (SimpleStrategy),
    rootStrategy1,
  )
import Grisette.Internal.Core.Data.Class.PPrint
  ( PPrint (pformatPrec),
    PPrint1 (liftPFormatPrec),
    groupedEnclose,
    pformatPrec1,
  )
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( PlainUnion (ifView, singleView),
    simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    SymBranching (mrgIfPropagatedStrategy, mrgIfWithStrategy),
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, sym),
    pattern Con,
  )
import Grisette.Internal.Core.Data.Class.Solver
  ( UnionWithExcept (extractUnionExcept),
  )
import Grisette.Internal.Core.Data.Class.SubstSym
  ( SubstSym (substSym),
    SubstSym1 (liftSubstSym),
    substSym1,
  )
import Grisette.Internal.Core.Data.Class.SymEq
  ( SymEq ((.==)),
    SymEq1 (liftSymEq),
    symEq1,
  )
import Grisette.Internal.Core.Data.Class.ToCon
  ( ToCon (toCon),
    ToCon1 (liftToCon),
    toCon1,
  )
import Grisette.Internal.Core.Data.Class.ToSym
  ( ToSym (toSym),
    ToSym1 (liftToSym),
    toSym1,
  )
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge (tryMergeWithStrategy),
    mrgSingle,
    mrgSingleWithStrategy,
    tryMerge,
  )
import Grisette.Internal.Core.Data.UnionBase
  ( UnionBase (UnionIf, UnionSingle),
    ifWithLeftMost,
  )
import Grisette.Internal.SymPrim.AllSyms
  ( AllSyms (allSymsS),
    AllSyms1 (liftAllSymsS),
    allSymsS1,
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.GeneralFun
  ( type (-->),
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep,
    SupportedPrim,
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN,
    SymWordN,
  )
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
import Language.Haskell.TH.Syntax.Compat (unTypeSplice)

-- $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

-- | Get the (possibly empty) cached merging strategy.
unionMergingStrategy :: Union a -> Maybe (MergingStrategy a)
unionMergingStrategy :: forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy (UMrg MergingStrategy a
s UnionBase a
_) = MergingStrategy a -> Maybe (MergingStrategy a)
forall a. a -> Maybe a
Just MergingStrategy a
s
unionMergingStrategy Union a
_ = Maybe (MergingStrategy a)
forall a. Maybe a
Nothing

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 (UAny UnionBase a
m) = (a -> ()) -> UnionBase a -> ()
forall a. (a -> ()) -> UnionBase a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a UnionBase a
m
  liftRnf a -> ()
_a (UMrg MergingStrategy a
_ UnionBase a
m) = (a -> ()) -> UnionBase a -> ()
forall a. (a -> ()) -> UnionBase a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a UnionBase a
m

instance (Lift a) => Lift (Union a) where
  liftTyped :: forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
liftTyped (UAny UnionBase a
v) = [||UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny UnionBase a
v||]
  liftTyped (UMrg MergingStrategy a
_ UnionBase a
v) = [||UnionBase a -> Union a
forall a. UnionBase a -> Union a
UAny UnionBase a
v||]
  lift :: forall (m :: * -> *). Quote m => Union a -> m Exp
lift = Splice m (Union a) -> m Exp
forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice (Splice m (Union a) -> m Exp)
-> (Union a -> Splice m (Union a)) -> Union a -> m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> Splice m (Union a)
forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
forall (m :: * -> *). Quote m => Union a -> Code m (Union a)
liftTyped

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

liftShowsPrecUnion ::
  forall a.
  (Int -> a -> ShowS) ->
  ([a] -> ShowS) ->
  Int ->
  UnionBase a ->
  ShowS
liftShowsPrecUnion :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
_ Int
i (UnionSingle a
a) = Int -> a -> ShowS
sp Int
i a
a
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
t UnionBase a
f) =
  Bool -> ShowS -> ShowS
showParen (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"If"
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SymBool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> UnionBase a -> ShowS
sp1 Int
11 UnionBase a
t
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> UnionBase a -> ShowS
sp1 Int
11 UnionBase a
f
  where
    sp1 :: Int -> UnionBase a -> ShowS
sp1 = (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl

wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket Char
l Char
r ShowS
p = Char -> ShowS
showChar Char
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
r

instance Show1 Union where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UAny UnionBase a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'<' Char
'>'
      (ShowS -> ShowS) -> (UnionBase a -> ShowS) -> UnionBase a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      (UnionBase a -> ShowS) -> UnionBase a -> ShowS
forall a b. (a -> b) -> a -> b
$ UnionBase a
a
  liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UMrg MergingStrategy a
_ UnionBase a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'{' Char
'}'
      (ShowS -> ShowS) -> (UnionBase a -> ShowS) -> UnionBase a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      (UnionBase a -> ShowS) -> UnionBase a -> ShowS
forall a b. (a -> b) -> a -> b
$ UnionBase a
a

instance (PPrint a) => PPrint (Union a) where
  pformatPrec :: forall ann. Int -> Union a -> Doc ann
pformatPrec = Int -> Union a -> Doc ann
forall (f :: * -> *) a ann.
(PPrint1 f, PPrint a) =>
Int -> f a -> Doc ann
pformatPrec1

instance PPrint1 Union where
  liftPFormatPrec :: forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> Union a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
_ = \case
    (UAny UnionBase a
a) -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"<" Doc ann
">" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall (f :: * -> *) a ann.
PPrint1 f =>
(Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
0 UnionBase a
a
    (UMrg MergingStrategy a
_ UnionBase a
a) -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"{" Doc ann
"}" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann
forall (f :: * -> *) a ann.
PPrint1 f =>
(Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
fa [a] -> Doc ann
fl Int
0 UnionBase a
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 #-}

-- | Check if a 'Union' is already merged.
isMerged :: Union a -> Bool
isMerged :: forall a. Union a -> Bool
isMerged UAny {} = Bool
False
isMerged UMrg {} = Bool
True
{-# INLINE isMerged #-}

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

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 (>>=) #-}

-- | Lift a unary operation to 'Union'.
unionUnaryOp :: (a -> a) -> Union a -> Union a
unionUnaryOp :: forall a. (a -> a) -> Union a -> Union a
unionUnaryOp a -> a
f Union a
a = do
  a
a1 <- Union a
a
  (a -> Union a)
-> (MergingStrategy a -> a -> Union a)
-> Maybe (MergingStrategy a)
-> a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a -> Union a
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return MergingStrategy a -> a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m) =>
MergingStrategy a -> a -> m a
mrgSingleWithStrategy (Union a -> Maybe (MergingStrategy a)
forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy Union a
a) (a -> Union a) -> a -> Union a
forall a b. (a -> b) -> a -> b
$ a -> a
f a
a1
{-# INLINE unionUnaryOp #-}

-- | Lift a binary operation to 'Union'.
unionBinOp ::
  (a -> a -> a) ->
  Union a ->
  Union a ->
  Union a
unionBinOp :: forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
f Union a
a Union a
b = do
  a
a1 <- Union a
a
  a
b1 <- Union a
b
  (a -> Union a)
-> (MergingStrategy a -> a -> Union a)
-> Maybe (MergingStrategy a)
-> a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    a -> Union a
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return
    MergingStrategy a -> a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m) =>
MergingStrategy a -> a -> m a
mrgSingleWithStrategy
    (Union a -> Maybe (MergingStrategy a)
forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy Union a
a Maybe (MergingStrategy a)
-> Maybe (MergingStrategy a) -> Maybe (MergingStrategy a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Union a -> Maybe (MergingStrategy a)
forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy Union a
b)
    (a -> Union a) -> a -> Union a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
f a
a1 a
b1
{-# INLINE unionBinOp #-}

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

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 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 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 (SymEq a) => SymEq (Union a) where
  .== :: Union a -> Union a -> SymBool
(.==) = Union a -> Union a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance SymEq1 Union where
  liftSymEq :: forall a b. (a -> b -> SymBool) -> Union a -> Union b -> SymBool
liftSymEq a -> b -> SymBool
f Union a
x Union b
y = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ a -> b -> SymBool
f (a -> b -> SymBool) -> Union a -> Union (b -> SymBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Union a
x Union (b -> SymBool) -> Union b -> Union SymBool
forall a b. Union (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union b
y
  {-# INLINE liftSymEq #-}

-- | Lift the 'Union' to any Applicative 'SymBranching'.
liftUnion ::
  forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a
liftUnion :: forall (u :: * -> *) a.
(Mergeable a, SymBranching u, Applicative u) =>
Union a -> u a
liftUnion Union a
u = UnionBase a -> u a
go (Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
u)
  where
    go :: UnionBase a -> u a
    go :: UnionBase a -> u a
go (UnionSingle a
v) = a -> u a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v
    go (UnionIf a
_ Bool
_ SymBool
c UnionBase a
t UnionBase a
f) = SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c (UnionBase a -> u a
go UnionBase a
t) (UnionBase a -> u a
go UnionBase a
f)

-- | Alias for `liftUnion`, but for monads.
liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a
liftToMonadUnion :: forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
Union a -> u a
liftToMonadUnion = Union a -> u a
forall (u :: * -> *) a.
(Mergeable a, SymBranching u, Applicative u) =>
Union a -> u a
liftUnion

instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (Union b) where
  toSym :: a -> Union b
toSym = b -> Union b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (b -> Union b) -> (a -> b) -> a -> Union b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b. ToSym a b => a -> b
toSym

instance (ToSym a b) => ToSym (Union a) (Union b) where
  toSym :: Union a -> Union b
toSym = Union a -> Union b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1

instance ToSym1 Union Union where
  liftToSym :: forall b a. Mergeable b => (a -> b) -> Union a -> Union b
liftToSym a -> b
f = Union b -> Union b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union b -> Union b) -> (Union a -> Union b) -> Union a -> Union b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Union a -> Union b
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f

instance ToSym (Union Bool) SymBool where
  toSym :: Union Bool -> SymBool
toSym = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool)
-> (Union Bool -> Union SymBool) -> Union Bool -> SymBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> SymBool) -> Union Bool -> Union SymBool
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> SymBool
forall c t. Solvable c t => c -> t
con

instance ToSym (Union Integer) SymInteger where
  toSym :: Union Integer -> SymInteger
toSym = Union SymInteger -> SymInteger
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymInteger -> SymInteger)
-> (Union Integer -> Union SymInteger)
-> Union Integer
-> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> SymInteger) -> Union Integer -> Union SymInteger
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> SymInteger
forall c t. Solvable c t => c -> t
con

instance (KnownNat n, 1 <= n) => ToSym (Union (IntN n)) (SymIntN n) where
  toSym :: Union (IntN n) -> SymIntN n
toSym = Union (SymIntN n) -> SymIntN n
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union (SymIntN n) -> SymIntN n)
-> (Union (IntN n) -> Union (SymIntN n))
-> Union (IntN n)
-> SymIntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntN n -> SymIntN n) -> Union (IntN n) -> Union (SymIntN n)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IntN n -> SymIntN n
forall c t. Solvable c t => c -> t
con

instance (KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) where
  toSym :: Union (WordN n) -> SymWordN n
toSym = Union (SymWordN n) -> SymWordN n
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union (SymWordN n) -> SymWordN n)
-> (Union (WordN n) -> Union (SymWordN n))
-> Union (WordN n)
-> SymWordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WordN n -> SymWordN n) -> Union (WordN n) -> Union (SymWordN n)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WordN n -> SymWordN n
forall c t. Solvable c t => c -> t
con

instance
  (SupportedPrim ((=->) ca cb), LinkedRep ca sa, LinkedRep cb sb) =>
  ToSym (Union ((=->) ca cb)) ((=~>) sa sb)
  where
  toSym :: Union (ca =-> cb) -> sa =~> sb
toSym = Union (sa =~> sb) -> sa =~> sb
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union (sa =~> sb) -> sa =~> sb)
-> (Union (ca =-> cb) -> Union (sa =~> sb))
-> Union (ca =-> cb)
-> sa =~> sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ca =-> cb) -> sa =~> sb)
-> Union (ca =-> cb) -> Union (sa =~> sb)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ca =-> cb) -> sa =~> sb
forall c t. Solvable c t => c -> t
con

instance
  (SupportedPrim ((-->) ca cb), LinkedRep ca sa, LinkedRep cb sb) =>
  ToSym (Union ((-->) ca cb)) ((-~>) sa sb)
  where
  toSym :: Union (ca --> cb) -> sa -~> sb
toSym = Union (sa -~> sb) -> sa -~> sb
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union (sa -~> sb) -> sa -~> sb)
-> (Union (ca --> cb) -> Union (sa -~> sb))
-> Union (ca --> cb)
-> sa -~> sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ca --> cb) -> sa -~> sb)
-> Union (ca --> cb) -> Union (sa -~> sb)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ca --> cb) -> sa -~> sb
forall c t. Solvable c t => c -> t
con

instance {-# INCOHERENT #-} (ToCon a b, Mergeable a) => ToCon (Union a) b where
  toCon :: Union a -> Maybe b
toCon Union a
v = UnionBase a -> Maybe b
forall {a} {b}. ToCon a b => UnionBase a -> Maybe b
go (UnionBase a -> Maybe b) -> UnionBase a -> Maybe b
forall a b. (a -> b) -> a -> b
$ Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase (Union a -> UnionBase a) -> Union a -> UnionBase a
forall a b. (a -> b) -> a -> b
$ Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge Union a
v
    where
      go :: UnionBase a -> Maybe b
go (UnionSingle a
x) = a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
x
      go UnionBase a
_ = Maybe b
forall a. Maybe a
Nothing

instance (ToCon a b) => ToCon (Union a) (Union b) where
  toCon :: Union a -> Maybe (Union b)
toCon = Union a -> Maybe (Union b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1

instance ToCon1 Union Union where
  liftToCon :: forall a b. (a -> Maybe b) -> Union a -> Maybe (Union b)
liftToCon a -> Maybe b
f Union a
v = UnionBase a -> Maybe (Union b)
go (UnionBase a -> Maybe (Union b)) -> UnionBase a -> Maybe (Union b)
forall a b. (a -> b) -> a -> b
$ Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
v
    where
      go :: UnionBase a -> Maybe (Union b)
go (UnionSingle a
x) = case a -> Maybe b
f a
x of
        Maybe b
Nothing -> Maybe (Union b)
forall a. Maybe a
Nothing
        Just b
v -> Union b -> Maybe (Union b)
forall a. a -> Maybe a
Just (Union b -> Maybe (Union b)) -> Union b -> Maybe (Union b)
forall a b. (a -> b) -> a -> b
$ b -> Union b
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return b
v
      go (UnionIf a
_ Bool
_ SymBool
c UnionBase a
t UnionBase a
f) = do
        Union b
t' <- UnionBase a -> Maybe (Union b)
go UnionBase a
t
        Union b
f' <- UnionBase a -> Maybe (Union b)
go UnionBase a
f
        Union b -> Maybe (Union b)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Union b -> Maybe (Union b)) -> Union b -> Maybe (Union b)
forall a b. (a -> b) -> a -> b
$ 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
c Union b
t' Union b
f'

instance (EvalSym a) => EvalSym (Union a) where
  evalSym :: Bool -> Model -> Union a -> Union a
evalSym = Bool -> Model -> Union a -> Union a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1

instance EvalSym1 Union where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a) -> Bool -> Model -> Union a -> Union a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model Union a
x = UnionBase a -> Union a
go (UnionBase a -> Union a) -> UnionBase a -> Union a
forall a b. (a -> b) -> a -> b
$ Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
x
    where
      go :: UnionBase a -> Union a
go (UnionSingle a
v) = a -> Union a
single (a -> Union a) -> a -> Union a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
v
      go (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
t UnionBase a
f) =
        SymBool -> Union a -> Union a -> Union a
unionIf (Bool -> Model -> SymBool -> SymBool
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model SymBool
cond) (UnionBase a -> Union a
go UnionBase a
t) (UnionBase a -> Union a
go UnionBase a
f)
      strategy :: Maybe (MergingStrategy a)
strategy = Union a -> Maybe (MergingStrategy a)
forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy Union a
x
      single :: a -> Union a
single = (a -> Union a)
-> (MergingStrategy a -> a -> Union a)
-> Maybe (MergingStrategy a)
-> a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a -> Union a
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return MergingStrategy a -> a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m) =>
MergingStrategy a -> a -> m a
mrgSingleWithStrategy Maybe (MergingStrategy a)
strategy
      unionIf :: SymBool -> Union a -> Union a -> Union a
unionIf = (SymBool -> Union a -> Union a -> Union a)
-> (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a)
-> Maybe (MergingStrategy a)
-> SymBool
-> Union a
-> Union a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SymBool -> Union a -> Union a -> Union a
forall a. SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
SymBranching u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy 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 Maybe (MergingStrategy a)
strategy

instance (SubstSym a) => SubstSym (Union a) where
  substSym :: forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> Union a -> Union a
substSym = TypedSymbol knd cb -> sb -> Union a -> Union a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1

instance SubstSym1 Union where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Union a -> Union a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb
sym sb
val Union a
x = UnionBase a -> Union a
go (UnionBase a -> Union a) -> UnionBase a -> Union a
forall a b. (a -> b) -> a -> b
$ Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
x
    where
      go :: UnionBase a -> Union a
go (UnionSingle a
v) = a -> Union a
single (a -> Union a) -> a -> Union a
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb
sym sb
val a
v
      go (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
t UnionBase a
f) =
        SymBool -> Union a -> Union a -> Union a
unionIf
          (TypedSymbol knd cb -> sb -> SymBool -> SymBool
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SymBool -> SymBool
substSym TypedSymbol knd cb
sym sb
val SymBool
cond)
          (UnionBase a -> Union a
go UnionBase a
t)
          (UnionBase a -> Union a
go UnionBase a
f)
      strategy :: Maybe (MergingStrategy a)
strategy = Union a -> Maybe (MergingStrategy a)
forall a. Union a -> Maybe (MergingStrategy a)
unionMergingStrategy Union a
x
      single :: a -> Union a
single = (a -> Union a)
-> (MergingStrategy a -> a -> Union a)
-> Maybe (MergingStrategy a)
-> a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a -> Union a
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return MergingStrategy a -> a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m) =>
MergingStrategy a -> a -> m a
mrgSingleWithStrategy Maybe (MergingStrategy a)
strategy
      unionIf :: SymBool -> Union a -> Union a -> Union a
unionIf = (SymBool -> Union a -> Union a -> Union a)
-> (MergingStrategy a -> SymBool -> Union a -> Union a -> Union a)
-> Maybe (MergingStrategy a)
-> SymBool
-> Union a
-> Union a
-> Union a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SymBool -> Union a -> Union a -> Union a
forall a. SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
SymBranching u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy 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 Maybe (MergingStrategy a)
strategy

instance (ExtractSym a) => ExtractSym (Union a) where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
Union a -> Maybe (SymbolSet knd)
extractSymMaybe = Union a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1

instance ExtractSym1 Union where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> Union a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
e Union a
v = UnionBase a -> Maybe (SymbolSet knd)
go (UnionBase a -> Maybe (SymbolSet knd))
-> UnionBase a -> Maybe (SymbolSet knd)
forall a b. (a -> b) -> a -> b
$ Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
v
    where
      go :: UnionBase a -> Maybe (SymbolSet knd)
go (UnionSingle a
x) = a -> Maybe (SymbolSet knd)
e a
x
      go (UnionIf a
_ Bool
_ SymBool
cond UnionBase a
t UnionBase a
f) = SymBool -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
SymBool -> Maybe (SymbolSet knd)
extractSymMaybe SymBool
cond Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> UnionBase a -> Maybe (SymbolSet knd)
go UnionBase a
t Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> UnionBase a -> Maybe (SymbolSet knd)
go UnionBase a
f

instance (Hashable a) => Hashable (Union a) where
  Int
s hashWithSalt :: Int -> Union a -> Int
`hashWithSalt` (UAny UnionBase a
u) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> UnionBase a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` UnionBase a
u
  Int
s `hashWithSalt` (UMrg MergingStrategy a
_ UnionBase a
u) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> UnionBase a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` UnionBase a
u

instance (Eq a) => Eq (Union a) where
  UAny UnionBase a
l == :: Union a -> Union a -> Bool
== UAny UnionBase a
r = UnionBase a
l UnionBase a -> UnionBase a -> Bool
forall a. Eq a => a -> a -> Bool
== UnionBase a
r
  UMrg MergingStrategy a
_ UnionBase a
l == UMrg MergingStrategy a
_ UnionBase a
r = UnionBase a
l UnionBase a -> UnionBase a -> Bool
forall a. Eq a => a -> a -> Bool
== UnionBase a
r
  Union a
_ == Union a
_ = Bool
False

instance Eq1 Union where
  liftEq :: forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
liftEq a -> b -> Bool
e Union a
l Union b
r = (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool
forall a b. (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e (Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase Union a
l) (Union b -> UnionBase b
forall a. Union a -> UnionBase a
unionBase Union b
r)

instance (Num a, Mergeable a) => Num (Union a) where
  fromInteger :: Integer -> Union a
fromInteger = a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> Union a) -> (Integer -> a) -> Integer -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger
  negate :: Union a -> Union a
negate = (a -> a) -> Union a -> Union a
forall a. (a -> a) -> Union a -> Union a
unionUnaryOp a -> a
forall a. Num a => a -> a
negate
  + :: Union a -> Union a -> Union a
(+) = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall a. Num a => a -> a -> a
(+)
  * :: Union a -> Union a -> Union a
(*) = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall a. Num a => a -> a -> a
(*)
  (-) = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp (-)
  abs :: Union a -> Union a
abs = (a -> a) -> Union a -> Union a
forall a. (a -> a) -> Union a -> Union a
unionUnaryOp a -> a
forall a. Num a => a -> a
abs
  signum :: Union a -> Union a
signum = (a -> a) -> Union a -> Union a
forall a. (a -> a) -> Union a -> Union a
unionUnaryOp a -> a
forall a. Num a => a -> a
signum

instance (ITEOp a, Mergeable a) => ITEOp (Union a) where
  symIte :: SymBool -> Union a -> Union a -> Union a
symIte = SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf

instance (LogicalOp a, Mergeable a) => LogicalOp (Union a) where
  true :: Union a
true = a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
forall b. LogicalOp b => b
true
  false :: Union a
false = a -> Union a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
forall b. LogicalOp b => b
false
  .|| :: Union a -> Union a -> Union a
(.||) = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.||)
  .&& :: Union a -> Union a -> Union a
(.&&) = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.&&)
  symNot :: Union a -> Union a
symNot = (a -> a) -> Union a -> Union a
forall a. (a -> a) -> Union a -> Union a
unionUnaryOp a -> a
forall b. LogicalOp b => b -> b
symNot
  symXor :: Union a -> Union a -> Union a
symXor = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
symXor
  symImplies :: Union a -> Union a -> Union a
symImplies = (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
symImplies

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
    t
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
    t -> Maybe c
forall c t. Solvable c t => t -> Maybe c
conView t
c
  {-# INLINE conView #-}

instance
  (Function f arg ret, Mergeable f, Mergeable ret) =>
  Function (Union f) arg (Union ret)
  where
  Union f
f # :: Union f -> arg -> Union ret
# arg
a = do
    f
f1 <- Union f
f
    ret -> Union ret
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (ret -> Union ret) -> ret -> Union ret
forall a b. (a -> b) -> a -> b
$ f
f1 f -> arg -> ret
forall f arg ret. Function f arg ret => f -> arg -> ret
# arg
a

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

-- AllSyms
instance (AllSyms a) => AllSyms (Union a) where
  allSymsS :: Union a -> [SomeSym] -> [SomeSym]
allSymsS = Union a -> [SomeSym] -> [SomeSym]
forall (f :: * -> *) a.
(AllSyms1 f, AllSyms a) =>
f a -> [SomeSym] -> [SomeSym]
allSymsS1

instance AllSyms1 Union where
  liftAllSymsS :: forall a.
(a -> [SomeSym] -> [SomeSym]) -> Union a -> [SomeSym] -> [SomeSym]
liftAllSymsS a -> [SomeSym] -> [SomeSym]
f = (a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall a.
(a -> [SomeSym] -> [SomeSym])
-> UnionBase a -> [SomeSym] -> [SomeSym]
forall (f :: * -> *) a.
AllSyms1 f =>
(a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
liftAllSymsS a -> [SomeSym] -> [SomeSym]
f (UnionBase a -> [SomeSym] -> [SomeSym])
-> (Union a -> UnionBase a) -> Union a -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase

-- Concrete Key HashMaps

-- | Tag for concrete types.
-- Useful for specifying the merge strategy for some parametrized types where we should have different
-- merge strategy for symbolic and concrete ones.
class (Eq t, Ord t, Hashable t) => IsConcrete t

instance IsConcrete Bool

instance IsConcrete Integer

instance (IsConcrete k, Mergeable t) => Mergeable (HML.HashMap k (Union (Maybe t))) where
  rootStrategy :: MergingStrategy (HashMap k (Union (Maybe t)))
rootStrategy = (SymBool
 -> HashMap k (Union (Maybe t))
 -> HashMap k (Union (Maybe t))
 -> HashMap k (Union (Maybe t)))
-> MergingStrategy (HashMap k (Union (Maybe t)))
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte

instance (IsConcrete k, Mergeable t) => SimpleMergeable (HML.HashMap k (Union (Maybe t))) where
  mrgIte :: SymBool
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
mrgIte SymBool
cond HashMap k (Union (Maybe t))
l HashMap k (Union (Maybe t))
r =
    (Union (Maybe t) -> Union (Maybe t) -> Union (Maybe t))
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HML.unionWith (SymBool -> Union (Maybe t) -> Union (Maybe t) -> Union (Maybe t)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond) HashMap k (Union (Maybe t))
ul HashMap k (Union (Maybe t))
ur
    where
      ul :: HashMap k (Union (Maybe t))
ul =
        (k -> HashMap k (Union (Maybe t)) -> HashMap k (Union (Maybe t)))
-> HashMap k (Union (Maybe t))
-> [k]
-> HashMap k (Union (Maybe t))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          ( \k
k HashMap k (Union (Maybe t))
m -> case k -> HashMap k (Union (Maybe t)) -> Maybe (Union (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (Union (Maybe t))
m of
              Maybe (Union (Maybe t))
Nothing -> k
-> Union (Maybe t)
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> Union (Maybe t)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (Union (Maybe t))
m
              Maybe (Union (Maybe t))
_ -> HashMap k (Union (Maybe t))
m
          )
          HashMap k (Union (Maybe t))
l
          (HashMap k (Union (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (Union (Maybe t))
r)
      ur :: HashMap k (Union (Maybe t))
ur =
        (k -> HashMap k (Union (Maybe t)) -> HashMap k (Union (Maybe t)))
-> HashMap k (Union (Maybe t))
-> [k]
-> HashMap k (Union (Maybe t))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          ( \k
k HashMap k (Union (Maybe t))
m -> case k -> HashMap k (Union (Maybe t)) -> Maybe (Union (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (Union (Maybe t))
m of
              Maybe (Union (Maybe t))
Nothing -> k
-> Union (Maybe t)
-> HashMap k (Union (Maybe t))
-> HashMap k (Union (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> Union (Maybe t)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (Union (Maybe t))
m
              Maybe (Union (Maybe t))
_ -> HashMap k (Union (Maybe t))
m
          )
          HashMap k (Union (Maybe t))
r
          (HashMap k (Union (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (Union (Maybe t))
l)

instance UnionWithExcept (Union (Either e v)) Union e v where
  extractUnionExcept :: Union (Either e v) -> Union (Either e v)
extractUnionExcept = Union (Either e v) -> Union (Either e v)
forall a. a -> a
id

-- | The size of a union is defined as the number of branches.
-- For example,
--
-- >>> unionSize (return True)
-- 1
-- >>> unionSize (mrgIf "a" (return 1) (return 2) :: Union Integer)
-- 2
-- >>> unionSize (choose [1..7] "a" :: Union Integer)
-- 7
unionSize :: Union a -> Int
unionSize :: forall a. Union a -> Int
unionSize = UnionBase a -> Int
forall {a} {a}. Num a => UnionBase a -> a
unionSize' (UnionBase a -> Int) -> (Union a -> UnionBase a) -> Union a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase
  where
    unionSize' :: UnionBase a -> a
unionSize' (UnionSingle a
_) = a
1
    unionSize' (UnionIf a
_ Bool
_ SymBool
_ UnionBase a
l UnionBase a
r) = UnionBase a -> a
unionSize' UnionBase a
l a -> a -> a
forall a. Num a => a -> a -> a
+ UnionBase a -> a
unionSize' UnionBase a
r