content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  module Grisette.Core.Data.Class.SymShiftTests (symShiftTests) where
  
  import Data.Bits (Bits (shift), FiniteBits (finiteBitSize))
  import Data.Data (Proxy (Proxy), Typeable, typeRep)
  import Data.Int (Int16, Int32, Int64, Int8)
  import Data.Word (Word16, Word32, Word64, Word8)
  import Grisette
    ( AsKey (AsKey),
      IntN,
      Solvable (con),
      SymIntN,
      SymShift (symShift, symShiftNegated),
      SymWordN,
      WordN,
    )
  import Grisette.Internal.Core.Data.Class.AsKey (KeyEq)
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit ((@?=))
  import Test.QuickCheck (Arbitrary, chooseInt, forAll, ioProperty)
  
  concreteUnsignedTypeSymShiftTests ::
    forall proxy a.
    ( Arbitrary a,
      Show a,
      Num a,
      SymShift a,
      FiniteBits a,
      Bounded a,
      Typeable a
    ) =>
    proxy a ->
    Test
  concreteUnsignedTypeSymShiftTests p =
    testGroup
      (show $ typeRep p)
      [ testGroup
          "SymShift"
          [ testProperty "symShift" $ \(x :: a) ->
              forAll (chooseInt (0, finiteBitSize x)) $
                \(s :: Int) ->
                  ioProperty $
                    symShift x (fromIntegral s) @?= shift x s,
            testProperty "symShiftNegated" $ \(x :: a) ->
              forAll (chooseInt (0, finiteBitSize x)) $
                \(s :: Int) ->
                  ioProperty $
                    symShiftNegated x (fromIntegral s) @?= shift x (-s),
            testProperty "symShift max" $ \(x :: a) ->
              ioProperty $ symShift x maxBound @?= 0,
            testProperty "symShiftNegated max" $ \(x :: a) ->
              ioProperty $ symShiftNegated x maxBound @?= 0
          ]
      ]
  
  concreteSignedTypeSymShiftTests ::
    forall proxy a.
    ( Arbitrary a,
      Show a,
      SymShift a,
      FiniteBits a,
      Bounded a,
      Typeable a,
      Integral a
    ) =>
    proxy a ->
    Test
  concreteSignedTypeSymShiftTests p =
    testGroup
      (show $ typeRep p)
      [ testGroup
          "SymShift"
          [ testProperty "symShift" $ \(x :: a) ->
              forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
                \(s :: Int) -> ioProperty $ do
                  symShift x (fromIntegral s)
                    @?= shift x (fromIntegral (fromIntegral s :: a)),
            testProperty "symShiftNegated" $ \(x :: a) ->
              forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
                \(s :: Int) -> ioProperty $ do
                  symShiftNegated x (fromIntegral s)
                    @?= shift x (-fromIntegral (fromIntegral s :: a)),
            testProperty "symShift max" $ \(x :: a) ->
              ioProperty $ do
                case finiteBitSize x of
                  1 -> symShift x maxBound @?= x
                  2 -> symShift x maxBound @?= shift x 1
                  _ -> symShift x maxBound @?= 0,
            testProperty "symShiftNegated max" $ \(x :: a) ->
              ioProperty $ do
                case finiteBitSize x of
                  1 -> symShiftNegated x maxBound @?= x
                  2 -> symShiftNegated x maxBound @?= shift x (-1)
                  _ -> symShiftNegated x maxBound @?= if x >= 0 then 0 else -1,
            testProperty "symShift min" $ \(x :: a) ->
              ioProperty $ do
                case finiteBitSize x of
                  1 -> symShift x minBound @?= shift x (-1)
                  2 -> symShift x minBound @?= shift x (-2)
                  _ -> symShift x minBound @?= if x >= 0 then 0 else -1,
            testProperty "symShiftNegated min" $ \(x :: a) ->
              ioProperty $ symShiftNegated x minBound @?= 0
          ]
      ]
  
  symbolicTypeSymShiftTests ::
    forall proxy c s.
    ( Arbitrary c,
      Show s,
      Num s,
      SymShift c,
      SymShift s,
      FiniteBits c,
      Bounded c,
      Typeable s,
      Integral c,
      Solvable c s,
      Show c,
      KeyEq s
    ) =>
    proxy s ->
    Test
  symbolicTypeSymShiftTests p =
    testGroup
      (show $ typeRep p)
      [ testGroup
          "SymShift"
          [ testProperty "concrete/concrete symShift" $ \(x :: c) ->
              forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
                \(s :: Int) ->
                  ioProperty $
                    AsKey (symShift (con x :: s) (fromIntegral s))
                      @?= con (symShift x (fromIntegral s)),
            testProperty "concrete/concrete symShiftNegated" $ \(x :: c) ->
              forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
                \(s :: Int) ->
                  ioProperty $
                    AsKey (symShiftNegated (con x :: s) (fromIntegral s))
                      @?= con (symShiftNegated x (fromIntegral s)),
            testProperty "symShift max" $ \(x :: c) ->
              ioProperty $
                AsKey (symShift (con x :: s) (con maxBound))
                  @?= con (symShift x maxBound),
            testProperty "symShiftNegated max" $ \(x :: c) ->
              ioProperty $
                AsKey (symShiftNegated (con x :: s) (con maxBound))
                  @?= con (symShiftNegated x maxBound),
            testProperty "symShift min" $ \(x :: c) ->
              ioProperty $ do
                AsKey (symShift (con x :: s) (con minBound))
                  @?= con (symShift x minBound),
            testProperty "symShiftNegated min" $ \(x :: c) ->
              ioProperty $ do
                AsKey (symShiftNegated (con x :: s) (con minBound))
                  @?= con (symShiftNegated x minBound)
          ]
      ]
  
  symShiftTests :: Test
  symShiftTests =
    testGroup
      "SymShift"
      [ concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word8),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word16),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word32),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word64),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 1)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 2)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 3)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 63)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 64)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 65)),
        concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 128)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy Int8),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy Int16),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy Int32),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy Int64),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy Int),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 1)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 2)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 3)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 63)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 64)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 65)),
        concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 128)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 1)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 2)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 3)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 63)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 64)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 65)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 128)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 1)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 2)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 3)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 63)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 64)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 65)),
        symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 128))
      ]
  