content: {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
  
  module Grisette.Core.Data.UnionBaseTests (unionBaseTests) where
  
  import GHC.Generics (Generic)
  import Grisette
    ( AsKey (AsKey),
      ITEOp (symIte),
      LogicalOp (symNot, (.&&), (.||)),
      Mergeable (rootStrategy),
      MergingStrategy (SortedStrategy),
      Solvable (con),
      SymInteger,
      wrapStrategy,
    )
  import Grisette.Internal.Core.Data.UnionBase
    ( UnionBase (UnionIf, UnionSingle),
      fullReconstruct,
      ifWithLeftMost,
      ifWithStrategy,
    )
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.HUnit ((@?=))
  
  data TripleSum a b c = TS1 a | TS2 b | TS3 c deriving (Show, Eq, Generic)
  
  instance
    (Mergeable a, Mergeable b, Mergeable c) =>
    Mergeable (TripleSum a b c)
    where
    rootStrategy =
      SortedStrategy
        (\case TS1 _ -> (0 :: Int); TS2 _ -> (1 :: Int); TS3 _ -> (2 :: Int))
        ( \case
            0 -> wrapStrategy rootStrategy TS1 (\(TS1 x) -> x)
            1 -> wrapStrategy rootStrategy TS2 (\(TS2 x) -> x)
            2 -> wrapStrategy rootStrategy TS3 (\(TS3 x) -> x)
            _ -> error "Bad"
        )
  
  unionBaseTests :: Test
  unionBaseTests =
    testGroup
      "UnionBase"
      [ testGroup
          "ifWithLeftMost"
          [ testCase
              "ifWithLeftMost should maintain left most info on Singles"
              $ do
                AsKey
                  ( ifWithLeftMost
                      False
                      "a"
                      (UnionSingle (1 :: Integer))
                      (UnionSingle 2)
                  )
                  @?= AsKey (UnionIf 1 False "a" (UnionSingle 1) (UnionSingle 2)),
            testCase "ifWithLeftMost should maintain left most info on Ifs" $ do
              AsKey
                ( ifWithLeftMost
                    True
                    "a"
                    ( UnionIf
                        1
                        True
                        "b"
                        (UnionSingle (1 :: Integer))
                        (UnionSingle 2)
                    )
                    (UnionIf 3 True "c" (UnionSingle 3) (UnionSingle 4))
                )
                @?= AsKey
                  ( UnionIf
                      1
                      True
                      "a"
                      ( UnionIf
                          1
                          True
                          "b"
                          (UnionSingle (1 :: Integer))
                          (UnionSingle 2)
                      )
                      (UnionIf 3 True "c" (UnionSingle 3) (UnionSingle 4))
                  )
          ],
        testGroup
          "ifWithStrategy"
          [ testGroup
              "ifWithStrategy with concrete condition"
              [ testCase "true" $ do
                  AsKey
                    ( ifWithStrategy
                        rootStrategy
                        (con True)
                        (UnionSingle (1 :: Integer))
                        (UnionSingle 2)
                    )
                    @?= AsKey (UnionSingle 1),
                testCase "false" $ do
                  AsKey
                    ( ifWithStrategy
                        rootStrategy
                        (con False)
                        (UnionSingle (1 :: Integer))
                        (UnionSingle 2)
                    )
                    @?= AsKey (UnionSingle 2)
              ],
            let a =
                  ifWithStrategy
                    rootStrategy
                    "a"
                    (UnionSingle (1 :: Integer))
                    (UnionSingle 2)
             in testGroup
                  "ifWithStrategy with condition equal to sub conditions"
                  [ testCase "ifTrue" $ do
                      AsKey
                        (ifWithStrategy rootStrategy "a" a (UnionSingle 3))
                        @?= AsKey (UnionIf 1 True "a" (UnionSingle 1) (UnionSingle 3)),
                    testCase "ifFalse" $ do
                      AsKey
                        (ifWithStrategy rootStrategy "a" (UnionSingle 0) a)
                        @?= AsKey (UnionIf 0 True "a" (UnionSingle 0) (UnionSingle 2))
                  ],
            testCase "ifWithStrategy with simple mergeables" $ do
              AsKey
                ( ifWithStrategy
                    rootStrategy
                    "a"
                    (UnionSingle ("b" :: AsKey SymInteger))
                    (UnionSingle "c")
                )
                @?= AsKey (UnionSingle (symIte "a" "b" "c")),
            testGroup
              "ifWithStrategy with ordered mergeables"
              [ testGroup
                  "ifWithStrategy on Single/Single"
                  [ testGroup
                      "idxt < idxf"
                      [ testCase "Integer" $
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle (1 :: Integer))
                                (UnionSingle 2)
                            )
                            @?= AsKey
                              ( UnionIf
                                  1
                                  True
                                  "a"
                                  (UnionSingle 1)
                                  (UnionSingle 2)
                              ),
                        testCase "Maybe Integer" $
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle Nothing)
                                (UnionSingle (Just (2 :: Integer)))
                            )
                            @?= AsKey
                              ( UnionIf
                                  Nothing
                                  True
                                  "a"
                                  (UnionSingle Nothing)
                                  (UnionSingle (Just 2))
                              )
                      ],
                    testGroup
                      "idxt == idxf"
                      [ testGroup
                          "idxt == idxf as terminal"
                          [ testCase "Integer" $
                              AsKey
                                ( ifWithStrategy
                                    rootStrategy
                                    "a"
                                    (UnionSingle (1 :: Integer))
                                    (UnionSingle 1)
                                )
                                @?= AsKey (UnionSingle 1),
                            testCase "Maybe Integer" $
                              AsKey
                                ( ifWithStrategy
                                    rootStrategy
                                    "a"
                                    (UnionSingle (Just ("b" :: AsKey SymInteger)))
                                    (UnionSingle (Just "c"))
                                )
                                @?= AsKey (UnionSingle (Just (symIte "a" "b" "c")))
                          ],
                        testGroup
                          "idxt == idxf but not terminal"
                          [ testCase "Maybe Integer" $
                              AsKey
                                ( ifWithStrategy
                                    rootStrategy
                                    "a"
                                    (UnionSingle (Just (1 :: Integer)))
                                    (UnionSingle (Just (2 :: Integer)))
                                )
                                @?= AsKey
                                  ( UnionIf
                                      (Just 1)
                                      True
                                      "a"
                                      (UnionSingle $ Just 1)
                                      (UnionSingle (Just 2))
                                  ),
                            testCase "Maybe (Maybe Integer)" $
                              AsKey
                                ( ifWithStrategy
                                    rootStrategy
                                    "a"
                                    (UnionSingle $ Just $ Just ("b" :: AsKey SymInteger))
                                    (UnionSingle $ Just $ Just "c")
                                )
                                @?= AsKey (UnionSingle (Just (Just (symIte "a" "b" "c"))))
                          ]
                      ],
                    testGroup
                      "idxt > idxf"
                      [ testCase "Integer" $
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle (2 :: Integer))
                                (UnionSingle 1)
                            )
                            @?= AsKey
                              ( UnionIf
                                  1
                                  True
                                  (symNot "a")
                                  (UnionSingle 1)
                                  (UnionSingle 2)
                              ),
                        testCase "Maybe Integer" $
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle (Just (2 :: Integer)))
                                (UnionSingle Nothing)
                            )
                            @?= AsKey
                              ( UnionIf
                                  Nothing
                                  True
                                  (symNot "a")
                                  (UnionSingle Nothing)
                                  (UnionSingle (Just 2))
                              )
                      ]
                  ],
                testGroup
                  "ifWithStrategy on Single/If"
                  [ testGroup
                      "Degenerate to Single/Single when idxft == idxff"
                      [ testCase "Degenerated case with idxt < idxf" $ do
                          let x =
                                ifWithStrategy
                                  rootStrategy
                                  "a"
                                  (UnionSingle (Just (1 :: Integer)))
                                  (UnionSingle (Just (2 :: Integer)))
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "b"
                                (UnionSingle Nothing)
                                x
                            )
                            @?= AsKey
                              ( UnionIf
                                  Nothing
                                  True
                                  "b"
                                  (UnionSingle Nothing)
                                  ( UnionIf
                                      (Just 1)
                                      True
                                      "a"
                                      (UnionSingle $ Just 1)
                                      (UnionSingle (Just 2))
                                  )
                              ),
                        let x =
                              ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle (Just (1 :: Integer)))
                                (UnionSingle (Just (3 :: Integer)))
                         in testGroup
                              "Degenerated case with idxt == idxf"
                              [ testCase "sub-idxt < sub-idxft" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        (UnionSingle $ Just 0)
                                        x
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 0)
                                          True
                                          "b"
                                          (UnionSingle $ Just 0)
                                          ( UnionIf
                                              (Just 1)
                                              True
                                              "a"
                                              (UnionSingle $ Just 1)
                                              (UnionSingle (Just 3))
                                          )
                                      ),
                                testCase "sub-idxt == sub-idxft" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        (UnionSingle $ Just 1)
                                        x
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ("b" .|| "a")
                                          (UnionSingle $ Just 1)
                                          (UnionSingle (Just 3))
                                      ),
                                testCase "subidxft < sub-idxt < sub-idxff" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        (UnionSingle $ Just 2)
                                        x
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ((symNot "b") .&& "a")
                                          (UnionSingle $ Just 1)
                                          ( UnionIf
                                              (Just 2)
                                              True
                                              "b"
                                              (UnionSingle $ Just 2)
                                              (UnionSingle $ Just 3)
                                          )
                                      ),
                                testCase "sub-idxt == sub-idxff" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        (UnionSingle $ Just 3)
                                        x
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ((symNot "b") .&& "a")
                                          (UnionSingle $ Just 1)
                                          (UnionSingle (Just 3))
                                      ),
                                testCase "sub-idxff < sub-idxt" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        (UnionSingle $ Just 4)
                                        x
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ((symNot "b") .&& "a")
                                          (UnionSingle $ Just 1)
                                          ( UnionIf
                                              (Just 3)
                                              True
                                              (symNot "b")
                                              (UnionSingle $ Just 3)
                                              (UnionSingle $ Just 4)
                                          )
                                      )
                              ],
                        testCase "Degenerated case with idxt > idxf" $ do
                          let x =
                                ifWithStrategy
                                  rootStrategy
                                  "a"
                                  (UnionSingle (Left (1 :: Integer)))
                                  (UnionSingle (Left (2 :: Integer)))
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "b"
                                (UnionSingle $ Right (1 :: Integer))
                                x
                            )
                            @?= AsKey
                              ( UnionIf
                                  (Left 1)
                                  True
                                  (symNot "b")
                                  ( UnionIf
                                      (Left 1)
                                      True
                                      "a"
                                      (UnionSingle $ Left 1)
                                      (UnionSingle (Left 2))
                                  )
                                  (UnionSingle $ Right 1)
                              )
                      ],
                    testCase "idxt < idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle (1 :: Integer))
                              (UnionSingle (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            (UnionSingle 0)
                            x
                        )
                        @?= AsKey
                          ( UnionIf
                              0
                              True
                              "b"
                              (UnionSingle 0)
                              ( UnionIf
                                  1
                                  True
                                  "a"
                                  (UnionSingle 1)
                                  (UnionSingle 3)
                              )
                          ),
                    testCase "idxt == idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            (UnionSingle $ Left 0)
                            x
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 0)
                              True
                              ("b" .|| "a")
                              ( UnionIf
                                  (Left 0)
                                  True
                                  "b"
                                  (UnionSingle $ Left 0)
                                  (UnionSingle $ Left 1)
                              )
                              (UnionSingle $ Right 3)
                          ),
                    testCase "idxt > idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            (UnionSingle $ Right 0)
                            x
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 1)
                              True
                              ((symNot "b") .&& "a")
                              (UnionSingle $ Left 1)
                              ( UnionIf
                                  (Right 0)
                                  True
                                  "b"
                                  (UnionSingle $ Right 0)
                                  (UnionSingle $ Right 3)
                              )
                          )
                  ],
                testGroup
                  "ifWithStrategy on If/Single"
                  [ testGroup
                      "Degenerate to Single/Single when idxtt == idxtf"
                      [ testCase "Degenerated case with idxt < idxf" $ do
                          let x =
                                ifWithStrategy
                                  rootStrategy
                                  "a"
                                  (UnionSingle (Left (1 :: Integer)))
                                  (UnionSingle (Left (2 :: Integer)))
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "b"
                                x
                                (UnionSingle $ Right (2 :: Integer))
                            )
                            @?= AsKey
                              ( UnionIf
                                  (Left 1)
                                  True
                                  "b"
                                  ( UnionIf
                                      (Left 1)
                                      True
                                      "a"
                                      (UnionSingle $ Left 1)
                                      (UnionSingle (Left 2))
                                  )
                                  (UnionSingle $ Right 2)
                              ),
                        let x =
                              ifWithStrategy
                                rootStrategy
                                "a"
                                (UnionSingle (Just (1 :: Integer)))
                                (UnionSingle (Just (3 :: Integer)))
                         in testGroup
                              "Degenerated case with idxt == idxf"
                              [ testCase "sub-idxf < sub-idxtt" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        x
                                        (UnionSingle $ Just 0)
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 0)
                                          True
                                          (symNot "b")
                                          (UnionSingle $ Just 0)
                                          ( UnionIf
                                              (Just 1)
                                              True
                                              "a"
                                              (UnionSingle $ Just 1)
                                              (UnionSingle (Just 3))
                                          )
                                      ),
                                testCase "sub-idxf == sub-idxtt" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        x
                                        (UnionSingle $ Just 1)
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ((symNot "b") .|| "a")
                                          (UnionSingle $ Just 1)
                                          (UnionSingle (Just 3))
                                      ),
                                testCase "sub-idxtt < sub-idxf < sub-idxtf" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        x
                                        (UnionSingle $ Just 2)
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ("b" .&& "a")
                                          (UnionSingle $ Just 1)
                                          ( UnionIf
                                              (Just 2)
                                              True
                                              (symNot "b")
                                              (UnionSingle $ Just 2)
                                              (UnionSingle $ Just 3)
                                          )
                                      ),
                                testCase "sub-idxf == sub-idxtf" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        x
                                        (UnionSingle $ Just 3)
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ("b" .&& "a")
                                          (UnionSingle $ Just 1)
                                          (UnionSingle (Just 3))
                                      ),
                                testCase "sub-idxtf < sub-idxf" $
                                  AsKey
                                    ( ifWithStrategy
                                        rootStrategy
                                        "b"
                                        x
                                        (UnionSingle $ Just 4)
                                    )
                                    @?= AsKey
                                      ( UnionIf
                                          (Just 1)
                                          True
                                          ("b" .&& "a")
                                          (UnionSingle $ Just 1)
                                          ( UnionIf
                                              (Just 3)
                                              True
                                              "b"
                                              (UnionSingle $ Just 3)
                                              (UnionSingle $ Just 4)
                                          )
                                      )
                              ],
                        testCase "Degenerated case with idxt > idxf" $ do
                          let x =
                                ifWithStrategy
                                  rootStrategy
                                  "a"
                                  (UnionSingle (Right (1 :: Integer)))
                                  (UnionSingle (Right (2 :: Integer)))
                          AsKey
                            ( ifWithStrategy
                                rootStrategy
                                "b"
                                x
                                (UnionSingle $ Left (1 :: Integer))
                            )
                            @?= AsKey
                              ( UnionIf
                                  (Left 1)
                                  True
                                  (symNot "b")
                                  (UnionSingle $ Left 1)
                                  ( UnionIf
                                      (Right 1)
                                      True
                                      "a"
                                      (UnionSingle $ Right 1)
                                      (UnionSingle (Right 2))
                                  )
                              )
                      ],
                    testCase "idxtt < idxf" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            x
                            (UnionSingle $ Right 0)
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 1)
                              True
                              ("b" .&& "a")
                              (UnionSingle $ Left 1)
                              ( UnionIf
                                  (Right 0)
                                  True
                                  (symNot "b")
                                  (UnionSingle $ Right 0)
                                  (UnionSingle $ Right 3)
                              )
                          ),
                    testCase "idxtt == idxf" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            x
                            (UnionSingle $ Left 0)
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 0)
                              True
                              ((symNot "b") .|| "a")
                              ( UnionIf
                                  (Left 0)
                                  True
                                  (symNot "b")
                                  (UnionSingle $ Left 0)
                                  (UnionSingle $ Left 1)
                              )
                              (UnionSingle $ Right 3)
                          ),
                    testCase "idxtt > idxf" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle (1 :: Integer))
                              (UnionSingle (3 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "b"
                            x
                            (UnionSingle 0)
                        )
                        @?= AsKey
                          ( UnionIf
                              0
                              True
                              (symNot "b")
                              (UnionSingle 0)
                              (UnionIf 1 True "a" (UnionSingle 1) (UnionSingle 3))
                          )
                  ],
                testGroup
                  "ifWithStrategy on If/If"
                  [ testCase "Degenerate to Single/If when idxtt == idxtf" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Left (2 :: Integer))
                      let y =
                            ifWithStrategy
                              rootStrategy
                              "b"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (2 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "c"
                            x
                            y
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 1)
                              True
                              ("c" .|| "b")
                              ( UnionIf
                                  (Left 1)
                                  True
                                  ((symNot "c") .|| "a")
                                  (UnionSingle $ Left 1)
                                  (UnionSingle $ Left 2)
                              )
                              (UnionSingle $ Right 2)
                          ),
                    testCase "Degenerate to Single/If when idxff == idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Left (2 :: Integer))
                      let y =
                            ifWithStrategy
                              rootStrategy
                              "b"
                              (UnionSingle $ Left (1 :: Integer))
                              (UnionSingle $ Right (2 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "c"
                            y
                            x
                        )
                        @?= AsKey
                          ( UnionIf
                              (Left 1)
                              True
                              ((symNot "c") .|| "b")
                              ( UnionIf
                                  (Left 1)
                                  True
                                  ("c" .|| "a")
                                  (UnionSingle $ Left 1)
                                  (UnionSingle $ Left 2)
                              )
                              (UnionSingle $ Right 2)
                          ),
                    testCase "Non-degenerated case when idxtt < idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ TS1 (1 :: Integer))
                              (UnionSingle $ TS2 (2 :: Integer))
                      let y =
                            ifWithStrategy
                              rootStrategy
                              "b"
                              (UnionSingle $ TS2 (1 :: Integer))
                              (UnionSingle $ TS3 (2 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "c"
                            x
                            y
                        )
                        @?= AsKey
                          ( UnionIf
                              (TS1 1)
                              True
                              ("c" .&& "a")
                              (UnionSingle $ TS1 1)
                              ( UnionIf
                                  (TS2 1)
                                  True
                                  ("c" .|| "b")
                                  ( UnionIf
                                      (TS2 1)
                                      True
                                      (symNot "c")
                                      (UnionSingle $ TS2 1)
                                      (UnionSingle $ TS2 2)
                                  )
                                  (UnionSingle $ TS3 2)
                              )
                          ),
                    testCase "Non-degenerated case when idxtt == idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ TS1 (1 :: Integer))
                              (UnionSingle $ TS2 (2 :: Integer))
                      let y =
                            ifWithStrategy
                              rootStrategy
                              "b"
                              (UnionSingle $ TS1 (2 :: Integer))
                              (UnionSingle $ TS3 (2 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "c"
                            x
                            y
                        )
                        @?= AsKey
                          ( UnionIf
                              (TS1 1)
                              True
                              (symIte "c" "a" "b")
                              ( UnionIf
                                  (TS1 1)
                                  True
                                  "c"
                                  (UnionSingle $ TS1 1)
                                  (UnionSingle $ TS1 2)
                              )
                              ( UnionIf
                                  (TS2 2)
                                  True
                                  "c"
                                  (UnionSingle $ TS2 2)
                                  (UnionSingle $ TS3 2)
                              )
                          ),
                    testCase "Non-degenerated case when idxtt > idxft" $ do
                      let x =
                            ifWithStrategy
                              rootStrategy
                              "a"
                              (UnionSingle $ TS2 (1 :: Integer))
                              (UnionSingle $ TS3 (2 :: Integer))
                      let y =
                            ifWithStrategy
                              rootStrategy
                              "b"
                              (UnionSingle $ TS1 (1 :: Integer))
                              (UnionSingle $ TS2 (2 :: Integer))
                      AsKey
                        ( ifWithStrategy
                            rootStrategy
                            "c"
                            x
                            y
                        )
                        @?= AsKey
                          ( UnionIf
                              (TS1 1)
                              True
                              ((symNot "c") .&& "b")
                              (UnionSingle $ TS1 1)
                              ( UnionIf
                                  (TS2 1)
                                  True
                                  ((symNot "c") .|| "a")
                                  ( UnionIf
                                      (TS2 1)
                                      True
                                      "c"
                                      (UnionSingle $ TS2 1)
                                      (UnionSingle $ TS2 2)
                                  )
                                  (UnionSingle $ TS3 2)
                              )
                          )
                  ],
                testCase "ifWithStrategy should tolerate non-merged Ifs" $ do
                  let x =
                        UnionIf
                          (Right 2)
                          False
                          "a"
                          (UnionSingle $ Right (2 :: Integer))
                          (UnionSingle $ Left (2 :: Integer))
                  let y =
                        UnionIf
                          (Right 3)
                          False
                          "b"
                          (UnionSingle $ Right 3)
                          (UnionSingle $ Left 1)
                  AsKey
                    ( ifWithStrategy
                        rootStrategy
                        "c"
                        x
                        y
                    )
                    @?= AsKey
                      ( UnionIf
                          (Left 1)
                          True
                          (symIte "c" (symNot "a") (symNot "b"))
                          ( UnionIf
                              (Left 1)
                              True
                              (symNot "c")
                              (UnionSingle $ Left 1)
                              (UnionSingle $ Left 2)
                          )
                          ( UnionIf
                              (Right 2)
                              True
                              "c"
                              (UnionSingle $ Right 2)
                              (UnionSingle $ Right 3)
                          )
                      )
              ]
          ],
        testGroup
          "fullReconstruct"
          [ testCase "fullReconstruct should work" $ do
              let x =
                    UnionIf
                      (Right 2)
                      False
                      "a"
                      (UnionSingle $ Right (2 :: Integer))
                      (UnionSingle $ Left (2 :: Integer))
              let y =
                    UnionIf
                      (Right 3)
                      False
                      "b"
                      (UnionSingle $ Right 3)
                      (UnionSingle $ Left 1)
              let z = UnionIf (Right 2) False "c" x y
              AsKey (fullReconstruct rootStrategy z)
                @?= AsKey
                  ( UnionIf
                      (Left 1)
                      True
                      (symIte "c" (symNot "a") (symNot "b"))
                      ( UnionIf
                          (Left 1)
                          True
                          (symNot "c")
                          (UnionSingle $ Left 1)
                          (UnionSingle $ Left 2)
                      )
                      ( UnionIf
                          (Right 2)
                          True
                          "c"
                          (UnionSingle $ Right 2)
                          (UnionSingle $ Right 3)
                      )
                  )
          ]
      ]
  