{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# HLINT ignore "Use <&>" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Grisette.Core.Control.Monad.UnionM
(
UnionM (..),
liftToMonadUnion,
underlyingUnion,
isMerged,
(.#),
IsConcrete,
unionSize,
)
where
import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), force, rnf1)
import Control.Parallel.Strategies (rpar, rseq, runEval)
import Data.Functor.Classes
( Eq1 (liftEq),
Show1 (liftShowsPrec),
showsPrec1,
)
import qualified Data.HashMap.Lazy as HML
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Core.Control.Monad.Class.MonadParallelUnion
( MonadParallelUnion (parBindUnion),
)
import Grisette.Core.Control.Monad.Union (MonadUnion)
import Grisette.Core.Data.BV (IntN, WordN)
import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
import Grisette.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.GPretty
( GPretty (gpretty),
groupedEnclose,
)
import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Core.Data.Class.LogicalOp
( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
)
import Grisette.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
Mergeable1 (liftRootStrategy),
MergingStrategy (SimpleStrategy),
)
import Grisette.Core.Data.Class.SEq (SEq ((.==)))
import Grisette.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
SimpleMergeable1 (liftMrgIte),
UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
UnionPrjOp (ifView, leftMost, singleView),
merge,
mrgIf,
mrgSingle,
simpleMerge,
(.#),
)
import Grisette.Core.Data.Class.Solvable
( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
pattern Con,
)
import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
import Grisette.Core.Data.Class.SubstituteSym (SubstituteSym (substituteSym))
import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Core.Data.Union
( Union (UnionIf, UnionSingle),
fullReconstruct,
ifWithStrategy,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( LinkedRep,
SupportedPrim,
type (-->),
)
import Grisette.IR.SymPrim.Data.SymPrim
( AllSyms (allSymsS),
SymBool,
SymIntN,
SymInteger,
SymWordN,
type (-~>),
type (=~>),
)
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
data UnionM a where
UAny ::
Union a ->
UnionM a
UMrg ::
MergingStrategy a ->
Union a ->
UnionM a
instance (NFData a) => NFData (UnionM a) where
rnf :: UnionM a -> ()
rnf = UnionM a -> ()
forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1
instance NFData1 UnionM where
liftRnf :: forall a. (a -> ()) -> UnionM a -> ()
liftRnf a -> ()
_a (UAny Union a
m) = (a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
liftRnf a -> ()
_a (UMrg MergingStrategy a
_ Union a
m) = (a -> ()) -> Union a -> ()
forall a. (a -> ()) -> Union a -> ()
forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
instance (Lift a) => Lift (UnionM a) where
liftTyped :: forall (m :: * -> *). Quote m => UnionM a -> Code m (UnionM a)
liftTyped (UAny Union a
v) = [||Union a -> UnionM a
forall a. Union a -> UnionM a
UAny Union a
v||]
liftTyped (UMrg MergingStrategy a
_ Union a
v) = [||Union a -> UnionM a
forall a. Union a -> UnionM a
UAny Union a
v||]
lift :: forall (m :: * -> *). Quote m => UnionM a -> m Exp
lift = Splice m (UnionM a) -> m Exp
forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice (Splice m (UnionM a) -> m Exp)
-> (UnionM a -> Splice m (UnionM a)) -> UnionM a -> m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Splice m (UnionM a)
forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
forall (m :: * -> *). Quote m => UnionM a -> Code m (UnionM a)
liftTyped
instance (Show a) => (Show (UnionM a)) where
showsPrec :: Int -> UnionM a -> ShowS
showsPrec = Int -> UnionM a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
liftShowsPrecUnion ::
forall a.
(Int -> a -> ShowS) ->
([a] -> ShowS) ->
Int ->
Union a ->
ShowS
liftShowsPrecUnion :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
_ Int
i (UnionSingle a
a) = Int -> a -> ShowS
sp Int
i a
a
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
Bool -> ShowS -> ShowS
showParen (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"If"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SymBool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
f
where
sp1 :: Int -> Union a -> ShowS
sp1 = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl
wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket Char
l Char
r ShowS
p = Char -> ShowS
showChar Char
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
r
instance Show1 UnionM where
liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> UnionM a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UAny Union a
a) =
Char -> Char -> ShowS -> ShowS
wrapBracket Char
'<' Char
'>'
(ShowS -> ShowS) -> (Union a -> ShowS) -> Union a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
(Union a -> ShowS) -> Union a -> ShowS
forall a b. (a -> b) -> a -> b
$ Union a
a
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UMrg MergingStrategy a
_ Union a
a) =
Char -> Char -> ShowS -> ShowS
wrapBracket Char
'{' Char
'}'
(ShowS -> ShowS) -> (Union a -> ShowS) -> Union a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
(Union a -> ShowS) -> Union a -> ShowS
forall a b. (a -> b) -> a -> b
$ Union a
a
instance (GPretty a) => GPretty (UnionM a) where
gpretty :: forall ann. UnionM a -> Doc ann
gpretty = \case
(UAny Union a
a) -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"<" Doc ann
">" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Union a -> Doc ann
forall a ann. GPretty a => a -> Doc ann
forall ann. Union a -> Doc ann
gpretty Union a
a
(UMrg MergingStrategy a
_ Union a
a) -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"{" Doc ann
"}" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Union a -> Doc ann
forall a ann. GPretty a => a -> Doc ann
forall ann. Union a -> Doc ann
gpretty Union a
a
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 #-}
isMerged :: UnionM a -> Bool
isMerged :: forall a. UnionM a -> Bool
isMerged UAny {} = Bool
False
isMerged UMrg {} = Bool
True
{-# INLINE isMerged #-}
instance UnionPrjOp UnionM where
singleView :: forall a. UnionM a -> Maybe a
singleView = Union a -> Maybe a
forall a. Union a -> Maybe a
forall (u :: * -> *) a. UnionPrjOp u => u a -> Maybe a
singleView (Union a -> Maybe a)
-> (UnionM a -> Union a) -> UnionM a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE singleView #-}
ifView :: forall a. UnionM a -> Maybe (SymBool, UnionM a, UnionM a)
ifView (UAny Union a
u) = case Union a -> Maybe (SymBool, Union a, Union a)
forall a. Union a -> Maybe (SymBool, Union a, Union a)
forall (u :: * -> *) a.
UnionPrjOp u =>
u a -> Maybe (SymBool, u a, u a)
ifView Union a
u of
Just (SymBool
c, Union a
t, Union a
f) -> (SymBool, UnionM a, UnionM a)
-> Maybe (SymBool, UnionM a, UnionM a)
forall a. a -> Maybe a
Just (SymBool
c, Union a -> UnionM a
forall a. Union a -> UnionM a
UAny Union a
t, Union a -> UnionM a
forall a. Union a -> UnionM a
UAny Union a
f)
Maybe (SymBool, Union a, Union a)
Nothing -> Maybe (SymBool, UnionM a, UnionM a)
forall a. Maybe a
Nothing
ifView (UMrg MergingStrategy a
m Union a
u) = case Union a -> Maybe (SymBool, Union a, Union a)
forall a. Union a -> Maybe (SymBool, Union a, Union a)
forall (u :: * -> *) a.
UnionPrjOp u =>
u a -> Maybe (SymBool, u a, u a)
ifView Union a
u of
Just (SymBool
c, Union a
t, Union a
f) -> (SymBool, UnionM a, UnionM a)
-> Maybe (SymBool, UnionM a, UnionM a)
forall a. a -> Maybe a
Just (SymBool
c, MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
t, MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
f)
Maybe (SymBool, Union a, Union a)
Nothing -> Maybe (SymBool, UnionM a, UnionM a)
forall a. Maybe a
Nothing
{-# INLINE ifView #-}
leftMost :: forall a. UnionM a -> a
leftMost = Union a -> a
forall a. Union a -> a
forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost (Union a -> a) -> (UnionM a -> Union a) -> UnionM a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE leftMost #-}
instance Functor UnionM where
fmap :: forall a b. (a -> b) -> UnionM a -> UnionM b
fmap a -> b
f UnionM a
fa = UnionM a
fa UnionM a -> (a -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> UnionM b
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> UnionM b) -> (a -> b) -> a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
{-# INLINE fmap #-}
instance Applicative UnionM where
pure :: forall a. a -> UnionM a
pure = a -> UnionM a
forall a. a -> UnionM a
forall (u :: * -> *) a. UnionLike u => a -> u a
single
{-# INLINE pure #-}
UnionM (a -> b)
f <*> :: forall a b. UnionM (a -> b) -> UnionM a -> UnionM b
<*> UnionM a
a = UnionM (a -> b)
f UnionM (a -> b) -> ((a -> b) -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a -> b
xf -> UnionM a
a UnionM a -> (a -> UnionM b) -> UnionM b
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (b -> UnionM b
forall a. a -> UnionM a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> UnionM b) -> (a -> b) -> a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
xf))
{-# INLINE (<*>) #-}
bindUnion :: Union a -> (a -> UnionM b) -> UnionM b
bindUnion :: forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (UnionSingle a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
bindUnion (UnionIf a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' =
SymBool -> UnionM b -> UnionM b -> UnionM b
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond (Union a -> (a -> UnionM b) -> UnionM b
forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion Union a
ifTrue a -> UnionM b
f') (Union a -> (a -> UnionM b) -> UnionM b
forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion Union a
ifFalse a -> UnionM b
f')
{-# INLINE bindUnion #-}
instance Monad UnionM where
UnionM a
a >>= :: forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
>>= a -> UnionM b
f = Union a -> (a -> UnionM b) -> UnionM b
forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) a -> UnionM b
f
{-# INLINE (>>=) #-}
parBindUnion'' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' (UnionSingle a
a) a -> UnionM b
f = UnionM b -> UnionM b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ a -> UnionM b
f a
a
parBindUnion'' Union a
u a -> UnionM b
f = Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
u a -> UnionM b
f
parBindUnion' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' (UnionSingle a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
parBindUnion' (UnionIf a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' = Eval (UnionM b) -> UnionM b
forall a. Eval a -> a
runEval (Eval (UnionM b) -> UnionM b) -> Eval (UnionM b) -> UnionM b
forall a b. (a -> b) -> a -> b
$ do
UnionM b
l <- Strategy (UnionM b)
forall a. Strategy a
rpar Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM b -> UnionM b
forall a. NFData a => a -> a
force (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifTrue a -> UnionM b
f'
UnionM b
r <- Strategy (UnionM b)
forall a. Strategy a
rpar Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM b -> UnionM b
forall a. NFData a => a -> a
force (UnionM b -> UnionM b) -> UnionM b -> UnionM b
forall a b. (a -> b) -> a -> b
$ Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifFalse a -> UnionM b
f'
UnionM b
l' <- Strategy (UnionM b)
forall a. Strategy a
rseq UnionM b
l
UnionM b
r' <- Strategy (UnionM b)
forall a. Strategy a
rseq UnionM b
r
Strategy (UnionM b)
forall a. Strategy a
rseq Strategy (UnionM b) -> Strategy (UnionM b)
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM b -> UnionM b -> UnionM b
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond UnionM b
l' UnionM b
r'
{-# INLINE parBindUnion' #-}
instance MonadParallelUnion UnionM where
parBindUnion :: forall b a.
(Mergeable b, NFData b) =>
UnionM a -> (a -> UnionM b) -> UnionM b
parBindUnion = Union a -> (a -> UnionM b) -> UnionM b
forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' (Union a -> (a -> UnionM b) -> UnionM b)
-> (UnionM a -> Union a) -> UnionM a -> (a -> UnionM b) -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE parBindUnion #-}
instance (Mergeable a) => Mergeable (UnionM a) where
rootStrategy :: MergingStrategy (UnionM a)
rootStrategy = (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a))
-> (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle
{-# INLINE rootStrategy #-}
instance (Mergeable a) => SimpleMergeable (UnionM a) where
mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a
mrgIte = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
{-# INLINE mrgIte #-}
instance Mergeable1 UnionM where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (UnionM a)
liftRootStrategy MergingStrategy a
m = (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a))
-> (SymBool -> UnionM a -> UnionM a -> UnionM a)
-> MergingStrategy (UnionM a)
forall a b. (a -> b) -> a -> b
$
\SymBool
cond UnionM a
t UnionM a
f -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (Union a -> UnionM a) -> (a -> Union a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Union a
forall a. a -> Union a
UnionSingle)
{-# INLINE liftRootStrategy #-}
instance SimpleMergeable1 UnionM where
liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> UnionM a -> UnionM a -> UnionM a
liftMrgIte SymBool -> a -> a -> a
m = MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall a.
MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
{-# INLINE liftMrgIte #-}
instance UnionLike UnionM where
mergeWithStrategy :: forall a. MergingStrategy a -> UnionM a -> UnionM a
mergeWithStrategy MergingStrategy a
_ m :: UnionM a
m@(UMrg MergingStrategy a
_ Union a
_) = UnionM a
m
mergeWithStrategy MergingStrategy a
s (UAny Union a
u) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
s (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> Union a -> Union a
forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
s Union a
u
{-# INLINE mergeWithStrategy #-}
mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
mrgIfWithStrategy MergingStrategy a
s (Con Bool
c) UnionM a
l UnionM a
r = if Bool
c then MergingStrategy a -> UnionM a -> UnionM a
forall a. MergingStrategy a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
l else MergingStrategy a -> UnionM a -> UnionM a
forall a. MergingStrategy a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
r
mrgIfWithStrategy MergingStrategy a
s SymBool
cond UnionM a
l UnionM a
r =
MergingStrategy a -> UnionM a -> UnionM a
forall a. MergingStrategy a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s (UnionM a -> UnionM a) -> UnionM a -> UnionM a
forall a b. (a -> b) -> a -> b
$ SymBool -> UnionM a -> UnionM a -> UnionM a
forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
l UnionM a
r
{-# INLINE mrgIfWithStrategy #-}
single :: forall a. a -> UnionM a
single = Union a -> UnionM a
forall a. Union a -> UnionM a
UAny (Union a -> UnionM a) -> (a -> Union a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Union a
forall a. a -> Union a
forall (u :: * -> *) a. UnionLike u => a -> u a
single
{-# INLINE single #-}
unionIf :: forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
unionIf SymBool
cond (UAny Union a
a) (UAny Union a
b) = Union a -> UnionM a
forall a. Union a -> UnionM a
UAny (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ SymBool -> Union a -> Union a -> Union a
forall a. SymBool -> Union a -> Union a -> Union a
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond Union a
a Union a
b
unionIf SymBool
cond (UMrg MergingStrategy a
m Union a
a) (UAny Union a
b) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
m SymBool
cond Union a
a Union a
b
unionIf SymBool
cond UnionM a
a (UMrg MergingStrategy a
m Union a
b) = MergingStrategy a -> Union a -> UnionM a
forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
m SymBool
cond (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) Union a
b
{-# INLINE unionIf #-}
instance (SEq a) => SEq (UnionM a) where
UnionM a
x .== :: UnionM a -> UnionM a -> SymBool
.== UnionM a
y = UnionM SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge (UnionM SymBool -> SymBool) -> UnionM SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
SymBool -> UnionM SymBool
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymBool -> UnionM SymBool) -> SymBool -> UnionM SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
y1
liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a
liftToMonadUnion :: forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
u = Union a -> u a
forall {u :: * -> *} {a}.
(UnionLike u, Mergeable a) =>
Union a -> u a
go (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
u)
where
go :: Union a -> u a
go (UnionSingle a
v) = a -> u a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c (Union a -> u a
go Union a
t) (Union a -> u a
go Union a
f)
instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where
toSym :: a -> UnionM b
toSym = b -> UnionM b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (b -> UnionM b) -> (a -> b) -> a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b. ToSym a b => a -> b
toSym
instance (ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) where
toSym :: UnionM a -> UnionM b
toSym = UnionM b -> UnionM b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM b -> UnionM b)
-> (UnionM a -> UnionM b) -> UnionM a -> UnionM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> UnionM a -> UnionM b
forall a b. (a -> b) -> UnionM a -> UnionM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
forall a b. ToSym a b => a -> b
toSym
#define TO_SYM_FROM_UNION_CON_SIMPLE(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (UnionM (contype n)) (symtype n) where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_FUN(conop, symop) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (conop ca cb)) (symop sa sb) where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_BV_SOME(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
toSym = simpleMerge . fmap (toSym :: contype -> symtype)
#if 1
TO_SYM_FROM_UNION_CON_SIMPLE(Bool, SymBool)
TO_SYM_FROM_UNION_CON_SIMPLE(Integer, SymInteger)
TO_SYM_FROM_UNION_CON_BV(IntN, SymIntN)
TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN)
TO_SYM_FROM_UNION_CON_FUN((=->), (=~>))
TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))
#endif
instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where
toCon :: UnionM a -> Maybe b
toCon UnionM a
v = Union a -> Maybe b
forall {a} {b}. ToCon a b => Union a -> Maybe b
go (Union a -> Maybe b) -> Union a -> Maybe b
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> Maybe b
go (UnionSingle a
x) = a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
x
go Union a
_ = Maybe b
forall a. Maybe a
Nothing
instance (ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) where
toCon :: UnionM a -> Maybe (UnionM b)
toCon UnionM a
v = Union a -> Maybe (UnionM b)
forall {a} {a} {u :: * -> *}.
(ToCon a a, UnionLike u, Mergeable a) =>
Union a -> Maybe (u a)
go (Union a -> Maybe (UnionM b)) -> Union a -> Maybe (UnionM b)
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> Maybe (u a)
go (UnionSingle a
x) = case a -> Maybe a
forall a b. ToCon a b => a -> Maybe b
toCon a
x of
Maybe a
Nothing -> Maybe (u a)
forall a. Maybe a
Nothing
Just a
v -> u a -> Maybe (u a)
forall a. a -> Maybe a
Just (u a -> Maybe (u a)) -> u a -> Maybe (u a)
forall a b. (a -> b) -> a -> b
$ a -> u a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
go (UnionIf a
_ Bool
_ SymBool
c Union a
t Union a
f) = do
u a
t' <- Union a -> Maybe (u a)
go Union a
t
u a
f' <- Union a -> Maybe (u a)
go Union a
f
u a -> Maybe (u a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (u a -> Maybe (u a)) -> u a -> Maybe (u a)
forall a b. (a -> b) -> a -> b
$ SymBool -> u a -> u a -> u a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c u a
t' u a
f'
instance (Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) where
evaluateSym :: Bool -> Model -> UnionM a -> UnionM a
evaluateSym Bool
fillDefault Model
model UnionM a
x = Union a -> UnionM a
go (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
where
go :: Union a -> UnionM a
go :: Union a -> UnionM a
go (UnionSingle a
v) = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model a
v
go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(Bool -> Model -> SymBool -> SymBool
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model SymBool
cond)
(Union a -> UnionM a
go Union a
t)
(Union a -> UnionM a
go Union a
f)
instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where
substituteSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> UnionM a -> UnionM a
substituteSym TypedSymbol cb
sym sb
val UnionM a
x = Union a -> UnionM a
go (Union a -> UnionM a) -> Union a -> UnionM a
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
where
go :: Union a -> UnionM a
go :: Union a -> UnionM a
go (UnionSingle a
v) = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substituteSym TypedSymbol cb
sym sb
val a
v
go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(TypedSymbol cb -> sb -> SymBool -> SymBool
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> SymBool -> SymBool
substituteSym TypedSymbol cb
sym sb
val SymBool
cond)
(Union a -> UnionM a
go Union a
t)
(Union a -> UnionM a
go Union a
f)
instance
(ExtractSymbolics a) =>
ExtractSymbolics (UnionM a)
where
extractSymbolics :: UnionM a -> SymbolSet
extractSymbolics UnionM a
v = Union a -> SymbolSet
forall {a}. ExtractSymbolics a => Union a -> SymbolSet
go (Union a -> SymbolSet) -> Union a -> SymbolSet
forall a b. (a -> b) -> a -> b
$ UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> SymbolSet
go (UnionSingle a
x) = a -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
x
go (UnionIf a
_ Bool
_ SymBool
cond Union a
t Union a
f) = SymBool -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
cond SymbolSet -> SymbolSet -> SymbolSet
forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
t SymbolSet -> SymbolSet -> SymbolSet
forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
f
instance (Hashable a) => Hashable (UnionM a) where
Int
s hashWithSalt :: Int -> UnionM a -> Int
`hashWithSalt` (UAny Union a
u) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) Int -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
u
Int
s `hashWithSalt` (UMrg MergingStrategy a
_ Union a
u) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> Union a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
u
instance (Eq a) => Eq (UnionM a) where
UAny Union a
l == :: UnionM a -> UnionM a -> Bool
== UAny Union a
r = Union a
l Union a -> Union a -> Bool
forall a. Eq a => a -> a -> Bool
== Union a
r
UMrg MergingStrategy a
_ Union a
l == UMrg MergingStrategy a
_ Union a
r = Union a
l Union a -> Union a -> Bool
forall a. Eq a => a -> a -> Bool
== Union a
r
UnionM a
_ == UnionM a
_ = Bool
False
instance Eq1 UnionM where
liftEq :: forall a b. (a -> b -> Bool) -> UnionM a -> UnionM b -> Bool
liftEq a -> b -> Bool
e UnionM a
l UnionM b
r = (a -> b -> Bool) -> Union a -> Union b -> Bool
forall a b. (a -> b -> Bool) -> Union a -> Union b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e (UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion UnionM a
l) (UnionM b -> Union b
forall a. UnionM a -> Union a
underlyingUnion UnionM b
r)
instance (Num a, Mergeable a) => Num (UnionM a) where
fromInteger :: Integer -> UnionM a
fromInteger = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (Integer -> a) -> Integer -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger
negate :: UnionM a -> UnionM a
negate UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Num a => a -> a
negate)
UnionM a
x + :: UnionM a -> UnionM a -> UnionM a
+ UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
y1
UnionM a
x - :: UnionM a -> UnionM a -> UnionM a
- UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
- a
y1
UnionM a
x * :: UnionM a -> UnionM a -> UnionM a
* UnionM a
y = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> a
forall a. Num a => a -> a -> a
* a
y1
abs :: UnionM a -> UnionM a
abs UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Num a => a -> a
abs
signum :: UnionM a -> UnionM a
signum UnionM a
x = UnionM a
x UnionM a -> (a -> UnionM a) -> UnionM a
forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (a -> a) -> a -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Num a => a -> a
signum
instance (ITEOp a, Mergeable a) => ITEOp (UnionM a) where
symIte :: SymBool -> UnionM a -> UnionM a -> UnionM a
symIte = SymBool -> UnionM a -> UnionM a -> UnionM a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
UnionM a
a .|| :: UnionM a -> UnionM a -> UnionM a
.|| UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
.|| a
b1
UnionM a
a .&& :: UnionM a -> UnionM a -> UnionM a
.&& UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
.&& a
b1
symNot :: UnionM a -> UnionM a
symNot UnionM a
x = do
a
x1 <- UnionM a
x
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a -> a
forall b. LogicalOp b => b -> b
symNot a
x1
symXor :: UnionM a -> UnionM a -> UnionM a
symXor UnionM a
a UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
`symXor` a
b1
symImplies :: UnionM a -> UnionM a -> UnionM a
symImplies UnionM a
a UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ a
a1 a -> a -> a
forall b. LogicalOp b => b -> b -> b
`symImplies` a
b1
instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
con :: c -> UnionM t
con = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> (c -> t) -> c -> UnionM t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> t
forall c t. Solvable c t => c -> t
con
{-# INLINE con #-}
ssym :: Text -> UnionM t
ssym = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> (Text -> t) -> Text -> UnionM t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> t
forall c t. Solvable c t => Text -> t
ssym
{-# INLINE ssym #-}
isym :: Text -> Int -> UnionM t
isym Text
i Int
s = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> Int -> t
forall c t. Solvable c t => Text -> Int -> t
isym Text
i Int
s
{-# INLINE isym #-}
sinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> UnionM t
sinfosym Text
s a
info = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
Text -> a -> t
sinfosym Text
s a
info
{-# INLINE sinfosym #-}
iinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> Int -> a -> UnionM t
iinfosym Text
i Int
s a
info = t -> UnionM t
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (t -> UnionM t) -> t -> UnionM t
forall a b. (a -> b) -> a -> b
$ Text -> Int -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> Int -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
Text -> Int -> a -> t
iinfosym Text
i Int
s a
info
{-# INLINE iinfosym #-}
conView :: UnionM t -> Maybe c
conView UnionM t
v = do
t
c <- UnionM t -> Maybe t
forall a. UnionM a -> Maybe a
forall (u :: * -> *) a. UnionPrjOp u => u a -> Maybe a
singleView UnionM t
v
t -> Maybe c
forall c t. Solvable c t => t -> Maybe c
conView t
c
{-# INLINE conView #-}
instance
(Function f, Mergeable f, Mergeable a, Ret f ~ a) =>
Function (UnionM f)
where
type Arg (UnionM f) = Arg f
type Ret (UnionM f) = UnionM (Ret f)
UnionM f
f # :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f)
# Arg (UnionM f)
a = do
f
f1 <- UnionM f
f
a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> a -> UnionM a
forall a b. (a -> b) -> a -> b
$ f
f1 f -> Arg f -> Ret f
forall f. Function f => f -> Arg f -> Ret f
# Arg f
Arg (UnionM f)
a
instance (IsString a, Mergeable a) => IsString (UnionM a) where
fromString :: String -> UnionM a
fromString = a -> UnionM a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> UnionM a) -> (String -> a) -> String -> UnionM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> a
forall a. IsString a => String -> a
fromString
instance (AllSyms a) => AllSyms (UnionM a) where
allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]
allSymsS = Union a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS (Union a -> [SomeSym] -> [SomeSym])
-> (UnionM a -> Union a) -> UnionM a -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
class (Eq t, Ord t, Hashable t) => IsConcrete t
instance IsConcrete Bool
instance IsConcrete Integer
instance (IsConcrete k, Mergeable t) => Mergeable (HML.HashMap k (UnionM (Maybe t))) where
rootStrategy :: MergingStrategy (HashMap k (UnionM (Maybe t)))
rootStrategy = (SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t)))
-> MergingStrategy (HashMap k (UnionM (Maybe t)))
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte
instance (IsConcrete k, Mergeable t) => SimpleMergeable (HML.HashMap k (UnionM (Maybe t))) where
mrgIte :: SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
mrgIte SymBool
cond HashMap k (UnionM (Maybe t))
l HashMap k (UnionM (Maybe t))
r =
(UnionM (Maybe t) -> UnionM (Maybe t) -> UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HML.unionWith (SymBool -> UnionM (Maybe t) -> UnionM (Maybe t) -> UnionM (Maybe t)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond) HashMap k (UnionM (Maybe t))
ul HashMap k (UnionM (Maybe t))
ur
where
ul :: HashMap k (UnionM (Maybe t))
ul =
(k -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)))
-> HashMap k (UnionM (Maybe t))
-> [k]
-> HashMap k (UnionM (Maybe t))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
( \k
k HashMap k (UnionM (Maybe t))
m -> case k -> HashMap k (UnionM (Maybe t)) -> Maybe (UnionM (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
Maybe (UnionM (Maybe t))
Nothing -> k
-> UnionM (Maybe t)
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> UnionM (Maybe t)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
)
HashMap k (UnionM (Maybe t))
l
(HashMap k (UnionM (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
r)
ur :: HashMap k (UnionM (Maybe t))
ur =
(k -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)))
-> HashMap k (UnionM (Maybe t))
-> [k]
-> HashMap k (UnionM (Maybe t))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
( \k
k HashMap k (UnionM (Maybe t))
m -> case k -> HashMap k (UnionM (Maybe t)) -> Maybe (UnionM (Maybe t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
Maybe (UnionM (Maybe t))
Nothing -> k
-> UnionM (Maybe t)
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (Maybe t -> UnionM (Maybe t)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Maybe t
forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
)
HashMap k (UnionM (Maybe t))
r
(HashMap k (UnionM (Maybe t)) -> [k]
forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
l)
instance UnionWithExcept (UnionM (Either e v)) UnionM e v where
extractUnionExcept :: UnionM (Either e v) -> UnionM (Either e v)
extractUnionExcept = UnionM (Either e v) -> UnionM (Either e v)
forall a. a -> a
id
unionSize :: UnionM a -> Int
unionSize :: forall a. UnionM a -> Int
unionSize = Union a -> Int
forall {a} {a}. Num a => Union a -> a
unionSize' (Union a -> Int) -> (UnionM a -> Union a) -> UnionM a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionM a -> Union a
forall a. UnionM a -> Union a
underlyingUnion
where
unionSize' :: Union a -> a
unionSize' (UnionSingle a
_) = a
1
unionSize' (UnionIf a
_ Bool
_ SymBool
_ Union a
l Union a
r) = Union a -> a
unionSize' Union a
l a -> a -> a
forall a. Num a => a -> a -> a
+ Union a -> a
unionSize' Union a
r