From 25c7757188b69331db282ed9eb0f3e572eeadce5 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Sun, 30 Mar 2025 20:42:47 +0200 Subject: [PATCH] Add `Clash.Class.Convert` Utilities for safely converting between various Clash number types. --- ...-30T20_42_00+02_00_add_clash_class_convert | 1 + clash-prelude/clash-prelude.cabal | 5 + clash-prelude/src/Clash/Class/Convert.hs | 31 ++ .../Clash/Class/Convert/Internal/Convert.hs | 164 +++++++++ .../Class/Convert/Internal/MaybeConvert.hs | 160 +++++++++ clash-prelude/tests/Clash/Tests/Convert.hs | 307 +++++++++++++++++ .../tests/Clash/Tests/MaybeConvert.hs | 323 ++++++++++++++++++ clash-prelude/tests/unittests.hs | 6 +- 8 files changed, 996 insertions(+), 1 deletion(-) create mode 100644 changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert create mode 100644 clash-prelude/src/Clash/Class/Convert.hs create mode 100644 clash-prelude/src/Clash/Class/Convert/Internal/Convert.hs create mode 100644 clash-prelude/src/Clash/Class/Convert/Internal/MaybeConvert.hs create mode 100644 clash-prelude/tests/Clash/Tests/Convert.hs create mode 100644 clash-prelude/tests/Clash/Tests/MaybeConvert.hs diff --git a/changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert b/changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert new file mode 100644 index 0000000000..1ff8a4254e --- /dev/null +++ b/changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert @@ -0,0 +1 @@ +ADD: `Clash.Class.Convert`: Utilities for safely converting between various Clash number types diff --git a/clash-prelude/clash-prelude.cabal b/clash-prelude/clash-prelude.cabal index 8871d82623..3ff6affe45 100644 --- a/clash-prelude/clash-prelude.cabal +++ b/clash-prelude/clash-prelude.cabal @@ -182,6 +182,9 @@ Library Clash.Class.Counter Clash.Class.Counter.Internal Clash.Class.Counter.TH + Clash.Class.Convert + Clash.Class.Convert.Internal.Convert + Clash.Class.Convert.Internal.MaybeConvert Clash.Class.Exp Clash.Class.HasDomain Clash.Class.HasDomain.HasSingleDomain @@ -428,10 +431,12 @@ test-suite unittests Clash.Tests.BlockRam.Blob Clash.Tests.Clocks Clash.Tests.Counter + Clash.Tests.Convert Clash.Tests.DerivingDataRepr Clash.Tests.DerivingDataReprTypes Clash.Tests.Fixed Clash.Tests.FixedExhaustive + Clash.Tests.MaybeConvert Clash.Tests.MaybeX Clash.Tests.NFDataX Clash.Tests.NumNewtypes diff --git a/clash-prelude/src/Clash/Class/Convert.hs b/clash-prelude/src/Clash/Class/Convert.hs new file mode 100644 index 0000000000..d26290ea82 --- /dev/null +++ b/clash-prelude/src/Clash/Class/Convert.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE UndecidableInstances #-} + +{- | Utilities for converting between Clash number types in a safe way. Its +existence is motivated by the observation that Clash users often need to convert +between different number types (e.g., 'Clash.Sized.Unsigned.Unsigned' to +'Clash.Sized.Signed.Signed') and that it is not always clear how to do so +properly. Two classes are exported: + +* 'Convert': for conversions that, based on types, are guaranteed to succeed. +* 'MaybeConvert': for conversions that may fail for some values. + +As opposed to 'Prelude.fromIntegral', all conversions are translatable to +synthesizable HDL. + +== __Relation to @convertible@__ +@clash-convertible@ is similar to the @convertible@ package in that it aims to +facilitate conversions between different number types. It has two key differences: + + 1. It offers no partial functions. + 2. All its conversions are translatable to synthesizable HDL. + +-} +module Clash.Class.Convert ( + Convert (..), + MaybeConvert (..), +) where + +import Clash.Class.Convert.Internal.Convert +import Clash.Class.Convert.Internal.MaybeConvert diff --git a/clash-prelude/src/Clash/Class/Convert/Internal/Convert.hs b/clash-prelude/src/Clash/Class/Convert/Internal/Convert.hs new file mode 100644 index 0000000000..7e378d06ee --- /dev/null +++ b/clash-prelude/src/Clash/Class/Convert/Internal/Convert.hs @@ -0,0 +1,164 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_HADDOCK hide #-} + +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-} + +module Clash.Class.Convert.Internal.Convert where + +import Prelude + +import Clash.Class.BitPack +import Clash.Class.Resize +import Clash.Sized.BitVector +import Clash.Sized.Index +import Clash.Sized.Signed +import Clash.Sized.Unsigned + +import GHC.TypeLits.Extra (CLog) +import GHC.TypeLits (KnownNat, type (<=), type (+), type (^)) + +import Data.Int (Int16, Int32, Int64, Int8) +import Data.Word (Word16, Word32, Word64, Word8) + +{- $setup +>>> import Clash.Prelude +>>> import Clash.Class.Convert +-} + +{- | Conversions that are, based on their types, guaranteed to succeed. + +== __Laws__ +A conversion is safe and total if a round trip conversion is guaranteed to be +lossless. I.e., + +> Just x == maybeConvert (convert @a @b x) + +for all values @x@ of type @a@. It should also preserve the numerical value +interpretation of the bits. For types that have an "Integral" instance, this +intuition is captured by: + +> toInteger x == toInteger (convert @a @b x) + +Instances should make sure their constraints are as \"tight\" as possible. I.e., +if an instance exist, but the constraints cannot be satisfied, then +'Clash.Class.Convert.convertMaybe' should return 'Nothing' for one or more values in +the domain of the source type @a@: + +> L.any isNothing (L.map (maybeConvert @a @b) [minBound ..]) + +Additionally, any implementation should be translatable to synthesizable RTL. +-} +class Convert a b where + {- | Convert a supplied value of type @a@ to a value of type @b@. The conversion + is guaranteed to succeed. + + >>> convert (3 :: Index 8) :: Unsigned 8 + 3 + + The following will fail with a type error, as we cannot prove that all values + of @Index 8@ can be represented by an @Unsigned 2@: + + >>> convert (3 :: Index 8) :: Unsigned 2 + ... + + For the time being, if the input is an @XException@, then the output is too. This + property might be relaxed in the future. + -} + convert :: a -> b + +instance (KnownNat n, KnownNat m, n <= m) => Convert (Index n) (Index m) where + convert = resize + +instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (Unsigned m) where + convert !a = resize $ bitCoerce a + +{- | Note: Conversion from @Index 1@ to @Signed 0@ is total, but not within the +constraints of the instance. +-} +instance (KnownNat n, KnownNat m, 1 <= n, CLog 2 n + 1 <= m) => Convert (Index n) (Signed m) where + convert !a = convert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a + +instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (BitVector m) where + convert !a = resize $ pack a + +instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (Unsigned n) (Index m) where + convert !a = bitCoerce $ resize a + +instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (Unsigned m) where + convert = resize + +{- | Note: Conversion from @Unsigned 0@ to @Signed 0@ is total, but not within the +constraints of the instance. +-} +instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (Unsigned n) (Signed m) where + convert = bitCoerce . resize + +instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (BitVector m) where + convert !a = resize $ pack a + +instance (KnownNat n, KnownNat m, n <= m) => Convert (Signed n) (Signed m) where + convert !a = resize a + +instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (BitVector n) (Index m) where + convert = unpack . resize + +instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (Unsigned m) where + convert = unpack . resize + +{- | Note: Conversion from @BitVector 0@ to @Signed 0@ is total, but not within the +constraints of the instance. +-} +instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (BitVector n) (Signed m) where + convert = unpack . resize + +instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (BitVector m) where + convert = resize + +instance (Convert (Unsigned 64) a) => Convert Word a where + convert = convert . bitCoerce @_ @(Unsigned 64) +instance (Convert (Unsigned 64) a) => Convert Word64 a where + convert = convert . bitCoerce @_ @(Unsigned 64) +instance (Convert (Unsigned 32) a) => Convert Word32 a where + convert = convert . bitCoerce @_ @(Unsigned 32) +instance (Convert (Unsigned 16) a) => Convert Word16 a where + convert = convert . bitCoerce @_ @(Unsigned 16) +instance (Convert (Unsigned 8) a) => Convert Word8 a where + convert = convert . bitCoerce @_ @(Unsigned 8) + +instance (Convert (Signed 64) a) => Convert Int a where + convert = convert . bitCoerce @_ @(Signed 64) +instance (Convert (Signed 64) a) => Convert Int64 a where + convert = convert . bitCoerce @_ @(Signed 64) +instance (Convert (Signed 32) a) => Convert Int32 a where + convert = convert . bitCoerce @_ @(Signed 32) +instance (Convert (Signed 16) a) => Convert Int16 a where + convert = convert . bitCoerce @_ @(Signed 16) +instance (Convert (Signed 8) a) => Convert Int8 a where + convert = convert . bitCoerce @_ @(Signed 8) + +instance (Convert a (Unsigned 64)) => Convert a Word where + convert = bitCoerce @(Unsigned 64) . convert +instance (Convert a (Unsigned 64)) => Convert a Word64 where + convert = bitCoerce @(Unsigned 64) . convert +instance (Convert a (Unsigned 32)) => Convert a Word32 where + convert = bitCoerce @(Unsigned 32) . convert +instance (Convert a (Unsigned 16)) => Convert a Word16 where + convert = bitCoerce @(Unsigned 16) . convert +instance (Convert a (Unsigned 8)) => Convert a Word8 where + convert = bitCoerce @(Unsigned 8) . convert + +instance (Convert a (Signed 64)) => Convert a Int where + convert = bitCoerce @(Signed 64) . convert +instance (Convert a (Signed 64)) => Convert a Int64 where + convert = bitCoerce @(Signed 64) . convert +instance (Convert a (Signed 32)) => Convert a Int32 where + convert = bitCoerce @(Signed 32) . convert +instance (Convert a (Signed 16)) => Convert a Int16 where + convert = bitCoerce @(Signed 16) . convert +instance (Convert a (Signed 8)) => Convert a Int8 where + convert = bitCoerce @(Signed 8) . convert diff --git a/clash-prelude/src/Clash/Class/Convert/Internal/MaybeConvert.hs b/clash-prelude/src/Clash/Class/Convert/Internal/MaybeConvert.hs new file mode 100644 index 0000000000..3abe231f73 --- /dev/null +++ b/clash-prelude/src/Clash/Class/Convert/Internal/MaybeConvert.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_HADDOCK hide #-} + +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-} + +module Clash.Class.Convert.Internal.MaybeConvert where + +import Clash.Class.BitPack +import Clash.Class.Resize +import Clash.Sized.BitVector +import Clash.Sized.Index +import Clash.Sized.Signed +import Clash.Sized.Unsigned + +import GHC.TypeLits.Extra (CLog) +import GHC.TypeLits (KnownNat, type (<=), type (+), type (^)) + +import Data.Int (Int16, Int32, Int64, Int8) +import Data.Word (Word16, Word32, Word64, Word8) + +{- $setup +>>> import Clash.Prelude +>>> import Clash.Class.Convert +-} + +{- | Conversions that may fail for some values. + +== __Laws__ +A conversion is safe if a round trip conversion does not produce errors (also +see "Clash.XException"). I.e., + +> x == fromMaybe x (maybeConvert @a @b x >>= maybeConvert @b @a) + +for all values @x@ of type @a@. It should also preserve the numerical value +interpretation of the bits. For types that have an "Integral" instance, this +intuition is captured by: + +> toInteger x == fromMaybe (toInteger x) (toInteger (convert @a @b x)) + +If a conversion succeeds one way, it should also succeed the other way. I.e., + +> isJust (maybeConvert @a @b x) `implies` isJust (maybeConvert @a @b x >>= maybeConvert @b @a) + +A conversion should succeed if and only if the value is representable in the +target type. For types that have a "Bounded" and "Integral" instance, this +intuition is captured by: + +> isJust (maybeConvert @a @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b)) + +where @i = toInteger@. + +Additionally, any implementation should be translatable to synthesizable RTL. +-} +class MaybeConvert a b where + {- | Convert a supplied value of type @a@ to a value of type @b@. If the value + cannot be represented in the target type, 'Nothing' is returned. + + >>> maybeConvert (1 :: Index 8) :: Maybe (Unsigned 2) + Just 1 + >>> maybeConvert (7 :: Index 8) :: Maybe (Unsigned 2) + Nothing + + For the time being, if the input is an @XException@, then the output is too. + This property might be relaxed in the future. + -} + maybeConvert :: a -> Maybe b + +instance (KnownNat n, KnownNat m) => MaybeConvert (Index n) (Index m) where + maybeConvert !a = maybeResize a + +instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Unsigned m) where + maybeConvert !a = maybeResize $ bitCoerce @_ @(Unsigned (CLog 2 n)) a + +instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Signed m) where + maybeConvert !a = maybeConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a + +instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (BitVector m) where + maybeConvert !a = maybeResize $ pack a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Index m) where + maybeConvert !a = maybeResize $ bitCoerce @_ @(Index (2 ^ n)) a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Unsigned m) where + maybeConvert !a = maybeResize a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Signed m) where + maybeConvert !a = maybeResize $ bitCoerce @(Unsigned (n + 1)) $ extend a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (BitVector m) where + maybeConvert !a = maybeResize $ pack a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Index m) where + maybeConvert n + | n < 0 = Nothing + | otherwise = maybeResize (bitCoerce @_ @(Index (2 ^ (n + 1))) (extend n)) + +instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Unsigned m) where + maybeConvert n + | n < 0 = Nothing + | otherwise = maybeResize (bitCoerce @(Signed (n + 1)) (extend n)) + +instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Signed m) where + maybeConvert !a = maybeResize a + +instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (BitVector m) where + maybeConvert n + | n < 0 = Nothing + | otherwise = maybeResize (pack @(Signed (n + 1)) (extend n)) + +instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Index m) where + maybeConvert !a = maybeResize $ unpack @(Index (2 ^ n)) a + +instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Unsigned m) where + maybeConvert !a = maybeResize $ unpack @(Unsigned n) a + +instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Signed m) where + maybeConvert !a = maybeResize $ unpack @(Signed (n + 1)) $ extend a + +instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (BitVector m) where + maybeConvert !a = maybeResize a + +instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word a where + maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64) +instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word64 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64) +instance (MaybeConvert (Unsigned 32) a) => MaybeConvert Word32 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 32) +instance (MaybeConvert (Unsigned 16) a) => MaybeConvert Word16 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 16) +instance (MaybeConvert (Unsigned 8) a) => MaybeConvert Word8 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 8) + +instance (MaybeConvert (Signed 64) a) => MaybeConvert Int a where + maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64) +instance (MaybeConvert (Signed 64) a) => MaybeConvert Int64 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64) +instance (MaybeConvert (Signed 32) a) => MaybeConvert Int32 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Signed 32) +instance (MaybeConvert (Signed 16) a) => MaybeConvert Int16 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Signed 16) +instance (MaybeConvert (Signed 8) a) => MaybeConvert Int8 a where + maybeConvert = maybeConvert . bitCoerce @_ @(Signed 8) + +instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word where + maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert +instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word64 where + maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert +instance (MaybeConvert a (Unsigned 32)) => MaybeConvert a Word32 where + maybeConvert = fmap (bitCoerce @(Unsigned 32)) . maybeConvert +instance (MaybeConvert a (Unsigned 16)) => MaybeConvert a Word16 where + maybeConvert = fmap (bitCoerce @(Unsigned 16)) . maybeConvert +instance (MaybeConvert a (Unsigned 8)) => MaybeConvert a Word8 where + maybeConvert = fmap (bitCoerce @(Unsigned 8)) . maybeConvert diff --git a/clash-prelude/tests/Clash/Tests/Convert.hs b/clash-prelude/tests/Clash/Tests/Convert.hs new file mode 100644 index 0000000000..7f09182c78 --- /dev/null +++ b/clash-prelude/tests/Clash/Tests/Convert.hs @@ -0,0 +1,307 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} + +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-} + +{- | Test generation of 'Convert' instances: + +> constraints = { +> ("Index", "Index") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> ("Index", "Unsigned") : (False, "SNat @{n} `compareSNat` SNat @(2 ^ {m})"), +> ("Index", "Signed") : (True, "SNat @(CLog 2 {n} + 1) `compareSNat` SNat @{m}"), +> ("Index", "BitVector") : (False, "SNat @{n} `compareSNat` SNat @(2 ^ {m})"), +> ("Unsigned", "Index") : (False, "SNat @(2^{n}) `compareSNat` SNat @{m}"), +> ("Unsigned", "Unsigned") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> ("Unsigned", "Signed") : (True, "SNat @({n} + 1) `compareSNat` SNat @{m}"), +> ("Unsigned", "BitVector") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> ("Signed", "Signed") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> ("BitVector", "Index") : (False, "SNat @(2^{n}) `compareSNat` SNat @{m}"), +> ("BitVector", "Unsigned") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> ("BitVector", "Signed") : (True, "SNat @({n} + 1) `compareSNat` SNat @{m}"), +> ("BitVector", "BitVector") : (False, "SNat @{n} `compareSNat` SNat @{m}"), +> } +> +> 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" +> if (a, b) not in constraints: +> continue +> print(f"""case_convert{a}{b} :: Assertion +> case_convert{a}{b} = +> forM_ [0 .. {ia_max}] $ \\n -> +> forM_ [0 .. {ib_max}] $ \\m -> +> withSomeSNat n $ \\(SNat :: SNat n) -> +> withSomeSNat m $ \\(SNat :: SNat m) -> +> case {constraints[(a, b)][1].format(n=n, m=m)} of +> SNatLE -> do +> assertBool (show (n, m)) (convertXException (Proxy @({a} {n})) (Proxy @({b} {m}))) +> forM_ [minBound .. maxBound] $ \\(i :: {a} {n}) -> do +> assertBool (show (n, m, i)) (convertLaw1 (Proxy @({b} {m})) i) +> assertBool (show (n, m, i)) (convertLaw2 (Proxy @({b} {m})) i) +> _ -> do +> assertBool (show (n, m)) (convertLaw3 (Proxy @({a} {n})) (Proxy @({b} {m}))) +> """) +-} +module Clash.Tests.Convert where + +import Clash.Class.Convert (Convert (convert), MaybeConvert (maybeConvert)) +import Control.Monad (forM_) +import Data.Data (Proxy (..)) +import Data.Either (isLeft) +import Data.Maybe (isNothing) +import GHC.TypeNats (someNatVal) +import Test.Tasty (TestTree, defaultMain) +import Test.Tasty.HUnit (Assertion, assertBool, testCase) +import Test.Tasty.TH (testGroupGenerator) + +import qualified Data.List as L + +#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 + +convertLaw1 :: forall a b. (Convert a b, MaybeConvert b a, Eq a) => Proxy b -> a -> Bool +convertLaw1 _ x = Just x == maybeConvert (convert @a @b x) + +convertLaw2 :: forall a b. (Convert a b, Eq a, Integral b, Integral a) => Proxy b -> a -> Bool +convertLaw2 _ x = toInteger x == toInteger (convert @a @b x) + +{- | Tightness law: this law is tested for if there is _no_ instance of +'Convert'. If this is the case, 'MaybeConvert' should at least return a 'Nothing' +once when converting the domain of @a@ to @b@. If all conversions are possible, +the constraints of the instances should be relaxed. If the domain of @a@ is +empty, this law is considered satisfied too. +-} +convertLaw3 :: forall a b. (MaybeConvert a b, Bounded a, Enum a) => Proxy a -> Proxy b -> Bool +convertLaw3 _ _ = L.any isNothing results || not (L.null results) + where + results = L.map (maybeConvert @a @b) [minBound ..] + +-- | Checks whether an @XException@ in, means an @XException@ out +convertXException :: forall a b. (Convert a b) => Proxy a -> Proxy b -> Bool +convertXException _ _ = isLeft $ isX $ convert @a @b (errorX "" :: a) + +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) + +indexMax :: Natural +indexMax = 128 + +otherMax :: Natural +otherMax = 8 + +case_convertIndexIndex :: Assertion +case_convertIndexIndex = + forM_ [0 .. indexMax] $ \n -> + forM_ [0 .. indexMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(n + 1) `compareSNat` SNat @(m + 1) of + SNatLE -> 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)) (convertLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Index (m + 1))) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(Index (m + 1)))) + +case_convertIndexUnsigned :: Assertion +case_convertIndexUnsigned = + forM_ [0 .. indexMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(n + 1) `compareSNat` SNat @(2 ^ m) of + SNatLE -> 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)) (convertLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Unsigned m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(Unsigned m))) + +case_convertIndexSigned :: Assertion +case_convertIndexSigned = + forM_ [0 .. indexMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(CLog 2 (n + 1) + 1) `compareSNat` SNat @m of + SNatLE -> 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)) (convertLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Signed m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(Signed m))) + +case_convertIndexBitVector :: Assertion +case_convertIndexBitVector = + forM_ [0 .. indexMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(n + 1) `compareSNat` SNat @(2 ^ m) of + SNatLE -> 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)) (convertLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(BitVector m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(BitVector m))) + +case_convertUnsignedIndex :: Assertion +case_convertUnsignedIndex = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. indexMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(2^n) `compareSNat` SNat @(m + 1) of + SNatLE -> 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)) (convertLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Index (m + 1))) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Unsigned n)) (Proxy @(Index (m + 1)))) + +case_convertUnsignedUnsigned :: Assertion +case_convertUnsignedUnsigned = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @n `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(Unsigned m))) + forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Unsigned m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Unsigned n)) (Proxy @(Unsigned m))) + +case_convertUnsignedSigned :: Assertion +case_convertUnsignedSigned = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(n + 1) `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(Signed m))) + forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Signed m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Unsigned n)) (Proxy @(Signed m))) + +case_convertUnsignedBitVector :: Assertion +case_convertUnsignedBitVector = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @n `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(Unsigned n)) (Proxy @(BitVector m))) + forM_ [minBound .. maxBound] $ \(i :: Unsigned n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(BitVector m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Unsigned n)) (Proxy @(BitVector m))) + +case_convertSignedSigned :: Assertion +case_convertSignedSigned = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @n `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(Signed n)) (Proxy @(Signed m))) + forM_ [minBound .. maxBound] $ \(i :: Signed n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Signed m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(Signed n)) (Proxy @(Signed m))) + +case_convertBitVectorIndex :: Assertion +case_convertBitVectorIndex = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. indexMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(2^n) `compareSNat` SNat @(m + 1) of + SNatLE -> 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)) (convertLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Index (m + 1))) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(BitVector n)) (Proxy @(Index (m + 1)))) + +case_convertBitVectorUnsigned :: Assertion +case_convertBitVectorUnsigned = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @n `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(Unsigned m))) + forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Unsigned m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(BitVector n)) (Proxy @(Unsigned m))) + +case_convertBitVectorSigned :: Assertion +case_convertBitVectorSigned = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @(n + 1) `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(Signed m))) + forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(Signed m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(BitVector n)) (Proxy @(Signed m))) + +case_convertBitVectorBitVector :: Assertion +case_convertBitVectorBitVector = + forM_ [0 .. otherMax] $ \n -> + forM_ [0 .. otherMax] $ \m -> + withSomeSNat n $ \(SNat :: SNat n) -> + withSomeSNat m $ \(SNat :: SNat m) -> + case SNat @n `compareSNat` SNat @m of + SNatLE -> do + assertBool (show (n, m)) (convertXException (Proxy @(BitVector n)) (Proxy @(BitVector m))) + forM_ [minBound .. maxBound] $ \(i :: BitVector n) -> do + assertBool (show (n, m, i)) (convertLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertLaw2 (Proxy @(BitVector m)) i) + _ -> do + assertBool (show (n, m)) (convertLaw3 (Proxy @(BitVector n)) (Proxy @(BitVector m))) diff --git a/clash-prelude/tests/Clash/Tests/MaybeConvert.hs b/clash-prelude/tests/Clash/Tests/MaybeConvert.hs new file mode 100644 index 0000000000..f0111f54ea --- /dev/null +++ b/clash-prelude/tests/Clash/Tests/MaybeConvert.hs @@ -0,0 +1,323 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} + +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-} + +{- | Test generation of 'MaybeConvert' 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)) (convertMaybeLaw1 (Proxy @({b} {m})) i) +> assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @({b} {m})) i) +> assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @({b} {m})) i) +> assertBool (show (n, m, i)) (convertMaybeLaw4 (Proxy @({b} {m})) i) +> """) +-} +module Clash.Tests.MaybeConvert where + +import Clash.Class.Convert (MaybeConvert (maybeConvert)) +import Control.Monad (forM_) +import Data.Data (Proxy (..)) +import Data.Either (isLeft) +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 + +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) + +convertMaybeLaw1 :: + forall a b. + (Eq a, MaybeConvert a b, MaybeConvert b a) => + Proxy b -> + a -> + Bool +convertMaybeLaw1 Proxy x = + x == fromMaybe x (maybeConvert @_ @b x >>= maybeConvert) + +convertMaybeLaw2 :: + forall a b. + (MaybeConvert a b, MaybeConvert b a, Integral b, Integral a) => + Proxy b -> + a -> + Bool +convertMaybeLaw2 Proxy x = + toInteger x == fromMaybe (toInteger x) (toInteger <$> maybeConvert @_ @b x) + +convertMaybeLaw3 :: + forall a b. + (MaybeConvert a b, MaybeConvert b a, Integral b, Integral a) => + Proxy b -> + a -> + Bool +convertMaybeLaw3 Proxy x = + isJust (maybeConvert @_ @b x) `implies` isJust (maybeConvert @_ @a =<< maybeConvert @_ @b x) + where + implies :: Bool -> Bool -> Bool + implies True False = False + implies _ _ = True + +convertMaybeLaw4 :: + forall a b. + (MaybeConvert a b, MaybeConvert b a, Integral b, Integral a, Bounded b, Bounded a) => + Proxy b -> + a -> + Bool +convertMaybeLaw4 Proxy x = + isJust (maybeConvert @_ @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. (MaybeConvert a b) => Proxy a -> Proxy b -> Bool +convertXException _ _ = isLeft $ isX $ maybeConvert @a @b (errorX "" :: a) + +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)) (convertMaybeLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Index (m + 1))) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Unsigned m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(Signed m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (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)) (convertMaybeLaw1 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw2 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw3 (Proxy @(BitVector m)) i) + assertBool (show (n, m, i)) (convertMaybeLaw4 (Proxy @(BitVector m)) i) diff --git a/clash-prelude/tests/unittests.hs b/clash-prelude/tests/unittests.hs index 4c4d6cde68..1e84c04aef 100644 --- a/clash-prelude/tests/unittests.hs +++ b/clash-prelude/tests/unittests.hs @@ -9,10 +9,12 @@ import qualified Clash.Tests.BitVector import qualified Clash.Tests.BlockRam import qualified Clash.Tests.BlockRam.Blob import qualified Clash.Tests.Clocks +import qualified Clash.Tests.Convert import qualified Clash.Tests.Counter import qualified Clash.Tests.DerivingDataRepr import qualified Clash.Tests.Fixed import qualified Clash.Tests.FixedExhaustive +import qualified Clash.Tests.MaybeConvert import qualified Clash.Tests.MaybeX import qualified Clash.Tests.NFDataX import qualified Clash.Tests.NumNewtypes @@ -35,13 +37,15 @@ tests = testGroup "Unittests" , Clash.Tests.AutoReg.tests , Clash.Tests.BitPack.tests , Clash.Tests.BitVector.tests - , Clash.Tests.BlockRam.tests , Clash.Tests.BlockRam.Blob.tests + , Clash.Tests.BlockRam.tests , Clash.Tests.Clocks.tests + , Clash.Tests.Convert.tests , Clash.Tests.Counter.tests , Clash.Tests.DerivingDataRepr.tests , Clash.Tests.Fixed.tests , Clash.Tests.FixedExhaustive.tests + , Clash.Tests.MaybeConvert.tests , Clash.Tests.MaybeX.tests , Clash.Tests.NFDataX.tests , Clash.Tests.NumNewtypes.tests