finitary 2.1.3.0 → 2.2.1.0
raw patch · 5 files changed
Files
- CHANGELOG.md +27/−0
- README.md +0/−7
- finitary.cabal +29/−17
- src/Data/Finitary.hs +199/−36
- test/Main.hs +97/−46
CHANGELOG.md view
@@ -1,5 +1,32 @@ # Revision history for finitary +## 2.2.1.0 -- 2026-08-06 + +* Adds the `typechecker-plugins` manual flag. + Disable this flag to compile the library without using typechecker plugins. + This does not change the API of the library, but it does entail passing + more `KnownNat` dictionaries around at runtime. + +## 2.2.0.1 -- 2026-04-18 + +* Relax upper bounds: + + - `ghc-typelits-knownnat`: `< 0.8 ==> < 0.9` + - `ghc-typelits-natnormalise`: `< 0.8 ==> < 0.10` + +* Update the testsuite to account for changes in `hspec-hedgehog`. + +## 2.2.0.0 -- 2024-08-07 + +* Fix behaviour of `previous` and `next`, which incorrectly handled endpoints. + Thanks to `blmage` for their contribution. + +* Relax upper bounds: + + - `primitive`: `< 0.8 ==> < 0.10` + - `vector`: `< 0.13 ==> < 0.14` + - `vector-sized`: `< 1.6 ==> < 1.7` + ## 2.1.3.0 -- 2024-05-09 * Add support for `finite-typelits >= 2.0.0`.
README.md view
@@ -133,13 +133,6 @@ If there's something else interesting you think can be done with this, let us know: it might make it onto this list, and into code. -## What will this work on? - -Currently, we support GHC versions ranging from 8.6 to 9.0. - -The library has been tested on x86_64, GNU/Linux and Windows. -If you have results on other platforms or architectures, please let us know too! - ## License This library is under the GNU General Public License, version 3 or later (SPDX
finitary.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: finitary -version: 2.1.3.0 +version: 2.2.1.0 synopsis: A better, more type-safe Enum. description: Provides a type class witnessing that a type has @@ -9,8 +9,8 @@ Generics, together with a range of instances for existing types. -homepage: https://notabug.org/sheaf/finitary -bug-reports: https://notabug.org/sheaf/finitary/issues +homepage: https://codeberg.org/sheaf/finitary +bug-reports: https://codeberg.org/sheaf/finitary/issues license: GPL-3.0-or-later license-file: LICENSE.md author: Koz Ross @@ -18,7 +18,6 @@ copyright: (C) Koz Ross 2019-2020 category: Data build-type: Simple -tested-with: GHC ==8.6.5 || ==8.8.3 || ==8.10.1 || == 9.0.1 extra-source-files: CHANGELOG.md README.md @@ -34,9 +33,17 @@ default: True manual: True +flag typechecker-plugins + description: + Use typechecker plugins in the library. + With typechecker plugins disabled, some workarounds are used that may + cause additional 'KnownNat' dictionaries to be passed at runtime. + default: True + manual: True + source-repository head type: git - location: git://notabug.org/sheaf/finitary.git + location: https://codeberg.org/sheaf/finitary.git library exposed-modules: Data.Finitary @@ -45,14 +52,19 @@ , base >= 4.12 && < 5 , finite-typelits - >= 0.1.4.2 && < 0.3 - , ghc-typelits-knownnat - ^>= 0.7.2 - , ghc-typelits-natnormalise - ^>= 0.7.2 + >= 0.1.4.2 && < 0.3 , template-haskell - >= 2.14.0.0 && < 3.0.0.0 + >= 2.14.0.0 && < 3 + if flag(typechecker-plugins) + cpp-options: + -DTCPLUGINS + build-depends: + , ghc-typelits-knownnat + >= 0.7.2 && < 0.9 + , ghc-typelits-natnormalise + >= 0.7.2 && < 0.10 + if flag(bitvec) cpp-options: -DBITVEC @@ -64,13 +76,13 @@ -DVECTOR build-depends: , primitive - ^>= 0.7.0.1 + >= 0.7.0.1 && < 0.10 , vector - ^>= 0.12.1.2 + >= 0.12.1.2 && < 0.14 , vector-sized - >= 1.4.1.0 && < 1.6 + >= 1.4.1.0 && < 1.7 , typelits-witnesses - ^>= 0.4.0.1 + >= 0.4.0.1 && < 0.5 hs-source-dirs: src ghc-options: @@ -91,11 +103,11 @@ , ghc-typelits-knownnat , ghc-typelits-natnormalise , hedgehog - >= 1.0.2 && < 1.3 + >= 1.0.2 && < 1.8 , hspec >= 2.7.1 && < 3.0 , hspec-hedgehog - >= 0.0.1.2 && < 0.2 + >= 0.0.1.2 && < 0.4 , primitive , template-haskell , typelits-witnesses
src/Data/Finitary.hs view
@@ -1,11 +1,13 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstrainedClassMethods #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MagicHash #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} @@ -15,9 +17,16 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE NoStarIsType #-} {-# LANGUAGE PatternSynonyms #-} + +#ifdef TCPLUGINS {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +#endif +#if __GLASGOW_HASKELL__ >= 914 +{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-} +#endif + {- - Copyright (C) 2019-2020 Koz Ross <koz.ross@retro-freedom.nz> - @@ -105,6 +114,9 @@ import Data.Ord (Down (..)) import Data.Proxy (Proxy (..)) import Data.Semigroup (All, Any, Dual, First, Last, Max, Min, Product, Sum) +#if !defined(TCPLUGINS) || defined(VECTOR) +import Data.Type.Equality ((:~:) (..)) +#endif import Data.Void (Void) import Data.Word (Word16, Word32, Word64, Word8) import GHC.Exts (proxy#) @@ -121,9 +133,13 @@ to, ) import GHC.TypeNats +#ifndef TCPLUGINS +import Unsafe.Coerce (unsafeCoerce) +#endif -- finitary import Data.Finitary.TH + ( charCardinality, cardinalityOf, adjustmentOf ) -- finite-typelits import Data.Finite @@ -150,7 +166,6 @@ import Control.Monad (forM_) import Control.Monad.Primitive (PrimMonad (..)) import Control.Monad.ST (ST, runST) -import Data.Type.Equality ((:~:) (..)) import Foreign.Storable (Storable) -- finite-typelits @@ -257,12 +272,12 @@ -- | @previous x@ gives 'Just' the inhabitant whose index precedes the index of @x@, -- or 'Nothing' if no such index exists. previous :: a -> Maybe a - previous = fmap fromFinite . guarded (/= maxBound) . dec . toFinite + previous = fmap (fromFinite . dec) . guarded (/= minBound) . toFinite -- | @next x@ gives 'Just' the inhabitant whose index follows the index of @x@, or -- 'Nothing' if no such index exists. next :: a -> Maybe a - next = fmap fromFinite . guarded (/= minBound) . inc . toFinite + next = fmap (fromFinite . inc) . guarded (/= maxBound) . toFinite class (KnownNat (GCardinality a)) => GFinitary (a :: Type -> Type) where type GCardinality a :: Nat @@ -290,15 +305,35 @@ {-# INLINE gToFinite #-} gToFinite = toFinite . unK1 -instance (GFinitary a, GFinitary b) => GFinitary (a :+: b) where +instance + ( GFinitary a + , GFinitary b +#ifndef TCPLUGINS + , KnownNat (GCardinality a + GCardinality b) +#endif + ) => GFinitary (a :+: b) where type GCardinality (a :+: b) = GCardinality a + GCardinality b {-# INLINE gFromFinite #-} gFromFinite = either (L1 . gFromFinite) (R1 . gFromFinite) . separateSum {-# INLINABLE gToFinite #-} - gToFinite (L1 x) = weakenN . gToFinite $ x - gToFinite (R1 x) = shiftN . gToFinite $ x + gToFinite (L1 x) = +#ifndef TCPLUGINS + claimLE @( GCardinality a ) @( GCardinality a + GCardinality b ) $ +#endif + weakenN . gToFinite $ x + gToFinite (R1 x) = +#ifndef TCPLUGINS + claimLE @( GCardinality b ) @( GCardinality a + GCardinality b ) $ +#endif + shiftN . gToFinite $ x -instance (GFinitary a, GFinitary b) => GFinitary (a :*: b) where +instance + ( GFinitary a + , GFinitary b +#ifndef TCPLUGINS + , KnownNat (GCardinality a * GCardinality b) +#endif + ) => GFinitary (a :*: b) where type GCardinality (a :*: b) = GCardinality a * GCardinality b {-# INLINABLE gFromFinite #-} gFromFinite i = @@ -420,9 +455,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) instance Finitary Word64 where type Cardinality Word64 = $(cardinalityOf @Word64) @@ -435,9 +470,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) instance Finitary Int8 where type Cardinality Int8 = $(cardinalityOf @Int8) @@ -480,9 +515,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) instance Finitary Int64 where type Cardinality Int64 = $(cardinalityOf @Int64) @@ -495,9 +530,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) -- Variable-width instances @@ -514,9 +549,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) -- | 'Word' has a finite number of inhabitants, varying by platform. This -- instance will determine this when the library is built. @@ -531,9 +566,9 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) -- | Since any type is isomorphic to itself, it follows that a \'valid\' @Finite -- n@ (meaning that @n@ is a 'KnownNat') has finite cardinality. @@ -548,28 +583,66 @@ {-# INLINE end #-} end = maxBound {-# INLINE next #-} - next = guarded (== minBound) . inc + next = fmap inc . guarded (/= maxBound) {-# INLINE previous #-} - previous = guarded (== maxBound) . dec + previous = fmap dec . guarded (/= minBound) -- | @Maybe a@ introduces one additional inhabitant (namely, 'Nothing') to @a@. -instance (Finitary a) => Finitary (Maybe a) +instance ( Finitary a +#ifndef TCPLUGINS + , KnownNat (1 + Cardinality a) +#endif + ) => Finitary (Maybe a) -- | The sum of two finite types will also be finite, with a cardinality equal -- to the sum of their cardinalities. -instance (Finitary a, Finitary b) => Finitary (Either a b) +instance ( Finitary a, Finitary b +#ifndef TCPLUGINS + , KnownNat (Cardinality a + Cardinality b) +#endif + ) => Finitary (Either a b) -- | The product of two finite types will also be finite, with a cardinality -- equal to the product of their cardinalities. -instance (Finitary a, Finitary b) => Finitary (a, b) +instance ( Finitary a, Finitary b +#ifndef TCPLUGINS + , KnownNat (Cardinality a * Cardinality b) +#endif + ) => Finitary (a, b) -instance (Finitary a, Finitary b, Finitary c) => Finitary (a, b, c) +instance ( Finitary a, Finitary b, Finitary c +#ifndef TCPLUGINS + , KnownNat (Cardinality a * (Cardinality b * Cardinality c)) + , KnownNat (Cardinality b * Cardinality c) +#endif + ) => Finitary (a, b, c) -instance (Finitary a, Finitary b, Finitary c, Finitary d) => Finitary (a, b, c, d) +instance ( Finitary a, Finitary b, Finitary c, Finitary d +#ifndef TCPLUGINS + , KnownNat ((Cardinality a * Cardinality b) * (Cardinality c * Cardinality d)) + , KnownNat (Cardinality a * Cardinality b) + , KnownNat (Cardinality c * Cardinality d) +#endif + ) => Finitary (a, b, c, d) -instance (Finitary a, Finitary b, Finitary c, Finitary d, Finitary e) => Finitary (a, b, c, d, e) +instance ( Finitary a, Finitary b, Finitary c, Finitary d, Finitary e +#ifndef TCPLUGINS + , KnownNat ((Cardinality a * Cardinality b) * (Cardinality c * (Cardinality d * Cardinality e))) + , KnownNat (Cardinality a * Cardinality b) + , KnownNat (Cardinality c * (Cardinality d * Cardinality e)) + , KnownNat (Cardinality d * Cardinality e) +#endif + ) => Finitary (a, b, c, d, e) -instance (Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f) => Finitary (a, b, c, d, e, f) +instance ( Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f +#ifndef TCPLUGINS + , KnownNat ((Cardinality a * (Cardinality b * Cardinality c)) * (Cardinality d * (Cardinality e * Cardinality f))) + , KnownNat (Cardinality a * (Cardinality b * Cardinality c)) + , KnownNat (Cardinality b * Cardinality c) + , KnownNat (Cardinality d * (Cardinality e * Cardinality f)) + , KnownNat (Cardinality e * Cardinality f) +#endif + ) => Finitary (a, b, c, d, e, f) instance (Finitary a) => Finitary (Const a b) @@ -608,7 +681,11 @@ -- with the ordering determined by the @Finitary a@ instance (thus, the -- \'first\' such @Vector@ is the one where each element is @start :: a@, and -- the \'last\' is the one where each element is @end :: a@). -instance (Finitary a, KnownNat n) => Finitary (VS.Vector n a) where +instance ( Finitary a, KnownNat n +#ifndef TCPLUGINS + , KnownNat (Cardinality a ^ n) +#endif + ) => Finitary (VS.Vector n a) where type Cardinality (VS.Vector n a) = Cardinality a ^ n {-# INLINABLE fromFinite #-} fromFinite i = runST (go i) @@ -621,7 +698,11 @@ {-# INLINE toFinite #-} toFinite = roll -instance (Finitary a, VUMS.Unbox a, KnownNat n) => Finitary (VUS.Vector n a) where +instance ( Finitary a, VUMS.Unbox a, KnownNat n +#ifndef TCPLUGINS + , KnownNat (Cardinality a ^ n) +#endif + ) => Finitary (VUS.Vector n a) where type Cardinality (VUS.Vector n a) = Cardinality a ^ n {-# INLINABLE fromFinite #-} fromFinite i = runST (go i) @@ -634,7 +715,11 @@ {-# INLINE toFinite #-} toFinite = roll -instance (Finitary a, Storable a, KnownNat n) => Finitary (VSS.Vector n a) where +instance ( Finitary a, Storable a, KnownNat n +#ifndef TCPLUGINS + , KnownNat (Cardinality a ^ n) +#endif + ) => Finitary (VSS.Vector n a) where type Cardinality (VSS.Vector n a) = Cardinality a ^ n {-# INLINABLE fromFinite #-} fromFinite i = runST (go i) @@ -647,21 +732,41 @@ {-# INLINE toFinite #-} toFinite = roll -unroll :: forall a m v n. (Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a) => VGMS.MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m () +unroll + :: forall a m v n + . ( Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a ) + => VGMS.MVector v n (PrimState m) a + -> Finite (Cardinality a ^ n) + -> m () unroll v acc = forM_ @_ @_ @_ @() (isLE (Proxy @1) (Proxy @n)) - ( \Refl -> do - let (d, r) = separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) acc + ( \ _pf@Refl -> +#ifndef TCPLUGINS + withPeel @a @n _pf $ +#endif + do + let (d, r) = separateProduct @(Cardinality a ^ (n - 1)) @(Cardinality a) acc let x = fromFinite r VGMS.write v 0 x unroll (VGMS.tail v) d ) -roll :: forall a v n. (Finitary a, VG.Vector v a, KnownNat n) => VGS.Vector v n a -> Finite (Cardinality a ^ n) +roll + :: forall a v n + . ( Finitary a, VG.Vector v a, KnownNat n +#ifndef TCPLUGINS + , KnownNat (Cardinality a ^ n) +#endif + ) + => VGS.Vector v n a + -> Finite (Cardinality a ^ n) roll v = case isLE (Proxy @1) (Proxy @n) of Nothing -> 0 - Just Refl -> + Just _pf@Refl -> +#ifndef TCPLUGINS + withPeel @a @n _pf $ +#endif let (h, t) = (VGS.head v, VGS.tail v) in combineProduct (roll t, toFinite h) #endif @@ -728,3 +833,61 @@ {-# INLINE opp #-} opp :: forall a. (KnownNat (Cardinality a)) => Finite (Cardinality a) -> Finite (Cardinality a) opp = ( maxBound - ) + +-------------------------------------------------------------------------------- +-- Workarounds when typechecker plugins aren't available. + +#ifndef TCPLUGINS + +-- | Claim @a <= b@, when a typechecker plugin would otherwise prove it. +claimLE + :: forall (a :: Nat) (b :: Nat) r. ( a <= b => r ) -> r +claimLE f + | Refl <- unsafeCoerce Refl :: ( a <=? b ) :~: True + = f +{-# INLINE claimLE #-} + +#ifdef VECTOR +-- | Claim @a~b@, when a typechecker plugin would otherwise prove it. +claimEq + :: forall (a :: Nat) (b :: Nat) r. ( a ~ b => r ) -> r +claimEq f + | Refl <- unsafeCoerce Refl :: a :~: b + = f +{-# INLINE claimEq #-} + +-- | Claim @KnownNat n@, when a typechecker plugin would otherwise prove it. +claimKN + :: forall n r. Natural -> ( KnownNat n => r ) -> r +claimKN i f = case someNatVal i of + SomeNat ( _ :: Proxy m ) + | Refl <- ( unsafeCoerce Refl :: n :~: m ) + -> f +{-# INLINE claimKN #-} + +-- | Bring into scope the facts needed to peel the first element off a vector +-- of length @n@ with elements in @a@, given a proof that @n@ is non-zero. +withPeel + :: forall a n r + . ( Finitary a, KnownNat n ) + => ( 1 <=? n ) :~: True + -> ( ( n ~ 1 + (n - 1) + , Cardinality a ^ n ~ (Cardinality a ^ (n - 1)) * Cardinality a + , KnownNat (n - 1) + , KnownNat (Cardinality a ^ (n - 1)) + ) => r + ) + -> r +withPeel Refl f = + claimEq @n @( 1 + (n - 1) ) $ + claimEq @( Cardinality a ^ n ) @( (Cardinality a ^ (n - 1)) * Cardinality a ) $ + claimKN @(n - 1) m $ + claimKN @(Cardinality a ^ (n - 1)) (natVal' @(Cardinality a) proxy# ^ m) $ + f + where + m :: Natural + m = natVal' @n proxy# - 1 +{-# INLINE withPeel #-} + +#endif +#endif
test/Main.hs view
@@ -4,7 +4,11 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} + {- - Copyright (C) 2019 Koz Ross <koz.ross@retro-freedom.nz> - @@ -24,106 +28,146 @@ module Main where +-- base +import Data.Bit (Bit) import Data.Finitary (Finitary (..)) -import Data.Int (Int16, Int32, Int8) +import Data.Finite (Finite) +import Data.Functor.Const (Const) +import Data.Functor.Identity (Identity) +import Data.Int (Int16, Int32, Int64, Int8) import Data.Ord (Down (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (All, Any, Dual, First, Last, Max, Min, Product, Sum) +import Data.Word (Word16, Word32, Word64, Word8) +import Foreign.Storable (Storable) +import GHC.Generics (Generic) +import GHC.TypeNats (type (<=)) + +-- vector-sized import qualified Data.Vector.Sized as V import qualified Data.Vector.Storable.Sized as VS import Data.Vector.Unboxed.Sized (Unbox) import qualified Data.Vector.Unboxed.Sized as VU -import Data.Word (Word16, Word32, Word8) -import Foreign.Storable (Storable) -import GHC.Generics (Generic) + +-- hedgehog import Hedgehog ((===), Gen, PropertyT, forAll) import qualified Hedgehog.Gen as Gen import Hedgehog.Range (constantBounded) -import Test.Hspec (SpecWith, describe, hspec, it, parallel) -import Test.Hspec.Hedgehog (hedgehog, modifyMaxSize) +-- hspec +import Test.Hspec (SpecWith, describe, hspec, it, parallel, shouldBe) + +-- hspec-hedgehod +import Test.Hspec.Hedgehog (hedgehog) + +-------------------------------------------------------------------------------- + main :: IO () main = hspec . parallel $ do + describe "Previous and next values for bounds" $ do + checkBoundsPrevNext (Proxy @All) "All" + checkBoundsPrevNext (Proxy @Any) "Any" + checkBoundsPrevNext (Proxy @Int16) "Int16" + checkBoundsPrevNext (Proxy @Int32) "Int32" + checkBoundsPrevNext (Proxy @Int64) "Int64" + checkBoundsPrevNext (Proxy @Int8) "Int8" + checkBoundsPrevNext (Proxy @Word16) "Word16" + checkBoundsPrevNext (Proxy @Word32) "Word32" + checkBoundsPrevNext (Proxy @Word64) "Word64" + checkBoundsPrevNext (Proxy @Word8) "Word8" + checkBoundsPrevNext (Proxy @Bit) "Bit" + checkBoundsPrevNext (Proxy @Ordering) "Ordering" + checkBoundsPrevNext (Proxy @()) "()" + checkBoundsPrevNext (Proxy @Bool) "Bool" + checkBoundsPrevNext (Proxy @Char) "Char" + checkBoundsPrevNext (Proxy @Int) "Int" + checkBoundsPrevNext (Proxy @Word) "Word" + checkBoundsPrevNext (Proxy @(Identity Int32)) "Identity a" + checkBoundsPrevNext (Proxy @(Down Int32)) "Down a" + checkBoundsPrevNext (Proxy @(First Int32)) "First a" + checkBoundsPrevNext (Proxy @(Last Int32)) "Last a" + checkBoundsPrevNext (Proxy @(Max Int32)) "Max a" + checkBoundsPrevNext (Proxy @(Min Int32)) "Min a" + checkBoundsPrevNext (Proxy @(Dual Int32)) "Dual a" + checkBoundsPrevNext (Proxy @(Product Int32)) "Product a" + checkBoundsPrevNext (Proxy @(Sum Int32)) "Sum a" + checkBoundsPrevNext (Proxy @(Finite 10000)) "Finite n" + checkBoundsPrevNext (Proxy @(Maybe Int32)) "Maybe a" + checkBoundsPrevNext (Proxy @(Either Bool Int32)) "Either a b" + checkBoundsPrevNext (Proxy @(Proxy Int32)) "Proxy a" + checkBoundsPrevNext (Proxy @(V.Vector 10 Int32)) "V.Vector a" + checkBoundsPrevNext (Proxy @(VS.Vector 10 Int32)) "VS.Vector a" + checkBoundsPrevNext (Proxy @(VU.Vector 10 Int32)) "VU.Vector a" + checkBoundsPrevNext (Proxy @(Bool, Int32)) "(a, b)" + checkBoundsPrevNext (Proxy @(Const Int32 Bool)) "Const a b" + checkBoundsPrevNext (Proxy @(Bool, Bool, Int32)) "(a, b, c)" + checkBoundsPrevNext (Proxy @(Bool, Int8, Bool, Int32)) "(a, b, c, d)" + checkBoundsPrevNext (Proxy @(Bool, Int8, Bool, Int8, Int32)) "(a, b, c, d, e)" + checkBoundsPrevNext (Proxy @(Bool, Int8, Bool, Int8, Bool, Int32)) "(a, b, c, d, e, f)" + checkBoundsPrevNext (Proxy @Foo) "Foo" describe "Bijectivity and order preservation" $ do checkBijection "Char" Gen.unicode checkBijection "Word8" (Gen.enumBounded @_ @Word8) - modifyMaxSize (const 10000) - . checkBijection "Word16" + checkBijection "Word16" $ Gen.enumBounded @_ @Word16 - modifyMaxSize (const 10000) - . checkBijection "Word32" + checkBijection "Word32" $ Gen.enumBounded @_ @Word32 - modifyMaxSize (const 10000) - . checkBijection "Word64" + checkBijection "Word64" $ Gen.word64 constantBounded checkBijection "Int8" (Gen.enumBounded @_ @Int8) - modifyMaxSize (const 10000) - . checkBijection "Int16" + checkBijection "Int16" $ Gen.enumBounded @_ @Int16 - modifyMaxSize (const 10000) - . checkBijection "Int32" + checkBijection "Int32" $ Gen.enumBounded @_ @Int32 - modifyMaxSize (const 10000) - . checkBijection "Int64" + checkBijection "Int64" $ Gen.int64 constantBounded - modifyMaxSize (const 10000) - . checkBijection "Int" + checkBijection "Int" $ Gen.int constantBounded - modifyMaxSize (const 10000) - . checkBijection "Word" + checkBijection "Word" $ Gen.word constantBounded describe "Down" $ do checkMonotonic "Bool" Gen.bool - modifyMaxSize (const 10000) - . checkMonotonic "Int" + checkMonotonic "Int" $ (Gen.enumBounded @_ @Int) - modifyMaxSize (const 10000) - . checkMonotonic "(Either Int Bool)" + checkMonotonic "(Either Int32 Bool)" $ Gen.choice - [ Left <$> Gen.enumBounded @_ @Int, + [ Left <$> Gen.enumBounded @_ @Int32, Right <$> Gen.enumBounded @_ @Bool ] - modifyMaxSize (const 10000) - . checkMonotonic "(Int, Bool)" + checkMonotonic "(Int32, Bool)" $ ( (,) - <$> Gen.enumBounded @_ @Int + <$> Gen.enumBounded @_ @Int32 <*> Gen.enumBounded @_ @Bool ) - modifyMaxSize (const 10000) - . checkMonotonic "of a user-defined type" + checkMonotonic "of a user-defined type" $ genFoo describe "Fixed-length vectors" $ do - modifyMaxSize (const 10000) - . checkStorable "Int8" + checkStorable "Int8" . genStorable $ Gen.enumBounded @_ @Int8 - modifyMaxSize (const 10000) - . checkUnboxed "Int8" + checkUnboxed "Int8" . genUnboxed $ Gen.enumBounded @_ @Int8 - modifyMaxSize (const 10000) - . checkRegular "Int8" + checkRegular "Int8" . genRegular $ Gen.enumBounded @_ @Int8 - modifyMaxSize (const 10000) - . checkUnboxed "(Int8, Int8)" + checkUnboxed "(Int8, Int8)" . genUnboxed $ ( (,) <$> Gen.enumBounded @_ @Int8 <*> Gen.enumBounded @_ @Int8 ) - modifyMaxSize (const 10000) - . checkRegular "(Int8, Int8)" + checkRegular "(Int8, Int8)" . genRegular $ ( (,) <$> Gen.enumBounded @_ @Int8 <*> Gen.enumBounded @_ @Int8 ) - modifyMaxSize (const 10000) - . checkRegular "Either Int8 Bool" + checkRegular "Either Int8 Bool" . genRegular . Gen.choice $ [ Left <$> Gen.enumBounded @_ @Int8, Right <$> Gen.bool ] - modifyMaxSize (const 10000) - . checkRegular "a user defined type" + checkRegular "a user defined type" . genRegular $ genFoo @@ -228,3 +272,10 @@ LT -> compare dx dy === GT EQ -> compare dx dy === EQ GT -> compare dx dy === LT + +checkBoundsPrevNext :: forall a. (1 <= Cardinality a, Show a, Finitary a) => Proxy a -> String -> SpecWith () +checkBoundsPrevNext _ name = do + it ("(start :: " <> name <> ") should have no predecessor") $ + previous (start @a) `shouldBe` Nothing + it ("(end :: " <> name <> ") should have no successor") $ + next (end @a) `shouldBe` Nothing