{-# 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.CBMCExcept
( CBMCEither (runCBMCEither),
)
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.Bool
( ITEOp (ites),
LogicalOp (implies, nots, xors, (&&~), (||~)),
SEq ((==~)),
)
import Grisette.Core.Data.Class.Evaluate (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.GenSym
( GenSym (fresh),
GenSymSimple (simpleFresh),
)
import Grisette.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
Mergeable1 (liftRootStrategy),
MergingStrategy (SimpleStrategy),
)
import Grisette.Core.Data.Class.SOrd
( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
)
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.ToCon (ToCon (toCon))
import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Core.Data.Union
( Union (If, Single),
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 = forall (f :: * -> *) a. (NFData1 f, NFData a) => f a -> ()
rnf1
instance NFData1 UnionM where
liftRnf :: forall a. (a -> ()) -> UnionM a -> ()
liftRnf a -> ()
_a (UAny Union a
m) = forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
liftRnf a -> ()
_a (UMrg MergingStrategy a
_ Union a
m) = forall (f :: * -> *) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf a -> ()
_a Union a
m
instance (Lift a) => Lift (UnionM a) where
liftTyped :: forall (m :: * -> *). Quote m => UnionM a -> Code m (UnionM a)
liftTyped (UAny Union a
v) = [||UAny v||]
liftTyped (UMrg MergingStrategy a
_ Union a
v) = [||UAny v||]
lift :: forall (m :: * -> *). Quote m => UnionM a -> m Exp
lift = forall a (m :: * -> *). Quote m => Splice m a -> m Exp
unTypeSplice forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
liftTyped
instance (Show a) => (Show (UnionM a)) where
showsPrec :: Int -> UnionM a -> ShowS
showsPrec = forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
liftShowsPrecUnion ::
forall a.
(Int -> a -> ShowS) ->
([a] -> ShowS) ->
Int ->
Union a ->
ShowS
liftShowsPrecUnion :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
_ Int
i (Single a
a) = Int -> a -> ShowS
sp Int
i a
a
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
i (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
Bool -> ShowS -> ShowS
showParen (Int
i forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"If"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SymBool
cond
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Union a -> ShowS
sp1 Int
11 Union a
f
where
sp1 :: Int -> Union a -> ShowS
sp1 = forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl
wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket :: Char -> Char -> ShowS -> ShowS
wrapBracket Char
l Char
r ShowS
p = Char -> ShowS
showChar Char
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
r
instance Show1 UnionM where
liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> UnionM a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UAny Union a
a) =
Char -> Char -> ShowS -> ShowS
wrapBracket Char
'<' Char
'>'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
forall a b. (a -> b) -> a -> b
$ Union a
a
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
_ (UMrg MergingStrategy a
_ Union a
a) =
Char -> Char -> ShowS -> ShowS
wrapBracket Char
'{' Char
'}'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS
liftShowsPrecUnion Int -> a -> ShowS
sp [a] -> ShowS
sl Int
0
forall a b. (a -> b) -> a -> b
$ Union a
a
instance (GPretty a) => GPretty (UnionM a) where
gpretty :: forall ann. UnionM a -> Doc ann
gpretty = \case
(UAny Union a
a) -> forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"<" Doc ann
">" forall a b. (a -> b) -> a -> b
$ forall a ann. GPretty a => a -> Doc ann
gpretty Union a
a
(UMrg MergingStrategy a
_ Union a
a) -> forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
groupedEnclose Doc ann
"{" Doc ann
"}" forall a b. (a -> b) -> a -> b
$ forall a ann. GPretty a => 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 = forall (u :: * -> *) a. UnionPrjOp u => u a -> Maybe a
singleView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE singleView #-}
ifView :: forall a. UnionM a -> Maybe (SymBool, UnionM a, UnionM a)
ifView (UAny Union a
u) = case forall (u :: * -> *) a.
UnionPrjOp u =>
u a -> Maybe (SymBool, u a, u a)
ifView Union a
u of
Just (SymBool
c, Union a
t, Union a
f) -> forall a. a -> Maybe a
Just (SymBool
c, forall a. Union a -> UnionM a
UAny Union a
t, forall a. Union a -> UnionM a
UAny Union a
f)
Maybe (SymBool, Union a, Union a)
Nothing -> forall a. Maybe a
Nothing
ifView (UMrg MergingStrategy a
m Union a
u) = case forall (u :: * -> *) a.
UnionPrjOp u =>
u a -> Maybe (SymBool, u a, u a)
ifView Union a
u of
Just (SymBool
c, Union a
t, Union a
f) -> forall a. a -> Maybe a
Just (SymBool
c, forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
t, forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m Union a
f)
Maybe (SymBool, Union a, Union a)
Nothing -> forall a. Maybe a
Nothing
{-# INLINE ifView #-}
leftMost :: forall a. UnionM a -> a
leftMost = forall (u :: * -> *) a. UnionPrjOp u => u a -> a
leftMost forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE leftMost #-}
instance Functor UnionM where
fmap :: forall a b. (a -> b) -> UnionM a -> UnionM b
fmap a -> b
f UnionM a
fa = UnionM a
fa forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
{-# INLINE fmap #-}
instance Applicative UnionM where
pure :: forall a. a -> UnionM a
pure = forall (u :: * -> *) a. UnionLike u => a -> u a
single
{-# INLINE pure #-}
UnionM (a -> b)
f <*> :: forall a b. UnionM (a -> b) -> UnionM a -> UnionM b
<*> UnionM a
a = UnionM (a -> b)
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a -> b
xf -> UnionM a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
xf))
{-# INLINE (<*>) #-}
bindUnion :: Union a -> (a -> UnionM b) -> UnionM b
bindUnion :: forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (Single a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
bindUnion (If a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' =
forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond (forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion Union a
ifTrue a -> UnionM b
f') (forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion Union a
ifFalse a -> UnionM b
f')
{-# INLINE bindUnion #-}
instance Monad UnionM where
UnionM a
a >>= :: forall a b. UnionM a -> (a -> UnionM b) -> UnionM b
>>= a -> UnionM b
f = forall a b. Union a -> (a -> UnionM b) -> UnionM b
bindUnion (forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) a -> UnionM b
f
{-# INLINE (>>=) #-}
parBindUnion'' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' (Single a
a) a -> UnionM b
f = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ a -> UnionM b
f a
a
parBindUnion'' Union a
u a -> UnionM b
f = forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
u a -> UnionM b
f
parBindUnion' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' :: forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' (Single a
a') a -> UnionM b
f' = a -> UnionM b
f' a
a'
parBindUnion' (If a
_ Bool
_ SymBool
cond Union a
ifTrue Union a
ifFalse) a -> UnionM b
f' = forall a. Eval a -> a
runEval forall a b. (a -> b) -> a -> b
$ do
UnionM b
l <- forall a. Strategy a
rpar forall a b. (a -> b) -> a -> b
$ forall a. NFData a => a -> a
force forall a b. (a -> b) -> a -> b
$ forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifTrue a -> UnionM b
f'
UnionM b
r <- forall a. Strategy a
rpar forall a b. (a -> b) -> a -> b
$ forall a. NFData a => a -> a
force forall a b. (a -> b) -> a -> b
$ forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion' Union a
ifFalse a -> UnionM b
f'
UnionM b
l' <- forall a. Strategy a
rseq UnionM b
l
UnionM b
r' <- forall a. Strategy a
rseq UnionM b
r
forall a. Strategy a
rseq forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond UnionM b
l' UnionM b
r'
{-# INLINE parBindUnion' #-}
instance MonadParallelUnion UnionM where
parBindUnion :: forall b a.
(Mergeable b, NFData b) =>
UnionM a -> (a -> UnionM b) -> UnionM b
parBindUnion = forall b a.
(Mergeable b, NFData b) =>
Union a -> (a -> UnionM b) -> UnionM b
parBindUnion'' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
{-# INLINE parBindUnion #-}
instance (Mergeable a) => Mergeable (UnionM a) where
rootStrategy :: MergingStrategy (UnionM a)
rootStrategy = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle
{-# INLINE rootStrategy #-}
instance (Mergeable a) => SimpleMergeable (UnionM a) where
mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a
mrgIte = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
{-# INLINE mrgIte #-}
instance Mergeable1 UnionM where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (UnionM a)
liftRootStrategy MergingStrategy a
m = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$ \SymBool
cond UnionM a
t UnionM a
f -> forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
t UnionM a
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Union a
Single)
{-# INLINE liftRootStrategy #-}
instance SimpleMergeable1 UnionM where
liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool -> UnionM a -> UnionM a -> UnionM a
liftMrgIte SymBool -> a -> a -> a
m = forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
{-# INLINE liftMrgIte #-}
instance UnionLike UnionM where
mergeWithStrategy :: forall a. MergingStrategy a -> UnionM a -> UnionM a
mergeWithStrategy MergingStrategy a
_ m :: UnionM a
m@(UMrg MergingStrategy a
_ Union a
_) = UnionM a
m
mergeWithStrategy MergingStrategy a
s (UAny Union a
u) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
s forall a b. (a -> b) -> a -> b
$ forall a. MergingStrategy a -> Union a -> Union a
fullReconstruct MergingStrategy a
s Union a
u
{-# INLINE mergeWithStrategy #-}
mrgIfWithStrategy :: forall a.
MergingStrategy a -> SymBool -> UnionM a -> UnionM a -> UnionM a
mrgIfWithStrategy MergingStrategy a
s (Con Bool
c) UnionM a
l UnionM a
r = if Bool
c then forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
l else forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s UnionM a
r
mrgIfWithStrategy MergingStrategy a
s SymBool
cond UnionM a
l UnionM a
r =
forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy MergingStrategy a
s forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond UnionM a
l UnionM a
r
{-# INLINE mrgIfWithStrategy #-}
single :: forall a. a -> UnionM a
single = forall a. Union a -> UnionM a
UAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: * -> *) a. UnionLike u => a -> u a
single
{-# INLINE single #-}
unionIf :: forall a. SymBool -> UnionM a -> UnionM a -> UnionM a
unionIf SymBool
cond (UAny Union a
a) (UAny Union a
b) = forall a. Union a -> UnionM a
UAny forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond Union a
a Union a
b
unionIf SymBool
cond (UMrg MergingStrategy a
m Union a
a) (UAny Union a
b) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
m SymBool
cond Union a
a Union a
b
unionIf SymBool
cond UnionM a
a (UMrg MergingStrategy a
m Union a
b) = forall a. MergingStrategy a -> Union a -> UnionM a
UMrg MergingStrategy a
m forall a b. (a -> b) -> a -> b
$ forall a.
MergingStrategy a -> SymBool -> Union a -> Union a -> Union a
ifWithStrategy MergingStrategy a
m SymBool
cond (forall a. UnionM a -> Union a
underlyingUnion UnionM a
a) Union a
b
{-# INLINE unionIf #-}
instance (SEq a) => SEq (UnionM a) where
UnionM a
x ==~ :: UnionM a -> UnionM a -> SymBool
==~ UnionM a
y = forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SEq a => a -> a -> SymBool
==~ a
y1
liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a
liftToMonadUnion :: forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
u = forall {u :: * -> *} {a}.
(UnionLike u, Mergeable a) =>
Union a -> u a
go (forall a. UnionM a -> Union a
underlyingUnion UnionM a
u)
where
go :: Union a -> u a
go (Single a
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
go (If a
_ Bool
_ SymBool
c Union a
t Union a
f) = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c (Union a -> u a
go Union a
t) (Union a -> u a
go Union a
f)
instance (SOrd a) => SOrd (UnionM a) where
UnionM a
x <=~ :: UnionM a -> UnionM a -> SymBool
<=~ UnionM a
y = forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
<=~ a
y1
UnionM a
x <~ :: UnionM a -> UnionM a -> SymBool
<~ UnionM a
y = forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
<~ a
y1
UnionM a
x >=~ :: UnionM a -> UnionM a -> SymBool
>=~ UnionM a
y = forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
>=~ a
y1
UnionM a
x >~ :: UnionM a -> UnionM a -> SymBool
>~ UnionM a
y = forall (u :: * -> *) a.
(SimpleMergeable a, UnionLike u, UnionPrjOp u) =>
u a -> a
simpleMerge forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. SOrd a => a -> a -> SymBool
>~ a
y1
UnionM a
x symCompare :: UnionM a -> UnionM a -> UnionM Ordering
`symCompare` UnionM a
y = forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion forall a b. (a -> b) -> a -> b
$ do
a
x1 <- UnionM a
x
a
y1 <- UnionM a
y
a
x1 forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` a
y1
instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where
toSym :: a -> UnionM b
toSym = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. ToSym a b => a -> b
toSym
instance (ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) where
toSym :: UnionM a -> UnionM b
toSym = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. ToSym a b => a -> b
toSym
#define TO_SYM_FROM_UNION_CON_SIMPLE(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (UnionM (contype n)) (symtype n) where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_FUN(conop, symop) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (conop ca cb)) (symop sa sb) where \
toSym = simpleMerge . fmap con
#define TO_SYM_FROM_UNION_CON_BV_SOME(contype, symtype) \
instance ToSym (UnionM contype) symtype where \
toSym = simpleMerge . fmap (toSym :: contype -> symtype)
#if 1
TO_SYM_FROM_UNION_CON_SIMPLE(Bool, SymBool)
TO_SYM_FROM_UNION_CON_SIMPLE(Integer, SymInteger)
TO_SYM_FROM_UNION_CON_BV(IntN, SymIntN)
TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN)
TO_SYM_FROM_UNION_CON_FUN((=->), (=~>))
TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))
#endif
instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where
toCon :: UnionM a -> Maybe b
toCon UnionM a
v = forall {a} {b}. ToCon a b => Union a -> Maybe b
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> Maybe b
go (Single a
x) = forall a b. ToCon a b => a -> Maybe b
toCon a
x
go Union a
_ = forall a. Maybe a
Nothing
instance (ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) where
toCon :: UnionM a -> Maybe (UnionM b)
toCon UnionM a
v = forall {a} {a} {u :: * -> *}.
(ToCon a a, UnionLike u, Mergeable a) =>
Union a -> Maybe (u a)
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> Maybe (u a)
go (Single a
x) = case forall a b. ToCon a b => a -> Maybe b
toCon a
x of
Maybe a
Nothing -> forall a. Maybe a
Nothing
Just a
v -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v
go (If a
_ Bool
_ SymBool
c Union a
t Union a
f) = do
u a
t' <- Union a -> Maybe (u a)
go Union a
t
u a
f' <- Union a -> Maybe (u a)
go Union a
f
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
c u a
t' u a
f'
instance (Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) where
evaluateSym :: Bool -> Model -> UnionM a -> UnionM a
evaluateSym Bool
fillDefault Model
model UnionM a
x = Union a -> UnionM a
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
x
where
go :: Union a -> UnionM a
go :: Union a -> UnionM a
go (Single a
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model a
v
go (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model SymBool
cond)
(Union a -> UnionM a
go Union a
t)
(Union a -> UnionM a
go Union a
f)
instance
(ExtractSymbolics a) =>
ExtractSymbolics (UnionM a)
where
extractSymbolics :: UnionM a -> SymbolSet
extractSymbolics UnionM a
v = forall {a}. ExtractSymbolics a => Union a -> SymbolSet
go forall a b. (a -> b) -> a -> b
$ forall a. UnionM a -> Union a
underlyingUnion UnionM a
v
where
go :: Union a -> SymbolSet
go (Single a
x) = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
x
go (If a
_ Bool
_ SymBool
cond Union a
t Union a
f) = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics SymBool
cond forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
t forall a. Semigroup a => a -> a -> a
<> Union a -> SymbolSet
go Union a
f
instance (Hashable a) => Hashable (UnionM a) where
Int
s hashWithSalt :: Int -> UnionM a -> Int
`hashWithSalt` (UAny Union a
u) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
u
Int
s `hashWithSalt` (UMrg MergingStrategy a
_ Union a
u) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Union a
u
instance (Eq a) => Eq (UnionM a) where
UAny Union a
l == :: UnionM a -> UnionM a -> Bool
== UAny Union a
r = Union a
l forall a. Eq a => a -> a -> Bool
== Union a
r
UMrg MergingStrategy a
_ Union a
l == UMrg MergingStrategy a
_ Union a
r = Union a
l forall a. Eq a => a -> a -> Bool
== Union a
r
UnionM a
_ == UnionM a
_ = Bool
False
instance Eq1 UnionM where
liftEq :: forall a b. (a -> b -> Bool) -> UnionM a -> UnionM b -> Bool
liftEq a -> b -> Bool
e UnionM a
l UnionM b
r = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
e (forall a. UnionM a -> Union a
underlyingUnion UnionM a
l) (forall a. UnionM a -> Union a
underlyingUnion UnionM b
r)
instance (Num a, Mergeable a) => Num (UnionM a) where
fromInteger :: Integer -> UnionM a
fromInteger = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger
negate :: UnionM a -> UnionM a
negate UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate)
UnionM a
x + :: UnionM a -> UnionM a -> UnionM a
+ UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
+ a
y1
UnionM a
x - :: UnionM a -> UnionM a -> UnionM a
- UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
- a
y1
UnionM a
x * :: UnionM a -> UnionM a -> UnionM a
* UnionM a
y = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x1 -> UnionM a
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y1 -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
x1 forall a. Num a => a -> a -> a
* a
y1
abs :: UnionM a -> UnionM a
abs UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs
signum :: UnionM a -> UnionM a
signum UnionM a
x = UnionM a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
signum
instance (ITEOp a, Mergeable a) => ITEOp (UnionM a) where
ites :: SymBool -> UnionM a -> UnionM a -> UnionM a
ites = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where
UnionM a
a ||~ :: UnionM a -> UnionM a -> UnionM a
||~ UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
||~ a
b1
UnionM a
a &&~ :: UnionM a -> UnionM a -> UnionM a
&&~ UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
&&~ a
b1
nots :: UnionM a -> UnionM a
nots UnionM a
x = do
a
x1 <- UnionM a
x
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall b. LogicalOp b => b -> b
nots a
x1
xors :: UnionM a -> UnionM a -> UnionM a
xors UnionM a
a UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
`xors` a
b1
implies :: UnionM a -> UnionM a -> UnionM a
implies UnionM a
a UnionM a
b = do
a
a1 <- UnionM a
a
a
b1 <- UnionM a
b
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
a1 forall b. LogicalOp b => b -> b -> b
`implies` a
b1
instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where
con :: c -> UnionM t
con = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c t. Solvable c t => c -> t
con
{-# INLINE con #-}
ssym :: String -> UnionM t
ssym = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c t. Solvable c t => String -> t
ssym
{-# INLINE ssym #-}
isym :: String -> Int -> UnionM t
isym String
i Int
s = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => String -> Int -> t
isym String
i Int
s
{-# INLINE isym #-}
sinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> a -> UnionM t
sinfosym String
s a
info = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
String -> a -> t
sinfosym String
s a
info
{-# INLINE sinfosym #-}
iinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> Int -> a -> UnionM t
iinfosym String
i Int
s a
info = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
String -> Int -> a -> t
iinfosym String
i Int
s a
info
{-# INLINE iinfosym #-}
conView :: UnionM t -> Maybe c
conView UnionM t
v = do
t
c <- forall (u :: * -> *) a. UnionPrjOp u => u a -> Maybe a
singleView UnionM t
v
forall c t. Solvable c t => t -> Maybe c
conView t
c
{-# INLINE conView #-}
instance
(Function f, Mergeable f, Mergeable a, Ret f ~ a) =>
Function (UnionM f)
where
type Arg (UnionM f) = Arg f
type Ret (UnionM f) = UnionM (Ret f)
UnionM f
f # :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f)
# Arg (UnionM f)
a = do
f
f1 <- UnionM f
f
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ f
f1 forall f. Function f => f -> Arg f -> Ret f
# Arg (UnionM f)
a
instance (IsString a, Mergeable a) => IsString (UnionM a) where
fromString :: String -> UnionM a
fromString = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsString a => String -> a
fromString
instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)
instance (GenSym spec a) => GenSymSimple spec (UnionM a) where
simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (UnionM a)
simpleFresh spec
spec = do
UnionM a
res <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
if Bool -> Bool
not (forall a. UnionM a -> Bool
isMerged UnionM a
res) then forall a. HasCallStack => String -> a
error String
"Not merged" else forall (m :: * -> *) a. Monad m => a -> m a
return UnionM a
res
instance
(GenSym a a, Mergeable a) =>
GenSym (UnionM a) a
where
fresh :: forall (m :: * -> *). MonadFresh m => UnionM a -> m (UnionM a)
fresh UnionM a
spec = forall {spec} {a} {m :: * -> *}.
(GenSym spec a, MonadFresh m) =>
Union spec -> m (UnionM a)
go (forall a. UnionM a -> Union a
underlyingUnion forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge UnionM a
spec)
where
go :: Union spec -> m (UnionM a)
go (Single spec
x) = forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
x
go (If spec
_ Bool
_ SymBool
_ Union spec
t Union spec
f) = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh () forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Union spec -> m (UnionM a)
go Union spec
f
instance (AllSyms a) => AllSyms (UnionM a) where
allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]
allSymsS = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
class (Eq t, Ord t, Hashable t) => IsConcrete t
instance IsConcrete Bool
instance IsConcrete Integer
instance (IsConcrete k, Mergeable t) => Mergeable (HML.HashMap k (UnionM (Maybe t))) where
rootStrategy :: MergingStrategy (HashMap k (UnionM (Maybe t)))
rootStrategy = forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a. SimpleMergeable a => SymBool -> a -> a -> a
mrgIte
instance (IsConcrete k, Mergeable t) => SimpleMergeable (HML.HashMap k (UnionM (Maybe t))) where
mrgIte :: SymBool
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
-> HashMap k (UnionM (Maybe t))
mrgIte SymBool
cond HashMap k (UnionM (Maybe t))
l HashMap k (UnionM (Maybe t))
r =
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HML.unionWith (forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond) HashMap k (UnionM (Maybe t))
ul HashMap k (UnionM (Maybe t))
ur
where
ul :: HashMap k (UnionM (Maybe t))
ul =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
( \k
k HashMap k (UnionM (Maybe t))
m -> case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
Maybe (UnionM (Maybe t))
Nothing -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
)
HashMap k (UnionM (Maybe t))
l
(forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
r)
ur :: HashMap k (UnionM (Maybe t))
ur =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
( \k
k HashMap k (UnionM (Maybe t))
m -> case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HML.lookup k
k HashMap k (UnionM (Maybe t))
m of
Maybe (UnionM (Maybe t))
Nothing -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HML.insert k
k (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing) HashMap k (UnionM (Maybe t))
m
Maybe (UnionM (Maybe t))
_ -> HashMap k (UnionM (Maybe t))
m
)
HashMap k (UnionM (Maybe t))
r
(forall k v. HashMap k v -> [k]
HML.keys HashMap k (UnionM (Maybe t))
l)
instance UnionWithExcept (UnionM (Either e v)) UnionM e v where
extractUnionExcept :: UnionM (Either e v) -> UnionM (Either e v)
extractUnionExcept = forall a. a -> a
id
instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where
extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v)
extractUnionExcept = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. CBMCEither a b -> Either a b
runCBMCEither
unionSize :: UnionM a -> Int
unionSize :: forall a. UnionM a -> Int
unionSize = forall {a} {a}. Num a => Union a -> a
unionSize' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnionM a -> Union a
underlyingUnion
where
unionSize' :: Union a -> a
unionSize' (Single a
_) = a
1
unionSize' (If a
_ Bool
_ SymBool
_ Union a
l Union a
r) = Union a -> a
unionSize' Union a
l forall a. Num a => a -> a -> a
+ Union a -> a
unionSize' Union a
r