finitary 0.1.0.0 → 1.0.0.0

raw patch · 5 files changed

+232/−114 lines, 5 filesdep +primitivedep +typelits-witnessesdep +vectordep ~basedep ~bitvecdep ~finite-typelitsPVP ok

version bump matches the API change (PVP)

Dependencies added: primitive, typelits-witnesses, vector

Dependency ranges changed: base, bitvec, finite-typelits, ghc-typelits-knownnat, ghc-typelits-natnormalise, hedgehog, monad-loops, mtl, template-haskell, vector-sized

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• README.md +1/−1
• finitary.cabal +17/−13
• src/Data/Finitary.hs +131/−90
• test/Main.hs +67/−10

@@ -1,5 +1,21 @@ # Revision history for finitary +## 1.0.0.0 -- 2019-09-17++* Rewritten documentation to be more clear, and state more laws.+* Added ``nextSkipping`` and ``previousSkipping`` methods to allow 'skipping+  over' some elements when enumerating in a more efficient manner.+* Added ``Eq a`` as a constraint for ``Finitary a`` instances (as without it,+  the laws don't make much sense).+* Fixed numerous typoes and unclear statements.+* Stated that ``Finitary`` must be order-preserving relative any instances with+  ``Ord`` instances; existing instances modified to follow this law.+* Added more tests.+* Fixed odd issue with some element cardinalities and lengths for sized+  ``Vector`` instances.+* Tightened bounds to be more conservative.+* Support GHC 8.8.+ ## 0.1.0.0 -- 2019-09-10  * First version. Released on an unsuspecting world.

@@ -107,7 +107,7 @@ import qualified Data.Vector.Sized as VS  data Foo = Bar | Baz (Word8, Word8) | Quux (VS.Vector 4 Bool)-  deriving (Generic, Finitary) +  deriving (Eq, Generic, Finitary)  ```  Furthermore, GHC will even calculate the cardinality for you. To assist in this,

@@ -3,7 +3,7 @@ -- PVP summary:        +-+------- breaking API changes --                     | | +----- non-breaking API additions --                     | | | +--- code changes with no API change-version:               0.1.0.0+version:               1.0.0.0 synopsis:              A better, more type-safe Enum. description:           Provides a type class witnessing that a type has                        finitely-many inhabitants, as well as its cardinality.@@ -19,7 +19,8 @@ copyright:             (C) Koz Ross 2019 category:              Data build-type:            Simple-tested-with:           GHC == 8.6.5, +tested-with:           GHC == 8.8.1,+                       GHC == 8.6.5,                         GHC == 8.4.4 extra-source-files:    CHANGELOG.md,                        README.md,@@ -32,15 +33,18 @@ library   exposed-modules:     Data.Finitary   other-modules:       Data.Finitary.TH-  build-depends:       base >= 4.11 && < 4.13,-                       finite-typelits >= 0.1.4.2 && < 1.0.0.0,+  build-depends:       base >= 4.11 && < 4.14,+                       finite-typelits >= 0.1.4.2 && < 0.2.0.0,                        coercible-utils >= 0.0.0 && < 1.0.0,-                       ghc-typelits-knownnat >= 0.7 && < 1.0,-                       ghc-typelits-natnormalise >= 0.7 && < 1.0,-                       vector-sized >= 1.2.0.1 && < 2.0.0.0,-                       mtl >= 2.2.2 && < 3.0.0,-                       template-haskell >= 2.13.0.0 && < 3.0.0.0,-                       bitvec >= 1.0.0.1 && < 2.0.0.0+                       ghc-typelits-knownnat >= 0.7 && < 0.8,+                       ghc-typelits-natnormalise >= 0.7 && < 0.8,+                       vector-sized >= 1.4.0.0 && < 1.5.0.0,+                       mtl >= 2.2.2 && < 2.3.0,+                       template-haskell >= 2.13.0.0 && < 2.16.0.0,+                       bitvec >= 1.0.0.1 && < 1.2.0.0,+                       primitive >= 0.6.4.0 && < 0.8.0.0,+                       vector >= 0.12.0.3 && < 0.13.0.0,+                       typelits-witnesses >= 0.4.0.0 && < 0.5.0.0   hs-source-dirs:      src   default-language:    Haskell2010 @@ -48,12 +52,12 @@   type:                exitcode-stdio-1.0   main-is:             Main.hs   hs-source-dirs:      test-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  ghc-options:         -O2 -threaded -rtsopts -with-rtsopts=-N   build-depends:       base,-                       hedgehog >= 1.0 && < 2.0,+                       hedgehog >= 1.0.1 && < 1.2,                        finitary,                        finite-typelits,                        vector-sized,-                       monad-loops >= 0.4.3 && < 1.0.0,+                       monad-loops >= 0.4.3 && < 0.5.0,                        bitvec   default-language:    Haskell2010

@@ -18,6 +18,7 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE ConstrainedClassMethods #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE FlexibleContexts #-}@@ -62,7 +63,7 @@ -- > import Data.Word -- > -- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16--- >    deriving (Generic, Finitary)+-- >    deriving (Eq, Generic, Finitary) -- -- This is the easiest method, and also the safest, as GHC will automatically -- determine the cardinality of @Foo@, as well as defining law-abiding methods.@@ -73,8 +74,8 @@ -- If you want a manually-defined instance, but don't wish to define every -- method, only 'fromFinite' and 'toFinite' are needed, along with -- 'Cardinality'. 'Cardinality' in particular must be defined with care, as--- otherwise, you may end up with inconstructable values or values of @Finite--- (Cardinality YourType)@ that don't correspond to anything.+-- otherwise, you may end up with inconstructable values or indexes that don't +-- correspond to anything. -- -- __By defining everything__ --@@ -85,16 +86,9 @@ Finitary(..) ) where +import Numeric.Natural (Natural) import Data.Semigroup (Max, Min, Sum, Product, Dual, Last, First, Any, All) import Data.Functor.Identity (Identity)-#if MIN_VERSION_base(4,12,0)-import Data.Ord (Down)-#else-import Data.Ord (Down(..))-#endif-import Foreign.Storable (Storable)-import Data.Maybe (fromJust)-import Control.Monad.State.Strict (MonadState(..), modify, evalState) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) import Data.Proxy (Proxy(..))@@ -105,17 +99,31 @@ import Control.Applicative (Alternative(..), Const) import Data.Kind (Type) import GHC.TypeNats-import Data.Finite (Finite, separateSum, separateProduct, combineProduct, weakenN, shiftN, strengthenN, finite)+import Data.Finite (Finite, separateSum, separateProduct, combineProduct, weakenN, shiftN)+import Data.Ord (Down(..))+import Control.Monad.Primitive (PrimMonad(..))+import Control.Monad (forM_)+import GHC.TypeLits.Compare (isLE)+import Data.Type.Equality ((:~:)(..))+import Control.Monad.ST (ST, runST)+import Foreign.Storable (Storable)  import qualified Data.Bit as B import qualified Data.Bit.ThreadSafe as BTS import qualified Data.Vector.Sized as VS+import qualified Data.Vector.Generic as VG+import qualified Data.Vector.Mutable.Sized as VMS+import qualified Data.Vector.Generic.Sized as VGS+import qualified Data.Vector.Generic.Mutable as VGM+import qualified Data.Vector.Generic.Mutable.Sized as VGMS import qualified Data.Vector.Unboxed.Sized as VUS+import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS import qualified Data.Vector.Storable.Sized as VSS+import qualified Data.Vector.Storable.Mutable.Sized as VSMS  import Data.Finitary.TH --- | Witnesses an isomorphism between @a@ and @(KnownNat n) => Finite n@.+-- | Witnesses an isomorphism between @a@ and some @(KnownNat n) => Finite n@. -- Effectively, a lawful instance of this shows that @a@ has exactly @n@ -- (non-@_|_@) inhabitants, and that we have a bijection with 'fromFinite' and -- 'toFinite' as each \'direction\'.@@ -133,19 +141,30 @@ -- --    * \[\texttt{fromFinite} \circ \texttt{toFinite} = \texttt{toFinite} \circ -- \texttt{fromFinite} = \texttt{id}\]---    * \[\forall x, y :: \texttt{Finite} \; n \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y+--    * \[\forall x, y :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y -- \rightarrow x = y\]---    * \[\forall x :: \texttt{Finite} \; n \; \exists y :: a \mid \texttt{fromFinite} \; x+--    * \[\forall x :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \exists y :: a \mid \texttt{fromFinite} \; x -- = y\] ----- Additionally, if you define any of the other methods, these laws must hold:+-- Furthermore, 'fromFinite' should be _order-preserving_. Namely, if @a@ is an+-- instance of @Ord@, we must have: -----    * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; 0 \]---    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; (n - 1)) \]+--    * \[\forall i, j :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \;+--    \texttt{fromFinite} \; i \leq \texttt{fromFinite} \; j \rightarrow i \leq j \]+--+-- Lastly, if you define any of the other methods, these laws must hold:+--+--    * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; \texttt{minBound} \]+--    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \] --    * \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x = -- (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]---    * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{prev} \; x =+--    * \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{nextSkipping} \; i =+--    \underbrace{\texttt{next} \circ \ldots \circ \texttt{next}}_{i} \]+--    * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x = -- (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]+--    * \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \;+--    \texttt{previousSkipping} \; i = \underbrace{\texttt{previous} \circ+--    \ldots \circ \texttt{previous}}_{i} \]  --    * \[ \forall x :: a \; \texttt{enumerateFrom} \; x = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..]} \] --    * \[ \forall x, y :: a \; \texttt{enumerateFromThen} \; x y = --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{, }\; y \texttt{..]} \]@@ -153,18 +172,21 @@ --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{..} \; y \texttt{]} \] --    * \[ \forall x, y, z :: a \; \texttt{enumerateFromThenTo} \; x \; y \; z = --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{,} \; y \texttt{..} \; z \texttt{]} \] ------ The default definitions follow these laws. Additionally, if you derive via--- 'Generic', these are also followed for you.------ Lastly, we /strongly/ suggest that @fromFinite@ and @toFinite@ should have--- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{n})\), where @n@ is the--- cardinality of @a@. The latter is in effect for instances generated using+-- +-- Together with the fact that @Finite n@ is well-ordered whenever @KnownNat n@+-- holds, a law-abiding @Finitary@ instance for a type @a@ defines a constructive+-- [well-order](https://en.wikipedia.org/wiki/Well-order), witnessed by+-- 'toFinite' and 'fromFinite', which agrees with the @Ord@ instance for @a@, if+-- any.+-- +-- We /strongly/ suggest that @fromFinite@ and @toFinite@ should have+-- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\). +-- The latter is the case for instances generated using -- @Generics@-based derivation, but not for \'basic\' types; thus, these -- functions for your derived types will only be as slow as their \'structure\', -- rather than their \'contents\', provided the contents are of these \'basic\' -- types. -class (KnownNat (Cardinality a)) => Finitary (a :: Type) where+class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where   -- | How many (non-@_|_@) inhabitants @a@ has, as a typelevel natural number.    type Cardinality a :: Nat   type Cardinality a = GCardinality (Rep a)@@ -186,14 +208,27 @@   -- or 'empty' if no such index exists.   previous :: (Alternative f) => a -> f a   previous = fmap fromFinite . guarded (== maxBound) . dec . toFinite+  -- | @previousSkipping i x@ \'skips back\' @i@ index values from the index of+  -- @x@, then gives the inhabitant whose index precedes the result, or 'empty'+  -- if no such index exists.+  previousSkipping :: (Alternative f) => Finite (Cardinality a) -> a -> f a+  previousSkipping i x = fmap fromFinite . guarded (> index) . subtract i $ index+    where index = toFinite x   -- | @next x@ gives the inhabitant whose index follows the index of @x@, or   -- 'empty' if no such index exists.   next :: (Alternative f) => a -> f a   next = fmap fromFinite . guarded (== minBound) . inc . toFinite+  -- | @nextSkipping i x@ \'skips forward\' @i@ index values from the index of+  -- @x@, then gives the inhabitant whose index follows the result, or 'empty'+  -- if no such index exists.+  nextSkipping :: (Alternative f) => Finite (Cardinality a) -> a -> f a+  nextSkipping i x = fmap fromFinite . guarded (< index) . (+ i) $ index+    where index = toFinite x   -- | @enumerateFrom x@ gives a list of inhabitants, starting with @x@,   -- followed by all other values whose indexes follow @x@, in index order.   enumerateFrom :: a -> [a]   enumerateFrom x = fromFinite <$> [toFinite x ..]+  -- | Like @enumerateFrom@, except in steps of @toFinite y - toFinite x@.   enumerateFromThen :: a -> a -> [a]   enumerateFromThen x y = fromFinite <$> [toFinite x, toFinite y ..]   -- | @enumerateFromTo x y@ gives a list of inhabitants, starting with @x@,@@ -201,6 +236,7 @@   -- those of @x@ and @y@. The list is in index order.   enumerateFromTo :: a -> a -> [a]   enumerateFromTo x y = fromFinite <$> [toFinite x .. toFinite y]+  -- | Like @enumerateFromTo@, except in steps of @toFinite y - toFinite x@.   enumerateFromThenTo :: a -> a -> a -> [a]   enumerateFromThenTo x y z = fromFinite <$> [toFinite x, toFinite y .. toFinite z] @@ -331,6 +367,8 @@   next = fmap succ . guarded (/= maxBound)   {-# INLINE previous #-}   previous = fmap pred . guarded (/= minBound)+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap toEnum . guarded (>= 0) . subtract (fromIntegral i) . fromEnum   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -354,6 +392,8 @@   next = fmap succ . guarded (/= maxBound)   {-# INLINE previous #-}   previous = fmap pred . guarded (/= minBound)+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Int   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -377,6 +417,8 @@   next = fmap succ . guarded (/= maxBound)   {-# INLINE previous #-}   previous = fmap pred . guarded (/= minBound)+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Int   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -400,6 +442,8 @@   next = guarded (== minBound) . inc   {-# INLINE previous #-}   previous = guarded (== maxBound) . dec+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -423,6 +467,8 @@   next = guarded (== minBound) . inc   {-# INLINE previous #-}   previous = guarded (== maxBound) . dec+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -567,6 +613,8 @@   next = guarded (== minBound) . inc   {-# INLINE previous #-}   previous = guarded (== maxBound) . dec+  {-# INLINE previousSkipping #-}+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -592,6 +640,8 @@   next = guarded (== minBound) . inc   {-# INLINE previous #-}   previous = guarded (== maxBound) . dec+  {-# INLINE previousSkipping #-}+  previousSkipping i = guarded (< i) . subtract i   {-# INLINE enumerateFrom #-}   enumerateFrom = enumFrom   {-# INLINE enumerateFromThen #-}@@ -622,33 +672,8 @@  instance (Finitary a) => Finitary (Const a b) -#if MIN_VERSION_base(4,12,0)-instance (Finitary a) => Finitary (Down a)-#else-instance (Finitary a) => Finitary (Down a) where-  type Cardinality (Down a) = Cardinality a-  {-# INLINE fromFinite #-}-  fromFinite = Down . fromFinite-  {-# INLINE toFinite #-}-  toFinite = toFinite . op Down-  {-# INLINE start #-}-  start = Down start-  {-# INLINE end #-}-  end = Down end-  {-# INLINE previous #-}-  previous = fmap Down . previous . op Down-  {-# INLINE next #-}-  next = fmap Down . next . op Down-  {-# INLINE enumerateFrom #-}-  enumerateFrom = fmap Down . enumerateFrom . op Down-  {-# INLINE enumerateFromThen #-}-  enumerateFromThen (Down x) (Down y) = fmap Down . enumerateFromThen x $ y-  {-# INLINE enumerateFromTo #-}-  enumerateFromTo (Down x) (Down y) = fmap Down . enumerateFromTo x $ y-  {-# INLINE enumerateFromThenTo #-}-  enumerateFromThenTo (Down x) (Down y) (Down z) = fmap Down . enumerateFromThenTo x y $ z-#endif-+-- | For any @newtype@-esque thing over a type with a @Finitary@ instance, we+-- can just \'inherit\' the behaviour of @a@. instance (Finitary a) => Finitary (Sum a)  instance (Finitary a) => Finitary (Product a)@@ -665,56 +690,72 @@  instance (Finitary a) => Finitary (Min a) --- | We can treat explicitly-sized @Vector@s as a fixed-length string over a--- finite alphabet, with the cardinality of the alphabet being the same as the--- cardinality of @a@. Thus, we can \'number off\' the possible @Vector@s starting--- with the one where every position is @start :: a@, and finishing with the one--- where every position is @end :: a@.-instance (Finitary a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VS.Vector n a) where+-- | Despite the @newtype@-esque nature of @Down@, due to the requirement that+-- 'fromFinite' is order-preserving, the instance for @Down a@ reverses the+-- indexing.+instance (Finitary a) => Finitary (Down a) where+  type Cardinality (Down a) = Cardinality a+  {-# INLINE fromFinite #-}+  fromFinite = Down . fromFinite . opp+    where opp = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural +          n = natVal @(Cardinality a) Proxy+  {-# INLINE toFinite #-}+  toFinite = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural . toFinite . op Down+    where n = natVal @(Cardinality a) Proxy ++-- | A fixed-length vector over a type @a@ with an instance of @Finitary@ can be+-- thought of as a fixed-length word over an alphabet of size @Cardinality a@.+-- Since there are only finitely-many of these, we can index them in lex order,+-- 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   type Cardinality (VS.Vector n a) = Cardinality a ^ n   {-# INLINE fromFinite #-}-  fromFinite = evalState (VS.replicateM (unrank typeSize))-    where typeSize = finite @(Cardinality (VS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  fromFinite i = runST (go i)+    where go :: Finite (Cardinality (VS.Vector n a)) -> ST s (VS.Vector n a)+          go ix = do v <- VMS.new+                     unroll v ix+                     VS.unsafeFreeze v   {-# INLINE toFinite #-}-  toFinite v = evalState go base-    where go = VS.foldM' (accumStep base) minBound v-          base = finite @(Cardinality (VS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  toFinite = roll -instance (Finitary a, VUS.Unbox a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VUS.Vector n a) where+instance (Finitary a, VUMS.Unbox a, KnownNat n) => Finitary (VUS.Vector n a) where   type Cardinality (VUS.Vector n a) = Cardinality a ^ n   {-# INLINE fromFinite #-}-  fromFinite = evalState (VUS.replicateM (unrank typeSize))-    where typeSize = finite @(Cardinality (VUS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  fromFinite i = runST (go i)+    where go :: Finite (Cardinality (VUS.Vector n a)) -> ST s (VUS.Vector n a)+          go ix = do v <- VUMS.new+                     unroll v ix+                     VUS.unsafeFreeze v   {-# INLINE toFinite #-}-  toFinite v = evalState go base-    where go = VUS.foldM' (accumStep base) minBound v-          base = finite @(Cardinality (VUS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  toFinite = roll -instance (Finitary a, Storable a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VSS.Vector n a) where+instance (Finitary a, Storable a, KnownNat n) => Finitary (VSS.Vector n a) where   type Cardinality (VSS.Vector n a) = Cardinality a ^ n   {-# INLINE fromFinite #-}-  fromFinite = evalState (VSS.replicateM (unrank typeSize))-    where typeSize = finite @(Cardinality (VSS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  fromFinite i = runST (go i)+    where go :: Finite (Cardinality (VSS.Vector n a)) -> ST s (VSS.Vector n a)+          go ix = do v <- VSMS.new+                     unroll v ix+                     VSS.unsafeFreeze v   {-# INLINE toFinite #-}-  toFinite v = evalState go base-    where go = VSS.foldM' (accumStep base) minBound v-          base = finite @(Cardinality (VSS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy+  toFinite = roll  -- Helpers- -{-# INLINE unrank #-}-unrank :: (MonadState (Finite n) m, Finitary a, KnownNat n, (Cardinality a) <= n) => Finite n -> m a-unrank typeSize = do remaining <- get-                     let (d, r) = remaining `divMod` typeSize-                     put d-                     return (fromFinite . fromJust . strengthenN $ r) -{-# INLINE accumStep #-}-accumStep :: (MonadState (Finite n) m, Finitary a, KnownNat n, (Cardinality a) <= n) => Finite n -> Finite n -> a -> m (Finite n)-accumStep base total e = do let e' = weakenN . toFinite $ e-                            ex <- get-                            modify (* base)-                            return (total + (e' * ex))+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+                                            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 v = case isLE (Proxy @1) (Proxy @n) of+          Nothing -> 0+          Just Refl -> let (h, t) = (VGS.head v, VGS.tail v) in+                          combineProduct (roll t, toFinite h)   {-# INLINE inc #-} inc :: (Num a) => a -> a

@@ -1,3 +1,20 @@+{-+ - Copyright (C) 2019  Koz Ross <koz.ross@retro-freedom.nz>+ -+ - This program is free software: you can redistribute it and/or modify+ - it under the terms of the GNU General Public License as published by+ - the Free Software Foundation, either version 3 of the License, or+ - (at your option) any later version.+ -+ - This program is distributed in the hope that it will be useful,+ - but WITHOUT ANY WARRANTY; without even the implied warranty of+ - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+ - GNU General Public License for more details.+ -+ - You should have received a copy of the GNU General Public License+ - along with this program.  If not, see <http://www.gnu.org/licenses/>.+ -}+ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeInType #-}@@ -12,6 +29,7 @@  module Main where +import Data.Ord (Down) import Data.Maybe (isNothing) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64)@@ -37,16 +55,26 @@  -- A representation of types data SomeFinitaryRep where-  SomeFinitaryRep :: forall (a :: Type) . (Finitary a, Show a, Eq a, Typeable a, 1 <= (Cardinality a)) => Proxy a -> SomeFinitaryRep+  SomeFinitaryRep :: forall (a :: Type) . (Finitary a, Ord a, Show a, Typeable a, 1 <= (Cardinality a)) => Proxy a -> SomeFinitaryRep  -- A representation of test functions data SomeTestFunction where-  SomeTestFunction :: (forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property) -> SomeTestFunction+  SomeTestFunction :: (forall (a :: Type) . (Finitary a, Ord a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property) -> SomeTestFunction  -- Some weird generic data Foo = Bar | Baz (VS.Vector 4 Bool) | Quux Word8-  deriving (Eq, Show, Typeable, Generic, Finitary)+  deriving (Eq, Show, Typeable, Generic, Finitary, Ord) +-- Something I will need for further tests+iterateMN :: forall (m :: Type -> Type) (a :: Type) (b :: Type) . (Eq a, Bounded a, Enum a, Monad m) => a -> (b -> m b) -> b -> m b+iterateMN i f x = if i == minBound+                  then f x+                  else iterateMN (pred i) f x >>= f++-- How much testing do I want to do for random inputs?+testLimit :: forall (a :: Type) (b :: Type) . (Finitary a, Num b) => b+testLimit = fromIntegral . (* 2) . min 32767 . natVal $ Proxy @(Cardinality a) + -- Generators choose :: forall (a :: Type) m . (MonadGen m, Finitary a) => m a choose = fromFinite <$> chooseFinite@@ -75,6 +103,7 @@   SomeFinitaryRep @Int64 Proxy,   SomeFinitaryRep @Int Proxy,   SomeFinitaryRep @Word Proxy,+  SomeFinitaryRep @(Down Int) Proxy,   SomeFinitaryRep @(Maybe Word8) Proxy,   SomeFinitaryRep @(Either Word8 Int8) Proxy,   SomeFinitaryRep @(Word8, Int8) Proxy,@@ -89,12 +118,16 @@   where go (SomeFinitaryRep p) = (fromString . show . typeRep $ p, testFunc p)  -- Properties-isBijection :: forall (a :: Type) . (Finitary a, Show a, Eq a) => Proxy a -> Property-isBijection _ = withTests testLimit (property $ do x <- forAll $ choose @a-                                                   x === (fromFinite . toFinite $ x))-  where testLimit = fromIntegral . (* 2) . min 32767 . natVal @(Cardinality a) $ Proxy+isBijection :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property+isBijection _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a+                                                        x === (fromFinite . toFinite $ x)) -startIsCorrect :: forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property+isOrderPreserving :: forall (a :: Type) . (Finitary a, Ord a) => Proxy a -> Property+isOrderPreserving _ = withTests (testLimit @a) (property $ do i <- forAll $ chooseFinite @(Cardinality a)+                                                              j <- forAll $ chooseFinite @(Cardinality a)+                                                              assert (fromFinite @a i > fromFinite @a j || i <= j)) ++startIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property startIsCorrect _ = property $ start @a === fromFinite minBound  previousStartNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property@@ -103,16 +136,40 @@ endNextNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property endNextNothing _ = property $ assert (isNothing . next $ end @a) -endIsCorrect :: forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property+endIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property endIsCorrect _ = property $ end @a === fromFinite maxBound +skipZeroIsPrevious :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property+skipZeroIsPrevious _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a+                                                               previous @a @Maybe x === previousSkipping 0 x)++skipZeroIsNext :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property+skipZeroIsNext _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a+                                                           next @a @Maybe x === nextSkipping 0 x)++skipNPreviousAgrees :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property+skipNPreviousAgrees _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a+                                                                i <- forAll $ choose @(Finite (Cardinality a))+                                                                iterateMN @Maybe i previous x === previousSkipping i x)++skipNNextAgrees :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property+skipNNextAgrees _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a+                                                            i <- forAll $ choose @(Finite (Cardinality a))+                                                            iterateMN @Maybe i next x === nextSkipping i x)++-- All the tests I want to use allTests :: [(SomeTestFunction, GroupName)] allTests = [   (SomeTestFunction isBijection, "bijectivity"),+  (SomeTestFunction isOrderPreserving, "order preservation"),   (SomeTestFunction startIsCorrect, "start"),   (SomeTestFunction endIsCorrect, "end"),   (SomeTestFunction previousStartNothing, "previous + start"),-  (SomeTestFunction endNextNothing, "next + end")+  (SomeTestFunction endNextNothing, "next + end"),+  (SomeTestFunction skipZeroIsPrevious, "previousSkipping 0"),+  (SomeTestFunction skipZeroIsNext, "nextSkipping 0"),+  (SomeTestFunction skipNPreviousAgrees, "previousSkipping n"),+  (SomeTestFunction skipNNextAgrees, "nextSkipping n")   ]  main :: IO Bool