Add tests for Finite laws

clash-prelude/clash-prelude.cabal

@@ -451,6 +451,7 @@ test-suite unittests
                  Clash.Tests.XException
 
                  Clash.Tests.Laws.Enum
+                 Clash.Tests.Laws.Finite
                  Clash.Tests.Laws.SaturatingNum
 
                  Hedgehog.Extra

clash-prelude/tests/Clash/Tests/Laws/Finite.hs

@@ -0,0 +1,181 @@
+module Clash.Tests.Laws.Finite (tests) where
+
+import Prelude hiding (reverse)
+
+import Control.DeepSeq (NFData)
+import Data.Functor.Compose (Compose(..))
+import Data.Functor.Const (Const(..))
+import Data.Functor.Identity (Identity(..))
+import Data.Functor.Product (Product)
+import Data.Functor.Sum (Sum)
+import Data.Int (Int8, Int16)
+import Data.Maybe (isNothing)
+import Data.Ord (Down(..))
+import Data.Proxy (Proxy(..))
+import Data.Void (Void)
+import Data.Word (Word8, Word16)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (Assertion, (@=?), testCase)
+
+import Clash.Class.Finite (Finite(..))
+import Clash.Promoted.Nat (natToInteger)
+import Clash.Sized.BitVector (BitVector, Bit)
+import Clash.Sized.Index (Index)
+import Clash.Sized.RTree (RTree)
+import Clash.Sized.Signed (Signed)
+import Clash.Sized.Unsigned (Unsigned)
+import Clash.Sized.Vector (Vec, indicesI, iterateI, reverse)
+
+indexOrderLaw ::
+  forall a.
+  (NFData a, Show a, Finite a) =>
+  Proxy a ->
+  Assertion
+indexOrderLaw Proxy =
+  index <$> elements @a @=? indicesI
+
+forwardIterateLaw ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+forwardIterateLaw Proxy =
+  iterateI (>>= after) (lowest @a) @=? Just <$> elements @a
+
+backwardIterateLaw ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+backwardIterateLaw Proxy =
+  iterateI (>>= before) (highest @a) @=? Just <$> reverse (elements @a)
+
+indexIsomorphismLaw ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+indexIsomorphismLaw Proxy =
+  ith . index <$> elements @a @=? elements @a
+
+minimumPredecessor ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+minimumPredecessor Proxy =
+  (lowest >>= before @a) @=? Nothing
+
+maximumSuccessor ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+maximumSuccessor Proxy =
+  (highest >>= after @a) @=? Nothing
+
+noUninhabitedExtremes ::
+  forall a.
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  Assertion
+noUninhabitedExtremes Proxy =
+   isNothing (lowest @a) && isNothing (highest @a)
+     @=? (natToInteger @(ElementCount a) == 0)
+
+finiteLaws ::
+  (NFData a, Show a, Eq a, Finite a) =>
+  Proxy a ->
+  [TestTree]
+finiteLaws proxy =
+  [ testCase "Index Order"             $ indexOrderLaw proxy
+  , testCase "Forward Iterate"         $ forwardIterateLaw proxy
+  , testCase "Backward Iterate"        $ backwardIterateLaw proxy
+  , testCase "Index Isomorphism"       $ indexIsomorphismLaw proxy
+  , testCase "Minimum Predecessor"     $ minimumPredecessor proxy
+  , testCase "Maximum Successor"       $ maximumSuccessor proxy
+  , testCase "No Uninhabited Extremes" $ noUninhabitedExtremes proxy
+  ]
+
+testFiniteLaws ::
+  (NFData a, Show a, Eq a, Finite a) =>
+  String ->
+  Proxy a ->
+  TestTree
+testFiniteLaws typeName =
+  testGroup typeName . finiteLaws
+
+tests :: TestTree
+tests = testGroup "Finite"
+  [ testFiniteLaws "Void" (Proxy @Void)
+  , testFiniteLaws "()" (Proxy @())
+  , testFiniteLaws "Bit" (Proxy @Bit)
+  , testFiniteLaws "Bool" (Proxy @Bool)
+  , testFiniteLaws "Ordering" (Proxy @Ordering)
+
+  , testFiniteLaws "Char" (Proxy @Char)
+  , testFiniteLaws "Int8" (Proxy @Int8)
+  , testFiniteLaws "Int16" (Proxy @Int16)
+  , testFiniteLaws "Word8" (Proxy @Word8)
+  , testFiniteLaws "Word16" (Proxy @Word16)
+
+  , testFiniteLaws "BitVector 0" (Proxy @(BitVector 0))
+  , testFiniteLaws "BitVector 1" (Proxy @(BitVector 1))
+  , testFiniteLaws "BitVector 8" (Proxy @(BitVector 8))
+
+  , testFiniteLaws "Index 0" (Proxy @(Index 0))
+  , testFiniteLaws "Index 1" (Proxy @(Index 1))
+  , testFiniteLaws "Index 128" (Proxy @(Index 128))
+
+  , testFiniteLaws "Signed 0" (Proxy @(Signed 0))
+  , testFiniteLaws "Signed 1" (Proxy @(Signed 1))
+  , testFiniteLaws "Signed 8" (Proxy @(Signed 8))
+
+  , testFiniteLaws "Unsigned 0" (Proxy @(Unsigned 0))
+  , testFiniteLaws "Unsigned 1" (Proxy @(Unsigned 1))
+  , testFiniteLaws "Unsigned 8" (Proxy @(Unsigned 8))
+
+  , testFiniteLaws "Maybe (Index 0)" (Proxy @(Maybe (Index 0)))
+  , testFiniteLaws "Maybe (Index 1)" (Proxy @(Maybe (Index 1)))
+  , testFiniteLaws "Maybe (Index 27)" (Proxy @(Maybe (Index 27)))
+
+  , testFiniteLaws "Either Void (Index 0)" (Proxy @(Either Void (Index 0)))
+  , testFiniteLaws "Either Void (Index 1)" (Proxy @(Either Void (Index 1)))
+  , testFiniteLaws "Either Void (Index 27)" (Proxy @(Either Void (Index 27)))
+  , testFiniteLaws "Either Bool (Index 0)" (Proxy @(Either Bool (Index 0)))
+  , testFiniteLaws "Either Bool (Index 1)" (Proxy @(Either Bool (Index 1)))
+  , testFiniteLaws "Either Bool (Index 27)" (Proxy @(Either Bool (Index 27)))
+
+  , testFiniteLaws "Compose Maybe Maybe Bool" (Proxy @(Compose Maybe Maybe Bool))
+  , testFiniteLaws "Const Bool [Int]" (Proxy @(Const Bool [Int]))
+  , testFiniteLaws "Down Bool" (Proxy @(Down Bool))
+  , testFiniteLaws "Identity Bool" (Proxy @(Identity Bool))
+  , testFiniteLaws "Product Maybe Maybe Bit" (Proxy @(Product Maybe Maybe Bit))
+  , testFiniteLaws "Sum Maybe Maybe Bit" (Proxy @(Sum Maybe Maybe Bit))
+
+  , testFiniteLaws "Vec 0 Void" (Proxy @(Vec 0 Void))
+  , testFiniteLaws "Vec 1 Void" (Proxy @(Vec 1 Void))
+  , testFiniteLaws "Vec 16 Void" (Proxy @(Vec 16 Void))
+  , testFiniteLaws "Vec 0 Bool" (Proxy @(Vec 0 Bool))
+  , testFiniteLaws "Vec 1 Bool" (Proxy @(Vec 1 Bool))
+  , testFiniteLaws "Vec 16 Bool" (Proxy @(Vec 16 Bool))
+
+  , testFiniteLaws "RTree 0 Void" (Proxy @(RTree 0 Void))
+  , testFiniteLaws "RTree 1 Void" (Proxy @(RTree 1 Void))
+  , testFiniteLaws "RTree 4 Void" (Proxy @(RTree 4 Void))
+  , testFiniteLaws "RTree 0 Bool" (Proxy @(RTree 0 Bool))
+  , testFiniteLaws "RTree 1 Bool" (Proxy @(RTree 1 Bool))
+  , testFiniteLaws "RTree 4 Bool" (Proxy @(RTree 4 Bool))
+
+  , testFiniteLaws "(Void, Void)" (Proxy @(Void, Void))
+  , testFiniteLaws "(Bool, Void)" (Proxy @(Bool, Void))
+  , testFiniteLaws "(Void, Bool)" (Proxy @(Void, Bool))
+  , testFiniteLaws "(Bool, Bool)" (Proxy @(Bool, Bool))
+
+  , testFiniteLaws "(Bool, Bool, Bool)" (Proxy @(Bool, Bool, Bool))
+  , testFiniteLaws "(Void, Bool, Bool)" (Proxy @(Void, Bool, Bool))
+  , testFiniteLaws "(Bool, Void, Bool)" (Proxy @(Bool, Void, Bool))
+  , testFiniteLaws "(Bool, Bool, Void)" (Proxy @(Bool, Bool, Void))
+
+  , testFiniteLaws "(Bool, Bool, Bool, Bool)" (Proxy @(Bool, Bool, Bool, Bool))
+  ]

clash-prelude/tests/unittests.hs

@@ -27,6 +27,7 @@ import qualified Clash.Tests.Vector
 import qualified Clash.Tests.XException
 
 import qualified Clash.Tests.Laws.Enum
+import qualified Clash.Tests.Laws.Finite
 import qualified Clash.Tests.Laws.SaturatingNum
 
 tests :: TestTree
@@ -56,6 +57,7 @@ tests = testGroup "Unittests"
   , Clash.Tests.XException.tests
   , testGroup "Laws"
     [ Clash.Tests.Laws.Enum.tests
+    , Clash.Tests.Laws.Finite.tests
     , Clash.Tests.Laws.SaturatingNum.tests
     ]
   ]