content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DerivingVia #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Grisette.Core.Data.Class.ExtractSymTests
    ( extractSymTests,
    )
  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 as B
  import Data.Int (Int16, Int32, Int64, Int8)
  import Data.Word (Word16, Word32, Word64, Word8)
  import GHC.Generics (Generic)
  import GHC.Stack (HasCallStack)
  import Generics.Deriving (Default (Default))
  import Grisette
    ( ExtractSym (extractSym),
      ITEOp (symIte),
      LogicalOp (symNot, (.&&), (.||)),
      Solvable (ssym),
      SymBool,
      SymEq ((.==)),
      SymbolSetOps (emptySet),
      SymbolSetRep (buildSymbolSet),
    )
  import Grisette.Core.Data.Class.TestValues
    ( isymBool,
      isymbolBool,
      ssymBool,
      ssymbolBool,
      symTrue,
    )
  import Grisette.Internal.SymPrim.SymInteger (SymInteger)
  import Test.Framework (Test, TestOptions' (topt_timeout), plusTestOptions, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit (Assertion, (@?=))
  import Test.QuickCheck (ioProperty)
  
  data A = A1 | A2 SymBool | A3 SymBool SymBool
    deriving (Generic, Show, Eq)
    deriving (ExtractSym) via (Default A)
  
  concreteExtractSymOkProp ::
    (HasCallStack, ExtractSym a) => (a, a) -> Assertion
  concreteExtractSymOkProp x = extractSym x @?= emptySet
  
  extractSymTests :: Test
  extractSymTests =
    testGroup
      "ExtractSym"
      [ plusTestOptions (mempty {topt_timeout = Just (Just 1000000)}) $
          testCase "proper memo" $ do
            let pair = ("a" :: SymInteger, "b" :: SymInteger)
            let iter (x, y) = (y, x + y)
            let r = iterate iter pair !! 100
            extractSym r @?= extractSym pair,
        testGroup
          "Common types"
          [ testGroup
              "SymBool"
              [ testCase "con" $
                  extractSym symTrue @?= emptySet,
                testCase "ssym" $
                  extractSym (ssymBool "a")
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "isym" $
                  extractSym (isymBool "a" 1)
                    @?= buildSymbolSet (isymbolBool "a" 1),
                testCase "And" $
                  extractSym (ssymBool "a" .&& isymBool "b" 1)
                    @?= buildSymbolSet (ssymbolBool "a", isymbolBool "b" 1),
                testCase "Or" $
                  extractSym (ssymBool "a" .|| isymBool "b" 1)
                    @?= buildSymbolSet (ssymbolBool "a", isymbolBool "b" 1),
                testCase "Equal" $
                  extractSym (ssymBool "a" .== isymBool "b" 1)
                    @?= buildSymbolSet (ssymbolBool "a", isymbolBool "b" 1),
                testCase "ITE" $
                  extractSym
                    (symIte (ssym "a") (isymBool "b" 1) (ssymBool "c"))
                    @?= buildSymbolSet
                      ( ssymbolBool "a",
                        isymbolBool "b" 1,
                        ssymbolBool "c"
                      ),
                testCase "Not" $
                  extractSym (symNot $ isymBool "a" 1)
                    @?= buildSymbolSet (isymbolBool "a" 1)
              ],
            testProperty "Bool" $
              ioProperty . concreteExtractSymOkProp @Bool,
            testProperty "Integer" $
              ioProperty . concreteExtractSymOkProp @Integer,
            testProperty "Char" $
              ioProperty . concreteExtractSymOkProp @Char,
            testProperty "Int" $ ioProperty . concreteExtractSymOkProp @Int,
            testProperty "Int8" $
              ioProperty . concreteExtractSymOkProp @Int8,
            testProperty "Int16" $
              ioProperty . concreteExtractSymOkProp @Int16,
            testProperty "Int32" $
              ioProperty . concreteExtractSymOkProp @Int32,
            testProperty "Int64" $
              ioProperty . concreteExtractSymOkProp @Int64,
            testProperty "Word" $
              ioProperty . concreteExtractSymOkProp @Word,
            testProperty "Word8" $
              ioProperty . concreteExtractSymOkProp @Word8,
            testProperty "Word16" $
              ioProperty . concreteExtractSymOkProp @Word16,
            testProperty "Word32" $
              ioProperty . concreteExtractSymOkProp @Word32,
            testProperty "Word64" $
              ioProperty . concreteExtractSymOkProp @Word64,
            testGroup
              "[SymBool]"
              [ testCase "[]" $
                  extractSym ([] :: [SymBool]) @?= emptySet,
                testCase "[v]" $
                  extractSym [ssymBool "a"]
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "[v1, v2]" $
                  extractSym [ssymBool "a", ssymBool "b"]
                    @?= buildSymbolSet (ssymbolBool "a", ssymbolBool "b")
              ],
            testGroup
              "Maybe SymBool"
              [ testCase "Nothing" $
                  extractSym (Nothing :: Maybe SymBool) @?= emptySet,
                testCase "Just v" $
                  extractSym (Just (ssymBool "a"))
                    @?= buildSymbolSet (ssymbolBool "a")
              ],
            testGroup
              "Either SymBool SymBool"
              [ testCase "Left v" $
                  extractSym
                    (Left (ssym "a") :: Either SymBool SymBool)
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "Right v" $
                  extractSym
                    (Right (ssym "a") :: Either SymBool SymBool)
                    @?= buildSymbolSet (ssymbolBool "a")
              ],
            testGroup
              "MaybeT Maybe SymBool"
              [ testCase "MaybeT Nothing" $
                  extractSym (MaybeT Nothing :: MaybeT Maybe SymBool)
                    @?= emptySet,
                testCase "MaybeT (Just Nothing)" $
                  extractSym (MaybeT (Just Nothing) :: MaybeT Maybe SymBool)
                    @?= emptySet,
                testCase "MaybeT (Just (Just v))" $
                  extractSym (MaybeT (Just (Just (ssymBool "a"))))
                    @?= buildSymbolSet (ssymbolBool "a")
              ],
            testGroup
              "ExceptT SymBool Maybe SymBool"
              [ testCase "ExceptT Nothing" $
                  extractSym
                    (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
                    @?= emptySet,
                testCase "ExceptT (Just (Left v))" $
                  extractSym
                    ( ExceptT (Just (Left (ssym "a"))) ::
                        ExceptT SymBool Maybe SymBool
                    )
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "ExceptT (Just (Right v))" $
                  extractSym
                    ( ExceptT (Just (Right (ssym "a"))) ::
                        ExceptT SymBool Maybe SymBool
                    )
                    @?= buildSymbolSet (ssymbolBool "a")
              ],
            testGroup
              "WriterT SymBool Maybe SymBool"
              [ testGroup
                  "Lazy"
                  [ testCase "WriterT Nothing" $
                      extractSym
                        ( WriterLazy.WriterT Nothing ::
                            WriterLazy.WriterT SymBool Maybe SymBool
                        )
                        @?= emptySet,
                    testCase "WriterT (Just (v1, v2))" $
                      extractSym
                        ( WriterLazy.WriterT
                            (Just (ssym "a", ssym "b")) ::
                            WriterLazy.WriterT SymBool Maybe SymBool
                        )
                        @?= buildSymbolSet (ssymbolBool "a", ssymbolBool "b")
                  ],
                testGroup
                  "Strict"
                  [ testCase "WriterT Nothing" $
                      extractSym
                        ( WriterStrict.WriterT Nothing ::
                            WriterStrict.WriterT SymBool Maybe SymBool
                        )
                        @?= emptySet,
                    testCase "WriterT (Just (v1, v2))" $
                      extractSym
                        ( WriterStrict.WriterT
                            (Just (ssym "a", ssym "b")) ::
                            WriterStrict.WriterT SymBool Maybe SymBool
                        )
                        @?= buildSymbolSet (ssymbolBool "a", ssymbolBool "b")
                  ]
              ],
            testProperty "()" (ioProperty . concreteExtractSymOkProp @()),
            testCase "(,)" $
              extractSym (ssymBool "a", ssymBool "b")
                @?= buildSymbolSet (ssymbolBool "a", ssymbolBool "b"),
            testCase "(,,)" $
              extractSym (ssymBool "a", ssymBool "b", ssymBool "c")
                @?= buildSymbolSet
                  (ssymbolBool "a", ssymbolBool "b", ssymbolBool "c"),
            testGroup
              "ByteString"
              [ testCase "\"\"" $
                  extractSym ("" :: B.ByteString) @?= emptySet,
                testCase "\"a\"" $
                  extractSym ("a" :: B.ByteString) @?= emptySet
              ],
            testCase "Identity SymBool" $
              extractSym (Identity (ssymBool "a"))
                @?= buildSymbolSet (ssymbolBool "a"),
            testGroup
              "IdentityT (Either SymBool) SymBool"
              [ testCase "Identity (Left v)" $
                  extractSym
                    ( IdentityT $ Left (ssym "a") ::
                        IdentityT (Either SymBool) SymBool
                    )
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "Identity (Right v)" $
                  extractSym
                    ( IdentityT $ Right (ssym "a") ::
                        IdentityT (Either SymBool) SymBool
                    )
                    @?= buildSymbolSet (ssymbolBool "a")
              ]
          ],
        testGroup
          "deriving ExtractSym for ADT"
          [ testGroup
              "Simple ADT"
              [ testCase "A1" $
                  extractSym A1 @?= emptySet,
                testCase "A2" $
                  extractSym (A2 (ssym "a"))
                    @?= buildSymbolSet (ssymbolBool "a"),
                testCase "A3" $
                  extractSym (A3 (ssym "a") (ssym "b"))
                    @?= buildSymbolSet (ssymbolBool "a", ssymbolBool "b")
              ]
          ]
      ]
  