grisette-0.4.0.0: test/Grisette/Core/Control/Monad/UnionMTests.hs
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Grisette.Core.Control.Monad.UnionMTests (unionMTests) where
import qualified Data.ByteString as B
import qualified Data.HashMap.Lazy as ML
import Grisette.Core.BuiltinUnionWrappers (mrgLeft, mrgRight)
import Grisette.Core.Control.Monad.UnionM
( UnionM,
isMerged,
underlyingUnion,
unionSize,
)
import Grisette.Core.Data.Class.EvaluateSym
( EvaluateSym (evaluateSym),
)
import Grisette.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Core.Data.Class.Function (Function ((#)))
import Grisette.Core.Data.Class.GenSym
( ListSpec (ListSpec),
choose,
genSym,
genSymSimple,
)
import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Core.Data.Class.LogicalOp
( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
)
import Grisette.Core.Data.Class.ModelOps
( ModelOps (emptyModel),
ModelRep (buildModel),
SymbolSetRep (buildSymbolSet),
)
import Grisette.Core.Data.Class.SEq (SEq ((.==)))
import Grisette.Core.Data.Class.SOrd
( SOrd (symCompare, (.<), (.<=), (.>), (.>=)),
)
import Grisette.Core.Data.Class.SimpleMergeable
( SimpleMergeable (mrgIte),
UnionLike (single, unionIf),
UnionPrjOp (ifView, leftMost, singleView, toGuardedList),
merge,
mrgIf,
mrgIte1,
mrgSingle,
(.#),
pattern If,
pattern Single,
)
import Grisette.Core.Data.Class.Solvable (Solvable (con, conView, isym, ssym))
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))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (TypedSymbol)
import Grisette.IR.SymPrim.Data.Prim.Model
( ModelValuePair ((::=)),
)
import Grisette.IR.SymPrim.Data.SymPrim (SymBool)
import Grisette.TestUtil.SymbolicAssertion ((@?=~))
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit (assertFailure, (@?=))
unionMTests :: Test
unionMTests =
testGroup
"UnionM"
[ testCase "Mergeable" $
do
let r =
( mrgIf
"a"
( mrgSingle
( mrgIf
"b"
(mrgSingle $ Left "c")
(mrgSingle $ Right "d")
)
)
( mrgSingle
( mrgIf
"e"
(mrgSingle $ Left "f")
(mrgSingle $ Right "g")
)
) ::
UnionM (UnionM (Either SymBool SymBool))
)
isMerged r @?= True
underlyingUnion (underlyingUnion <$> r)
@?= UnionSingle
( UnionIf
(Left $ symIte "a" "c" "f")
True
(symIte "a" "b" "e")
(UnionSingle $ Left $ symIte "a" "c" "f")
(UnionSingle $ Right $ symIte "a" "d" "g")
),
testCase "SimpleMergeable" $ do
let l :: UnionM (Either SymBool SymBool) =
mrgIf "b" (mrgSingle $ Left "c") (mrgSingle $ Right "d")
let r = mrgIf "e" (mrgSingle $ Left "f") (mrgSingle $ Right "g")
let res = mrgIte "a" l r
let ref =
UnionIf
(Left $ symIte "a" "c" "f")
True
(symIte "a" "b" "e")
(UnionSingle $ Left $ symIte "a" "c" "f")
(UnionSingle $ Right $ symIte "a" "d" "g")
isMerged res @?= True
underlyingUnion res @?= ref,
testCase "SimpleMergeable1" $ do
let l :: UnionM SymBool = mrgIf "b" (mrgSingle "c") (mrgSingle "d")
let r :: UnionM SymBool = mrgIf "e" (mrgSingle "f") (mrgSingle "g")
let res = mrgIte1 "a" l r
isMerged res @?= True
underlyingUnion res
@?= UnionSingle
( symIte
"a"
(symIte "b" "c" "d")
(symIte "e" "f" "g")
),
testGroup
"Functor"
[ testCase "fmap should work but would strip mergeable knowledge" $ do
let x :: UnionM Integer =
(+ 1) <$> mrgIf "a" (mrgSingle 1) (mrgSingle 2)
x @?= unionIf "a" (return 2) (return 3)
],
testGroup
"Applicative"
[ testCase "pure should work but won't give us mergeable knowledge" $
(pure 1 :: UnionM Integer) @?= single 1,
testCase "<*> should work but won't give us mergeable knowledge" $ do
let f :: UnionM (Integer -> Integer) =
mrgIf "a" (mrgSingle id) (mrgSingle (+ 1))
let v :: UnionM Integer = mrgIf "b" (mrgSingle 1) (mrgSingle 3)
f
<*> v
@?= unionIf
"a"
(unionIf "b" (single 1) (single 3))
(unionIf "b" (single 2) (single 4))
],
testGroup
"Monad"
[ testCase "return should work but won't give us mergeable knowledge" $
(pure 1 :: UnionM Integer) @?= single 1,
testCase ">>= should work and keeps mergeable knowledge" $ do
let v :: UnionM Integer = mrgIf "a" (mrgSingle 0) (mrgSingle 1)
let f :: Integer -> UnionM Integer = \i ->
mrgIf "b" (mrgSingle $ i + 1) (mrgSingle $ i + 3)
(v >>= f)
@?= mrgIf
"a"
(mrgIf "b" (mrgSingle 1) (mrgSingle 3))
(mrgIf "b" (mrgSingle 2) (mrgSingle 4))
],
testGroup
"UnionOp"
[ testCase "single" $ do
let r1 :: UnionM SymBool = single "a"
isMerged r1 @?= False
underlyingUnion r1 @?= UnionSingle "a",
testGroup
"unionIf"
[ testCase "unionIf should work when no merged" $ do
let r1 :: UnionM SymBool = unionIf "a" (single "b") (single "c")
isMerged r1 @?= False
underlyingUnion r1
@?= UnionIf "b" False "a" (UnionSingle "b") (UnionSingle "c"),
testCase
"unionIf should propagate and merge the results when some branch merged"
$ do
let r1 :: UnionM SymBool =
unionIf "a" (mrgSingle "b") (single "c")
isMerged r1 @?= True
underlyingUnion r1 @?= UnionSingle (symIte "a" "b" "c")
let r2 :: UnionM SymBool =
unionIf "a" (single "b") (mrgSingle "c")
isMerged r2 @?= True
underlyingUnion r2 @?= UnionSingle (symIte "a" "b" "c")
let r3 :: UnionM SymBool =
unionIf "a" (mrgSingle "b") (mrgSingle "c")
isMerged r3 @?= True
underlyingUnion r3 @?= UnionSingle (symIte "a" "b" "c")
],
testCase "singleView should work" $ do
singleView (single "a" :: UnionM SymBool) @?= Just "a"
singleView (mrgSingle "a" :: UnionM SymBool) @?= Just "a"
singleView
( unionIf "a" (single $ Left "b") (single $ Right "c") ::
UnionM (Either SymBool SymBool)
)
@?= Nothing
case (single "a" :: UnionM SymBool) of
Single r -> r @?= "a"
_ -> assertFailure "Single match failed"
case (mrgSingle "a" :: UnionM SymBool) of
Single r -> r @?= "a"
_ -> assertFailure "Single match failed"
case ( unionIf "a" (single $ Left "b") (single $ Right "c") ::
UnionM (Either SymBool SymBool)
) of
Single _ -> assertFailure "Single match failed"
_ -> return (),
testCase "ifView should work" $ do
let r1 :: UnionM (Either SymBool SymBool) =
unionIf "a" (single $ Left "b") (single $ Right "c")
let r2 :: UnionM (Either SymBool SymBool) =
mrgIf "a" (mrgSingle $ Left "b") (mrgSingle $ Right "c")
ifView r1 @?= Just ("a", single $ Left "b", single $ Right "c")
ifView r2
@?= Just ("a", mrgSingle $ Left "b", mrgSingle $ Right "c")
ifView (single "a" :: UnionM SymBool) @?= Nothing
case r1 of
If c l r -> do
c @?= "a"
l @?= single (Left "b")
r @?= single (Right "c")
_ -> assertFailure "Single match failed"
case r2 of
If c l r -> do
c @?= "a"
l @?= mrgSingle (Left "b")
r @?= mrgSingle (Right "c")
_ -> assertFailure "Single match failed"
case single "a" :: UnionM SymBool of
If {} -> assertFailure "Single match failed"
_ -> return (),
testCase "leftMost should work" $ do
leftMost (single "a" :: UnionM SymBool) @?= "a"
leftMost (mrgSingle "a" :: UnionM SymBool) @?= "a"
let r1 :: UnionM (Either SymBool SymBool) =
unionIf "a" (single $ Left "b") (single $ Right "c")
let r2 :: UnionM (Either SymBool SymBool) =
mrgIf "a" (mrgSingle $ Left "b") (mrgSingle $ Right "c")
leftMost r1 @?= Left "b"
leftMost r2 @?= Left "b",
testCase "toGuardedList should work" $ do
let actual =
toGuardedList
( mrgIf "a" (single 1) (mrgIf "b" (single 2) (single 3)) ::
UnionM Integer
)
let expected =
[ ("a", 1),
(symNot "a" .&& "b", 2),
(symNot "a" .&& symNot "b", 3)
]
actual @?=~ expected
],
testGroup
"MonadUnion"
[ testCase "merge should work" $ do
let r1 :: UnionM SymBool =
merge (unionIf "a" (single "b") (single "c"))
isMerged r1 @?= True
underlyingUnion r1 @?= UnionSingle (symIte "a" "b" "c"),
testCase "mrgSingle should work" $ do
let r1 :: UnionM SymBool = mrgSingle "a"
isMerged r1 @?= True
underlyingUnion r1 @?= UnionSingle "a",
testGroup
"mrgIf should work"
[ testCase "mrgIf should perform lazy evaluation" $ do
(mrgIf (con True) (mrgSingle "a") undefined :: UnionM SymBool)
@?= mrgSingle "a"
(mrgIf (con False) undefined (mrgSingle "a") :: UnionM SymBool)
@?= mrgSingle "a",
testCase "mrgIf should work" $
(mrgIf "a" (single "b") (single "c") :: UnionM SymBool)
@?= merge (unionIf "a" (single "b") (single "c"))
]
],
let a :: SymBool = "a"
b :: SymBool = "b"
c :: SymBool = "c"
d :: SymBool = "d"
e :: SymBool = "e"
f :: SymBool = "f"
g1 :: UnionM (Either SymBool SymBool) =
mrgIf a (mrgSingle $ Left b) (mrgSingle $ Right c)
g2 :: UnionM (Either SymBool SymBool) =
mrgIf d (mrgSingle $ Left e) (mrgSingle $ Right f)
in testGroup
"SEq"
[ testCase "Single/Single" $
(mrgSingle a :: UnionM SymBool)
.== mrgSingle b
@?= (a .== b),
testCase "If/Single" $ do
g1
.== mrgSingle (Left d)
@?= symIte a (b .== d) (con False)
g1
.== mrgSingle (Right d)
@?= symIte a (con False) (c .== d),
testCase "Single/If" $ do
mrgSingle (Left d)
.== g1
@?= symIte a (d .== b) (con False)
mrgSingle (Right d)
.== g1
@?= symIte a (con False) (d .== c),
testCase "If/If" $
g1
.== g2
@?= symIte
a
(symIte d (b .== e) (con False))
(symIte d (con False) (c .== f))
],
let a :: SymBool = "a"
b :: SymBool = "b"
c :: SymBool = "c"
d :: SymBool = "d"
e :: SymBool = "e"
f :: SymBool = "f"
g1 :: UnionM (Either SymBool SymBool) =
mrgIf a (mrgSingle $ Left b) (mrgSingle $ Right c)
g2 :: UnionM (Either SymBool SymBool) =
mrgIf d (mrgSingle $ Left e) (mrgSingle $ Right f)
in testGroup
"SOrd"
[ testCase "Single/Single" $ do
(mrgSingle a :: UnionM SymBool)
.<= mrgSingle b
@?= (a .<= b :: SymBool)
(mrgSingle a :: UnionM SymBool)
.< mrgSingle b
@?= (a .< b :: SymBool)
(mrgSingle a :: UnionM SymBool)
.>= mrgSingle b
@?= (a .>= b :: SymBool)
(mrgSingle a :: UnionM SymBool)
.> mrgSingle b
@?= (a .> b :: SymBool)
(mrgSingle a :: UnionM SymBool)
`symCompare` mrgSingle b
@?= (a `symCompare` b :: UnionM Ordering),
testCase "If/Single" $ do
g1
.<= mrgSingle (Left d)
@?= symIte a (b .<= d) (con False)
g1
.< mrgSingle (Left d)
@?= symIte a (b .< d) (con False)
g1
.>= mrgSingle (Left d)
@?= symIte a (b .>= d) (con True)
g1
.> mrgSingle (Left d)
@?= symIte a (b .> d) (con True)
g1
`symCompare` mrgSingle (Left d)
@?= ( mrgIf a (b `symCompare` d) (mrgSingle GT) ::
UnionM Ordering
)
g1
.<= mrgSingle (Right d)
@?= symIte a (con True) (c .<= d)
g1
.< mrgSingle (Right d)
@?= symIte a (con True) (c .< d)
g1
.>= mrgSingle (Right d)
@?= symIte a (con False) (c .>= d)
g1
.> mrgSingle (Right d)
@?= symIte a (con False) (c .> d)
g1
`symCompare` mrgSingle (Right d)
@?= ( mrgIf a (mrgSingle LT) (c `symCompare` d) ::
UnionM Ordering
),
testCase "Single/If" $ do
mrgSingle (Left d)
.<= g1
@?= symIte a (d .<= b) (con True)
mrgSingle (Left d)
.< g1
@?= symIte a (d .< b) (con True)
mrgSingle (Left d)
.>= g1
@?= symIte a (d .>= b) (con False)
mrgSingle (Left d)
.> g1
@?= symIte a (d .> b) (con False)
mrgSingle (Left d)
`symCompare` g1
@?= ( mrgIf a (d `symCompare` b) (mrgSingle LT) ::
UnionM Ordering
)
mrgSingle (Right d)
.<= g1
@?= symIte a (con False) (d .<= c)
mrgSingle (Right d)
.< g1
@?= symIte a (con False) (d .< c)
mrgSingle (Right d)
.>= g1
@?= symIte a (con True) (d .>= c)
mrgSingle (Right d)
.> g1
@?= symIte a (con True) (d .> c)
mrgSingle (Right d)
`symCompare` g1
@?= ( mrgIf a (mrgSingle GT) (d `symCompare` c) ::
UnionM Ordering
),
testCase "If/If" $ do
g1
.<= g2
@?= symIte
a
(symIte d (b .<= e) (con True))
(symIte d (con False) (c .<= f))
g1
.< g2
@?= symIte
a
(symIte d (b .< e) (con True))
(symIte d (con False) (c .< f))
g1
.>= g2
@?= symIte
a
(symIte d (b .>= e) (con False))
(symIte d (con True) (c .>= f))
g1
.> g2
@?= symIte
a
(symIte d (b .> e) (con False))
(symIte d (con True) (c .> f))
g1
`symCompare` g2
@?= ( mrgIf
a
(mrgIf d (b `symCompare` e) (mrgSingle LT))
(mrgIf d (mrgSingle GT) (c `symCompare` f)) ::
UnionM Ordering
)
],
testGroup
"ToSym"
[ testCase "From single" $
(toSym True :: UnionM SymBool) @?= mrgSingle (con True),
testCase "From UnionMBase" $
(toSym (mrgSingle True :: UnionM Bool) :: UnionM SymBool)
@?= mrgSingle (con True)
],
testGroup
"ToCon"
[ testCase "To single" $ do
(toCon (mrgSingle (con True) :: UnionM SymBool) :: Maybe Bool)
@?= Just True
(toCon (mrgSingle "a" :: UnionM SymBool) :: Maybe Bool) @?= Nothing
( toCon
( mrgIf "a" (mrgLeft $ con False) (mrgRight $ con True) ::
UnionM (Either SymBool SymBool)
) ::
Maybe (Either Bool Bool)
)
@?= Nothing,
testCase "To UnionMBase" $ do
( toCon (mrgSingle (con True) :: UnionM SymBool) ::
Maybe (UnionM Bool)
)
@?= Just (mrgSingle True)
(toCon (mrgSingle "a" :: UnionM SymBool) :: Maybe (UnionM Bool))
@?= Nothing
( toCon
( mrgIf "a" (mrgLeft $ con False) (mrgRight $ con True) ::
UnionM (Either SymBool SymBool)
) ::
Maybe (UnionM (Either Bool Bool))
)
@?= Just (mrgIf "a" (mrgLeft False) (mrgRight True))
( toCon
( mrgIf "a" (mrgLeft "b") (mrgRight $ con True) ::
UnionM (Either SymBool SymBool)
) ::
Maybe (UnionM (Either Bool Bool))
)
@?= Nothing
],
testCase "Evaluate" $ do
let model = emptyModel
let model1 = buildModel ("a" ::= True, "b" ::= False, "c" ::= True)
evaluateSym False model (mrgSingle "a")
@?= (mrgSingle "a" :: UnionM SymBool)
evaluateSym True model (mrgSingle "a")
@?= (mrgSingle $ con False :: UnionM SymBool)
evaluateSym False model1 (mrgSingle "a")
@?= (mrgSingle $ con True :: UnionM SymBool)
evaluateSym True model1 (mrgSingle "a")
@?= (mrgSingle $ con True :: UnionM SymBool)
evaluateSym
False
model1
( mrgIf
"a"
(mrgSingle $ Left "d")
(mrgSingle $ Right "e")
)
@?= (mrgSingle $ Left "d" :: UnionM (Either SymBool SymBool))
evaluateSym
True
model1
( mrgIf
"a"
(mrgSingle $ Left "d")
(mrgSingle $ Right "e")
)
@?= (mrgSingle $ Left $ con False :: UnionM (Either SymBool SymBool))
evaluateSym
False
model1
( mrgIf
"d"
(mrgSingle $ Left "a")
(mrgSingle $ Right "b")
)
@?= ( mrgIf
"d"
(mrgSingle $ Left $ con True)
(mrgSingle $ Right $ con False) ::
UnionM (Either SymBool SymBool)
)
evaluateSym
True
model1
( mrgIf
"d"
(mrgSingle $ Left "a")
(mrgSingle $ Right "b")
)
@?= (mrgSingle $ Right $ con False :: UnionM (Either SymBool SymBool))
evaluateSym
False
model1
( mrgIf
"a"
(mrgSingle $ Left "b")
(mrgSingle $ Right "c")
)
@?= ( mrgSingle $ Left $ con False ::
UnionM
(Either SymBool SymBool)
),
testCase "SubstituteSym" $ do
let asym = "a" :: TypedSymbol Bool
let a = "a"
let b = "b"
let c = "c"
substituteSym
asym
b
(mrgSingle $ Left a :: UnionM (Either SymBool SymBool))
@?= mrgSingle (Left b)
substituteSym
asym
b
(mrgSingle $ Left c :: UnionM (Either SymBool SymBool))
@?= mrgSingle (Left c)
substituteSym
asym
b
(mrgSingle $ Right a :: UnionM (Either SymBool SymBool))
@?= mrgSingle (Right b)
substituteSym
asym
b
(mrgSingle $ Right c :: UnionM (Either SymBool SymBool))
@?= mrgSingle (Right c)
substituteSym
asym
b
( mrgIf a (mrgSingle $ Left a) (mrgSingle $ Right c) ::
UnionM (Either SymBool SymBool)
)
@?= mrgIf b (mrgSingle $ Left b) (mrgSingle $ Right c)
substituteSym
asym
b
( mrgIf c (mrgSingle $ Left c) (mrgSingle $ Right a) ::
UnionM (Either SymBool SymBool)
)
@?= mrgIf c (mrgSingle $ Left c) (mrgSingle $ Right b),
testCase "ExtractSymbolic" $ do
extractSymbolics (mrgSingle "a" :: UnionM SymBool)
@?= buildSymbolSet ("a" :: TypedSymbol Bool)
extractSymbolics
( mrgIf "a" (mrgSingle $ Left "b") (mrgSingle $ Right "c") ::
UnionM (Either SymBool SymBool)
)
@?= buildSymbolSet
( "a" :: TypedSymbol Bool,
"b" :: TypedSymbol Bool,
"c" :: TypedSymbol Bool
),
testGroup
"Num"
[ testCase "fromInteger" $ (1 :: UnionM Integer) @?= mrgSingle 1,
testCase "negate" $
negate (mrgIf "a" (mrgSingle 1) (mrgSingle 2) :: UnionM Integer)
@?= mrgIf "a" (mrgSingle $ -1) (mrgSingle $ -2),
testCase "plus" $
(mrgIf "a" (mrgSingle 0) (mrgSingle 1) :: UnionM Integer)
+ mrgIf "b" (mrgSingle 1) (mrgSingle 3)
@?= mrgIf
"a"
(mrgIf "b" (mrgSingle 1) (mrgSingle 3))
(mrgIf "b" (mrgSingle 2) (mrgSingle 4)),
testCase "minus" $
(mrgIf "a" (mrgSingle 0) (mrgSingle 1) :: UnionM Integer)
- mrgIf "b" (mrgSingle $ -3) (mrgSingle $ -1)
@?= mrgIf
"a"
(mrgIf (symNot "b") (mrgSingle 1) (mrgSingle 3))
(mrgIf (symNot "b") (mrgSingle 2) (mrgSingle 4)),
testCase "times" $
(mrgIf "a" (mrgSingle 1) (mrgSingle 2) :: UnionM Integer)
* mrgIf "b" (mrgSingle 3) (mrgSingle 4)
@?= mrgIf
"a"
(mrgIf "b" (mrgSingle 3) (mrgSingle 4))
(mrgIf "b" (mrgSingle 6) (mrgSingle 8)),
testCase "abs" $
abs (mrgIf "a" (mrgSingle $ -1) (mrgSingle 2) :: UnionM Integer)
@?= mrgIf "a" (mrgSingle 1) (mrgSingle 2),
testCase "signum" $
signum (mrgIf "a" (mrgSingle $ -1) (mrgSingle 2) :: UnionM Integer)
@?= mrgIf "a" (mrgSingle $ -1) (mrgSingle 1)
],
testGroup
"symIteOp"
[ testCase "symIte" $
symIte "a" (mrgSingle "b") (mrgSingle "c")
@?= (mrgSingle (symIte "a" "b" "c") :: UnionM SymBool)
],
let l = mrgIf "a" (mrgSingle False) (mrgSingle True)
r = mrgIf "b" (mrgSingle False) (mrgSingle True)
in testGroup
"LogicalOp"
[ testCase ".||" $
l
.|| r
@?= ( mrgIf
("a" .&& "b")
(mrgSingle False)
(mrgSingle True) ::
UnionM Bool
),
testCase ".&&" $
l
.&& r
@?= ( mrgIf
("a" .|| "b")
(mrgSingle False)
(mrgSingle True) ::
UnionM Bool
),
testCase "symNot" $
symNot l
@?= mrgIf (symNot "a") (mrgSingle False) (mrgSingle True),
testCase "symXor" $
l
`symXor` r
@?= ( mrgIf
(symIte "a" "b" (symNot "b"))
(mrgSingle False)
(mrgSingle True) ::
UnionM Bool
),
testCase "symImplies" $
l
`symImplies` r
@?= ( mrgIf
(symNot "a" .&& "b")
(mrgSingle False)
(mrgSingle True) ::
UnionM Bool
)
],
testCase "PrimWrapper" $ do
con True @?= (mrgSingle $ con True :: UnionM SymBool)
ssym "a" @?= (mrgSingle "a" :: UnionM SymBool)
isym "a" 0 @?= (mrgSingle $ isym "a" 0 :: UnionM SymBool)
conView (mrgSingle $ con True :: UnionM SymBool) @?= Just True
conView (mrgSingle "a" :: UnionM SymBool) @?= Nothing
conView
( mrgIf
"a"
(mrgSingle $ con False)
(mrgSingle $ con True) ::
UnionM SymBool
)
@?= Nothing,
testGroup
"Function class"
[ testCase "Applying function in UnionMBase" $ do
let func =
mrgIf "a" (mrgSingle (+ 1)) (mrgSingle (+ 2)) ::
UnionM (Integer -> Integer)
func # (1 :: Integer) @?= mrgIf "a" (mrgSingle 2) (mrgSingle 3),
testCase "Helper for applying on UnionMBase" $ do
let func (x :: Integer) =
mrgIf "a" (mrgSingle $ x + 1) (mrgSingle $ x + 3)
(func .# (mrgIf "b" (mrgSingle 0) (mrgSingle 1) :: UnionM Integer))
@?= ( mrgIf
"b"
(mrgIf "a" (mrgSingle 1) (mrgSingle 3))
(mrgIf "a" (mrgSingle 2) (mrgSingle 4)) ::
UnionM Integer
)
],
testCase "IsString" $ ("x" :: UnionM B.ByteString) @?= mrgSingle "x",
testGroup
"GenSym"
[ testCase "GenSym with spec" $ do
(genSym (ListSpec 1 3 ()) "a" :: UnionM (UnionM [SymBool]))
@?= mrgSingle
( mrgIf
(isym "a" 3)
(mrgSingle [isym "a" 2])
( mrgIf
(isym "a" 4)
(mrgSingle [isym "a" 1, isym "a" 2])
(mrgSingle [isym "a" 0, isym "a" 1, isym "a" 2])
)
)
(genSymSimple (ListSpec 1 3 ()) "a" :: UnionM [SymBool])
@?= mrgIf
(isym "a" 3)
(mrgSingle [isym "a" 2])
( mrgIf
(isym "a" 4)
(mrgSingle [isym "a" 1, isym "a" 2])
(mrgSingle [isym "a" 0, isym "a" 1, isym "a" 2])
),
testCase "GenSym with same shape" $
( genSym
( mrgIf
"a"
(mrgSingle ["x"])
(mrgSingle ["y", "z"]) ::
UnionM [SymBool]
)
"a" ::
UnionM [SymBool]
)
@?= mrgIf
(isym "a" 0)
(mrgSingle [isym "a" 1])
(mrgSingle [isym "a" 2, isym "a" 3])
],
testGroup
"Concrete Key HashMaps"
[ testCase "Concrete Key HashMap should work" $ do
mrgIte
"a"
( ML.fromList
[ (1, mrgSingle $ Just 1),
(2, mrgSingle $ Just 2)
] ::
ML.HashMap Integer (UnionM (Maybe Integer))
)
(ML.fromList [(1, mrgSingle $ Just 2), (3, mrgSingle $ Just 3)])
@?= ML.fromList
[ (1, mrgIf "a" (mrgSingle $ Just 1) (mrgSingle $ Just 2)),
( 2,
mrgIf
(symNot "a")
(mrgSingle Nothing)
(mrgSingle $ Just 2)
),
(3, mrgIf "a" (mrgSingle Nothing) (mrgSingle $ Just 3))
]
mrgIf
"a"
( mrgSingle $
ML.fromList
[ (1, mrgSingle $ Just 1),
(2, mrgSingle $ Just 2)
] ::
UnionM (ML.HashMap Integer (UnionM (Maybe Integer)))
)
( mrgSingle
( ML.fromList
[ (1, mrgSingle $ Just 2),
(3, mrgSingle $ Just 3)
]
)
)
@?= mrgSingle
( ML.fromList
[ (1, mrgIf "a" (mrgSingle $ Just 1) (mrgSingle $ Just 2)),
( 2,
mrgIf
(symNot "a")
(mrgSingle Nothing)
(mrgSingle $ Just 2)
),
(3, mrgIf "a" (mrgSingle Nothing) (mrgSingle $ Just 3))
]
)
],
testCase
"unionSize"
$ do
unionSize (single 1 :: UnionM Integer) @?= 1
unionSize (mrgIf (ssym "a") (single 1) (single 2) :: UnionM Integer)
@?= 2
unionSize (choose [1, 2, 3, 4, 5, 6, 7] "a" :: UnionM Integer) @?= 7
]