diff --git a/clash-prelude/src/Clash/Class/Resize.hs b/clash-prelude/src/Clash/Class/Resize.hs index e19d778e5b..7a407c2122 100644 --- a/clash-prelude/src/Clash/Class/Resize.hs +++ b/clash-prelude/src/Clash/Class/Resize.hs @@ -6,6 +6,7 @@ License : BSD2 (see the file LICENSE) Maintainer : QBayLogic B.V. -} +{-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE NoGeneralizedNewtypeDeriving #-} {-# LANGUAGE Safe #-} @@ -20,12 +21,14 @@ module Clash.Class.Resize , checkedResize , checkedFromIntegral , checkedTruncateB + , maybeResize + , maybeTruncateB ) where import Data.Kind (Type) import Data.Proxy (Proxy(Proxy)) import GHC.Stack (HasCallStack) -import GHC.TypeLits (Nat, KnownNat, type (+)) +import GHC.TypeLits (Nat, KnownNat, type (+), OrderingI(EQI, GTI), cmpNat) import Clash.Sized.Internal (formatRange) @@ -117,3 +120,30 @@ checkedTruncateB :: f (a + b) -> f a checkedTruncateB v = checkIntegral (Proxy @(f a)) v `seq` truncateB v + +-- | Like 'resize', but returns 'Nothing' if /f a/ is out of bounds for /f b/. +maybeResize :: + forall a b f. + ( Resize f + , KnownNat a, Integral (f a) + , KnownNat b, Integral (f b), Bounded (f b) ) => + f a -> Maybe (f b) +maybeResize v = + case Proxy @a `cmpNat` Proxy @b of + GTI | v > resize (maxBound @(f b)) -> Nothing + GTI | v < resize (minBound @(f b)) -> Nothing + EQI -> Just v -- optional, for performance reasons? + _ -> Just (resize v) + +-- | Like 'truncateB', but returns 'Nothing' if /f (a + b)/ is out of bounds for +-- /f a/. +maybeTruncateB :: + forall a b f. + ( Resize f + , KnownNat b, Integral (f (a + b)) + , KnownNat a, Integral (f a), Bounded (f a) ) => + f (a + b) -> Maybe (f a) +maybeTruncateB v + | v > resize (maxBound @(f a)) = Nothing + | v < resize (minBound @(f a)) = Nothing + | otherwise = Just (truncateB v) diff --git a/clash-prelude/tests/Clash/Tests/Resize.hs b/clash-prelude/tests/Clash/Tests/Resize.hs index 3d324695bc..14d820a7ca 100644 --- a/clash-prelude/tests/Clash/Tests/Resize.hs +++ b/clash-prelude/tests/Clash/Tests/Resize.hs @@ -1,18 +1,37 @@ +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} -module Clash.Tests.Resize (tests) where +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-} +module Clash.Tests.Resize (tests, main) where + +import Clash.XException (XException) import Control.DeepSeq (NFData) import Control.Exception (SomeException, try, evaluate) -import Clash.XException (XException) import Data.Either (isLeft) import Data.Proxy (Proxy(Proxy)) -import GHC.TypeNats (KnownNat, type (<=)) -import Test.Tasty (TestTree, testGroup) -import Test.Tasty.QuickCheck +import GHC.TypeNats (KnownNat, SomeNat(..), type (<=), type (+), Nat, Natural, someNatVal) +import Hedgehog ((===)) +import Test.Tasty (TestTree, testGroup, defaultMain, adjustOption) +import Test.Tasty.Hedgehog (HedgehogTestLimit(..), testPropertyNamed) +import Test.Tasty.QuickCheck (testProperty, discard, ioProperty, counterexample) + +import qualified Test.Tasty.QuickCheck as Q +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range import qualified Clash.Class.Resize as Resize -import Clash.Sized.Index +import Clash.Promoted.Nat (SNat(..)) +import Clash.Prelude (Unsigned, Signed, BitVector, Index) + +withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r +withSomeSNat n f = case someNatVal n of + SomeNat (_ :: Proxy n) -> f (SNat @n) -- | Anything that's in bounds should not cause an error indexProp :: @@ -26,7 +45,7 @@ indexProp Proxy v = indexFailProp :: forall a b. ((b <= a), KnownNat a, KnownNat b) => - Proxy b -> Index a -> Property + Proxy b -> Index a -> Q.Property indexFailProp Proxy v = let checked = Resize.checkedResize @a @b v in if toInteger v > toInteger (maxBound @(Index b)) then @@ -34,8 +53,138 @@ indexFailProp Proxy v = else discard +maybeResizePropT :: + forall f a b . + ( Integral (f a) + , Bounded (f a) + , Show (f a) + , Integral (f b) + , Bounded (f b) + , Show (f b) + , Resize.Resize f + , KnownNat a + , KnownNat b + ) => + Proxy (f a) -> + Proxy (f b) -> + H.PropertyT IO () +maybeResizePropT _ _ = do + let + minFa = fromIntegral (minBound @(f a)) :: Integer + maxFa = fromIntegral (maxBound @(f a)) :: Integer + minFb = fromIntegral (minBound @(f b)) :: Integer + maxFb = fromIntegral (maxBound @(f b)) :: Integer + + H.footnote $ "minFa: " <> show minFa + H.footnote $ "maxFa: " <> show maxFa + H.footnote $ "minFb: " <> show minFb + H.footnote $ "maxFb: " <> show maxFb + + input <- H.forAll $ Gen.integral (Range.linear minFa maxFa) + let output = Resize.maybeResize @a @b @f (fromIntegral input) + if minFb <= input && input <= maxFb + then output === Just (fromIntegral input) + else output === Nothing + +maybeResizeUnsignedProp :: H.Property +maybeResizeUnsignedProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeResizePropT @Unsigned @a @b Proxy Proxy + +maybeResizeSignedProp :: H.Property +maybeResizeSignedProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeResizePropT @Signed @a @b Proxy Proxy + +maybeResizeIndexProp :: H.Property +maybeResizeIndexProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 1 100) + b <- H.forAll $ Gen.integral (Range.linear 1 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeResizePropT @Index @a @b Proxy Proxy + +maybeResizeBitVectorProp :: H.Property +maybeResizeBitVectorProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeResizePropT @BitVector @a @b Proxy Proxy + +maybeTruncatePropT :: + forall f a b . + ( Integral (f a) + , Bounded (f a) + , Show (f a) + , Integral (f (a + b)) + , Bounded (f (a + b)) + , Show (f (a + b)) + , Resize.Resize f + , KnownNat a + , KnownNat b + ) => + Proxy (f a) -> + Proxy (f (a + b)) -> + H.PropertyT IO () +maybeTruncatePropT _ _ = do + let + minFa = fromIntegral (minBound @(f a)) :: Integer + maxFa = fromIntegral (maxBound @(f a)) :: Integer + minFab = fromIntegral (minBound @(f (a + b))) :: Integer + maxFab = fromIntegral (maxBound @(f (a + b))) :: Integer + + H.footnote $ "minFa: " <> show minFa + H.footnote $ "maxFa: " <> show maxFa + H.footnote $ "minFab: " <> show minFab + H.footnote $ "maxFab: " <> show maxFab + + input <- H.forAll $ Gen.integral (Range.linear minFa maxFa) + let output = Resize.maybeTruncateB @a @b @f (fromIntegral input) + if minFab <= input && input <= maxFab + then output === Just (fromIntegral input) + else output === Nothing + +maybeTruncateUnsignedProp :: H.Property +maybeTruncateUnsignedProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeTruncatePropT @Unsigned @a @b Proxy Proxy + +maybeTruncateSignedProp :: H.Property +maybeTruncateSignedProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeTruncatePropT @Signed @a @b Proxy Proxy + +maybeTruncateIndexProp :: H.Property +maybeTruncateIndexProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 1 100) + b <- H.forAll $ Gen.integral (Range.linear 1 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeTruncatePropT @Index @a @b Proxy Proxy + +maybeTruncateBitVectorProp :: H.Property +maybeTruncateBitVectorProp = H.property $ do + a <- H.forAll $ Gen.integral (Range.linear 0 100) + b <- H.forAll $ Gen.integral (Range.linear 0 100) + withSomeSNat a $ \(SNat :: SNat a) -> do + withSomeSNat b $ \(SNat :: SNat b) -> do + maybeTruncatePropT @BitVector @a @b Proxy Proxy + -- | Succeed if evaluating leads to a non-XException Exception -expectExceptionNoX :: (Show a, NFData a) => a -> Property +expectExceptionNoX :: (Show a, NFData a) => a -> Q.Property expectExceptionNoX a0 = ioProperty $ do a1 <- try @SomeException (try @XException (evaluate a0)) pure $ @@ -49,5 +198,16 @@ tests = testGroup "Resize" [ testProperty "indexProp @17 @19" (indexProp @17 @19 Proxy) , testProperty "indexProp @19 @19" (indexProp @19 @19 Proxy) , testProperty "indexFailProp @37 @7" (indexFailProp @37 @7 Proxy) + , testPropertyNamed "maybeResizeUnsignedProp" "maybeResizeUnsignedProp" maybeResizeUnsignedProp + , testPropertyNamed "maybeResizeSignedProp" "maybeResizeSignedProp" maybeResizeSignedProp + , testPropertyNamed "maybeResizeIndexProp" "maybeResizeIndexProp" maybeResizeIndexProp + , testPropertyNamed "maybeResizeBitVectorProp" "maybeResizeBitVectorProp" maybeResizeBitVectorProp + , testPropertyNamed "maybeTruncateUnsignedProp" "maybeTruncateUnsignedProp" maybeTruncateUnsignedProp + , testPropertyNamed "maybeTruncateSignedProp" "maybeTruncateSignedProp" maybeTruncateSignedProp + , testPropertyNamed "maybeTruncateIndexProp" "maybeTruncateIndexProp" maybeTruncateIndexProp + , testPropertyNamed "maybeTruncateBitVectorProp" "maybeTruncateBitVectorProp" maybeTruncateBitVectorProp ] ] + +main :: IO () +main = defaultMain $ adjustOption (\_ -> HedgehogTestLimit (Just 1_000_000)) $ tests