{-# LANGUAGE BinaryLiterals #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Grisette.SymPrim.Prim.BitsTests (bitsTests) where

import Data.Bits (Bits (rotateL, rotateR), FiniteBits)
import Grisette
  ( IntN,
    SymRotate,
    WordN,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalRotateTerm
      ( pevalRotateLeftTerm,
        pevalRotateRightTerm
      ),
    PEvalShiftTerm
      ( pevalShiftLeftTerm,
        pevalShiftRightTerm
      ),
    Term,
    andBitsTerm,
    complementBitsTerm,
    conTerm,
    orBitsTerm,
    rotateLeftTerm,
    rotateRightTerm,
    shiftLeftTerm,
    shiftRightTerm,
    ssymTerm,
    xorBitsTerm,
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit ((@=?))
import Test.QuickCheck (Property, discard, ioProperty)

bitsTests :: Test
bitsTests =
  testGroup
    "Bits"
    [ testGroup
        "AndBits"
        [ testCase "On both concrete" $ do
            pevalAndBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @=? conTerm 1,
          testCase "On zeroBits" $ do
            pevalAndBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @=? conTerm 0
            pevalAndBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @=? conTerm 0,
          testCase "On all one bits" $ do
            pevalAndBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @=? ssymTerm "a"
            pevalAndBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @=? ssymTerm "a",
          testCase "On symbolic" $ do
            pevalAndBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @=? andBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "OrBits"
        [ testCase "On both concrete" $ do
            pevalOrBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @=? conTerm 7,
          testCase "On zeroBits" $ do
            pevalOrBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @=? ssymTerm "a"
            pevalOrBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @=? ssymTerm "a",
          testCase "On all one bits" $ do
            pevalOrBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @=? conTerm 15
            pevalOrBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @=? conTerm 15,
          testCase "On symbolic" $ do
            pevalOrBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @=? orBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "XorBits"
        [ testCase "On both concrete" $ do
            pevalXorBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @=? conTerm 6,
          testCase "On zeroBits" $ do
            pevalXorBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @=? ssymTerm "a"
            pevalXorBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @=? ssymTerm "a",
          testCase "On all one bits" $ do
            pevalXorBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @=? pevalComplementBitsTerm (ssymTerm "a")
            pevalXorBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @=? pevalComplementBitsTerm (ssymTerm "a"),
          testCase "On single complement" $ do
            pevalXorBitsTerm
              (pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @=? pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"))
            pevalXorBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (pevalComplementBitsTerm $ ssymTerm "b")
              @=? pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both complement" $ do
            pevalXorBitsTerm
              (pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
              (pevalComplementBitsTerm $ ssymTerm "b")
              @=? pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"),
          testCase "On symbolic" $ do
            pevalXorBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @=? xorBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "ComplementBits"
        [ testCase "On concrete" $ do
            pevalComplementBitsTerm (conTerm 5 :: Term (WordN 4)) @=? conTerm 10,
          testCase "On complement" $ do
            pevalComplementBitsTerm (pevalComplementBitsTerm (ssymTerm "a") :: Term (WordN 4)) @=? ssymTerm "a",
          testCase "On symbolic" $ do
            pevalComplementBitsTerm (ssymTerm "a" :: Term (WordN 4))
              @=? complementBitsTerm (ssymTerm "a" :: Term (WordN 4))
        ],
      testGroup
        "ShiftLeft"
        [ testCase "On concrete" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @=? conTerm 12
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @=? conTerm 12,
          testCase "shift 0" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
          testCase "shift greater or equal to left bitsize" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @=? conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4) @=? conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @=? conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5) @=? conTerm 0,
          testCase "shift negative amount is undefined on for IntN" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @=? shiftLeftTerm (conTerm 15) (conTerm $ -1)
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @=? shiftLeftTerm (conTerm 15) (conTerm $ -8),
          testCase "shift symbolic" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @=? shiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: shift by very large number" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm 0
            pevalShiftLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm 0
        ],
      testGroup
        "ShiftRight"
        [ testCase "On concrete, should perform arithmetic shifting on IntN" $ do
            pevalShiftRightTerm (conTerm 7 :: Term (IntN 4)) (conTerm 2) @=? conTerm 1
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @=? conTerm 15,
          testCase "On concrete, should perform logical shifting on WordN" $ do
            pevalShiftRightTerm (conTerm 7 :: Term (WordN 4)) (conTerm 2) @=? conTerm 1
            pevalShiftRightTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @=? conTerm 3,
          testCase "shift 0" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
          testCase "shift greater or equal to left bitsize on WordN" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @=? conTerm 0
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @=? conTerm 0,
          testCase "shift greater or equal to left bitsize on IntN will not be reduced" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @=? shiftRightTerm (ssymTerm "a") (conTerm 5)
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @=? shiftRightTerm (ssymTerm "a") (conTerm 4),
          testCase "shift negative amount is undefined on for IntN" $ do
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @=? shiftRightTerm (conTerm 15) (conTerm $ -1)
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @=? shiftRightTerm (conTerm 15) (conTerm $ -8),
          testCase "shift symbolic" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @=? shiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: shift by very large number" $ do
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm 0
            pevalShiftRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm 0
        ],
      testGroup
        "RotateLeft"
        [ testCase "On concrete" $ do
            pevalRotateLeftTerm (conTerm 0b10100101 :: Term (WordN 8)) (conTerm 2) @=? conTerm 0b10010110
            pevalRotateLeftTerm (conTerm 0b10100101 :: Term (IntN 8)) (conTerm 2) @=? conTerm 0b10010110,
          testCase "rotate 0" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
          testCase "rotate bitsize" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
              @=? ssymTerm "a"
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @=? ssymTerm "a",
          testCase "rotate greater than left bitsize" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
              @=? rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @=? rotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
          testCase "rotate negative amount is undefined on for IntN" $ do
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @=? rotateLeftTerm (conTerm 15) (conTerm $ -1)
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @=? rotateLeftTerm (conTerm 15) (conTerm $ -8),
          testCase "rotate symbolic" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @=? rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: rotate by very large number" $ do
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm (rotateR 15 1)
            pevalRotateLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm (rotateR 15 1)
        ],
      testGroup
        "RotateRight"
        [ testProperty "On concrete WordN 1" $
            concreteSmallRotateRightCorrect @(WordN 1),
          testProperty "On concrete WordN 2" $
            concreteSmallRotateRightCorrect @(WordN 2),
          testProperty "On concrete WordN 3" $
            concreteSmallRotateRightCorrect @(WordN 3),
          testProperty "On concrete WordN 4" $
            concreteSmallRotateRightCorrect @(WordN 4),
          testProperty "On concrete WordN 8" $
            concreteSmallRotateRightCorrect @(WordN 8),
          testProperty "On concrete IntN 1" $
            concreteSmallRotateRightCorrect @(IntN 1),
          testProperty "On concrete IntN 2" $
            concreteSmallRotateRightCorrect @(IntN 2),
          testProperty "On concrete IntN 3" $
            concreteSmallRotateRightCorrect @(IntN 3),
          testProperty "On concrete IntN 4" $
            concreteSmallRotateRightCorrect @(IntN 4),
          testProperty "On concrete IntN 8" $
            concreteSmallRotateRightCorrect @(IntN 8),
          testCase "rotate 0" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
          testCase "rotate bitsize" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
              @=? ssymTerm "a"
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @=? ssymTerm "a",
          testCase "rotate greater than left bitsize" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
              @=? rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @=? rotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
          testCase "rotate negative amount is undefined on for IntN" $ do
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @=? rotateRightTerm (conTerm 15) (conTerm $ -1)
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @=? rotateRightTerm (conTerm 15) (conTerm $ -8),
          testCase "rotate symbolic" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @=? rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: rotate by very large number" $ do
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm (rotateL 15 1)
            pevalRotateRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm (rotateL 15 1)
        ]
    ]

concreteSmallRotateRightCorrect ::
  (PEvalRotateTerm a, Integral a, FiniteBits a, SymRotate a) =>
  a ->
  a ->
  Property
concreteSmallRotateRightCorrect _ b | b < 0 = discard
concreteSmallRotateRightCorrect a b = ioProperty $ do
  pevalRotateRightTerm (conTerm a) (conTerm b)
    @=? conTerm (rotateR a (fromIntegral b))