{-
 - 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/>.
 -}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE CPP #-}

#if MIN_VERSION_base(4,12,0)
{-# LANGUAGE NoStarIsType #-}
#endif

-- | 
-- Module:        Data.Finitary
-- Description:   A type class witnessing that a type has finite cardinality.
-- Copyright:     (C) Koz Ross, 2019
-- License:       GPL version 3.0 or later
-- Maintainer:    koz.ross@retro-freedom.nz
-- Stability:     Experimental
-- Portability:   GHC only
--
-- This package provides the 'Finitary' type class, as well as a range of useful
-- \'base\' instances for commonly-used finitary types. 
--
-- For your own types, there are three possible ways to define an instance of
-- 'Finitary':
--
-- __Via 'Generic'__
--
-- If your data type implements 'Generic' (and is finitary), you can
-- automatically derive your instance:
--
-- > {-# LANGUAGE DeriveAnyClass #-}
-- > {-# LANGUAGE DeriveGeneric #-}
-- >
-- > import GHC.Generics
-- > import Data.Word
-- >
-- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16
-- >    deriving (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.
-- It may be somewhat slower than a \'hand-rolled\' method in some cases.
--
-- __By defining only 'Cardinality', 'fromFinite' and 'toFinite'__
--
-- 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.
--
-- __By defining everything__
--
-- For maximum control, you can define all the methods. Ensure you follow all
-- the laws!
--
module Data.Finitary (
Finitary(..)
) where

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(..))
import Data.Void (Void)
import Data.Bool (bool)
import CoercibleUtils (op)
import GHC.Generics (Generic, Rep, U1(..), K1(..), V1, (:+:)(..), (:*:)(..), M1(..), from, to)
import Control.Applicative (Alternative(..), Const)
import Data.Kind (Type)
import GHC.TypeNats
import Data.Finite (Finite, separateSum, separateProduct, combineProduct, weakenN, shiftN, strengthenN, finite)

import qualified Data.Bit as B
import qualified Data.Bit.ThreadSafe as BTS
import qualified Data.Vector.Sized as VS
import qualified Data.Vector.Unboxed.Sized as VUS
import qualified Data.Vector.Storable.Sized as VSS

import Data.Finitary.TH

-- | Witnesses an isomorphism between @a@ and @(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\'.
--
-- For any type @a@ with an instance of @Finitary@, for every non-@_|_@ @x :: a@, we have
-- a unique /index/ @i :: Finite n@. We will also refer to any such @x@ as an
-- /inhabitant/ of @a@. We can convert inhabitants to indexes using @toFinite@,
-- and also convert indexes to inhabitants with @fromFinite@.
--
-- __Laws__
--
-- The main laws state that 'fromFinite' should be a bijection, with 'toFinite' as
-- its inverse, and 'Cardinality' must be a truthful representation of the
-- cardinality of the type. Thus:
--
--    * \[\texttt{fromFinite} \circ \texttt{toFinite} = \texttt{toFinite} \circ
-- \texttt{fromFinite} = \texttt{id}\]
--    * \[\forall x, y :: \texttt{Finite} \; n \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y
-- \rightarrow x = y\]
--    * \[\forall x :: \texttt{Finite} \; n \; \exists y :: a \mid \texttt{fromFinite} \; x
-- = y\]
--
-- Additionally, if you define any of the other methods, these laws must hold:
--
--    * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; 0 \]
--    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; (n - 1)) \]
--    * \[ \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 =
-- (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]
--    * \[ \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{..]} \]
--    * \[ \forall x, y :: a \; \texttt{enumerateFromTo} \; x \; y =
--    \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
-- @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
  -- | How many (non-@_|_@) inhabitants @a@ has, as a typelevel natural number. 
  type Cardinality a :: Nat
  type Cardinality a = GCardinality (Rep a)
  -- | Converts an index into its corresponding inhabitant.
  fromFinite :: Finite (Cardinality a) -> a
  default fromFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => Finite (Cardinality a) -> a
  fromFinite = to . gFromFinite
  -- | Converts an inhabitant to its corresponding index.
  toFinite :: a -> Finite (Cardinality a)
  default toFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => a -> Finite (Cardinality a)
  toFinite = gToFinite . from
  -- | The first inhabitant, by index, assuming @a@ has any inhabitants.
  start :: (1 <= Cardinality a) => a
  start = fromFinite minBound
  -- | The last inhabitant, by index, assuming @a@ has any inhabitants.
  end :: (1 <= Cardinality a) => a
  end = fromFinite maxBound
  -- | @previous x@ gives the inhabitant whose index precedes the index of @x@,
  -- or 'empty' if no such index exists.
  previous :: (Alternative f) => a -> f a
  previous = fmap fromFinite . guarded (== maxBound) . dec . toFinite
  -- | @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
  -- | @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 ..]
  enumerateFromThen :: a -> a -> [a]
  enumerateFromThen x y = fromFinite <$> [toFinite x, toFinite y ..]
  -- | @enumerateFromTo x y@ gives a list of inhabitants, starting with @x@,
  -- ending with @y@, and containing all other values whose indices lie between
  -- those of @x@ and @y@. The list is in index order.
  enumerateFromTo :: a -> a -> [a]
  enumerateFromTo x y = fromFinite <$> [toFinite x .. toFinite y]
  enumerateFromThenTo :: a -> a -> a -> [a]
  enumerateFromThenTo x y z = fromFinite <$> [toFinite x, toFinite y .. toFinite z]

class (KnownNat (GCardinality a)) => GFinitary (a :: Type -> Type) where
  type GCardinality a :: Nat
  gFromFinite :: Finite (GCardinality a) -> a x
  gToFinite :: a x -> Finite (GCardinality a) 

instance GFinitary V1 where
  type GCardinality V1 = 0
  {-# INLINE gFromFinite #-}
  gFromFinite = const undefined
  {-# INLINE gToFinite #-}
  gToFinite = const undefined 

instance GFinitary U1 where
  type GCardinality U1 = 1
  {-# INLINE gFromFinite #-}
  gFromFinite = const U1
  {-# INLINE gToFinite #-}
  gToFinite = const 0

instance (Finitary a) => GFinitary (K1 _1 a) where
  type GCardinality (K1 _1 a) = Cardinality a
  {-# INLINE gFromFinite #-}
  gFromFinite = K1 . fromFinite
  {-# INLINE gToFinite #-}
  gToFinite = toFinite . op K1

instance (GFinitary a, GFinitary b) => GFinitary (a :+: b) where
  type GCardinality (a :+: b) = GCardinality a + GCardinality b
  {-# INLINE gFromFinite #-}
  gFromFinite = either (L1 . gFromFinite) (R1 . gFromFinite) . separateSum
  {-# INLINE gToFinite #-}
  gToFinite (L1 x) = weakenN . gToFinite $ x
  gToFinite (R1 x) = shiftN . gToFinite $ x 

instance (GFinitary a, GFinitary b) => GFinitary (a :*: b) where
  type GCardinality (a :*: b) = GCardinality a * GCardinality b
  {-# INLINE gFromFinite #-}
  gFromFinite i = let (x, y) = separateProduct i in
                    gFromFinite x :*: gFromFinite y
  {-# INLINE gToFinite #-}
  gToFinite (x :*: y) = combineProduct @(GCardinality a) @(GCardinality b) (weakenN . gToFinite $ x, weakenN . gToFinite $ y)

instance (GFinitary a) => GFinitary (M1 _x _y a) where
  type GCardinality (M1 _x _y a) = GCardinality a
  {-# INLINE gFromFinite #-}
  gFromFinite = M1 . gFromFinite
  {-# INLINE gToFinite #-}
  gToFinite = gToFinite . op M1

-- * Instances
-- Basic types

instance Finitary Void

instance Finitary ()

instance Finitary (Proxy a)

instance Finitary Bool

instance Finitary Any

instance Finitary All

instance Finitary B.Bit where
  type Cardinality B.Bit = 2
  {-# INLINE fromFinite #-}
  fromFinite = B.Bit . toEnum . fromEnum
  {-# INLINE toFinite #-}
  toFinite = toEnum . fromEnum . op B.Bit
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (== minBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (== maxBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary BTS.Bit where
  type Cardinality BTS.Bit = 2
  {-# INLINE fromFinite #-}
  fromFinite = BTS.Bit . toEnum . fromEnum
  {-# INLINE toFinite #-}
  toFinite = toEnum . fromEnum . op BTS.Bit
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (== minBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (== maxBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Ordering

-- | 'Char' has one inhabitant per Unicode code point.
instance Finitary Char where
  type Cardinality Char = $(charCardinality)
  {-# INLINE fromFinite #-}
  fromFinite = toEnum . fromEnum
  {-# INLINE toFinite #-}
  toFinite = toEnum . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (/= maxBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (/= minBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Word8 where
  type Cardinality Word8 = $(cardinalityOf @Word8)
  {-# INLINE fromFinite #-}
  fromFinite = toEnum . fromEnum
  {-# INLINE toFinite #-}
  toFinite = toEnum . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (/= maxBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (/= minBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Word16 where
  type Cardinality Word16 = $(cardinalityOf @Word16)
  {-# INLINE fromFinite #-}
  fromFinite = toEnum . fromEnum
  {-# INLINE toFinite #-}
  toFinite = toEnum . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (/= maxBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (/= minBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Word32 where
  type Cardinality Word32 = $(cardinalityOf @Word32)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral
  {-# INLINE toFinite #-}
  toFinite = fromIntegral
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Word64 where
  type Cardinality Word64 = $(cardinalityOf @Word64)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral
  {-# INLINE toFinite #-}
  toFinite = fromIntegral
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Int8 where
  type Cardinality Int8 = $(cardinalityOf @Int8)
  {-# INLINE fromFinite #-}  
  fromFinite = fromIntegral . subtract 128 . fromIntegral @_ @Int16
  {-# INLINE toFinite #-}
  toFinite = fromIntegral . (+ 128) . fromIntegral @_ @Int16
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (/= maxBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (/= minBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Int16 where
  type Cardinality Int16 = $(cardinalityOf @Int16)
  {-# INLINE fromFinite #-}  
  fromFinite = fromIntegral . subtract 32768 . fromIntegral @_ @Int32
  {-# INLINE toFinite #-}
  toFinite = fromIntegral . (+ 32768) . fromIntegral @_ @Int32
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = fmap succ . guarded (/= maxBound)
  {-# INLINE previous #-}
  previous = fmap pred . guarded (/= minBound)
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Int32 where
  type Cardinality Int32 = $(cardinalityOf @Int32)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral @_ @Int32 . subtract $(adjustmentOf @Int32) . fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite = fromIntegral . (+ $(adjustmentOf @Int32)) . fromIntegral @_ @Integer . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

instance Finitary Int64 where
  type Cardinality Int64 = $(cardinalityOf @Int64)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral @_ @Int64 . subtract $(adjustmentOf @Int64) . fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite = fromIntegral . (+ $(adjustmentOf @Int64)) . fromIntegral @_ @Integer . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

-- Variable-width instances

-- | 'Int' has a finite number of inhabitants, varying by platform. This
-- instance will determine this when the library is built.
instance Finitary Int where
  type Cardinality Int = $(cardinalityOf @Int)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral @_ @Int . subtract $(adjustmentOf @Int) . fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite = fromIntegral . (+ $(adjustmentOf @Int)) . fromIntegral @_ @Integer . fromEnum
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

-- | 'Word' has a finite number of inhabitants, varying by platform. This
-- instance will determine this when the library is built.
instance Finitary Word where
  type Cardinality Word = $(cardinalityOf @Word)
  {-# INLINE fromFinite #-}
  fromFinite = fromIntegral
  {-# INLINE toFinite #-}
  toFinite = fromIntegral
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

-- | Since any type is isomorphic to itself, it follows that a \'valid\' @Finite
-- n@ (meaning that @n@ is a 'KnownNat') has finite cardinality.
instance (KnownNat n) => Finitary (Finite n) where
  type Cardinality (Finite n) = n
  {-# INLINE fromFinite #-}
  fromFinite = id
  {-# INLINE toFinite #-}
  toFinite = id
  {-# INLINE start #-}
  start = minBound
  {-# INLINE end #-}
  end = maxBound
  {-# INLINE next #-}
  next = guarded (== minBound) . inc
  {-# INLINE previous #-}
  previous = guarded (== maxBound) . dec
  {-# INLINE enumerateFrom #-}
  enumerateFrom = enumFrom
  {-# INLINE enumerateFromThen #-}
  enumerateFromThen = enumFromThen
  {-# INLINE enumerateFromTo #-}
  enumerateFromTo = enumFromTo
  {-# INLINE enumerateFromThenTo #-}
  enumerateFromThenTo = enumFromThenTo

-- | @Maybe a@ introduces one additional inhabitant (namely, 'Nothing') to @a@.
instance (Finitary a) => 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)

-- | 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, Finitary c) => 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, Finitary e) => 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 (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

instance (Finitary a) => Finitary (Sum a)

instance (Finitary a) => Finitary (Product a)

instance (Finitary a) => Finitary (Dual a)

instance (Finitary a) => Finitary (Last a)

instance (Finitary a) => Finitary (First a)

instance (Finitary a) => Finitary (Identity a)

instance (Finitary a) => Finitary (Max a)

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
  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
  {-# 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

instance (Finitary a, VUS.Unbox a, KnownNat n, Cardinality a <= Cardinality a ^ 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
  {-# 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

instance (Finitary a, Storable a, KnownNat n, Cardinality a <= Cardinality a ^ 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
  {-# 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

-- 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))

{-# INLINE inc #-}
inc :: (Num a) => a -> a
inc = (+ 1)

{-# INLINE dec #-}
dec :: (Num a) => a -> a
dec = subtract 1

{-# INLINE guarded #-}
guarded :: forall (a :: Type) (f :: Type -> Type) . (Alternative f) => (a -> Bool) -> a -> f a
guarded p x = bool empty (pure x) (p x)