{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

module Grisette.Core.Data.Class.GenSymTests (genSymTests) where

import Control.Monad (replicateM)
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Data.Text as T
import Grisette
  ( AsKey,
    EnumGenBound (EnumGenBound),
    EnumGenUpperBound (EnumGenUpperBound),
    Fresh,
    FreshT,
    GenSymSimple (simpleFresh),
    ITEOp (symIte),
    ListSpec (ListSpec),
    MonadFresh (localIdentifier),
    SExpr (Atom),
    SimpleListSpec (SimpleListSpec),
    Solvable (con, isym, ssym),
    SymBool,
    choose,
    chooseFresh,
    chooseSimple,
    chooseSimpleFresh,
    chooseUnion,
    chooseUnionFresh,
    freshString,
    genSym,
    genSymSimple,
    liftFresh,
    mapMetadata,
    mrgIf,
    mrgSingle,
    runFresh,
    runFreshT,
    withMetadata,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.AsKey (AsKey1 (AsKey1))
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))

genSymTests :: Test
genSymTests =
  testGroup
    "GenSym"
    [ testGroup
        "GenSym for common types"
        [ testGroup
            "SymBool"
            [ testGroup
                "() spec"
                [ testCase "genSym" $
                    AsKey1 (genSym () "a" :: Union (AsKey SymBool))
                      @?= mrgSingle (isym "a" 0),
                  testCase "genSymSimple" $
                    (genSymSimple () "a" :: AsKey SymBool) @?= isym "a" 0
                ],
              testGroup
                "SymBool spec"
                [ testCase "genSym" $
                    AsKey1 (genSym (con True :: AsKey SymBool) "a" :: Union (AsKey SymBool))
                      @?= mrgSingle (isym "a" 0),
                  testCase "genSymSimple" $
                    (genSymSimple (con True :: AsKey SymBool) "a" :: AsKey SymBool)
                      @?= isym "a" 0
                ]
            ],
          testGroup
            "Bool"
            [ testCase "() spec" $
                AsKey1 (genSym () "a" :: Union Bool)
                  @?= AsKey1 (mrgIf (isym "a" 0) (mrgSingle False) (mrgSingle True)),
              testGroup
                "Bool spec"
                [ testGroup
                    "genSym"
                    [ testCase "True" $
                        AsKey1 (genSym True "a" :: Union Bool)
                          @?= mrgSingle True,
                      testCase "False" $
                        AsKey1 (genSym False "a" :: Union Bool)
                          @?= mrgSingle False
                    ],
                  testGroup
                    "genSymSimple"
                    [ testCase "True" $
                        (genSymSimple True "a" :: Bool)
                          @?= True,
                      testCase "False" $
                        (genSymSimple False "a" :: Bool)
                          @?= False
                    ]
                ]
            ],
          testGroup
            "Integer"
            [ testGroup
                "Integer spec"
                [ testCase "genSym" $
                    AsKey1 (genSym (1 :: Integer) "a" :: Union Integer)
                      @?= mrgSingle 1,
                  testCase "genSymSimple" $
                    (genSymSimple (1 :: Integer) "a" :: Integer)
                      @?= 1
                ],
              testCase "Upper bound spec" $
                AsKey1 (genSym (EnumGenUpperBound (3 :: Integer)) "a" :: Union Integer)
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle 0)
                    (mrgIf (isym "a" 1) (mrgSingle 1) (mrgSingle 2)),
              testCase "Bound spec" $
                AsKey1 (genSym (EnumGenBound (-1 :: Integer) 2) "a" :: Union Integer)
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle (-1))
                    (mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1))
            ],
          testGroup
            "Char"
            [ testGroup
                "Char spec"
                [ testCase "genSym" $
                    AsKey1 (genSym 'x' "a" :: Union Char)
                      @?= mrgSingle 'x',
                  testCase "genSymSimple" $
                    (genSymSimple 'x' "a" :: Char) @?= 'x'
                ],
              testCase "Upper bound spec" $
                AsKey1 (genSym (EnumGenUpperBound @Char (toEnum 3)) "a" :: Union Char)
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle $ toEnum 0)
                    ( mrgIf
                        (isym "a" 1)
                        (mrgSingle $ toEnum 1)
                        (mrgSingle $ toEnum 2)
                    ),
              testCase "Bound spec" $
                AsKey1 (genSym (EnumGenBound 'a' 'd') "a" :: Union Char)
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle 'a')
                    (mrgIf (isym "a" 1) (mrgSingle 'b') (mrgSingle 'c'))
            ],
          testGroup
            "Maybe SymBool"
            [ testGroup
                "Maybe SymBool spec"
                [ testGroup
                    "Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym (Nothing :: Maybe (AsKey SymBool)) "a" ::
                              Union (Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle Nothing,
                      testCase "genSymSimple" $
                        ( genSymSimple (Nothing :: Maybe (AsKey SymBool)) "a" ::
                            Maybe (AsKey SymBool)
                        )
                          @?= Nothing
                    ],
                  testGroup
                    "Just v"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym (Just (ssym "a" :: AsKey SymBool)) "a" ::
                              Union (Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (Just (isym "a" 0)),
                      testCase "genSymSimple" $
                        ( genSymSimple (Just (ssym "a" :: AsKey SymBool)) "a" ::
                            Maybe (AsKey SymBool)
                        )
                          @?= Just (isym "a" 0)
                    ]
                ],
              testCase "() spec" $
                AsKey1 (genSym () "a" :: Union (Maybe (AsKey SymBool)))
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle Nothing)
                    (mrgSingle (Just (isym "a" 1)))
            ],
          testGroup
            "Either SymBool SymBool"
            [ testGroup
                "Either SymBool SymBool spec"
                [ testGroup
                    "Left v"
                    [ testCase "genSym" $
                        ( AsKey1 $
                            genSym
                              ( Left (ssym "a") ::
                                  Either (AsKey SymBool) (AsKey SymBool)
                              )
                              "a" ::
                            AsKey1 Union (Either (AsKey SymBool) (AsKey SymBool))
                        )
                          @?= mrgSingle (Left (isym "a" 0)),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( Left (ssym "a") ::
                                Either (AsKey SymBool) (AsKey SymBool)
                            )
                            "a" ::
                            Either (AsKey SymBool) (AsKey SymBool)
                        )
                          @?= Left (isym "a" 0)
                    ],
                  testGroup
                    "Right v"
                    [ testCase "genSym" $
                        ( AsKey1 $
                            genSym
                              ( Right (ssym "a") ::
                                  Either (AsKey SymBool) (AsKey SymBool)
                              )
                              "a" ::
                            AsKey1 Union (Either (AsKey SymBool) (AsKey SymBool))
                        )
                          @?= mrgSingle (Right (isym "a" 0)),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( Right (ssym "a") ::
                                Either (AsKey SymBool) (AsKey SymBool)
                            )
                            "a" ::
                            Either (AsKey SymBool) (AsKey SymBool)
                        )
                          @?= Right (isym "a" 0)
                    ]
                ],
              testCase "() spec" $ do
                (AsKey1 (genSym () "a" :: Union (Either (AsKey SymBool) (AsKey SymBool))))
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle $ Left $ isym "a" 1)
                    (mrgSingle $ Right $ isym "a" 2)
            ],
          testGroup
            "lists"
            [ testGroup
                "Max length spec"
                [ testCase "max length = 0" $
                    AsKey1 (genSym (0 :: Integer) "a" :: Union [AsKey SymBool])
                      @?= mrgSingle [],
                  testCase "max length = 3" $
                    AsKey1 (genSym (3 :: Integer) "a" :: Union [AsKey SymBool])
                      @?= mrgIf
                        (isym "a" 3)
                        (mrgSingle [])
                        ( mrgIf
                            (isym "a" 4)
                            (mrgSingle [isym "a" 2])
                            ( mrgIf
                                (isym "a" 5)
                                (mrgSingle [isym "a" 1, isym "a" 2])
                                ( mrgSingle
                                    [ isym "a" 0,
                                      isym "a" 1,
                                      isym "a" 2
                                    ]
                                )
                            )
                        )
                ],
              testGroup
                "Min & max length spec"
                [ testCase "min length = 1, max length = 3" $
                    AsKey1 (genSym (ListSpec 1 3 ()) "a" :: Union [AsKey SymBool])
                      @?= mrgIf
                        (isym "a" 3)
                        (mrgSingle [isym "a" 2])
                        ( mrgIf
                            (isym "a" 4)
                            (mrgSingle [isym "a" 1, isym "a" 2])
                            ( mrgSingle
                                [ isym "a" 0,
                                  isym "a" 1,
                                  isym "a" 2
                                ]
                            )
                        ),
                  testCase "min length = 1, max length = 2, nested" $
                    AsKey1
                      ( genSym (ListSpec 1 2 (ListSpec 1 2 ())) "a" ::
                          Union [AsKey1 Union [AsKey SymBool]]
                      )
                      @?= mrgIf
                        (isym "a" 6)
                        ( mrgSingle
                            [ mrgIf
                                (isym "a" 5)
                                (mrgSingle [isym "a" 4])
                                (mrgSingle [isym "a" 3, isym "a" 4])
                            ]
                        )
                        ( mrgSingle
                            [ mrgIf
                                (isym "a" 2)
                                (mrgSingle [isym "a" 1])
                                (mrgSingle [isym "a" 0, isym "a" 1]),
                              mrgIf
                                (isym "a" 5)
                                (mrgSingle [isym "a" 4])
                                (mrgSingle [isym "a" 3, isym "a" 4])
                            ]
                        )
                ],
              testGroup
                "Exact length spec"
                [ testGroup
                    "length = 2"
                    [ testCase "genSym" $
                        AsKey1
                          (genSym (SimpleListSpec 2 ()) "a" :: Union [AsKey SymBool])
                          @?= mrgSingle [isym "a" 0, isym "a" 1],
                      testCase "genSymSimple" $
                        (genSymSimple (SimpleListSpec 2 ()) "a" :: [AsKey SymBool])
                          @?= [isym "a" 0, isym "a" 1]
                    ],
                  testGroup
                    "length = 2, nested"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              (SimpleListSpec 2 (SimpleListSpec 2 ()))
                              "a" ::
                              Union [[AsKey SymBool]]
                          )
                          @?= mrgSingle
                            [ [isym "a" 0, isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                      testCase "genSymSimple" $
                        ( genSymSimple
                            (SimpleListSpec 2 (SimpleListSpec 2 ()))
                            "a" ::
                            [[AsKey SymBool]]
                        )
                          @?= [ [isym "a" 0, isym "a" 1],
                                [isym "a" 2, isym "a" 3]
                              ]
                    ]
                ],
              testGroup
                "List with same shape spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          [[con True :: AsKey SymBool], [ssym "a", ssym "b"]]
                          "a" ::
                          Union [[AsKey SymBool]]
                      )
                      @?= mrgSingle
                        [ [isym "a" 0],
                          [isym "a" 1, isym "a" 2]
                        ],
                  testCase "genSymSimple" $
                    ( genSymSimple
                        [ [con True :: AsKey SymBool],
                          [ssym "a", ssym "b"]
                        ]
                        "a" ::
                        [[AsKey SymBool]]
                    )
                      @?= [[isym "a" 0], [isym "a" 1, isym "a" 2]]
                ]
            ],
          testGroup
            "()"
            [ testCase "() spec" $ do
                AsKey1 (genSym () "a" :: Union ()) @?= mrgSingle ()
                (genSymSimple () "a" :: ()) @?= ()
            ],
          testGroup
            "(,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union (Integer, Integer)
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [ [ssym "b" :: AsKey SymBool],
                            [ssym "b", ssym "c"]
                          ]
                        )
                        "a" ::
                        (AsKey SymBool, [[AsKey SymBool]])
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ]
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      (genSym () "a" :: Union (AsKey SymBool, AsKey SymBool))
                      @?= mrgSingle (isym "a" 0, isym "a" 1),
                  testCase "genSymSimple" $
                    (genSymSimple () "a" :: (AsKey SymBool, AsKey SymBool))
                      @?= (isym "a" 0, isym "a" 1)
                ]
            ],
          testGroup
            "(,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union (Integer, Integer, Integer)
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ((), [[ssym "b" :: AsKey SymBool], [ssym "b", ssym "c"]], ())
                        "a" ::
                        (AsKey SymBool, [[AsKey SymBool]], AsKey SymBool)
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      (genSym () "a" :: Union (AsKey SymBool, AsKey SymBool, AsKey SymBool))
                      @?= mrgSingle
                        (isym "a" 0, isym "a" 1, isym "a" 2),
                  testCase "genSymSimple" $
                    (genSymSimple () "a" :: (AsKey SymBool, AsKey SymBool, AsKey SymBool))
                      @?= (isym "a" 0, isym "a" 1, isym "a" 2)
                ]
            ],
          testGroup
            "(,,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union (Integer, Integer, Integer, Integer)
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        x4 <- mrgIf (isym "a" 3) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3, x4),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [[ssym "b" :: AsKey SymBool], [ssym "b", ssym "c"]],
                          (),
                          ()
                        )
                        "a" ::
                        (AsKey SymBool, [[AsKey SymBool]], AsKey SymBool, AsKey SymBool)
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4,
                            isym "a" 5
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym () "a" ::
                          Union (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool)
                      )
                      @?= mrgSingle
                        ( isym "a" 0,
                          isym "a" 1,
                          isym "a" 2,
                          isym "a" 3
                        ),
                  testCase "genSymSimple" $
                    ( genSymSimple () "a" ::
                        (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool)
                    )
                      @?= ( isym "a" 0,
                            isym "a" 1,
                            isym "a" 2,
                            isym "a" 3
                          )
                ]
            ],
          testGroup
            "(,,,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union (Integer, Integer, Integer, Integer, Integer)
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        x4 <- mrgIf (isym "a" 3) (mrgSingle 0) (mrgSingle 1)
                        x5 <- mrgIf (isym "a" 4) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3, x4, x5),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [ [ssym "b" :: AsKey SymBool],
                            [ssym "b", ssym "c"]
                          ],
                          (),
                          (),
                          ()
                        )
                        "a" ::
                        (AsKey SymBool, [[AsKey SymBool]], AsKey SymBool, AsKey SymBool, AsKey SymBool)
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym () "a" ::
                          Union (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool)
                      )
                      @?= mrgSingle
                        ( isym "a" 0,
                          isym "a" 1,
                          isym "a" 2,
                          isym "a" 3,
                          isym "a" 4
                        ),
                  testCase "genSymSimple" $
                    ( genSymSimple () "a" ::
                        (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool)
                    )
                      @?= ( isym "a" 0,
                            isym "a" 1,
                            isym "a" 2,
                            isym "a" 3,
                            isym "a" 4
                          )
                ]
            ],
          testGroup
            "(,,,,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union
                            ( Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer
                            )
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        x4 <- mrgIf (isym "a" 3) (mrgSingle 0) (mrgSingle 1)
                        x5 <- mrgIf (isym "a" 4) (mrgSingle 0) (mrgSingle 1)
                        x6 <- mrgIf (isym "a" 5) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3, x4, x5, x6),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [ [ssym "b" :: AsKey SymBool],
                            [ssym "b", ssym "c"]
                          ],
                          (),
                          (),
                          (),
                          ()
                        )
                        "a" ::
                        ( AsKey SymBool,
                          [[AsKey SymBool]],
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6,
                            isym "a" 7
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym () "a" ::
                          Union
                            ( AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool
                            )
                      )
                      @?= mrgSingle
                        ( isym "a" 0,
                          isym "a" 1,
                          isym "a" 2,
                          isym "a" 3,
                          isym "a" 4,
                          isym "a" 5
                        ),
                  testCase "genSymSimple" $
                    ( genSymSimple () "a" ::
                        ( AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            isym "a" 1,
                            isym "a" 2,
                            isym "a" 3,
                            isym "a" 4,
                            isym "a" 5
                          )
                ]
            ],
          testGroup
            "(,,,,,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union
                            ( Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer
                            )
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        x4 <- mrgIf (isym "a" 3) (mrgSingle 0) (mrgSingle 1)
                        x5 <- mrgIf (isym "a" 4) (mrgSingle 0) (mrgSingle 1)
                        x6 <- mrgIf (isym "a" 5) (mrgSingle 0) (mrgSingle 1)
                        x7 <- mrgIf (isym "a" 6) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3, x4, x5, x6, x7),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [ [ssym "b" :: AsKey SymBool],
                            [ssym "b", ssym "c"]
                          ],
                          (),
                          (),
                          (),
                          (),
                          ()
                        )
                        "a" ::
                        ( AsKey SymBool,
                          [[AsKey SymBool]],
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6,
                            isym "a" 7,
                            isym "a" 8
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym () "a" ::
                          Union
                            ( AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool
                            )
                      )
                      @?= mrgSingle
                        ( isym "a" 0,
                          isym "a" 1,
                          isym "a" 2,
                          isym "a" 3,
                          isym "a" 4,
                          isym "a" 5,
                          isym "a" 6
                        ),
                  testCase "genSymSimple" $
                    ( genSymSimple () "a" ::
                        ( AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            isym "a" 1,
                            isym "a" 2,
                            isym "a" 3,
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6
                          )
                ]
            ],
          testGroup
            "(,,,,,,,)"
            [ testGroup
                "Some spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym
                          ( EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2,
                            EnumGenUpperBound @Integer 2
                          )
                          "a" ::
                          Union
                            ( Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer,
                              Integer
                            )
                      )
                      @?= do
                        x1 <- mrgIf (isym "a" 0) (mrgSingle 0) (mrgSingle 1)
                        x2 <- mrgIf (isym "a" 1) (mrgSingle 0) (mrgSingle 1)
                        x3 <- mrgIf (isym "a" 2) (mrgSingle 0) (mrgSingle 1)
                        x4 <- mrgIf (isym "a" 3) (mrgSingle 0) (mrgSingle 1)
                        x5 <- mrgIf (isym "a" 4) (mrgSingle 0) (mrgSingle 1)
                        x6 <- mrgIf (isym "a" 5) (mrgSingle 0) (mrgSingle 1)
                        x7 <- mrgIf (isym "a" 6) (mrgSingle 0) (mrgSingle 1)
                        x8 <- mrgIf (isym "a" 7) (mrgSingle 0) (mrgSingle 1)
                        mrgSingle (x1, x2, x3, x4, x5, x6, x7, x8),
                  testCase "genSymSimple" $
                    ( genSymSimple
                        ( (),
                          [ [ssym "b" :: AsKey SymBool],
                            [ssym "b", ssym "c"]
                          ],
                          (),
                          (),
                          (),
                          (),
                          (),
                          ()
                        )
                        "a" ::
                        ( AsKey SymBool,
                          [[AsKey SymBool]],
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            [ [isym "a" 1],
                              [isym "a" 2, isym "a" 3]
                            ],
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6,
                            isym "a" 7,
                            isym "a" 8,
                            isym "a" 9
                          )
                ],
              testGroup
                "No spec"
                [ testCase "genSym" $
                    AsKey1
                      ( genSym () "a" ::
                          Union
                            ( AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool,
                              AsKey SymBool
                            )
                      )
                      @?= mrgSingle
                        ( isym "a" 0,
                          isym "a" 1,
                          isym "a" 2,
                          isym "a" 3,
                          isym "a" 4,
                          isym "a" 5,
                          isym "a" 6,
                          isym "a" 7
                        ),
                  testCase "genSymSimple" $
                    ( genSymSimple () "a" ::
                        ( AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool,
                          AsKey SymBool
                        )
                    )
                      @?= ( isym "a" 0,
                            isym "a" 1,
                            isym "a" 2,
                            isym "a" 3,
                            isym "a" 4,
                            isym "a" 5,
                            isym "a" 6,
                            isym "a" 7
                          )
                ]
            ],
          testGroup
            "MaybeT Maybe SymBool"
            [ testGroup
                "Same shape spec"
                [ testGroup
                    "MaybeT Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              (MaybeT Nothing :: MaybeT Maybe (AsKey SymBool))
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT Nothing),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            (MaybeT Nothing :: MaybeT Maybe (AsKey SymBool))
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT Nothing
                    ],
                  testGroup
                    "MaybeT (Just Nothing)"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( MaybeT (Just Nothing) ::
                                  MaybeT Maybe (AsKey SymBool)
                              )
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT (Just Nothing)),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( MaybeT (Just (Just $ ssym "a")) ::
                                MaybeT Maybe (AsKey SymBool)
                            )
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT (Just (Just $ isym "a" 0))
                    ],
                  testGroup
                    "MaybeT (Just (Just v))"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( MaybeT (Just (Just $ ssym "a")) ::
                                  MaybeT Maybe (AsKey SymBool)
                              )
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT (Just (Just $ isym "a" 0))),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( MaybeT (Just (Just $ ssym "a")) ::
                                MaybeT Maybe (AsKey SymBool)
                            )
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT (Just (Just $ isym "a" 0))
                    ]
                ],
              testCase "No spec" $
                AsKey1
                  (genSym () "a" :: Union (MaybeT Maybe (AsKey SymBool)))
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle $ MaybeT Nothing)
                    ( mrgIf
                        (isym "a" 1)
                        (mrgSingle $ MaybeT $ Just Nothing)
                        (mrgSingle $ MaybeT $ Just $ Just $ isym "a" 2)
                    ),
              testGroup
                "Maybe (Maybe SymBool) spec"
                [ testGroup
                    "Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              (Nothing :: Maybe (Maybe (AsKey SymBool)))
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT Nothing),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            (Nothing :: Maybe (Maybe (AsKey SymBool)))
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT Nothing
                    ],
                  testGroup
                    "Just Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              (Just Nothing :: Maybe (Maybe (AsKey SymBool)))
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT (Just Nothing)),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            (Just Nothing :: Maybe (Maybe (AsKey SymBool)))
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT (Just Nothing)
                    ],
                  testGroup
                    "Just (Just v)"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( Just $ Just $ ssym "a" ::
                                  Maybe (Maybe (AsKey SymBool))
                              )
                              "a" ::
                              Union (MaybeT Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (MaybeT (Just (Just $ isym "a" 0))),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( Just $ Just $ ssym "a" ::
                                Maybe (Maybe (AsKey SymBool))
                            )
                            "a" ::
                            MaybeT Maybe (AsKey SymBool)
                        )
                          @?= MaybeT (Just (Just $ isym "a" 0))
                    ]
                ]
            ],
          testGroup
            "ExceptT SymBool Maybe SymBool"
            [ testGroup
                "Same shape spec"
                [ testGroup
                    "ExceptT Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( ExceptT Nothing ::
                                  ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                              )
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (ExceptT Nothing),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( ExceptT Nothing ::
                                ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                            )
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT Nothing
                    ],
                  testGroup
                    "ExceptT (Just (Left v))"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( ExceptT $ Just $ Left $ ssym "a" ::
                                  ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                              )
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle
                            (ExceptT $ Just $ Left $ isym "a" 0),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( ExceptT $ Just $ Left $ ssym "a" ::
                                ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                            )
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT (Just $ Left $ isym "a" 0)
                    ],
                  testGroup
                    "ExceptT (Just (Right v))"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( ExceptT $ Just $ Right $ ssym "a" ::
                                  ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                              )
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle
                            (ExceptT $ Just $ Right $ isym "a" 0),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( ExceptT $ Just $ Right $ ssym "a" ::
                                ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                            )
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT (Just $ Right $ isym "a" 0)
                    ]
                ],
              testCase "() spec" $ do
                AsKey1
                  (genSym () "a" :: Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool)))
                  @?= mrgIf
                    (isym "a" 0)
                    (mrgSingle $ ExceptT Nothing)
                    ( mrgIf
                        (isym "a" 1)
                        (mrgSingle $ ExceptT $ Just $ Left $ isym "a" 2)
                        (mrgSingle $ ExceptT $ Just $ Right $ isym "a" 3)
                    ),
              testGroup
                "Maybe (Either SymBool SymBool) spec"
                [ testGroup
                    "Nothing"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              (Nothing :: Maybe (Either (AsKey SymBool) (AsKey SymBool)))
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle (ExceptT Nothing),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            (Nothing :: Maybe (Either (AsKey SymBool) (AsKey SymBool)))
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT Nothing
                    ],
                  testGroup
                    "Just (left v)"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( Just $ Left $ ssym "a" ::
                                  Maybe (Either (AsKey SymBool) (AsKey SymBool))
                              )
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle
                            (ExceptT (Just (Left $ isym "a" 0))),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( Just $ Left $ ssym "a" ::
                                Maybe (Either (AsKey SymBool) (AsKey SymBool))
                            )
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT (Just (Left $ isym "a" 0))
                    ],
                  testGroup
                    "Just (left v)"
                    [ testCase "genSym" $
                        AsKey1
                          ( genSym
                              ( Just $ Right $ ssym "a" ::
                                  Maybe (Either (AsKey SymBool) (AsKey SymBool))
                              )
                              "a" ::
                              Union (ExceptT (AsKey SymBool) Maybe (AsKey SymBool))
                          )
                          @?= mrgSingle
                            (ExceptT (Just (Right $ isym "a" 0))),
                      testCase "genSymSimple" $
                        ( genSymSimple
                            ( Just $ Right $ ssym "a" ::
                                Maybe (Either (AsKey SymBool) (AsKey SymBool))
                            )
                            "a" ::
                            ExceptT (AsKey SymBool) Maybe (AsKey SymBool)
                        )
                          @?= ExceptT (Just (Right $ isym "a" 0))
                    ]
                ]
            ]
        ],
      testGroup
        "choose*"
        [ testCase "chooseFresh" $ do
            (AsKey1 (runFresh (chooseFresh [1, 2, 3]) "a" :: Union Int))
              @?= mrgIf
                (isym "a" 0)
                (mrgSingle 1)
                (mrgIf (isym "a" 1) (mrgSingle 2) (mrgSingle 3)),
          testCase "choose" $ do
            (AsKey1 (choose [1, 2, 3] "a" :: Union Int))
              @?= mrgIf
                (isym "a" 0)
                (mrgSingle 1)
                (mrgIf (isym "a" 1) (mrgSingle 2) (mrgSingle 3)),
          testCase "chooseSimpleFresh" $ do
            (runFresh (chooseSimpleFresh ["x", "y", "z"]) "a" :: AsKey SymBool)
              @?= symIte
                (isym "a" 0)
                (ssym "x")
                (symIte (isym "a" 1) (ssym "y") (ssym "z")),
          testCase "chooseSimple" $ do
            (chooseSimple ["x", "y", "z"] "a" :: AsKey SymBool)
              @?= symIte
                (isym "a" 0)
                (ssym "x")
                (symIte (isym "a" 1) (ssym "y") (ssym "z")),
          testCase "chooseUnionFresh" $ do
            AsKey1
              ( runFresh
                  ( chooseUnionFresh
                      [ mrgIf (ssym "x") 1 2,
                        mrgIf (ssym "x") 2 3,
                        mrgIf (ssym "x") 3 4
                      ]
                  )
                  "a" ::
                  Union Int
              )
              @?= mrgIf
                (isym "a" 0)
                (mrgIf (ssym "x") 1 2)
                ( mrgIf
                    (isym "a" 1)
                    (mrgIf (ssym "x") 2 3)
                    (mrgIf (ssym "x") 3 4)
                ),
          testCase "chooseUnion" $ do
            AsKey1
              ( chooseUnion
                  [ mrgIf (ssym "x") 1 2,
                    mrgIf (ssym "x") 2 3,
                    mrgIf (ssym "x") 3 4
                  ]
                  "a" ::
                  Union Int
              )
              @?= mrgIf
                (isym "a" 0)
                (mrgIf (ssym "x") 1 2)
                ( mrgIf
                    (isym "a" 1)
                    (mrgIf (ssym "x") 2 3)
                    (mrgIf (ssym "x") 3 4)
                ),
          testCase "liftFresh" $ do
            let orig = simpleFresh () :: Fresh (AsKey SymBool, AsKey SymBool)
            let actual = flip runFreshT "a" $ do
                  r1 <- liftFresh orig
                  r2 <- liftFresh orig
                  return (r1, r2) ::
                    FreshT (AsKey1 Union) ((AsKey SymBool, AsKey SymBool), (AsKey SymBool, AsKey SymBool))
            let expected =
                  return
                    ( (isym "a" 0, isym "a" 1),
                      (isym "a" 2, isym "a" 3)
                    )
            actual @?= expected
        ],
      testCase "freshString" $ do
        runFresh (replicateM 2 $ freshString "a") "b" @?= ["b@0[a]", "b@1[a]"],
      testCase "localIdentifier" $ do
        let computation = do
              a <- simpleFresh ()
              (b1, b2) <-
                localIdentifier (mapMetadata (const $ Atom ("b" :: T.Text))) $ do
                  b1 <- simpleFresh ()
                  b2 <- simpleFresh ()
                  return (b1, b2)
              c <- simpleFresh ()
              return [a, b1, b2, c :: AsKey SymBool]
        let actual = runFresh computation "c"
        actual
          @?= [ isym "c" 0,
                isym (withMetadata "c" (Atom ("b" :: T.Text))) 0,
                isym (withMetadata "c" (Atom ("b" :: T.Text))) 1,
                isym "c" 1
              ]
    ]