content: {-# LANGUAGE CPP #-}
  {-# 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.Maybe (fromMaybe, isJust)
  import GHC.TypeNats (someNatVal)
  import Test.Tasty (TestTree, defaultMain)
  import Test.Tasty.HUnit (Assertion, assertBool, testCase)
  import Test.Tasty.TH (testGroupGenerator)
  
  #if MIN_VERSION_base(4,18,0)
  import Clash.Prelude hiding (someNatVal, withSomeSNat)
  #else
  import Clash.Prelude hiding (someNatVal)
  #endif
  
  #if !MIN_VERSION_base(4,16,0)
  import Numeric.Natural (Natural)
  #endif
  
  import qualified Data.List as L
  
  main :: IO ()
  main = defaultMain tests
  
  tests :: TestTree
  tests = $(testGroupGenerator)
  
  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)
  