{-# LANGUAGE BangPatterns #-}
{-# 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-cse #-}

{-# HLINT ignore "Use <&>" #-}

-- {-# 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,
  )
where

import Control.DeepSeq
import Control.Monad.Identity (Identity (..))
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 Grisette.Core.Control.Monad.CBMCExcept
import Grisette.Core.Control.Monad.Union
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 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 ::
    -- | (Possibly) cached merging result.
    IORef (Either (Union a) (UnionM a)) ->
    -- | 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 IORef (Either (Union a) (UnionM a))
i Union a
m) = IORef (Either (Union a) (UnionM a)) -> ()
forall a. NFData a => a -> ()
rnf IORef (Either (Union a) (UnionM a))
i () -> () -> ()
`seq` (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 (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 IORef (Either (Union a) (UnionM a))
_ Union a
v) = [||freshUAny v||]
  liftTyped (UMrg MergingStrategy a
_ Union a
v) = [||freshUAny 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
liftTyped

freshUAny :: Union a -> UnionM a
freshUAny :: forall a. Union a -> UnionM a
freshUAny Union a
v = IORef (Either (Union a) (UnionM a)) -> Union a -> UnionM a
forall a.
IORef (Either (Union a) (UnionM a)) -> Union a -> UnionM a
UAny (IO (IORef (Either (Union a) (UnionM a)))
-> IORef (Either (Union a) (UnionM a))
forall a. IO a -> a
unsafeDupablePerformIO (IO (IORef (Either (Union a) (UnionM a)))
 -> IORef (Either (Union a) (UnionM a)))
-> IO (IORef (Either (Union a) (UnionM a)))
-> IORef (Either (Union a) (UnionM a))
forall a b. (a -> b) -> a -> b
$ Either (Union a) (UnionM a)
-> IO (IORef (Either (Union a) (UnionM a)))
forall a. a -> IO (IORef a)
newIORef (Either (Union a) (UnionM a)
 -> IO (IORef (Either (Union a) (UnionM a))))
-> Either (Union a) (UnionM a)
-> IO (IORef (Either (Union a) (UnionM a)))
forall a b. (a -> b) -> a -> b
$ Union a -> Either (Union a) (UnionM a)
forall a b. a -> Either a b
Left Union a
v) Union a
v
{-# NOINLINE freshUAny #-}

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 (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 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
i (UAny IORef (Either (Union a) (UnionM 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
  liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (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

-- | Extract the underlying Union. May be unmerged.
underlyingUnion :: UnionM a -> Union a
underlyingUnion :: forall a. UnionM a -> Union a
underlyingUnion (UAny IORef (Either (Union a) (UnionM a))
_ 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 (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 IORef (Either (Union a) (UnionM a))
_ Union a
u) = case 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
freshUAny Union a
t, Union a -> UnionM a
forall a. Union a -> UnionM a
freshUAny 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 (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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> UnionM b
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 (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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (b -> UnionM b
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 (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' =
  SymBool -> UnionM b -> UnionM b -> UnionM b
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 (>>=) #-}

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 (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 (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 (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 (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
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 = 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 IORef (Either (Union a) (UnionM a))
ref Union a
u) = IO (UnionM a) -> UnionM a
forall a. IO a -> a
unsafeDupablePerformIO (IO (UnionM a) -> UnionM a) -> IO (UnionM a) -> UnionM a
forall a b. (a -> b) -> a -> b
$
    IORef (Either (Union a) (UnionM a))
-> (Either (Union a) (UnionM a)
    -> (Either (Union a) (UnionM a), UnionM a))
-> IO (UnionM a)
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Either (Union a) (UnionM a))
ref ((Either (Union a) (UnionM a)
  -> (Either (Union a) (UnionM a), UnionM a))
 -> IO (UnionM a))
-> (Either (Union a) (UnionM a)
    -> (Either (Union a) (UnionM a), UnionM a))
-> IO (UnionM a)
forall a b. (a -> b) -> a -> b
$ \case
      x :: Either (Union a) (UnionM a)
x@(Right UnionM a
r) -> (Either (Union a) (UnionM a)
x, UnionM a
r)
      Left Union a
_ -> (UnionM a -> Either (Union a) (UnionM a)
forall a b. b -> Either a b
Right UnionM a
r, UnionM a
r)
        where
          !r :: UnionM a
r = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
s (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
s Union a
u -- m >>= mrgSingle
  {-# NOINLINE 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 (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 (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 (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 (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
freshUAny (Union a -> UnionM a) -> (a -> Union a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 IORef (Either (Union a) (UnionM a))
_ Union a
a) (UAny IORef (Either (Union a) (UnionM a))
_ Union a
b) = Union a -> UnionM a
forall a. Union a -> UnionM a
freshUAny (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ 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 IORef (Either (Union a) (UnionM a))
_ 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 bool (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 (Single a
v) = a -> u a
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) = 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 (SOrd a) => SOrd (UnionM a) where
  UnionM a
x <=~ :: UnionM a -> UnionM a -> SymBool
<=~ UnionM a
y = UnionM SymBool -> SymBool
forall bool (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. SOrd a => a -> a -> SymBool
<=~ a
y1
  UnionM a
x <~ :: UnionM a -> UnionM a -> SymBool
<~ UnionM a
y = UnionM SymBool -> SymBool
forall bool (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. SOrd a => a -> a -> SymBool
<~ a
y1
  UnionM a
x >=~ :: UnionM a -> UnionM a -> SymBool
>=~ UnionM a
y = UnionM SymBool -> SymBool
forall bool (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. SOrd a => a -> a -> SymBool
>=~ a
y1
  UnionM a
x >~ :: UnionM a -> UnionM a -> SymBool
>~ UnionM a
y = UnionM SymBool -> SymBool
forall bool (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. SOrd a => a -> a -> SymBool
>~ a
y1
  UnionM a
x symCompare :: UnionM a -> UnionM a -> UnionM Ordering
`symCompare` UnionM a
y = UnionM Ordering -> UnionM Ordering
forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion (UnionM Ordering -> UnionM Ordering)
-> UnionM Ordering -> UnionM Ordering
forall a b. (a -> b) -> a -> b
$ do
    a
x1 <- UnionM a
x
    a
y1 <- UnionM a
y
    a
x1 a -> a -> UnionM Ordering
forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` a
y1

instance {-# OVERLAPPABLE #-} (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 {-# OVERLAPPING #-} (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
forall a b. ToSym a b => a -> b
toSym

instance {-# OVERLAPPABLE #-} (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 (Single 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 {-# OVERLAPPING #-} (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 (Single 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 (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
        u a -> Maybe (u 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 (Single 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 (If 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 b. TypedSymbol b -> Sym b -> UnionM a -> UnionM a
substituteSym TypedSymbol b
sym Sym b
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 (Single 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 b -> Sym b -> a -> a
forall a b. SubstituteSym a => TypedSymbol b -> Sym b -> a -> a
substituteSym TypedSymbol b
sym Sym b
val a
v
      go (If 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 b -> Sym b -> SymBool -> SymBool
forall a b. SubstituteSym a => TypedSymbol b -> Sym b -> a -> a
substituteSym TypedSymbol b
sym Sym b
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 (Single a
x) = a -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
x
      go (If 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 IORef (Either (Union a) (UnionM a))
_ 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 IORef (Either (Union a) (UnionM a))
_ Union a
l == :: UnionM a -> UnionM a -> Bool
== UAny IORef (Either (Union a) (UnionM a))
_ 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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
  ites :: SymBool -> UnionM a -> UnionM a -> UnionM a
ites = 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
  nots :: UnionM a -> UnionM a
nots 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
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
    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
`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
    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
`implies` 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 :: String -> UnionM t
ssym = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> (String -> t) -> String -> UnionM t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> t
forall c t. Solvable c t => String -> t
ssym
  {-# INLINE ssym #-}
  isym :: String -> Int -> UnionM t
isym String
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
$ String -> Int -> t
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 = 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
$ String -> a -> t
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 = 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
$ String -> Int -> a -> t
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 <- UnionM t -> Maybe t
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

{-
foldMapUnion :: (Monoid m) => (a -> m) -> Union a -> m
foldMapUnion f (Single v) = f v
foldMapUnion f (If _ _ _ l r) = foldMapUnion f l <> foldMapUnion f r

instance Foldable UnionM where
  foldMap f u = foldMapUnion f (underlyingUnion u)

sequenceAUnion :: (Applicative m, SymBoolOp bool) => Union (m a) -> m (Union a)
sequenceAUnion (Single v) = single <$> v
sequenceAUnion (If _ _ cond l r) = unionIf cond <$> sequenceAUnion l <*> sequenceAUnion r

instance  Traversable UnionM where
  sequenceA u = freshUAny <$> sequenceAUnion (underlyingUnion u)
  -}

-- 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 <- spec -> m (UnionM a)
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
    if Bool -> Bool
not (UnionM a -> Bool
forall a. UnionM a -> Bool
isMerged UnionM a
res) then String -> m (UnionM a)
forall a. HasCallStack => String -> a
error String
"Not merged" else UnionM a -> m (UnionM a)
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 = Union a -> m (UnionM a)
forall {spec} {a} {m :: * -> *}.
(GenSym spec a, MonadFresh m) =>
Union spec -> m (UnionM a)
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion (UnionM a -> Union a) -> UnionM a -> Union a
forall a b. (a -> b) -> a -> b
$ UnionM a -> UnionM a
forall (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) = spec -> m (UnionM a)
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) = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> m SymBool -> m (UnionM a -> UnionM a -> UnionM a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m SymBool
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh () m (UnionM a -> UnionM a -> UnionM a)
-> m (UnionM a) -> m (UnionM a -> UnionM a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
t m (UnionM a -> UnionM a) -> m (UnionM a) -> m (UnionM a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
f

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

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