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

-- {-# OPTIONS_GHC -fno-full-laziness #-}

-- |
-- Module      :   Grisette.Core.Control.Monad.UnionM
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Core.Control.Monad.UnionM
  ( -- * UnionM and helpers
    UnionM (..),
    liftToMonadUnion,
    underlyingUnion,
    isMerged,
    (.#),
    IsConcrete,
    unionSize,
  )
where

import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), force, rnf1)
import Control.Parallel.Strategies (rpar, rseq, runEval)
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.Core.Control.Monad.Class.MonadParallelUnion
  ( MonadParallelUnion (parBindUnion),
  )
import Grisette.Core.Control.Monad.Union (MonadUnion)
import Grisette.Core.Data.BV (IntN, WordN)
import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
import Grisette.Core.Data.Class.ExtractSymbolics
  ( ExtractSymbolics (extractSymbolics),
  )
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.GPretty
  ( GPretty (gpretty),
    groupedEnclose,
  )
import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Core.Data.Class.LogicalOp
  ( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
  )
import Grisette.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (SimpleStrategy),
  )
import Grisette.Core.Data.Class.SEq (SEq ((.==)))
import Grisette.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
    UnionPrjOp (ifView, leftMost, singleView),
    merge,
    mrgIf,
    mrgSingle,
    simpleMerge,
    (.#),
  )
import Grisette.Core.Data.Class.Solvable
  ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
    pattern Con,
  )
import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
import Grisette.Core.Data.Class.SubstituteSym (SubstituteSym (substituteSym))
import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Core.Data.Union
  ( Union (UnionIf, UnionSingle),
    fullReconstruct,
    ifWithStrategy,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( LinkedRep,
    SupportedPrim,
    type (-->),
  )
import Grisette.IR.SymPrim.Data.SymPrim
  ( AllSyms (allSymsS),
    SymBool,
    SymIntN,
    SymInteger,
    SymWordN,
    type (-~>),
    type (=~>),
  )
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
import Language.Haskell.TH.Syntax.Compat (unTypeSplice)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.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}
--
-- 'unionIf' cannot resolve the 'Mergeable' constraint.
--
-- >>> unionIf "a" (return 1) (unionIf "b" (return 1) (return 2)) :: UnionM Integer
-- <If a 1 (If b 1 2)>
--
-- But 'unionIf' is able to merge the result if some of the branches are merged:
--
-- >>> unionIf "a" (return 1) (unionIf "b" (mrgReturn 1) (return 2)) :: UnionM Integer
-- {If (|| a b) 1 2}
--
-- The '>>=' operator uses 'unionIf' internally. When the final statement in a do-block
-- merges the values, the system can then merge the final result.
--
-- >>> :{
--   do
--     x <- unionIf (ssym "a") (return 1) (unionIf (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 <- unionIf (ssym "a") (return 1) (unionIf (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 UnionPrjOp UnionM where
  singleView :: forall a. UnionM a -> Maybe a
singleView = Union a -> Maybe a
forall a. Union a -> Maybe a
forall (u :: * -> *) a. UnionPrjOp 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.
UnionPrjOp 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.
UnionPrjOp 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 #-}
  leftMost :: forall a. UnionM a -> a
leftMost = Union a -> a
forall a. Union a -> a
forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost (Union a -> a) -> (UnionM a -> Union a) -> UnionM a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
  {-# INLINE leftMost #-}

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 = a -> UnionM a
forall a. a -> UnionM a
forall (u :: * -> *) a. UnionLike u => a -> u a
single
  {-# 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. UnionLike u => SymBool -> u a -> u a -> u a
unionIf 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 (>>=) #-}

parBindUnion'' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' (UnionSingle a
a) a -> UnionM b
f = UnionM b -> UnionM b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ a -> UnionM b
f a
a
parBindUnion'' Union a
u a -> UnionM b
f = Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
u a -> UnionM b
f

parBindUnion' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' (UnionSingle a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
parBindUnion' (UnionIf a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' = Eval (UnionM b) -> UnionM b
forall a. Eval a -> a
runEval (Eval (UnionM b) -> UnionM b) -> Eval (UnionM b) -> UnionM b
forall a b. (a -> b) -> a -> b
$ do
  UnionM b
l <- Strategy (UnionM b)
forall a. Strategy a
rpar Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM b -> UnionM b
forall a. NFData a => a -> a
force (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifTrue a -> UnionM b
f'
  UnionM b
r <- Strategy (UnionM b)
forall a. Strategy a
rpar Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM b -> UnionM b
forall a. NFData a => a -> a
force (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifFalse a -> UnionM b
f'
  UnionM b
l' <- Strategy (UnionM b)
forall a. Strategy a
rseq UnionM b
l
  UnionM b
r' <- Strategy (UnionM b)
forall a. Strategy a
rseq UnionM b
r
  Strategy (UnionM b)
forall a. Strategy a
rseq Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM b -> UnionM b -> UnionM b
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond UnionM b
l' UnionM b
r'
{-# INLINE parBindUnion' #-}

instance MonadParallelUnion UnionM where
  parBindUnion :: forall b a.
(Mergeable b, NFData b) =>
UnionM a -> (a -> UnionM b) -> UnionM b
parBindUnion = Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' (Union a -> (a -> UnionM b) -> UnionM b)
-> (UnionM a -> Union a) -> UnionM a -> (a -> UnionM b) -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
  {-# INLINE parBindUnion #-}

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)
 -> MergingStrategy (UnionM a))
-> (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle
  {-# 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.
(UnionLike 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
$
    \SymBool
cond UnionM a
t UnionM a
f -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (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
UnionSingle)
  {-# 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.
UnionLike 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 UnionLike UnionM where
  mergeWithStrategy :: forall a. MergingStrategy a -> UnionM a -> UnionM a
mergeWithStrategy MergingStrategy a
_ m :: UnionM a
m@(UMrg MergingStrategy a
_ Union a
_) = UnionM a
m
  mergeWithStrategy 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
fullReconstruct MergingStrategy a
s Union a
u
  {-# INLINE mergeWithStrategy #-}
  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 (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
l else MergingStrategy a -> UnionM a -> UnionM a
forall a. MergingStrategy a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
r
  mrgIfWithStrategy MergingStrategy a
s SymBool
cond UnionM a
l UnionM a
r =
    MergingStrategy a -> UnionM a -> UnionM a
forall a. MergingStrategy a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s (UnionM a -> UnionM a) -> UnionM a -> UnionM a
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
l UnionM a
r
  {-# INLINE mrgIfWithStrategy #-}
  single :: forall a. a -> UnionM a
single = 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 (u :: * -> *) a. UnionLike u => a -> u a
single
  {-# INLINE single #-}
  unionIf :: forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
unionIf SymBool
cond (UAny Union a
a) (UAny Union a
b) = 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
$ SymBool -> Union a -> Union a -> Union a
forall a. SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond Union a
a Union a
b
  unionIf SymBool
cond (UMrg MergingStrategy a
m Union a
a) (UAny Union a
b) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (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
ifWithStrategy MergingStrategy a
m SymBool
cond Union a
a Union a
b
  unionIf SymBool
cond UnionM a
a (UMrg MergingStrategy a
m Union a
b) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (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
ifWithStrategy MergingStrategy a
m SymBool
cond (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) Union a
b
  {-# INLINE unionIf #-}

instance (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, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge (UnionM SymBool -> SymBool) -> UnionM SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    SymBool -> UnionM SymBool
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymBool -> UnionM SymBool) -> SymBool -> UnionM SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
y1

-- | Lift the 'UnionM' to any 'MonadUnion'.
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 = Union a -> u a
forall {u :: * -> *} {a}.
(UnionLike u, Mergeable a) =>
Union a -> u a
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
u)
  where
    go :: Union a -> u a
go (UnionSingle a
v) = a -> u a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
    go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c (Union a -> u a
go Union a
t) (Union a -> u a
go Union a
f)

instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where
  toSym :: a -> UnionM b
toSym = b -> UnionM b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (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 ca, SupportedPrim 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) => 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
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 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} {u :: * -> *}.
(ToCon a a, UnionLike u, Mergeable a) =>
Union a -> Maybe (u 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
v
    where
      go :: Union a -> Maybe (u 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 (u a)
forall a. Maybe a
Nothing
        Just a
v -> u a -> Maybe (u a)
forall a. a -> Maybe a
Just (u a -> Maybe (u a)) -> u a -> Maybe (u a)
forall a b. (a -> b) -> a -> b
$ a -> u a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
      go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = do
        u a
t' <- Union a -> Maybe (u a)
go Union a
t
        u a
f' <- Union a -> Maybe (u a)
go Union a
f
        u a -> Maybe (u a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (u a -> Maybe (u a)) -> u a -> Maybe (u a)
forall a b. (a -> b) -> a -> b
$ SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c u a
t' u 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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.
(UnionLike 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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.
(UnionLike 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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 UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Num a => a -> a
negate)
  UnionM a
x + :: UnionM a -> UnionM a -> UnionM a
+ UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
y1
  UnionM a
x - :: UnionM a -> UnionM a -> UnionM a
- UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
- a
y1
  UnionM a
x * :: UnionM a -> UnionM a -> UnionM a
* UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
* a
y1
  abs :: UnionM a -> UnionM a
abs UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Num a => a -> a
abs
  signum :: UnionM a -> UnionM a
signum UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf

instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
  UnionM a
a .|| :: UnionM a -> UnionM a -> UnionM a
.|| UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
.|| a
b1
  UnionM a
a .&& :: UnionM a -> UnionM a -> UnionM a
.&& UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
.&& a
b1
  symNot :: UnionM a -> UnionM a
symNot UnionM a
x = do
    a
x1 <- UnionM a
x
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a -> a
forall b. LogicalOp b => b -> b
symNot a
x1
  symXor :: UnionM a -> UnionM a -> UnionM a
symXor UnionM a
a UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
`symXor` a
b1
  symImplies :: UnionM a -> UnionM a -> UnionM a
symImplies UnionM a
a UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
`symImplies` a
b1

instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
  con :: c -> UnionM t
con = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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 #-}
  ssym :: Text -> UnionM t
ssym = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> (Text -> t) -> Text -> UnionM t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> t
forall c t. Solvable c t => Text -> t
ssym
  {-# INLINE ssym #-}
  isym :: Text -> Int -> UnionM t
isym Text
i Int
s = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> Int -> t
forall c t. Solvable c t => Text -> Int -> t
isym Text
i Int
s
  {-# INLINE isym #-}
  sinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> UnionM t
sinfosym Text
s a
info = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
Text -> a -> t
sinfosym Text
s a
info
  {-# INLINE sinfosym #-}
  iinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> Int -> a -> UnionM t
iinfosym Text
i Int
s a
info = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> Int -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> Int -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
Text -> Int -> a -> t
iinfosym Text
i Int
s a
info
  {-# INLINE iinfosym #-}
  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. UnionPrjOp u => u a -> Maybe a
singleView UnionM t
v
    t -> Maybe c
forall c t. Solvable c t => t -> Maybe c
conView t
c
  {-# INLINE conView #-}

instance
  (Function f, Mergeable f, Mergeable a, Ret f ~ a) =>
  Function (UnionM f)
  where
  type Arg (UnionM f) = Arg f
  type Ret (UnionM f) = UnionM (Ret f)
  UnionM f
f # :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f)
# Arg (UnionM f)
a = do
    f
f1 <- UnionM f
f
    a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ f
f1 f -> Arg f -> Ret f
forall f. Function f => f -> Arg f -> Ret f
# Arg f
Arg (UnionM f)
a

instance (IsString a, Mergeable a) => IsString (UnionM a) where
  fromString :: String -> UnionM a
fromString = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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, Hashable 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.
(UnionLike 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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 (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u 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 (single True)
-- 1
-- >>> unionSize (mrgIf "a" (single 1) (single 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