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

import Control.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)
import Control.Monad.Identity (Identity (Identity, runIdentity))
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Functor.Classes
  ( Eq1 (liftEq),
    Show1 (liftShowsPrec),
    showsPrec1,
  )
import qualified Data.HashMap.Lazy as HML
import Data.Hashable (Hashable (hashWithSalt))
import Data.Hashable.Lifted (Hashable1 (liftHashWithSalt), hashWithSalt1)
import qualified Data.Serialize as Cereal
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),
    MergingStrategy (SimpleStrategy),
  )
import Grisette.Internal.Core.Data.Class.PPrint
  ( PPrint (pformatPrec),
    PPrint1 (liftPFormatPrec),
    groupedEnclose,
    pformatPrec1,
  )
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SymBranching (mrgIfPropagatedStrategy, mrgIfWithStrategy),
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (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.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
  ( mrgSingle,
    mrgSingleWithStrategy,
    tryMerge,
  )
import Grisette.Internal.Internal.Decl.Core.Control.Monad.Union
  ( Union (UAny, UMrg),
    unionBase,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq
  ( SymEq ((.==)),
    SymEq1 (liftSymEq),
    symEq1,
  )
import Grisette.Internal.Internal.Decl.Core.Data.UnionBase
  ( UnionBase (UnionIf, UnionSingle),
  )
import Grisette.Internal.Internal.Impl.Core.Data.UnionBase ()
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,
    SupportedNonFuncPrim,
    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

instance (Mergeable a, Serial a) => Serial (Union a) where
  serialize :: forall (m :: * -> *). MonadPut m => Union a -> m ()
serialize = UnionBase a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => UnionBase a -> m ()
serialize (UnionBase a -> m ())
-> (Union a -> UnionBase a) -> Union a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union a -> UnionBase a
forall a. Union a -> UnionBase a
unionBase
  deserialize :: forall (m :: * -> *). MonadGet m => m (Union a)
deserialize = MergingStrategy a -> UnionBase a -> Union a
forall a. MergingStrategy a -> UnionBase a -> Union a
UMrg MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy (UnionBase a -> Union a) -> m (UnionBase a) -> m (Union a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (UnionBase a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (UnionBase a)
deserialize

instance (Mergeable a, Serial a) => Cereal.Serialize (Union a) where
  put :: Putter (Union a)
put = Putter (Union a)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Union a -> m ()
serialize
  get :: Get (Union a)
get = Get (Union a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (Union a)
deserialize

instance (Mergeable a, Serial a) => Binary.Binary (Union a) where
  put :: Union a -> Put
put = Union a -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Union a -> m ()
serialize
  get :: Get (Union a)
get = Get (Union a)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (Union a)
deserialize

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

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

-- | 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
  a1 <- Union a
a
  maybe return mrgSingleWithStrategy (unionMergingStrategy a) $ f 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
  a1 <- Union a
a
  b1 <- b
  maybe
    return
    mrgSingleWithStrategy
    (unionMergingStrategy a <|> unionMergingStrategy b)
    $ f a1 b1
{-# INLINE unionBinOp #-}

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 (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 a b. (a -> b) -> Union a -> Union b
liftToSym = (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

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

instance ToSym1 Identity Union where
  liftToSym :: forall a b. (a -> b) -> Identity a -> Union b
liftToSym a -> b
f Identity a
v = b -> Union b
forall a. a -> Union a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Union b) -> b -> Union b
forall a b. (a -> b) -> a -> b
$ Identity b -> b
forall a. Identity a -> a
runIdentity (Identity b -> b) -> Identity b -> b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> Identity a -> Identity b
forall a b. (a -> b) -> Identity a -> Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Identity a
v

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),
    SupportedNonFuncPrim ca,
    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),
    SupportedNonFuncPrim ca,
    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 (ToCon a b) => ToCon (Union a) (Identity b) where
  toCon :: Union a -> Maybe (Identity b)
toCon = Union a -> Maybe (Identity b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1

instance ToCon1 Union Identity where
  liftToCon :: forall a b. (a -> Maybe b) -> Union a -> Maybe (Identity b)
liftToCon a -> Maybe b
f Union a
v = UnionBase a -> Maybe (Identity b)
go (UnionBase a -> Maybe (Identity b))
-> UnionBase a -> Maybe (Identity 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 (Identity b)
go (UnionSingle a
x) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> Maybe b -> Maybe (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x
      go (UnionIf a
_ Bool
_ SymBool
c UnionBase a
t UnionBase a
f) =
        case SymBool -> Maybe Bool
forall a b. ToCon a b => a -> Maybe b
toCon SymBool
c of
          Maybe Bool
Nothing -> Maybe (Identity b)
forall a. Maybe a
Nothing
          Just Bool
True -> UnionBase a -> Maybe (Identity b)
go UnionBase a
t
          Just Bool
False -> UnionBase a -> Maybe (Identity b)
go UnionBase a
f

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
        t' <- UnionBase a -> Maybe (Union b)
go UnionBase a
t
        f' <- go f
        return $ mrgIfPropagatedStrategy c t' 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
  hashWithSalt :: Int -> Union a -> Int
hashWithSalt = Int -> Union a -> Int
forall (f :: * -> *) a.
(Hashable1 f, Hashable a) =>
Int -> f a -> Int
hashWithSalt1

instance Hashable1 Union where
  liftHashWithSalt :: forall a. (Int -> a -> Int) -> Int -> Union a -> Int
liftHashWithSalt Int -> a -> Int
f Int
s (UAny UnionBase a
u) =
    (Int -> a -> Int) -> Int -> UnionBase a -> Int
forall a. (Int -> a -> Int) -> Int -> UnionBase a -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt Int -> a -> Int
f (Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)) UnionBase a
u
  liftHashWithSalt Int -> a -> Int
f Int
s (UMrg MergingStrategy a
_ UnionBase a
u) =
    (Int -> a -> Int) -> Int -> UnionBase a -> Int
forall a. (Int -> a -> Int) -> Int -> UnionBase a -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt Int -> a -> Int
f (Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int)) 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 = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> (Union a -> Union a) -> Union a -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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
l + :: Union a -> Union a -> Union a
+ Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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
l Union a
r
  Union a
l * :: Union a -> Union a -> Union a
* Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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
l Union a
r
  Union a
l - :: Union a -> Union a -> Union a
- Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Union a -> Union a -> Union a
forall a. (a -> a -> a) -> Union a -> Union a -> Union a
unionBinOp (-) Union a
l Union a
r
  abs :: Union a -> Union a
abs = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> (Union a -> Union a) -> Union a -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> (Union a -> Union a) -> Union a -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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
l .|| :: Union a -> Union a -> Union a
.|| Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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
l Union a
r
  Union a
l .&& :: Union a -> Union a -> Union a
.&& Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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
l Union a
r
  symNot :: Union a -> Union a
symNot = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> (Union a -> Union a) -> Union a -> Union a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 Union a
l Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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 Union a
l Union a
r
  symImplies :: Union a -> Union a -> Union a
symImplies Union a
l Union a
r = Union a -> Union a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union a -> Union a) -> Union a -> Union a
forall a b. (a -> b) -> a -> b
$ (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 Union a
l Union a
r

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
    f1 <- Union f
f
    mrgSingle $ f1 # a

-- 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 {t} {a}. Num t => UnionBase a -> t
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 -> t
unionSize' (UnionSingle a
_) = t
1
    unionSize' (UnionIf a
_ Bool
_ SymBool
_ UnionBase a
l UnionBase a
r) = UnionBase a -> t
unionSize' UnionBase a
l t -> t -> t
forall a. Num a => a -> a -> a
+ UnionBase a -> t
unionSize' UnionBase a
r