content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Grisette.Core.Data.Class.ToConTests (toConTests) where
  
  import Control.Monad.Except (ExceptT (ExceptT))
  import Control.Monad.Identity
    ( Identity (Identity),
      IdentityT (IdentityT),
    )
  import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
  import qualified Control.Monad.Writer.Lazy as WriterLazy
  import qualified Control.Monad.Writer.Strict as WriterStrict
  import qualified Data.ByteString.Char8 as C
  import Data.Foldable (traverse_)
  import Data.Functor.Sum (Sum (InL, InR))
  import Data.Int (Int16, Int32, Int64, Int8)
  import Data.Word (Word16, Word32, Word64, Word8)
  import GHC.Stack (HasCallStack)
  import Grisette
    ( ITEOp (symIte),
      LogicalOp (symNot, (.&&), (.||)),
      SymBool,
      SymEq ((.==)),
      ToCon (toCon),
    )
  import Grisette.Core.Data.Class.TestValues
    ( conBool,
      isymBool,
      ssymBool,
      symFalse,
      symTrue,
    )
  import Grisette.TestUtil.SymbolicAssertion ((.@?=))
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit (Assertion, (@?=))
  import Test.QuickCheck (ioProperty)
  
  toConForConcreteOkProp :: (HasCallStack, Show v, Eq v) => v -> Assertion
  toConForConcreteOkProp v = toCon v @?= Just v
  
  toConTests :: Test
  toConTests =
    testGroup
      "ToCon"
      [ testGroup
          "ToCon for common types"
          [ testGroup
              "SymBool"
              [ testGroup
                  "To Bool"
                  [ testCase "con" $ do
                      let bools :: [Bool] = [True, False]
                      traverse_ (\v -> toCon (conBool v) @?= Just v) bools,
                    testCase "Symbolic SymBools" $ do
                      let sbools :: [SymBool] =
                            [ ssymBool "a",
                              isymBool "a" 1,
                              ssymBool "a" .&& ssymBool "b",
                              ssymBool "a" .|| ssymBool "b",
                              symNot $ ssymBool "a",
                              ssymBool "a" .== ssymBool "b",
                              symIte (ssymBool "a") (ssymBool "b") (ssymBool "c")
                            ]
                      traverse_ (\v -> toCon v @?= (Nothing :: Maybe Bool)) sbools
                  ],
                testCase "To SymBool" $ do
                  let sbools :: [SymBool] =
                        [ symTrue,
                          ssymBool "a",
                          isymBool "a" 1,
                          ssymBool "a" .&& ssymBool "b",
                          ssymBool "a" .|| ssymBool "b",
                          symNot $ ssymBool "a",
                          ssymBool "a" .== ssymBool "b",
                          symIte (ssymBool "a") (ssymBool "b") (ssymBool "c")
                        ]
                  traverse_ (\v -> toCon v .@?= Just v) sbools
              ],
            testProperty "Bool" $ ioProperty . toConForConcreteOkProp @Bool,
            testProperty "Integer" $ ioProperty . toConForConcreteOkProp @Integer,
            testProperty "Char" $ ioProperty . toConForConcreteOkProp @Char,
            testProperty "Int" $ ioProperty . toConForConcreteOkProp @Int,
            testProperty "Int8" $ ioProperty . toConForConcreteOkProp @Int8,
            testProperty "Int16" $ ioProperty . toConForConcreteOkProp @Int16,
            testProperty "Int32" $ ioProperty . toConForConcreteOkProp @Int32,
            testProperty "Int64" $ ioProperty . toConForConcreteOkProp @Int64,
            testProperty "Word" $ ioProperty . toConForConcreteOkProp @Word,
            testProperty "Word8" $ ioProperty . toConForConcreteOkProp @Word8,
            testProperty "Word16" $ ioProperty . toConForConcreteOkProp @Word16,
            testProperty "Word32" $ ioProperty . toConForConcreteOkProp @Word32,
            testProperty "Word64" $ ioProperty . toConForConcreteOkProp @Word64,
            testProperty "()" $ ioProperty . toConForConcreteOkProp @(),
            testProperty "ByteString" $
              ioProperty
                . \(v :: String) -> toConForConcreteOkProp (C.pack v),
            testGroup
              "List"
              [ testProperty "[Integer]" $
                  ioProperty . toConForConcreteOkProp @[Integer],
                testCase "[SymBool]" $ do
                  toCon ([] :: [SymBool]) @?= (Just [] :: Maybe [Bool])
                  toCon ([symTrue] :: [SymBool]) @?= (Just [True] :: Maybe [Bool])
                  toCon ([ssymBool "a"] :: [SymBool])
                    @?= (Nothing :: Maybe [Bool])
                  toCon ([symTrue, symFalse] :: [SymBool])
                    @?= (Just [True, False] :: Maybe [Bool])
                  toCon ([symTrue, ssymBool "a"] :: [SymBool])
                    @?= (Nothing :: Maybe [Bool])
              ],
            testGroup
              "Maybe"
              [ testProperty "Maybe Integer" $
                  ioProperty . toConForConcreteOkProp @(Maybe Integer),
                testCase "Maybe SymBool" $ do
                  let toConMaybe :: Maybe SymBool -> Maybe (Maybe Bool)
                      toConMaybe = toCon
                  toConMaybe Nothing @?= (Just Nothing)
                  toConMaybe (Just symTrue) @?= (Just (Just True))
                  toConMaybe (Just $ ssymBool "a") @?= Nothing
              ],
            testGroup
              "Either"
              [ testProperty "Either Integer Integer" $
                  ioProperty . toConForConcreteOkProp @(Either Integer Integer),
                testCase "Either SymBool SymBool" $ do
                  let toConEither ::
                        Either SymBool SymBool ->
                        Maybe (Either Bool Bool)
                      toConEither = toCon
                  toConEither (Left symTrue) @?= (Just (Left True))
                  toConEither (Right symTrue) @?= (Just (Right True))
                  toConEither (Left $ ssymBool "a") @?= Nothing
                  toConEither (Right $ ssymBool "a") @?= Nothing
              ],
            testGroup
              "MaybeT"
              [ testProperty "MaybeT Maybe Integer" $
                  ioProperty . \(v :: Maybe (Maybe Integer)) ->
                    toConForConcreteOkProp (MaybeT v),
                testCase "MaybeT Maybe SymBool" $ do
                  toCon (MaybeT Nothing :: MaybeT Maybe SymBool)
                    @?= (Just $ MaybeT Nothing :: Maybe (MaybeT Maybe Bool))
                  toCon (MaybeT $ Just Nothing :: MaybeT Maybe SymBool)
                    @?= ( Just $ MaybeT $ Just Nothing ::
                            Maybe (MaybeT Maybe Bool)
                        )
                  toCon
                    ( MaybeT $ Just $ Just symTrue ::
                        MaybeT Maybe SymBool
                    )
                    @?= ( Just $ MaybeT $ Just $ Just True ::
                            Maybe (MaybeT Maybe Bool)
                        )
                  toCon
                    ( MaybeT $ Just $ Just $ ssymBool "a" ::
                        MaybeT Maybe SymBool
                    )
                    @?= (Nothing :: Maybe (MaybeT Maybe Bool))
              ],
            testGroup
              "ExceptT"
              [ testProperty "ExceptT Integer Maybe Integer" $
                  ioProperty . \(v :: Maybe (Either Integer Integer)) ->
                    toConForConcreteOkProp (ExceptT v),
                testCase "ExceptT SymBool Maybe SymBool" $ do
                  let toConExceptT ::
                        ExceptT SymBool Maybe SymBool ->
                        Maybe (ExceptT Bool Maybe Bool)
                      toConExceptT = toCon
                  toConExceptT (ExceptT Nothing) @?= Just (ExceptT Nothing)
                  toConExceptT (ExceptT $ Just $ Left symTrue)
                    @?= Just (ExceptT $ Just $ Left True)
                  toConExceptT (ExceptT $ Just $ Left $ ssymBool "a") @?= Nothing
                  toConExceptT (ExceptT $ Just $ Right symTrue)
                    @?= Just (ExceptT $ Just $ Right True)
                  toConExceptT (ExceptT $ Just $ Right $ ssymBool "a") @?= Nothing
              ],
            testGroup
              "(,)"
              [ testProperty "(Integer, Integer)" $
                  ioProperty . toConForConcreteOkProp @(Integer, Integer),
                testCase "(SymBool, SymBool)" $ do
                  let toConTuple2 :: (SymBool, SymBool) -> Maybe (Bool, Bool)
                      toConTuple2 = toCon
                  toConTuple2 (symTrue, symFalse) @?= Just (True, False)
                  toConTuple2 (symTrue, ssymBool "a") @?= Nothing
              ],
            testGroup
              "(,,)"
              [ testProperty "(Integer, Integer, Integer)" $
                  ioProperty
                    . toConForConcreteOkProp @(Integer, Integer, Integer),
                testCase "(SymBool, SymBool, SymBool)" $ do
                  let toConTuple3 ::
                        (SymBool, SymBool, SymBool) ->
                        Maybe (Bool, Bool, Bool)
                      toConTuple3 = toCon
                  toConTuple3 (symFalse, symTrue, symFalse)
                    @?= Just (False, True, False)
                  toConTuple3 (symFalse, symTrue, ssymBool "a")
                    @?= Nothing
              ],
            testGroup
              "(,,,)"
              [ testProperty "(Integer, Integer, Integer, Integer)" $
                  ioProperty
                    . toConForConcreteOkProp
                      @(Integer, Integer, Integer, Integer),
                testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
                  let toConTuple4 ::
                        (SymBool, SymBool, SymBool, SymBool) ->
                        Maybe (Bool, Bool, Bool, Bool)
                      toConTuple4 = toCon
                  toConTuple4 (symTrue, symFalse, symTrue, symFalse)
                    @?= Just (True, False, True, False)
                  toConTuple4 (symTrue, symFalse, symTrue, ssymBool "a")
                    @?= Nothing
              ],
            testGroup
              "(,,,,)"
              [ testProperty "(Integer, Integer, Integer, Integer, Integer)" $
                  ioProperty
                    . toConForConcreteOkProp
                      @(Integer, Integer, Integer, Integer, Integer),
                testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
                  let toConTuple5 ::
                        (SymBool, SymBool, SymBool, SymBool, SymBool) ->
                        Maybe (Bool, Bool, Bool, Bool, Bool)
                      toConTuple5 = toCon
                  toConTuple5 (symFalse, symTrue, symFalse, symTrue, symFalse)
                    @?= Just (False, True, False, True, False)
                  toConTuple5 (symFalse, symTrue, symFalse, symTrue, ssymBool "a")
                    @?= Nothing
              ],
            testGroup
              "(,,,,,)"
              [ testProperty
                  "(Integer, Integer, Integer, Integer, Integer, Integer)"
                  $ ioProperty
                    . toConForConcreteOkProp
                      @(Integer, Integer, Integer, Integer, Integer, Integer),
                testCase
                  "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                  $ do
                    let toConTuple6 ::
                          ( SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool
                          ) ->
                          Maybe (Bool, Bool, Bool, Bool, Bool, Bool)
                        toConTuple6 = toCon
                    toConTuple6
                      (symTrue, symFalse, symTrue, symFalse, symTrue, symFalse)
                      @?= Just (True, False, True, False, True, False)
                    toConTuple6
                      (symTrue, symFalse, symTrue, symFalse, symTrue, ssymBool "a")
                      @?= Nothing
              ],
            testGroup
              "(,,,,,,)"
              [ testProperty
                  "(Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
                  $ ioProperty
                    . toConForConcreteOkProp
                      @( Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer
                       ),
                testCase
                  "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                  $ do
                    let toConTuple7 ::
                          ( SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool
                          ) ->
                          Maybe (Bool, Bool, Bool, Bool, Bool, Bool, Bool)
                        toConTuple7 = toCon
                    toConTuple7
                      ( symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse
                      )
                      @?= Just (False, True, False, True, False, True, False)
                    toConTuple7
                      ( symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        ssymBool "a"
                      )
                      @?= Nothing
              ],
            testGroup
              "(,,,,,,,)"
              [ testProperty
                  "(Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
                  $ ioProperty
                    . toConForConcreteOkProp
                      @( Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer,
                         Integer
                       ),
                testCase
                  "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
                  $ do
                    let toConTuple8 ::
                          ( SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool,
                            SymBool
                          ) ->
                          Maybe (Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool)
                        toConTuple8 = toCon
                    toConTuple8
                      ( symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse
                      )
                      @?= Just
                        ( True,
                          False,
                          True,
                          False,
                          True,
                          False,
                          True,
                          False
                        )
                    toConTuple8
                      ( symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        symFalse,
                        symTrue,
                        ssymBool "a"
                      )
                      @?= Nothing
              ],
            testGroup
              "Sum"
              [ testProperty "Sum Maybe Maybe Integer" $
                  ioProperty . \(v :: Either (Maybe Integer) (Maybe Integer)) ->
                    toConForConcreteOkProp $ case v of
                      Left x -> InL x
                      Right x -> InR x,
                testCase "Sum Maybe (Either SymBool) SymBool" $ do
                  let toConSum ::
                        Sum Maybe (Either SymBool) SymBool ->
                        Maybe (Sum Maybe (Either Bool) Bool)
                      toConSum = toCon
                  toConSum (InL (Just symTrue)) @?= Just (InL (Just True))
                  toConSum (InL (Just $ ssymBool "a")) @?= Nothing
                  toConSum (InR (Left symTrue)) @?= Just (InR (Left True))
                  toConSum (InR (Right symTrue)) @?= Just (InR (Right True))
                  toConSum (InR (Left $ ssymBool "a")) @?= Nothing
                  toConSum (InR (Right $ ssymBool "a")) @?= Nothing
              ],
            testGroup
              "WriterT"
              [ testGroup
                  "Lazy"
                  [ testProperty "WriterT Integer (Either Integer) Integer" $
                      ioProperty . \(v :: Either Integer (Integer, Integer)) ->
                        toConForConcreteOkProp $ WriterLazy.WriterT v,
                    testCase "WriterT SymBool (Either SymBool) SymBool" $ do
                      let toConWriterT ::
                            WriterLazy.WriterT SymBool (Either SymBool) SymBool ->
                            Maybe (WriterLazy.WriterT Bool (Either Bool) Bool)
                          toConWriterT = toCon
                      toConWriterT (WriterLazy.WriterT $ Left symTrue)
                        @?= Just (WriterLazy.WriterT $ Left True)
                      toConWriterT (WriterLazy.WriterT $ Left $ ssymBool "a")
                        @?= Nothing
                      toConWriterT (WriterLazy.WriterT $ Right (symTrue, symTrue))
                        @?= Just (WriterLazy.WriterT $ Right (True, True))
                      toConWriterT
                        (WriterLazy.WriterT $ Right (ssymBool "a", symTrue))
                        @?= Nothing
                      toConWriterT
                        (WriterLazy.WriterT $ Right (symTrue, ssymBool "a"))
                        @?= Nothing
                      toConWriterT
                        (WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "b"))
                        @?= Nothing
                  ],
                testGroup
                  "Strict"
                  [ testProperty "WriterT Integer (Either Integer) Integer" $
                      ioProperty . \(v :: Either Integer (Integer, Integer)) ->
                        toConForConcreteOkProp $ WriterStrict.WriterT v,
                    testCase "WriterT SymBool (Either SymBool) SymBool" $ do
                      let toConWriterT ::
                            WriterStrict.WriterT
                              SymBool
                              (Either SymBool)
                              SymBool ->
                            Maybe (WriterStrict.WriterT Bool (Either Bool) Bool)
                          toConWriterT = toCon
                      toConWriterT (WriterStrict.WriterT $ Left symTrue)
                        @?= Just (WriterStrict.WriterT $ Left True)
                      toConWriterT (WriterStrict.WriterT $ Left $ ssymBool "a")
                        @?= Nothing
                      toConWriterT
                        (WriterStrict.WriterT $ Right (symTrue, symTrue))
                        @?= Just (WriterStrict.WriterT $ Right (True, True))
                      toConWriterT
                        (WriterStrict.WriterT $ Right (ssymBool "a", symTrue))
                        @?= Nothing
                      toConWriterT
                        (WriterStrict.WriterT $ Right (symTrue, ssymBool "a"))
                        @?= Nothing
                      toConWriterT
                        (WriterStrict.WriterT $ Right (ssymBool "a", ssymBool "b"))
                        @?= Nothing
                  ]
              ],
            testGroup
              "Identity"
              [ testProperty "Identity Integer" $
                  ioProperty . \(v :: Integer) ->
                    toConForConcreteOkProp $ Identity v,
                testCase "Identity SymBool" $ do
                  toCon (Identity symTrue) @?= Just (Identity True)
                  toCon (Identity $ ssymBool "a") @?= (Nothing :: Maybe (Identity Bool))
              ],
            testGroup
              "IdentityT"
              [ testProperty "IdentityT (Either Integer) Integer" $
                  ioProperty . \(v :: Either Integer Integer) ->
                    toConForConcreteOkProp $ IdentityT v,
                testCase "IdentityT (Either SymBool) SymBool" $ do
                  let toConIdentityT ::
                        IdentityT (Either SymBool) SymBool ->
                        Maybe (IdentityT (Either Bool) Bool)
                      toConIdentityT = toCon
                  toConIdentityT (IdentityT $ Left symTrue)
                    @?= Just (IdentityT $ Left True)
                  toConIdentityT (IdentityT $ Left $ ssymBool "a")
                    @?= Nothing
                  toConIdentityT (IdentityT $ Right symTrue)
                    @?= Just (IdentityT $ Right True)
                  toConIdentityT (IdentityT $ Right $ ssymBool "a")
                    @?= Nothing
              ]
          ]
      ]
  