{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}

{- |
Copyright  :  (C) 2025     , Martijn Bastiaan
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

Test generation of 'MaybeNumConvert' instances:

> for a in ["Index", "Unsigned", "Signed", "BitVector"]:
>     for b in ["Index", "Unsigned", "Signed", "BitVector"]:
>          ia_max = "indexMax" if a == "Index" else "otherMax"
>          ib_max = "indexMax" if b == "Index" else "otherMax"
>          n = "(n + 1)" if a == "Index" else "n"
>          m = "(m + 1)" if b == "Index" else "m"
>          print(f"""case_maybeConvert{a}{b} :: Assertion
> case_maybeConvert{a}{b} =
>   forM_ [0 .. {ia_max}] $ \\n ->
>     forM_ [0 .. {ib_max}] $ \\m ->
>       withSomeSNat n $ \(SNat :: SNat n) ->
>         withSomeSNat m $ \(SNat :: SNat m) ->
>           forM_ [minBound .. maxBound] $ \(i :: {a} {n}) -> do
>             assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @({b} {m})) i)
>             assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @({b} {m})) i)
>             assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @({b} {m})) i)
>             assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @({b} {m})) i)
>  """)
-}
module Clash.Tests.MaybeNumConvert where

import Control.Monad (forM_)
import Data.Data (Proxy (..))
import Data.Int (Int64)
import Data.Maybe (fromMaybe, isJust)
import Data.Word (Word64)
import GHC.TypeNats (someNatVal)
import Test.Tasty (TestTree, defaultMain)
import Test.Tasty.HUnit (Assertion, assertBool, testCase)
import Test.Tasty.TH (testGroupGenerator)

import Clash.Prelude hiding (someNatVal, withSomeSNat)

import qualified Data.List as L

main :: IO ()
main = defaultMain tests

tests :: TestTree
tests = $(testGroupGenerator)

-- Tests for maybeNumConvert (conversions that can fail)

case_MaybeInt64Word64 :: Assertion
case_MaybeInt64Word64 = do
  -- Successful conversions (non-negative values)
  assertBool "0" $ maybeNumConvert (0 :: Int64) == Just (0 :: Word64)
  assertBool "1" $ maybeNumConvert (1 :: Int64) == Just (1 :: Word64)
  assertBool "42" $ maybeNumConvert (42 :: Int64) == Just (42 :: Word64)
  assertBool "maxBound" $ maybeNumConvert (maxBound :: Int64) == Just (9223372036854775807 :: Word64)
  -- Failed conversions (negative values)
  assertBool "-1" $ maybeNumConvert (-1 :: Int64) == (Nothing :: Maybe Word64)
  assertBool "-42" $ maybeNumConvert (-42 :: Int64) == (Nothing :: Maybe Word64)
  assertBool "minBound" $ maybeNumConvert (minBound :: Int64) == (Nothing :: Maybe Word64)

case_MaybeWord64Unsigned32 :: Assertion
case_MaybeWord64Unsigned32 = do
  -- Successful conversions (small values)
  assertBool "0" $ maybeNumConvert (0 :: Word64) == Just (0 :: Unsigned 32)
  assertBool "1" $ maybeNumConvert (1 :: Word64) == Just (1 :: Unsigned 32)
  assertBool "42" $ maybeNumConvert (42 :: Word64) == Just (42 :: Unsigned 32)
  assertBool "maxBound32" $ maybeNumConvert (4294967295 :: Word64) == Just (maxBound :: Unsigned 32)
  -- Failed conversions (values too large)
  assertBool "overflow1" $ maybeNumConvert (4294967296 :: Word64) == (Nothing :: Maybe (Unsigned 32))
  assertBool "overflow2" $ maybeNumConvert (5000000000 :: Word64) == (Nothing :: Maybe (Unsigned 32))
  assertBool "maxBound64" $ maybeNumConvert (maxBound :: Word64) == (Nothing :: Maybe (Unsigned 32))

withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat n f = case someNatVal n of
  SomeNat (_ :: Proxy n) -> f (SNat @n)

maybeConvertLaw1 ::
  forall a b.
  (Eq a, MaybeNumConvert a b, MaybeNumConvert b a) =>
  Proxy b ->
  a ->
  Bool
maybeConvertLaw1 Proxy x =
  x == fromMaybe x (maybeNumConvert @_ @b x >>= maybeNumConvert)

maybeConvertLaw2 ::
  forall a b.
  (MaybeNumConvert a b, MaybeNumConvert b a, Integral b, Integral a) =>
  Proxy b ->
  a ->
  Bool
maybeConvertLaw2 Proxy x =
  toInteger x == fromMaybe (toInteger x) (toInteger <$> maybeNumConvert @_ @b x)

maybeConvertLaw3 ::
  forall a b.
  (MaybeNumConvert a b, MaybeNumConvert b a, Integral b, Integral a) =>
  Proxy b ->
  a ->
  Bool
maybeConvertLaw3 Proxy x =
  isJust (maybeNumConvert @_ @b x) `implies` isJust (maybeNumConvert @_ @a =<< maybeNumConvert @_ @b x)
 where
  implies :: Bool -> Bool -> Bool
  implies True False = False
  implies _ _ = True

maybeConvertLaw4 ::
  forall a b.
  (MaybeNumConvert a b, MaybeNumConvert b a, Integral b, Integral a, Bounded b, Bounded a) =>
  Proxy b ->
  a ->
  Bool
maybeConvertLaw4 Proxy x =
  isJust (maybeNumConvert @_ @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b))
 where
  i :: (Integral c) => c -> Integer
  i = toInteger

-- | Checks whether an 'XException' in, means an 'XException' out
convertXException :: forall a b. (MaybeNumConvert a b) => Proxy a -> Proxy b -> Bool
convertXException _ _ = case isX $ maybeNumConvert @a @b (errorX "BOO" :: a) of
  Left s -> "BOO" `L.isInfixOf` s
  Right _ -> False

indexMax :: Natural
indexMax = 128

otherMax :: Natural
otherMax = 8

case_maybeConvertIndexIndex :: Assertion
case_maybeConvertIndexIndex =
  forM_ [0 .. indexMax] $ \n ->
    forM_ [0 .. indexMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Index (n + 1))) (Proxy @(Index (m + 1))))
          forM_ [minBound .. maxBound] $ \(i :: Index (n + 1)) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Index (m + 1))) i)

case_maybeConvertIndexUnsigned :: Assertion
case_maybeConvertIndexUnsigned =
  forM_ [0 .. indexMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Index (n + 1))) (Proxy @(Unsigned m)))
          forM_ [minBound .. maxBound] $ \(i :: Index (n + 1)) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Unsigned m)) i)

case_maybeConvertIndexSigned :: Assertion
case_maybeConvertIndexSigned =
  forM_ [0 .. indexMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Index (n + 1))) (Proxy @(Signed m)))
          forM_ [minBound .. maxBound] $ \(i :: Index (n + 1)) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Signed m)) i)

case_maybeConvertIndexBitVector :: Assertion
case_maybeConvertIndexBitVector =
  forM_ [0 .. indexMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Index (n + 1))) (Proxy @(BitVector m)))
          forM_ [minBound .. maxBound] $ \(i :: Index (n + 1)) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(BitVector m)) i)

case_maybeConvertUnsignedIndex :: Assertion
case_maybeConvertUnsignedIndex =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. indexMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(Index (m + 1))))
          forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Index (m + 1))) i)

case_maybeConvertUnsignedUnsigned :: Assertion
case_maybeConvertUnsignedUnsigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(Unsigned m)))
          forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Unsigned m)) i)

case_maybeConvertUnsignedSigned :: Assertion
case_maybeConvertUnsignedSigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(Signed m)))
          forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Signed m)) i)

case_maybeConvertUnsignedBitVector :: Assertion
case_maybeConvertUnsignedBitVector =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(BitVector m)))
          forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(BitVector m)) i)

case_maybeConvertSignedIndex :: Assertion
case_maybeConvertSignedIndex =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. indexMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Signed n)) (Proxy @(Index (m + 1))))
          forM_ [minBound .. maxBound] $ \(i :: Signed n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Index (m + 1))) i)

case_maybeConvertSignedUnsigned :: Assertion
case_maybeConvertSignedUnsigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Signed n)) (Proxy @(Unsigned m)))
          forM_ [minBound .. maxBound] $ \(i :: Signed n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Unsigned m)) i)

case_maybeConvertSignedSigned :: Assertion
case_maybeConvertSignedSigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Signed n)) (Proxy @(Signed m)))
          forM_ [minBound .. maxBound] $ \(i :: Signed n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Signed m)) i)

case_maybeConvertSignedBitVector :: Assertion
case_maybeConvertSignedBitVector =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(Signed n)) (Proxy @(BitVector m)))
          forM_ [minBound .. maxBound] $ \(i :: Signed n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(BitVector m)) i)

case_maybeConvertBitVectorIndex :: Assertion
case_maybeConvertBitVectorIndex =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. indexMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(Index (m + 1))))
          forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Index (m + 1))) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Index (m + 1))) i)

case_maybeConvertBitVectorUnsigned :: Assertion
case_maybeConvertBitVectorUnsigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(Unsigned m)))
          forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Unsigned m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Unsigned m)) i)

case_maybeConvertBitVectorSigned :: Assertion
case_maybeConvertBitVectorSigned =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(Signed m)))
          forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(Signed m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(Signed m)) i)

case_maybeConvertBitVectorBitVector :: Assertion
case_maybeConvertBitVectorBitVector =
  forM_ [0 .. otherMax] $ \n ->
    forM_ [0 .. otherMax] $ \m ->
      withSomeSNat n $ \(SNat :: SNat n) ->
        withSomeSNat m $ \(SNat :: SNat m) -> do
          assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(BitVector m)))
          forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do
            assertBool (show (n, m, i)) (maybeConvertLaw1 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw2 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw3 (Proxy @(BitVector m)) i)
            assertBool (show (n, m, i)) (maybeConvertLaw4 (Proxy @(BitVector m)) i)