content: {-# 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)]
              ]
          ]
      ]
  