{-# 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.UnionM
-- 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.UnionM
  ( -- * UnionM and helpers
    UnionM (..),
    unionMUnaryOp,
    unionMBinOp,
    liftUnionM,
    liftToMonadUnion,
    underlyingUnion,
    isMerged,
    unionSize,
    IsConcrete,
  )
where

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.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
  ( ExtractSymbolics (extractSymbolics),
  )
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.Core.Data.Class.GPretty
  ( GPretty (gpretty),
    groupedEnclose,
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
  )
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (SimpleStrategy),
  )
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( PlainUnion (ifView, singleView),
    simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SEq (SEq ((.==)))
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    UnionMergeable1 (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.SubstituteSym (SubstituteSym (substituteSym))
import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge (tryMergeWithStrategy),
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.Core.Data.Union
  ( Union (UnionIf, UnionSingle),
    ifWithLeftMost,
  )
import Grisette.Internal.SymPrim.AllSyms
  ( AllSyms (allSymsS),
  )
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
-- >>> :set -XScopedTypeVariables

-- | 'UnionM' is the 'Union' container (hidden) enhanced with
-- 'MergingStrategy'
-- [knowledge propagation](https://okmij.org/ftp/Haskell/set-monad.html#PE).
--
-- The 'Union' 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 Union a
-- >   = Single a
-- >   | If bool (Union a) (Union a)
--
-- The 'Single' constructor is for a single value with the path condition
-- @true@, and the 'If' constructor is the if operator in an if-then-else
-- tree.
-- For clarity, when printing a 'UnionM' value, we will omit the 'Single'
-- 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 'Union' 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.
--
-- 'Union' 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, 'UnionM' that
-- would try to cache the merging strategy.
-- The 'UnionM' has two data constructors (hidden intentionally), 'UAny' and 'UMrg'.
-- The 'UAny' data constructor (printed as @<@@...@@>@) wraps an arbitrary (probably
-- unmerged) 'Union'. 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 'UnionM' along with the
-- 'Mergeable' constraint. This constraint can be propagated to the contexts
-- without 'Mergeable' knowledge, and helps the system to merge the resulting
-- 'Union'.
--
-- __/Examples:/__
--
-- 'return' cannot resolve the 'Mergeable' constraint.
--
-- >>> return 1 :: UnionM Integer
-- <1>
--
-- 'Grisette.Lib.Control.Monad.mrgReturn' can resolve the 'Mergeable' constraint.
--
-- >>> import Grisette.Lib.Base
-- >>> mrgReturn 1 :: UnionM Integer
-- {1}
--
-- 'mrgIfPropagatedStrategy' does not try to 'Mergeable' constraint.
--
-- >>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: UnionM 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)) :: UnionM 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 :: UnionM 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
-- >>> :{
--   do
--     x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))
--     f x (x + 1) :: UnionM Integer
-- :}
-- {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 UnionM a where
  -- | 'UnionM' with no 'Mergeable' knowledge.
  UAny ::
    -- | Original 'Union'.
    Union a ->
    UnionM a
  -- | 'UnionM' with 'Mergeable' knowledge.
  UMrg ::
    -- | Cached merging strategy.
    MergingStrategy a ->
    -- | Merged Union
    Union a ->
    UnionM a

instance (NFData a) => NFData (UnionM a) where
  rnf :: UnionM a -> ()
rnf = UnionM a -> ()
forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1

instance NFData1 UnionM where
  liftRnf :: forall a. (a -> ()) -> UnionM a -> ()
liftRnf a -> ()
_a (UAny Union a
m) = (a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
  liftRnf a -> ()
_a (UMrg MergingStrategy a
_ Union a
m) = (a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m

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

instance (Show a) => (Show (UnionM a)) where
  showsPrec :: Int -> UnionM a -> ShowS
showsPrec = Int -> UnionM a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

liftShowsPrecUnion ::
  forall a.
  (Int -> a -> ShowS) ->
  ([a] -> ShowS) ->
  Int ->
  Union a ->
  ShowS
liftShowsPrecUnion :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union 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 Union a
t Union a
f) =
  Bool -> ShowS -> ShowS
showParen (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"If"
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SymBool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
f
  where
    sp1 :: Int -> Union a -> ShowS
sp1 = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
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 UnionM where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> UnionM a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UAny Union a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'<' Char
'>'
      (ShowS -> ShowS) -> (Union a -> ShowS) -> Union a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      (Union a -> ShowS) -> Union a -> ShowS
forall a b. (a -> b) -> a -> b
$ Union a
a
  liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UMrg MergingStrategy a
_ Union a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'{' Char
'}'
      (ShowS -> ShowS) -> (Union a -> ShowS) -> Union a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      (Union a -> ShowS) -> Union a -> ShowS
forall a b. (a -> b) -> a -> b
$ Union a
a

instance (GPretty a) => GPretty (UnionM a) where
  gpretty :: forall ann. UnionM a -> Doc ann
gpretty = \case
    (UAny Union 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
$ Union a -> Doc ann
forall a ann. GPretty a => a -> Doc ann
forall ann. Union a -> Doc ann
gpretty Union a
a
    (UMrg MergingStrategy a
_ Union 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
$ Union a -> Doc ann
forall a ann. GPretty a => a -> Doc ann
forall ann. Union a -> Doc ann
gpretty Union a
a

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

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

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

instance Functor UnionM where
  fmap :: forall a b. (a -> b) -> UnionM a -> UnionM b
fmap a -> b
f UnionM a
fa = UnionM a
fa UnionM a -> (a -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> UnionM b
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> UnionM b) -> (a -> b) -> a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
  {-# INLINE fmap #-}

instance Applicative UnionM where
  pure :: forall a. a -> UnionM a
pure = Union a -> UnionM a
forall a. Union a -> UnionM a
UAny (Union a -> UnionM a) -> (a -> Union a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Union a
forall a. a -> Union a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE pure #-}
  UnionM (a -> b)
f <*> :: forall a b. UnionM (a -> b) -> UnionM a -> UnionM b
<*> UnionM a
a = UnionM (a -> b)
f UnionM (a -> b) -> ((a -> b) -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a -> b
xf -> UnionM a
a UnionM a -> (a -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (b -> UnionM b
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> UnionM b) -> (a -> b) -> a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
xf))
  {-# INLINE (<*>) #-}

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

instance Monad UnionM where
  UnionM a
a >>= :: forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
>>= a -> UnionM b
f = Union a -> (a -> UnionM b) -> UnionM b
forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) a -> UnionM b
f
  {-# INLINE (>>=) #-}

unionMUnaryOp :: (Mergeable a, Mergeable b) => (a -> b) -> UnionM a -> UnionM b
unionMUnaryOp :: forall a b.
(Mergeable a, Mergeable b) =>
(a -> b) -> UnionM a -> UnionM b
unionMUnaryOp a -> b
f UnionM a
a = do
  a
a1 <- UnionM a -> UnionM a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM a
a
  b -> UnionM b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (b -> UnionM b) -> b -> UnionM b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a1
{-# INLINE unionMUnaryOp #-}

unionMBinOp ::
  (Mergeable a, Mergeable b, Mergeable c) =>
  (a -> b -> c) ->
  UnionM a ->
  UnionM b ->
  UnionM c
unionMBinOp :: forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> b -> c
f UnionM a
a UnionM b
b = do
  a
a1 <- UnionM a -> UnionM a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM a
a
  b
b1 <- UnionM b -> UnionM b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM b
b
  c -> UnionM c
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (c -> UnionM c) -> c -> UnionM c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
a1 b
b1
{-# INLINE unionMBinOp #-}

instance (Mergeable a) => Mergeable (UnionM a) where
  rootStrategy :: MergingStrategy (UnionM a)
rootStrategy = (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
  {-# INLINE rootStrategy #-}

instance (Mergeable a) => SimpleMergeable (UnionM a) where
  mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a
mrgIte = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
  {-# INLINE mrgIte #-}

instance Mergeable1 UnionM where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (UnionM a)
liftRootStrategy MergingStrategy a
m = (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> UnionM a -> UnionM a -> UnionM a)
 -> MergingStrategy (UnionM a))
-> (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a.
MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionMergeable1 u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy MergingStrategy a
m
  {-# INLINE liftRootStrategy #-}

instance SimpleMergeable1 UnionM where
  liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> UnionM a -> UnionM a -> UnionM a
liftMrgIte SymBool -> a -> a -> a
m = MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a.
MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionMergeable1 u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
  {-# INLINE liftMrgIte #-}

instance TryMerge UnionM where
  tryMergeWithStrategy :: forall a. MergingStrategy a -> UnionM a -> UnionM a
tryMergeWithStrategy MergingStrategy a
_ m :: UnionM a
m@(UMrg MergingStrategy a
_ Union a
_) = UnionM a
m
  tryMergeWithStrategy MergingStrategy a
s (UAny Union a
u) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
s (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ 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
u
  {-# INLINE tryMergeWithStrategy #-}

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

instance (Mergeable a, SEq a) => SEq (UnionM a) where
  UnionM a
x .== :: UnionM a -> UnionM a -> SymBool
.== UnionM a
y = UnionM SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (UnionM SymBool -> SymBool) -> UnionM SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ (a -> a -> SymBool) -> UnionM a -> UnionM a -> UnionM SymBool
forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
(.==) UnionM a
x UnionM a
y
  {-# INLINE (.==) #-}

-- | Lift the 'UnionM' to any Applicative 'UnionMergeable1'.
liftUnionM :: (Mergeable a, UnionMergeable1 u, Applicative u) => UnionM a -> u a
liftUnionM :: forall a (u :: * -> *).
(Mergeable a, UnionMergeable1 u, Applicative u) =>
UnionM a -> u a
liftUnionM UnionM a
u = Union a -> u a
forall {m :: * -> *} {a}.
(Applicative m, Mergeable a, UnionMergeable1 m) =>
Union a -> m a
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
u)
  where
    go :: Union a -> m a
go (UnionSingle a
v) = a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v
    go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c (Union a -> m a
go Union a
t) (Union a -> m a
go Union a
f)

-- | Alias for `liftUnionM`, but for monads.
liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a
liftToMonadUnion :: forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion = UnionM a -> u a
forall a (u :: * -> *).
(Mergeable a, UnionMergeable1 u, Applicative u) =>
UnionM a -> u a
liftUnionM

instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where
  toSym :: a -> UnionM b
toSym = b -> UnionM b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (b -> UnionM b) -> (a -> b) -> a -> UnionM 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, Mergeable b) => ToSym (UnionM a) (UnionM b) where
  toSym :: UnionM a -> UnionM b
toSym = UnionM b -> UnionM b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (UnionM b -> UnionM b)
-> (UnionM a -> UnionM b) -> UnionM a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> UnionM a -> UnionM b
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
forall a b. ToSym a b => a -> b
toSym

#define TO_SYM_FROM_UNION_CON_SIMPLE(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
  toSym = simpleMerge . fmap con

#define TO_SYM_FROM_UNION_CON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (UnionM (contype n)) (symtype n) where \
  toSym = simpleMerge . fmap con

#define TO_SYM_FROM_UNION_CON_FUN(conop, symop) \
instance (SupportedPrim (conop ca cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (conop ca cb)) (symop sa sb) where \
  toSym = simpleMerge . fmap con

#define TO_SYM_FROM_UNION_CON_BV_SOME(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
  toSym = simpleMerge . fmap (toSym :: contype -> symtype)

#if 1
TO_SYM_FROM_UNION_CON_SIMPLE(Bool, SymBool)
TO_SYM_FROM_UNION_CON_SIMPLE(Integer, SymInteger)
TO_SYM_FROM_UNION_CON_BV(IntN, SymIntN)
TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN)
TO_SYM_FROM_UNION_CON_FUN((=->), (=~>))
TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))
#endif

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

instance
  (ToCon a b, Mergeable a, Mergeable b) =>
  ToCon (UnionM a) (UnionM b)
  where
  toCon :: UnionM a -> Maybe (UnionM b)
toCon UnionM a
v = Union a -> Maybe (UnionM b)
forall {a} {a} {m :: * -> *}.
(ToCon a a, Applicative m, Mergeable a, UnionMergeable1 m) =>
Union a -> Maybe (m a)
go (Union a -> Maybe (UnionM b)) -> Union a -> Maybe (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion (UnionM a -> Union a) -> UnionM a -> Union a
forall a b. (a -> b) -> a -> b
$ UnionM a -> UnionM a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM a
v
    where
      go :: Union a -> Maybe (m a)
go (UnionSingle a
x) = case a -> Maybe a
forall a b. ToCon a b => a -> Maybe b
toCon a
x of
        Maybe a
Nothing -> Maybe (m a)
forall a. Maybe a
Nothing
        Just a
v -> m a -> Maybe (m a)
forall a. a -> Maybe a
Just (m a -> Maybe (m a)) -> m a -> Maybe (m a)
forall a b. (a -> b) -> a -> b
$ a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
v
      go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = do
        m a
t' <- Union a -> Maybe (m a)
go Union a
t
        m a
f' <- Union a -> Maybe (m a)
go Union a
f
        m a -> Maybe (m a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (m a -> Maybe (m a)) -> m a -> Maybe (m a)
forall a b. (a -> b) -> a -> b
$ SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c m a
t' m a
f'

instance (Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) where
  evaluateSym :: Bool -> Model -> UnionM a -> UnionM a
evaluateSym Bool
fillDefault Model
model UnionM a
x = Union a -> UnionM a
go (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
    where
      go :: Union a -> UnionM a
      go :: Union a -> UnionM a
go (UnionSingle a
v) = a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model a
v
      go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
        SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
          (Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model SymBool
cond)
          (Union a -> UnionM a
go Union a
t)
          (Union a -> UnionM a
go Union a
f)

instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where
  substituteSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> UnionM a -> UnionM a
substituteSym TypedSymbol cb
sym sb
val UnionM a
x = Union a -> UnionM a
go (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
    where
      go :: Union a -> UnionM a
      go :: Union a -> UnionM a
go (UnionSingle a
v) = a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substituteSym TypedSymbol cb
sym sb
val a
v
      go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
        SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
          (TypedSymbol cb -> sb -> SymBool -> SymBool
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> SymBool -> SymBool
substituteSym TypedSymbol cb
sym sb
val SymBool
cond)
          (Union a -> UnionM a
go Union a
t)
          (Union a -> UnionM a
go Union a
f)

instance
  (ExtractSymbolics a) =>
  ExtractSymbolics (UnionM a)
  where
  extractSymbolics :: UnionM a -> SymbolSet
extractSymbolics UnionM a
v = Union a -> SymbolSet
forall {a}. ExtractSymbolics a => Union a -> SymbolSet
go (Union a -> SymbolSet) -> Union a -> SymbolSet
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
    where
      go :: Union a -> SymbolSet
go (UnionSingle a
x) = a -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
x
      go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) = SymBool -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
cond SymbolSet -> SymbolSet -> SymbolSet
forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
t SymbolSet -> SymbolSet -> SymbolSet
forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
f

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

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

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

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

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

instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
  .|| :: UnionM a -> UnionM a -> UnionM a
(.||) = (a -> a -> a) -> UnionM a -> UnionM a -> UnionM a
forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.||)
  .&& :: UnionM a -> UnionM a -> UnionM a
(.&&) = (a -> a -> a) -> UnionM a -> UnionM a -> UnionM a
forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
(.&&)
  symNot :: UnionM a -> UnionM a
symNot = (a -> a) -> UnionM a -> UnionM a
forall a b.
(Mergeable a, Mergeable b) =>
(a -> b) -> UnionM a -> UnionM b
unionMUnaryOp a -> a
forall b. LogicalOp b => b -> b
symNot
  symXor :: UnionM a -> UnionM a -> UnionM a
symXor = (a -> a -> a) -> UnionM a -> UnionM a -> UnionM a
forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
symXor
  symImplies :: UnionM a -> UnionM a -> UnionM a
symImplies = (a -> a -> a) -> UnionM a -> UnionM a -> UnionM a
forall a b c.
(Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> UnionM a -> UnionM b -> UnionM c
unionMBinOp a -> a -> a
forall b. LogicalOp b => b -> b -> b
symImplies

instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
  con :: c -> UnionM t
con = t -> UnionM t
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (t -> UnionM t) -> (c -> t) -> c -> UnionM 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 -> UnionM t
sym = t -> UnionM t
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (t -> UnionM t) -> (Symbol -> t) -> Symbol -> UnionM 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 :: UnionM t -> Maybe c
conView UnionM t
v = do
    t
c <- UnionM t -> Maybe t
forall a. UnionM a -> Maybe a
forall (u :: * -> *) a. PlainUnion u => u a -> Maybe a
singleView (UnionM t -> Maybe t) -> UnionM t -> Maybe t
forall a b. (a -> b) -> a -> b
$ UnionM t -> UnionM t
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge UnionM 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 (UnionM f) arg (UnionM ret)
  where
  UnionM f
f # :: UnionM f -> arg -> UnionM ret
# arg
a = do
    f
f1 <- UnionM f
f
    ret -> UnionM ret
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (ret -> UnionM ret) -> ret -> UnionM 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 (UnionM a) where
  fromString :: String -> UnionM a
fromString = a -> UnionM a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> UnionM a) -> (String -> a) -> String -> UnionM 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 (UnionM a) where
  allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]
allSymsS = Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS (Union a -> [SomeSym] -> [SomeSym])
-> (UnionM a -> Union a) -> UnionM a -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion

-- 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 (UnionM (Maybe t))) where
  rootStrategy :: MergingStrategy (HashMap k (UnionM (Maybe t)))
rootStrategy = (SymBool
 -> HashMap k (UnionM (Maybe t))
 -> HashMap k (UnionM (Maybe t))
 -> HashMap k (UnionM (Maybe t)))
-> MergingStrategy (HashMap k (UnionM (Maybe t)))
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte

instance (IsConcrete k, Mergeable t) => SimpleMergeable (HML.HashMap k (UnionM (Maybe t))) where
  mrgIte :: SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
mrgIte SymBool
cond HashMap k (UnionM (Maybe t))
l HashMap k (UnionM (Maybe t))
r =
    (UnionM (Maybe t) -> UnionM (Maybe t) -> UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HML.unionWith (SymBool -> UnionM (Maybe t) -> UnionM (Maybe t) -> UnionM (Maybe t)
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond) HashMap k (UnionM (Maybe t))
ul HashMap k (UnionM (Maybe t))
ur
    where
      ul :: HashMap k (UnionM (Maybe t))
ul =
        (k -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)))
-> HashMap k (UnionM (Maybe t))
-> [k]
-> HashMap k (UnionM (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 (UnionM (Maybe t))
m -> case k -> HashMap k (UnionM (Maybe t)) -> Maybe (UnionM (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
              Maybe (UnionM (Maybe t))
Nothing -> k
-> UnionM (Maybe t)
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> UnionM (Maybe t)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
              Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
          )
          HashMap k (UnionM (Maybe t))
l
          (HashMap k (UnionM (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
r)
      ur :: HashMap k (UnionM (Maybe t))
ur =
        (k -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)))
-> HashMap k (UnionM (Maybe t))
-> [k]
-> HashMap k (UnionM (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 (UnionM (Maybe t))
m -> case k -> HashMap k (UnionM (Maybe t)) -> Maybe (UnionM (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
              Maybe (UnionM (Maybe t))
Nothing -> k
-> UnionM (Maybe t)
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> UnionM (Maybe t)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
              Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
          )
          HashMap k (UnionM (Maybe t))
r
          (HashMap k (UnionM (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
l)

instance UnionWithExcept (UnionM (Either e v)) UnionM e v where
  extractUnionExcept :: UnionM (Either e v) -> UnionM (Either e v)
extractUnionExcept = UnionM (Either e v) -> UnionM (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) :: UnionM Integer)
-- 2
-- >>> unionSize (choose [1..7] "a" :: UnionM Integer)
-- 7
unionSize :: UnionM a -> Int
unionSize :: forall a. UnionM a -> Int
unionSize = Union a -> Int
forall {a} {a}. Num a => Union a -> a
unionSize' (Union a -> Int) -> (UnionM a -> Union a) -> UnionM a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
  where
    unionSize' :: Union a -> a
unionSize' (UnionSingle a
_) = a
1
    unionSize' (UnionIf a
_ Bool
_ SymBool
_ Union a
l Union a
r) = Union a -> a
unionSize' Union a
l a -> a -> a
forall a. Num a => a -> a -> a
+ Union a -> a
unionSize' Union a
r