content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Grisette.Core.Data.Class.SafeLinearArithTests
    ( safeLinearArithTests,
    )
  where
  
  import Control.Exception (ArithException (Overflow, Underflow))
  import Control.Monad.Except (ExceptT, MonadError)
  import Data.Data (Proxy (Proxy), Typeable, typeRep)
  import Data.Int (Int16, Int32, Int64, Int8)
  import Data.Word (Word16, Word32, Word64, Word8)
  import Grisette
    ( BV (bv),
      IntN,
      Mergeable,
      SafeLinearArith (safeAdd, safeNeg, safeSub),
      SomeBVException (BitwidthMismatch),
      SomeIntN,
      SomeWordN,
      TryMerge,
      Union,
      WordN,
      mrgSingle,
      pattern SomeIntN,
      pattern SomeWordN,
    )
  import Grisette.Lib.Control.Monad.Except (mrgModifyError, mrgThrowError)
  import Grisette.Lib.Data.Functor (mrgFmap)
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit ((@?=))
  import Test.QuickCheck (Arbitrary, ioProperty)
  
  binSafeOp ::
    forall a m.
    ( Integral a,
      Bounded a,
      MonadError ArithException m,
      TryMerge m,
      Mergeable a
    ) =>
    (Integer -> Integer -> Integer) ->
    a ->
    a ->
    m a
  binSafeOp op l r
    | result > fromIntegral (maxBound :: a) =
        mrgThrowError Overflow
    | result < fromIntegral (minBound :: a) =
        mrgThrowError Underflow
    | otherwise = mrgSingle $ fromIntegral result
    where
      result = op (fromIntegral l) (fromIntegral r)
  
  unarySafeOp ::
    forall a m.
    ( Integral a,
      Bounded a,
      MonadError ArithException m,
      TryMerge m,
      Mergeable a
    ) =>
    (Integer -> Integer) ->
    a ->
    m a
  unarySafeOp op l
    | result > fromIntegral (maxBound :: a) =
        mrgThrowError Overflow
    | result < fromIntegral (minBound :: a) =
        mrgThrowError Underflow
    | otherwise = mrgSingle $ fromIntegral result
    where
      result = op (fromIntegral l)
  
  safeLinearArithTest ::
    forall a b e.
    ( SafeLinearArith e b (ExceptT e Union),
      Integral a,
      Bounded a,
      Arbitrary a,
      Show a,
      Show b,
      Eq b,
      Eq e,
      Show e,
      Typeable a,
      Mergeable a,
      Mergeable e
    ) =>
    (a -> b) ->
    (ArithException -> e) ->
    Test
  safeLinearArithTest wrap transformError =
    testGroup
      (show $ typeRep (Proxy @a))
      [ testProperty "safeAdd" $ \(l :: a) (r :: a) -> ioProperty $ do
          let actual = safeAdd (wrap l) (wrap r)
          let expected = mrgModifyError transformError $ binSafeOp (+) l r
          actual @?= (mrgFmap wrap expected :: ExceptT e Union b),
        testProperty "safeSub" $ \(l :: a) (r :: a) -> ioProperty $ do
          let actual = safeSub (wrap l) (wrap r)
          let expected = mrgModifyError transformError $ binSafeOp (-) l r
          actual @?= (mrgFmap wrap expected :: ExceptT e Union b),
        testProperty "safeNeg" $ \(l :: a) -> ioProperty $ do
          let actual = safeNeg (wrap l) :: ExceptT e Union b
          let expected = mrgModifyError transformError $ unarySafeOp negate l
          actual @?= mrgFmap wrap expected
      ]
  
  safeLinearArithTestSimple ::
    forall a.
    ( SafeLinearArith ArithException a (ExceptT ArithException Union),
      Integral a,
      Bounded a,
      Arbitrary a,
      Show a,
      Typeable a
    ) =>
    Test
  safeLinearArithTestSimple = safeLinearArithTest @a @a id id
  
  safeLinearArithTests :: Test
  safeLinearArithTests =
    testGroup
      "SafeLinearArith"
      [ safeLinearArithTestSimple @Int,
        safeLinearArithTestSimple @Int8,
        safeLinearArithTestSimple @Int16,
        safeLinearArithTestSimple @Int32,
        safeLinearArithTestSimple @Int64,
        safeLinearArithTestSimple @(IntN 1),
        safeLinearArithTestSimple @(IntN 2),
        safeLinearArithTestSimple @(IntN 3),
        safeLinearArithTestSimple @(IntN 128),
        safeLinearArithTest @(IntN 2)
          @SomeIntN
          @(Either SomeBVException ArithException)
          SomeIntN
          Right,
        safeLinearArithTest @(IntN 128)
          @SomeIntN
          @(Either SomeBVException ArithException)
          SomeIntN
          Right,
        testCase "SomeIntN different bit width" $ do
          let l = bv 2 1 :: SomeIntN
          let r = bv 3 1 :: SomeIntN
          let actual =
                safeAdd l r ::
                  ExceptT (Either SomeBVException ArithException) Union SomeIntN
          let expected = mrgThrowError $ Left BitwidthMismatch
          actual @?= expected,
        safeLinearArithTestSimple @Word,
        safeLinearArithTestSimple @Word8,
        safeLinearArithTestSimple @Word16,
        safeLinearArithTestSimple @Word32,
        safeLinearArithTestSimple @Word64,
        safeLinearArithTestSimple @(WordN 1),
        safeLinearArithTestSimple @(WordN 2),
        safeLinearArithTestSimple @(WordN 3),
        safeLinearArithTestSimple @(WordN 128),
        safeLinearArithTest @(WordN 2)
          @SomeWordN
          @(Either SomeBVException ArithException)
          SomeWordN
          Right,
        safeLinearArithTest @(WordN 128)
          @SomeWordN
          @(Either SomeBVException ArithException)
          SomeWordN
          Right,
        testCase "SomeWordN different bit width" $ do
          let l = bv 2 1 :: SomeWordN
          let r = bv 3 1 :: SomeWordN
          let actual =
                safeAdd l r ::
                  ExceptT
                    (Either SomeBVException ArithException)
                    Union
                    SomeWordN
          let expected = mrgThrowError $ Left BitwidthMismatch
          actual @?= expected
      ]
  