content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
  
  {-# HLINT ignore "Unused LANGUAGE pragma" #-}
  
  -- {-# OPTIONS_GHC -ddump-simpl -dsuppress-module-prefixes -dsuppress-uniques #-}
  -- {-# OPTIONS_GHC -ddump-timings #-}
  
  module Grisette.Core.TH.DerivationTest (derivationTest) where
  
  import Data.Bytes.Get (runGetS)
  import Data.Bytes.Put (runPutS)
  import Data.Bytes.Serial (Serial (deserialize, serialize))
  import Data.Functor.Classes (showsPrec1, showsPrec2)
  import qualified Data.Text as T
  import GHC.TypeLits (KnownNat, type (<=))
  import Grisette
    ( AsKey (AsKey),
      AsKey1 (AsKey1),
      FP32,
      Mergeable,
      PPrint (pformat, pformatPrec),
      Solvable (con),
      SymEq ((.==)),
      SymOrd (symCompare),
      ValidFP,
      WordN32,
      docToTextWithWidth,
      mrgSingle,
      pformatPrec1,
      pformatPrec2,
      symCompare1,
      symCompare2,
      symEq1,
      symEq2,
    )
  import Grisette.Core.TH.DerivationData
    ( Extra (Extra),
      GGG,
      Serializable,
      gggToVVV,
      replaceVVVShown,
    )
  import Grisette.Core.TH.PartialEvalMode (PartialEvalMode)
  import Grisette.TestUtil.SymbolicAssertion ((.@?=))
  import Grisette.Unified
    ( BaseMonad,
      EvalModeTag (C),
      GetBool,
      GetData,
      extractData,
    )
  import qualified Grisette.Unified as GU
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.QuickCheck.Property ((.&.), (===))
  
  #if MIN_VERSION_base(4,16,0)
  ftst ::
    forall mode n eb sb a.
    ( PartialEvalMode mode,
      KnownNat n,
      1 <= n,
      ValidFP eb sb,
      Mergeable a
    ) =>
    GetBool mode ->
    GetData mode (Extra mode n eb sb a) ->
    GetData mode (Extra mode n eb sb a) ->
    BaseMonad mode (Extra mode n eb sb a)
  ftst c t f =
    GU.mrgIf @mode
      c
      (extractData t)
      (extractData f)
  
  derivationExtraTest :: [Test]
  derivationExtraTest =
    [ testCase "ftst" $ do
        let x = Extra True [1 :: WordN32] [] (0 :: FP32) 0 0 (0 :: Int)
        let y = Extra False [1 :: WordN32] [] (0 :: FP32) 0 0 (0 :: Int)
        let a = ftst @'C True (return x) (return y)
        a .@?= return x
    ]
  #else
  derivationExtraTest :: [Test]
  derivationExtraTest = []
  #endif
  
  derivationTest :: Test
  derivationTest =
    testGroup "Derivation" $
      [ testProperty "GADT Show instance for regular types" $
          \(g :: GGG (GGG Int String) [Int]) ->
            let v = gggToVVV g
             in replaceVVVShown (T.pack (show g))
                  === replaceVVVShown (T.pack (show v)),
        testProperty "GADT Show and Show1 are consistent" $
          \(g :: GGG (GGG Char String) [Int]) ->
            T.pack (show g)
              === T.pack (showsPrec1 0 g "")
              .&. T.pack (showsPrec 11 g "")
              === T.pack (showsPrec1 11 g ""),
        testProperty "GADT Show and Show2 are consistent" $
          \(g :: GGG (GGG Char String) [Int]) ->
            T.pack (show g)
              === T.pack (showsPrec2 0 g "")
              .&. T.pack (showsPrec 11 g "")
              === T.pack (showsPrec2 11 g ""),
        testProperty "GADT PPrint instance for regular types" $
          \(g :: GGG (GGG Int String) [Int]) ->
            let v = gggToVVV g
             in replaceVVVShown (docToTextWithWidth 1000 (pformat g))
                  === replaceVVVShown (docToTextWithWidth 1000 (pformat v))
                  .&. replaceVVVShown (docToTextWithWidth 0 (pformat g))
                  === replaceVVVShown (docToTextWithWidth 0 (pformat v)),
        testProperty "GADT PPrint and PPrint1 are consistent" $
          \(g :: GGG (GGG Char String) [Int]) ->
            docToTextWithWidth 1000 (pformatPrec 0 g)
              === docToTextWithWidth 1000 (pformatPrec1 0 g)
              .&. docToTextWithWidth 1000 (pformatPrec 11 g)
              === docToTextWithWidth 1000 (pformatPrec1 11 g)
              .&. docToTextWithWidth 0 (pformatPrec 0 g)
              === docToTextWithWidth 0 (pformatPrec1 0 g)
              .&. docToTextWithWidth 0 (pformatPrec 11 g)
              === docToTextWithWidth 0 (pformatPrec1 11 g),
        testProperty "GADT PPrint and PPrint2 are consistent" $
          \(g :: GGG (GGG Char String) [Int]) ->
            docToTextWithWidth 1000 (pformatPrec 0 g)
              === docToTextWithWidth 1000 (pformatPrec2 0 g)
              .&. docToTextWithWidth 1000 (pformatPrec 11 g)
              === docToTextWithWidth 1000 (pformatPrec2 11 g)
              .&. docToTextWithWidth 0 (pformatPrec 0 g)
              === docToTextWithWidth 0 (pformatPrec2 0 g)
              .&. docToTextWithWidth 0 (pformatPrec 11 g)
              === docToTextWithWidth 0 (pformatPrec2 11 g),
        testProperty "GADT SymEq and Eq are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            let v1 = gggToVVV g1
                v2 = gggToVVV g2
             in AsKey (con (g1 == g2)) === AsKey (v1 .== v2),
        testProperty "GADT SymEq1 and SymEq are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            AsKey (symEq1 g1 g2) === AsKey (g1 .== g2),
        testProperty "GADT SymEq2 and SymEq are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            AsKey (symEq2 g1 g2) === AsKey (g1 .== g2),
        testProperty "GADT SymOrd and Ord are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            let v1 = gggToVVV g1
                v2 = gggToVVV g2
             in mrgSingle (g1 `compare` g2) === AsKey1 (v1 `symCompare` v2),
        testProperty "GADT SymOrd1 and SymOrd are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            AsKey1 (symCompare1 g1 g2) === AsKey1 (g1 `symCompare` g2),
        testProperty "GADT SymOrd2 and SymOrd are consistent" $
          \(g1 :: GGG (GGG Int String) [Int]) g2 ->
            AsKey1 (symCompare2 g1 g2) === AsKey1 (g1 `symCompare` g2),
        testProperty "Serialize" $ do
          \(s :: Serializable Int) ->
            let bs = runPutS (serialize s)
                s' = runGetS deserialize bs
             in Right s === s'
      ]
        ++ derivationExtraTest
  