packages feed

grisette-0.13.0.1: test/Grisette/Core/Data/Class/MergeableTests.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Grisette.Core.Data.Class.MergeableTests (mergeableTests) where

import Control.Monad.Cont (ContT (ContT, runContT))
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
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.ByteString.Char8 as C
import Data.Functor.Sum (Sum (InL, InR))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Stack (HasCallStack)
import Grisette
  ( AsKey,
    DynamicSortedIdx (DynamicSortedIdx),
    ITEOp (symIte),
    LogicalOp (symNot, (.&&), (.||)),
    Mergeable (rootStrategy),
    MergingStrategy (NoStrategy, SimpleStrategy),
    Solvable (con, ssym),
    StrategyList (StrategyList),
    SymBool,
    Union,
    buildStrategyList,
    mrgIf,
    mrgSingle,
    resolveStrategy,
  )
import Grisette.Internal.Core.Data.Class.AsKey (AsKey1)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, assertFailure, (@?=))
import Test.QuickCheck (ioProperty)

testMergeableSimpleEquivClass ::
  (HasCallStack, Mergeable x, Show x, Eq x) =>
  x ->
  [DynamicSortedIdx] ->
  [(SymBool, x, x, x)] ->
  Assertion
testMergeableSimpleEquivClass x idxs cases = do
  let (idxsT, s) = resolveStrategy rootStrategy x
  case s of
    SimpleStrategy m -> do
      idxsT @?= idxs
      go cases
      where
        go [] = return ()
        go ((c, t, f, r) : xs) = do
          fst (resolveStrategy rootStrategy t) @?= idxs
          fst (resolveStrategy rootStrategy f) @?= idxs
          fst (resolveStrategy rootStrategy r) @?= idxs
          m c t f @?= r
          go xs
    _ -> assertFailure $ "Bad strategy type for " ++ show x

mergeableTests :: Test
mergeableTests =
  testGroup
    "Mergeable"
    [ testGroup
        "Mergeable for common types"
        [ let SimpleStrategy f = rootStrategy :: MergingStrategy (AsKey SymBool)
           in testGroup
                "Mergeable for SymBool"
                [ testCase "true condition" $ do
                    f (con True) (ssym "a") (ssym "b") @?= ssym "a",
                  testCase "false condition" $
                    f (con False) (ssym "a") (ssym "b") @?= ssym "b",
                  testCase "general condition" $
                    f (ssym "a") (ssym "b") (ssym "c")
                      @?= symIte (ssym "a") (ssym "b") (ssym "c")
                ],
          testProperty "Bool" $
            ioProperty . \(x :: Bool) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Integer" $
            ioProperty . \(x :: Integer) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Char" $
            ioProperty . \(x :: Char) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Int" $
            ioProperty . \(x :: Int) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Int8" $
            ioProperty . \(x :: Int8) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Int16" $
            ioProperty . \(x :: Int16) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Int32" $
            ioProperty . \(x :: Int32) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Int64" $
            ioProperty . \(x :: Int64) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Word" $
            ioProperty . \(x :: Word) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Word8" $
            ioProperty . \(x :: Word8) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Word16" $
            ioProperty . \(x :: Word16) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Word32" $
            ioProperty . \(x :: Word32) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "Word64" $
            ioProperty . \(x :: Word64) ->
              testMergeableSimpleEquivClass
                x
                [DynamicSortedIdx x]
                [(ssym "a", x, x, x)],
          testProperty "()" $
            ioProperty . \(x :: ()) ->
              testMergeableSimpleEquivClass x [] [(ssym "a", x, x, x)],
          testProperty "ByteString" $
            ioProperty . \(x :: String) ->
              let b = C.pack x
               in testMergeableSimpleEquivClass
                    b
                    [DynamicSortedIdx b]
                    [(ssym "a", b, b, b)],
          testGroup
            "Either"
            [ testGroup
                "Either Integer Integer"
                [ testProperty "Left x" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        (Left x :: Either Integer Integer)
                        [DynamicSortedIdx False, DynamicSortedIdx x]
                        [(ssym "a", Left x, Left x, Left x)],
                  testProperty "Right x" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        (Right x :: Either Integer Integer)
                        [DynamicSortedIdx True, DynamicSortedIdx x]
                        [(ssym "a", Right x, Right x, Right x)]
                ],
              testGroup
                "Either SymBool SymBool"
                [ testCase "Left v" $ do
                    let (idxsL, SimpleStrategy fL) =
                          resolveStrategy
                            rootStrategy
                            (Left (ssym "a") :: Either (AsKey SymBool) (AsKey SymBool))
                    idxsL @?= [DynamicSortedIdx False]
                    fL (ssym "a") (Left $ ssym "b") (Left $ ssym "c")
                      @?= Left (symIte (ssym "a") (ssym "b") (ssym "c")),
                  testCase "Right v" $ do
                    let (idxsR, SimpleStrategy fR) =
                          resolveStrategy
                            rootStrategy
                            (Right (ssym "a") :: Either (AsKey SymBool) (AsKey SymBool))
                    idxsR @?= [DynamicSortedIdx True]
                    fR (ssym "a") (Right $ ssym "b") (Right $ ssym "c")
                      @?= Right (symIte (ssym "a") (ssym "b") (ssym "c"))
                ]
            ],
          testGroup
            "Maybe"
            [ testGroup
                "Maybe Integer"
                [ testProperty "Nothing" $
                    ioProperty . \(_ :: Integer) -> do
                      testMergeableSimpleEquivClass
                        (Nothing :: Maybe Integer)
                        [DynamicSortedIdx False]
                        [(ssym "a", Nothing, Nothing, Nothing)],
                  testProperty "Just v" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        (Just x :: Maybe Integer)
                        [DynamicSortedIdx True, DynamicSortedIdx x]
                        [(ssym "a", Just x, Just x, Just x)]
                ],
              testCase "Maybe AsKey SymBool / Just v" $ do
                let (idxsJ, SimpleStrategy fJ) =
                      resolveStrategy
                        rootStrategy
                        (Just (ssym "a") :: Maybe (AsKey SymBool))
                idxsJ @?= [DynamicSortedIdx True]
                fJ (ssym "a") (Just $ ssym "b") (Just $ ssym "c")
                  @?= Just (symIte (ssym "a") (ssym "b") (ssym "c"))
            ],
          testGroup
            "List"
            [ testCase "BuildStrategyList" $ do
                case buildStrategyList @Integer rootStrategy [1, 2, 3] of
                  StrategyList idxs _ -> do
                    idxs
                      @?= [ [DynamicSortedIdx (1 :: Integer)],
                            [DynamicSortedIdx (2 :: Integer)],
                            [DynamicSortedIdx (3 :: Integer)]
                          ],
              testProperty "List for ordered type" $
                ioProperty . \(x :: [Integer]) -> do
                  testMergeableSimpleEquivClass
                    x
                    [ DynamicSortedIdx (length x),
                      DynamicSortedIdx $ buildStrategyList rootStrategy x
                    ]
                    [(ssym "a", x, x, x)],
              testProperty "Nested List for ordered type" $
                ioProperty . \(x :: [[Integer]]) -> do
                  testMergeableSimpleEquivClass
                    x
                    [ DynamicSortedIdx (length x),
                      DynamicSortedIdx $ buildStrategyList rootStrategy x
                    ]
                    [(ssym "a", x, x, x)],
              testGroup
                "[SymBool]"
                [ testCase "[]" $
                    testMergeableSimpleEquivClass
                      ([] :: [AsKey SymBool])
                      [DynamicSortedIdx (0 :: Int)]
                      [(ssym "a", [], [], [])],
                  testCase "[v1, v2]" $
                    testMergeableSimpleEquivClass
                      [ssym "a" :: AsKey SymBool, ssym "b"]
                      [DynamicSortedIdx (2 :: Int)]
                      [ ( ssym "a",
                          [ssym "b", ssym "c"],
                          [ssym "d", ssym "e"],
                          [ symIte (ssym "a") (ssym "b") (ssym "d"),
                            symIte (ssym "a") (ssym "c") (ssym "e")
                          ]
                        )
                      ]
                ]
            ],
          testCase "(,)" $
            testMergeableSimpleEquivClass
              ([1 :: Integer], [ssym "b" :: AsKey SymBool, ssym "c"])
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int)
              ]
              [ ( ssym "a",
                  ([1], [ssym "c", ssym "d"]),
                  ([1], [ssym "f", ssym "g"]),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ]
                  )
                )
              ],
          testCase "(,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int)
              ]
              [ ( ssym "a",
                  ([1], [ssym "c", ssym "d"], ssym "e"),
                  ([1], [ssym "f", ssym "g"], ssym "h"),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h")
                  )
                )
              ],
          testCase "(,,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool,
                [ssym "f" :: AsKey SymBool]
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx (1 :: Int)
              ]
              [ ( ssym "a",
                  ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"]),
                  ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"]),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h"),
                    [symIte (ssym "a") (ssym "i") (ssym "j")]
                  )
                )
              ],
          testCase "(,,,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool,
                [ssym "f" :: AsKey SymBool],
                [2 :: Integer, 3]
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [2 :: Integer, 3]
              ]
              [ ( ssym "a",
                  ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3]),
                  ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3]),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h"),
                    [symIte (ssym "a") (ssym "i") (ssym "j")],
                    [2, 3]
                  )
                )
              ],
          testCase "(,,,,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool,
                [ssym "f" :: AsKey SymBool],
                [2 :: Integer, 3],
                2 :: Integer
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [2 :: Integer, 3],
                DynamicSortedIdx (2 :: Integer)
              ]
              [ ( ssym "a",
                  ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3], 2),
                  ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3], 2),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h"),
                    [symIte (ssym "a") (ssym "i") (ssym "j")],
                    [2, 3],
                    2
                  )
                )
              ],
          testCase "(,,,,,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool,
                [ssym "f" :: AsKey SymBool],
                [2 :: Integer, 3],
                2 :: Integer,
                Just (ssym "a" :: AsKey SymBool)
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [2 :: Integer, 3],
                DynamicSortedIdx (2 :: Integer),
                DynamicSortedIdx True
              ]
              [ ( ssym "a",
                  ( [1],
                    [ssym "c", ssym "d"],
                    ssym "e",
                    [ssym "i"],
                    [2, 3],
                    2,
                    Just (ssym "k")
                  ),
                  ( [1],
                    [ssym "f", ssym "g"],
                    ssym "h",
                    [ssym "j"],
                    [2, 3],
                    2,
                    Just (ssym "l")
                  ),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h"),
                    [symIte (ssym "a") (ssym "i") (ssym "j")],
                    [2, 3],
                    2,
                    Just $ symIte (ssym "a") (ssym "k") (ssym "l")
                  )
                )
              ],
          testCase "(,,,,,,,)" $
            testMergeableSimpleEquivClass
              ( [1 :: Integer],
                [ssym "b" :: AsKey SymBool, ssym "c"],
                ssym "d" :: AsKey SymBool,
                [ssym "f" :: AsKey SymBool],
                [2 :: Integer, 3],
                2 :: Integer,
                Just (ssym "a" :: AsKey SymBool),
                Left 1 :: Either Integer Integer
              )
              [ DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [1 :: Integer],
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx (1 :: Int),
                DynamicSortedIdx (2 :: Int),
                DynamicSortedIdx $
                  buildStrategyList rootStrategy [2 :: Integer, 3],
                DynamicSortedIdx (2 :: Integer),
                DynamicSortedIdx True,
                DynamicSortedIdx False,
                DynamicSortedIdx (1 :: Integer)
              ]
              [ ( ssym "a",
                  ( [1],
                    [ssym "c", ssym "d"],
                    ssym "e",
                    [ssym "i"],
                    [2, 3],
                    2,
                    Just (ssym "k"),
                    Left 1
                  ),
                  ( [1],
                    [ssym "f", ssym "g"],
                    ssym "h",
                    [ssym "j"],
                    [2, 3],
                    2,
                    Just (ssym "l"),
                    Left 1
                  ),
                  ( [1],
                    [ symIte (ssym "a") (ssym "c") (ssym "f"),
                      symIte (ssym "a") (ssym "d") (ssym "g")
                    ],
                    symIte (ssym "a") (ssym "e") (ssym "h"),
                    [symIte (ssym "a") (ssym "i") (ssym "j")],
                    [2, 3],
                    2,
                    Just $ symIte (ssym "a") (ssym "k") (ssym "l"),
                    Left 1
                  )
                )
              ],
          let f1 :: Maybe (AsKey SymBool) -> AsKey SymBool =
                \case Just x -> x; Nothing -> (con True)
              f2 :: Maybe (AsKey SymBool) -> AsKey SymBool =
                \case Just x -> (symNot x); Nothing -> (con False)
           in testGroup
                "Function"
                [ testCase "Simply mergeable result" $ do
                    case rootStrategy ::
                           MergingStrategy (Maybe (AsKey SymBool) -> AsKey SymBool) of
                      SimpleStrategy f -> do
                        let r = f (ssym "a") f1 f2
                        r (Just (ssym "x"))
                          @?= symIte (ssym "a") (ssym "x") (symNot (ssym "x"))
                        r Nothing @?= symIte (ssym "a") (con True) (con False)
                      _ -> assertFailure "Bad mergeable strategy type",
                  testCase "Other mergeable result" $ do
                    case rootStrategy ::
                           MergingStrategy (Maybe SymBool -> Integer) of
                      NoStrategy -> return ()
                      _ -> assertFailure "Bad mergeable strategy type"
                ],
          testGroup
            "MaybeT"
            [ testGroup
                "MaybeT Maybe Integer"
                [ testCase "MaybeT Nothing" $
                    testMergeableSimpleEquivClass
                      (MaybeT Nothing :: MaybeT Maybe Integer)
                      [DynamicSortedIdx False]
                      [ ( ssym "a",
                          MaybeT Nothing,
                          MaybeT Nothing,
                          MaybeT Nothing
                        )
                      ],
                  testCase "MaybeT (Just Nothing)" $
                    testMergeableSimpleEquivClass
                      (MaybeT $ Just Nothing :: MaybeT Maybe Integer)
                      [DynamicSortedIdx True, DynamicSortedIdx False]
                      [ ( ssym "a",
                          MaybeT $ Just Nothing,
                          MaybeT $ Just Nothing,
                          MaybeT $ Just Nothing
                        )
                      ],
                  testProperty "MaybeT (Just (Just v))" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        (MaybeT $ Just $ Just x :: MaybeT Maybe Integer)
                        [ DynamicSortedIdx True,
                          DynamicSortedIdx True,
                          DynamicSortedIdx x
                        ]
                        [ ( ssym "a",
                            MaybeT $ Just $ Just x,
                            MaybeT $ Just $ Just x,
                            MaybeT $ Just $ Just x
                          )
                        ]
                ],
              testCase "MaybeT Maybe SymBool / MaybeT (Just (Just v))" $ do
                let (idxsJ, SimpleStrategy fJ) =
                      resolveStrategy
                        rootStrategy
                        ( MaybeT (Just (Just (ssym "a"))) ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                idxsJ @?= [DynamicSortedIdx True, DynamicSortedIdx True]
                fJ
                  (ssym "a")
                  (MaybeT $ Just $ Just $ ssym "b")
                  (MaybeT $ Just $ Just $ ssym "c")
                  @?= MaybeT
                    (Just (Just (symIte (ssym "a") (ssym "b") (ssym "c"))))
            ],
          testGroup
            "ExceptT"
            [ testGroup
                "ExceptT Integer Maybe Integer"
                [ testCase "ExceptT Nothing" $
                    testMergeableSimpleEquivClass
                      (ExceptT Nothing :: ExceptT Integer Maybe Integer)
                      [DynamicSortedIdx False]
                      [ ( ssym "a",
                          ExceptT Nothing,
                          ExceptT Nothing,
                          ExceptT Nothing
                        )
                      ],
                  testProperty "ExceptT (Just (Left v))" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        ( ExceptT $ Just $ Left x ::
                            ExceptT Integer Maybe Integer
                        )
                        [ DynamicSortedIdx True,
                          DynamicSortedIdx False,
                          DynamicSortedIdx x
                        ]
                        [ ( ssym "a",
                            ExceptT $ Just $ Left x,
                            ExceptT $ Just $ Left x,
                            ExceptT $ Just $ Left x
                          )
                        ],
                  testProperty "ExceptT (Just (Right v))" $
                    ioProperty . \(x :: Integer) -> do
                      testMergeableSimpleEquivClass
                        ( ExceptT $ Just $ Right x ::
                            ExceptT Integer Maybe Integer
                        )
                        [ DynamicSortedIdx True,
                          DynamicSortedIdx True,
                          DynamicSortedIdx x
                        ]
                        [ ( ssym "a",
                            ExceptT $ Just $ Right x,
                            ExceptT $ Just $ Right x,
                            ExceptT $ Just $ Right x
                          )
                        ]
                ],
              testGroup
                "ExceptT SymBool Maybe SymBool"
                [ testCase "ExceptT (Just (Left v))" $ do
                    let (idxsJL, SimpleStrategy fJL) =
                          resolveStrategy
                            rootStrategy
                            ( ExceptT (Just (Left (ssym "a"))) ::
                                ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                            )
                    idxsJL @?= [DynamicSortedIdx True, DynamicSortedIdx False]
                    fJL
                      (ssym "a")
                      (ExceptT $ Just $ Left $ ssym "b")
                      (ExceptT $ Just $ Left $ ssym "c")
                      @?= ExceptT
                        (Just (Left (symIte (ssym "a") (ssym "b") (ssym "c")))),
                  testCase "ExceptT (Just (Right v))" $ do
                    let (idxsJR, SimpleStrategy fJR) =
                          resolveStrategy
                            rootStrategy
                            ( ExceptT (Just (Right (ssym "a"))) ::
                                ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                            )
                    idxsJR @?= [DynamicSortedIdx True, DynamicSortedIdx True]
                    fJR
                      (ssym "a")
                      (ExceptT $ Just $ Right $ ssym "b")
                      (ExceptT $ Just $ Right $ ssym "c")
                      @?= ExceptT
                        (Just (Right (symIte (ssym "a") (ssym "b") (ssym "c"))))
                ]
            ],
          testGroup
            "StateT"
            [ testCase "Lazy StateT" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          (StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool))
                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 = s (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)),
              testCase "Strict StateT" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          (StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool))
                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 = s (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))
            ],
          testCase "ContT" $ do
            let SimpleStrategy s =
                  rootStrategy ::
                    MergingStrategy
                      (ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer))
            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 = s (ssym "c") c1 c2
            runContT
              c3
              ( \(a, x) ->
                  mrgIf
                    (ssym "p")
                    (mrgSingle (a, x))
                    (mrgSingle (symNot a, x + 1))
              )
              @?= 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))
                ),
          testGroup
            "RWST"
            [ testCase "Lazy RWST" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          ( RWSTLazy.RWST
                              (Integer, AsKey SymBool)
                              (Integer, AsKey SymBool)
                              (Integer, AsKey SymBool)
                              (AsKey1 Union)
                              (Integer, AsKey SymBool)
                          )
                let rws1 ::
                      RWSTLazy.RWST
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTLazy.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .&& bs),
                              (ir - is, br .|| bs),
                              (ir * is, bs .&& br)
                            )
                let rws2 ::
                      RWSTLazy.RWST
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTLazy.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .|| bs),
                              (ir - is, br .&& bs),
                              (ir * is, bs .|| br)
                            )
                let rws3 = s (ssym "c") rws1 rws2

                let res1 ::
                      AsKey1
                        Union
                        ( (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool)
                        ) =
                        mrgIf
                          (ssym "c")
                          ( mrgSingle
                              ( (1, ssym "a" .&& ssym "b"),
                                (-1, ssym "a" .|| ssym "b"),
                                (0, ssym "b" .&& ssym "a")
                              )
                          )
                          ( mrgSingle
                              ( (1, ssym "a" .|| ssym "b"),
                                (-1, ssym "a" .&& ssym "b"),
                                (0, ssym "b" .|| ssym "a")
                              )
                          )
                RWSTLazy.runRWST rws3 (0, ssym "a") (1, ssym "b") @?= res1,
              testCase "Strict RWST" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          ( RWSTStrict.RWST
                              (Integer, AsKey SymBool)
                              (Integer, AsKey SymBool)
                              (Integer, AsKey SymBool)
                              (AsKey1 Union)
                              (Integer, AsKey SymBool)
                          )
                let rws1 ::
                      RWSTStrict.RWST
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTStrict.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .&& bs),
                              (ir - is, br .|| bs),
                              (ir * is, bs .&& br)
                            )
                let rws2 ::
                      RWSTStrict.RWST
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (Integer, AsKey SymBool)
                        (AsKey1 Union)
                        (Integer, AsKey SymBool) =
                        RWSTStrict.RWST $ \(ir, br) (is, bs) ->
                          mrgSingle
                            ( (ir + is, br .|| bs),
                              (ir - is, br .&& bs),
                              (ir * is, bs .|| br)
                            )
                let rws3 = s (ssym "c") rws1 rws2

                let res1 ::
                      AsKey1
                        Union
                        ( (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool),
                          (Integer, AsKey SymBool)
                        ) =
                        mrgIf
                          (ssym "c")
                          ( mrgSingle
                              ( (1, "a" .&& "b"),
                                (-1, "a" .|| "b"),
                                (0, "b" .&& "a")
                              )
                          )
                          ( mrgSingle
                              ( (1, "a" .|| "b"),
                                (-1, "a" .&& "b"),
                                (0, "b" .|| "a")
                              )
                          )
                RWSTStrict.runRWST rws3 (0, ssym "a") (1, ssym "b") @?= res1
            ],
          testGroup
            "WriterT"
            [ testCase "Lazy WriterT" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          (WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool))
                let w1 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterLazy.WriterT $ mrgSingle (ssym "a", 1)
                let w2 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterLazy.WriterT $ mrgSingle (ssym "b", 2)
                let w3 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterLazy.WriterT $ mrgSingle (ssym "c", 1)
                let w4 = s (ssym "d") w1 w2
                let w5 = s (ssym "d") w1 w3
                WriterLazy.runWriterT w4
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterLazy.runWriterT w5
                  @?= mrgSingle (symIte (ssym "d") (ssym "a") (ssym "c"), 1),
              testCase "Strict WriterT" $ do
                let SimpleStrategy s =
                      rootStrategy ::
                        MergingStrategy
                          (WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool))
                let w1 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterStrict.WriterT $ mrgSingle (ssym "a", 1)
                let w2 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterStrict.WriterT $ mrgSingle (ssym "b", 2)
                let w3 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool) =
                      WriterStrict.WriterT $ mrgSingle (ssym "c", 1)
                let w4 = s (ssym "d") w1 w2
                let w5 = s (ssym "d") w1 w3
                WriterStrict.runWriterT w4
                  @?= mrgIf
                    (ssym "d")
                    (mrgSingle (ssym "a", 1))
                    (mrgSingle (ssym "b", 2))
                WriterStrict.runWriterT w5
                  @?= mrgSingle (symIte (ssym "d") (ssym "a") (ssym "c"), 1)
            ],
          testCase "ReaderT" $ do
            let SimpleStrategy s =
                  rootStrategy ::
                    MergingStrategy (ReaderT Integer (AsKey1 Union) Integer)
            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 = s (ssym "c") r1 r2
            runReaderT r3 2 @?= mrgSingle 4
            runReaderT r3 3 @?= mrgIf (ssym "c") (mrgSingle 5) (mrgSingle 6),
          testGroup
            "Identity"
            [ testProperty "Identity Integer" $
                ioProperty . \x -> do
                  testMergeableSimpleEquivClass
                    (Identity x :: Identity Integer)
                    [DynamicSortedIdx x]
                    [(ssym "a", Identity x, Identity x, Identity x)],
              testCase "Identity SymBool" $ do
                testMergeableSimpleEquivClass
                  (Identity (ssym "a" :: AsKey SymBool))
                  []
                  [ ( ssym "a",
                      Identity $ ssym "b",
                      Identity $ ssym "c",
                      Identity $ symIte (ssym "a") (ssym "b") (ssym "c")
                    )
                  ]
            ],
          testGroup
            "IdentityT Maybe Integer"
            [ testGroup
                "IdentityT Maybe Integer"
                [ testCase "IdentityT Nothing" $
                    testMergeableSimpleEquivClass
                      (IdentityT Nothing :: IdentityT Maybe Integer)
                      [DynamicSortedIdx False]
                      [ ( ssym "a",
                          IdentityT Nothing,
                          IdentityT Nothing,
                          IdentityT Nothing
                        )
                      ],
                  testProperty "IdentityT (Just v)" $
                    ioProperty . \x -> do
                      testMergeableSimpleEquivClass
                        (IdentityT $ Just x :: IdentityT Maybe Integer)
                        [DynamicSortedIdx True, DynamicSortedIdx x]
                        [ ( ssym "a",
                            IdentityT $ Just x,
                            IdentityT $ Just x,
                            IdentityT $ Just x
                          )
                        ]
                ],
              testGroup
                "IdentityT Maybe SymBool"
                [ testCase "IdentityT Nothing" $
                    testMergeableSimpleEquivClass
                      (IdentityT Nothing :: IdentityT Maybe (AsKey SymBool))
                      [DynamicSortedIdx False]
                      [ ( ssym "a",
                          IdentityT Nothing,
                          IdentityT Nothing,
                          IdentityT Nothing
                        )
                      ],
                  testCase "IdentityT (Just v)" $
                    testMergeableSimpleEquivClass
                      (IdentityT $ Just $ ssym "a" :: IdentityT Maybe (AsKey SymBool))
                      [DynamicSortedIdx True]
                      [ ( ssym "a",
                          IdentityT $ Just $ ssym "b",
                          IdentityT $ Just $ ssym "c",
                          IdentityT $
                            Just $
                              symIte (ssym "a") (ssym "b") (ssym "c")
                        )
                      ]
                ]
            ],
          testGroup
            "Sum"
            [ testGroup
                "Sum Maybe Maybe Integer"
                [ testCase "InL Nothing" $
                    testMergeableSimpleEquivClass
                      (InL Nothing :: Sum Maybe Maybe Integer)
                      [DynamicSortedIdx False, DynamicSortedIdx False]
                      [(ssym "a", InL Nothing, InL Nothing, InL Nothing)],
                  testProperty "InL (Just v)" $
                    ioProperty . \x -> do
                      testMergeableSimpleEquivClass
                        (InL $ Just x :: Sum Maybe Maybe Integer)
                        [ DynamicSortedIdx False,
                          DynamicSortedIdx True,
                          DynamicSortedIdx x
                        ]
                        [(ssym "a", InL $ Just x, InL $ Just x, InL $ Just x)],
                  testCase "InR Nothing" $
                    testMergeableSimpleEquivClass
                      (InR Nothing :: Sum Maybe Maybe Integer)
                      [DynamicSortedIdx True, DynamicSortedIdx False]
                      [(ssym "a", InR Nothing, InR Nothing, InR Nothing)],
                  testProperty "InR (Just v)" $
                    ioProperty . \x -> do
                      testMergeableSimpleEquivClass
                        (InR $ Just x :: Sum Maybe Maybe Integer)
                        [ DynamicSortedIdx True,
                          DynamicSortedIdx True,
                          DynamicSortedIdx x
                        ]
                        [(ssym "a", InR $ Just x, InR $ Just x, InR $ Just x)]
                ],
              testGroup
                "Sum Maybe Maybe SymBool"
                [ testCase "InL Nothing" $
                    testMergeableSimpleEquivClass
                      (InL Nothing :: Sum Maybe Maybe (AsKey SymBool))
                      [DynamicSortedIdx False, DynamicSortedIdx False]
                      [(ssym "a", InL Nothing, InL Nothing, InL Nothing)],
                  testCase "InL (Just v)" $
                    testMergeableSimpleEquivClass
                      (InL $ Just $ ssym "a" :: Sum Maybe Maybe (AsKey SymBool))
                      [DynamicSortedIdx False, DynamicSortedIdx True]
                      [ ( ssym "a",
                          InL $ Just $ ssym "b",
                          InL $ Just $ ssym "c",
                          InL $ Just $ symIte (ssym "a") (ssym "b") (ssym "c")
                        )
                      ],
                  testCase "InR Nothing" $
                    testMergeableSimpleEquivClass
                      (InR Nothing :: Sum Maybe Maybe (AsKey SymBool))
                      [DynamicSortedIdx True, DynamicSortedIdx False]
                      [(ssym "a", InR Nothing, InR Nothing, InR Nothing)],
                  testCase "InR (Just v)" $
                    testMergeableSimpleEquivClass
                      (InR $ Just $ ssym "a" :: Sum Maybe Maybe (AsKey SymBool))
                      [DynamicSortedIdx True, DynamicSortedIdx True]
                      [ ( ssym "a",
                          InR $ Just $ ssym "b",
                          InR $ Just $ ssym "c",
                          InR $ Just $ symIte (ssym "a") (ssym "b") (ssym "c")
                        )
                      ]
                ]
            ],
          testGroup
            "Ordering"
            [ testCase "LT" $
                testMergeableSimpleEquivClass
                  LT
                  [DynamicSortedIdx LT]
                  [(ssym "a", LT, LT, LT)],
              testCase "EQ" $
                testMergeableSimpleEquivClass
                  EQ
                  [DynamicSortedIdx EQ]
                  [(ssym "a", EQ, EQ, EQ)],
              testCase "GT" $
                testMergeableSimpleEquivClass
                  GT
                  [DynamicSortedIdx GT]
                  [(ssym "a", GT, GT, GT)]
            ]
        ]
    ]