grisette-0.13.0.1: test/Grisette/Core/Data/Class/SimpleMergeableTests.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Grisette.Core.Data.Class.SimpleMergeableTests
( simpleMergeableTests,
)
where
import Control.Monad.Cont (ContT (ContT, runContT))
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
( Identity (Identity, runIdentity),
IdentityT (IdentityT, runIdentityT),
)
import qualified Control.Monad.RWS.Lazy as RWSTLazy
import qualified Control.Monad.RWS.Strict as RWSTStrict
import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.Monoid as Monoid
import GHC.Generics (Generic)
import Generics.Deriving (Default (Default))
import Grisette
( ITEOp (symIte),
LogicalOp (symNot, (.&&), (.||)),
Mergeable,
SimpleMergeable (mrgIte),
Solvable (con, ssym),
SymBool,
Union,
mrgIf,
mrgIte1,
mrgSingle,
)
import Grisette.Core.Data.Class.TestValues (ssymBool)
import Grisette.Internal.Core.Data.Class.AsKey (AsKey, AsKey1)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))
newtype AndMonoidSymBool = AndMonoidSymBool (AsKey SymBool)
deriving (Show, Generic, Eq)
deriving (Mergeable) via (Default AndMonoidSymBool)
instance Semigroup AndMonoidSymBool where
(AndMonoidSymBool a) <> (AndMonoidSymBool b) = AndMonoidSymBool (a .&& b)
instance Monoid AndMonoidSymBool where
mempty = AndMonoidSymBool $ con True
simpleMergeableTests :: Test
simpleMergeableTests =
testGroup
"SimpleMergeable"
[ testGroup
"SimpleMergeable for common types"
[ testCase "SymBool" $ do
mrgIte (ssym "a") (ssym "b" :: AsKey SymBool) (ssym "c")
@?= symIte (ssym "a") (ssym "b") (ssym "c"),
testCase "()" $ do
mrgIte (ssym "a") () () @?= (),
testCase "(SymBool, SymBool)" $ do
mrgIte
(ssym "a")
(ssym "b" :: AsKey SymBool, ssym "d" :: AsKey SymBool)
(ssym "c", ssym "e")
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e")
),
testCase "(SymBool, SymBool, SymBool)" $ do
mrgIte
(ssym "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool
)
(ssym "c", ssym "e", ssym "g")
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g")
),
testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
mrgIte
(ssym "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool,
ssym "h" :: AsKey SymBool
)
(ssym "c", ssym "e", ssym "g", ssym "i")
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g"),
symIte (ssym "a") (ssym "h") (ssym "i")
),
testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
mrgIte
(ssym "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool,
ssym "h" :: AsKey SymBool,
ssym "j" :: AsKey SymBool
)
( ssym "c",
ssym "e",
ssym "g",
ssym "i",
ssym "k"
)
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g"),
symIte (ssym "a") (ssym "h") (ssym "i"),
symIte (ssym "a") (ssym "j") (ssym "k")
),
testCase "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
mrgIte
(ssym "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool,
ssym "h" :: AsKey SymBool,
ssym "j" :: AsKey SymBool,
ssym "l" :: AsKey SymBool
)
( ssym "c",
ssym "e",
ssym "g",
ssym "i",
ssym "k",
ssym "m"
)
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g"),
symIte (ssym "a") (ssym "h") (ssym "i"),
symIte (ssym "a") (ssym "j") (ssym "k"),
symIte (ssym "a") (ssym "l") (ssym "m")
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
mrgIte
(ssym "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool,
ssym "h" :: AsKey SymBool,
ssym "j" :: AsKey SymBool,
ssym "l" :: AsKey SymBool,
ssym "n" :: AsKey SymBool
)
( ssym "c",
ssym "e",
ssym "g",
ssym "i",
ssym "k",
ssym "m",
ssym "o"
)
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g"),
symIte (ssym "a") (ssym "h") (ssym "i"),
symIte (ssym "a") (ssym "j") (ssym "k"),
symIte (ssym "a") (ssym "l") (ssym "m"),
symIte (ssym "a") (ssym "n") (ssym "o")
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
mrgIte
(ssymBool "a")
( ssym "b" :: AsKey SymBool,
ssym "d" :: AsKey SymBool,
ssym "f" :: AsKey SymBool,
ssym "h" :: AsKey SymBool,
ssym "j" :: AsKey SymBool,
ssym "l" :: AsKey SymBool,
ssym "n" :: AsKey SymBool,
ssym "p" :: AsKey SymBool
)
( ssym "c" :: AsKey SymBool,
ssym "e" :: AsKey SymBool,
ssym "g" :: AsKey SymBool,
ssym "i" :: AsKey SymBool,
ssym "k" :: AsKey SymBool,
ssym "m" :: AsKey SymBool,
ssym "o" :: AsKey SymBool,
ssym "q" :: AsKey SymBool
)
@?= ( symIte (ssym "a") (ssym "b") (ssym "c"),
symIte (ssym "a") (ssym "d") (ssym "e"),
symIte (ssym "a") (ssym "f") (ssym "g"),
symIte (ssym "a") (ssym "h") (ssym "i"),
symIte (ssym "a") (ssym "j") (ssym "k"),
symIte (ssym "a") (ssym "l") (ssym "m"),
symIte (ssym "a") (ssym "n") (ssym "o"),
symIte (ssym "a") (ssym "p") (ssym "q")
),
testCase "SymBool -> SymBool" $ do
let f = mrgIte (ssym "a") symNot ((ssym "b" :: AsKey SymBool) .&&)
f (ssym "c")
@?= symIte
(ssym "a")
(symNot $ ssym "c")
((ssym "b") .&& (ssym "c")),
testCase "MaybeT (Union) SymBool" $ do
let l :: MaybeT (AsKey1 Union) (AsKey SymBool) =
MaybeT
( mrgIf
(ssym "b")
(mrgSingle Nothing)
(mrgSingle $ Just $ ssym "c")
)
let r :: MaybeT (AsKey1 Union) (AsKey SymBool) =
MaybeT
( mrgIf
(ssym "d")
(mrgSingle Nothing)
(mrgSingle $ Just $ ssym "e")
)
let res :: MaybeT (AsKey1 Union) (AsKey SymBool) =
MaybeT
( mrgIf
(ssym "a")
( mrgIf
(ssym "b")
(mrgSingle Nothing)
(mrgSingle $ Just $ ssym "c")
)
( mrgIf
(ssym "d")
(mrgSingle Nothing)
(mrgSingle $ Just $ ssym "e")
)
)
mrgIte (ssym "a") l r @?= res
mrgIte1 (ssym "a") l r @?= res
mrgIf (ssym "a") l r @?= res,
testCase "ExceptT SymBool (Union) SymBool" $ do
let l :: ExceptT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
ExceptT
( mrgIf
(ssym "b")
(mrgSingle $ Left $ ssym "c")
(mrgSingle $ Right $ ssym "d")
)
let r =
ExceptT
( mrgIf
(ssym "e")
(mrgSingle $ Left $ ssym "f")
(mrgSingle $ Right $ ssym "g")
)
let res =
ExceptT
( mrgIf
(ssym "a")
( mrgIf
(ssym "b")
(mrgSingle $ Left $ ssym "c")
(mrgSingle $ Right $ ssym "d")
)
( mrgIf
(ssym "e")
(mrgSingle $ Left $ ssym "f")
(mrgSingle $ Right $ ssym "g")
)
)
mrgIte (ssym "a") l r @?= res
mrgIte1 (ssym "a") l r @?= res
mrgIf (ssym "a") l r @?= res,
testGroup
"StateT Integer (Union) SymBool"
[ testCase "Lazy" $ do
let st1 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool) =
StateLazy.StateT $ \(x :: Integer) ->
mrgSingle (ssym "a", x + 2)
let st2 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool) =
StateLazy.StateT $ \(x :: Integer) ->
mrgSingle (ssym "b", x * 2)
let st3 = mrgIte (ssym "c") st1 st2
let st31 = mrgIte1 (ssym "c") st1 st2
let st3u1 = mrgIf (ssym "c") st1 st2
StateLazy.runStateT st3 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateLazy.runStateT st3 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6))
StateLazy.runStateT st31 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateLazy.runStateT st31 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6))
StateLazy.runStateT st3u1 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateLazy.runStateT st3u1 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6)),
testCase "Strict" $ do
let st1 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool) =
StateStrict.StateT $ \(x :: Integer) ->
mrgSingle (ssym "a", x + 2)
let st2 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool) =
StateStrict.StateT $ \(x :: Integer) ->
mrgSingle (ssym "b", x * 2)
let st3 = mrgIte (ssym "c") st1 st2
let st31 = mrgIte1 (ssym "c") st1 st2
let st3u1 = mrgIf (ssym "c") st1 st2
StateStrict.runStateT st3 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateStrict.runStateT st3 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6))
StateStrict.runStateT st31 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateStrict.runStateT st31 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6))
StateStrict.runStateT st3u1 2
@?= mrgSingle
(symIte (ssym "c") (ssym "a") (ssym "b"), 4)
StateStrict.runStateT st3u1 3
@?= mrgIf
(ssym "c")
(mrgSingle (ssym "a", 5))
(mrgSingle (ssym "b", 6))
],
testCase "ContT (SymBool, Integer) (Union) (SymBool, Integer)" $ do
let c1 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer) =
ContT $ \f -> f (ssym "a", 2)
let c2 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer) =
ContT $ \f -> f (ssym "b", 3)
let c3 = mrgIte (ssym "c") c1 c2
let c3u1 = mrgIf (ssym "c") c1 c2
let r =
mrgIf
(ssym "c")
( mrgIf
(ssym "p")
(mrgSingle (ssym "a", 2))
(mrgSingle (symNot $ ssym "a", 3))
)
( mrgIf
(ssym "p")
(mrgSingle (ssym "b", 3))
(mrgSingle (symNot $ ssym "b", 4))
)
let f (a, x) =
mrgIf
(ssym "p")
(mrgSingle (a, x))
(mrgSingle (symNot a, x + 1)) ::
AsKey1 Union (AsKey SymBool, Integer)
runContT c3 f @?= r
runContT c3u1 f @?= r,
testGroup
"RWST (Integer, SymBool) (Monoid.Sum Integer, AndMonoidSymBool) (Integer, SymBool) (Union) (Integer, SymBool)"
[ testCase "Lazy" $ do
let rws1 ::
RWSTLazy.RWST
(Integer, AsKey SymBool)
(Monoid.Sum Integer, AndMonoidSymBool)
(Integer, AsKey SymBool)
(AsKey1 Union)
(Integer, AsKey SymBool) =
RWSTLazy.RWST $ \(ir, br) (is, bs) ->
mrgSingle
( (ir + is, br .&& bs),
(ir - is, br .|| bs),
( Monoid.Sum $ ir * is,
AndMonoidSymBool $ bs .&& br
)
)
let rws2 ::
RWSTLazy.RWST
(Integer, AsKey SymBool)
(Monoid.Sum Integer, AndMonoidSymBool)
(Integer, AsKey SymBool)
(AsKey1 Union)
(Integer, AsKey SymBool) =
RWSTLazy.RWST $ \(ir, br) (is, bs) ->
mrgSingle
( (ir + is, br .|| bs),
(ir - is, br .&& bs),
( Monoid.Sum $ ir * is,
AndMonoidSymBool $ bs .|| br
)
)
let rws3 = mrgIte (ssymBool "c") rws1 rws2
let rws3u1 = mrgIf (ssymBool "c") rws1 rws2
let res1 ::
AsKey1
Union
( (Integer, AsKey SymBool),
(Integer, AsKey SymBool),
(Monoid.Sum Integer, AndMonoidSymBool)
) =
mrgIf
(ssym "c")
( mrgSingle
( (1, ssym "a" .&& ssym "b"),
(-1, ssym "a" .|| ssym "b"),
( 0,
AndMonoidSymBool $
ssym "b" .&& ssym "a"
)
)
)
( mrgSingle
( (1, ssym "a" .|| ssym "b"),
(-1, ssym "a" .&& ssym "b"),
( 0,
AndMonoidSymBool $
ssym "b" .|| ssym "a"
)
)
)
RWSTLazy.runRWST rws3 (0, ssym "a") (1, ssym "b")
@?= res1
RWSTLazy.runRWST rws3u1 (0, ssym "a") (1, ssym "b")
@?= res1,
testCase "Strict" $ do
let rws1 ::
RWSTStrict.RWST
(Integer, AsKey SymBool)
(Monoid.Sum Integer, AndMonoidSymBool)
(Integer, AsKey SymBool)
(AsKey1 Union)
(Integer, AsKey SymBool) =
RWSTStrict.RWST $ \(ir, br) (is, bs) ->
mrgSingle
( (ir + is, br .&& bs),
(ir - is, br .|| bs),
( Monoid.Sum $ ir * is,
AndMonoidSymBool $ bs .&& br
)
)
let rws2 ::
RWSTStrict.RWST
(Integer, AsKey SymBool)
(Monoid.Sum Integer, AndMonoidSymBool)
(Integer, AsKey SymBool)
(AsKey1 Union)
(Integer, AsKey SymBool) =
RWSTStrict.RWST $ \(ir, br) (is, bs) ->
mrgSingle
( (ir + is, br .|| bs),
(ir - is, br .&& bs),
( Monoid.Sum $ ir * is,
AndMonoidSymBool $ bs .|| br
)
)
let rws3 = mrgIte (ssymBool "c") rws1 rws2
let rws3u1 = mrgIf (ssymBool "c") rws1 rws2
let res1 ::
AsKey1
Union
( (Integer, AsKey SymBool),
(Integer, AsKey SymBool),
(Monoid.Sum Integer, AndMonoidSymBool)
) =
mrgIf
(ssymBool "c")
( mrgSingle
( (1, ssym "a" .&& ssym "b"),
(-1, ssym "a" .|| ssym "b"),
( 0,
AndMonoidSymBool $
ssym "b" .&& ssym "a"
)
)
)
( mrgSingle
( (1, ssym "a" .|| ssym "b"),
(-1, ssym "a" .&& ssym "b"),
( 0,
AndMonoidSymBool $
ssym "b" .|| ssym "a"
)
)
)
RWSTStrict.runRWST rws3 (0, ssym "a") (1, ssym "b")
@?= res1
RWSTStrict.runRWST rws3u1 (0, ssym "a") (1, ssym "b")
@?= res1
],
testGroup
"WriterT (Monoid.Sum Integer) (Union) SymBool"
[ testCase "Lazy" $ do
let st1 ::
WriterLazy.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterLazy.WriterT $ mrgSingle (ssym "a", 1)
let st2 ::
WriterLazy.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterLazy.WriterT $ mrgSingle (ssym "b", 2)
let st3 ::
WriterLazy.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterLazy.WriterT $ mrgSingle (ssym "c", 1)
let st4 = mrgIte (ssym "d") st1 st2
let st41 = mrgIte1 (ssym "d") st1 st2
let st4u1 = mrgIf (ssym "d") st1 st2
let st5 = mrgIte (ssym "d") st1 st3
let st51 = mrgIte1 (ssym "d") st1 st3
let st5u1 = mrgIf (ssym "d") st1 st3
WriterLazy.runWriterT st4
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterLazy.runWriterT st41
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterLazy.runWriterT st4u1
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterLazy.runWriterT st5
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1)
WriterLazy.runWriterT st51
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1)
WriterLazy.runWriterT st5u1
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1),
testCase "Strict" $ do
let st1 ::
WriterStrict.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterStrict.WriterT $ mrgSingle (ssym "a", 1)
let st2 ::
WriterStrict.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterStrict.WriterT $ mrgSingle (ssym "b", 2)
let st3 ::
WriterStrict.WriterT
(Monoid.Sum Integer)
(AsKey1 Union)
(AsKey SymBool) =
WriterStrict.WriterT $ mrgSingle (ssym "c", 1)
let st4 = mrgIte (ssym "d") st1 st2
let st41 = mrgIte1 (ssym "d") st1 st2
let st4u1 = mrgIf (ssym "d") st1 st2
let st5 = mrgIte (ssym "d") st1 st3
let st51 = mrgIte1 (ssym "d") st1 st3
let st5u1 = mrgIf (ssym "d") st1 st3
WriterStrict.runWriterT st4
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterStrict.runWriterT st41
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterStrict.runWriterT st4u1
@?= mrgIf
(ssym "d")
(mrgSingle (ssym "a", 1))
(mrgSingle (ssym "b", 2))
WriterStrict.runWriterT st5
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1)
WriterStrict.runWriterT st51
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1)
WriterStrict.runWriterT st5u1
@?= mrgSingle
(symIte (ssym "d") (ssym "a") (ssym "c"), 1)
],
testCase "ReaderT Integer (Union) Integer" $ do
let r1 :: ReaderT Integer (AsKey1 Union) Integer =
ReaderT $ \(x :: Integer) -> mrgSingle $ x + 2
let r2 :: ReaderT Integer (AsKey1 Union) Integer =
ReaderT $ \(x :: Integer) -> mrgSingle $ x * 2
let r3 = mrgIte (ssym "c") r1 r2
let r3u1 = mrgIf (ssym "c") r1 r2
runReaderT r3 2 @?= mrgSingle 4
runReaderT r3 3 @?= mrgIf (ssym "c") (mrgSingle 5) (mrgSingle 6)
runReaderT r3u1 2 @?= mrgSingle 4
runReaderT r3u1 3
@?= mrgIf
(ssym "c")
(mrgSingle 5)
(mrgSingle 6)
let r4 :: ReaderT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
ReaderT $ \x -> mrgSingle $ x .&& ssym "x"
let r5 :: ReaderT (AsKey SymBool) (AsKey1 Union) (AsKey SymBool) =
ReaderT $ \x -> mrgSingle $ x .|| ssym "y"
let r61 = mrgIte1 (ssym "c") r4 r5
runReaderT r61 (ssym "a")
@?= mrgSingle
( symIte
(ssym "c")
(ssym "a" .&& ssym "x")
(ssym "a" .|| ssym "y")
),
testCase "Identity SymBool" $ do
let i1 :: Identity (AsKey SymBool) = Identity $ ssym "a"
let i2 :: Identity (AsKey SymBool) = Identity $ ssym "b"
let i3 = mrgIte (ssym "c") i1 i2
let i31 = mrgIte1 (ssym "c") i1 i2
runIdentity i3 @?= symIte (ssym "c") (ssym "a") (ssym "b")
runIdentity i31
@?= symIte (ssym "c") (ssym "a") (ssym "b"),
testCase "IdentityT (Union) SymBool" $ do
let i1 :: IdentityT (AsKey1 Union) (AsKey SymBool) =
IdentityT $ mrgSingle $ ssym "a"
let i2 :: IdentityT (AsKey1 Union) (AsKey SymBool) =
IdentityT $ mrgSingle $ ssym "b"
let i3 = mrgIte (ssym "c") i1 i2
let i31 = mrgIte1 (ssym "c") i1 i2
let i3u1 = mrgIf (ssym "c") i1 i2
runIdentityT i3
@?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
runIdentityT i31
@?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
runIdentityT i3u1
@?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"))
]
]