{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# HLINT ignore "Use <&>" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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
import Control.Monad.Identity (Identity (..))
import Control.Parallel.Strategies
import Data.Functor.Classes
import qualified Data.HashMap.Lazy as HML
import Data.Hashable
import Data.IORef
import Data.String
import GHC.IO hiding (evaluate)
import GHC.TypeNats
import Grisette.Core.Control.Monad.CBMCExcept
import Grisette.Core.Control.Monad.Class.MonadParallelUnion
import Grisette.Core.Control.Monad.Union
import Grisette.Core.Data.BV
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.Function
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.SOrd
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.Solver
import Grisette.Core.Data.Class.Substitute
import Grisette.Core.Data.Class.ToCon
import Grisette.Core.Data.Class.ToSym
import Grisette.Core.Data.Union
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.SymPrim
import Grisette.IR.SymPrim.Data.TabularFun
import Language.Haskell.TH.Syntax
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 = 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) = forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
  liftRnf a -> ()
_a (UMrg MergingStrategy a
_ Union a
m) = 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) = [||UAny v||]
  liftTyped (UMrg MergingStrategy a
_ Union a
v) = [||UAny v||]
  lift :: forall (m :: * -> *). Quote m => UnionM a -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped

instance (Show a) => (Show (UnionM a)) where
  showsPrec :: Int -> UnionM a -> ShowS
showsPrec = 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 (Single a
a) = Int -> a -> ShowS
sp Int
i a
a
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
  Bool -> ShowS -> ShowS
showParen (Int
i forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"If"
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
      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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
p 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
i (UAny Union a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'<' Char
'>'
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      forall a b. (a -> b) -> a -> b
$ Union a
a
  liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (UMrg MergingStrategy a
_ Union a
a) =
    Char -> Char -> ShowS -> ShowS
wrapBracket Char
'{' Char
'}'
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
      forall a b. (a -> b) -> a -> b
$ 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 = forall (u :: * -> *) a. UnionPrjOp u => u a -> Maybe a
singleView forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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) -> forall a. a -> Maybe a
Just (SymBool
c, forall a. Union a -> UnionM a
UAny Union a
t, forall a. Union a -> UnionM a
UAny Union a
f)
    Maybe (SymBool, Union a, Union a)
Nothing -> forall a. Maybe a
Nothing
  ifView (UMrg MergingStrategy a
m Union a
u) = case 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) -> forall a. a -> Maybe a
Just (SymBool
c, forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
t, forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
f)
    Maybe (SymBool, Union a, Union a)
Nothing -> forall a. Maybe a
Nothing
  {-# INLINE ifView #-}
  leftMost :: forall a. UnionM a -> a
leftMost = forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a -> b
xf -> UnionM a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. Monad m => a -> m a
return 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 (Single a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
bindUnion (If a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' =
  forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond (forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion Union a
ifTrue a -> UnionM b
f') (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 = forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (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'' (Single a
a) a -> UnionM b
f = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ a -> UnionM b
f a
a
parBindUnion'' Union a
u a -> UnionM b
f = 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' (Single a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
parBindUnion' (If a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' = forall a. Eval a -> a
runEval forall a b. (a -> b) -> a -> b
$ do
  UnionM b
l <- forall a. Strategy a
rpar forall a b. (a -> b) -> a -> b
$ forall a. NFData a => a -> a
force forall a b. (a -> b) -> a -> 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 <- forall a. Strategy a
rpar forall a b. (a -> b) -> a -> b
$ forall a. NFData a => a -> a
force forall a b. (a -> b) -> a -> 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' <- forall a. Strategy a
rseq UnionM b
l
  UnionM b
r' <- forall a. Strategy a
rseq UnionM b
r
  forall a. Strategy a
rseq forall a b. (a -> b) -> a -> 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 = forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
  {-# INLINE parBindUnion #-}

instance (Mergeable a) => Mergeable (UnionM a) where
  rootStrategy :: MergingStrategy (UnionM a)
rootStrategy = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 = 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 = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Union a
Single)
  {-# 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 = forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (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) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
s forall a b. (a -> b) -> a -> b
$ 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 forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
l else 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 =
    forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s forall a b. (a -> b) -> a -> b
$ 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 = forall a. Union a -> UnionM a
UAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. Union a -> UnionM a
UAny forall a b. (a -> b) -> a -> b
$ 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) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall a b. (a -> b) -> a -> b
$ 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) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
m SymBool
cond (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 = forall bool (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 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 = forall {u :: * -> *} {a}.
(UnionLike u, Mergeable a) =>
Union a -> u a
go (forall a. UnionM a -> Union a
underlyingUnion UnionM a
u)
  where
    go :: Union a -> u a
go (Single a
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
    go (If a
_ Bool
_ SymBool
c Union a
t Union a
f) = 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 (SOrd a) => SOrd (UnionM a) where
  UnionM a
x <=~ :: UnionM a -> UnionM a -> SymBool
<=~ UnionM a
y = forall bool (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
<=~ a
y1
  UnionM a
x <~ :: UnionM a -> UnionM a -> SymBool
<~ UnionM a
y = forall bool (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
<~ a
y1
  UnionM a
x >=~ :: UnionM a -> UnionM a -> SymBool
>=~ UnionM a
y = forall bool (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
>=~ a
y1
  UnionM a
x >~ :: UnionM a -> UnionM a -> SymBool
>~ UnionM a
y = forall bool (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
>~ a
y1
  UnionM a
x symCompare :: UnionM a -> UnionM a -> UnionM Ordering
`symCompare` UnionM a
y = forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    a
x1 forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` a
y1

instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where
  toSym :: a -> UnionM b
toSym = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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((-->), (-~>))
TO_SYM_FROM_UNION_CON_BV_SOME(SomeIntN, SomeSymIntN)
TO_SYM_FROM_UNION_CON_BV_SOME(SomeWordN, SomeSymWordN)
#endif

instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where
  toCon :: UnionM a -> Maybe b
toCon UnionM a
v = forall {a} {b}. ToCon a b => Union a -> Maybe b
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
    where
      go :: Union a -> Maybe b
go (Single a
x) = forall a b. ToCon a b => a -> Maybe b
toCon a
x
      go Union a
_ = 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 = forall {a} {a} {u :: * -> *}.
(ToCon a a, UnionLike u, Mergeable a) =>
Union a -> Maybe (u a)
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
    where
      go :: Union a -> Maybe (u a)
go (Single a
x) = case forall a b. ToCon a b => a -> Maybe b
toCon a
x of
        Maybe a
Nothing -> forall a. Maybe a
Nothing
        Just a
v -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
      go (If 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
    where
      go :: Union a -> UnionM a
      go :: Union a -> UnionM a
go (Single a
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model a
v
      go (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
        forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
          (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 sym val x = go $ underlyingUnion x
    where
      go :: Union a -> UnionM a
      go (Single v) = mrgSingle $ substituteSym sym val v
      go (If _ _ cond t f) =
        mrgIf
          (substituteSym sym val cond)
          (go t)
          (go f)
          -}

instance
  (ExtractSymbolics a) =>
  ExtractSymbolics (UnionM a)
  where
  extractSymbolics :: UnionM a -> SymbolSet
extractSymbolics UnionM a
v = forall {a}. ExtractSymbolics a => Union a -> SymbolSet
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
    where
      go :: Union a -> SymbolSet
go (Single a
x) = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
x
      go (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
cond forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
t 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 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
u
  Int
s `hashWithSalt` (UMrg MergingStrategy a
_ Union a
u) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: 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 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 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 = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e (forall a. UnionM a -> Union a
underlyingUnion UnionM a
l) (forall a. UnionM a -> Union a
underlyingUnion UnionM b
r)

instance (Num a, Mergeable a) => Num (UnionM a) where
  fromInteger :: Integer -> UnionM a
fromInteger = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger
  negate :: UnionM a -> UnionM a
negate UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate)
  UnionM a
x + :: UnionM a -> UnionM a -> UnionM a
+ UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
+ a
y1
  UnionM a
x - :: UnionM a -> UnionM a -> UnionM a
- UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
- a
y1
  UnionM a
x * :: UnionM a -> UnionM a -> UnionM a
* UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
* a
y1
  abs :: UnionM a -> UnionM a
abs UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs
  signum :: UnionM a -> UnionM a
signum UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
signum

instance (ITEOp a, Mergeable a) => ITEOp (UnionM a) where
  ites :: SymBool -> UnionM a -> UnionM a -> UnionM a
ites = 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
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 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
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
&&~ a
b1
  nots :: UnionM a -> UnionM a
nots UnionM a
x = do
    a
x1 <- UnionM a
x
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall b. LogicalOp b => b -> b
nots a
x1
  xors :: UnionM a -> UnionM a -> UnionM a
xors UnionM a
a UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
`xors` a
b1
  implies :: UnionM a -> UnionM a -> UnionM a
implies UnionM a
a UnionM a
b = do
    a
a1 <- UnionM a
a
    a
b1 <- UnionM a
b
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
`implies` a
b1

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

instance (IsString a, Mergeable a) => IsString (UnionM a) where
  fromString :: String -> UnionM a
fromString = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsString a => String -> a
fromString

-- GenSym
instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)

instance (GenSym spec a) => GenSymSimple spec (UnionM a) where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
simpleFresh spec
spec = do
    UnionM a
res <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
    if Bool -> Bool
not (forall a. UnionM a -> Bool
isMerged UnionM a
res) then forall a. HasCallStack => String -> a
error String
"Not merged" else forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
res

instance
  (GenSym a a, Mergeable a) =>
  GenSym (UnionM a) a
  where
  fresh :: forall (m :: * -> *). MonadFresh m => UnionM a -> m (UnionM a)
fresh UnionM a
spec = forall {spec} {a} {m :: * -> *}.
(GenSym spec a, MonadFresh m) =>
Union spec -> m (UnionM a)
go (forall a. UnionM a -> Union a
underlyingUnion forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge UnionM a
spec)
    where
      go :: Union spec -> m (UnionM a)
go (Single spec
x) = forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
x
      go (If spec
_ Bool
_ SymBool
_ Union spec
t Union spec
f) = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh () forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
f

-- AllSyms
instance AllSyms a => AllSyms (UnionM a) where
  allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]
allSymsS = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy 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 =
    forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HML.unionWith (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 =
        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          ( \k
k HashMap k (UnionM (Maybe t))
m -> case 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 -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle 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
          (forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
r)
      ur :: HashMap k (UnionM (Maybe t))
ur =
        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          ( \k
k HashMap k (UnionM (Maybe t))
m -> case 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 -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle 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
          (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 = forall a. a -> a
id

instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where
  extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v)
extractUnionExcept = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. CBMCEither a b -> Either a b
runCBMCEither

-- | 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 = forall {a} {a}. Num a => Union a -> a
unionSize' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
  where
    unionSize' :: Union a -> a
unionSize' (Single a
_) = a
1
    unionSize' (If a
_ Bool
_ SymBool
_ Union a
l Union a
r) = Union a -> a
unionSize' Union a
l forall a. Num a => a -> a -> a
+ Union a -> a
unionSize' Union a
r